Yref

Lgtm/Experiments/Dummy.lean

@@ -16,13 +16,13 @@ lang_def Lang.get :=
 lang_def Lang.nonempty :=
   fun xind xval =>
     let N := len xind in
-    let ans := ref false in
+    ref ans := false in
     for i in [0:N] {
       let v := xval[i] in
       ans ||= v
     }
     let a := !ans in
-    free ans; a
+    a
 
 variable (xind xval : loc) (N : ℕ)
 variable (x_ind : ℤ -> ℝ) (x_val : ℤ -> Bool)
@@ -57,7 +57,7 @@ instance : Coe val Prop := ⟨toProp⟩
   | `($_ $v) => `($v)
   | _ => throw ( )
 
-attribute [-simp] fun_insert
+attribute [-simp] fun_insert hhwandE
 
 
 lemma nonempty_spec (r : ℝ)  :
@@ -67,7 +67,12 @@ lemma nonempty_spec (r : ℝ)  :
   [2| i in · => Lang.get xind xval ⟪i.val⟫]
   {v,
     ⌜ v ⟨1,r⟩ = ∃ i : ℝ, v ⟨2,i⟩ ⌝ ∗ (⊤ : hhProp (Labeled ℝ)) } := by
-  -- srw LGTM.triple
+  srw LGTM.triple
+  yfocus 1
+  ywp ; yapp
+  ywp; yref p
+
+
   -- yfocus 2, (x_ind '' ⟦0, (N : ℤ)⟧)
   -- yapp get_spec_out
   -- ysimp_start

Lgtm/Experiments/UnaryCommon.lean

@@ -71,7 +71,7 @@ lemma incr_spec (p : loc) (n : Int) :
 lang_def findIdx :=
   fun arr target  =>
     let N := len arr in
-    let ind := ref 0 in
+    ref ind := 0 in
     while (
       let ind    := !ind in
       let indLN  := ind < N in
@@ -82,7 +82,7 @@ lang_def findIdx :=
         incr ind
     };
     let res := !ind in
-    free ind ; res
+    res
 
 abbrev to_real (v : val) : ℝ :=
   match v with
@@ -99,11 +99,11 @@ instance : Coe val ℝ := ⟨to_real⟩
 instance : Coe val ℤ := ⟨to_int⟩
 
 -- #hint_xapp triple_arrayFun_length ????
-#hint_xapp triple_ref
+-- #hint_xapp triple_ref
 #hint_xapp triple_get
 #hint_xapp triple_lt
 #hint_xapp triple_neq
-#hint_xapp triple_free
+-- #hint_xapp triple_free
 #hint_xapp incr_spec
 #hint_xapp triple_arrayFun_length
 #hint_xapp triple_harrayFun_get
@@ -126,7 +126,7 @@ lemma findIdx_spec (arr : loc) (f : Int -> ℝ) (target : ℝ) (N : ℕ) :
   { v, ⌜ v = f.invFunOn ⟦0, (N : ℤ)⟧ target ⌝ ∗ arr(arr, x in N => f x) } := by
   move=> inj fin
   xwp; xapp triple_arrayFun_length
-  xwp; xapp=> p
+  xwp; xref
   let cond (i : ℤ) := (i < N ∧ f.invFunOn ⟦0, (N : ℤ)⟧ target != i)
   xwhile_up (fun b i =>
     ⌜0 <= i ∧ i <= N ∧ target ∉ f '' ⟦0, i⟧⌝ ∗
@@ -156,7 +156,15 @@ lemma findIdx_spec (arr : loc) (f : Int -> ℝ) (target : ℝ) (N : ℕ) :
     srw cond /== }
   move=> hv /=; xsimp=> i ?; srw cond=> /== fE
   sdo 2 (xwp; xapp)
-  xwp; xval; xsimp
+  xwp; xval
+  -- xsimp --(buggy)
+  xsimp_start
+  xsimp_step
+  xsimp_step
+  xsimp_step
+  xsimp_step
+  apply (xsimp_r_hexists)
+  xsimp_step
   srw fE; scase: [i = N]=> [|?] //; omega
 
 lemma findIdx_spec_out (arr : loc) (f : Int -> ℝ) (target : ℝ) (N : ℕ) :
@@ -167,7 +175,7 @@ lemma findIdx_spec_out (arr : loc) (f : Int -> ℝ) (target : ℝ) (N : ℕ) :
   { v, ⌜ v = val_int N ⌝ ∗ arr(arr, x in N => f x) } := by
   move=> ? img
   xwp; xapp
-  xwp; xapp=> p
+  xwp; xref
   let cond (i : ℤ) := (i < N ∧ target != f i)
   xwhile_up (fun b i =>
     ⌜0 <= i ∧ i <= N ∧ target ∉ f '' ⟦0, i⟧⌝ ∗
@@ -196,7 +204,15 @@ lemma findIdx_spec_out (arr : loc) (f : Int -> ℝ) (target : ℝ) (N : ℕ) :
     srw cond /== }
   move=> hv /=; xsimp=> i ?; srw cond=> /== fE
   sdo 2 (xwp; xapp)
-  xwp; xval; xsimp
+  xwp; xval
+  --xsimp --buggy
+  xsimp_start
+  xsimp_step
+  xsimp_step
+  xsimp_step
+  xsimp_step
+  apply (xsimp_r_hexists)
+  xsimp_step
   scase: [i = N]=> [?|?] //;
   move: img; srw fE //== <;> try omega
   move=> /(_ i)=> // H

Lgtm/Hyper/HProp.lean

@@ -19,7 +19,9 @@ def hhProp (α : Type) := @hheap α -> Prop
 
 @[ext]
 lemma hhProp_ext (h₁ h₂ : hhProp α) :
-  (∀ a, h₁ a = h₂ a) -> (h₁ = h₂)  := by sorry
+  (∀ a, h₁ a = h₂ a) -> (h₁ = h₂)  := by
+  move=> ?
+  sby funext
 
 def hunion (h₁ h₂ : @hheap α) : @hheap α :=
   λ a => h₁ a ∪ h₂ a

Lgtm/Hyper/ProofMode.lean

@@ -399,6 +399,25 @@ by
   ysimp
   apply htriple_ramified_frame=> //
 
+lemma yref_lemma_aux s (x : α → var) (v : α → val) (t : α → trm) H Q :
+  (∀ p : α → loc, H ==> ((p i ~⟨i in s⟩~> v i) -∗
+    protect (hwp s (fun i ↦ subst (x i) (p i) (t i))
+    (Q ∗ ∃ʰ (u : α → val), p i ~⟨i in s⟩~> u i)))) →
+  H ==> hwpgen_ref s x (fun i ↦ trm_val (v i)) t Q :=
+by
+  move=> M h /M
+  unfold hwpgen_ref=> /hhforall_inv {}M
+  exists v=> /==
+  sby srw hhstar_hhpure_l
+
+lemma yref_lemma (x : α → var) (v : α → val) (t : α → trm) H Q :
+  (∀ p : α → loc, H ∗ (p i ~⟨i in s⟩~> v i) ==>
+    (hwp s (fun i ↦ subst (x i) (p i) (t i))
+    (Q ∗ ∃ʰ (u : α → val), p i ~⟨i in s⟩~> u i))) →
+  H ==> hwpgen_ref s x (fun i ↦ trm_val (v i)) t Q :=
+by
+  move=> himp; apply yref_lemma_aux=> p
+  ysimp; ychange himp
 
 lemma ywp_lemma_fun (v1 v2 : hval α) (x : α -> var) (t : htrm α) H Q :
   (∀ i, v1 i = val_fun (x i) (t i)) →
@@ -466,6 +485,12 @@ macro "yif" : tactic => do
   `(tactic|
   (yseq_xlet_if_needed; ystruct_if_needed; apply yif_lemma))
 
+
+macro "yref" p:term : tactic => do
+  `(tactic|
+  (yseq_xlet_if_needed; ystruct_if_needed; apply yref_lemma; intro $p:term;
+    try simp [$(mkIdent `subst):ident]))
+
 set_option linter.unreachableTactic false in
 set_option linter.unusedTactic false in
 elab "yapp_try_clear_unit_result" : tactic => do

Lgtm/Hyper/SepLog.lean

@@ -10,6 +10,7 @@ import Lgtm.Hyper.HProp
 import Lgtm.Hyper.YSimp
 import Lgtm.Hyper.YChange
 
+import Lgtm.Common.State
 
 section HSepLog
 
@@ -520,6 +521,107 @@ lemma heval_fix (s : Set α) (x f : α -> var) (ht₁ : α -> trm) :
   move=> hv' /= ? /= H ⟨|⟨|⟩⟩/=; exact (fun a => val_fix (f a) (x a) (ht₁ a))
   all_goals sby funext a; move: (H a); scase_if
 
+/- def heval (s : Set α) (hh : hheap) (ht : htrm) (hQ : hval -> hhProp) : Prop :=
+   ∃ (hQ' : α -> val -> hProp),
+    heval_nonrel s hh ht hQ' ∧
+    ∀ hv, bighstarDef s (fun a => hQ' a (hv a)) hh ==> ∃ʰ hv', hQ (hv ∪_s hv') -/
+
+def fresh_ptr (s : state) : loc :=
+  match s.keys.max with
+  | ⊥      => 1
+  | some n => n + 1
+
+theorem fresh_ptr_sound (s : state) :
+  fresh_ptr s ∉ s :=
+by
+  unfold fresh_ptr
+  cases eqn:(s.keys.max)=> /=
+  { move: eqn=> /Finset.max_eq_bot
+    sby srw Not -Finmap.mem_keys }
+  move: eqn=> /Finset.not_mem_of_max_lt
+  sby srw -Finmap.mem_keys
+
+lemma mem_exists_union (p : loc) (h : state) :
+  p ∈ h →
+  ∃ v, h = Finmap.singleton p v ∪ (h.erase p) := by
+  move=> /Finmap.mem_iff [v] ?
+  exists  v=> /==
+  apply Finmap.ext_lookup=> >
+  scase: [x = p]
+  { move=> ?
+    sby srw Finmap.lookup_union_right }
+  move=> ->
+  sby srw Finmap.lookup_union_left
+
+lemma hwand_pointer_erase :
+  p ∈ h →
+  H h →
+  (hexists fun u ↦ p ~~> u -∗ H) (h.erase p) := by
+  move=> /mem_exists_union [v] heq ?
+  srw hwandE
+  exists v=> /=
+  exists (fun h' ↦ Finmap.singleton p v ∪ h' = h)=> /=
+  srw hstar_hpure_r=> ⟨//|⟩
+  sby move=> s ![>] /hsingl_inv -> /= -> ? ->
+
+/- def heval_nonrel (s : Set α) (hh : hheap) (ht : htrm) (hQ : α -> val -> hProp) : Prop :=
+  ∀ a ∈ s, eval (hh a) (ht a) (hQ a) -/
+lemma heval_ref (x : α → var) (hh : α → heap) (hv : α → val) (ht : α → trm) :
+  (∀ (hp : α → loc), (∀ i ∈ s, hp i ∉ hh i) →
+    heval s (fun i ↦ if i ∈ s then (hh i).insert (hp i) (hv i) else hh i) -- ∪_s
+      (fun d ↦ subst (x d) (hp d) (ht d)) (Q ∗ ∃ʰ (hu : α → val), hp i ~⟨i in s⟩~> hu i )) →
+  heval s hh (fun d ↦ trm_ref (x d) (hv d) (ht d)) Q :=
+by
+  move=> h
+  exists (fun a v ↦ hexists fun p ↦ hpure (p ∉ hh a) ∗
+    (hexists fun u ↦ p ~~> u -∗ sP' (if a ∈ s then (hh a).insert p (hv a) else hh a) (subst (x a) p (ht a)) v))
+  /- maybe should be something like:
+     fun a v ↦ ∃ʰ p, ⌜p ∉ hh a⌝ ∗
+      fun h ↦ ⌜p ∉ h⌝ ∗ ∃ʰ u, (sP ...) v (h.insert p u)
+    obviously not correct notation but something similar might work.
+   -/
+  -- exists fun a v ↦ hexists fun p ↦ (hpure (p ∉ hh a)) ∗ fun (h : heap) ↦ p ∉ h ∧
+  --   ∃ u, (sP ((hh a).insert p (hv a)) (subst (x a) p (ht a))) v (h.insert p u)
+  constructor=> /==
+  { move=> /== > /[dup] ain ?
+    apply (eval.eval_ref _ _ _ _ _ (fun v s ↦ v = hv a ∧ s = hh a ))=> //
+    move=> > [-> ->] > ?
+    let hp (d : α) := if d = a then p else fresh_ptr (hh d)
+    have hin:(∀ i ∈ s, hp i ∉ hh i) := by
+      { move=> > _ ; srw hp
+        scase_if=> // _ ; apply fresh_ptr_sound }
+    apply h in hin=> {h} ![hQ' hev himp]
+    move: (heval_nonrel_sat' hev)=> ![hh₂' hv₂' hQH₁ hheq]
+    have hheq':(∀ a ∉ s, hh₂' a = hh a) := by
+      { move=> > /[dup] ? /hheq ; sby scase_if }
+    move=> {hheq}
+    specialize hev a ; apply hev in ain=> /== ; scase_if=> // _
+    srw hp=> /= {}hev
+    apply (eval_conseq (Q1 := sP' (Finmap.insert p (hv a) (hh a)) (subst (x a) p (ht a))))
+    { sby apply sP'_post }
+    move=> v h /= hsP
+    exists p=> /==
+    srw hstar_hpure_l=> ⟨//|⟩
+    apply hwand_pointer_erase=> //
+    move: hev hsP=> /sP'_post_exact /evalExact_WellAlloc /[apply]
+    srw -Finmap.mem_keys=> -> ; sby srw Finmap.mem_keys }
+  move=> hv' ; srw ?bighstarDef_hexists
+  apply hhimpl_hhexists_l=> hp
+  srw -(empty_hunion hh) -bighstarDef_hhstar; rotate_left
+  { move=> ?; apply Finmap.disjoint_empty }
+  erw [bighstarDef_hpure] ; srw empty_hunion
+  apply hhimpl_hstar_hhpure_l=> /h {h} ![hQ' /hstrongest_postP sPimp /= himp]
+  -- apply hhimpl_trans_r
+  -- { apply hhimpl_trans_r ; rotate_left ; apply himp hv'
+  --   move=> hh' ![hv₂ hh₂ hh₃] ? [hv₃] /=
+  --   sorry  }
+  let hh' := fun i ↦ (hh i).insert (hp i) (hv i)
+  specialize himp hv' (hh' ∪_s hh) ?_
+  { move=> > ; scase_if=> //== /[dup] ? /sPimp {}sPimp
+    specialize sPimp (hv' a) ((hh' ∪_s hh) a) ; apply sPimp=> /=
+    unfold hsP=> /== ; srw hh' ; scase_if=> // _
+    sorry }
+  sorry
 
 end HEvalTrm
 
@@ -701,12 +803,12 @@ notation (priority := high) "funloc" p "=>" H => fun hv => ∃ʰ p, ⌜ hv = val
 
 open Classical
 
-lemma htriple_ref' (v : α -> val) :
-  htriple s (fun a => trm_app val_ref (v a))
-    emp
-    (fun hv => [∗ i in s| hexists fun p => hpure (hv i = val_loc p) ∗ p ~~> v i]) := by
-    srw -(bighstar_hhempty (s := s)); apply htriple_prod (Q := fun a v' => hexists fun p => hpure (v' = val_loc p) ∗ p ~~> v a)
-    move=> ??; apply triple_ref
+-- lemma htriple_ref' (v : α -> val) :
+--   htriple s (fun a => trm_app val_ref (v a))
+--     emp
+--     (fun hv => [∗ i in s| hexists fun p => hpure (hv i = val_loc p) ∗ p ~~> v i]) := by
+--     srw -(bighstar_hhempty (s := s)); apply htriple_prod (Q := fun a v' => hexists fun p => hpure (v' = val_loc p) ∗ p ~~> v a)
+--     move=> ??; apply triple_ref
 
 lemma htriple_hv_ext :
   htriple s ht H (fun hv => ∃ʰ hv', Q (hv ∪_s hv')) ->
@@ -717,18 +819,18 @@ lemma htriple_hv_ext :
   sby srw fun_insert_ss
 
 
-lemma htriple_ref (v : α -> val) :
-  htriple s (fun a => trm_app val_ref (v a))
-    emp
-    (funloc p =>  p i ~⟨i in s⟩~> v i) := by
-    apply htriple_hv_ext
-    apply htriple_conseq; apply htriple_ref'; apply hhimpl_refl
-    move=> hv /=; srw bighstar_hexists
-    ypull=> p;
-    srw -bighstar_hhstar bighstar
-    erw [(bighstarDef_hpure (P := fun i => hv i = val_loc (p i)))]
-    ysimp[val_loc ∘ p, p]=> //
-    sby funext x
+-- lemma htriple_ref (v : α -> val) :
+--   htriple s (fun a => trm_app val_ref (v a))
+--     emp
+--     (funloc p =>  p i ~⟨i in s⟩~> v i) := by
+--     apply htriple_hv_ext
+--     apply htriple_conseq; apply htriple_ref'; apply hhimpl_refl
+--     move=> hv /=; srw bighstar_hexists
+--     ypull=> p;
+--     srw -bighstar_hhstar bighstar
+--     erw [(bighstarDef_hpure (P := fun i => hv i = val_loc (p i)))]
+--     ysimp[val_loc ∘ p, p]=> //
+--     sby funext x
 
 lemma htriple_prod_val_eq (ht : htrm) (H : α -> _) (Q : α -> _) (fv : hval) :
   (∀ a ∈ s, triple (ht a) (H a) (fun v => hpure (v = fv a) ∗ Q a)) ->
@@ -769,13 +871,13 @@ lemma htriple_set (hv hu : hval) (p : α -> loc) :
     apply htriple_prod_val_eq
     move=> ??; apply triple_set
 
-lemma htriple_free (hv : hval) (p : α -> loc) :
-  htriple s (fun a => trm_app val_free (val_loc (p a)))
-    [∗ i in s| p i ~~> hv i]
-    (fun _ => emp) := by
-    srw -(bighstar_hhempty (s := s))
-    apply htriple_prod (Q := fun _ _ => hempty)
-    move=> ??; apply triple_free
+-- lemma htriple_free (hv : hval) (p : α -> loc) :
+--   htriple s (fun a => trm_app val_free (val_loc (p a)))
+--     [∗ i in s| p i ~~> hv i]
+--     (fun _ => emp) := by
+--     srw -(bighstar_hhempty (s := s))
+--     apply htriple_prod (Q := fun _ _ => hempty)
+--     move=> ??; apply triple_free
 
 lemma htriple_unop (op : α -> prim) (v₁ v : hval) :
   (∀ a ∈ s, evalunop (op a) (v₁ a) (· = v a)) ->