The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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