Merge branch 'robbert/proofmode_anon_hyps' into 'master'

Improved treatment of anonymous hypotheses in the proof mode

See merge request FP/iris-coq!83

theories/base_logic/lib/invariants.v

@@ -92,7 +92,7 @@ End inv.
 Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
   let Htmp := iFresh in
   let patback := intro_pat.parse_one Hclose in
-  let pat := constr:(IList [[IName Htmp; patback]]) in
+  let pat := constr:(IList [[IIdent Htmp; patback]]) in
   iMod (inv_open _ N with "[#]") as pat;
     [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
     [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end

theories/base_logic/lib/wsat.v

@@ -104,7 +104,7 @@ Qed.
 Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
 Proof.
   rewrite /ownI /wsat -!lock.
-  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
+  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
   iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
@@ -115,7 +115,7 @@ Qed.
 Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}.
 Proof.
   rewrite /ownI /wsat -!lock.
-  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
+  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
   iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
   - iDestruct (ownD_singleton_twice with "[$]") as %[].
@@ -128,7 +128,7 @@ Lemma ownI_alloc φ P :
   wsat ∗ ▷ P ==∗ ∃ i, ⌜φ i⌝ ∗ wsat ∗ ownI i P.
 Proof.
   iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
-  iDestruct "Hw" as (I) "[? HI]".
+  iDestruct "Hw" as (I) "[Hw HI]".
   iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
   iMod (own_updateP with "[$]") as "HE".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
@@ -150,7 +150,7 @@ Lemma ownI_alloc_open φ P :
   (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
   wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
 Proof.
-  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[? HI]".
+  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
   iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
   iMod (own_updateP with "[$]") as "HD".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).

theories/heap_lang/lib/ticket_lock.v

@@ -153,7 +153,7 @@ Section proof.
     wp_store.
     iDestruct (own_valid_2 with "Hauth Hγo") as
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
-    iDestruct "Haown" as "[[Hγo' _]|?]".
+    iDestruct "Haown" as "[[Hγo' _]|Haown]".
     { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
     iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
     { apply auth_update, prod_local_update_1.

theories/proofmode/base.v

@@ -49,3 +49,37 @@ Qed.
 
 Lemma string_beq_reflect s1 s2 : reflect (s1 = s2) (string_beq s1 s2).
 Proof. apply iff_reflect. by rewrite string_beq_true. Qed.
+
+Module Export ident.
+Inductive ident :=
+  | IAnon : positive → ident
+  | INamed :> string → ident.
+End ident.
+
+Instance maybe_IAnon : Maybe IAnon := λ i,
+  match i with IAnon n => Some n | _ => None end.
+Instance maybe_INamed : Maybe INamed := λ i,
+  match i with INamed s => Some s | _ => None end.
+
+Instance beq_eq_dec : EqDecision ident.
+Proof. solve_decision. Defined.
+
+Definition positive_beq := Eval compute in Pos.eqb.
+
+Lemma positive_beq_true x y : positive_beq x y = true ↔ x = y.
+Proof. apply Pos.eqb_eq. Qed.
+
+Definition ident_beq (i1 i2 : ident) : bool :=
+  match i1, i2 with
+  | IAnon n1, IAnon n2 => positive_beq n1 n2
+  | INamed s1, INamed s2 => string_beq s1 s2
+  | _, _ => false
+  end.
+
+Lemma ident_beq_true i1 i2 : ident_beq i1 i2 = true ↔ i1 = i2.
+Proof.
+  destruct i1, i2; rewrite /= ?string_beq_true ?positive_beq_true; naive_solver.
+Qed.
+
+Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
+Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.

theories/proofmode/coq_tactics.v

 From iris.base_logic Require Export base_logic.
 From iris.base_logic Require Import big_op tactics.
 From iris.proofmode Require Export base environments classes.
-From stdpp Require Import stringmap hlist.
 Set Default Proof Using "Type".
 Import uPred.
 Import env_notations.
@@ -36,22 +35,22 @@ Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
   env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
 }.
 
-Definition envs_dom {M} (Δ : envs M) : list string :=
+Definition envs_dom {M} (Δ : envs M) : list ident :=
   env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
 
-Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
+Definition envs_lookup {M} (i : ident) (Δ : envs M) : option (bool * uPred M) :=
   let (Γp,Γs) := Δ in
   match env_lookup i Γp with
   | Some P => Some (true, P) | None => P ← env_lookup i Γs; Some (false, P)
   end.
 
-Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
+Definition envs_delete {M} (i : ident) (p : bool) (Δ : envs M) : envs M :=
   let (Γp,Γs) := Δ in
   match p with
   | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
   end.
 
-Definition envs_lookup_delete {M} (i : string)
+Definition envs_lookup_delete {M} (i : ident)
     (Δ : envs M) : option (bool * uPred M * envs M) :=
   let (Γp,Γs) := Δ in
   match env_lookup_delete i Γp with
@@ -59,7 +58,7 @@ Definition envs_lookup_delete {M} (i : string)
   | None => '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
   end.
 
-Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : bool)
+Fixpoint envs_lookup_delete_list {M} (js : list ident) (remove_persistent : bool)
     (Δ : envs M) : option (bool * list (uPred M) * envs M) :=
   match js with
   | [] => Some (true, [], Δ)
@@ -71,7 +70,7 @@ Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : boo
   end.
 
 Definition envs_snoc {M} (Δ : envs M)
-    (p : bool) (j : string) (P : uPred M) : envs M :=
+    (p : bool) (j : ident) (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).
 
@@ -83,7 +82,7 @@ Definition envs_app {M} (p : bool)
   | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs')
   end.
 
-Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
+Definition envs_simple_replace {M} (i : ident) (p : bool) (Γ : env (uPred M))
     (Δ : envs M) : option (envs M) :=
   let (Γp,Γs) := Δ in
   match p with
@@ -91,7 +90,7 @@ Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
   | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs')
   end.
 
-Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
+Definition envs_replace {M} (i : ident) (p q : bool) (Γ : env (uPred M))
     (Δ : envs M) : option (envs M) :=
   if eqb p q then envs_simple_replace i p Γ Δ
   else envs_app q Γ (envs_delete i p Δ).
@@ -106,7 +105,7 @@ Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
   Envs Enil (env_spatial Δ).
 
 Fixpoint envs_split_go {M}
-    (js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
+    (js : list ident) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
   match js with
   | [] => Some (Δ1, Δ2)
   | j :: js =>
@@ -117,7 +116,7 @@ Fixpoint envs_split_go {M}
 (* if [d = Right] then [result = (remaining hyps, hyps named js)] and
    if [d = Left] then [result = (hyps named js, remaining hyps)] *)
 Definition envs_split {M} (d : direction)
-    (js : list string) (Δ : envs M) : option (envs M * envs M) :=
+    (js : list ident) (Δ : envs M) : option (envs M * envs M) :=
   '(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
@@ -224,11 +223,11 @@ Proof.
   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; destruct (string_beq_reflect j i); naive_solver.
+      intros j; destruct (ident_beq_reflect j i); naive_solver.
     + by rewrite persistently_sep assoc.
   - apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
-      intros j; destruct (string_beq_reflect j i); naive_solver.
+      intros j; destruct (ident_beq_reflect j i); naive_solver.
     + solve_sep_entails.
 Qed.
 

theories/proofmode/environments.v

-From stdpp Require Export strings.
 From iris.proofmode Require Import base.
 From iris.algebra Require Export base.
-From stdpp Require Import stringmap.
 Set Default Proof Using "Type".
 
 Inductive env (A : Type) : Type :=
   | Enil : env A
-  | Esnoc : env A → string → A → env A.
+  | Esnoc : env A → ident → A → env A.
 Arguments Enil {_}.
-Arguments Esnoc {_} _ _%string _.
+Arguments Esnoc {_} _ _ _.
 Instance: Params (@Enil) 1.
 Instance: Params (@Esnoc) 1.
 
-Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
+Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
   match Γ with
   | Enil => None
-  | Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
+  | Esnoc Γ j x => if ident_beq i j then Some x else env_lookup i Γ
   end.
 
 Module env_notations.
@@ -37,7 +35,7 @@ Fixpoint env_to_list {A} (E : env A) : list A :=
 Coercion env_to_list : env >-> list.
 Instance: Params (@env_to_list) 1.
 
-Fixpoint env_dom {A} (Γ : env A) : list string :=
+Fixpoint env_dom {A} (Γ : env A) : list ident :=
   match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
 
 Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
@@ -48,28 +46,28 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
      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) :=
+Fixpoint env_replace {A} (i: ident) (Γi: env A) (Γ: env A) : option (env A) :=
   match Γ with
   | Enil => None
   | Esnoc Γ j x =>
-     if string_beq i j then env_app Γi Γ else
+     if ident_beq i j then env_app Γi Γ else
      match Γi !! j with
      | None => Γ' ← env_replace i Γi Γ; Some (Esnoc Γ' j x)
      | Some _ => None
      end
   end.
 
-Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
+Fixpoint env_delete {A} (i : ident) (Γ : env A) : env A :=
   match Γ with
   | Enil => Enil
-  | Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x
+  | Esnoc Γ j x => if ident_beq i j then Γ else Esnoc (env_delete i Γ) j x
   end.
 
-Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
+Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
   match Γ with
   | Enil => None
   | Esnoc Γ j x =>
-     if string_beq i j then Some (x,Γ)
+     if ident_beq i j then Some (x,Γ)
      else '(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
   end.
 
@@ -88,15 +86,15 @@ Inductive env_subenv {A} : relation (env A) :=
 Section env.
 Context {A : Type}.
 Implicit Types Γ : env A.
-Implicit Types i : string.
+Implicit Types i : ident.
 Implicit Types x : A.
 Hint Resolve Esnoc_wf Enil_wf.
 
 Ltac simplify :=
   repeat match goal with
   | _ => progress simplify_eq/=
-  | H : context [string_beq ?s1 ?s2] |- _ => destruct (string_beq_reflect s1 s2)
-  | |- context [string_beq ?s1 ?s2] => destruct (string_beq_reflect s1 s2)
+  | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
+  | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
   | _ => case_match
   end.
 

theories/proofmode/intro_patterns.v

@@ -3,7 +3,7 @@ From iris.proofmode Require Import base tokens sel_patterns.
 Set Default Proof Using "Type".
 
 Inductive intro_pat :=
-  | IName : string → intro_pat
+  | IIdent : ident → intro_pat
   | IAnom : intro_pat
   | IDrop : intro_pat
   | IFrame : intro_pat
@@ -73,7 +73,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   match ts with
   | [] => Some k
   | TName "_" :: ts => parse_go ts (SPat IDrop :: k)
-  | TName s :: ts => parse_go ts (SPat (IName s) :: k)
+  | TName s :: ts => parse_go ts (SPat (IIdent s) :: k)
   | TAnom :: ts => parse_go ts (SPat IAnom :: k)
   | TFrame :: ts => parse_go ts (SPat IFrame :: k)
   | TBracketL :: ts => parse_go ts (SList :: k)
@@ -98,11 +98,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   end
 with parse_clear (ts : list token) (k : stack) : option stack :=
   match ts with
-  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
+  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelIdent s)) :: k)
   | TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
   | TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
   | TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
-  | TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
+  | TName s :: ts => parse_clear ts (SPat (IClear (SelIdent s)) :: k)
   | TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
   | TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
   | TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
@@ -134,6 +134,7 @@ Ltac parse s :=
      lazymatch eval vm_compute in (parse s) with
      | Some ?pats => pats | _ => fail "invalid list intro_pat" s
      end
+  | ident => constr:([IIdent s])
   | ?X => fail "intro_pat.parse:" s "has unexpected type" X
   end.
 Ltac parse_one s :=
@@ -165,6 +166,7 @@ Ltac intro_pat_persistent p :=
   | string =>
      let pat := intro_pat.parse p in
      eval cbv in (forallb intro_pat_persistent pat)
+  | ident => false
   | bool => p
   | ?X => fail "intro_pat_persistent:" p "has unexpected type" X
   end.

theories/proofmode/notation.v

@@ -8,9 +8,12 @@ Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
 
 Notation "" := Enil (only printing) : proof_scope.
-Notation "Γ H : P" := (Esnoc Γ H P)
+Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
+Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
+  (at level 1, P at level 200,
+   left associativity, format "Γ '_'  :  P '//'", only printing) : proof_scope.
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Γ Δ) Q%I)

theories/proofmode/sel_patterns.v

@@ -6,7 +6,7 @@ Inductive sel_pat :=
   | SelPure
   | SelPersistent
   | SelSpatial
-  | SelName : string → sel_pat.
+  | SelIdent : ident → sel_pat.
 
 Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
   match ps with
@@ -19,7 +19,7 @@ Module sel_pat.
 Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :=
   match ts with
   | [] => Some (reverse k)
-  | TName s :: ts => parse_go ts (SelName s :: k)
+  | TName s :: ts => parse_go ts (SelIdent s :: k)
   | TPure :: ts => parse_go ts (SelPure :: k)
   | TAlways :: ts => parse_go ts (SelPersistent :: k)
   | TSep :: ts => parse_go ts (SelSpatial :: k)
@@ -32,7 +32,9 @@ Ltac parse s :=
   lazymatch type of s with
   | sel_pat => constr:([s])
   | list sel_pat => s
-  | list string => eval vm_compute in (SelName <$> s)
+  | ident => constr:([SelIdent s])
+  | list ident => eval vm_compute in (SelIdent <$> s)
+  | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
   | string =>
      lazymatch eval vm_compute in (parse s) with
      | Some ?pats => pats | _ => fail "invalid sel_pat" s

theories/proofmode/spec_patterns.v

 From stdpp Require Export strings.
-From iris.proofmode Require Import tokens.
+From iris.proofmode Require Import base tokens.
 Set Default Proof Using "Type".
 
 Inductive goal_kind := GSpatial | GModal | GPersistent.
@@ -7,14 +7,14 @@ Inductive goal_kind := GSpatial | GModal | GPersistent.
 Record spec_goal := SpecGoal {
   spec_goal_kind : goal_kind;
   spec_goal_negate : bool;
-  spec_goal_frame : list string;
-  spec_goal_hyps : list string;
+  spec_goal_frame : list ident;
+  spec_goal_hyps : list ident;
   spec_goal_done : bool
 }.
 
 Inductive spec_pat :=
   | SForall : spec_pat
-  | SName : string → spec_pat
+  | SIdent : ident → spec_pat
   | SPureGoal : bool → spec_pat
   | SGoal : spec_goal → spec_pat
   | SAutoFrame : goal_kind → spec_pat.
@@ -36,7 +36,7 @@ Inductive state :=
 Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | [] => Some (reverse k)
-  | TName s :: ts => parse_go ts (SName s :: k)
+  | TName s :: ts => parse_go ts (SIdent s :: k)
   | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GPersistent :: k)
   | TBracketL :: TFrame :: TBracketR :: ts =>
@@ -52,14 +52,14 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
   | _ => None
   end
 with parse_goal (ts : list token)
-    (ki : goal_kind) (neg : bool) (frame hyps : list string)
+    (ki : goal_kind) (neg : bool) (frame hyps : list ident)
     (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | TMinus :: ts =>
      guard (¬neg ∧ frame = [] ∧ hyps = []);
      parse_goal ts ki true frame hyps k
-  | TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
-  | TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
+  | TName s :: ts => parse_goal ts ki neg frame (INamed s :: hyps) k
+  | TFrame :: TName s :: ts => parse_goal ts ki neg (INamed s :: frame) hyps k
   | TDone :: TBracketR :: ts =>
      parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
   | TBracketR :: ts =>
@@ -76,11 +76,4 @@ Ltac parse s :=
               | Some ?pats => pats | _ => fail "invalid list spec_pat" s
               end
   end.
-Ltac parse_one s :=
-  lazymatch type of s with
-  | spec_pat => s
-  | string => lazymatch eval vm_compute in (parse s) with
-              | Some [?pat] => pat | _ => fail "invalid spec_pat" s
-              end
-  end.
 End spec_pat.

theories/proofmode/tactics.v

@@ -3,11 +3,12 @@ From iris.proofmode Require Import base intro_patterns spec_patterns sel_pattern
 From iris.base_logic Require Export base_logic big_op.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
-From stdpp Require Import stringmap hlist.
+From stdpp Require Import hlist pretty.
 Set Default Proof Using "Type".
+Export ident.
 
 Declare Reduction env_cbv := cbv [
-  beq ascii_beq string_beq
+  beq ascii_beq string_beq positive_beq 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
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
@@ -20,16 +21,19 @@ Ltac env_reflexivity := env_cbv; exact eq_refl.
 
 (** * Misc *)
 (* Tactic Notation tactics cannot return terms *)
-Ltac iFresh' H :=
+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 (fresh_string_of_set H (of_list Hs))
-  | _ => H
+     eval vm_compute in
+       (IAnon (match Hs with
+         | [] => 1
+         | _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
+         end))%positive
+  | _ => constr:(IAnon 1)
   end.
-Ltac iFresh := iFresh' "~".
 
 Ltac iMissingHyps Hs :=
   let Δ :=
@@ -83,7 +87,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
 
 Local Inductive esel_pat :=
   | ESelPure
-  | ESelName : bool → string → esel_pat.
+  | ESelIdent : bool → ident → esel_pat.
 
 Ltac iElaborateSelPat pat :=
   let rec go pat Δ Hs :=
@@ -93,14 +97,14 @@ Ltac iElaborateSelPat pat :=
     | SelPersistent :: ?pat =>
        let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
        let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
-       go pat Δ' ((ESelName true <$> Hs') ++ Hs)
+       go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
     | SelSpatial :: ?pat =>
        let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
        let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
-       go pat Δ' ((ESelName false <$> Hs') ++ Hs)
-    | SelName ?H :: ?pat =>
+       go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
+    | SelIdent ?H :: ?pat =>
        lazymatch eval env_cbv in (envs_lookup_delete H Δ) with
-       | Some (?p,_,?Δ') => go pat Δ' (ESelName p H :: Hs)
+       | Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
        | None => fail "iElaborateSelPat:" H "not found"
        end
     end in
@@ -109,14 +113,16 @@ Ltac iElaborateSelPat pat :=
     let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
   end.
 
+Local Ltac iClearHyp H :=
+  eapply tac_clear with _ H _ _; (* (i:=H) *)
+    [env_reflexivity || fail "iClear:" H "not found"|].
+
 Tactic Notation "iClear" constr(Hs) :=
   let rec go Hs :=
     lazymatch Hs with
     | [] => idtac
     | ESelPure :: ?Hs => clear; go Hs
-    | ESelName _ ?H :: ?Hs =>
-       eapply tac_clear with _ H _ _; (* (i:=H) *)
-         [env_reflexivity || fail "iClear:" H "not found"|go Hs]
+    | ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
     end in
   let Hs := iElaborateSelPat Hs in go Hs.
 
@@ -260,7 +266,7 @@ Tactic Notation "iFrame" constr(Hs) :=
     | SelPure :: ?Hs => iFrameAnyPure; go Hs
     | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
     | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
-    | SelName ?H :: ?Hs => iFrameHyp H; go Hs
+    | SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
     end
   in let Hs := sel_pat.parse Hs in go Hs.
 Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
@@ -406,7 +412,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
     | SForall :: ?pats =>
        idtac "the * specialization pattern is deprecated because it is applied implicitly";
        go H1 pats
-    | SName ?H2 :: ?pats =>
+    | SIdent ?H2 :: ?pats =>
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_reflexivity || fail "iSpecialize:" H2 "not found"
          |env_reflexivity || fail "iSpecialize:" H1 "not found"
@@ -486,12 +492,17 @@ defaults to [false] (i.e. spatial hypotheses are not preserved). *)