The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

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

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