diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean index 0a7e07c..a7b37f7 100644 --- a/Lampe/Lampe/Hoare/Builtins.lean +++ b/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⟩), ?_ diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean index 5ea8e0a..c6817d5 100644 --- a/Lampe/Lampe/Hoare/SepTotal.lean +++ b/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 diff --git a/Lampe/Lampe/Semantics.lean b/Lampe/Lampe/Semantics.lean index 7524970..650130e 100644 --- a/Lampe/Lampe/Semantics.lean +++ b/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 diff --git a/Lampe/Lampe/SeparationLogic/State.lean b/Lampe/Lampe/SeparationLogic/State.lean index 11295a4..460c7c8 100644 --- a/Lampe/Lampe/SeparationLogic/State.lean +++ b/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