From 7b63a3da2f32aa0e28bd4417f705121875d36404 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 13:07:44 +0200
Subject: [PATCH] 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.
---
 ProofMode.md             |   3 +-
 proofmode/coq_tactics.v  | 123 ++++++++++++++++++++++++++++++++-------
 proofmode/environments.v |  73 +++++------------------
 proofmode/tactics.v      |  12 ++--
 4 files changed, 125 insertions(+), 86 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 4f14da9f3..9c1404676 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 408ca2844..e9f809ec2 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 0278dba89..e3385e5fd 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 3411a4361..113b9bef5 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 "".
-- 
GitLab