Fix missing bound variable renaming in help

This bug was pointed out by Pierre Boutry
PatrickMassot · Apr 25, 2024 · 7efc519 · 7efc519
1 parent b356076
commit 7efc519
Show file tree

Hide file tree

Showing 3 changed files with 40 additions and 2 deletions.
diff --git a/Verbose/English/Help.lean b/Verbose/English/Help.lean
@@ -813,3 +813,21 @@ info: Help
 example : True := by
   help
   trivial
+
+/--
+info: Help
+• By h we get x_1 such that (hx_1 : f x_1 = y)
+-/
+#guard_msgs in
+example {X Y} (f : X → Y) (x : X) (y : Y) (h : ∃ x, f x = y) : True := by
+  help h
+  trivial
+
+/--
+info: Help
+• By h we get x_1 such that (x_1_dans : x_1 ∈ s) and (hx_1 : f x_1 = y)
+-/
+#guard_msgs in
+example {X Y} (f : X → Y) (s : Set X) (x : X) (y : Y) (h : ∃ x ∈ s, f x = y) : True := by
+  help h
+  trivial
diff --git a/Verbose/French/Help.lean b/Verbose/French/Help.lean
@@ -817,3 +817,21 @@ info: Aide
 example : True := by
   aide
   trivial
+
+/--
+info: Aide
+• Par h on obtient x_1 tel que (hx_1 : f x_1 = y)
+-/
+#guard_msgs in
+example {X Y} (f : X → Y) (x : X) (y : Y) (h : ∃ x, f x = y) : True := by
+  aide h
+  trivial
+
+/--
+info: Aide
+• Par h on obtient x_1 tel que (x_1_dans : x_1 ∈ s) et (hx_1 : f x_1 = y)
+-/
+#guard_msgs in
+example {X Y} (f : X → Y) (s : Set X) (x : X) (y : Y) (h : ∃ x ∈ s, f x = y) : True := by
+  aide h
+  trivial
diff --git a/Verbose/Tactics/Help.lean b/Verbose/Tactics/Help.lean
@@ -231,13 +231,14 @@ def helpExistsRel : HypHelpExt where
   run (goal : MVarId) (hyp : Name) (hypType : VExpr) : SuggestionM Unit := do
     if let .exist_rel _ var_name _typ rel rel_rhs propo := hypType then
     let y ← ppExpr rel_rhs
-    let pS ← propo.delab
     let name ← goal.getUnusedUserName var_name
     let nameS := mkIdent name
     let hS := mkIdent s!"h{name}"
     let ineqName := Name.mkSimple s!"{name}{symb_to_hyp rel rel_rhs}"
     let ineqIdent := mkIdent ineqName
     let ineqS ← mkRelStx name rel rel_rhs
+    withRenamedFVar var_name name do
+    let pS ← propo.delab
     helpExistRelSuggestion hyp s!"∃ {var_name}{rel}{y}, ..." nameS ineqIdent hS ineqS pS
 
 register_endpoint helpExistsSimpleSuggestion (hyp n hn : Name) (headDescr : String) (pS : Term) :
@@ -247,9 +248,10 @@ register_endpoint helpExistsSimpleSuggestion (hyp n hn : Name) (headDescr : Stri
 def helpExistsSimple : HypHelpExt where
   run (goal : MVarId) (hyp : Name) (hypType : VExpr) : SuggestionM Unit := do
     if let .exist_simple _ var_name _typ propo := hypType then
-    let pS ← propo.delab
     let n ← goal.getUnusedUserName var_name
     let hn := Name.mkSimple s!"h{n}"
+    withRenamedFVar var_name n do
+    let pS ← propo.delab
     let headDescr := s!"∃ {var_name}, ..."
     helpExistsSimpleSuggestion hyp n hn headDescr pS