some proof simplifications

reilabs · Dec 4, 2024 · fd39af5 · fd39af5
1 parent 327a194
commit fd39af5
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 16 deletions.
diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean
@@ -352,9 +352,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

diff --git a/Lampe/Lampe/Semantics.lean b/Lampe/Lampe/Semantics.lean
@@ -162,26 +162,16 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
     . exists s₁, s₂
       simp only [LawfulHeap.disjoint] at *
       refine ⟨by tauto, ?_, ?_, by tauto⟩
-      . simp only [State.union_parts] at hin₂
-        injection hin₂
+      . simp_all
       . 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
+      . simp_all
       . rw [hin₄]
   | callDecl =>
     intro