The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have often found that [appcontext] is a useful tool to blow holes through the abstraction of Ltac:

Goal forall T P, (exists old : T,  P old) /\ True.
intros T P.                
match goal with            
  | [ |- ?A /\ True ]      
    => match A with        
         | appcontext G[P] 
           => let G' := context G[fun x => P x /\ True] in
              assert G'    
       end                 
end.

Here's a slightly more general version of the same tactic:

Goal forall T P, (exists old : T,  P old) /\ True.
intros T P.                
match goal with            
  | [ |- ?A /\ True ]      
    => match A with        
         | @ex ?T ?P       
           => match A with 
                | appcontext G[P]
                  => let G' := context G[fun x => P x /\ True] in
                     assert G'
              end          
       end                 
end.

I suspect the reason for your troubles is that 'y' has two names, 'y' and 'old', and which name is used depends on where 'y' occurs in the _expression_.  I'll leave it to someone more familiar with the coq source code to explain which OCaml methods correspond to which names, and where each gets used.  (Or I might go source-diving myself, later.)

-Jason

On Tue, Jun 11, 2013 at 1:40 PM, Andrew W. Appel <appel AT cs.princeton.edu> wrote:

(* 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.
*)