"Closure" renamed to "lambda" across the project for precision

Lampe/Lampe.lean

@@ -97,7 +97,9 @@ nr_def simple_lambda<>(x : Field) -> Field {
   ^foo(x) : Field;
 }
 
-example {p Γ x} : STHoare p Γ ⟦⟧ (simple_lambda.fn.body (Tp.denote p) h![] h![x]) fun v => v = x := by
+example {p Γ x} : STHoare p Γ ⟦⟧ (simple_lambda.fn.body (Tp.denote p) h![] h![x])
+  fun v => v = x := by
   simp only [simple_lambda]
   steps <;> try tauto
-  all_goals sorry
+  . apply STHoare.var_intro
+  . sorry -- unsolvable

Lampe/Lampe/Hoare/Builtins.lean

@@ -355,7 +355,7 @@ theorem ref_intro:
   apply THoare.consequence ?_ THoare.ref_intro (fun _ => SLP.entails_self)
   simp only [SLP.true_star]
   intro st hH r hr
-  exists (⟨Finmap.singleton r ⟨tp, v⟩, st.closures⟩ ∪ st), ∅
+  exists (⟨Finmap.singleton r ⟨tp, v⟩, st.lambdas⟩ ∪ st), ∅
   apply And.intro (by rw [LawfulHeap.disjoint_symm_iff]; apply LawfulHeap.disjoint_empty)
   constructor
   . simp only [State.insertVal, Finmap.insert_eq_singleton_union, LawfulHeap_union_empty]
@@ -395,7 +395,7 @@ theorem readRef_intro:
     apply Option.isSome_some
   simp only [SLP.true_star, SLP.star_assoc]
   rename_i st₁ st₂ _ _
-  exists (⟨Finmap.singleton r ⟨tp, v⟩, st₁.closures⟩), ?_
+  exists (⟨Finmap.singleton r ⟨tp, v⟩, st₁.lambdas⟩), ?_
   unfold State.valSingleton at hs
   rw [←hs]
   repeat apply And.intro (by tauto)
@@ -420,7 +420,7 @@ theorem writeRef_intro:
     simp_all [State.membership_in_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₁.closures⟩), ?_
+  exists (⟨Finmap.singleton r ⟨tp, v'⟩, st₁.lambdas⟩), ?_
   refine ⟨?_, ?_, ?_, (by apply SLP.ent_star_top; assumption)⟩
   . simp only [LawfulHeap.disjoint] at *
     have _ : r ∉ st₂.vals := by

Lampe/Lampe/Hoare/SepTotal.lean

@@ -348,11 +348,11 @@ theorem newLambda_intro :
     . apply Finmap.singleton_disjoint_of_not_mem (by tauto)
   . simp only [State.union_parts, State.mk.injEq]
     refine ⟨by simp_all, ?_⟩
-    have hd : Finmap.Disjoint st.closures (Finmap.singleton r lambda) := by
+    have hd : Finmap.Disjoint st.lambdas (Finmap.singleton r lambda) := by
       rw [Finmap.Disjoint.symm_iff]
       apply Finmap.singleton_disjoint_of_not_mem (by assumption)
     simp only [Finmap.insert_eq_singleton_union, Finmap.union_comm_of_disjoint hd]
-  . unfold State.clsSingleton
+  . unfold State.lmbSingleton
     tauto
   . apply SLP.ent_star_top
     tauto

Lampe/Lampe/Hoare/Total.lean

@@ -43,7 +43,7 @@ theorem letIn_intro {P Q}
 
 theorem ref_intro {v P} :
     THoare p Γ
-      (fun st => ∀r, r ∉ st → P r ⟨(st.vals.insert r ⟨tp, v⟩), st.closures⟩)
+      (fun st => ∀r, r ∉ st → P r ⟨(st.vals.insert r ⟨tp, v⟩), st.lambdas⟩)
       (.call h![] [tp] (Tp.ref tp) (.builtin .ref) h![v])
       P := by
   unfold THoare
@@ -64,7 +64,7 @@ theorem readRef_intro {ref} :
 
 theorem writeRef_intro {ref v} :
     THoare p Γ
-      (fun st => ref ∈ st ∧ P () ⟨(st.vals.insert ref ⟨tp, v⟩), st.closures⟩)
+      (fun st => ref ∈ st ∧ P () ⟨(st.vals.insert ref ⟨tp, v⟩), st.lambdas⟩)
       (.call h![] [tp.ref, tp] .unit (.builtin .writeRef) h![ref, v])
       P := by
   unfold THoare

Lampe/Lampe/Semantics.lean

@@ -35,7 +35,7 @@ inductive Omni : (p : Prime) → Env → State p → Expr (Tp.denote p) tp → (
   (Q₁ none → Q none) →
   Omni p Γ st (.letIn e b) Q
 | callBuiltin {st : State p} {Q : Option (State p × Tp.denote p resType) → Prop} :
-  (b.omni p st.vals argTypes resType args (mapToValHeapCondition st.closures Q)) →
+  (b.omni p st.vals argTypes resType args (mapToValHeapCondition st.lambdas Q)) →
   Omni p Γ st (Expr.call h![] argTypes resType (.builtin b) args) Q
 | callDecl :
   Γ fname = some fn →
@@ -44,13 +44,13 @@ inductive Omni : (p : Prime) → Env → State p → Expr (Tp.denote p) tp → (
   (htco : fn.outTp (hkc ▸ generics) = res) →
   Omni p Γ st (htco ▸ fn.body _ (hkc ▸ generics) (htci ▸ args)) Q →
   Omni p Γ st (@Expr.call _ tyKinds generics argTypes res (.decl fname) args) Q
-| callLambda {cls : Closures} :
-  cls.lookup ref = some ⟨Tp.denote p, argTps, outTp, lambdaBody⟩ →
-  Omni p Γ ⟨vh, cls⟩ (lambdaBody args) Q →
-  Omni p Γ ⟨vh, cls⟩ (Expr.call h![] argTps outTp (.lambda ref) args) Q
+| callLambda {lambdas : Lambdas} :
+  lambdas.lookup ref = some ⟨Tp.denote p, argTps, outTp, lambdaBody⟩ →
+  Omni p Γ ⟨vh, lambdas⟩ (lambdaBody args) Q →
+  Omni p Γ ⟨vh, lambdas⟩ (Expr.call h![] argTps outTp (.lambda ref) args) Q
 | newLambda {Q} :
-  (∀ ref, ref ∉ cls → Q (some (⟨vh, cls.insert ref ⟨_, argTps, outTp, lambdaBody⟩⟩, ref))) →
-  Omni p Γ ⟨vh, cls⟩ (.lambda argTps outTp lambdaBody) Q
+  (∀ ref, ref ∉ lambdas → Q (some (⟨vh, lambdas.insert ref ⟨_, argTps, outTp, lambdaBody⟩⟩, ref))) →
+  Omni p Γ ⟨vh, lambdas⟩ (Expr.lambda argTps outTp lambdaBody) Q
 | loopDone :
   lo ≥ hi →
   Omni p Γ st (.loop lo hi body) Q
@@ -137,7 +137,7 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
       refine ⟨by tauto, ?_, ?_, by tauto⟩
       . simp only [State.union_parts] at hin₂
         injection hin₂
-      . have hc : s₁.closures = st₁.closures := by
+      . have hc : s₁.lambdas = st₁.lambdas := by
           obtain ⟨_, hd₂⟩ := hin₁
           rw [State.union_parts] at hin₂
           injection hin₂ with _ hu
@@ -150,7 +150,7 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
           tauto
         rw [←hc]
         tauto
-    . exists ⟨s₁, st₁.closures⟩, ⟨s₂, st₂.closures⟩
+    . 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]
@@ -189,19 +189,19 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
     constructor
     intros
     simp only
-    rename Closures => cls
+    rename Lambdas => lmbs
     rename ValHeap _ => vh
     rename Ref => r
     generalize hL : (⟨_, _, _, _⟩ : Lambda) = lambda
-    have hi : r ∉ cls ∧ r ∉ st₂.closures := by aesop
-    have hd₁ : Finmap.Disjoint cls (Finmap.singleton r lambda) := by
+    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₂.closures := by
+    have hd₂ : Finmap.Disjoint (Finmap.singleton r lambda) st₂.lambdas := by
       apply Finmap.singleton_disjoint_iff_not_mem.mpr
       tauto
-    exists ⟨vh, cls ∪ Finmap.singleton r lambda⟩, st₂
+    exists ⟨vh, lmbs ∪ Finmap.singleton r lambda⟩, st₂
     refine ⟨?_, ?_, ?_, by tauto⟩
     . simp only [LawfulHeap.disjoint]
       refine ⟨by tauto, ?_⟩
@@ -212,7 +212,7 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
       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 ∉ cls, _) => hQ
+      rename (∀ref ∉ lmbs, _) => hQ
       rw [hL] at hQ
       simp only [Finmap.insert_eq_singleton_union] at hQ
       rw [Finmap.union_comm_of_disjoint hd₁]

Lampe/Lampe/SeparationLogic/State.lean

@@ -4,11 +4,11 @@ import Lampe.Ast
 
 namespace Lampe
 
-abbrev Closures := Finmap fun _ : Ref => Lambda
+abbrev Lambdas := Finmap fun _ : Ref => Lambda
 
 structure State (p : Prime) where
   vals : ValHeap p
-  closures : Closures
+  lambdas : Lambdas
 
 instance : Membership Ref (State p) where
   mem := fun a e => e ∈ a.vals
@@ -19,12 +19,12 @@ lemma State.membership_in_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 closures fixed -/
+/-- Maps a post-condition on `State`s to a post-condition on `ValHeap`s by keeping the lambdas fixed -/
 @[reducible]
 def mapToValHeapCondition
-  (closures : Closures)
+  (lambdas : Lambdas)
   (Q : Option (State p × T) → Prop) : Option (ValHeap p × T) → Prop :=
-  fun vv => Q (vv.map (fun (vals, t) => ⟨⟨vals, closures⟩, t⟩))
+  fun vv => Q (vv.map (fun (vals, t) => ⟨⟨vals, lambdas⟩, t⟩))
 
 /-- Maps a post-condition on `ValHeap`s to a post-condition on `State`s -/
 @[reducible]
@@ -33,10 +33,10 @@ def mapToStateCondition
   fun stv => Q (stv.map (fun (st, t) => ⟨st.vals, t⟩))
 
 def State.insertVal (self : State p) (r : Ref) (v : AnyValue p) : State p :=
-  ⟨self.vals.insert r v, self.closures⟩
+  ⟨self.vals.insert r v, self.lambdas⟩
 
 lemma State.eq_constructor {st₁ : State p} :
-  (st₁ = st₂) ↔ (State.mk st₁.vals st₁.closures = State.mk st₂.vals st₂.closures) := by
+  (st₁ = st₂) ↔ (State.mk st₁.vals st₁.lambdas = State.mk st₂.vals st₂.lambdas) := by
   rfl
 
 @[simp]
@@ -46,8 +46,8 @@ lemma State.eq_closures :
   injection h
 
 instance : LawfulHeap (State p) where
-  union := fun a b => ⟨a.vals ∪ b.vals, a.closures ∪ b.closures⟩
-  disjoint := fun a b => a.vals.Disjoint b.vals ∧ a.closures.Disjoint b.closures
+  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
   empty := ⟨∅, ∅⟩
   union_empty := by
     intros
@@ -71,7 +71,7 @@ instance : LawfulHeap (State p) where
   disjoint_union_left := by
     intros x y z
     have h1 := (Finmap.disjoint_union_left x.vals y.vals z.vals)
-    have h2 := (Finmap.disjoint_union_left x.closures y.closures z.closures)
+    have h2 := (Finmap.disjoint_union_left x.lambdas y.lambdas z.lambdas)
     constructor
     intro h3
     simp only [Union.union] at h3
@@ -85,24 +85,24 @@ def State.valSingleton (r : Ref) (v : AnyValue p) : SLP (State p) :=
 notation:max "[" l " ↦ " r "]" => State.valSingleton l r
 
 @[reducible]
-def State.clsSingleton (r : Ref) (v : Lambda) : SLP (State p) :=
-  fun st => st.closures = Finmap.singleton r v
+def State.lmbSingleton (r : Ref) (v : Lambda) : SLP (State p) :=
+  fun st => st.lambdas = Finmap.singleton r v
 
-notation:max "[" l " ↣ " r "]" => State.clsSingleton l r
+notation:max "[" l " ↣ " r "]" => State.lmbSingleton l r
 
 @[simp]
 lemma State.union_parts_left :
-  (State.mk v c ∪ st₂ = State.mk (v ∪ st₂.vals) (c ∪ st₂.closures)) := by
+  (State.mk v c ∪ st₂ = State.mk (v ∪ st₂.vals) (c ∪ st₂.lambdas)) := by
   rfl
 
 @[simp]
 lemma State.union_parts_right :
-  (st₂ ∪ State.mk v c = State.mk (st₂.vals ∪ v) (st₂.closures ∪ c)) := by
+  (st₂ ∪ State.mk v c = State.mk (st₂.vals ∪ v) (st₂.lambdas ∪ c)) := by
   rfl
 
 @[simp]
 lemma State.union_parts :
-  st₁ ∪ st₂ = State.mk (st₁.vals ∪ st₂.vals) (st₁.closures ∪ st₂.closures) := by
+  st₁ ∪ st₂ = State.mk (st₁.vals ∪ st₂.vals) (st₁.lambdas ∪ st₂.lambdas) := by
   rfl
 
 @[simp]
@@ -111,6 +111,6 @@ lemma State.union_vals {st₁ st₂ : State p} :
 
 @[simp]
 lemma State.union_closures {st₁ st₂ : State p} :
-  (st₁ ∪ st₂).closures = (st₁.closures ∪ st₂.closures) := by rfl
+  (st₁ ∪ st₂).lambdas = (st₁.lambdas ∪ st₂.lambdas) := by rfl
 
 end Lampe

Lampe/Lampe/Tactic/SeparationLogic.lean

@@ -14,7 +14,7 @@ inductive SLTerm where
 | star : Expr → SLTerm → SLTerm → SLTerm
 | lift : Expr → SLTerm
 | singleton : Expr → Expr → SLTerm
-| clsSingleton : Expr → Expr → SLTerm
+| lmbSingleton : Expr → Expr → SLTerm
 | mvar : Expr → SLTerm
 | all : Expr → SLTerm
 | exi : Expr → SLTerm
@@ -29,7 +29,7 @@ def SLTerm.toString : SLTerm → String
 | star _ a b => s!"({a.toString} ⋆ {b.toString})"
 | lift e => s!"⟦{e.dbgToString}⟧"
 | singleton e₁ _ => s!"[{e₁.dbgToString} ↦ _]"
-| clsSingleton e₁ _ => s!"[{e₁.dbgToString} ↣ _]"
+| lmbSingleton e₁ _ => s!"[{e₁.dbgToString} ↣ _]"
 | mvar e => s!"MV{e.dbgToString}"
 | unrecognized e => s!"<unrecognized: {e.dbgToString}>"
 
@@ -189,11 +189,11 @@ partial def parseSLExpr (e: Expr): TacticM SLTerm := do
     let fst ← args[1]?
     let snd ← args[2]?
     return SLTerm.singleton fst snd
-  else if e.isAppOf ``State.clsSingleton then
+  else if e.isAppOf ``State.lmbSingleton then
     let args := e.getAppArgs
     let fst ← args[1]?
     let snd ← args[2]?
-    return SLTerm.clsSingleton fst snd
+    return SLTerm.lmbSingleton fst snd
   else if e.isAppOf ``SLP.top then
     return SLTerm.top
   else if e.isAppOf ``SLP.lift then
@@ -333,7 +333,7 @@ theorem singleton_congr_mv {p} {r} {v₁ v₂ : AnyValue p} : (v₁ = v₂) →
   simp
   apply SLP.entails_self
 
-theorem clsSingleton_congr_mv {p} {r} {l₁ l₂ : Lambda} : (l₁ = l₂) → (([r ↣ l₁] : SLP (State p)) ⊢ [r ↣ l₂] ⋆ ⟦⟧) := by
+theorem lmbSingleton_congr_mv {p} {r} {l₁ l₂ : Lambda} : (l₁ = l₂) → (([r ↣ l₁] : SLP (State p)) ⊢ [r ↣ l₂] ⋆ ⟦⟧) := by
   rintro rfl
   simp
   apply SLP.entails_self
@@ -343,7 +343,7 @@ theorem singleton_star_congr {p} {r} {v₁ v₂ : AnyValue p} {R} : (v₁ = v₂
   rintro rfl
   apply SLP.entails_self
 
-theorem clsSingleton_star_congr {p} {r} {v₁ v₂ : Lambda} {R : SLP (State p)} :
+theorem lmbSingleton_star_congr {p} {r} {v₁ v₂ : Lambda} {R : SLP (State p)} :
   (v₁ = v₂) → ([r ↣ v₁] ⋆ R ⊢ [r ↣ v₂] ⋆ R) := by
   rintro rfl
   apply SLP.entails_self
@@ -365,9 +365,9 @@ partial def solveSingletonStarMV (goal : MVarId) (lhs : SLTerm) (rhs : Expr): Ta
         catch _ => pure [newGoal]
       pure $ newGoal ++ newGoals
     else throwError "not equal"
-  | SLTerm.clsSingleton v _ =>
+  | SLTerm.lmbSingleton v _ =>
     if v == rhs then
-      let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``clsSingleton_congr_mv)
+      let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``lmbSingleton_congr_mv)
       let newGoal ← newGoals[0]?
       let newGoal ← try newGoal.refl; pure []
         catch _ => pure [newGoal]
@@ -388,10 +388,10 @@ partial def solveSingletonStarMV (goal : MVarId) (lhs : SLTerm) (rhs : Expr): Ta
         let newGoal ← newGoals[0]?
         let new' ← solveSingletonStarMV newGoal r rhs
         return new' ++ newGoals
-    | SLTerm.clsSingleton v _ => do
+    | SLTerm.lmbSingleton v _ => do
       if v == rhs then
         -- [TODO] This should use EQ, not ent_self as well
-        let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``clsSingleton_star_congr)
+        let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``lmbSingleton_star_congr)
         let newGoal ← newGoals[0]?
         let newGoal ← try newGoal.refl; pure []
           catch _ => pure [newGoal]
@@ -432,14 +432,14 @@ partial def solvePureStarMV (goal : MVarId) (lhs : SLTerm): TacticM (List MVarId
       return ng ++ goals
   | .singleton _ _ =>
       goal.apply (←mkConstWithFreshMVarLevels ``skip_evidence_pure)
-  | .clsSingleton _ _ =>
+  | .lmbSingleton _ _ =>
       goal.apply (←mkConstWithFreshMVarLevels ``skip_evidence_pure)
   | _ => throwError "not a lift {lhs}"
 
 partial def solveStarMV (goal : MVarId) (lhs : SLTerm) (rhsNonMv : SLTerm): TacticM (List MVarId) := do
   match rhsNonMv with
   | .singleton v _ => solveSingletonStarMV goal lhs v
-  | .clsSingleton v _ => solveSingletonStarMV goal lhs v
+  | .lmbSingleton v _ => solveSingletonStarMV goal lhs v
   | .lift _ => solvePureStarMV goal lhs
   | _ => throwError "not a singleton srry {rhsNonMv}"