diff --git a/Lgtm/Common/State.lean b/Lgtm/Common/State.lean new file mode 100644 index 0000000..234687d --- /dev/null +++ b/Lgtm/Common/State.lean @@ -0,0 +1,643 @@ +import Mathlib.Data.Finmap +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Multiset.Nodup + +import Lgtm.Unary.Util +import Lgtm.Unary.Lang + + +/- ========= Useful Lemmas about disjointness and state operations ========= -/ + +lemma disjoint_update_not_r (h1 h2 : state) (x : loc) (v: val) : + Finmap.Disjoint h1 h2 → + x ∉ h2 → + Finmap.Disjoint (Finmap.insert x v h1) h2 := +by + srw Finmap.Disjoint => ?? + srw Finmap.Disjoint Finmap.mem_insert => ? + sby scase + +lemma in_read_union_l (h1 h2 : state) (x : loc) : + x ∈ h1 → read_state x (h1 ∪ h2) = read_state x h1 := +by + move=> ? + srw []read_state + sby srw (Finmap.lookup_union_left) + +lemma disjoint_insert_l (h1 h2 : state) (x : loc) (v : val) : + Finmap.Disjoint h1 h2 → + x ∈ h1 → + Finmap.Disjoint (Finmap.insert x v h1) h2 := +by + srw Finmap.Disjoint => * + srw Finmap.Disjoint Finmap.mem_insert => ? + sby scase + +lemma insert_disjoint_l (h1 h2 : state) (x : loc) (v : val) : + h2.Disjoint (h1.insert x v) → + x ∉ h2 ∧ h2.Disjoint h1 := by + unfold Finmap.Disjoint=> hdis ⟨|⟩ + { sby unfold Not=> /hdis } + sby move=> > + +lemma remove_disjoint_union_l (h1 h2 : state) (x : loc) : + x ∈ h1 → Finmap.Disjoint h1 h2 → + Finmap.erase x (h1 ∪ h2) = Finmap.erase x h1 ∪ h2 := +by + srw Finmap.Disjoint => * ; apply Finmap.ext_lookup => y + scase: [x = y]=> hEq + { scase: [y ∈ Finmap.erase x h1]=> hErase + { srw Finmap.lookup_union_right + rw [Finmap.lookup_erase_ne] + apply Finmap.lookup_union_right + srw Finmap.mem_erase at hErase=>// + srw Not at * => * // + sby srw Not } + srw Finmap.lookup_union_left + sby sdo 2 rw [Finmap.lookup_erase_ne] } + srw -hEq + srw Finmap.lookup_union_right=>// + srw Finmap.lookup_erase + apply Eq.symm + sby srw Finmap.lookup_eq_none + +lemma remove_not_in_l (h1 h2 : state) (p : loc) : + p ∉ h1 → + (h1 ∪ h2).erase p = h1 ∪ h2.erase p := by + move=> ? + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> ? + srw Finmap.lookup_erase_ne=> // + scase: [x ∈ h1] + { move=> ? ; sby srw ?Finmap.lookup_union_right } + move=> ? ; sby srw ?Finmap.lookup_union_left } + move=> -> + sby srw Finmap.lookup_union_right + +lemma remove_not_in_r (h1 h2 : state) (p : loc) : + p ∉ h2 → + (h1 ∪ h2).erase p = h1.erase p ∪ h2 := by + move=> ? + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> ? + srw Finmap.lookup_erase_ne=> // + scase: [x ∈ h1] + { move=> ? ; sby srw ?Finmap.lookup_union_right } + move=> ? ; sby srw ?Finmap.lookup_union_left } + move=> -> + sby srw Finmap.lookup_union_left_of_not_in + +lemma disjoint_remove_l (h1 h2 : state) (x : loc) : + Finmap.Disjoint h1 h2 → + Finmap.Disjoint (Finmap.erase x h1) h2 := +by + srw Finmap.Disjoint=> ?? + sby srw Finmap.mem_erase + +lemma erase_disjoint (h1 h2 : state) (p : loc) : + h1.Disjoint h2 → + (h1.erase p).Disjoint h2 := by + sby unfold Finmap.Disjoint=> ?? > /Finmap.mem_erase + +lemma disjoint_single (h : state) : + p ∉ h → + h.Disjoint (Finmap.singleton p v) := by + move=> ? + unfold Finmap.Disjoint=> > ? + sby scase: [x = p] + +lemma insert_union (h1 h2 : state) (p : loc) (v : val) : + p ∉ h1 ∪ h2 → + (h1 ∪ h2).insert p v = (h1.insert p v) ∪ h2 := by + move=> ? + apply Finmap.ext_lookup=> > + scase: [x = p]=> ? + { srw Finmap.lookup_insert_of_ne=> // + scase: [x ∈ h1]=> ? + { sby srw ?Finmap.lookup_union_right } + sby srw ?Finmap.lookup_union_left } + sby subst x + +lemma insert_mem_keys (s : state) : + p ∈ s → + (s.insert p v).keys = s.keys := by + move=> ? + apply Finset.ext=> > + sby srw ?Finmap.mem_keys + +lemma non_mem_union (h1 h2 : state) : + a ∉ h1 ∪ h2 ↔ a ∉ h1 ∧ a ∉ h2 := by sdone + +lemma insert_delete_id (h : state) (p : loc) : + p ∉ h → + h = (h.insert p v).erase p := by + move=> hin + apply Finmap.ext_lookup=> > + scase: [x = p]=> ? + { sby srw Finmap.lookup_erase_ne } + subst x + move: hin=> /Finmap.lookup_eq_none ? + sby srw Finmap.lookup_erase + +lemma insert_same (h1 h2 : state) : + p ∉ h1 → p ∉ h2 → + (h1.insert p v).keys = (h2.insert p v').keys → + h1.keys = h2.keys := by + move=> ?? /Finset.ext_iff + srw Finmap.mem_keys Finmap.mem_insert=> hin + apply Finset.ext=> > ; srw ?Finmap.mem_keys + scase: [a = p]=> ? + { apply Iff.intro + sdo 2 (sby move=> /(Or.intro_right (a = p)) /hin []) } + sby subst a + +lemma insert_same_eq (h1 h2 : state) : + p ∉ h1 → p ∉ h2 → + h1.insert p v = h2.insert p v → + h1 = h2 := by + move=> /Finmap.lookup_eq_none ? /Finmap.lookup_eq_none ? * + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> /Finmap.lookup_insert_of_ne hlook + sby srw -(hlook _ v h1) -(hlook _ v h2) } + sby move=> [] + +lemma union_same_keys (h₁ h₂ h₃ : state) : + h₁.Disjoint h₃ → h₂.Disjoint h₃ → + (h₁ ∪ h₃).keys = (h₂ ∪ h₃).keys → + h₁.keys = h₂.keys := by + unfold Finmap.Disjoint + move=> ?? /Finset.ext_iff + srw Finmap.mem_keys Finmap.mem_union=> hin + apply Finset.ext=> > ; srw ?Finmap.mem_keys + apply Iff.intro + sdo 2 (sby move=> /[dup] ? /(Or.intro_left (a ∈ h₃)) /hin []) + +lemma insert_eq_union_single (h : state) : + p ∉ h → + h.insert p v = h ∪ (Finmap.singleton p v) := by + move=> ? + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> ? + srw Finmap.lookup_insert_of_ne=> // + sby srw Finmap.lookup_union_left_of_not_in } + sby move=> [] + +lemma keys_eq_not_mem_r (h1 h2 : state) : + h1.keys = h2.keys → + p ∉ h2 → + p ∉ h1 := by + move=> /Finset.ext_iff + sby srw Finmap.mem_keys + +lemma keys_eq_not_mem_l (h1 h2 : state) : + h1.keys = h2.keys → + p ∉ h1 → + p ∉ h2 := by + move=> /Finset.ext_iff + sby srw Finmap.mem_keys + +lemma keys_eq_mem_r (h1 h2 : state) : + h1.keys = h2.keys → + p ∈ h2 → + p ∈ h1 := by + move=> /Finset.ext_iff + sby srw Finmap.mem_keys + +lemma state_eq_not_mem (p : loc) (h1 h2 : state) : + h1 = h2 → + p ∉ h1 → + p ∉ h2 := by sdone + +lemma erase_of_non_mem (h : state) : + p ∉ h → + h.erase p = h := by + move=> /Finmap.lookup_eq_none ? + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> /Finmap.lookup_erase_ne Hlook + srw Hlook } + move=> [] + sby srw Finmap.lookup_erase + +lemma insert_neq_of_non_mem (h : state) : + x ∉ h → + x ≠ p → + x ∉ h.insert p v := by + move=> * ; unfold Not + sby move=> /Finmap.mem_insert + +lemma reinsert_erase_union (h1 h2 h3 : state) : + h3.lookup p = some v → + p ∉ h2 → + h3.erase p = h1 ∪ h2 → + h3 = (h1.insert p v) ∪ h2 := by + move=> ?? heq + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> /[dup] /Finmap.lookup_erase_ne hlook + srw -hlook {hlook} heq + scase: [x ∈ h1] + { sby move=> * ; srw ?Finmap.lookup_union_right } + move=> * ; sby srw ?Finmap.lookup_union_left } + move=> [] + sby srw Finmap.lookup_union_left + +lemma union_singleton_eq_erase (h h' : state) : + h.Disjoint (Finmap.singleton p v) → + h' = h ∪ Finmap.singleton p v → + h = h'.erase p := by + move=> hdisj [] + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> ? + srw Finmap.lookup_erase_ne=> // + sby srw Finmap.lookup_union_left_of_not_in } + move=> [] + srw Finmap.lookup_erase + srw Finmap.lookup_eq_none + sby move: hdisj ; unfold Finmap.Disjoint Not=> /[apply] + +lemma union_singleton_eq_insert (h : state) : + Finmap.singleton p v ∪ h = h.insert p v := by + apply Finmap.ext_lookup=> > + sby scase: [x = p] + +lemma disjoint_keys (h₁ h₂ : state) : + h₁.Disjoint h₂ → + Disjoint h₁.keys h₂.keys := by + unfold Finmap.Disjoint + srw -Finmap.mem_keys Finset.disjoint_iff_ne + move=> hFmap > /hFmap ? > hb + sby srw Not + +lemma non_mem_diff_helper1 (h₁ : state) (l : @AList loc fun _ ↦ val) : + a ∉ l → + p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) (Finmap.erase a h₁) l.entries → + p ≠ a := by + elim: l h₁=> // + move=> > ? ih > /== ?? + srw Finmap.erase_erase + srw List.kerase_of_not_mem_keys=> // ? + sby apply ih + +lemma non_mem_diff_helper2 (h₁ : state) (l : @AList loc fun _ ↦ val) : + p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) (Finmap.erase a h₁) l.entries → + p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) h₁ l.entries := by + elim: l h₁=> // + move=> > ? ih > + srw AList.insert_entries List.foldl_cons=> /= + srw List.kerase_of_not_mem_keys=> // ? + apply ih + sby srw Finmap.erase_erase + +theorem mem_diff_r (h₁ h₂ : state) : + p ∈ h₁ \ h₂ → p ∉ h₂ := by + refine Finmap.induction_on h₂ ? + move=> > + unfold Finmap.instSDiff Finmap.sdiff Finmap.foldl=> /== + elim: a + { sdone } + move=> > ih1 ih2 + srw AList.insert_entries List.foldl_cons=> /= + srw List.kerase_of_not_mem_keys=> //== ? ⟨|⟩ + { sby apply non_mem_diff_helper1 } + apply ih2 + sby apply non_mem_diff_helper2 + +lemma mem_erase_right (s : state) : + p ∈ s.erase x → p ∈ s := by + sby move=> /Finmap.mem_erase + +lemma list_foldl_erase_mem (h₁ : state) (l : @AList loc fun _ ↦ val) : + p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) h₁ l.entries → p ∈ h₁ := by + elim: l h₁=> // + move=> > ? ih /= + srw List.kerase_of_not_mem_keys=> // > /ih + sby srw Finmap.mem_erase + +lemma mem_diff_helper (h₁ : state) (l : @AList loc fun _ ↦ val) : + a ∉ l → + (p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) h₁ l.entries → p ∈ h₁) → + p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) (Finmap.erase a h₁) l.entries → + p ∈ h₁ := by + elim: l h₁=> > + { sdone } + move=> ? ih > /== ? + srw List.kerase_of_not_mem_keys=> // + srw Finmap.erase_erase=> ??? + apply (@mem_erase_right p a_1 h₁) + sby apply ih=> // /list_foldl_erase_mem + +theorem mem_diff_l (h₁ h₂ : state) : + p ∈ h₁ \ h₂ → p ∈ h₁ := by + refine Finmap.induction_on h₂ ? _ + move=> > + unfold Finmap.instSDiff Finmap.sdiff Finmap.foldl=> /= + elim: a=> > // + move=> ? ih + srw AList.insert_entries List.foldl_cons=> /= + srw List.kerase_of_not_mem_keys=> // + sby apply mem_diff_helper + +lemma mem_diff_rev_helper (h₁ : state) (l : @AList loc fun _ ↦ val) : + a ∉ l → + (p ∈ h₁ ∧ p ∉ l.toFinmap → p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) h₁ l.entries) → + p ∈ h₁ ∧ p ∉ (AList.insert a b l).toFinmap → + p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) (Finmap.erase a h₁) l.entries := by + elim: l h₁=> > + { move=> ? /== _ ? + unfold Not=> hsing ⟨| // ⟩ + move=> [] + apply hsing + sby srw AList.mem_keys AList.keys_singleton } + move=> ? ih > ? /= + srw List.kerase_of_not_mem_keys=> // ? + srw Finmap.erase_erase=> ? + sby apply ih + +theorem mem_diff_rev (h₁ h₂ : state) : + p ∈ h₁ ∧ p ∉ h₂ → p ∈ h₁ \ h₂ := by + refine Finmap.induction_on h₂ ? _ + move=> > + unfold Finmap.instSDiff Finmap.sdiff Finmap.foldl=> /= + elim: a=> > // + move=> ? ih /= + srw List.kerase_of_not_mem_keys=> // ? + sby apply mem_diff_rev_helper + +/- Main theorem about set difference for Finmaps -/ +@[simp] +theorem mem_diff_iff (h₁ h₂ : state) : + p ∈ h₁ \ h₂ ↔ p ∈ h₁ ∧ p ∉ h₂ := by + apply Iff.intro + { sby move=> /[dup] /mem_diff_l ? /mem_diff_r } + apply mem_diff_rev + +theorem diff_non_mem (h₁ h₂ : state) : + p ∈ h₂ → p ∉ h₁ \ h₂ := by sdone + +lemma union_difference_id (h₁ h₂ : state) : + h₁.Disjoint h₂ → + (h₁ ∪ h₂) \ h₂ = h₁ := by + refine Finmap.induction_on h₂ ? _ + move=> > + unfold Finmap.instSDiff Finmap.sdiff Finmap.foldl=> /= + elim: a=> > //== ? + srw List.kerase_of_not_mem_keys=> // ih + srw -Finmap.insert_toFinmap=> /insert_disjoint_l ? + srw remove_not_in_l=> // + sby srw -insert_delete_id + +lemma diff_disjoint (h₁ h₂ : state) : + h₂.Disjoint (h₁ \ h₂) := by sdone + +lemma disjoint_disjoint_diff (h₁ h₂ h₃ : state) : + h₁.Disjoint h₂ → + (h₁ \ h₃).Disjoint h₂ := by + sby unfold Finmap.Disjoint + +lemma lookup_diff (h₁ h₂ : state) : + p ∉ h₂ → + (h₁ \ h₂).lookup p = h₁.lookup p := by + refine Finmap.induction_on h₂ ? _ + move=> > + unfold Finmap.instSDiff Finmap.sdiff Finmap.foldl=> /== + elim: a h₁=> > // + move=> ? ih > /= + sby srw List.kerase_of_not_mem_keys + +lemma lookup_diff_none (h₁ h₂ : state) : + p ∈ h₂ → + (h₁ \ h₂).lookup p = none := by + sby move=> /(diff_non_mem h₁) /Finmap.lookup_eq_none + +lemma union_diff_disjoint_r (h₁ h₂ h₃ : state) : + h₂.Disjoint h₃ → + (h₁ ∪ h₂) \ h₃ = (h₁ \ h₃) ∪ h₂ := by + unfold Finmap.Disjoint=> hdis + apply Finmap.ext_lookup=> > + scase: [x ∈ h₃] + { move=> ? + scase: [x ∈ h₁] + { move=> ? ; sby srw lookup_diff } + move=> ? ; srw Finmap.lookup_union_left=> // + sby srw ?lookup_diff } + move=> ? + scase: [x ∈ h₂] + { move=> ? ; srw Finmap.lookup_union_left_of_not_in=> // + sby srw ?lookup_diff_none } + sby move=> /hdis + + lemma diff_disjoint_eq (s₁ s₂ s₃ : state) : + s₁.Disjoint s₂ → + s₂.keys = s₃.keys → + (s₁ ∪ s₂) \ s₃ = s₁ := by + srw Finmap.Disjoint.symm_iff Finmap.Disjoint=> hdis + srw Finset.ext_iff Finmap.mem_keys=> hsub + apply Finmap.ext_lookup=> > + scase: [x ∈ s₃] + { move=> /[dup] ? /lookup_diff -> + srw Finmap.lookup_union_left_of_not_in + sby unfold Not=> /hsub } + move=> /[dup] /hsub /hdis /Finmap.lookup_eq_none -> + sby move=> /lookup_diff_none + + lemma intersect_comm (s2 d : state) (a₁ : loc) (b₁ : val) (a₂ : loc) (b₂ : val) : + (fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s) + ((fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s) d a₁ b₁) a₂ b₂ = + (fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s) + ((fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s) d a₂ b₂) a₁ b₁ := by + dsimp + scase: [a₁ ∈ s2]=> > /= + scase: [a₂ ∈ s2]=> > /= + apply Finmap.erase_erase + +def intersect (s1 s2 : state) := + s1.foldl (fun s x _ ↦ if x ∈ s2 then s else s.erase x) (intersect_comm s2) s1 + +def st1 : state := (Finmap.singleton 0 1).insert 1 1 +def st2 : state := ((Finmap.singleton 0 2).insert 2 2).insert 1 2 +#reduce intersect st1 st2 + +lemma insert_eq_union_singleton (s : state) : + p ∉ s → + s.insert p v = Finmap.singleton p v ∪ s := by + move=> ? + apply Finmap.ext_lookup=> > + scase: [x = p] + { move=> ? + sby srw Finmap.lookup_insert_of_ne } + move=> -> + sby srw Finmap.lookup_insert Finmap.lookup_union_left_of_not_in + +lemma AList_erase_entries (l : @AList loc (fun _ ↦ val)) : + (l.erase p).entries = (l.entries).kerase p := by sdone + +lemma Alist_insert_delete_id (l : @AList loc (fun _ ↦ val)) : + p ∉ l → + (l.insert p v).erase p = l := by + move=> ? + elim: l p v=> > /== + { move=> > + apply AList.ext=> /= + sby srw AList_erase_entries } + move=> ? ? > ??> + apply AList.ext=> /== + srw AList_erase_entries=> /== + sby srw List.kerase_of_not_mem_keys + +lemma intersect_foldl_mem (s₂ : state) (l₁ l₂ : @AList loc fun _ ↦ val): + p ∈ List.foldl (fun d s ↦ if s.fst ∈ s₂ then d else Finmap.erase s.fst d) + l₁.toFinmap l₂.entries → + p ∈ l₁ := by + elim: l₂ l₁=> > // + move=> ? ih /== + srw List.kerase_of_not_mem_keys=> // > + sby scase_if=> // ? /ih + +lemma intersect_mem_l (s₁ s₂ : state) : + p ∈ (intersect s₁ s₂) → p ∈ s₁ := by + refine Finmap.induction_on s₁ ? _ + move=> > + unfold intersect Finmap.foldl=> /== + elim: a=> //= + move=> > ? ih + srw List.kerase_of_not_mem_keys=> // + scase_if=> ? /== + { sby move=> /intersect_foldl_mem } + sby srw Alist_insert_delete_id + +lemma intersect_mem_r_helper (s₂ : state) (l : @AList loc fun _ ↦ val) : + (p ∈ List.foldl (fun d s ↦ if s.fst ∈ s₂ then d else Finmap.erase s.fst d) + l.toFinmap l.entries → p ∈ s₂) → + a ∈ s₂ → + p ∈ List.foldl (fun d s ↦ if s.fst ∈ s₂ then d else Finmap.erase s.fst d) + (AList.insert a b l).toFinmap l.entries → + p ∈ s₂ := by + elim: l=> > /== + { sby move=> _ ? /AList.mem_keys } + move=> ? ih1 > + srw List.kerase_of_not_mem_keys=> // + move=> ih2 ? + sorry + +lemma intersect_foldl_mem_s2 (s₂ : state) (l₁ : @AList loc fun _ ↦ val) : + p ∈ List.foldl (fun d s ↦ if s.fst ∈ s₂ then d else Finmap.erase s.fst d) + l₁.toFinmap l₁.entries → + p ∈ s₂ := by + elim: l₁=> // > + move=> ? ih /== + srw Alist_insert_delete_id=> // + srw List.kerase_of_not_mem_keys=> // + scase_if=> ? // + sorry + +lemma intersect_mem_r (s₁ s₂ : state) : + p ∈ (intersect s₁ s₂) → p ∈ s₂ := by + refine Finmap.induction_on s₁ ? _ + move=> > + unfold intersect Finmap.foldl=> /= + elim: a=> > //= + move=> ? ih + srw List.kerase_of_not_mem_keys=> //== + srw Alist_insert_delete_id=> // + scase_if=> // + move: ih=> /== /intersect_mem_r_helper ih + specialize (ih a b) + sby move=> /ih + +lemma mem_intersect : + p ∈ s₁ ∧ p ∈ s₂ → p ∈ (intersect s₁ s₂) := by + refine Finmap.induction_on s₁ ? _ + move=> > + unfold intersect Finmap.foldl=> /== + elim: a=> > //? ih ? /== + move=> ? + srw Alist_insert_delete_id=> // + srw List.kerase_of_not_mem_keys=> // + sorry + +@[simp] +lemma intersect_mem_iff (s₁ s₂ : state) : + p ∈ (intersect s₁ s₂) ↔ p ∈ s₁ ∧ p ∈ s₂ := by + apply Iff.intro + { sby move=> /[dup] /intersect_mem_l ? /intersect_mem_r } + apply mem_intersect + +lemma lookup_intersect (s₁ s₂ : state) : + p ∈ s₁ ∧ p ∈ s₂ → + (intersect s₁ s₂).lookup p = s₁.lookup p := by + move=> ? + refine Finmap.induction_on s₁ ? _ + move=> > + unfold intersect Finmap.foldl=> /== + elim: a=> > // + move=> ? ih /== + scase_if=> ? ; srw List.kerase_of_not_mem_keys=> // + { sorry } + srw Alist_insert_delete_id=> // + sorry + +lemma diff_insert_intersect_id (s₁ s₂ : state) : + (s₁ \ s₂) ∪ (intersect s₁ s₂) = s₁ := by + apply Finmap.ext_lookup=> > + scase: [x ∈ s₁] + { move=> /[dup] ? /Finmap.lookup_eq_none -> + srw Finmap.lookup_union_right=> // + have eqn:(x ∉ intersect s₁ s₂) := by sdone + sby move: eqn=> /Finmap.lookup_eq_none } + move=> ? + scase: [x ∈ s₂]=> ? + { srw Finmap.lookup_union_left=> // + sby srw lookup_diff } + srw Finmap.lookup_union_right=> // + sby srw lookup_intersect + +lemma union_monotone_r (s₃ s₁ s₂ : state) : + s₁ = s₂ → + s₁ ∪ s₃ = s₂ ∪ s₃ := by sdone + +lemma non_mem_union' (s₁ s₂ : state) : + x ∉ s₁ → x ∉ s₂ → x ∉ s₁ ∪ s₂ := by sdone + +lemma union_same_eq_r (s₁ s₂ s₃ : state) : + s₁.Disjoint s₃ → + s₂.Disjoint s₃ → + s₁ ∪ s₃ = s₂ ∪ s₃ → + s₁ = s₂ := by + move=> hdis₁ hdis₂ heq + apply Finmap.ext_lookup=> > + scase: [x ∈ s₁] + { move=> /[dup] /Finmap.lookup_eq_none -> + scase: [x ∈ s₃] + { move=> h /non_mem_union' + move: h=> /[swap] /[apply] + sby srw heq=> /== /Finmap.lookup_eq_none } + sby srw Finmap.Disjoint.symm_iff at hdis₂=> /hdis₂ /Finmap.lookup_eq_none } + move=> /[dup] /hdis₁ ? /Finmap.lookup_union_left h + specialize h s₃ ; sby srw -h heq Finmap.lookup_union_left_of_not_in + +lemma disjoint_intersect_r (s₁ s₂ s₃ : state) : + s₂.Disjoint s₃ → + (intersect s₁ s₂).Disjoint s₃ := by + sby unfold Finmap.Disjoint + +lemma intersect_disjoint_cancel (s₁ s₂ s₃ : state) : + s₁.Disjoint s₃ → + (s₁ ∪ intersect s₂ s₃) \ s₃ = s₁ := by + unfold Finmap.Disjoint=> hdis + apply Finmap.ext_lookup=> > + scase: [x ∈ s₁] + { move=> /[dup] ? /Finmap.lookup_eq_none -> + scase: [x ∈ s₃] + { move=> ? + srw lookup_diff=> // + srw Finmap.lookup_union_right=> // + sby srw Finmap.lookup_eq_none } + sby move=> /lookup_diff_none } + move=> /[dup] ? /hdis ? + sby srw lookup_diff diff --git a/Lgtm/Experiments/Dummy.lean b/Lgtm/Experiments/Dummy.lean index 3f8c985..d292f6d 100644 --- a/Lgtm/Experiments/Dummy.lean +++ b/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 diff --git a/Lgtm/Experiments/UnaryCommon.lean b/Lgtm/Experiments/UnaryCommon.lean index 63de1b9..4df9e1d 100644 --- a/Lgtm/Experiments/UnaryCommon.lean +++ b/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 diff --git a/Lgtm/Hyper/HProp.lean b/Lgtm/Hyper/HProp.lean index bd7eb76..6bfb330 100644 --- a/Lgtm/Hyper/HProp.lean +++ b/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 diff --git a/Lgtm/Hyper/ProofMode.lean b/Lgtm/Hyper/ProofMode.lean index 885f9dd..9ad20de 100644 --- a/Lgtm/Hyper/ProofMode.lean +++ b/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 diff --git a/Lgtm/Hyper/SepLog.lean b/Lgtm/Hyper/SepLog.lean index 85f2d51..832f7b6 100644 --- a/Lgtm/Hyper/SepLog.lean +++ b/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)) -> diff --git a/Lgtm/Hyper/WP.lean b/Lgtm/Hyper/WP.lean index d39760c..2084719 100644 --- a/Lgtm/Hyper/WP.lean +++ b/Lgtm/Hyper/WP.lean @@ -176,6 +176,29 @@ lemma hwp_for' (n₁ n₂ : α -> Int) (ht : α -> trm) (vr : α -> var) (Q : hv hwp s (fun a => trm_for (vr a) (n₁ a) (n₂ a) (ht a)) Q := by sby move=> ??; apply heval_for' +lemma hunion_equiv (h₁ h₂ : @hheap α) : + h₁ ∪ h₂ = fun a ↦ h₁ a ∪ h₂ a := by sdone + +lemma hwp_ref (x : α → var) (hv : α → val) (ht : α → trm) (Q : hval → hhProp) : + (h∀ (p : α → loc), p i ~⟨i in s⟩~> hv i -∗ + hwp s (fun a ↦ subst (x a) (p a) (ht a)) (Q ∗ ∃ʰ (u : α → val), p i ~⟨i in s⟩~> u i)) ==> + hwp s (fun a ↦ trm_ref (x a) (hv a) (ht a)) Q := +by + move=> > /hhforall_inv Hwp ; apply heval_ref=> > + move: (Hwp hp)=> {Hwp} /hhwand_inv Hwp hmem -- fun i ↦ Finmap.singleton (p i) (hv i) + specialize Hwp (fun i ↦ if i ∈ s then Finmap.singleton (hp i) (hv i) else ∅) + have eqn:((fun i ↦ if i ∈ s then Finmap.singleton (hp i) (hv i) else ∅) ∪ h = + fun i ↦ if i ∈ s then Finmap.insert (hp i) (hv i) (h i) else h i) := by + { srw hunion_equiv + apply funext=> > ; sby scase_if } + srw -eqn + apply Hwp=> {Hwp} /= > + { unfold hhsingle bighstar=> /= > + sby scase_if } + scase_if=> ? + { sby unfold Finmap.Disjoint } + apply Finmap.disjoint_empty + /- ------------------ Definition of [hwpgen] ------------------ -/ /- Defining [hmkstruct] -/ @@ -293,6 +316,13 @@ def wpgen_while (F1 F2 : hformula) : hformula := hmkstruct fun Q => let F := hwpgen_if_trm F1 (hwpgen_seq F2 R) (hwpgen_val fun _ => val_unit) ⌜hstructural R ∧ F ===> R⌝ -∗ R Q +def hwpgen_ref (s : Set α) (x : α → var) (ht₁ ht₂ : htrm) : hformula := + fun Q ↦ ∃ʰ hv : hval, ⌜ht₁ = fun a ↦ trm_val (hv a)⌝ ∗ + h∀ (p : α → loc), + (p i ~⟨i in s⟩~> hv i) -∗ + protect (hwp s (fun i ↦ subst (x i) (p i) (ht₂ i)) + (fun hv ↦ Q hv ∗ ∃ʰ u : hval, p i ~⟨i in s⟩~> u i)) + -- @[simp] -- abbrev isubst (E : ctx α) (a : α) (t : trm) : trm := -- match t with @@ -367,6 +397,9 @@ instance {x : α -> var} {t₁ t₂ : htrm} : instance {t₁ t₂ : htrm} : HWpSound s (fun a => trm_app (t₁ a) (t₂ a)) (hwpgen_app s (fun a => trm_app (t₁ a) (t₂ a))) := ⟨by sby move=> Q; srw hwpgen_app; ysimp⟩ +instance {x : α → var} {t₁ t₂ : htrm} : + HWpSound s (fun a ↦ trm_ref (x a) (t₁ a) (t₂ a)) (hwpgen_ref s x t₁ t₂) := ⟨by + move=> > ; srw hwpgen_ref ; ypull=> > ; apply hwp_ref ⟩ lemma hwp_of_hwpgen [inst: HWpSound s t F] : H ==> F Q -> @@ -379,7 +412,6 @@ example : if i > 0 then let x := 5 in let y := 7 in - free (x + y); y else y := x + 6; diff --git a/Lgtm/Unary/Arrays.lean b/Lgtm/Unary/Arrays.lean index 75d93e1..a5226b4 100644 --- a/Lgtm/Unary/Arrays.lean +++ b/Lgtm/Unary/Arrays.lean @@ -1,3 +1,5 @@ +import Lgtm.Common.State + import Lgtm.Unary.XSimp import Lgtm.Unary.XChange import Lgtm.Unary.Util @@ -6,110 +8,19 @@ import Lgtm.Unary.WP1 import Lgtm.Unary.Lang -/- ============== Definitions for Arrays ============== -/ - open val trm prim open Unary -def hheader (n : Int) (p : loc) : hProp := - p ~~> (val_int n) - -lemma hheader_eq p n : - (hheader n p) = (p ~~> (val_int n)) := by - sdone - -def hcell (v : val) (p : loc) (i : Int) : hProp := - ((p + 1 + (Int.natAbs i)) ~~> v) ∗ ⌜i >= 0⌝ - -lemma hcell_eq v p i : - (hcell v p i) = ((p + 1 + (Int.natAbs i)) ~~> v) ∗ ⌜i >= 0⌝ := by - sdone - -lemma hcell_nonneg v p i : - hcell v p i ==> hcell v p i ∗ ⌜i >= 0⌝ := by - sby srw hcell_eq ; xsimp - -def hseg (L : List val) (p : loc) (j : Int) : hProp := - match L with - | [] => emp - | x :: L' => (hcell x p j) ∗ (hseg L' p (j + 1)) - -def harray (L : List val) (p : loc) : hProp := - hheader (L.length) p ∗ hseg L p 0 - -lemma harray_eq p L : - harray L p = ∃ʰ n, ⌜n = L.length⌝ ∗ hheader n p ∗ hseg L p 0 := by - sby srw harray ; sorry - -/- inversion lemma for hseg -/ - -lemma hseg_start_eq L p j1 j2 : - j1 = j2 → - hseg L p j1 ==> hseg L p j2 := by - sdone - - -/- ================== Implementation of Arrays ================= -/ - -/- A simplified specification for non-negative pointer addition -/ - -lemma natabs_nonneg (p : Nat) (n : Int) : - n ≥ 0 → (p + n).natAbs = p + n.natAbs := by - omega +/- Syntax for array operations -/ -lemma triple_ptr_add_nonneg (p : loc) (n : Int) : - n >= 0 → - triple [lang| p ++ n] - emp - (fun r ↦ ⌜r = val_loc (p + Int.natAbs n)⌝) := by - move=> ? - apply (triple_conseq _ emp - (fun r ↦ ⌜r = val_loc (Int.toNat (Int.natAbs (p + n)))⌝)) - apply triple_ptr_add - { omega } - { xsimp } - xsimp ; xsimp=> /== - sby apply natabs_nonneg - - -/- Semantics of Low-Level Block Allocation -/ - -#check val_alloc - -#check eval.eval_alloc -/- eval.eval_alloc (n : ℤ) (sa : state) (Q : val → state → Prop) : - n ≥ 0 → - (∀ (p : loc) (sb : state), - sb = conseq val (make_list n.natAbs val_uninit) p → - p ≠ null → - Finmap.Disjoint sa sb → - Q p (sb ∪ sa)) → - eval sa (trm_app val_aloc n) Q - -/ - -/- Heap predicate for describing a range of cells -/ - -def hrange (L : List val) (p : loc) : hProp := - match L with - | [] => emp - | x :: L' => (p ~~> x) ∗ (hrange L' (p + 1)) - -lemma hrange_intro L p : - (hrange L p) (conseq L p) := by - induction L generalizing p ; srw conseq hrange=> // - apply hstar_intro=>// - sby apply disjoint_single_conseq - -lemma triple_alloc (n : Int) : - n ≥ 0 → - triple [lang| alloc n ] - emp - (funloc p ↦ hrange (make_list n.natAbs val_uninit) p ∗ ⌜p ≠ null⌝ ) := by - move=> ?? [] ; apply eval.eval_alloc=>// > * - apply (hexists_intro _ p) - srw hstar_hpure_l Finmap.union_empty hstar_hpure_r => ⟨|⟨|⟩⟩ // - subst sb ; apply hrange_intro +-- set_option pp.notation false +#check [lang| + let arr := mkarr 5 1 in + arr[4] := 2 ; + arr[3] + ] +/- ==================== Properties of Arrays ==================== -/ /- Implementing absolute value operator -/ @@ -136,18 +47,6 @@ lemma triple_abs (i : Int) : sby srw nonneg_eq_abs -/- Syntax for array operations -/ - --- set_option pp.notation false -#check [lang| - let arr := mkarr 5 1 in - arr[4] := 2 ; - arr[3] - ] - - -/- ==================== Properties of Arrays ==================== -/ - /- properties of [hseg] -/ lemma hseg_nil p j : @@ -408,24 +307,24 @@ lemma make_list_len (n : Int) (v : val) : move=> ? /= sby srw make_list -lemma triple_array_make_hseg (n : Int) (v : val) : - n >= 0 → - triple (trm_app val_array_make n v) - emp - (funloc p ↦ hheader n.natAbs p ∗ hseg (make_list (n.natAbs) v) p 0) := by - xwp - xapp triple_add ; xwp - xapp triple_alloc=> > ; xwp - rw [nat_abs_succ, make_list, hrange] - srw ?of_nat_nat //== ; any_goals omega - xapp ; xwp - srw -hheader_eq -(hseg_eq_hrange (make_list n.natAbs val_uninit) p 0) - xapp triple_array_fill ; xwp - { xval ; xsimp => // - apply himpl_of_eq - sby srw nonneg_eq_abs } - srw make_list_len - omega +-- lemma triple_array_make_hseg (n : Int) (v : val) : +-- n >= 0 → +-- triple (trm_app val_array_make n v) +-- emp +-- (funloc p ↦ hheader n.natAbs p ∗ hseg (make_list (n.natAbs) v) p 0) := by +-- xwp +-- xapp triple_add ; xwp +-- xapp triple_alloc=> > ; xwp +-- rw [nat_abs_succ, make_list, hrange] +-- srw ?of_nat_nat //== ; any_goals omega +-- xapp ; xwp +-- srw -hheader_eq -(hseg_eq_hrange (make_list n.natAbs val_uninit) p 0) +-- xapp triple_array_fill ; xwp +-- { xval ; xsimp => // +-- apply himpl_of_eq +-- sby srw nonneg_eq_abs } +-- srw make_list_len +-- omega lemma triple_array_get L (p : loc) (i : Int) : --(v : 0 <= i ∧ i < L.length) : 0 <= i ∧ i < L.length → @@ -455,18 +354,18 @@ lemma triple_array_length L (p : loc) : xapp triple_array_length_hheader xsimp -lemma triple_array_make (n : Int) (v : val) : - n ≥ 0 → - triple (trm_app val_array_make n v) - emp - (funloc p ↦ harray (make_list n.natAbs v) p) := by - move=> ? - xtriple - srw harray - xapp triple_array_make_hseg=> > - xsimp - { sdone } - sby srw make_list_len nonneg_eq_abs +-- lemma triple_array_make (n : Int) (v : val) : +-- n ≥ 0 → +-- triple (trm_app val_array_make n v) +-- emp +-- (funloc p ↦ harray (make_list n.natAbs v) p) := by +-- move=> ? +-- xtriple +-- srw harray +-- xapp triple_array_make_hseg=> > +-- xsimp +-- { sdone } +-- sby srw make_list_len nonneg_eq_abs /- Rules for [default_get] and [default_set] -/ diff --git a/Lgtm/Unary/Demos.lean b/Lgtm/Unary/Demos.lean index b068d5e..7f49439 100644 --- a/Lgtm/Unary/Demos.lean +++ b/Lgtm/Unary/Demos.lean @@ -2,17 +2,17 @@ import Lean import Lgtm.Unary.WP1 -open val prim trm +open val prim trm Unary /- ################################################################# -/ /-* * Demo Programs -/ #hint_xapp triple_lt #hint_xapp triple_get -#hint_xapp triple_ref +-- #hint_xapp triple_ref #hint_xapp triple_add #hint_xapp triple_set -#hint_xapp triple_free +-- #hint_xapp triple_free lang_def incr := fun p => @@ -32,23 +32,29 @@ lemma triple_incr (p : loc) (n : Int) : lang_def mysucc := fun n => - let r := ref n in + ref r := n in incr r; let x := !r in - free r; - x - -lang_def myfun := - fun n => - let x := ⟨1⟩ in x lemma triple_mysucc (n : Int) : { emp } [mysucc n] - {v, ⌜ v = n + 1 ⌝} := by - sdo 4 (xwp; xapp); - xwp; xval; xsimp=> // + {v, ⌜ v = val_int (n + 1) ⌝} := by + xwp ; -- xseq_xlet_if_needed ; xstruct_if_needed ; (apply xref_lemma) + xref r + xwp ; xapp + xwp ; xapp + xwp ; xval + xsimp_start + xsimp_step ; xsimp_step + -- xsimp_step + apply (xsimp_r_hexists) + xsimp_step + try rev_pure + try hide_mvars + try hsimp + lang_def addp := fun n m => @@ -62,17 +68,17 @@ lang_def addp := lemma triple_addp (p q : loc) (m n : Int) : { p ~~> n ∗ q ~~> m ∗ ⌜m >= 0⌝ } [addp p q] - { p ~~> n + m ∗ q ~~> m } := by + { p ~~> val_int (n + m) ∗ q ~~> m } := by xwp; xapp=> ? - xfor (fun i => p ~~> n + i)=> // + xfor (fun i => p ~~> val_int (n + i))=> // { move=> ? _; xapp; xsimp; omega } xapp lang_def mulp := fun n m => - let i := ref 0 in - let ans := ref 0 in + ref i := 0 in + ref ans := 0 in let m := !m in while ( let i := !i in @@ -102,9 +108,9 @@ lemma triple_mulp (p q : loc) (m n : Int) : { p ~~> n ∗ q ~~> m ∗ ⌜m > 0 ∧ n >= 0⌝ } [mulp p q] {ans, ⌜ans = n * m⌝ ∗ ⊤ } := by - xwp; xapp=> ? i - xwp; xapp=> ans - xwp; xapp + xwp ; xref i + xwp ; xref ans + xwp ; xapp xwhile_up (fun b j => p ~~> n ∗ q ~~> m ∗ i ~~> j ∗ ans ~~> n * j ∗ ⌜(b = decide (j < m)) ∧ 0 <= j ∧ j <= m⌝) m { xsimp=> // } { sby move=>>; xwp; xapp=> ?; xapp; xsimp } @@ -114,4 +120,5 @@ lemma triple_mulp (p q : loc) (m n : Int) : move=> ? /=; xsimp=> a /== * -- here we need to do [xsimp] before [xapp] -- to introduce variable [a], which is needed -- to instantiate the `ans` - sby xapp; xsimp + sby xapp; sorry + --xsimp --same xsimp bug as in [triple_mysucc] diff --git a/Lgtm/Unary/HProp.lean b/Lgtm/Unary/HProp.lean index 455df15..7741ae7 100644 --- a/Lgtm/Unary/HProp.lean +++ b/Lgtm/Unary/HProp.lean @@ -81,6 +81,9 @@ macro_rules | `($x ∗ $y) => `(binop% HStar.hStar $x $y) instance : HStar hProp hProp hProp where hStar := hstar +instance : HStar hProp (heap → Prop) hProp where + hStar := hstar + /- This notation sucks (`h` prefix is not uniform across other notations) But I dunno know what would be a better one -/ section @@ -161,6 +164,9 @@ infixr:55 " -∗ " => HWand.hWand instance : HWand hProp hProp hProp where hWand := hwand +instance : HWand hProp (heap → Prop) hProp where + hWand := hwand + instance (α : Type) : HWand (α → hProp) (α → hProp) hProp where hWand := qwand diff --git a/Lgtm/Unary/Lang.lean b/Lgtm/Unary/Lang.lean index e94bf83..a7ff3b8 100644 --- a/Lgtm/Unary/Lang.lean +++ b/Lgtm/Unary/Lang.lean @@ -11,10 +11,10 @@ open Classical /- =========================== Language Syntax =========================== -/ inductive prim where - | val_ref : prim + -- | val_ref : prim | val_get : prim | val_set : prim - | val_free : prim + -- | val_free : prim | val_neg : prim | val_opp : prim | val_eq : prim @@ -46,7 +46,7 @@ mutual | val_fix : var -> var -> trm -> val | val_uninit : val | val_error : val - | val_alloc : val + -- | val_alloc : val -- | val_array_make : val -- | val_array_length : val -- | val_array_get : val @@ -63,6 +63,8 @@ mutual | trm_if : trm -> trm -> trm -> trm | trm_for : var -> trm -> trm -> trm -> trm | trm_while : trm -> trm -> trm + | trm_ref : var → trm → trm → trm + | trm_alloc : var → trm → trm → trm end /- States and heaps are represented as finite maps -/ @@ -127,6 +129,8 @@ def subst (y : var) (v' : val) (t : trm) : trm := | trm_if t0 t1 t2 => trm_if (subst y v' t0) (subst y v' t1) (subst y v' t2) | trm_for x t1 t2 t3 => trm_for x (subst y v' t1) (subst y v' t2) (if_y_eq x t3 (subst y v' t3)) | trm_while t1 t2 => trm_while (subst y v' t1) (subst y v' t2) + | trm_ref x t1 t2 => trm_ref x (subst y v' t1) (if_y_eq x t2 (subst y v' t2)) + | trm_alloc x t1 t2 => trm_alloc x (subst y v' t1) (if_y_eq x t2 (subst y v' t2)) noncomputable def is_true (P : Prop) : Bool := if P then true else false @@ -358,6 +362,20 @@ inductive evalbinop : val → val → val → (val->Prop) → Prop where evalbinop val_ptr_add (val_loc p1) (val_int n) (fun v => v = val_loc (Int.natAbs p2)) +lemma evalunop_unique : + evalunop op v P → evalunop op v P' → P = P' := by + elim=> > + { sby move=> [] } + { sby move=> [] } + { sby move=> [] } + { sby move=> ? [] } + +lemma evalbinop_unique : + evalbinop op v1 v2 P → evalbinop op v1 v2 P' → P = P' := by + elim=> > + any_goals (sby move=> []) + all_goals (sby move=> ? []) + /- ========================= Big-step Semantics ========================= -/ @@ -411,6 +429,12 @@ def make_list {A} (n : Nat) (v : A) : List A := | 0 => [] | n' + 1 => v :: make_list n' v +def test1 : Finmap (fun _ : ℕ ↦ ℕ) := Finmap.singleton 0 1 +def test2 : Finmap (fun _ : ℕ ↦ ℕ) := Finmap.singleton 1 2 + +#reduce test1 \ test2 +-- { entries := Quot.mk List.Perm [⟨0, 1⟩], nodupKeys := ⋯ } + /- Big-step relation -/ inductive eval : state → trm → (val → state → Prop) -> Prop where @@ -460,11 +484,11 @@ inductive eval : state → trm → (val → state → Prop) -> Prop where evalbinop op v1 v2 P -> purepostin s P Q -> eval s (trm_app (trm_app op v1) v2) Q - | eval_ref : forall s v Q, - v = trm_val v' -> - (forall p, ¬ p ∈ s -> - Q (val_loc p) (Finmap.insert p v' s)) -> - eval s (trm_app val_ref v) Q + | eval_ref : forall s x t1 t2 (Q Q₁ : val → state → Prop), + eval s t1 Q₁ → + (∀ v1 s1, Q₁ v1 s1 → ∀ p ∉ s1, + eval (s1.insert p v1) (subst x p t2) fun v s ↦ Q v (s.erase p)) → + eval s (trm_ref x t1 t2) Q | eval_get : forall s p Q, p ∈ s -> Q (read_state p s) s -> @@ -474,18 +498,27 @@ inductive eval : state → trm → (val → state → Prop) -> Prop where p ∈ s -> Q val_unit (Finmap.insert p v' s) -> eval s (trm_app (trm_app val_set (val_loc p)) v) Q - | eval_free : forall s p Q, - p ∈ s -> - Q val_unit (Finmap.erase p s) -> - eval s (trm_app val_free (val_loc p)) Q - | eval_alloc : forall (n : Int) (sa : state) Q, - n ≥ 0 → - ( forall (p : loc) (sb : state), - sb = conseq (make_list n.natAbs val_uninit) p → - p ≠ null → - Finmap.Disjoint sa sb → - Q (val_loc p) (sb ∪ sa) ) → - eval sa (trm_app val_alloc n) Q + | eval_alloc_arg : forall s Q₁ Q, + ¬ trm_is_val t1 → + eval s t1 Q₁ → + (∀ v' s', Q₁ v' s' → eval s' (trm_alloc x v' t2) Q) → + eval s (trm_alloc x t1 t2) Q + | eval_alloc : forall (sa : state) (n : ℤ) Q, + n ≥ 0 → + (∀ (p : loc) (sb : state), + sb = conseq (make_list n.natAbs val_uninit) p → + p ≠ null → + Finmap.Disjoint sa sb → + eval (sb ∪ sa) (subst x p t2) fun v s ↦ Q v (s \ sb)) → + eval sa (trm_alloc x n t2) Q + -- | eval_alloc : forall (n : Int) (sa : state) Q, + -- n ≥ 0 → + -- ( forall (p : loc) (sb : state), + -- sb = conseq (make_list n.natAbs val_uninit) p → + -- p ≠ null → + -- Finmap.Disjoint sa sb → + -- Q (val_loc p) (sb ∪ sa) ) → + -- eval sa (trm_app val_alloc n) Q | eval_for (n₁ n₂ : Int) (Q : val -> state -> Prop) : eval s (if (n₁ < n₂) then (trm_seq (subst x n₁ t₁) (trm_for x (val_int (n₁ + 1)) n₂ t₁)) @@ -602,8 +635,142 @@ def eval_like (t1 t2:trm) : Prop := -- { move=> Q1 *; exists Q1 } +inductive evalExact : state → trm → (val → state → Prop) -> Prop where + | val : forall s v, + evalExact s (trm_val v) (fun v' s' ↦ v' = v ∧ s' = s) + | fun : forall s x t1, + evalExact s (trm_fun x t1) (fun v' s' ↦ v' = val_fun x t1 ∧ s' = s) + | fix : forall s f x t1, + evalExact s (trm_fix f x t1) (fun v' s' ↦ v' = val_fix f x t1 ∧ s' = s) + | app_arg1 : forall s1 t1 t2 Q1 Q, + ¬ trm_is_val t1 -> + evalExact s1 t1 Q1 -> + (forall v1 s2, Q1 v1 s2 -> evalExact s2 (trm_app v1 t2) Q) -> + evalExact s1 (trm_app t1 t2) Q + | app_arg2 : forall s1 (v1 : val) t2 Q1 Q, + ¬ trm_is_val t2 -> + evalExact s1 t2 Q1 -> + (forall v2 s2, Q1 v2 s2 -> evalExact s2 (trm_app v1 v2) Q) -> + evalExact s1 (trm_app v1 t2) Q + | app_fun : forall s1 v1 (v2 :val) x t1 Q, + v1 = val_fun x t1 -> + evalExact s1 (subst x v2 t1) Q -> + evalExact s1 (trm_app v1 v2) Q + | app_fix : forall s (v1 v2 : val) f x t1 Q, + v1 = val_fix f x t1 -> + evalExact s (subst x v2 (subst f v1 t1)) Q -> + evalExact s (trm_app v1 v2) Q + | seq : forall Q1 s t1 t2 Q, + evalExact s t1 Q1 -> + (forall v1 s2, Q1 v1 s2 -> evalExact s2 t2 Q) -> + evalExact s (trm_seq t1 t2) Q + | let : forall Q1 s x t1 t2 Q, + evalExact s t1 Q1 -> + (forall v1 s2, Q1 v1 s2 -> evalExact s2 (subst x v1 t2) Q) -> + evalExact s (trm_let x t1 t2) Q + | if : forall s (b : Bool) t1 t2 Q, + evalExact s (if b then t1 else t2) Q -> + evalExact s (trm_if (val_bool b) t1 t2) Q + | unop : forall op s v1 P, + evalunop op v1 P -> + evalExact s (trm_app op v1) (purepost s P) + | binop : forall op s (v1 v2 : val) P, + evalbinop op v1 v2 P -> + evalExact s (trm_app (trm_app op v1) v2) (purepost s P) + | ref : forall s x t1 t2 Q Q₁, + evalExact s t1 Q₁ → + (∀ v1 s1, Q₁ v1 s1 → ∀ p ∉ s1, + evalExact (s1.insert p v1) (subst x p t2) fun v s ↦ Q v (s.erase p)) → + evalExact s (trm_ref x t1 t2) Q + | get : forall s p, + p ∈ s -> + evalExact s (trm_app val_get (val_loc p)) + (fun v' s' ↦ v' = read_state p s ∧ s' = s) + | set : forall s p v, + v = trm_val v' -> + p ∈ s -> + evalExact s (trm_app (trm_app val_set (val_loc p)) v) + (fun v'' s' ↦ v'' = val_unit ∧ s' = s.insert p v') + | alloc_arg : forall s Q₁ Q, + ¬ trm_is_val t1 → + evalExact s t1 Q₁ → + (∀ v' s', Q₁ v' s' → evalExact s' (trm_alloc x v' t2) Q) → + evalExact s (trm_alloc x t1 t2) Q + | alloc : forall (sa : state) (n : ℤ) Q, + n ≥ 0 → + (∀ (p : loc) (sb : state), + sb = conseq (make_list n.natAbs val_uninit) p → + p ≠ null → + Finmap.Disjoint sa sb → + evalExact (sb ∪ sa) (subst x p t2) fun v s ↦ Q v (s \ sb)) → + evalExact sa (trm_alloc x n t2) Q + -- | alloc : forall (n : Int) (sa : state), + -- n ≥ 0 → + -- evalExact sa (trm_app val_alloc n) + -- (fun v s ↦ ∃ p, p ≠ null ∧ v = p ∧ + -- sa.Disjoint (conseq (make_list n.natAbs val_uninit) p) ∧ + -- s = conseq (make_list n.natAbs val_uninit) p ∪ sa ) + | for (n₁ n₂ : Int) (Q : val -> state -> Prop) : + evalExact s (if (n₁ < n₂) then + (trm_seq (subst x n₁ t₁) (trm_for x (val_int (n₁ + 1)) n₂ t₁)) + else val_unit) Q -> + evalExact s (trm_for x n₁ n₂ t₁) Q + | while (t₁ t₂ : trm) (Q Q₁ : val -> state -> Prop) : + evalExact s t₁ Q₁ -> + (∀ s v, Q₁ v s -> evalExact s (trm_if v (trm_seq t₂ (trm_while t₁ t₂)) val_unit) Q) -> + evalExact s (trm_while t₁ t₂) Q + + +def evalExact_ref_nonpositive s x t1 t2 (Q : val → state → Prop) := + ∃ Q₁, evalExact s t1 Q₁ ∧ + (∀ v1 s1, Q₁ v1 s1 → ∀ p ∉ s1, + (evalExact (s1.insert p v1) (subst x p t2) (fun v s ↦ Q v (s.erase p)))) + +def val.is_loc : val -> Prop + | val_loc _ => True + | _ => False + +example : + evalExact_ref_nonpositive ∅ "x" (trm_val (val_int 0)) (trm_var "x") fun v h => v.is_loc ∧ h = ∅ := by + unfold evalExact_ref_nonpositive + exists (fun v s ↦ v = 0 ∧ s = ∅)=> ⟨//| ⟩ + move=> > /= [->->] > ? ; simp [subst] + sorry + +lemma evalExact_post_eq : + Q = Q' → + evalExact s t Q → + evalExact s t Q' := by sdone + +lemma exact_imp_eval : + evalExact s t Q → eval s t Q := by + elim=> > + { sby constructor } + { sby constructor } + { sby constructor } + { move=> * ; sby constructor } + { move=> * ; sby apply eval.eval_app_arg2 } + { move=> * ; sby apply eval.eval_app_fun } + { move=> * ; sby apply eval.eval_app_fix } + { move=> ??? h ; apply (eval.eval_seq Q1)=>// ; exact h } + { move=> * ; sby constructor } + { move=> * ; sby constructor } + { move=> * ; apply eval.eval_unop=> // + sby unfold purepostin purepost } + { move=> * ; apply eval.eval_binop=> // + sby unfold purepostin purepost } + { move=> * ; sby apply eval.eval_ref } + { move=> * ; sby apply eval.eval_get } + { move=> * ; sby apply eval.eval_set } + { move=> * ; sby apply eval.eval_alloc_arg } + { move=> * ; sby apply eval.eval_alloc } + { move=> ?ih ; sby constructor } + move=> * ; sby constructor + + end eval + /- ================================================================= -/ /-* ** Notation for Concrete Terms -/ @@ -654,6 +821,8 @@ syntax:25 lang lang:30 : lang syntax "if " lang "then " lang "end " : lang syntax ppIndent("if " lang " then") ppSpace lang ppDedent(ppSpace) ppRealFill("else " lang) : lang syntax "let" ident " := " lang " in" ppDedent(ppLine lang) : lang +syntax "ref" ident " := " lang " in" ppDedent(ppLine lang) : lang +syntax "alloc" lang " as " ident " in" ppDedent(ppLine lang) : lang syntax "for" ident " in " "[" lang " : " lang "]" " {" (ppLine lang) ( " }") : lang syntax "while" lang " {" (ppLine lang) ( " }") : lang -- TODO: I suspect it should be `withPosition(lang ";") ppDedent(ppLine lang) : lang`, but Lean parser crashes. Report a bug. @@ -666,7 +835,7 @@ syntax uop lang:30 : lang syntax lang:30 bop lang:30 : lang syntax "(" lang ")" : lang syntax "⟨" term "⟩" : lang -syntax "alloc" lang : lang +-- syntax "alloc" lang : lang syntax "⟪" term "⟫" : lang syntax " := " : bop @@ -685,7 +854,7 @@ syntax " ++ " : bop syntax "!" : uop syntax "-" : uop -syntax "ref" : uop +-- syntax "ref" : uop syntax "free" : uop syntax "not" : uop syntax "mkarr" : uop @@ -710,6 +879,10 @@ macro_rules | `([lang| if $t1 then $t2 end]) => `(trm_if [lang| $t1] [lang| $t2] (trm_val val_unit)) | `([lang| let $x := $t1:lang in $t2:lang]) => `(trm_let $(%x) [lang| $t1] [lang| $t2]) + | `([lang| ref $x := $t1:lang in $t2:lang]) => + `(trm_ref $(%x) [lang| $t1] [lang| $t2]) + | `([lang| alloc $t1:lang as $x in $t2:lang]) => + `(trm_alloc $(%x) [lang| $t1] [lang| $t2]) | `([lang| $t1 ; $t2]) => `(trm_seq [lang| $t1] [lang| $t2]) | `([lang| fun_ $xs* => $t]) => do let xs <- xs.mapM fun x => `(term| $(%x)) @@ -723,10 +896,10 @@ macro_rules | `([lang| fix $f $xs* => $t]) => do let xs <- xs.mapM fun x => `(term| $(%x)) `(val_fixs $(%f) [ $xs,* ] [lang| $t]) - | `([lang| ref $t]) => `(trm_val (val_prim val_ref) [lang| $t]) + -- | `([lang| ref $t]) => `(trm_val (val_prim val_ref) [lang| $t]) | `([lang| free $t]) => `(trm_val (val_prim val_free) [lang| $t]) | `([lang| not $t]) => `(trm_val (val_prim val_not) [lang| $t]) - | `([lang| alloc $n]) => `(trm_val (val_alloc) [lang| $n]) + -- | `([lang| alloc $n]) => `(trm_val (val_alloc) [lang| $n]) | `([lang| !$t]) => `(trm_val val_get [lang| $t]) | `([lang| $t1 := $t2]) => `(trm_val val_set [lang| $t1] [lang| $t2]) | `([lang| $t1 + $t2]) => `(trm_val val_add [lang| $t1] [lang| $t2]) @@ -815,7 +988,7 @@ def val_array_fill : val := [lang| def val_array_make : val := [lang| fun n v => let m := n + 1 in - let p := alloc m in + alloc m as p in (val_set p) n ; (((val_array_fill p) 0) n) v ; p ] @@ -851,7 +1024,7 @@ macro_rules | _ => throw ( ) @[app_unexpander val_prim] def unexpandPrim : Lean.PrettyPrinter.Unexpander - | `($(_) val_ref) => `([uop| ref]) + -- | `($(_) val_ref) => `([uop| ref]) | `($(_) val_free) => `([uop| free]) | `($(_) val_not) => `([uop| not]) | `($(_) val_opp) => `([uop| -]) @@ -939,6 +1112,20 @@ macro_rules `([lang| let $name := $t1 in $t2]) | _ => throw ( ) +@[app_unexpander trm_ref] def unexpandRef : Lean.PrettyPrinter.Unexpander + | `($(_) $x:str [lang| $t1] [lang| $t2]) => + let str := x.getString + let name := Lean.mkIdent $ Lean.Name.mkSimple str + `([lang| ref $name := $t1 in $t2]) + | _ => throw ( ) + +@[app_unexpander trm_alloc] def unexpandAlloc : Lean.PrettyPrinter.Unexpander + | `($(_) $x:str [lang| $t1] [lang| $t2]) => + let str := x.getString + let name := Lean.mkIdent $ Lean.Name.mkSimple str + `([lang| alloc $t1 as $name in $t2]) + | _ => throw ( ) + @[app_unexpander trm_for] def unexpandFor : Lean.PrettyPrinter.Unexpander | `($(_) $x:str [lang| $n1] [lang| $n2] [lang| $t]) => let str := x.getString @@ -1011,9 +1198,9 @@ macro_rules `([lang| fix $nameF $nameX => $t]) | _ => throw ( ) -@[app_unexpander val_alloc] def unexpandVAlloc : Lean.PrettyPrinter.Unexpander - | `($(_) [lang| $n]) => `([lang| alloc $n]) - | _ => throw ( ) +-- @[app_unexpander val_alloc] def unexpandVAlloc : Lean.PrettyPrinter.Unexpander +-- | `($(_) [lang| $n]) => `([lang| alloc $n]) +-- | _ => throw ( ) -- @[app_unexpander trm_apps] def unexpandApps : Lean.PrettyPrinter.Unexpander -- -- Unexpand function applications when arguments are program-variables @@ -1086,21 +1273,22 @@ instance : HAdd ℤ ℕ val := ⟨fun x y => val_int (x + (y : Int))⟩ if F y z then for i in [z : y] { - let z := ref i in - let z := p[i] in - p[i] := z; + ref z := i in + ref x := i in !z } else for i in [z : y] { - let z := ref i in - let z := ref i in + ref z := i in + ref x := i in i := i +1; i := i +1; !z }; !z ] +#print val_array_make + -- set_option pp.notation false #check fun (p : loc) => [lang| fix f y z => @@ -1119,7 +1307,7 @@ instance : HAdd ℤ ℕ val := ⟨fun x y => val_int (x + (y : Int))⟩ i} ] #check [lang| 1 ++ 2] -#check [lang| let x := 6 in alloc(x)] +#check [lang| let x := 6 in alloc(x) as y in ()] #check fun (p : loc) => [lang| fix f y z => diff --git a/Lgtm/Unary/SepLog.lean b/Lgtm/Unary/SepLog.lean index 8e9439f..a36b054 100644 --- a/Lgtm/Unary/SepLog.lean +++ b/Lgtm/Unary/SepLog.lean @@ -1,5 +1,9 @@ -- import Ssreflect.Lang import Mathlib.Data.Finmap +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Multiset.Nodup + +import Lgtm.Common.State import Lgtm.Unary.Util import Lgtm.Unary.HProp @@ -38,139 +42,615 @@ lemma eval_conseq s t Q1 Q2 : by move=> heval srw (qimpl) (himpl)=> Imp - elim: heval ; move=> * ; constructor=>// - { sby constructor } - { sby apply eval.eval_app_arg2 } - { sby apply eval.eval_app_fun } - { sby apply eval.eval_app_fix } - { apply eval.eval_seq =>// - move=> * ; aesop } - { sby constructor=>// } - { apply eval.eval_unop=>// + elim: heval Q2 + { move=> * ; sby constructor } + { move=> * ; sby constructor } + { move=> * ; sby constructor } + { move=> * ; sby constructor } + { move=> * ; sby apply eval.eval_app_arg2 } + { move=> * ; sby apply eval.eval_app_fun } + { move=> * ; sby apply eval.eval_app_fix } + { move=> * ; apply eval.eval_seq =>// + move=> * ; aesop } + { move=> * ; sby constructor } + { move=> * ; sby constructor } + { move=> * ; apply eval.eval_unop=>// sby srw (purepostin) at * } - { apply eval.eval_binop=>// + { move=> * ; apply eval.eval_binop=>// sby srw (purepostin) at * } - { sby apply eval.eval_ref } - { sby apply eval.eval_get } - { sby apply eval.eval_set } - { apply eval.eval_free <;> try assumption - case eval_free.a Imp x y => - apply Imp - apply y } - { sby apply eval.eval_alloc } - { constructor=> // } - - -/- Useful Lemmas about disjointness and state operations -/ -lemma disjoint_update_not_r (h1 h2 : state) (x : loc) (v: val) : - Finmap.Disjoint h1 h2 → - x ∉ h2 → - Finmap.Disjoint (Finmap.insert x v h1) h2 := -by - srw Finmap.Disjoint => ?? - srw Finmap.Disjoint Finmap.mem_insert => ? - sby scase + { move=> * ; sby apply eval.eval_ref } + { move=> * ; sby apply eval.eval_get } + { move=> * ; sby apply eval.eval_set } + { move=> * ; sby constructor } + { move=> * ; sby apply eval.eval_alloc } + { move=> * ; sby constructor } + move=> * ; sby constructor -lemma in_read_union_l (h1 h2 : state) (x : loc) : - x ∈ h1 → read_state x (h1 ∪ h2) = read_state x h1 := -by - move=> ? - srw []read_state - sby srw (Finmap.lookup_union_left) -lemma disjoint_insert_l (h1 h2 : state) (x : loc) (v : val) : - Finmap.Disjoint h1 h2 → - x ∈ h1 → - Finmap.Disjoint (Finmap.insert x v h1) h2 := -by - srw Finmap.Disjoint => * - srw Finmap.Disjoint Finmap.mem_insert => ? - sby scase - -lemma remove_disjoint_union_l (h1 h2 : state) (x : loc) : - x ∈ h1 → Finmap.Disjoint h1 h2 → - Finmap.erase x (h1 ∪ h2) = Finmap.erase x h1 ∪ h2 := -by - srw Finmap.Disjoint => * ; apply Finmap.ext_lookup => y - scase: [x = y]=> hEq - { scase: [y ∈ Finmap.erase x h1]=> hErase - { srw Finmap.lookup_union_right - rw [Finmap.lookup_erase_ne] - apply Finmap.lookup_union_right - srw Finmap.mem_erase at hErase=>// - srw Not at * => * // - sby srw Not } - srw Finmap.lookup_union_left - sby sdo 2 rw [Finmap.lookup_erase_ne] } - srw -hEq - srw Finmap.lookup_union_right=>// - srw Finmap.lookup_erase - apply Eq.symm - sby srw Finmap.lookup_eq_none - -lemma disjoint_remove_l (h1 h2 : state) (x : loc) : - Finmap.Disjoint h1 h2 → - Finmap.Disjoint (Finmap.erase x h1) h2 := -by - srw Finmap.Disjoint=> ?? - sby srw Finmap.mem_erase +/- ============== Necessary Lemmas about [eval] and [evalExact] ============== -/ + +lemma finite_state (s : state) : + ∃ p, p ∉ s := by + scase: [s.keys.Nonempty] + { srw Finset.nonempty_iff_ne_empty=> /== ? + exists 0 ; unfold Not + sby srw -Finmap.mem_keys } + move=> /Finset.max_of_nonempty [>] + have eqn:(w < w + 1) := by sdone + move: eqn=> /Finset.not_mem_of_max_lt /[apply] ? + exists (w + 1) + +lemma conseq_ind (n : ℕ) (v : val) (p : loc) : + x ∈ conseq (make_list n v) p → x ≥ p := by + elim: n p=> > // + move=> ih > + unfold conseq make_list=> /== [] // + move=> /ih ; omega + +lemma finite_state' n (s : state) : + ∃ p, p ≠ null ∧ + Finmap.Disjoint s (conseq (make_list n val_uninit) p) := by + scase: [s.keys.Nonempty] + { srw Finset.nonempty_iff_ne_empty=> /== ? + exists 1 ; unfold null Finmap.Disjoint=> /== > + sby srw -Finmap.mem_keys } + move=> /Finset.max_of_nonempty [>] hmax + exists (w + 1)=> ⟨|⟩ + { sby unfold null } + unfold Finmap.Disjoint=> > + move: hmax=> /[swap] + srw -Finmap.mem_keys=> /Finset.le_max_of_eq /[apply] ? + unfold Not=> /conseq_ind /== + sby srw Nat.lt_succ_iff + +lemma eval_sat : + eval h t Q -> ∃ h v, Q h v := by + elim=> // > + { move=> ??? ![>?]; sapply=> // } + { move=> ??? ![>?]; sapply=> // } + { move=> ?? ![>?]; sapply=> // } + { move=> ?? ![>?]; sapply=> // } + { scase=> > + any_goals move=> pp; (sdo 2 econstructor); apply pp=> // + move=> ? pp; sdo 2 econstructor; apply pp=> //} + { scase=> > + any_goals move=> pp; (sdo 2 econstructor); apply pp=> // + any_goals move=> ? pp; (sdo 2 econstructor); apply pp=> // } + { move=> ?? ![>] /[swap] /[apply] + scase: (finite_state w_1)=> p hp + sby move: hp=> /[swap] /[apply] ![>] } + { sby move=> ??? ![>] /[swap] /[apply] } + { move=> ?? /== ih + scase: (finite_state' n.natAbs sa) + sby move=> p [] /ih /[apply] ![>] } + move=> ? /[swap]![>] /[swap] _ /[swap]/[apply]// + +lemma evalExact_sat : + evalExact s t Q → ∃ v s, Q v s := by + elim=> > // + { move=> _ _ _ ![] > /[swap] ; sapply } + { move=> _ _ _ ![] > /[swap] ; sapply } + { move=> _ _ ![] > /[swap] ; sapply } + { move=> _ _ ![] > /[swap] ; sapply } + { sby move=> [] } + { sby move=> [] } + { move=> ?? ![>] /[swap] /[apply] + scase: (finite_state w_1)=> p hp + sby move: hp=> /[swap] /[apply] ![>] } + { sby move=> _ _ _ ![>] /[swap] /[apply] } + { move=> ? _ /== ih + scase: (finite_state' n.natAbs sa) + sby move=> p [] /ih /[apply] ![>] } + move=> ? /[swap]![>] /[swap] _ /[swap]/[apply]// + +lemma evalExact_post : + eval s t Q → evalExact s t Q' → Q' ===> Q:= by + move=> H + elim: H Q'=> > + -- elim=> > + { sby move=> ? > [] v h /== } + { sby move=> ? > [] v h /== } + { sby move=> ? > [] v h /== } + { move=> ??? ih1 ih2 > [] // > + { move=> > _ /[dup] h h' + apply evalExact_sat in h=> ![] v s' /[dup] hQ1_1 hQ1_1' + apply ih1 in h'=> himp hev + apply himp in hQ1_1 + sby apply hev in hQ1_1'=> ? /ih2 } + { move=> ? + scase: op=> > ? // + scase: a=> > ? // [] // } + move=> ? [] // } + { move=> ? _ _ ih1 ih2 > [] // > _ /[dup] h h' + apply evalExact_sat in h=> ![] v s' /[dup] hQ1_1 hQ1_1' + apply ih1 in h'=> himp hev + apply himp in hQ1_1 + sby apply hev in hQ1_1'=> ? /ih2 } + { sby move=> [] ?? > [] } + { sby move=> [] ?? > [] } + { move=> _ _ ih1 ih2 > [] > /[dup] h h' + apply evalExact_sat in h=> ![] v s' > /[dup] hQ1_1 hQ1_1' hev + apply ih1 in h'=> himp + apply himp in hQ1_1 + sby apply hev in hQ1_1'=> ? /ih2 } + { move=> _ _ ih1 ih2 > [] > /[dup] h /evalExact_sat ![] v s' + move=> /[dup] hQ1_1 hQ1_1' hev + apply ih1 in h=> himp + apply himp in hQ1_1 + sby apply hev in hQ1_1'=> ? /ih2 } + { sby move=> _ ih > [] } + { unfold purepostin=> hOP ? > [] // + apply evalunop_unique in hOP=> hP + move=> > /hP [] + sby unfold purepost=> ?? } + { unfold purepostin=> hOP ? > [] // + { scase: op=> > // + scase: a=> > // ? > ? [] // } + apply evalbinop_unique in hOP=> hP + move=> > /hP [] + sby unfold purepost=> ?? } + { move=> ?? ih1 ih2 > [Q₁'] hevEx hev + move=> > h + move: hevEx hev + move=> /[dup] /ih1 {} ih1 /evalExact_sat ![>] /[dup] /ih1 {}ih1 + move=> /[swap] /[apply] + scase: (finite_state (h ∪ w_1))=> p /non_mem_union [] ? hp + move: hp=> /[dup] hp /[swap] /[apply] + move: ih1 hp=> /ih2 /[apply] {}ih2 + specialize (@ih2 fun v (s : state) ↦ Q' v (s.erase p)) + move: ih2=> /[apply] + unfold qimpl himpl=> /== ? + sby srw (insert_delete_id h p) } + { sby move=> ?? > [] // _ ?? } + { move=> [] ?? > [] // + { move=> > ? [] // } + sby move=> > _ [] ?? } + { move=> ? _ _ ih1 ih2 > [] // + move=> Q₁' ? /[dup] /ih1 {}ih1 /evalExact_sat ![>] /[dup] /ih1 {} ih1 + move=> /[swap] /[apply] + sby move: ih1=> /ih2 } + { move=> ? _ /== ih > hev + move=> > h + move: hev=> [] // _ /== hev + scase: (finite_state' n.natAbs (sa ∪ h)) + move=> p [] /[dup] /ih {}ih /hev {}hev /Finmap.disjoint_union_left [] + move=> /[dup] /hev /[swap] /ih {}ih {hev} /ih {}ih /union_difference_id <- + sby move=> /ih } + { sby move=> ?? > [] } + { move=> ?? ih1 ih2 > [] Q₁' + move=> /[dup] /ih1 {}ih1 /evalExact_sat ![>] /[dup] /ih1 {}ih1 + move=> /[swap] /[apply] + sby move: ih1=> /ih2 } + +lemma evalExact_WellAlloc : + evalExact s t Q → + Q v s' → + s'.keys = s.keys := by + move=> hev + elim: hev s' v + { sby move=> > [] } + { sby move=> > [] } + { sby move=> > [] } + { move=> > _ /evalExact_sat ![>] /[dup] hQ1 /[swap] _ /[swap] /[apply] heq + move: hQ1=> /[swap] /[apply] /[apply] + sby srw heq=> {}heq > /heq } + { move=> > _ /evalExact_sat ![>] /[dup] hQ1 /[swap] _ /[swap] /[apply] heq + move: hQ1=> /[swap] /[apply] /[apply] + sby srw heq=> {}heq > /heq } + { sby move=> > _ _ ih > /ih } + { sby move=> > _ _ ih > /ih } + { move=> > /evalExact_sat ![>] /[dup] hQ1 /[swap] _ /[swap] /[apply] heq + move: hQ1=> /[swap] /[apply] /[apply] + sby srw heq=> {}heq > /heq } + { move=> > /evalExact_sat ![>] /[dup] hQ1 /[swap] _ /[swap] /[apply] heq + move: hQ1=> /[swap] /[apply] /[apply] + sby srw heq=> {}heq > /heq } + { sby move=> > _ ih > /ih } + { sby unfold purepost } + { sby unfold purepost } + { move=> > /evalExact_sat ![>] /[dup] hQ₁ /[swap] /[apply] ? ih1 ih2 > + move: hQ₁=> /[dup] hQ₁ /ih1 {}ih1 + scase: (finite_state (s' ∪ w_1))=> p /non_mem_union [] + move=> /[dup] /insert_same hins ? /[dup] /hins {}hins + move: hQ₁=> /ih2 /[apply] /== {}ih2 + srw [1](insert_delete_id s' p)=> // + sby move=> /ih2 /hins } + { sdone } + { move=> > _ ? > /= [] _ [] + sby srw insert_mem_keys } + { move=> > _ /evalExact_sat ![>] /[dup] hQ₁ /[swap] _ /[swap] /[apply] ? + sby move: hQ₁=> /[swap] /[apply] ih > /ih } + { move=> > ? _ ih > + scase: (finite_state' n.natAbs (sa ∪ s')) + move=> p [] /ih /== {}ih /Finmap.disjoint_union_left /[dup] hdisj [] /ih {}ih + move=> /union_difference_id heq + srw -[1]heq=> /ih + srw [2]Finmap.union_comm_of_disjoint ; rotate_left + { sby srw Finmap.Disjoint.symm_iff } + sby move: hdisj=> [] /[swap] /union_same_keys /[apply] } + { sby move=> > _ ih > /ih } + move=> > /evalExact_sat ![>] /[dup] hQ1 /[swap] _ /[swap] /[apply] heq + move: hQ1=> /[swap] /[apply] /[apply] + sby srw heq=> {}heq > /heq + +lemma evalExact_det : + evalExact s t Q → + Q v₁ s₁ → + Q v₂ s₂ → + v₁ = v₂ ∧ s₁ = s₂ := by + move=> heval + elim: heval v₁ v₂ s₁ s₂ + { sdone } + { sdone } + { sdone } + { move=> > _ /evalExact_sat ![>] /[swap] _ /[swap] _ /[swap] /[apply] ih + sby move=> > /ih /[apply] } + { move=> > _ /evalExact_sat ![>] /[swap] _ /[swap] _ /[swap] /[apply] ih + sby move=> > /ih /[apply] } + { sby move=> > ?? ih > /ih /[apply] } + { sby move=> > ?? ih > /ih /[apply] } + { move=> > /evalExact_sat ![>] /[swap] _ /[swap] _ /[swap] /[apply] ih + sby move=> > /ih /[apply] } + { move=> > /evalExact_sat ![>] /[swap] _ /[swap] _ /[swap] /[apply] ih + sby move=> > /ih /[apply] } + { sby move=> > _ ih > /ih /[apply] } + { unfold purepost=> > ; scase: op=> > // + { sby move=> [>] } + { sby move=> [] > } + sorry } -- can't have val_rand + { unfold purepost=> > ; scase: op=> // > + scase: a=> // + any_goals (sby move=> [] >) } + { move=> > hev₁ hev₂ ih1 ih2 > + scase: (finite_state s_1)=> p ? + have hev:(evalExact s_1 (trm_ref x t1 t2) Q_1) := by + { sby apply evalExact.ref } + move: hev hev₁=> /evalExact_WellAlloc hev + move=> /[dup] /evalExact_sat ![>] /[dup] /ih2 {}ih2 /evalExact_WellAlloc /[apply] heq + have eqn:(p ∉ w_1) := by + { unfold Not=> /Finmap.mem_keys ; sby srw heq } + apply ih2 in eqn=> {}ih2 {heq} + move=> /[dup] /hev heq₁ + have hs₁:(p ∉ s₁) := by + { unfold Not=> /Finmap.mem_keys ; sby srw heq₁ } + srw [1](insert_delete_id s₁ p) ; rotate_left ; apply hs₁=> {heq₁} + apply w=> /ih2 {}ih2 /[dup] /hev heq₂ {hev} + have hs₂:(p ∉ s₂) := by + { unfold Not=> /Finmap.mem_keys ; sby srw heq₂ } + srw [1](insert_delete_id s₂ p) ; rotate_left ; apply hs₂=> {heq₂} + apply w=> /ih2 ? ⟨//|⟩ + sby apply (@insert_same_eq p w s₁ s₂) } + { sdone } + { sdone } + { move=> > _ /evalExact_sat ![>] /[swap] _ /[swap] _ /[swap] /[apply] ih + sby move=> > /ih /[apply] } + { move=> > ? + scase: (finite_state' n.natAbs sa)=> p [hp hsb] /== hev ih > + have hev':(evalExact sa (trm_alloc x n t2) Q_1) := by + { sby apply evalExact.alloc } + move: hev' hp hsb=> {hev} /evalExact_WellAlloc hwa /ih + move=> /[swap] /[dup] hsb /[swap] /[apply] {}ih + move=> /[dup] /hwa heq₁ + have hdis₁:(s₁.Disjoint (conseq (make_list n.natAbs val_uninit) p)) := by + { unfold Finmap.Disjoint ; srw -Finmap.mem_keys heq₁ Finmap.mem_keys + apply hsb } + srw -[1](diff_disjoint_eq s₁ (conseq (make_list n.natAbs val_uninit) p) + (conseq (make_list n.natAbs val_uninit) p)) + rotate_left ; apply hdis₁ ; rfl + move=> /ih {}ih {heq₁} /[dup] /hwa {hwa} heq₂ + have hdis₂: (s₂.Disjoint (conseq (make_list n.natAbs val_uninit) p)) := by + { unfold Finmap.Disjoint ; srw -Finmap.mem_keys heq₂ Finmap.mem_keys + apply hsb } + srw -[1](diff_disjoint_eq s₂ (conseq (make_list n.natAbs val_uninit) p) + (conseq (make_list n.natAbs val_uninit) p)) + rotate_left ; apply hdis₂ ; rfl + move=> {hsb heq₂} /ih {ih} [??] ⟨//|⟩ + sby apply union_same_eq_r } + { sby move=> > _ ih > /ih /[apply] } + move=> > /evalExact_sat ![>] /[swap] _ /[swap] _ /[swap] /[apply] + sby move=> ih > /ih /[apply] + +lemma eval_imp_exact : + eval s t Q → ∃ Q', evalExact s t Q' := by + elim=> > + { sby move=> * ; exists (fun v' s' ↦ v' = v ∧ s' = s_1) } + { sby move=> * ; exists (fun v' s' ↦ v' = (val_fun x t1) ∧ s' = s_1) } + { sby move=> * ; exists (fun v' s' ↦ v' = (val_fix f x t1) ∧ s' = s_1) } + { move=> ? /evalExact_post hpost ? [Q1'] /[dup] /hpost {}hpost + move=> /[dup] /evalExact_det hdet /[dup] ? /evalExact_sat ![>] /[dup] /hdet {}hdet + move=> /hpost /[swap] /[apply] [Q'] ? + exists Q' ; apply evalExact.app_arg1=> // + sby move=> > /hdet [] } + { move=> ? /evalExact_post hpost ? [Q1'] /[dup] /hpost {}hpost + move=> /[dup] /evalExact_det hdet /[dup] ? /evalExact_sat ![>] /[dup] /hdet {}hdet + move=> /hpost /[swap] /[apply] [Q'] ? + exists Q' ; apply evalExact.app_arg2=> // + sby move=> > /hdet [] } + { move=> [] ? [Q'] ? + exists Q' + sby apply evalExact.app_fun } + { move=> [] ? [Q'] ? + exists Q' + sby apply evalExact.app_fix } + { move=> /evalExact_post hpost ? [Q1'] /[dup] /hpost {}hpost + move=> /[dup] /evalExact_det hdet /[dup] ? /evalExact_sat ![>] /[dup] /hdet {}hdet + move=> /hpost /[swap] /[apply] [Q'] ? + exists Q' ; apply evalExact.seq=> // + sby move=> > /hdet [] } + { move=> /evalExact_post hpost ? [Q1'] /[dup] /hpost {}hpost + move=> /[dup] /evalExact_det hdet /[dup] ? /evalExact_sat ![>] /[dup] /hdet {}hdet + move=> /hpost /[swap] /[apply] [Q'] ? + exists Q' ; apply evalExact.let=> // + sby move=> > /hdet [] } + { move=> ? [Q'] ? + exists Q' + sby constructor } + { move=> ?? + exists (purepost s_1 P) + sby apply evalExact.unop } + { move=> ?? + exists (purepost s_1 P) + sby apply evalExact.binop } + { move=> /evalExact_post hpost hev [Q₁'] /[dup] /hpost {}hpost + move=> /[dup] /evalExact_det hdet /[dup] ? /evalExact_sat ![>] /[dup] /hdet {}hdet + move=> /hpost /[swap] /[apply] + scase: (finite_state w_1)=> p /[swap] /[apply] [Q'] hex + exists (fun v' ↦ (∃ʰ u, p ~~> u) -∗ Q' v') + apply evalExact.ref + { sdone } + move=> > /hdet [<-<-] p' + -- exists (fun v' s' ↦ Q' v' (s'.insert p w)) ; apply evalExact.ref + -- { sdone } + -- move=> > /hpost /hev {}hev p_1 + sorry } + { move=> * + exists (fun v' s' ↦ v' = read_state p s_1 ∧ s' = s_1) + sby apply evalExact.get } + { move=> * + exists (fun v'' s' ↦ v'' = val_unit ∧ s' = s_1.insert p v') + sby apply evalExact.set } + { move=> ? /evalExact_post hpost ? [Q1'] /[dup] /hpost {}hpost + move=> /[dup] /evalExact_det hdet /[dup] ? /evalExact_sat ![>] /[dup] /hdet {}hdet + move=> /hpost /[swap] /[apply] [Q'] ? + exists Q' ; apply evalExact.alloc_arg=> // + sby move=> > /hdet [] } + { move=> ? /== hev ih + sorry } + { move=> ? [Q'] ? + sby exists Q' } + move=> /evalExact_post hpost ? [Q1'] /[dup] /hpost {}hpost + move=> /[dup] /evalExact_det hdet /[dup] ? /evalExact_sat ![>] /[dup] /hdet {}hdet + move=> /hpost /[swap] /[apply] [Q'] ? + exists Q' ; apply evalExact.while=> // + sby move=> > /hdet [] + + +/- ----------------------------- Frame Rule ----------------------------- -/ abbrev tohProp (h : heap -> Prop) : hProp := h abbrev ofhProp (h : val -> hProp) : val -> heap -> Prop := h -lemma eval_frame (h1 h2 : state) t (Q : val -> hProp) : - eval h1 t (ofhProp Q) → +lemma frame_eq_rw : + s.Disjoint h2 → + (fun v' s' ↦ v' = v ∧ s' = s ∪ h2) = + (qstar (fun v' s' ↦ v' = v ∧ s' = s) (tohProp (fun h ↦ h = h2))) := by + move=> ? ; funext=> /== + apply Iff.intro + { move=> [] * + exists s, h2 } + unfold tohProp + sby move=> ![] > + +lemma evalExact_frame_val (v : val) (s h2 : state) : + s.Disjoint h2 → + evalExact (s ∪ h2) t (fun v' s' ↦ v' = v ∧ s' = s ∪ h2) → + evalExact (s ∪ h2) t + (qstar (fun v' s' ↦ v' = v ∧ s' = s) (tohProp (fun h ↦ h = h2))) := by + move=> ? + sby srw frame_eq_rw + +lemma purepost_frame : + s.Disjoint h2 → + (purepost (s ∪ h2) P) = + (qstar (purepost s P) (tohProp fun h ↦ h = h2)) := by + move=> ? + unfold purepost tohProp + funext=> /== + apply Iff.intro + { move=> [] * + exists s, h2 } + sby move=> ![>] + +lemma evalExact_frame_unop_binop : + s.Disjoint h2 → + evalExact (s ∪ h2) t (purepost (s ∪ h2) P) → + evalExact (s ∪ h2) t (qstar (purepost s P) (tohProp fun h ↦ h = h2)) := by + move=> ? + sby srw purepost_frame + +lemma read_state_frame : + s.Disjoint h2 → + p ∈ s → + (fun v' s' ↦ v' = read_state p (s ∪ h2) ∧ s' = s ∪ h2 ) = + (qstar (fun v' s' ↦ v' = read_state p s ∧ s' = s) (tohProp fun h ↦ h = h2)) := by + move=> ?? + unfold tohProp + funext=> /== + apply Iff.intro + { sby srw in_read_union_l } + srw in_read_union_l + sby move=> ![>] + +lemma evalExact_frame_get : + s.Disjoint h2 → + p ∈ s → + evalExact (s ∪ h2) t (fun v' s' ↦ v' = read_state p (s ∪ h2) ∧ s' = s ∪ h2 ) → + evalExact (s ∪ h2) t + (qstar (fun v' s' ↦ v' = read_state p s ∧ s' = s) (tohProp fun h ↦ h = h2)) := by + move=> ?? + sby srw read_state_frame + +lemma insert_frame : + s.Disjoint h2 → + p ∈ s → + fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' (s ∪ h2) = + (qstar (fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' s) (tohProp fun h ↦ h = h2)) := by + move=> ?? + unfold tohProp + funext=> /== + apply Iff.intro + { srw Finmap.insert_union + move=> [] * + exists Finmap.insert p v' s, h2=> /== ⟨|⟩ // ⟨|⟩ + sby apply disjoint_insert_l } + move=> ![>] /== [] [] [] ? [] /== + sby srw Finmap.insert_union + +lemma evalExact_frame_set : + s.Disjoint h2 → + p ∈ s → + evalExact (s ∪ h2) t + (fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' (s ∪ h2)) → + evalExact (s ∪ h2) t + (qstar (fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' s) (tohProp fun h ↦ h = h2)) := by + move=> ?? + sby srw insert_frame + +lemma evalExact_frame (h1 h2 : state) t (Q : val → hProp) : + evalExact h1 t (ofhProp Q) → Finmap.Disjoint h1 h2 → - eval (h1 ∪ h2) t (Q ∗ (tohProp (fun h ↦ h = h2))) := + evalExact (h1 ∪ h2) t (Q ∗ (tohProp (fun h ↦ h = h2))) := by simp [ofhProp] move=> /== heval elim: heval h2 - { sby move=> * } - { sby move=> * } - { sby move=> * } + { move=> > * + sby apply evalExact_frame_val } + { move=> > * + sby apply evalExact_frame_val } + { move=> > * + sby apply evalExact_frame_val } { move=> ???????? ih1 ?? /ih1 ? ; constructor=>// sby move=> ?? ![] } - { move=> ???????? ih1 ?? /ih1 ? ; apply eval.eval_app_arg2=>// + { move=> ???????? ih1 ?? /ih1 ? ; apply evalExact.app_arg2=>// sby move=> ?? ![] } - { sby move=> * ; apply eval.eval_app_fun } - { sby move=> * ; apply eval.eval_app_fix } - { move=> ??????? ih1 ih2 ? /ih1 ? ; apply eval.eval_seq=>// + { sby move=> * ; apply evalExact.app_fun } + { sby move=> * ; apply evalExact.app_fix } + { move=> ??????? ih1 ih2 ? /ih1 ? ; apply evalExact.seq=>// move=> ? s2 ![??? hQ2 *] ; subst s2 hQ2 sby apply ih2 } - { move=> ???????? ih1 ih2 ? /ih1 ? ; apply eval.eval_let=>// + { move=> ???????? ih1 ih2 ? /ih1 ? ; apply evalExact.let=>// move=> ?? ![??? hQ2 ? hU] ; subst hU hQ2 sby apply ih2} { sby move=> * } - { move=> * ; apply eval.eval_unop=>// - srw purepostin at * => ?? - sby apply hstar_intro } - { move=> * ; apply eval.eval_binop=>// - srw purepostin at * => ?? - sby apply hstar_intro } - { move=> * ; apply eval.eval_ref=>// - move=> ? ; srw (Not) (Finmap.insert_union) => ? - apply hstar_intro=>// + { move=> > ? > * + apply evalExact_frame_unop_binop=> // + sby apply evalExact.unop } + { move=> > ? > * + apply evalExact_frame_unop_binop=> // + sby apply evalExact.binop } + { move=> > ; unfold tohProp + move=> _ _ ih1 ih2 > /ih1 {}ih1 + apply evalExact.ref + { apply ih1 } + move=> {ih1} > ![>] hQ₁ /= -> ? -> p ? + have eqn:(p ∉ w) := by sdone + have eqn':((w.insert p v1).Disjoint h2) := by sby apply disjoint_update_not_r + move: hQ₁ eqn eqn'=> /ih2 /[apply] /[apply] {ih2} + srw insert_union=> // hq + apply evalExact_post_eq ; rotate_left ; apply hq + apply funext=> v ; apply funext=> h ; apply propext=> ⟨|⟩ + { move=> ![>] /= ? -> ? -> + exists (w_2.erase p), h2=> ⟨//|/==⟩ ⟨|⟩ + apply erase_disjoint=> // + sby srw remove_not_in_r } + move=> ![>] /= ? -> ? + scase: [p ∈ h] + { move=> ? ; srw erase_of_non_mem=> // [] + exists w_2, h2=> /== ⟨|⟩ // + sby srw erase_of_non_mem } + move=> /Finmap.mem_iff [v'] /reinsert_erase_union heq herase + srw (heq w_2 h2)=> // {heq} + exists (w_2.insert p v'), h2=> /== ⟨|⟩ + { srw -insert_delete_id=> // + have eqn:(p ∉ h.erase p) := by apply Finmap.not_mem_erase_self + move: eqn + sby srw herase } sby apply disjoint_update_not_r } - { move=> * ; apply eval.eval_get=>// - srw in_read_union_l ; sby apply hstar_intro } - { move=> * ; apply eval.eval_set=>// - srw qstarE Finmap.insert_union ; apply hstar_intro=>// - sby apply disjoint_insert_l } - { move=> * ; apply eval.eval_free=>// - srw remove_disjoint_union_l ; apply hstar_intro=>// - sby apply disjoint_remove_l } - { move=> >? ih * ; apply eval.eval_alloc=>// - move=> > /ih h /h hQ1 /[dup] /Finmap.disjoint_union_left [] /hQ1 * - srw qstarE -Finmap.union_assoc - apply hstar_intro=>// - srw Finmap.disjoint_union_left at * - sby srw Finmap.Disjoint.symm_iff } + { move=> > ? > * + apply evalExact_frame_get=> // + sby apply evalExact.get } + { move=> > [] ? > * * ; + apply evalExact_frame_set=> // + sby apply evalExact.set } + -- { move=> * ; apply eval.eval_free=>// + -- srw remove_disjoint_union_l ; apply hstar_intro=>// + -- sby apply disjoint_remove_l } + { move=> > ??? ih1 ih2 > /ih1 {ih1} ? + apply evalExact.alloc_arg=> // > + sby move=> ![>] } + { unfold tohProp=> > ?? ih > ? ; apply evalExact.alloc=> // > + move=> /ih /[apply] {}ih /Finmap.disjoint_union_left [] /[dup] /ih {}ih ? + srw Finmap.Disjoint.symm_iff -Finmap.union_assoc=> ? + have eqn:((sb ∪ sa).Disjoint h2) := by + sby srw Finmap.disjoint_union_left + apply ih in eqn=> {ih} hq ; apply evalExact_post_eq ; rotate_left ; apply hq + apply funext=> v ; apply funext=> h ; apply propext=> ⟨|⟩ + { move=> ![>] /= ? -> ? -> + exists (w \ sb), h2=> /== ⟨|⟩ // ⟨|⟩ + { sby apply disjoint_disjoint_diff } + apply union_diff_disjoint_r + sby apply Finmap.Disjoint.symm } + move=> ![>] /= ? -> ? /[dup] heq + have eqn:((w ∪ h2).Disjoint sb) := by + { srw -heq ; unfold Finmap.Disjoint=> /== } + move: eqn=> /Finmap.disjoint_union_left [ ? _] + move=> /(union_monotone_r (intersect h sb)) + srw diff_insert_intersect_id Finmap.union_assoc [2]Finmap.union_comm_of_disjoint + rotate_left + { apply Finmap.Disjoint.symm ; sby apply disjoint_intersect_r } + srw -Finmap.union_assoc=> ? + exists (w ∪ intersect h sb), h2=> //== ⟨|⟩ + { sby srw intersect_disjoint_cancel } + constructor=> // + srw Finmap.disjoint_union_left ; constructor=> // + sby apply disjoint_intersect_r } { move=> // } move=> > ?? ih₁ ih₂ ??; econstructor { apply ih₁=> // } sby move=> > ![] +lemma eval_frame (h1 h2 : state) t (Q : val -> hProp) : + eval h1 t (ofhProp Q) → + Finmap.Disjoint h1 h2 → + eval (h1 ∪ h2) t (Q ∗ (tohProp (fun h ↦ h = h2))) := +by + unfold ofhProp tohProp + move=> /[dup] hev /eval_imp_exact [Q'] /[dup] hex /evalExact_frame /[apply] + move=> /exact_imp_eval /eval_conseq ; sapply=> ? + srw ?qstarE + apply himpl_frame_l + apply evalExact_post + sby apply hev + +-- previous free proof + + -- { move=> > ; unfold tohProp + -- move=> > ?? hin hfree ih1 ih2 > /ih1 {}ih1 + -- apply eval.eval_ref + -- { apply ih1 } + -- { move=> > ![>] hQ₁ * + -- subst s₂ + -- have eqn:(p ∉ w) := by sdone + -- have eqn':((w.insert p v).Disjoint w_1) := by sby apply disjoint_update_not_r + -- move: hQ₁ eqn eqn'=> /ih2 /[apply] /[apply] + -- sby srw insert_union } + -- { sby move=> > ![>] /hin } + -- move=> > ![>] /[dup] /hin ? /hfree hQ_1 /= [] ? [] + -- exists (w.erase p), h2=> /== ⟨|⟩ // ⟨|⟩ + -- apply erase_disjoint=> // + -- sby apply remove_disjoint_union_l } + end evalProp @@ -337,6 +817,30 @@ by move=> ? sby apply triple_hpure +-- WIP +/- wp (trm_ref x (val_int n) t) Q = + (p ~~> n) -* wp (subst x t) (Q * ∃ʰ n, (p ~~> n)) -/ +lemma triple_ref (v : val) : + (forall (p : loc), triple (subst x p t2) (H ∗ (p ~~> v)) (Q ∗ ∃ʰ v, p ~~> v)) → + triple (trm_ref x (trm_val v) t2) H Q := +by + move=> htriple h ? + apply eval.eval_ref + { sby apply (eval.eval_val h v (fun v' h' ↦ v' = v ∧ h' = h)) } + move=> > [->->] > ? + move: (htriple p)=> /triple_conseq {}htriple + have eqn:(triple (subst x p t2) (H ∗ p ~~> v) fun v s ↦ Q v (s.erase p)) := by + apply htriple=> // + move=> > h /= ![>] ? /hexists_inv [v'] /hsingl_inv -> + sby move=> /union_singleton_eq_erase /[apply] <- + move=> {htriple} + apply eqn + exists h, Finmap.singleton p v + move=> ⟨//|⟩ ⟨|⟩ + apply hsingle_intro=> ⟨|⟩ + apply disjoint_single=>// + sby apply insert_eq_union_single=> // + lemma triple_if (b : Bool) t1 t2 H Q : triple (if b then t1 else t2) H Q → triple (trm_if b t1 t2) H Q := @@ -383,16 +887,6 @@ lemma read_state_single p v : by srw read_state Finmap.lookup_singleton_eq -lemma triple_ref (v : val) : - triple (trm_app val_ref v) - emp - (fun r ↦ ∃ʰ p, ⌜r = val_loc p⌝ ∗ (p ~~> v)) := -by - move=> ? [] - apply eval.eval_ref=>// p ? - apply (hexists_intro _ p) - sby srw hstar_hpure_l - lemma triple_get v (p : loc) : triple (trm_app val_get p) (p ~~> v) @@ -412,26 +906,26 @@ by apply eval.eval_set=>// sby srw Finmap.insert_singleton_eq hstar_hpure_l -lemma triple_free' p v : - triple (trm_app val_free (val_loc p)) - (p ~~> v) - (fun r ↦ ⌜r = val_unit⌝) := -by - move=> ? [] - apply eval.eval_free=>// - srw hpure hexists hempty - exists rfl - apply Finmap.ext_lookup => ? - sby srw Finmap.lookup_empty Finmap.lookup_eq_none Finmap.mem_erase - -lemma triple_free p v: - triple (trm_app val_free (val_loc p)) - (p ~~> v) - (fun _ ↦ emp) := -by - apply (triple_conseq _ _ _ _ _ (triple_free' p v)) - { sdone } - xsimp ; xsimp +-- lemma triple_free' p v : +-- triple (trm_app val_free (val_loc p)) +-- (p ~~> v) +-- (fun r ↦ ⌜r = val_unit⌝) := +-- by +-- move=> ? [] +-- apply eval.eval_free=>// +-- srw hpure hexists hempty +-- exists rfl +-- apply Finmap.ext_lookup => ? +-- sby srw Finmap.lookup_empty Finmap.lookup_eq_none Finmap.mem_erase + +-- lemma triple_free p v: +-- triple (trm_app val_free (val_loc p)) +-- (p ~~> v) +-- (fun _ ↦ emp) := +-- by +-- apply (triple_conseq _ _ _ _ _ (triple_free' p v)) +-- { sdone } +-- xsimp ; xsimp /- Rules for Other Primitive Operations -/ @@ -642,11 +1136,194 @@ by apply triple_conseq _ _ _ _ _ (triple_ptr_add p f _)=>// ? /= sby xsimp +/- ============== Definitions for Arrays ============== -/ + +def hheader (n : Int) (p : loc) : hProp := + p ~~> (val_int n) + +lemma hheader_eq p n : + (hheader n p) = (p ~~> (val_int n)) := by + sdone + +def hcell (v : val) (p : loc) (i : Int) : hProp := + ((p + 1 + (Int.natAbs i)) ~~> v) ∗ ⌜i >= 0⌝ + +lemma hcell_eq v p i : + (hcell v p i) = ((p + 1 + (Int.natAbs i)) ~~> v) ∗ ⌜i >= 0⌝ := by + sdone + +lemma hcell_nonneg v p i : + hcell v p i ==> hcell v p i ∗ ⌜i >= 0⌝ := by + sby srw hcell_eq ; xsimp + +def hseg (L : List val) (p : loc) (j : Int) : hProp := + match L with + | [] => emp + | x :: L' => (hcell x p j) ∗ (hseg L' p (j + 1)) + +def harray (L : List val) (p : loc) : hProp := + hheader (L.length) p ∗ hseg L p 0 + +lemma harray_eq p L : + harray L p = ∃ʰ n, ⌜n = L.length⌝ ∗ hheader n p ∗ hseg L p 0 := by + sby srw harray ; sorry + +/- inversion lemma for hseg -/ + +lemma hseg_start_eq L p j1 j2 : + j1 = j2 → + hseg L p j1 ==> hseg L p j2 := by + sdone + + +/- ================== Implementation of Arrays ================= -/ + +/- A simplified specification for non-negative pointer addition -/ + +lemma natabs_nonneg (p : Nat) (n : Int) : + n ≥ 0 → (p + n).natAbs = p + n.natAbs := by + omega + +lemma triple_ptr_add_nonneg (p : loc) (n : Int) : + n >= 0 → + triple [lang| p ++ n] + emp + (fun r ↦ ⌜r = val_loc (p + Int.natAbs n)⌝) := by + move=> ? + apply (triple_conseq _ emp + (fun r ↦ ⌜r = val_loc (Int.toNat (Int.natAbs (p + n)))⌝)) + apply triple_ptr_add + { omega } + { xsimp } + xsimp ; xsimp=> /== + sby apply natabs_nonneg + + +/- Semantics of Low-Level Block Allocation -/ + +#check eval.eval_alloc +/- eval.eval_alloc {x : var} {t2 : trm} (sa : state) (n : ℤ) (Q : val → state → Prop) : + n ≥ 0 → + (∀ (p : loc) (sb : state), + sb = conseq (make_list n.natAbs val_uninit) p → + p ≠ null → + Finmap.Disjoint sa sb → eval (sb ∪ sa) + (subst x p t2) fun v s ↦ Q v (s \ sb)) → + eval sa (trm_alloc x ([lang| n]) t2) Q + -/ + +/- Heap predicate for describing a range of cells -/ + +def hrange (L : List val) (p : loc) : hProp := + match L with + | [] => emp + | x :: L' => (p ~~> x) ∗ (hrange L' (p + 1)) + +lemma hrange_intro L p : + (hrange L p) (conseq L p) := by + induction L generalizing p ; srw conseq hrange=> // + apply hstar_intro=>// + sby apply disjoint_single_conseq + +lemma triple_alloc_arg : + ¬trm_is_val t1 → + triple t1 H Q1 → + (∀ v, triple (trm_alloc x (trm_val v) t2) (Q1 v) Q ) → + triple (trm_alloc x t1 t2) H Q := by + unfold triple=> ? hs ? > /hs ? + sby apply eval.eval_alloc_arg + +#check triple_ref + +lemma int_eq_sub (l m n : ℤ) : + l + m = n → l = n - m := by omega + +lemma list_inc_natabs {α : Type} (L : List α) : + ((L.length : ℤ) + 1).natAbs = (L.length : ℤ).natAbs + 1 := by + omega + +lemma hrange_eq_conseq (L : List val) (n : ℤ) (p : loc) (s : state) : + L.length = n → + hrange L p s → + s.keys = (conseq (make_list n.natAbs val_uninit) p).keys := by + elim: L n p s=> > ; unfold hrange + { sby move=> /= <- /= /hempty_inv -> } + move=> ih > /== /[dup] /int_eq_sub /[dup] hn /ih {}ih <- + srw -hn at ih + move: ih=> /= ih {hn} + unfold hrange=> ![>] /hsingl_inv ? /ih {}ih ? -> + unfold conseq make_list + srw list_inc_natabs=> /== > + move: ih + sby srw ?Finset.ext_iff Finmap.mem_keys=> ? + +lemma triple_alloc (n : Int) : + n ≥ 0 → + (∀ (p : loc), triple (subst x p t) + (H ∗ ⌜p ≠ null⌝ ∗ hrange (make_list n.natAbs val_uninit) p) + (Q ∗ ⌜p ≠ null⌝ ∗ ∃ʰ L, ⌜L.length = n⌝ ∗ hrange L p) ) → + triple (trm_alloc x n t) H Q := by + move=> ? htriple h ? + apply eval.eval_alloc=> // > * + move: (htriple p)=> /triple_conseq {}htriple + specialize (htriple (H ∗ ⌜p ≠ null⌝ ∗ hrange (make_list n.natAbs val_uninit) p)) + specialize (htriple (fun v s ↦ Q v (s \ sb))) + have eqn:(triple (subst x p t) + (H ∗ ⌜p ≠ null⌝ ∗ hrange (make_list n.natAbs val_uninit) p) + fun v s ↦ Q v (s \ sb)) := by + { apply htriple=> // {htriple} + move=> > s ![>] ? ![>] /hpure_inv [] _ -> + move=> /hexists_inv [L] ![>] /hpure_inv [] ? -> ? _ + move=> /== -> _ -> ? -> + srw diff_disjoint_eq=> // + subst sb ; sby apply hrange_eq_conseq } + move=> {htriple} + apply eqn + exists h, sb=> ⟨//|⟩ ⟨|⟩ + { exists ∅, sb => ⟨//|/==⟩ ⟨|⟩ + subst sb ; apply hrange_intro + sdone } + constructor=> // + sby srw Finmap.union_comm_of_disjoint Finmap.Disjoint.symm_iff + + /- --------------------- Strongest Post Condition --------------------- -/ abbrev sP h t :=fun v => h∀ (Q : val -> hProp), ⌜eval h t Q⌝ -∗ Q v open Classical + +open Classical + +noncomputable def sP' (h : heap) (t : trm) : (val → hProp) := + if ex : ∃ Q, evalExact h t Q then choose ex else fun _ _ ↦ False + +lemma sP'_strongest : + eval h t Q → sP' h t ===> Q := by + move=> /evalExact_post hex + unfold sP' + scase: [∃ Q, evalExact h t Q] + { move=> > ; sby srw dif_neg=> // ?? } + move=> > ; srw (dif_pos h_1)=> // + sby apply choose_spec in h_1=> /hex + +lemma evalExact_sP' : + evalExact h t Q → evalExact h t (sP' h t) := by + move=> ? + have hex:(∃ Q, evalExact h t Q) := by exists Q + unfold sP' + scase: [∃ Q, evalExact h t Q]=> // > + srw (dif_pos hex) + apply choose_spec + +lemma sP'_post : + eval h t Q → eval h t (sP' h t) := by + sby move=> /eval_imp_exact=> [>] /evalExact_sP' /exact_imp_eval + +lemma sP'_post_exact : + eval h t Q → evalExact h t (sP' h t) := by + sby move=> /eval_imp_exact [>] /evalExact_sP' + lemma hpure_intr : (P -> H s) -> (⌜P⌝ -∗ H) s := by move=> ? @@ -737,17 +1414,21 @@ lemma sP_post : move=> eop'; sapply; scase: eop any_goals (try scase: eop'=> //) any_goals (try move=> ?? [] //) - move=> /= ???->? []// } - { move=> ->?; apply eval.eval_ref=> // ??? - apply hpure_intr=> []// } + move=> ???->? []// } + { sorry + -- move=> ->?; apply eval.eval_ref=> // ??? + -- apply hpure_intr=> []// + } { move=> ??; apply eval.eval_get=> // ? apply hpure_intr=> []// } { move=> ->??; apply eval.eval_set=> // ? apply hpure_intr=> []// ?? []// } - { move=> ??; apply eval.eval_free=> // ? - apply hpure_intr=> []// } - { move=> ??; apply eval.eval_alloc=> // *? - apply hpure_intr=> []// } + -- { move=> ??; apply eval.eval_free=> // ? + -- apply hpure_intr=> []// } + -- { move=> ??; apply eval.eval_alloc=> // *? + -- apply hpure_intr=> []// } + { sorry } + { sorry } { move=> ev₁ ev₂; constructor apply eval_conseq=> // v dsimp [sP]; apply himpl_hforall=> Q/= @@ -759,30 +1440,4 @@ lemma sP_post : move=> v; dsimp [sP]; apply himpl_hforall=> Q/= xsimp=> ev; srw hwand_hpure_l=> // scase: ev=> // ? ev; sapply - apply sP_strongest; apply ev=> // - - - -lemma finite_state (s : state) : - ∃ p, p ∉ s := by sorry - -lemma finite_state' n (s : state) : - ∃ p, p ≠ null ∧ - Finmap.Disjoint s (conseq (make_list n val_uninit) p) := by sorry - -lemma eval_sat : - eval h t Q -> ∃ h v, Q h v := by - elim=> // > - { move=> ??? ![>?]; sapply=> // } - { move=> ??? ![>?]; sapply=> // } - { move=> ?? ![>?]; sapply=> // } - { move=> ?? ![>?]; sapply=> // } - { scase=> > - any_goals move=> pp; (sdo 2 econstructor); apply pp=> // - move=> ? pp; sdo 2 econstructor; apply pp=> //} - { scase=> > - any_goals move=> pp; (sdo 2 econstructor); apply pp=> // - any_goals move=> ? pp; (sdo 2 econstructor); apply pp=> // } - { move=> ?; scase: (finite_state s)=> p /[swap]/[apply]// } - { sby move=> ?; scase: (finite_state' n.natAbs sa)=> p ? /(_ p) H } - move=> ? /[swap]![>] /[swap] _ /[swap]/[apply]// + apply sP_strongest; sby apply ev diff --git a/Lgtm/Unary/WP1.lean b/Lgtm/Unary/WP1.lean index 66f7397..7483955 100644 --- a/Lgtm/Unary/WP1.lean +++ b/Lgtm/Unary/WP1.lean @@ -3,6 +3,8 @@ import Lean -- import Ssreflect.Lang import Mathlib.Data.Finmap +import Lgtm.Common.State + import Lgtm.Unary.Util import Lgtm.Unary.HProp import Lgtm.Unary.XSimp @@ -142,6 +144,76 @@ by { sby scase_if=> ?? } apply wp_if +lemma wp_ref x v t Q : + (h∀ p, (p ~~> v) -∗ wp (subst x p t) (Q ∗ ∃ʰ v', (p ~~> v'))) ==> + wp (trm_ref x v t) Q := +by + move=> > /hforall_inv hwp + apply (eval.eval_ref _ _ _ _ _ (fun v' s' ↦ v' = v ∧ s' = h))=> //== > ? + apply (eval_conseq _ _ (Q ∗ ∃ʰ v', p ~~> v' )) + { move: (hwp p)=> {hwp} /(hwand_inv (Finmap.singleton p v)) + srw union_singleton_eq_insert=> wp + apply wp=> // + sby unfold Finmap.Disjoint=> > /== -> } + move=> > s ![>] ? [v'] /= /hsingl_inv -> hdis -> + srw Finmap.union_comm_of_disjoint=> // + srw union_singleton_eq_insert -insert_delete_id=> // + move: hdis=> /Finmap.Disjoint.symm + sby unfold Finmap.Disjoint + +lemma wp_ref_trm x t1 t2 Q : + wp t1 (fun v ↦ h∀ p, (p ~~> v) -∗ wp (subst x p t2) (Q ∗ ∃ʰ v', (p ~~> v'))) ==> + wp (trm_ref x t1 t2) Q := +by + move=> > hwp + apply eval.eval_ref + { apply hwp } + move=> > /hforall_inv {}hwp > ? + move: (hwp p)=> /(hwand_inv (Finmap.singleton p v1)) {}hwp + srw -union_singleton_eq_insert + apply (eval_conseq _ _ (Q ∗ ∃ʰ v', p ~~> v' )) + { apply hwp=> // + sby unfold Finmap.Disjoint } + move=> > s ![>] ? [v'] /= /hsingl_inv -> hdis -> + srw Finmap.union_comm_of_disjoint=> // + srw union_singleton_eq_insert -insert_delete_id=> // + move: hdis=> /Finmap.Disjoint.symm + sby unfold Finmap.Disjoint + +lemma mem_conseq : + x ∈ conseq L p → p ≤ x := by + elim: L p=> > // + move=> ih > + unfold conseq=> /== [] // /ih + omega + +lemma hrange_of_conseq : + (hrange L p) (conseq L p) := by + elim: L p=> > // + move=> ? > + unfold hrange conseq + exists (Finmap.singleton p head), conseq tail (p + 1)=> ⟨//|⟩ ⟨//|⟩ ⟨|//⟩ + unfold Finmap.Disjoint=> > /== -> /mem_conseq + omega + +lemma wp_alloc x (n : ℤ) t Q : + n ≥ 0 → + (h∀ p, (hrange (make_list n.natAbs val_uninit) p) -∗ + wp (subst x p t) (Q ∗ ⌜p ≠ null⌝ ∗ ∃ʰ L, ⌜L.length = n⌝ ∗ hrange L p)) ==> + wp (trm_alloc x n t) Q := +by + move=> ? h /hforall_inv hwp + apply eval.eval_alloc=> // > * + apply (eval_conseq _ _ (Q ∗ ⌜p ≠ null⌝ ∗ ∃ʰ L, ⌜↑L.length = n⌝ ∗ hrange L p)) + { move: (hwp p)=> /(hwand_inv sb) + srw Finmap.Disjoint.symm_iff=> {}hwp + apply hwp=> // ; subst sb + apply hrange_of_conseq } + move=> > s ![>] ? ![>] /hpure_inv [_ ->] /== + move=> /hexists_inv [L] ![>] /hpure_inv [? ->] /== ? _ -> _ -> ? -> + srw diff_disjoint_eq=> // ; subst sb + sby apply hrange_eq_conseq + /- ======================= WP Generator ======================= -/ /- Below we define a function [wpgen t] recursively over [t] such that @@ -442,6 +514,18 @@ def wpgen_while (F1 F2 : formula) : formula := mkstruct fun Q => let F := wpgen_if_trm F1 (wpgen_seq F2 R) (wpgen_val val_unit) ⌜structural R ∧ F ===> R⌝ -∗ R Q +def wpgen_ref (x : var) (t1 t2 : trm) : formula := + fun Q ↦ ∃ʰ v, ⌜t1 = trm_val v⌝ ∗ + h∀ p, (p ~~> v) -∗ protect (wp (subst x p t2) (fun hv ↦ Q hv ∗ ∃ʰ u, p ~~> u)) + +def wpgen_alloc (x : var) (t1 t2 : trm) : formula := + fun Q ↦ ∃ʰ n : ℤ, + ⌜n ≥ 0 ∧ t1 = trm_val n⌝ ∗ + h∀ p, + (hrange (make_list n.natAbs val_uninit) p) -∗ + protect wp (subst x p t2) (Q ∗ ⌜p ≠ null⌝ ∗ ∃ʰ L, ⌜L.length = n⌝ ∗ hrange L p) + + /- Recursive Definition of [wpgen] -/ def wpgen (t : trm) : formula := @@ -456,6 +540,8 @@ def wpgen (t : trm) : formula := | trm_app _ _ => wpgen_app t | trm_for x v1 v2 t1 => wpgen_for v1 v2 (fun v ↦ wp $ subst x v t1) | trm_while t0 t1 => wpgen_while (wp t0) (wp t1) + | trm_ref x t1 t2 => wpgen_ref x t1 t2 + | trm_alloc x t1 t2 => wpgen_alloc x t1 t2 | _ => wp t ) @@ -486,7 +572,7 @@ lemma mkstruct_sound t F : formula_sound t F → formula_sound t (mkstruct F) := by - srw []formula_sound => ? ? + srw ?formula_sound => ? ? srw -mkstruct_wp sby apply mkstruct_monotone=> ?? @@ -510,18 +596,26 @@ lemma wpgen_fun_sound x t1 Fof : (forall vx, formula_sound (subst x vx t1) (Fof vx)) → formula_sound (trm_fun x t1) (wpgen_fun Fof) := by - move=> ? ? + srw ?formula_sound=> h > srw wpgen_fun apply (himpl_hforall_l _ (val_fun x t1)) - sorry -- xchange hwand_hpure_l + srw hwand_hpure_l=> // + apply wp_fun=> > + xchange h + sby apply wp_app_fun lemma wpgen_fix_sound f x t1 Fof : (forall vf vx, formula_sound (subst v vx (subst f vf t1)) (Fof vf vx)) → formula_sound (trm_fix f x t1) (wpgen_fix Fof) := by - move=> ? ? + srw ?formula_sound=> h > srw wpgen_fix apply (himpl_hforall_l _ (val_fix f x t1)) + srw hwand_hpure_l + { apply wp_fix } + move=> > + xchange h + apply wp_app_fix sorry -- xchange hwand_hpure_l lemma wpgen_seq_sound F1 F2 t1 t2 : @@ -529,7 +623,7 @@ lemma wpgen_seq_sound F1 F2 t1 t2 : formula_sound t2 F2 → formula_sound (trm_seq t1 t2) (wpgen_seq F1 F2) := by - srw []formula_sound => ?? Q + srw ?formula_sound => ?? Q srw wpgen_seq apply (himpl_trans (wp t1 (fun _ ↦ wp t2 Q))) { apply (himpl_trans (wp t1 fun _ ↦ F2 Q)) @@ -543,7 +637,7 @@ lemma wpgen_let_sound F1 F2of x t1 t2 : (forall v, formula_sound (subst x v t2) (F2of v)) → formula_sound (trm_let x t1 t2) (wpgen_let F1 F2of) := by - srw []formula_sound => ?? Q + srw ?formula_sound => ?? Q srw wpgen_let apply himpl_trans (wp t1 (fun v ↦ wp (subst x v t2) Q)) { apply himpl_trans (wp t1 (fun v ↦ F2of v Q )) @@ -557,7 +651,7 @@ lemma wpgen_if_sound F1 F2 t0 t1 t2 : formula_sound t2 F2 → formula_sound (trm_if t0 t1 t2) (wpgen_if t0 F1 F2) := by - srw []formula_sound => ?? Q + srw ?formula_sound => ?? Q srw wpgen_if xpull=> > apply himpl_trans (wp (trm_if b t1 t2) Q)=> // @@ -607,37 +701,53 @@ lemma wpgen_for_sound x v1 v2 F1 : { sorry } sorry +lemma wpgen_ref_sound x t1 t2 : + formula_sound (trm_ref x t1 t2) (wpgen_ref x t1 t2) := +by + srw ?formula_sound=> > + unfold wpgen_ref + xpull=> > + apply wp_ref + +lemma wpgen_alloc_sound x t1 t2 : + formula_sound (trm_alloc x t1 t2) (wpgen_alloc x t1 t2) := +by + srw formula_sound=> > + unfold wpgen_alloc + xpull=> > [? ->] + sby apply wp_alloc /- Main soundness lemma -/ lemma wpgen_sound t : formula_sound t (wpgen t) := -by sorry +by -- elim: t - -- scase: t - -- any_goals move=> * ; srw wpgen ; try apply mkstruct_sound - -- { apply wpgen_val_sound } + scase: t + any_goals move=> > * ; srw wpgen ; try apply mkstruct_sound=> /= + { apply wpgen_val_sound } + { sorry } -- { srw wpgen_var -- cases eqn:(lookup _ E)=> /= -- { apply wpgen_fail_sound } -- apply wpgen_val_sound } - -- { apply wpgen_fun_sound=> ? - -- srw -isubst_rem - -- sorry /- need induction -/ } - -- { apply wpgen_fix_sound=> * - -- srw -isubst_rem_2 - -- sorry } - -- { srw isubst - -- apply wpgen_app_sound } - -- { apply wpgen_seq_sound - -- sorry ; sorry } - -- { apply wpgen_let_sound - -- sorry - -- move=> ? - -- srw -isubst_rem - -- sorry } - -- { apply wpgen_if_sound - -- sorry ; sorry } + { apply wpgen_fun_sound=> > + sby srw formula_sound } + { apply wpgen_fix_sound=> > + rotate_left ; apply a_1 + sby srw formula_sound } + { apply wpgen_app_sound } + { apply wpgen_seq_sound + sby srw formula_sound } + { apply wpgen_let_sound + sby srw formula_sound } + { apply wpgen_if_sound + sby srw formula_sound } + { apply wpgen_for_sound + sby srw formula_sound } + { sorry } + { apply wpgen_ref_sound } + { apply wpgen_alloc_sound } lemma himpl_wpgen_wp t Q : wpgen t Q ==> wp t Q := @@ -663,6 +773,24 @@ by /- ================================================================= -/ /-* ** Lemmas for Tactics to Manipulate [wpgen] Formulae -/ +lemma xref_lemma_aux x v t2 H Q : + ( ∀ p, H ==> (p ~~> v) -∗ + protect (wp (subst x p t2) (fun hv ↦ Q hv ∗ ∃ʰ u, p ~~> u))) → + H ==> wpgen_ref x (trm_val v) t2 Q := +by + move=> h s /h + srw wpgen_ref=> /hforall_inv {}h + exists v=> /== + sby srw hstar_hpure_l + +lemma xref_lemma x v t2 H Q : + ( ∀ p, H ∗ (p ~~> v) ==> + (wp (subst x p t2) (fun hv ↦ Q hv ∗ ∃ʰ u, p ~~> u))) → + H ==> wpgen_ref x (trm_val v) t2 Q := +by + move=> M ; apply xref_lemma_aux=> > + xsimp ; sby xchange M + lemma xstruct_lemma F H Q : H ==> F Q → H ==> mkstruct F Q := by @@ -815,6 +943,12 @@ macro "xif" : tactic => do `(tactic| (xseq_xlet_if_needed; xstruct_if_needed; apply xif_lemma)) +macro "xref" p:term : tactic => do + `(tactic| + (xseq_xlet_if_needed ; xstruct_if_needed ; apply xref_lemma ; + intro $p:term ; try (simp [$(mkIdent `subst):ident]) + try (simp [$(mkIdent `_root_.subst):ident]))) + set_option linter.unreachableTactic false in set_option linter.unusedTactic false in elab "xapp_try_clear_unit_result" : tactic => do @@ -993,6 +1127,10 @@ def isubst (E : ctx) (t : trm) : trm := trm_seq (isubst E t1) (isubst E t2) | trm_let x t1 t2 => trm_let x (isubst E t1) (isubst (erase x E) t2) + | trm_ref x t1 t2 => + trm_ref x (isubst E t1) (isubst (erase x E) t2) + | trm_alloc x t1 t2 => + trm_alloc x (isubst E t1) (isubst (erase x E) t2) | trm_app t1 t2 => trm_app (isubst E t1) (isubst E t2) | trm_for x n1 n2 t => @@ -1117,8 +1255,8 @@ lemma wp_structural : structural (wp t) := by #hint_xapp triple_get #hint_xapp triple_set #hint_xapp triple_add -#hint_xapp triple_ref -#hint_xapp triple_free +-- #hint_xapp triple_ref +-- #hint_xapp triple_free elab "xseq_xlet_if_needed_xwp" : tactic => do diff --git a/Lgtm/Unary/XSimp.lean b/Lgtm/Unary/XSimp.lean index 706bf54..de2e0a4 100644 --- a/Lgtm/Unary/XSimp.lean +++ b/Lgtm/Unary/XSimp.lean @@ -754,7 +754,9 @@ def eApplyAndName (lem : Name) (mvarName : Name) : TacticM Unit := withMainConte def xsimp_r_hexists_apply_hints (x : Ident) : TacticM Unit := do let hints <- hintExt.getSSR match hints with - | [] => eApplyAndName `xsimp_r_hexists $ `xsimp ++ x.getId + | [] => + trace[xsimp] "no hints" + eApplyAndName `xsimp_r_hexists $ `xsimp ++ x.getId | h :: hs => hintExt.setSSR hs match h with @@ -862,6 +864,21 @@ elab "xsimp_step" : tactic => do xsimp_step_r xsimp <|> xsimp_step_lr xsimp +elab "xsimp_step_l_tac" : tactic => do + let xsimp <- XSimpRIni + withMainContext do + xsimp_step_l xsimp + +elab "xsimp_step_r_tac" : tactic => do + let xsimp <- XSimpRIni + withMainContext do + xsimp_step_r xsimp + +elab "xsimp_step_lr_tac" : tactic => do + let xsimp <- XSimpRIni + withMainContext do + xsimp_step_lr xsimp + elab "rev_pure" : tactic => do {| try subst_vars |} for n in <- revExt.getSSR do