The Coq mailing list

["Andrew W. Appel" <appel AT CS.Princeton.EDU>]

(* This little Coq development asks, "can an Ltac program choose the 
name of
 a bound variable when building a lambda?"
 If you know a way, please tell me.  If you know it is not possible, 
tell me that too.
 I don't subscribe to coq-club, so please cc me on any e-mail.
 Sincerely,  Andrew Appel.
*)

Axiom ex_and:  forall A (F: A -> Prop) Q, (ex F /\ Q) = (ex (fun x => F 
x /\ Q)).
Parameter P: nat -> Prop.

Goal  (exists old,  P old) /\ True.
  rewrite ex_and.
(* PROBLEM: the goal is now,  exists x : nat, P x /\ True
 when I want it to be,     exists old : nat, P old /\ True
*)
Abort.

Goal  (exists old,  P old) /\ True.
 replace ((exists old : nat, P old) /\ True)
      with (exists old : nat, P old /\ True)
       by (symmetry; apply ex_and).
(* NOTE: the goal is now,    exists old : nat, P old /\ True
  This demonstrates that in some circumstances
  the user CAN choose the name of the bound variable.
*)
Abort.

Goal  (exists old,  P old) /\ True.
match goal with |- (ex (fun y => _)) /\ _ =>
   pose (y := False)
end.
(* The goal is now,
  old := False : Prop
  ______________________________________(1/1)
  (exists old0 : nat, P old0) /\ True

 This demonstrates that the tactic system CAN
 grab the name of a bound variable from a term.
*)
Abort.

Goal  (exists old,  P old) /\ True.
match goal with |- ex ?A /\ _ =>
    match A with (fun y => _) =>
       assert (ex (fun y => A y /\ True))
    end
end.
(* The goal is now,  exists y : nat, P y /\ True.
 This demonstrates that the user cannot choose the "new"
  bound variable y to match the name of the old one.
*)
Abort.

Goal  (exists old,  P old) /\ True.
match goal with |- ex ?A /\ _ =>
    match A with (fun y => _) =>
       let y' := fresh y in
       assert (ex (fun y' => A y' /\ True))
    end
end.
(* The goal is now,  exists y' : nat, P y' /\ True.
 This demonstrates that the [fresh] tactic is not useful here.
*)
Abort.

(* CHALLENGE:  write an Ltac that, for any name n,
  rewrites a goal of the form
  (exists n, P n) /\ True    into     (exists n, P n /\ True)
such that the bound variable [n] in the right-hand side
is the same as the name matched on the left-hand side.
*)