Proof simplifications & additional lemmas

Lampe/Lampe/Hoare/Builtins.lean

@@ -17,13 +17,13 @@ theorem pureBuiltin_intro {A : Type} {a : A} {sgn desc args} :
   constructor
   cases em (desc a args).fst
   . apply Builtin.genericPureOmni.ok
-    . simp_all only [mapToValHeapCondition, SLP.true_star, exists_const]
+    . simp_all only [mapToVHCond, SLP.true_star, exists_const]
       apply SLP.ent_star_top
       simp_all only [SLP.true_star, exists_const]
     . tauto
   . apply Builtin.genericPureOmni.err
     . tauto
-    . simp_all [mapToValHeapCondition]
+    . simp_all [mapToVHCond]
 
 lemma pureBuiltin_intro_consequence
     {A : Type} {a : A} {sgn desc args} {Q : Tp.denote p outTp → Prop}
@@ -417,7 +417,7 @@ theorem writeRef_intro:
   apply And.intro
   . rename_i st₁ st₂ _ _
     have _ : r ∈ st₁.vals := by rw [hs]; tauto
-    simp_all [State.membership_in_val]
+    simp_all [State.mem_iff_mem_val]
   simp only [Finmap.insert_eq_singleton_union, ←Finmap.union_assoc, Finmap.union_singleton, SLP.star_assoc]
   rename_i st₁ st₂ _ _
   exists (⟨Finmap.singleton r ⟨tp, v'⟩, st₁.lambdas⟩), ?_

Lampe/Lampe/Hoare/SepTotal.lean

@@ -328,16 +328,13 @@ theorem callLambda_intro {lambdaBody} {P : SLP (State p)} {Q : Tp.denote p outTp
       obtain ⟨hi₁, _, _, hi₂⟩ := h₃
       simp only [State.lmbSingleton] at hi₂
       simp only [LawfulHeap.disjoint] at hi₁
-      obtain ⟨_, hj₁⟩ := hi₁
-      rw [hi₂] at hj₁
-      tauto
+      aesop
     simp [Finmap.lookup_union_right (by tauto)]
   . apply consequence <;> tauto
     apply consequence_frame_left
-    rotate_left 2
-    exact P
+    simp_all only [SLP.star_assoc]
     exact h
-    simp only [SLP.true_star, SLP.entails_self]
+    apply SLP.entails_self
 
 theorem lam_intro :
   STHoare p Γ ⟦⟧ (.lambda argTps outTp lambdaBody)
@@ -352,9 +349,8 @@ theorem lam_intro :
   exists ⟨∅, Finmap.singleton r lambda⟩, st
   refine ⟨?_, ?_, ?_, ?_⟩
   . simp only [LawfulHeap.disjoint]
-    refine ⟨?_, ?_⟩
-    . apply Finmap.disjoint_empty
-    . apply Finmap.singleton_disjoint_of_not_mem (by tauto)
+    refine ⟨?_, by simp_all⟩
+    apply Finmap.disjoint_empty
   . simp only [State.union_parts, State.mk.injEq]
     refine ⟨by simp_all, ?_⟩
     have hd : Finmap.Disjoint st.lambdas (Finmap.singleton r lambda) := by

Lampe/Lampe/Semantics.lean

@@ -61,7 +61,7 @@ inductive Omni : Env → State p → Expr (Tp.denote p) tp → (Option (State p
   (∀ ref, ref ∉ lambdas → Q (some (⟨vh, lambdas.insert ref ⟨argTps, outTp, lambdaBody⟩⟩, ref))) →
   Omni Γ ⟨vh, lambdas⟩ (Expr.lambda argTps outTp lambdaBody) Q
 | callBuiltin {Q} :
-    (b.omni p st argTypes resType args (mapToValHeapCondition st.lambdas Q)) →
+    (b.omni p st argTypes resType args (mapToVHCond st.lambdas Q)) →
     Omni Γ st (Expr.call h![] argTypes resType (.builtin b) args) Q
 | callDecl:
     (fname, fn) ∈ Γ.functions →
@@ -144,45 +144,29 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
     rename Builtin => b
     intros
     constructor
-    simp only [State.union_closures, State.union_vals]
     rename_i _ st₁ _ _ _ _ hd
+    simp only [State.union_parts, LawfulHeap.disjoint] at *
+    rw [mapToVHCond_iff_fun_match]
     have hf := b.frame hq (st₂ := st₂)
-    unfold mapToValHeapCondition at *
-    simp_all only [LawfulHeap.disjoint, true_implies]
+    simp_all only [true_implies]
     convert hf
-    funext
     rename Option _ → Prop => Q'
     casesm Option (ValHeap _ × _) <;> try rfl
     simp_all only [SLP.star, eq_iff_iff]
-    apply Iff.intro
-    all_goals (
+    apply Iff.intro <;> (
       intros hin
-      obtain ⟨s₁, ⟨s₂, ⟨hin₁, hin₂, hin₃, hin₄⟩⟩⟩ := hin
+      obtain ⟨s₁, ⟨s₂, ⟨hin₁, _, _, _⟩⟩⟩ := hin
     )
     . exists s₁, s₂
       simp only [LawfulHeap.disjoint] at *
-      refine ⟨by tauto, ?_, ?_, by tauto⟩
-      . simp only [State.union_parts] at hin₂
-        injection hin₂
+      refine ⟨by tauto, by simp_all, ?_, by tauto⟩
       . have hc : s₁.lambdas = st₁.lambdas := by
           obtain ⟨_, hd₂⟩ := hin₁
-          rw [State.union_parts] at hin₂
-          injection hin₂ with _ hu
-          rw [State.mk.injEq] at hin₄
-          obtain ⟨_, hin₀⟩ := hin₄
-          rw [←hin₀] at hu
-          obtain ⟨_, hd₁⟩ := hd
-          rw [←hin₀] at hd₁
-          rw [Finmap.union_cancel hd₁ hd₂] at hu
-          tauto
+          apply Finmap.union_cancel hd₂ ?_ |>.mp <;> simp_all
         rw [←hc]
         tauto
     . exists ⟨s₁, st₁.lambdas⟩, ⟨s₂, st₂.lambdas⟩
-      simp only [LawfulHeap.disjoint] at *
-      refine ⟨by tauto, ?_, by tauto, ?_⟩
-      . simp only [State.union_parts, State.mk.injEq]
-        tauto
-      . rw [hin₄]
+      refine ⟨by tauto, by simp_all, by tauto, by simp_all⟩
   | callDecl =>
     intro
     constructor
@@ -210,13 +194,9 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
   | callLambda h _ _ =>
     intro hd
     constructor <;> try tauto
-    simp_all
-    simp only [LawfulHeap.disjoint] at hd
-    simp only [Finmap.lookup_union_left (Finmap.mem_of_lookup_eq_some h)]
-    tauto
+    simp_all [LawfulHeap.disjoint, Finmap.lookup_union_left (Finmap.mem_of_lookup_eq_some h)]
   | lam =>
     intros h
-    simp only [LawfulHeap.disjoint, State.union_parts_left] at *
     obtain ⟨_, hd⟩ := h
     constructor
     intros
@@ -225,29 +205,13 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
     rename ValHeap _ => vh
     rename Ref => r
     generalize hL : (⟨_, _, _⟩ : Lambda _) = lambda
-    have hi : r ∉ lmbs ∧ r ∉ st₂.lambdas := by aesop
-    have hd₁ : Finmap.Disjoint lmbs (Finmap.singleton r lambda) := by
-      apply Finmap.Disjoint.symm
-      apply Finmap.singleton_disjoint_iff_not_mem.mpr
-      tauto
-    have hd₂ : Finmap.Disjoint (Finmap.singleton r lambda) st₂.lambdas := by
-      apply Finmap.singleton_disjoint_iff_not_mem.mpr
-      tauto
+    have hd : Finmap.Disjoint lmbs (Finmap.singleton r lambda) := by
+      simp_all [Finmap.Disjoint.symm, Finmap.singleton_disjoint_iff_not_mem]
     exists ⟨vh, lmbs ∪ Finmap.singleton r lambda⟩, st₂
     refine ⟨?_, ?_, ?_, by tauto⟩
-    . simp only [LawfulHeap.disjoint]
-      refine ⟨by tauto, ?_⟩
-      simp only [Finmap.disjoint_union_left]
-      tauto
-    . simp only [State.union_parts_left, State.mk.injEq]
-      refine ⟨by tauto, ?_⟩
-      simp only [Finmap.insert_eq_singleton_union]
-      simp only [Finmap.union_comm_of_disjoint hd₁, Finmap.union_assoc]
-    . simp [Finmap.union_comm_of_disjoint, Finmap.insert_eq_singleton_union]
-      rename (∀ref ∉ lmbs, _) => hQ
-      rw [hL] at hQ
-      simp only [Finmap.insert_eq_singleton_union] at hQ
-      rw [Finmap.union_comm_of_disjoint hd₁]
-      tauto
+    . simp_all [LawfulHeap.disjoint, Finmap.disjoint_union_left]
+    . simp_all [State.union_parts_left, Finmap.insert_eq_singleton_union, Finmap.union_comm_of_disjoint hd, Finmap.union_assoc]
+    . simp only
+      simp_all [Finmap.insert_eq_singleton_union, Finmap.union_comm_of_disjoint hd]
 
 end Lampe

Lampe/Lampe/SeparationLogic/State.lean

@@ -14,37 +14,37 @@ instance : Membership Ref (State p) where
   mem := fun a e => e ∈ a.vals
 
 @[simp]
-lemma State.membership_in_val {a : State p} : e ∈ a ↔ e ∈ a.vals := by rfl
+theorem State.mem_iff_mem_val {a : State p} : e ∈ a ↔ e ∈ a.vals := by rfl
 
 instance : Coe (State p) (ValHeap p) where
   coe := fun s => s.vals
 
 /-- Maps a post-condition on `State`s to a post-condition on `ValHeap`s by keeping the lambdas fixed -/
 @[reducible]
-def mapToValHeapCondition
-  (lambdas : Lambdas p)
-  (Q : Option (State p × T) → Prop) : Option (ValHeap p × T) → Prop :=
-  fun vv => Q (vv.map (fun (vals, t) => ⟨⟨vals, lambdas⟩, t⟩))
+def mapToVHCond (lambdas : Lambdas p) (Q : Option (State p × T) → Prop) : Option (ValHeap p × T) → Prop :=
+  fun vhv => Q (vhv.map (fun (vals, t) => ⟨⟨vals, lambdas⟩, t⟩))
 
-/-- Maps a post-condition on `ValHeap`s to a post-condition on `State`s -/
-@[reducible]
-def mapToStateCondition
-  (Q : Option (ValHeap p × T) → Prop) : Option (State p × T) → Prop :=
-  fun stv => Q (stv.map (fun (st, t) => ⟨st.vals, t⟩))
+@[simp]
+theorem mapToVHCond_some_iff {Q : Option (State p × T) → Prop} :
+  ((mapToVHCond lmbds Q) (some ⟨vh, v⟩)) ↔ (Q (some ⟨⟨vh, lmbds⟩, v⟩)) := by tauto
+
+@[simp]
+theorem mapToVHCond_none_iff {Q : Option (State p × T) → Prop} :
+  ((mapToVHCond lmbds Q) none) ↔ (Q none) := by tauto
+
+theorem mapToVHCond_iff_fun_match {Q : Option (State p × T) → Prop} :
+(mapToVHCond lmbds Q) =
+  (fun vhv => match vhv with
+    | none => Q none
+    | some (vh, v) => Q (some ⟨⟨vh, lmbds⟩, v⟩)) := by
+    unfold mapToVHCond
+    simp only
+    funext vhv
+    casesm Option (ValHeap _ × _) <;> rfl
 
 def State.insertVal (self : State p) (r : Ref) (v : AnyValue p) : State p :=
   ⟨self.vals.insert r v, self.lambdas⟩
 
-lemma State.eq_constructor {st₁ : State p} :
-  (st₁ = st₂) ↔ (State.mk st₁.vals st₁.lambdas = State.mk st₂.vals st₂.lambdas) := by
-  rfl
-
-@[simp]
-lemma State.eq_closures :
-  (State.mk v c = State.mk v' c') → (c = c') := by
-  intro h
-  injection h
-
 instance : LawfulHeap (State p) where
   union := fun a b => ⟨a.vals ∪ b.vals, a.lambdas ∪ b.lambdas⟩
   disjoint := fun a b => a.vals.Disjoint b.vals ∧ a.lambdas.Disjoint b.lambdas
@@ -55,18 +55,12 @@ instance : LawfulHeap (State p) where
   thm_union_assoc := by
     intros
     simp only [Union.union, State.mk.injEq]
-    apply And.intro
-    . apply Finmap.union_assoc
-    . apply Finmap.union_assoc
+    apply And.intro <;> apply Finmap.union_assoc
   thm_disjoint_symm_iff := by tauto
   thm_union_comm_of_disjoint := by
     intros
     simp only [Union.union, State.mk.injEq]
-    apply And.intro
-    . apply Finmap.union_comm_of_disjoint
-      tauto
-    . apply Finmap.union_comm_of_disjoint
-      tauto
+    apply And.intro <;> { apply Finmap.union_comm_of_disjoint; tauto }
   thm_disjoint_empty := by tauto
   thm_disjoint_union_left := by
     intros x y z
@@ -91,26 +85,26 @@ def State.lmbSingleton (r : Ref) (v : Lambda (Tp.denote p)) : SLP (State p) :=
 notation:max "[" "λ" l " ↦ " r "]" => State.lmbSingleton l r
 
 @[simp]
-lemma State.union_parts_left :
+theorem State.union_parts_left :
   (State.mk v c ∪ st₂ = State.mk (v ∪ st₂.vals) (c ∪ st₂.lambdas)) := by
   rfl
 
 @[simp]
-lemma State.union_parts_right :
+theorem State.union_parts_right :
   (st₂ ∪ State.mk v c = State.mk (st₂.vals ∪ v) (st₂.lambdas ∪ c)) := by
   rfl
 
 @[simp]
-lemma State.union_parts :
+theorem State.union_parts :
   st₁ ∪ st₂ = State.mk (st₁.vals ∪ st₂.vals) (st₁.lambdas ∪ st₂.lambdas) := by
   rfl
 
 @[simp]
-lemma State.union_vals {st₁ st₂ : State p} :
+theorem State.union_vals {st₁ st₂ : State p} :
   (st₁ ∪ st₂).vals = (st₁.vals ∪ st₂.vals) := by rfl
 
 @[simp]
-lemma State.union_closures {st₁ st₂ : State p} :
+theorem State.union_closures {st₁ st₂ : State p} :
   (st₁ ∪ st₂).lambdas = (st₁.lambdas ∪ st₂.lambdas) := by rfl
 
 end Lampe