From fd39af50084d0de9ecd1b8f47426e2bba1427191 Mon Sep 17 00:00:00 2001 From: utkn Date: Wed, 4 Dec 2024 18:57:07 +0300 Subject: [PATCH] some proof simplifications --- Lampe/Lampe/Hoare/SepTotal.lean | 5 ++--- Lampe/Lampe/Semantics.lean | 16 +++------------- 2 files changed, 5 insertions(+), 16 deletions(-) diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean index bb9dfd9..45509db 100644 --- 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 index 3c7dd1a..a48d6d7 100644 --- 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