Use user-supplied names in iIntros

Preserve identifiers in binders where possible, analogous to the support
for destructing existentials in !479.

Fixes #336.

CHANGELOG.md

@@ -14,6 +14,11 @@ lemma.
   yourself, since the typeclass now forwards names. If your instance transforms
   one `IntoExist` into another, you can generally just forward the name from the
   premise.
+* The proofmode also preserves user-supplied names in `iIntros`, for example
+  with `iIntros (?)` and `iIntros "%"`, as described for destructing
+  existentials above. As part of this change, it now uses a base name of `H` for
+  pure facts rather than the previous default of `a`. This also requires some
+  changes if you were implementing `FromForall`, in order to forward names.
 
 ## Iris 3.3.0 (released 2020-07-15)
 

tests/proofmode.ref

@@ -100,10 +100,23 @@ Tactic failure: iExistDestruct: cannot destruct P.
   
   PROP : bi
   Ψ : nat → PROP
-  a : nat
+  x : nat
+  ============================
+  --------------------------------------∗
+  Ψ x → Ψ x
+  
+"test_iIntros_pure_names"
+     : string
+1 subgoal
+  
+  PROP : bi
+  H : True
+  P : PROP
+  x, y : nat
+  H0 : x = y
   ============================
   --------------------------------------∗
-  Ψ a → Ψ a
+  P -∗ P
   
 The command has indeed failed with message:
 No applicable tactic.

tests/proofmode.v

@@ -219,6 +219,32 @@ Lemma test_very_fast_iIntros P :
   ∀ x y : nat, ⊢ ⌜ x = y ⌝ → P -∗ P.
 Proof. by iIntros. Qed.
 
+Lemma test_iIntros_automatic_name (Φ: nat → PROP) :
+  ∀ y, Φ y -∗ ∃ x, Φ x.
+Proof. iIntros (?) "H". by iExists y. Qed.
+
+Lemma test_iIntros_automatic_name_proofmode_intro (Φ: nat → PROP) :
+  ∀ y, Φ y -∗ ∃ x, Φ x.
+Proof. iIntros "% H". by iExists y. Qed.
+
+(* even an object-level forall should get the right name *)
+Lemma test_iIntros_object_forall P :
+  P -∗ ∀ (y:unit), P.
+Proof. iIntros "H". iIntros (?). destruct y. iAssumption. Qed.
+
+Lemma test_iIntros_object_proofmode_intro (Φ: nat → PROP) :
+  ⊢ ∀ y, Φ y -∗ ∃ x, Φ x.
+Proof. iIntros "% H". by iExists y. Qed.
+
+Check "test_iIntros_pure_names".
+Lemma test_iIntros_pure_names (H:True) P :
+  ∀ x y : nat, ⊢ ⌜ x = y ⌝ → P -∗ P.
+Proof.
+  iIntros (???).
+  (* the pure hypothesis should get a sensible [H0] as its name *)
+  Show. auto.
+Qed.
+
 Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x ⌝)%I.
 Lemma test_iIntros_tc_opaque : ⊢ tc_opaque_test.
 Proof. by iIntros (x). Qed.

theories/proofmode/class_instances.v

@@ -874,29 +874,31 @@ Proof.
 Qed.
 
 (** FromForall *)
-Global Instance from_forall_forall {A} (Φ : A → PROP) :
-  FromForall (∀ x, Φ x) Φ.
+Global Instance from_forall_forall {A} (Φ : A → PROP) name :
+  AsIdentName Φ name → FromForall (bi_forall Φ) Φ name.
 Proof. by rewrite /FromForall. Qed.
-Global Instance from_forall_tforall {TT : tele} (Φ : TT → PROP) :
-  FromForall (∀.. x, Φ x) Φ.
+Global Instance from_forall_tforall {TT : tele} (Φ : TT → PROP) name :
+  AsIdentName Φ name → FromForall (bi_tforall Φ) Φ name.
 Proof. by rewrite /FromForall bi_tforall_forall. Qed.
-Global Instance from_forall_pure {A} (φ : A → Prop) :
-  @FromForall PROP A ⌜∀ a : A, φ a⌝ (λ a, ⌜ φ a ⌝)%I.
+Global Instance from_forall_pure {A} (φ : A → Prop) name :
+  AsIdentName φ name → @FromForall PROP A ⌜∀ a : A, φ a⌝ (λ a, ⌜ φ a ⌝)%I name.
 Proof. by rewrite /FromForall pure_forall. Qed.
-Global Instance from_tforall_pure {TT : tele} (φ : TT → Prop) :
-  @FromForall PROP TT ⌜∀.. x : TT, φ x⌝ (λ x, ⌜ φ x ⌝)%I.
+Global Instance from_tforall_pure {TT : tele} (φ : TT → Prop) name :
+  AsIdentName φ name → @FromForall PROP TT ⌜tforall φ⌝ (λ x, ⌜ φ x ⌝)%I name.
 Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
+
+(* [H] is the default name for the [φ] hypothesis, in the following three instances *)
 Global Instance from_forall_pure_not (φ : Prop) :
-  @FromForall PROP φ ⌜¬ φ⌝ (λ a : φ, False)%I.
+  @FromForall PROP φ ⌜¬ φ⌝ (λ _ : φ, False)%I (to_ident_name H).
 Proof. by rewrite /FromForall pure_forall. Qed.
 Global Instance from_forall_impl_pure P Q φ :
-  IntoPureT P φ → FromForall (P → Q) (λ _ : φ, Q).
+  IntoPureT P φ → FromForall (P → Q) (λ _ : φ, Q) (to_ident_name H).
 Proof.
   intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
 Qed.
 Global Instance from_forall_wand_pure P Q φ :
   IntoPureT P φ → TCOr (Affine P) (Absorbing Q) →
-  FromForall (P -∗ Q) (λ _ : φ, Q)%I.
+  FromForall (P -∗ Q) (λ _ : φ, Q)%I (to_ident_name H).
 Proof.
   intros (φ'&->&?) [|]; rewrite /FromForall; apply wand_intro_r.
   - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
@@ -904,14 +906,14 @@ Proof.
   - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
 Qed.
 
-Global Instance from_forall_intuitionistically `{BiAffine PROP} {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (□ P) (λ a, □ (Φ a))%I.
+Global Instance from_forall_intuitionistically `{BiAffine PROP} {A} P (Φ : A → PROP) name :
+  FromForall P Φ name → FromForall (□ P) (λ a, □ (Φ a))%I name.
 Proof.
   rewrite /FromForall=> <-. setoid_rewrite intuitionistically_into_persistently.
   by rewrite persistently_forall.
 Qed.
-Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (<pers> P) (λ a, <pers> (Φ a))%I.
+Global Instance from_forall_persistently {A} P (Φ : A → PROP) name :
+  FromForall P Φ name → FromForall (<pers> P) (λ a, <pers> (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
 
 (** ElimModal *)

theories/proofmode/class_instances_embedding.v

@@ -129,8 +129,8 @@ Global Instance into_forall_embed {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
 Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
 
-Global Instance from_forall_embed {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Global Instance from_forall_embed {A} P (Φ : A → PROP) name :
+  FromForall P Φ name → FromForall ⎡P⎤ (λ a, ⎡Φ a⎤%I) name.
 Proof. by rewrite /FromForall -embed_forall => <-. Qed.
 
 Global Instance into_inv_embed P N : IntoInv P N → IntoInv ⎡P⎤ N := {}.

theories/proofmode/class_instances_later.v

@@ -185,16 +185,16 @@ Global Instance into_forall_except_0 {A} P (Φ : A → PROP) :
 Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
 
 (** FromForall *)
-Global Instance from_forall_later {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I.
+Global Instance from_forall_later {A} P (Φ : A → PROP) name :
+  FromForall P Φ name → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
 
-Global Instance from_forall_laterN {A} P (Φ : A → PROP) n :
-      FromForall P Φ → FromForall (▷^n P)%I (λ a, ▷^n (Φ a))%I.
+Global Instance from_forall_laterN {A} P (Φ : A → PROP) n name :
+      FromForall P Φ name → FromForall (▷^n P)%I (λ a, ▷^n (Φ a))%I name.
 Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed.
 
-Global Instance from_forall_except_0 {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I.
+Global Instance from_forall_except_0 {A} P (Φ : A → PROP) name :
+  FromForall P Φ name → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
 
 (** IsExcept0 *)

theories/proofmode/class_instances_plainly.v

@@ -83,8 +83,8 @@ Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 
-Global Instance from_forall_plainly {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (■ P)%I (λ a, ■ (Φ a))%I.
+Global Instance from_forall_plainly {A} P (Φ : A → PROP) name :
+  FromForall P Φ name → FromForall (■ P)%I (λ a, ■ (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 
 Global Instance from_modal_plainly P :

theories/proofmode/class_instances_updates.v

@@ -96,20 +96,20 @@ Proof.
 Qed.
 
 Global Instance from_forall_fupd
-    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
+    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) name :
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
-  FromForall P Φ → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I.
+  FromForall P Φ name → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I name.
 Proof.
   rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
 Qed.
 Global Instance from_forall_step_fupd
-    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
+    `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) name :
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
-  FromForall P Φ → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1}[E2]▷=> P)%I (λ a, |={E1}[E2]▷=> (Φ a))%I.
+  FromForall P Φ name → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1}[E2]▷=> P)%I (λ a, |={E1}[E2]▷=> (Φ a))%I name.
 Proof.
   rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
 Qed.

theories/proofmode/classes.v

@@ -216,11 +216,11 @@ Arguments IntoForall {_ _} _%I _%I : simpl never.
 Arguments into_forall {_ _} _%I _%I {_}.
 Hint Mode IntoForall + - ! - : typeclass_instances.
 
-Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
+Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
   from_forall : (∀ x, Φ x) ⊢ P.
-Arguments FromForall {_ _} _%I _%I : simpl never.
-Arguments from_forall {_ _} _%I _%I {_}.
-Hint Mode FromForall + - ! - : typeclass_instances.
+Arguments FromForall {_ _} _%I _%I _ : simpl never.
+Arguments from_forall {_ _} _%I _%I _ {_}.
+Hint Mode FromForall + - ! - - : typeclass_instances.
 
 Class IsExcept0 {PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
 Arguments IsExcept0 {_} _%I : simpl never.
@@ -619,8 +619,8 @@ Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   FromExist P Φ → FromExist (tc_opaque P) Φ := id.
 Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
   IntoExist P Φ name → IntoExist (tc_opaque P) Φ name := id.
-Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
-  FromForall P Φ → FromForall (tc_opaque P) Φ := id.
+Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
+  FromForall P Φ name → FromForall (tc_opaque P) Φ name := id.
 Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
 Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}

theories/proofmode/coq_tactics.v

@@ -693,9 +693,11 @@ Proof.
 Qed.
 
 (** * Forall *)
-Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q :
-  FromForall Q Φ →
-  (∀ a, envs_entails Δ (Φ a)) →
+Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q name :
+  FromForall Q Φ name →
+  ( (* see [tac_exist_destruct] for an explanation of this let binding *)
+   let _ := name in
+   ∀ a, envs_entails Δ (Φ a)) →
   envs_entails Δ Q.
 Proof. rewrite envs_entails_eq /FromForall=> <-. apply forall_intro. Qed.
 

theories/proofmode/ltac_tactics.v

@@ -474,7 +474,12 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
         [iSolveTC ||
          let P := match goal with |- FromForall ?P _ => P end in
          fail "iIntro: cannot turn" P "into a universal quantifier"
-        |pm_prettify; intros x
+        |let name := lazymatch goal with
+                     | |- let _ := (λ name, _) in _ => name
+                     end in
+         pm_prettify;
+         let y := fresh name in
+         intros y; revert y; intros x
          (* subgoal *)]
     end).
 

theories/proofmode/monpred.v

@@ -254,14 +254,14 @@ Proof. done. Qed.
 
 Global Instance from_forall_monPred_at_wand P Q (Φ Ψ : I → PROP) i :
   (∀ j, MakeMonPredAt j P (Φ j)) → (∀ j, MakeMonPredAt j Q (Ψ j)) →
-  FromForall ((P -∗ Q) i)%I (λ j, ⌜i ⊑ j⌝ → Φ j -∗ Ψ j)%I.
+  FromForall ((P -∗ Q) i)%I (λ j, ⌜i ⊑ j⌝ → Φ j -∗ Ψ j)%I (to_ident_name idx).
 Proof.
   rewrite /FromForall /MakeMonPredAt monPred_at_wand=> H1 H2. do 2 f_equiv.
   by rewrite H1 H2.
 Qed.
 Global Instance from_forall_monPred_at_impl P Q (Φ Ψ : I → PROP) i :
   (∀ j, MakeMonPredAt j P (Φ j)) → (∀ j, MakeMonPredAt j Q (Ψ j)) →
-  FromForall ((P → Q) i)%I (λ j, ⌜i ⊑ j⌝ → Φ j → Ψ j)%I.
+  FromForall ((P → Q) i)%I (λ j, ⌜i ⊑ j⌝ → Φ j → Ψ j)%I (to_ident_name idx).
 Proof.
   rewrite /FromForall /MakeMonPredAt monPred_at_impl=> H1 H2. do 2 f_equiv.
   by rewrite H1 H2 bi.pure_impl_forall.
@@ -321,7 +321,7 @@ Proof.
 Qed.
 
 Global Instance from_forall_monPred_at_objectively P (Φ : I → PROP) i :
-  (∀ i, MakeMonPredAt i P (Φ i)) → FromForall ((<obj> P) i)%I Φ.
+  (∀ i, MakeMonPredAt i P (Φ i)) → FromForall ((<obj> P) i)%I Φ (to_ident_name idx).
 Proof.
   rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
 Qed.
@@ -345,8 +345,8 @@ Proof.
   rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
 Qed.
 
-Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
-  FromForall P Φ → (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → FromForall (P i) Ψ.
+Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) name (Ψ : A → PROP) i :
+  FromForall P Φ name → (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → FromForall (P i) Ψ name.
 Proof.
   rewrite /FromForall /MakeMonPredAt=><- H. setoid_rewrite <- H.
   by rewrite monPred_at_forall.
@@ -460,7 +460,7 @@ Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
 
 Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ :
   (∀ i, MakeMonPredAt i P (Φ i)) →
-  FromForall ((■ P) i) (λ j, ■ (Φ j))%I.
+  FromForall ((■ P) i) (λ j, ■ (Φ j))%I (to_ident_name idx).
 Proof.
   rewrite /FromForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly.
   by setoid_rewrite HPΦ.