From 938ea90c7122dc1b63f40a26ee6ff605ceb4368d Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Mon, 12 Mar 2018 00:01:05 -0400
Subject: [PATCH] Store a counter in  to assign fresh names with .

---
 theories/proofmode/coq_tactics.v | 72 ++++++++++++++++++++------------
 theories/proofmode/notation.v    | 10 ++---
 theories/proofmode/tactics.v     | 37 ++++++++--------
 theories/tests/proofmode.v       | 15 ++++++-
 4 files changed, 81 insertions(+), 53 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index cc9c7c09a..561af06f7 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -8,11 +8,12 @@ Import env_notations.
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
 Record envs (PROP : bi) :=
-  Envs { env_persistent : env PROP; env_spatial : env PROP }.
+  Envs { env_persistent : env PROP; env_spatial : env PROP; env_counter : positive }.
 Add Printing Constructor envs.
-Arguments Envs {_} _ _.
+Arguments Envs {_} _ _ _.
 Arguments env_persistent {_} _.
 Arguments env_spatial {_} _.
+Arguments env_counter {_} _.
 
 Record envs_wf {PROP} (Δ : envs PROP) := {
   env_persistent_valid : env_wf (env_persistent Δ);
@@ -43,7 +44,7 @@ Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
   env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
 
 Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match env_lookup i Γp with
   | Some P => Some (true, P)
   | None => P ← env_lookup i Γs; Some (false, P)
@@ -51,18 +52,18 @@ Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP
 
 Definition envs_delete {PROP} (remove_persistent : bool)
     (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match p with
-  | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs
-  | false => Envs Γp (env_delete i Γs)
+  | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
+  | false => Envs Γp (env_delete i Γs) n
   end.
 
 Definition envs_lookup_delete {PROP} (remove_persistent : bool)
     (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match env_lookup_delete i Γp with
-  | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs)
-  | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
+  | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
+  | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
   end.
 
 Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
@@ -77,23 +78,23 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
 
 Definition envs_snoc {PROP} (Δ : envs PROP)
     (p : bool) (j : ident) (P : PROP) : envs PROP :=
-  let (Γp,Γs) := Δ in
-  if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).
+  let (Γp,Γs,n) := Δ in
+  if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
 
 Definition envs_app {PROP : bi} (p : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match p with
-  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs)
-  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs')
+  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs n)
+  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs' n)
   end.
 
 Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  let (Γp,Γs) := Δ in
+  let (Γp,Γs,n) := Δ in
   match p with
-  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs)
-  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs')
+  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs n)
+  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs' n)
   end.
 
 Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
@@ -105,10 +106,13 @@ Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
   if env_spatial Δ is Enil then true else false.
 
 Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs (env_persistent Δ) Enil.
+  Envs (env_persistent Δ) Enil (env_counter Δ).
 
 Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs Enil (env_spatial Δ).
+  Envs Enil (env_spatial Δ) (env_counter Δ).
+
+Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
+  Envs (env_persistent Δ) (env_spatial Δ) (Pos.succ (env_counter Δ)).
 
 Fixpoint envs_split_go {PROP}
     (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
@@ -464,7 +468,7 @@ Proof.
     eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails.
 Qed.
 Global Instance Envs_proper (R : relation PROP) :
-  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
+  Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP).
 Proof. by constructor. Qed.
 
 Global Instance envs_entails_proper :
@@ -474,8 +478,12 @@ Global Instance envs_entails_flip_mono :
   Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
 Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
 
+Instance envs_incr_counter_proper :
+  Proper (envs_Forall2 (⊣⊢) ==> envs_Forall2 (⊣⊢)) (@envs_incr_counter PROP).
+Proof. intros ?? [? ?]; by constructor => //=. Qed.
+
 (** * Adequacy *)
-Lemma tac_adequate P : envs_entails (Envs Enil Enil) P → P.
+Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P → P.
 Proof.
   rewrite envs_entails_eq /of_envs /= persistently_True_emp
           affinely_persistently_emp left_id=><-.
@@ -1083,6 +1091,18 @@ Lemma tac_accu Δ P :
   envs_entails Δ P.
 Proof. rewrite envs_entails_eq=><-. apply prop_of_env_sound. Qed.
 
+(** * Fresh *)
+Lemma envs_incr_counter_equiv Δ: envs_Forall2 (⊣⊢) Δ (envs_incr_counter Δ).
+Proof. rewrite //=. Qed.
+
+Lemma tac_fresh Δ Δ' (Q : PROP) :
+  envs_incr_counter Δ = Δ' →
+  envs_entails Δ' Q → envs_entails Δ Q.
+Proof.
+  rewrite envs_entails_eq => <-. by setoid_rewrite <-envs_incr_counter_equiv.
+Qed.
+
+
 End bi_tactics.
 
 (** The following _private_ classes are used internally by [tac_modal_intro] /
@@ -1260,15 +1280,15 @@ Section tac_modal_intro.
   Qed.
 
   (** The actual introduction tactic *)
-  Lemma tac_modal_intro {A} (sel : A) Γp Γs Γp' Γs' Q Q' fi :
+  Lemma tac_modal_intro {A} (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
     FromModal M sel Q' Q →
     IntoModalPersistentEnv M Γp Γp' (modality_persistent_spec M) →
     IntoModalSpatialEnv M Γs Γs' (modality_spatial_spec M) fi →
     (if fi then Absorbing Q' else TCTrue) →
-    envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
+    envs_entails (Envs Γp' Γs' n) Q → envs_entails (Envs Γp Γs n) Q'.
   Proof.
     rewrite envs_entails_eq /FromModal /of_envs /= => HQ' HΓp HΓs ? HQ.
-    apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')) as Hwf.
+    apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs' n)) as Hwf.
     { split; simpl in *.
       - destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
       - destruct HΓs as [| |?????? []| |]; eauto using Enil_wf.
@@ -1363,10 +1383,10 @@ Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
       (MaybeIntoLaterN false n) (env_spatial Δ1) (env_spatial Δ2) false
 }.
 
-Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
+Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 m :
   TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
   TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
-  MaybeIntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
+  MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
 Proof. by split. Qed.
 
 Lemma into_laterN_env_sound n Δ1 Δ2 :
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index b0d9d5157..37bce07be 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -3,7 +3,7 @@ From stdpp Require Export strings.
 Set Default Proof Using "Type".
 
 Delimit Scope proof_scope with env.
-Arguments Envs _ _%proof_scope _%proof_scope.
+Arguments Envs _ _%proof_scope _%proof_scope _.
 Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%I.
 
@@ -16,17 +16,17 @@ Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
    left associativity, format "Γ '_'  :  P '//'", only printing) : proof_scope.
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
-  (envs_entails (Envs Γ Δ) Q%I)
+  (envs_entails (Envs Γ Δ _) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
   stdpp_scope.
 Notation "Δ '--------------------------------------' ∗ Q" :=
-  (envs_entails (Envs Enil Δ) Q%I)
+  (envs_entails (Envs Enil Δ _) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
 Notation "Γ '--------------------------------------' □ Q" :=
-  (envs_entails (Envs Γ Enil) Q%I)
+  (envs_entails (Envs Γ Enil _) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : stdpp_scope.
-Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil) Q%I)
+Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil _) Q%I)
   (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 268d813e4..bbee041e1 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -10,12 +10,12 @@ Export ident.
 
 Declare Reduction env_cbv := cbv [
   option_bind
-  beq ascii_beq string_beq positive_beq ident_beq
+  beq ascii_beq string_beq positive_beq Pos.succ ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
-  env_persistent env_spatial env_spatial_is_nil envs_dom
+  env_persistent env_spatial env_counter env_spatial_is_nil envs_dom
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
     envs_simple_replace envs_replace envs_split
-    envs_clear_spatial envs_clear_persistent
+    envs_clear_spatial envs_clear_persistent envs_incr_counter
     envs_split_go envs_split prop_of_env].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
@@ -44,14 +44,11 @@ Ltac iSolveTC :=
 Ltac iFresh :=
   lazymatch goal with
   |- envs_entails ?Δ _ =>
-     (* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
-     first use [cbv] to compute the domain of [Δ] *)
-     let Hs := eval cbv in (envs_dom Δ) in
-     eval vm_compute in
-       (IAnon (match Hs with
-         | [] => 1
-         | _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
-         end))%positive
+  let do_incr := (lazymatch goal with
+                    _ => eapply tac_fresh; first by (env_reflexivity)
+                  end) in
+    let n := eval env_cbv in (Pos.succ (env_counter Δ)) in
+    constr:(IAnon n)
   | _ => constr:(IAnon 1)
   end.
 
@@ -200,13 +197,13 @@ Tactic Notation "iAssumptionCore" :=
     | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j|find Γ i P]
     end in
   match goal with
-  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
+  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
      first [is_evar i; fail 1 | env_reflexivity]
-  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
+  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
      is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
-  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
      first [is_evar i; fail 1 | env_reflexivity]
-  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
      is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
   end.
 
@@ -228,7 +225,7 @@ Tactic Notation "iAssumption" :=
        |find p Γ Q]
     end in
   lazymatch goal with
-  | |- envs_entails (Envs ?Γp ?Γs) ?Q =>
+  | |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
      first [find true Γp Q | find false Γs Q
            |fail "iAssumption:" Q "not found"]
   end.
@@ -974,7 +971,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Modality introduction *)
 Tactic Notation "iModIntro" uconstr(sel) :=
   iStartProof;
-  notypeclasses refine (tac_modal_intro _ sel _ _ _ _ _ _ _ _ _ _ _ _);
+  notypeclasses refine (tac_modal_intro _ sel _ _ _ _ _ _ _ _ _ _ _ _ _);
     [iSolveTC ||
      fail "iModIntro: the goal is not a modality"
     |iSolveTC ||
@@ -1569,8 +1566,8 @@ Ltac iHypsContaining x :=
        | _ => go Γ x Hs
        end
      end in
-  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _) _ => Γp end in
-  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs) _ => Γs end in
+  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _ _) _ => Γp end in
+  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs _) _ => Γs end in
   let Hs := go Γp x (@nil ident) in go Γs x Hs.
 
 Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
@@ -1872,7 +1869,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
       first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i]
     end in
   lazymatch goal with
-  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some _ =>
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some _ =>
      first [find Γp i|find Γs i]; env_reflexivity
   end.
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index fc8ff5bcd..f9c38b371 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
-From stdpp Require Import gmap.
+From iris.proofmode Require Import tactics intro_patterns.
+From stdpp Require Import gmap hlist.
 Set Default Proof Using "Type".
 
 Section tests.
@@ -112,6 +112,17 @@ Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
   P -∗ Q → R -∗ emp.
 Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
 
+Let test_fresh P Q:
+  (P ∗ Q) -∗ (P ∗ Q).
+Proof.
+  iIntros "H".
+  let H1 := iFresh in
+  let H2 := iFresh in
+  let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in 
+  iDestruct "H" as pat.
+  iFrame.
+Qed.
+
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
-- 
GitLab