The Coq mailing list

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

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

Le mer. 7 sept. 2016 à 19:39, Jonathan Leivent <jonikelee AT gmail.com> a écrit :

I've been experimenting with ways to refer to things by their type
instead of by name.  One that seems obvious is using a very generic
typeclass for all definitions that aren't already Instances of some
other typeclass:


Class Witness (signature : Type) := witness : signature.

Then, for any Definition/Lemma of the form : "Lemma Foo : <quantifers>
-> T", I would instead define "Instance Foo : <quantifiers> -> Witness
T".  The proof just needs an extra "unfold Witness" at the beginning.
The definitions are still usable by name.  But, because they are now
instances, I can also look them up by type, as with "pose proof (witness
: T)".  A Generalize_Witness instance allows a single other instance to
be found by any of its possible generalizations:


Instance Generalize_Witness{A : Type}{B : A -> Type}(H : forall a,
Witness (B a)) : Witness (forall a, B a).
Proof.
   red. apply H.
Defined.


The question is - is there a down side to doing this for all
definitions?  Would I be slowing down instance resolution on non-Witness
classes as a result?  Also, might there be some way a definition can be
used such that an Instance in its place won't work as well?


-- Jonathan