The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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