From 7cfa82f6dbb7d9e34adbf7837e65e001053ec336 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 22 Jul 2020 18:55:25 +0200
Subject: [PATCH] Set default name for unnamed binders to H

Fixes #337.
---
 tests/proofmode.ref             | 13 +++++++++++++
 tests/proofmode.v               | 12 ++++++++++++
 theories/proofmode/ident_name.v |  7 +++++--
 3 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3af7a37cc..8ddfcb423 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -94,6 +94,19 @@ Tactic failure: iExistDestruct: cannot destruct P.
   --------------------------------------â–¡
   P
   
+"test_iDestruct_exists_anonymous"
+     : string
+1 subgoal
+  
+  PROP : bi
+  P : PROP
+  Φ : nat → PROP
+  H : nat
+  ============================
+  "HΦ" : ∃ x : nat, Φ x
+  --------------------------------------∗
+  ∃ x : nat, Φ x
+  
 "test_iIntros_forall_pure"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 893a7e6a5..56aa97a8d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -184,6 +184,18 @@ Proof.
   iExists y0; auto.
 Qed.
 
+(* regression test for #337 *)
+Check "test_iDestruct_exists_anonymous".
+Lemma test_iDestruct_exists_anonymous P Φ :
+  (∃ _:nat, P) ∗ (∃ x:nat, Φ x) -∗ P ∗ ∃ x, Φ x.
+Proof.
+  iIntros "[HP HΦ]".
+  (* this should not use [x] as the default name for the unnamed binder *)
+  iDestruct "HP" as (?) "$". Show.
+  iDestruct "HΦ" as (x) "HΦ".
+  by iExists x.
+Qed.
+
 Definition an_exists P : PROP := (∃ (an_exists_name:nat), ▷^an_exists_name P)%I.
 
 (* should use the name from within [an_exists] *)
diff --git a/theories/proofmode/ident_name.v b/theories/proofmode/ident_name.v
index c5886dcb0..c79e67e81 100644
--- a/theories/proofmode/ident_name.v
+++ b/theories/proofmode/ident_name.v
@@ -27,8 +27,11 @@ Arguments as_ident_name {A B f} name : assert.
 
 Ltac solve_as_ident_name :=
   lazymatch goal with
-  | |- AsIdentName (λ x, _) _ =>
-    let name := to_ident_name x in
+  (* The [H] here becomes the default name if the binder is anonymous. We use
+     [H] with the idea that an unnamed and unused binder is likely to be a
+     proposition. *)
+  | |- AsIdentName (λ H, _) _ =>
+    let name := to_ident_name H in
     notypeclasses refine (as_ident_name name)
   | _ => notypeclasses refine (to_ident_name __unknown)
   end.
-- 
GitLab