The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/08/2016 11:19 AM, Jonathan Leivent wrote:
> On 09/08/2016 10:25 AM, Théo Zimmermann wrote:
> > Wow, I'm impressed!
> > Of course, when discussing this feature, we started by looking for a 
> > way to
> > implement it using Ltac.
> > We had come up with something that used tactics-in-terms but you 
> > could only
> > match on exact types, not on patterns.
> > At the last Coq coding sprint, when Pierre-Évariste started the
> > implementation, I don't think there was anyone there who could see 
> > that it
> > could be implemented without a line of OCaml.
> > Still, there is a limitation to what the code you provide can do: you
> > cannot use pattern variables ?x (like when using Search). We realized
> > recently that this is something that cortouche handles (no example of 
> > this
> > has been added yet, though).
>
> My understanding of what is going on with those underscores is that 
> the type expression in "exact (hyp : is_foo _ _)" is an open_constr.  
> Which means one can use something like ?x pattern variables - ?[X] 
> evar names.  However, one has to use ?[X] as the first occurrence of 
> X, then use "?X" as the others - and so one must know which part of 
> the pattern Coq will try to match first.

Here's an example of using evar names as non-linear patterns:

Parameter is_bar : nat -> nat -> Prop.

Lemma example_with_evar_names :
  is_bar 1 0 -> is_bar 1 1 -> is_bar 0 1 -> exists n1 n2, is_bar n1 n2 
/\ is_bar n1 n2.
Proof.
  intros.
  do 2 eexists; split.
  exact (hyp: is_bar ?[X] ?X). (*second subgoal is now is_bar 1 1*)
  exact (hyp: is_bar 1 1).
Qed.

-- Jonathan