The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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.

I have another tactic which is also based on open_constrs:

Ltac head_is term h :=
  tryif unify term h then idtac else
  lazymatch term with
  | ?F _ => head_is F h
  end.

Tactic Notation "onhead" open_constr(term) tactic3(tac) :=
  multimatch goal with
  | H :?T |- _ => head_is T term; tac H
  end.

Lemma example_onhead :
  forall t e1 e2 ,
  is_foo e1 t -> is_foo e2 t -> is_foo e1 t.
Proof.
  intros.
  onhead is_foo fun H => exact H.
Qed.

Hence, "onhead" allows one to just mention some head prefix of the type 
of the hyp one wants.  It is not quite as nice syntactically due to 
often needing the "fun H => ..." wrapper.

I think using evars as patterns is a bit heavy-handed, so IMHO it would 
be nice to have a way to represent patterns and pattern variables 
directly.  For example, unmatched evars leave dangling open subgoals.  I 
commented about this on PMP's new Ltac2 proposal.

-- Jonathan

> Le jeu. 8 sept. 2016 à 15:36, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  a
> écrit :
>
> > On 09/08/2016 07:38 AM, Théo Zimmermann wrote:
> > > You might be interested by Pierre-Évariste's, still experimental,
> > > "cortouche" plugin:
> > > https://github.com/pedagand/cortouche
> > > So far it only looks for witnesses in the proof environment though, so it
> > > is not exactly the same as what you are proposing.
> > >
> > > Théo
> > It is possible to almost duplicate the functionality in Cortouche's
> > readme using just 2 instance-free typeclasses and 2 hints:
> >
> > Class Hyp (T : Type) := hyp : T.
> > Hint Extern 10 (Hyp _) => exactly_once multimatch goal with H : _ |- _
> > => exact H end : typeclass_instances.
> > Class AHyp (T : Type) := ahyp : T.
> > Hint Extern 10 (AHyp _) => exactly_once multimatch goal with H : _ |- _
> > => eapply H end : typeclass_instances.
> >
> > Parameter typ: Type.
> > Parameter exp: Type.
> > Parameter is_foo: exp -> typ -> Prop.
> >
> > Lemma example:
> >     forall t e1 e2 ,
> >       is_foo e1 t -> is_foo e2 t -> is_foo e1 t.
> > Proof.
> >     intros.
> >     exact (hyp: is_foo e1 t).
> > Qed.
> >
> > Lemma example_patt:
> >     forall t e1 e2 ,
> >       is_foo e1 t -> is_foo e2 t -> is_foo e1 t.
> > Proof.
> >     intros.
> >     exact (hyp: is_foo e1 _).
> > Qed.
> >
> > Lemma example_too_general:
> >     forall t e1 e2 ,
> >       is_foo e1 t -> is_foo e2 t -> is_foo e1 t.
> > Proof.
> >     intros.
> >     exact (hyp: is_foo _ _).
> > Abort.
> >
> > Lemma example_too_many_successes :
> >     forall t e1 e2 ,
> >     is_foo e1 t -> is_foo e2 t -> exists e, is_foo e t.
> > Proof.
> >     intros.
> >     eexists.
> >     Fail exact (hyp: is_foo _ _). (*Error: This tactic has more than one
> > success.*)
> >     exact (hyp: is_foo e1 _).
> > Qed.
> >
> > Lemma example_concl:
> >     (forall e t, is_foo e t) -> forall e t, is_foo e t.
> > Proof.
> >     intros.
> >     Fail exact (hyp: is_foo _ _).
> >     exact (ahyp: is_foo _ _).
> > Qed.
> >
> >
> > Note that I could not get is_foo _ _ to fail in example_too_general -
> > but that is because it isn't too general based on successes, but is
> > based on matching.  In terms of successes, there is only one possible
> > success, which is is_foo e1 t.  I added example_too_many_successes to
> > show that multiple successes can be made to fail (due to the
> > "exactly_one multimatch" combo in the hints).
> >
> > -- Jonathan