lawfulheap lemmas moved into namespace. class props now have a "thm_"…

… prefix to distinguish them

Lampe/Lampe/Hoare/Builtins.lean

@@ -356,9 +356,9 @@ theorem ref_intro:
   simp only [SLP.true_star]
   intro st hH r hr
   exists (⟨Finmap.singleton r ⟨tp, v⟩, st.lambdas⟩ ∪ st), ∅
-  apply And.intro (by rw [LawfulHeap.disjoint_symm_iff]; apply LawfulHeap.disjoint_empty)
+  apply And.intro (by rw [LawfulHeap.disjoint_symm_iff]; apply LawfulHeap.empty_disjoint)
   constructor
-  . simp only [State.insertVal, Finmap.insert_eq_singleton_union, LawfulHeap_union_empty]
+  . simp only [State.insertVal, Finmap.insert_eq_singleton_union, LawfulHeap.union_empty]
     simp only [State.union_parts_left, Finmap.union_self]
   . apply And.intro ?_ (by simp)
     exists (⟨Finmap.singleton r ⟨tp, v⟩, ∅⟩), st

Lampe/Lampe/SeparationLogic/LawfulHeap.lean

@@ -7,69 +7,73 @@ class LawfulHeap (α : Type _) where
   disjoint : α → α → Prop
   empty : α
 
-  union_empty {a : α} : union a empty = a
-  union_assoc {s₁ s₂ s₃ : α} : union (union s₁ s₂) s₃ = union s₁ (union s₂ s₃)
-  disjoint_symm_iff {a b : α} : disjoint a b ↔ disjoint b a
-  union_comm_of_disjoint {s₁ s₂ : α} : disjoint s₁ s₂ → union s₁ s₂ = union s₂ s₁
-  disjoint_union_left (x y z : α) : disjoint (union x y) z ↔ disjoint x z ∧ disjoint y z
-  disjoint_empty (x : α) : disjoint empty x
+  private thm_union_empty {a : α} : union a empty = a
+  private thm_union_assoc {s₁ s₂ s₃ : α} : union (union s₁ s₂) s₃ = union s₁ (union s₂ s₃)
+  private thm_disjoint_symm_iff {a b : α} : disjoint a b ↔ disjoint b a
+  private thm_union_comm_of_disjoint {s₁ s₂ : α} : disjoint s₁ s₂ → union s₁ s₂ = union s₂ s₁
+  private thm_disjoint_union_left (x y z : α) : disjoint (union x y) z ↔ disjoint x z ∧ disjoint y z
+  private thm_disjoint_empty (x : α) : disjoint empty x
 
 instance [LawfulHeap α] : Union α := ⟨LawfulHeap.union⟩
 instance [LawfulHeap α] : EmptyCollection α := ⟨LawfulHeap.empty⟩
 
-theorem LawfulHeap_union_empty_commutative [LawfulHeap α] {a : α} :
-  a ∪ ∅ = ∅ ∪ a := by
-  have h := LawfulHeap.disjoint_empty a
-  simp [Union.union, EmptyCollection.emptyCollection]
-  rw [LawfulHeap.union_comm_of_disjoint h]
+theorem LawfulHeap.disjoint_symm_iff [LawfulHeap α] {s₁ s₂ : α} :
+  LawfulHeap.disjoint s₁ s₂ ↔ LawfulHeap.disjoint s₂ s₁ := by
+  exact LawfulHeap.thm_disjoint_symm_iff
 
-theorem LawfulHeap_union_comm_of_disjoint [LawfulHeap α] {s₁ s₂ : α}:
+theorem LawfulHeap.union_comm_of_disjoint_ [LawfulHeap α] {s₁ s₂ : α} :
   LawfulHeap.disjoint s₁ s₂ → s₁ ∪ s₂ = s₂ ∪ s₁ := by
   simp [Union.union]
-  exact LawfulHeap.union_comm_of_disjoint
+  exact LawfulHeap.thm_union_comm_of_disjoint
+
+theorem LawfulHeap.union_empty_comm [LawfulHeap α] {a : α} :
+  a ∪ ∅ = ∅ ∪ a := by
+  have h := LawfulHeap.thm_disjoint_empty a
+  simp [Union.union, EmptyCollection.emptyCollection]
+  rw [LawfulHeap.thm_union_comm_of_disjoint h]
 
 @[simp]
-theorem LawfulHeap_disjoint_empty [LawfulHeap α] {a : α} :
-  LawfulHeap.disjoint a ∅ := by
-   rw [LawfulHeap.disjoint_symm_iff]
-   apply LawfulHeap.disjoint_empty
+theorem LawfulHeap.union_empty [LawfulHeap α] {a : α} :
+  a ∪ ∅ = a := by
+  apply LawfulHeap.thm_union_empty
 
 @[simp]
-theorem LawfulHeap_empty_disjoint [LawfulHeap α] {a : α} :
-  LawfulHeap.disjoint ∅ a := by
-   apply LawfulHeap.disjoint_empty
+theorem LawfulHeap.empty_union [LawfulHeap α] {a : α} :
+  ∅ ∪ a = a := by
+  rw [←LawfulHeap.union_empty_comm]
+  apply LawfulHeap.thm_union_empty
 
 @[simp]
-theorem LawfulHeap_union_empty [LawfulHeap α] {a : α} :
-  a ∪ ∅ = a := by
-  apply LawfulHeap.union_empty
+theorem LawfulHeap.disjoint_empty [LawfulHeap α] {a : α} :
+  LawfulHeap.disjoint a ∅ := by
+   rw [LawfulHeap.thm_disjoint_symm_iff]
+   apply LawfulHeap.thm_disjoint_empty
 
 @[simp]
-theorem LawfulHeap_empty_union [LawfulHeap α] {a : α} :
-  ∅ ∪ a = a := by
-  rw [←LawfulHeap_union_empty_commutative]
-  apply LawfulHeap.union_empty
+theorem LawfulHeap.empty_disjoint [LawfulHeap α] {a : α} :
+  LawfulHeap.disjoint ∅ a := by
+   apply LawfulHeap.thm_disjoint_empty
 
-theorem LawfulHeap_union_assoc [LawfulHeap α] {s₁ s₂ s₃ : α} :
+theorem LawfulHeap.union_assoc [LawfulHeap α] {s₁ s₂ s₃ : α} :
   s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) := by
   simp [Union.union]
-  apply LawfulHeap.union_assoc
+  apply LawfulHeap.thm_union_assoc
 
-theorem LawfulHeap_disjoint_union_left [LawfulHeap α] (x y z : α) :
+theorem LawfulHeap.disjoint_union_left [LawfulHeap α] (x y z : α) :
   LawfulHeap.disjoint (x ∪ y) z ↔ LawfulHeap.disjoint x z ∧ LawfulHeap.disjoint y z := by
   simp [Union.union]
-  apply LawfulHeap.disjoint_union_left
+  apply LawfulHeap.thm_disjoint_union_left
 
-theorem LawfulHeap_disjoint_union_right [LawfulHeap α] (x y z : α) :
+theorem LawfulHeap.disjoint_union_right [LawfulHeap α] (x y z : α) :
   LawfulHeap.disjoint x (y ∪ z) ↔ LawfulHeap.disjoint x y ∧ LawfulHeap.disjoint x z := by
   conv =>
     lhs
-    rw [LawfulHeap.disjoint_symm_iff]
+    rw [LawfulHeap.thm_disjoint_symm_iff]
   conv =>
     rhs
-    rw [LawfulHeap.disjoint_symm_iff]
+    rw [LawfulHeap.thm_disjoint_symm_iff]
     rhs
-    rw [LawfulHeap.disjoint_symm_iff]
-  apply LawfulHeap.disjoint_union_left
+    rw [LawfulHeap.thm_disjoint_symm_iff]
+  apply LawfulHeap.thm_disjoint_union_left
 
 end Lampe

Lampe/Lampe/SeparationLogic/SLP.lean

@@ -76,8 +76,8 @@ theorem pure_right [LawfulHeap α] {H₁ H₂ : SLP α} : P → (H₁ ⊢ H₂)
   apply And.intro rfl
   apply_assumption
   assumption
-  . simp only [LawfulHeap_empty_union]
-  . apply LawfulHeap.disjoint_empty
+  . simp only [LawfulHeap.empty_union]
+  . apply LawfulHeap.empty_disjoint
 
 theorem entails_self [LawfulHeap α] {H : SLP α} : H ⊢ H := by tauto
 
@@ -108,7 +108,7 @@ theorem star_comm [LawfulHeap α] {G H : SLP α} : (G ⋆ H) = (H ⋆ G) := by
     repeat apply Exists.intro
     rw [LawfulHeap.disjoint_symm_iff]
     apply And.intro (by assumption)
-    rw [LawfulHeap_union_comm_of_disjoint (by rw [LawfulHeap.disjoint_symm_iff]; assumption)]
+    rw [LawfulHeap.union_comm_of_disjoint_ (by rw [LawfulHeap.disjoint_symm_iff]; assumption)]
     tauto
   }
 
@@ -134,8 +134,8 @@ theorem star_assoc [LawfulHeap α] {F G H : SLP α} : ((F ⋆ G) ⋆ H) = (F ⋆
   apply Iff.intro
   · intro_cases
     subst_vars
-    rw [LawfulHeap_union_assoc]
-    simp only [LawfulHeap_disjoint_union_left] at *
+    rw [LawfulHeap.union_assoc]
+    simp only [LawfulHeap.disjoint_union_left] at *
     cases_type And
     repeat apply Exists.intro
     apply And.intro ?_
@@ -146,11 +146,11 @@ theorem star_assoc [LawfulHeap α] {F G H : SLP α} : ((F ⋆ G) ⋆ H) = (F ⋆
     apply And.intro rfl
     simp_all
     assumption
-    simp_all [LawfulHeap_disjoint_union_right]
+    simp_all [LawfulHeap.disjoint_union_right]
   · intro_cases
     subst_vars
-    rw [←LawfulHeap_union_assoc]
-    simp only [LawfulHeap_disjoint_union_right] at *
+    rw [←LawfulHeap.union_assoc]
+    simp only [LawfulHeap.disjoint_union_right] at *
     cases_type And
     repeat apply Exists.intro
     apply And.intro ?_
@@ -161,7 +161,7 @@ theorem star_assoc [LawfulHeap α] {F G H : SLP α} : ((F ⋆ G) ⋆ H) = (F ⋆
     apply And.intro rfl
     simp_all
     assumption
-    simp_all [LawfulHeap_disjoint_union_left]
+    simp_all [LawfulHeap.disjoint_union_left]
 
 @[simp]
 theorem ent_star_top [LawfulHeap α] {H : SLP α} : H ⊢ H ⋆ ⊤ := by
@@ -188,7 +188,7 @@ theorem star_mono_l' [LawfulHeap α] {P Q : SLP α} : (⟦⟧ ⊢ Q) → (P ⊢
   tauto
   simp
   rw [LawfulHeap.disjoint_symm_iff]
-  apply LawfulHeap.disjoint_empty
+  apply LawfulHeap.empty_disjoint
 
 theorem star_mono [LawfulHeap α] {H₁ H₂ Q₁ Q₂ : SLP α} : (H₁ ⊢ H₂) → (Q₁ ⊢ Q₂) → (H₁ ⋆ Q₁ ⊢ H₂ ⋆ Q₂) := by
   unfold star entails
@@ -239,7 +239,7 @@ theorem wand_self_star [LawfulHeap α] {H : SLP α}: (H -⋆ H ⋆ top) = top :=
     simp
     rotate_left
     rotate_left
-    rw [LawfulHeap_union_comm_of_disjoint (by assumption)]
+    rw [LawfulHeap.union_comm_of_disjoint_ (by assumption)]
     rw [LawfulHeap.disjoint_symm_iff]
     assumption
 
@@ -256,7 +256,7 @@ theorem wand_cancel [LawfulHeap α] {P Q : SLP α} : (P ⋆ (P -⋆ Q)) ⊢ Q :=
   intro_cases
   subst_vars
   rename_i h
-  rw [LawfulHeap_union_comm_of_disjoint (by assumption)]
+  rw [LawfulHeap.union_comm_of_disjoint_ (by assumption)]
   apply_assumption
   rw [LawfulHeap.disjoint_symm_iff]
   tauto

Lampe/Lampe/SeparationLogic/State.lean

@@ -49,26 +49,26 @@ 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
   empty := ⟨∅, ∅⟩
-  union_empty := by
+  thm_union_empty := by
     intros
     simp only [Finmap.union_empty]
-  union_assoc := by
+  thm_union_assoc := by
     intros
     simp only [Union.union, State.mk.injEq]
     apply And.intro
     . apply Finmap.union_assoc
     . apply Finmap.union_assoc
-  disjoint_symm_iff := by tauto
-  union_comm_of_disjoint := by
+  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
-  disjoint_empty := by tauto
-  disjoint_union_left := by
+  thm_disjoint_empty := by tauto
+  thm_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.lambdas y.lambdas z.lambdas)

Lampe/Lampe/SeparationLogic/ValHeap.lean

@@ -33,11 +33,11 @@ instance : LawfulHeap (ValHeap p) where
   union := fun a b => a ∪ b
   disjoint := fun a b => a.Disjoint b
   empty := ∅
-  union_empty := Finmap.union_empty
-  union_assoc := Finmap.union_assoc
-  disjoint_symm_iff := by tauto
-  union_comm_of_disjoint := Finmap.union_comm_of_disjoint
-  disjoint_union_left := Finmap.disjoint_union_left
-  disjoint_empty := Finmap.disjoint_empty
+  thm_union_empty := Finmap.union_empty
+  thm_union_assoc := Finmap.union_assoc
+  thm_disjoint_symm_iff := by tauto
+  thm_union_comm_of_disjoint := Finmap.union_comm_of_disjoint
+  thm_disjoint_union_left := Finmap.disjoint_union_left
+  thm_disjoint_empty := Finmap.disjoint_empty
 
 end Lampe

Lampe/Lampe/Tactic/SeparationLogic.lean

@@ -317,7 +317,7 @@ theorem exi_prop_l [LawfulHeap α] {P : Prop} {H : P → SLP α} {Q : SLP α} :
   apply h
   use ∅, st
   refine ⟨?_, ?_, ?_, ?_⟩
-  apply LawfulHeap.disjoint_empty
+  apply LawfulHeap.empty_disjoint
   all_goals simp_all [LawfulHeap.disjoint_empty, SLP.lift]
 
 theorem use_right [LawfulHeap α] {R L G H : SLP α} : (R ⊢ G ⋆ H) → (L ⋆ R ⊢ G ⋆ L ⋆ H) := by