diff --git a/ProofMode.md b/ProofMode.md index 4f14da9f32956fbd64c9d3f31e9945cc5ec2b5cf..9c14046768d3a805031cf133b9ffa8e077a9ef1d 100644 --- a/ProofMode.md +++ b/ProofMode.md @@ -58,7 +58,8 @@ Introduction of logical connectives one of the operands is persistent. - `iSplitL "H1 ... Hn"` : introduction of a separating conjunction. The hypotheses `H1 ... Hn` are used for the left conjunct, and the remaining ones - for the right conjunct. + for the right conjunct. Persistent hypotheses are ignored, since these do not + need to be split. - `iSplitR "H0 ... Hn"` : symmetric version of the above. - `iExist t1, .., tn` : introduction of an existential quantifier. diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v index 408ca28444abd5f058f03e9d69416357a53681d4..e9f809ec263f82d8c59803f58f83e561fbac4ba6 100644 --- a/proofmode/coq_tactics.v +++ b/proofmode/coq_tactics.v @@ -56,6 +56,11 @@ Definition envs_lookup_delete {M} (i : string) | None => '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs') end. +Definition envs_snoc {M} (Δ : envs M) + (p : bool) (j : string) (P : uPred M) : envs M := + let (Γp,Γs) := Δ in + if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P). + Definition envs_app {M} (p : bool) (Γ : env (uPred M)) (Δ : envs M) : option (envs M) := let (Γp,Γs) := Δ in @@ -77,23 +82,29 @@ Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M)) if eqb p q then envs_simple_replace i p Γ Δ else envs_app q Γ (envs_delete i p Δ). -(* if [lr = false] then [result = (hyps named js, remaining hyps)], - if [lr = true] then [result = (remaining hyps, hyps named js)] *) -Definition envs_split {M} - (lr : bool) (js : list string) (Δ : envs M) : option (envs M * envs M) := - let (Γp,Γs) := Δ in - '(Γs1,Γs2) ← env_split js Γs; - match lr with - | false => Some (Envs Γp Γs1, Envs Γp Γs2) - | true => Some (Envs Γp Γs2, Envs Γp Γs1) - end. - Definition env_spatial_is_nil {M} (Δ : envs M) := if env_spatial Δ is Enil then true else false. Definition envs_clear_spatial {M} (Δ : envs M) : envs M := Envs (env_persistent Δ) Enil. +Fixpoint envs_split_go {M} + (js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) := + match js with + | [] => Some (Δ1, Δ2) + | j :: js => + '(p,P,Δ1') ← envs_lookup_delete j Δ1; + if p then envs_split_go js Δ1 Δ2 else + envs_split_go js Δ1' (envs_snoc Δ2 false j P) + end. +(* if [lr = true] then [result = (remaining hyps, hyps named js)] and + if [lr = false] then [result = (hyps named js, remaining hyps)] *) +Definition envs_split {M} (lr : bool) + (js : list string) (Δ : envs M) : option (envs M * envs M) := + '(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ); + if lr then Some (Δ1,Δ2) else Some (Δ2,Δ1). + + (* Coq versions of the tactics *) Section tactics. Context {M : ucmraT}. @@ -158,6 +169,35 @@ Lemma envs_lookup_delete_sound' Δ Δ' i p P : envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ P ★ Δ'. Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed. +Lemma envs_lookup_snoc Δ i p P : + envs_lookup i Δ = None → envs_lookup i (envs_snoc Δ p i P) = Some (p, P). +Proof. + rewrite /envs_lookup /envs_snoc=> ?. + destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc. +Qed. +Lemma envs_lookup_snoc_ne Δ i j p P : + i ≠ j → envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ. +Proof. + rewrite /envs_lookup /envs_snoc=> ?. + destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne. +Qed. + +Lemma envs_snoc_sound Δ p i P : + envs_lookup i Δ = None → Δ ⊢ □?p P -★ envs_snoc Δ p i P. +Proof. + rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_sep_l=> Hwf. + destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=. + apply wand_intro_l; destruct p; simpl. + - apply sep_intro_True_l; [apply pure_intro|]. + + destruct Hwf; constructor; simpl; eauto using Esnoc_wf. + intros j; case_decide; naive_solver. + + by rewrite always_and_sep always_sep assoc. + - apply sep_intro_True_l; [apply pure_intro|]. + + destruct Hwf; constructor; simpl; eauto using Esnoc_wf. + intros j; case_decide; naive_solver. + + solve_sep_entails. +Qed. + Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ □?p [★] Γ -★ Δ'. Proof. rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf. @@ -222,16 +262,13 @@ Lemma envs_replace_sound Δ Δ' i p q P Γ : Δ ⊢ □?p P ★ (□?q [★] Γ -★ Δ'). Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed. -Lemma envs_split_sound Δ lr js Δ1 Δ2 : - envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ★ Δ2. +Lemma envs_lookup_envs_clear_spatial Δ j : + envs_lookup j (envs_clear_spatial Δ) + = '(p,P) ← envs_lookup j Δ; if p then Some (p,P) else None. Proof. - rewrite /envs_split /of_envs=> ?; apply pure_elim_sep_l=> Hwf. - destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=. - rewrite (env_split_perm Γs) // big_sep_app {1}always_sep_dup'. - destruct lr; simplify_eq/=; cancel [□ [∧] Γp; □ [∧] Γp; [★] Γs1; [★] Γs2]%I; - destruct Hwf; apply sep_intro_True_l; apply pure_intro; constructor; - naive_solver eauto using env_split_wf_1, env_split_wf_2, - env_split_fresh_1, env_split_fresh_2. + rewrite /envs_lookup /envs_clear_spatial. + destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto. + by destruct (Γs !! j). Qed. Lemma envs_clear_spatial_sound Δ : Δ ⊢ envs_clear_spatial Δ ★ [★] env_spatial Δ. @@ -252,6 +289,52 @@ Lemma env_spatial_is_nil_persistent Δ : Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed. Hint Immediate env_spatial_is_nil_persistent : typeclass_instances. +Lemma envs_lookup_envs_delete Δ i p P : + envs_wf Δ → + envs_lookup i Δ = Some (p,P) → envs_lookup i (envs_delete i p Δ) = None. +Proof. + rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup. + destruct Δ as [Γp Γs], p; simplify_eq/=. + - rewrite env_lookup_env_delete //. revert Hlookup. + destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _). + - rewrite env_lookup_env_delete //. by destruct (Γp !! _). +Qed. +Lemma envs_lookup_envs_delete_ne Δ i j p : + i ≠ j → envs_lookup i (envs_delete j p Δ) = envs_lookup i Δ. +Proof. + rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=. + - by rewrite env_lookup_env_delete_ne. + - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne. +Qed. + +Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' : + (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) → + envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') → Δ1 ★ Δ2 ⊢ Δ1' ★ Δ2'. +Proof. + revert Δ1 Δ2 Δ1' Δ2'. + induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|]. + apply pure_elim with (envs_wf Δ1); [unfold of_envs; solve_sep_entails|]=> Hwf. + destruct (envs_lookup_delete j Δ1) + as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq; auto. + apply envs_lookup_delete_Some in Hdel as [??]; subst. + rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc. + rewrite -(IH _ _ _ _ _ HΔ); last first. + { intros j' P'; destruct (decide (j = j')) as [->|]. + - by rewrite (envs_lookup_envs_delete _ _ _ P). + - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. } + rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto. +Qed. +Lemma envs_split_sound Δ lr js Δ1 Δ2 : + envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ★ Δ2. +Proof. + rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ). + rewrite {2}envs_clear_spatial_sound sep_elim_l always_and_sep_r. + destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done]. + apply envs_split_go_sound in HΔ as ->; last first. + { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. } + destruct lr; simplify_eq; solve_sep_entails. +Qed. + Global Instance envs_Forall2_refl (R : relation (uPred M)) : Reflexive R → Reflexive (envs_Forall2 R). Proof. by constructor. Qed. diff --git a/proofmode/environments.v b/proofmode/environments.v index 0278dba89e3f6880e4cdfba5199e1722ef78a2b3..e3385e5fdd9e8ec8b9d92bcbccbce153fbd03bcd 100644 --- a/proofmode/environments.v +++ b/proofmode/environments.v @@ -48,6 +48,7 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) := Γ' ← env_app Γapp Γ; match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end end. + Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) := match Γ with | Enil => None @@ -58,11 +59,13 @@ Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) : | Some _ => None end end. + Fixpoint env_delete {A} (i : string) (Γ : env A) : env A := match Γ with | Enil => Enil | Esnoc Γ j x => if decide (i = j) then Γ else Esnoc (env_delete i Γ) j x end. + Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) := match Γ with | Enil => None @@ -70,14 +73,6 @@ Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) := if decide (i = j) then Some (x,Γ) else '(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x) end. -Fixpoint env_split_go {A} (js : list string) - (Γ1 Γ2 : env A) : option (env A * env A) := - match js with - | [] => Some (Γ1, Γ2) - | j::js => '(x,Γ2) ← env_lookup_delete j Γ2; env_split_go js (Esnoc Γ1 j x) Γ2 - end. -Definition env_split {A} (js : list string) - (Γ : env A) : option (env A * env A) := env_split_go js Enil Γ. Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop := | env_Forall2_nil : env_Forall2 P Enil Enil @@ -98,6 +93,12 @@ Proof. induction Γ; intros; simplify; rewrite 1?Permutation_swap; f_equiv; eauto. Qed. +Lemma env_lookup_snoc Γ i P : env_lookup i (Esnoc Γ i P) = Some P. +Proof. induction Γ; simplify; auto. Qed. +Lemma env_lookup_snoc_ne Γ i j P : + i ≠ j → env_lookup i (Esnoc Γ j P) = env_lookup i Γ. +Proof. induction Γ=> ?; simplify; auto. Qed. + Lemma env_app_perm Γ Γapp Γ' : env_app Γapp Γ = Some Γ' → env_to_list Γ' ≡ₚ Γapp ++ Γ. Proof. revert Γ'; induction Γapp; intros; simplify; f_equal; auto. Qed. @@ -144,63 +145,17 @@ Proof. induction Γ; intros; simplify; eauto. Qed. Lemma env_lookup_delete_Some Γ Γ' i x : env_lookup_delete i Γ = Some (x,Γ') ↔ Γ !! i = Some x ∧ Γ' = env_delete i Γ. Proof. rewrite env_lookup_delete_correct; simplify; naive_solver. Qed. -Lemma env_delete_fresh_eq Γ j : env_wf Γ → env_delete j Γ !! j = None. + +Lemma env_lookup_env_delete Γ j : env_wf Γ → env_delete j Γ !! j = None. Proof. induction 1; intros; simplify; eauto. Qed. +Lemma env_lookup_env_delete_ne Γ i j : i ≠ j → env_delete j Γ !! i = Γ !! i. +Proof. induction Γ; intros; simplify; eauto. Qed. Lemma env_delete_fresh Γ i j : Γ !! i = None → env_delete j Γ !! i = None. Proof. induction Γ; intros; simplify; eauto. Qed. + Lemma env_delete_wf Γ j : env_wf Γ → env_wf (env_delete j Γ). Proof. induction 1; simplify; eauto using env_delete_fresh. Qed. -Lemma env_split_fresh Γ1 Γ2 Γ1' Γ2' js i : - env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') → - Γ1 !! i = None → Γ2 !! i = None → Γ1' !! i = None ∧ Γ2' !! i = None. -Proof. - revert Γ1 Γ2. - induction js as [|j js IH]=> Γ1 Γ2 ???; simplify_eq/=; eauto. - destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=. - apply env_lookup_delete_Some in Hdelete as [? ->]. - eapply IH; eauto; simplify; eauto using env_delete_fresh. -Qed. -Lemma env_split_go_wf Γ1 Γ2 Γ1' Γ2' js : - env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') → - (∀ i, Γ1 !! i = None ∨ Γ2 !! i = None) → - env_wf Γ1 → env_wf Γ2 → env_wf Γ1' ∧ env_wf Γ2'. -Proof. - revert Γ1 Γ2. - induction js as [|j js IH]=> Γ1 Γ2 ? Hdisjoint ??; simplify_eq/=; auto. - destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=. - apply env_lookup_delete_Some in Hdelete as [? ->]. - eapply IH; eauto using env_delete_wf. - - intros i; simplify; eauto using env_delete_fresh_eq. - destruct (Hdisjoint i); eauto using env_delete_fresh. - - constructor; auto. - destruct (Hdisjoint j) as [?|[]%eq_None_not_Some]; eauto. -Qed. -Lemma env_split_go_perm Γ1 Γ2 Γ1' Γ2' js : - env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') → Γ1 ++ Γ2 ≡ₚ Γ1' ++ Γ2'. -Proof. - revert Γ1 Γ2. induction js as [|j js IH]=> Γ1 Γ2 ?; simplify_eq/=; auto. - destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=. - apply env_lookup_delete_Some in Hdelete as [? ->]. - by rewrite -(IH (Esnoc _ _ _) (env_delete _ _)) //= - Permutation_middle -env_lookup_perm. -Qed. - -Lemma env_split_fresh_1 Γ Γ1 Γ2 js i : - env_split js Γ = Some (Γ1,Γ2) → Γ !! i = None → Γ1 !! i = None. -Proof. intros. by apply (env_split_fresh Enil Γ Γ1 Γ2 js). Qed. -Lemma env_split_fresh_2 Γ Γ1 Γ2 js i : - env_split js Γ = Some (Γ1,Γ2) → Γ !! i = None → Γ2 !! i = None. -Proof. intros. by apply (env_split_fresh Enil Γ Γ1 Γ2 js). Qed. -Lemma env_split_wf_1 Γ Γ1 Γ2 js : - env_split js Γ = Some (Γ1,Γ2) → env_wf Γ → env_wf Γ1. -Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed. -Lemma env_split_wf_2 Γ Γ1 Γ2 js : - env_split js Γ = Some (Γ1,Γ2) → env_wf Γ → env_wf Γ2. -Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed. -Lemma env_split_perm Γ Γ1 Γ2 js : env_split js Γ = Some (Γ1,Γ2) → Γ ≡ₚ Γ1 ++ Γ2. -Proof. apply env_split_go_perm. Qed. - Global Instance env_Forall2_refl (P : relation A) : Reflexive P → Reflexive (env_Forall2 P). Proof. intros ? Γ. induction Γ; constructor; auto. Qed. diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 3411a43617d92fdaa48ef6e3ad635bbcd09bb32c..113b9bef5888930a4ac99dfc7df3dee88decce99 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -5,16 +5,16 @@ From iris.proofmode Require Import class_instances. From iris.prelude Require Import stringmap hlist. Declare Reduction env_cbv := cbv [ - env_lookup env_fold env_lookup_delete env_delete env_app - env_replace env_split_go env_split + env_lookup env_fold env_lookup_delete env_delete env_app env_replace decide (* operational classes *) sumbool_rec sumbool_rect (* sumbool *) bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *) assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect string_eq_dec string_rec string_rect (* strings *) env_persistent env_spatial env_spatial_is_nil - envs_lookup envs_lookup_delete envs_delete envs_app - envs_simple_replace envs_replace envs_split envs_clear_spatial]. + envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app + envs_simple_replace envs_replace envs_split envs_clear_spatial + envs_split_go envs_split]. Ltac env_cbv := match goal with |- ?u => let v := eval env_cbv in u in change v end. @@ -396,14 +396,14 @@ Tactic Notation "iSplitL" constr(Hs) := [let P := match goal with |- FromSep ?P _ _ => P end in apply _ || fail "iSplitL:" P "not a separating conjunction" |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs - "not found in the spatial context"| |]. + "not found in the context"| |]. Tactic Notation "iSplitR" constr(Hs) := let Hs := words Hs in eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *) [let P := match goal with |- FromSep ?P _ _ => P end in apply _ || fail "iSplitR:" P "not a separating conjunction" |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs - "not found in the spatial context"| |]. + "not found in the context"| |]. Tactic Notation "iSplitL" := iSplitR "". Tactic Notation "iSplitR" := iSplitL "".