Commit f1564b05 by Ike Mulder

### Notation fixes for 8.15.

parent 7b400617
 ... ... @@ -61,7 +61,7 @@ Section proof. Definition is_list (v : val) : iProp Σ := ∃ (l : loc) (lk : val) γ, ⌜v = (#l, lk)%V⌝ ∗ is_lock γ lk (∃ z v, l ↦ v ∗ is_node z v). Global Instance none_is_node z : HINT empty_hyp_first ✱ [emp] ⊫ [id]; is_node z NONEV ✱ [emp]. HINT empty_hyp_first ✱ [- ; emp] ⊫ [id]; is_node z NONEV ✱ [emp]. Proof. iStepS. rewrite is_node_unfold. iSmash. Qed. Global Instance some_is_node z (l : loc) lk : ... ...
 ... ... @@ -80,7 +80,7 @@ Section node. Global Instance allocate_any_loc l : (* ideally the sidecondition would be a forall. but that is not sound: we must be able to know l now *) HINT empty_hyp_last ✱ [emp] ⊫ [bupd] γ; own γ None ✱ [own γ \$ Excl' l]. HINT empty_hyp_last ✱ [- ; emp] ⊫ [bupd] γ; own γ None ✱ [own γ \$ Excl' l]. Proof. iStepS. iAssert (|==> ∃ γ, own γ (Excl' l))%I as ">[%γ Hγ]"; iStepsS. Qed. End node. ... ...
 ... ... @@ -154,7 +154,7 @@ Section biabd_instances. Qed. Global Instance as_persistent_mapsto p l q v : HINT □⟨p⟩ l ↦{q} v ✱ [emp] ⊫ [bupd]; l ↦□v ✱ [l ↦□ v] | 100. HINT □⟨p⟩ l ↦{q} v ✱ [- ; emp] ⊫ [bupd]; l ↦□v ✱ [l ↦□ v] | 100. Proof. iStepS. rewrite bi.intuitionistically_if_elim. iMod (mapsto_persist with "H1") as "#Hl". ... ...
 ... ... @@ -86,7 +86,7 @@ Section instances. Global Instance mapsto_val_have_enough (l : loc) (v1 v2 : val) (q1 q2 : Qp) mq : FracSub q1 q2 mq → HINT l ↦{#q1} v1 ✱ [⌜v1 = v2⌝] ⊫ [id]; l ↦{#q2}v2 ✱ [⌜v1 = v2⌝ ∗ match mq with | Some q => l ↦{#q} v1 | _ => True end] | 54. HINT l ↦{#q1} v1 ✱ [- ; ⌜v1 = v2⌝] ⊫ [id]; l ↦{#q2}v2 ✱ [⌜v1 = v2⌝ ∗ match mq with | Some q => l ↦{#q} v1 | _ => True end] | 54. Proof. rewrite /= /FracSub => <-. destruct mq; iStepsS. ... ... @@ -109,7 +109,7 @@ Section instances. Qed. Global Instance as_persistent_mapsto p l q v : HINT □⟨p⟩ l ↦{q} v ✱ [emp] ⊫ [bupd]; l ↦□ v ✱ [l ↦□ v] | 100. HINT □⟨p⟩ l ↦{q} v ✱ [- ; emp] ⊫ [bupd]; l ↦□ v ✱ [l ↦□ v] | 100. Proof. iIntros "Hl" => /=. rewrite /= right_id bi.intuitionistically_if_elim. ... ... @@ -121,7 +121,7 @@ Section instances. Global Instance array_mapsto_head l v vs q l' : OffsetLoc l 1 l' → (* this makes us get (l +ₗ (1 + 1)) instead of ((l +ₗ 1) +ₗ 1) *) HINT l ↦∗{q} vs ✱ [⌜hd_error vs = Some v⌝] ⊫ [id]; l ↦{q} v ✱ [l' ↦∗{q} tail vs ∗ ⌜hd_error vs = Some v⌝] | 20. HINT l ↦∗{q} vs ✱ [- ; ⌜hd_error vs = Some v⌝] ⊫ [id]; l ↦{q} v ✱ [l' ↦∗{q} tail vs ∗ ⌜hd_error vs = Some v⌝] | 20. Proof. rewrite /= /OffsetLoc => ->. iIntros "[H %] /=". ... ... @@ -132,7 +132,7 @@ Section instances. Global Instance head_mapsto_array l v vs q l' : OffsetLoc l 1 l' → HINT l ↦{q} v ✱ [⌜hd_error vs = Some v⌝ ∗ l' ↦∗{q} tail vs] ⊫ [id]; l ↦∗{q} vs ✱ [emp] | 20. HINT l ↦{q} v ✱ [- ; ⌜hd_error vs = Some v⌝ ∗ l' ↦∗{q} tail vs] ⊫ [id]; l ↦∗{q} vs ✱ [emp] | 20. Proof. rewrite /= => ->. iIntros "(H & % & Htl) /=". ... ... @@ -145,7 +145,7 @@ Section instances. Global Instance array_mapsto_head_offset l v vs q i l': SolveSepSideCondition (0 ≤ i < length vs)%Z → (* that this is_Some is given, but that it is equal to v is a proof obligation *) OffsetLoc l (Z.succ i) l' → HINT l ↦∗{q} vs ✱ [⌜vs !! Z.to_nat i = Some v⌝] ⊫ [id]; (l +ₗ i) ↦{q} v ✱ [ HINT l ↦∗{q} vs ✱ [ - ; ⌜vs !! Z.to_nat i = Some v⌝] ⊫ [id]; (l +ₗ i) ↦{q} v ✱ [ (l ↦∗{q} take (Z.to_nat i) vs) ∗ ⌜vs !! Z.to_nat i = Some v⌝ ∗ (l' ↦∗{q} drop (S \$ Z.to_nat i) vs)] | 20. Proof. rewrite /SolveSepSideCondition /= => Hi ->. ... ... @@ -162,7 +162,7 @@ Section instances. Global Instance array_from_shorter vs1 vs2 l l' q : SolveSepSideCondition (length vs1 ≤ length vs2) → OffsetLoc l (length vs1) l' → HINT l ↦∗{q} vs1 ✱ [⌜take (length vs1) vs2 = vs1⌝ ∗ l' ↦∗{q} (list.drop (length vs1) vs2) ] ⊫ [id]; HINT l ↦∗{q} vs1 ✱ [- ; ⌜take (length vs1) vs2 = vs1⌝ ∗ l' ↦∗{q} (list.drop (length vs1) vs2) ] ⊫ [id]; l ↦∗{q} vs2 ✱ [emp] | 51. Proof. rewrite /SolveSepSideCondition => Hl -> /=. ... ... @@ -172,7 +172,7 @@ Section instances. Qed. Global Instance empty_array_solve l q : HINT empty_hyp_last ✱ [emp] ⊫ [id]; l ↦∗{q} [] ✱ [emp]. HINT empty_hyp_last ✱ [- ; emp] ⊫ [id]; l ↦∗{q} [] ✱ [emp]. Proof. iStepsS. rewrite array_nil. iStepsS. Qed. ... ...
 ... ... @@ -18,7 +18,7 @@ Section biabd_instances. Global Instance bi_abd_from_assumption p P P' : (* this requirement will remember newly proven persistent things *) TCIf (TCAnd (TCEq p false) \$ Persistent P) (TCEq P' P) (TCEq P' emp%I) → HINT □⟨p⟩ P ✱ [emp] ⊫ [id]; P ✱ [P'] | 50. HINT □⟨p⟩ P ✱ [- ; emp] ⊫ [id]; P ✱ [P'] | 50. Proof. rewrite /BiAbd /= !right_id //. case => [[-> HP] -> /= | ->]. ... ... @@ -28,11 +28,11 @@ Section biabd_instances. Qed. Global Instance bi_abd_from_assumption_intuit P : HINT □⟨true⟩ P ✱ [emp] ⊫ [id]; □ P ✱ [emp]. HINT □⟨true⟩ P ✱ [- ; emp] ⊫ [id]; □ P ✱ [emp]. Proof. by rewrite /BiAbd /= !right_id. Qed. Global Instance bi_abd_empty_goal_from_emp p : HINT □⟨p⟩ emp ✱ [emp] ⊫ [@id PROP]; empty_goal ✱ [emp] | 50. HINT □⟨p⟩ emp ✱ [- ; emp] ⊫ [@id PROP]; empty_goal ✱ [emp] | 50. Proof. by rewrite /BiAbd /= empty_goal_eq bi.intuitionistically_if_elim. Qed. ... ...
 ... ... @@ -104,7 +104,7 @@ Section automation. Global Instance biabd_create_token γ p1 p2 : SolveSepSideCondition (p2 = Pos.succ p1) → HINT token_counter P γ p1 ✱ [emp] ⊫ [bupd]; token_counter P γ p2 ✱ [token P γ]. HINT token_counter P γ p1 ✱ [- ; emp] ⊫ [bupd]; token_counter P γ p2 ✱ [token P γ]. Proof. apply: tokenizable.biabd_create_token. Qed. Global Instance biabd_create_first_token γ p : ... ... @@ -131,7 +131,7 @@ Section automation. Global Instance no_tokens_split γ q1 q2 mq : FracSub q1 q2 mq → HINT no_tokens P γ q1 ✱ [True] ⊫ [id]; no_tokens P γ q2 ✱ [match mq with | Some q => no_tokens P γ q | None => True end]. HINT no_tokens P γ q1 ✱ [- ; True] ⊫ [id]; no_tokens P γ q2 ✱ [match mq with | Some q => no_tokens P γ q | None => True end]. Proof. apply: tokenizable.no_tokens_split. Qed. Fixpoint token_iter n γ : iProp Σ := ... ...
 ... ... @@ -83,7 +83,7 @@ Section laterable_hyp. Global Instance laterable_into_parts' (L : PROP) : Laterable L → HINT L ✱ [emp] ⊫ [id] P; later_later_part_of L P ✱ [pers_part_of L P]. HINT L ✱ [- ; emp] ⊫ [id] P; later_later_part_of L P ✱ [pers_part_of L P]. Proof. rewrite /Laterable => HL. iStepS. rewrite {1}HL. rewrite later_later_part_of_eq /later_later_part_of_def later_part_of_eq pers_part_of_eq /pers_part_of_def /=. ... ... @@ -126,11 +126,11 @@ Section laterable_hyp. Proof. rewrite /IntoWand /= later_part_of_eq pers_part_of_eq; iStepsS. Qed. Global Instance later_later_from_later_later (L P : PROP) : HINT ▷ later_part_of L P ✱ [emp] ⊫ [id]; later_later_part_of L P ✱ [emp]. HINT ▷ later_part_of L P ✱ [- ; emp] ⊫ [id]; later_later_part_of L P ✱ [emp]. Proof. rewrite /BiAbd /= later_later_part_of_eq //. Qed. Global Instance later_later_from_now_later (L P : PROP) : HINT later_part_of L P ✱ [emp] ⊫ [id]; later_later_part_of L P ✱ [emp]. HINT later_part_of L P ✱ [- ; emp] ⊫ [id]; later_later_part_of L P ✱ [emp]. Proof. rewrite /BiAbd /= later_later_part_of_eq /later_later_part_of_def. iIntros "[HP _]". by iFrame. Qed. End laterable_hyp. \ No newline at end of file
 ... ... @@ -113,7 +113,7 @@ Section loc_map. Qed. Global Instance biabd_ex_falso {PROP : bi} p (P : PROP) : HINT □⟨p⟩ False ✱ [emp] ⊫ [id]; P ✱ [False] | 52. HINT □⟨p⟩ False ✱ [- ; emp] ⊫ [id]; P ✱ [False] | 52. Proof. iStepS. rewrite bi.intuitionistically_if_elim. iReIntro "H1". Qed. ... ... @@ -198,7 +198,7 @@ Section loc_map. Global Opaque loc_map_elem global_reg. Global Instance alloc_global_reg_biabd E : HINT empty_hyp_last ✱ [emp] ⊫ [fupd E E] γ; global_reg γ ✱ [global_reg γ]. HINT empty_hyp_last ✱ [- ; emp] ⊫ [fupd E E] γ; global_reg γ ✱ [global_reg γ]. Proof. iStepS. iMod (alloc_global_reg) as "[%γ #Hγ]". ... ...
 ... ... @@ -1978,7 +1978,7 @@ Section generic_instances. Global Instance unit_abduct2 {A : ucmra} `{inG Σ A} (x : A) γ : AsCmraUnit x → HINT empty_hyp_last ✱ [emp] ⊫ [bupd]; own γ x ✱ [emp] | 150. HINT empty_hyp_last ✱ [- ; emp] ⊫ [bupd]; own γ x ✱ [emp] | 150. Proof. move => ->. iStepS. rewrite right_id. iApply own_unit. Qed. ... ...
 ... ... @@ -197,7 +197,7 @@ Section automation. Lemma biabd_create_token γ p1 p2 : SolveSepSideCondition (p2 = Pos.succ p1) → HINT token_counter tc γ p1 ✱ [emp] ⊫ [bupd]; token_counter tc γ p2 ✱ [token tc γ]. HINT token_counter tc γ p1 ✱ [- ; emp] ⊫ [bupd]; token_counter tc γ p2 ✱ [token tc γ]. Proof. move => ->; iStepS. by iApply create_token_succ. ... ... @@ -242,7 +242,7 @@ Section automation. Lemma no_tokens_split γ q1 q2 mq : FracSub q1 q2 mq → HINT no_tokens tc γ q1 ✱ [True] ⊫ [id]; HINT no_tokens tc γ q1 ✱ [- ; True] ⊫ [id]; no_tokens tc γ q2 ✱ [match mq with | Some q => no_tokens tc γ q | None => True end]. Proof. move => <-. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!