Commit 7b63a3da authored by Robbert Krebbers's avatar Robbert Krebbers

Make iSplit{L,R} ignore persistent hypotheses.

Before, it failed when these tactics were invoked with persistent
hypotheses. The new behavior is more convenient when using these
tactics to build other tactics.
parent 0afa9b92
Pipeline #2718 passed with stage
in 9 minutes and 25 seconds
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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 "".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment