The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/23/2014 12:14 PM, Jonathan wrote:
> Oh - wait - context can be used for that:
>
>    Ltac name_evars :=
>       repeat match goal with |- context[?V] => is_evar V; set V end.
>
>
> Hey, I like that!  But now one has a bunch of hypotheses each with an 
> evar as their value.  Nicer, since now instantiate's funky numbering 
> is no longer needed.  But, is there a way to fill in the values of 
> those evars without using instantiate?  Hmmm:
>
>    Ltac assign name term :=
>       match goal with name := ?V : _ |- _ => unify V term end.
>
>
> Cool!  These tactics need to be dressed up a bit using Tactic 
> Notation.  But, now I think I can deal with the possible deprecation 
> of instantiate.
>
> -- Jonathan

I cleaned those tactics up and added a few more - attached.

-- Jonathan

Ltac name_evars id := 
  repeat match goal with |- context[?V] => is_evar V; let H := fresh id in set (H:=V) in * end.

Ltac name_evars_in hyp id :=
  repeat match type of hyp with 
             context[?V] => 
             is_evar V; 
               let H:=fresh id in set (H:=V) in *; move H at bottom end.

Ltac name_evars_of type id :=
  repeat match goal with 
             |- context[?V] =>
             is_evar V; match type of V with type => let H:= fresh id in set (H:=V) in * end end.

Ltac name_evars_in_of hyp type id :=
  repeat match type of hyp with
             context[?V] => 
             is_evar V; match type of V with
                            type => 
                            let H:=fresh id in 
                            set (H:=V) in *; move H at bottom end end.

Ltac assign name term :=
  match goal with H := ?V : _ |- _ => match H with name => unify V term end end.

Ltac assign_any term :=
  match goal with H := ?V : _ |- _ => is_evar V; unify V term end.

Section Tests.

  Variable Foo : nat -> bool -> nat -> list nat -> Prop.
  
  Goal exists n b1 b2 m l, Foo n b1 m l -> Foo m (negb b2) n l.
  repeat eexists.
  intro H.
  name_evars_in_of H nat i0.
  name_evars_of bool b.
  name_evars_in H x0.
  assign b true.
  assign_any (0::1::2::nil)%list.
  assign i0 42.
  assign i1 13.
  assign x0 (negb b).
  Abort.

End Tests.