callLambda intro updated and proven

reilabs · Nov 26, 2024 · 427f728 · 427f728
1 parent fbca229
commit 427f728
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 13 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -100,6 +100,21 @@ nr_def simple_lambda<>(x : Field) -> Field {
 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
-  . apply STHoare.var_intro
-  . sorry -- unsolvable
+  steps
+  rotate_left 2
+  exact (fun v => v = x)
+  rotate_left 1
+  . steps
+    intros
+    subst_vars
+    rfl
+  . apply STHoare.ramified_frame_top
+    apply STHoare.callLambda_intro
+    rotate_left 2
+    exact ⟦⟧
+    exact (fun v => v = x)
+    rotate_left 2
+    exact (fun h![a] => (Expr.var a))
+    rotate_left 1
+    apply STHoare.var_intro
+    sorry
diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
@@ -29,8 +29,8 @@ lemma pureBuiltin_intro_consequence
     {A : Type} {a : A} {sgn desc args} {Q : Tp.denote p outTp → Prop}
     (h1 : argTps = (sgn a).fst)
     (h2 : outTp = (sgn a).snd)
-    (hp : (h: (desc a (h1 ▸ args)).fst) → Q (h2 ▸ (desc a (h1 ▸ args)).snd h))
-    : STHoare p Γ ⟦⟧
+    (hp : (h: (desc a (h1 ▸ args)).fst) → Q (h2 ▸ (desc a (h1 ▸ args)).snd h)) :
+    STHoare p Γ ⟦⟧
       (.call h![] argTps outTp (.builtin (Builtin.newGenericPureBuiltin sgn desc)) args)
       fun v => Q v := by
   subst_vars

diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean
@@ -306,11 +306,11 @@ theorem skip_intro :
   . apply SLP.ent_star_top
     tauto
 
-theorem callLambda_intro {lambdaBody} :
-  @STHoare outTp p Γ ⟦⟧ (lambdaBody args) (fun v => v = v') →
-  STHoare p Γ [ref ↣ ⟨_, argTps, outTp, lambdaBody⟩]
+theorem callLambda_intro {lambdaBody} {P : SLP (State p)} {Q : Tp.denote p outTp → SLP (State p)}:
+  @STHoare outTp p Γ P (lambdaBody args) Q →
+  STHoare p Γ (P ⋆ [ref ↣ ⟨_, argTps, outTp, lambdaBody⟩])
     (Expr.call h![] argTps outTp (.lambda ref) args)
-    (fun v => ⟦v = v'⟧ ⋆ [ref ↣ ⟨_, argTps, outTp, lambdaBody⟩]) := by
+    (fun v => (Q v) ⋆ [ref ↣ ⟨_, argTps, outTp, lambdaBody⟩]) := by
   intros
   rename_i h
   unfold STHoare THoare
@@ -319,14 +319,24 @@ theorem callLambda_intro {lambdaBody} :
   unfold SLP.star at *
   . rename_i st h
     obtain ⟨st₁, ⟨st₂, ⟨_, h₂, h₃, _⟩⟩⟩ := h
-    simp only [State.union_parts, h₃] at h₂
-    simp only [h₂]
-    simp_all
+    obtain ⟨st₁', ⟨st₂', _⟩⟩ := h₃
+    simp_all only [State.union_parts, Finmap.mem_union, Finmap.mem_singleton, or_true,
+      Finmap.lookup_union_left]
+    generalize hL : (⟨_, _, _, _⟩ : Lambda) = lmb at *
+    have _ : ref ∉ st₁'.lambdas := by
+      rename_i h₃
+      obtain ⟨hi₁, _, _, hi₂⟩ := h₃
+      simp only [State.lmbSingleton] at hi₂
+      simp only [LawfulHeap.disjoint] at hi₁
+      obtain ⟨_, hj₁⟩ := hi₁
+      rw [hi₂] at hj₁
+      tauto
+    simp [Finmap.lookup_union_right (by tauto)]
   . apply consequence
     <;> tauto
     apply consequence_frame_left
     rotate_left 2
-    exact ⟦⟧
+    exact P
     exact h
     simp only [SLP.true_star, SLP.entails_self]