The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/30/2016 12:33 PM, Jason Gross wrote:
> The issue with axioms sounds like a bug.  Is it present in 8.4?  In any
> case, you should report it in the bug tracker.

I don't have easy access to 8.4.  I will submit to bugzilla shortly.  I 
agree that an Axiom should be treated differently from a 
Variable/Hypothesis/Parameter - since Axiom, which is used rarely, says 
it will never be proved, while the others are much more common and 
merely postpone the need for proof.  But I still think it is weird that 
these other declarations without proofs automagically become instances 
of Existing Class types, while definitions - declarations with proofs - 
don't.  I can understand how hypotheses in a local context of a proof 
benefit from becoming instances automatically - but in those command 
cases, one always has the opportunity to explicitly add them with 
Existing Instance, so the automatic aspect there is just a small 
convenience, right?

I also noticed that local definitions via Section Lets don't become 
automatic instances, but local definitions in a proof context do.  A 
bug?  Or just idiosyncratic?

> [Local Existing Class] should be requested on the bug tracker with this
> example about variables.

That, too.  Although, maybe it should mirror Instances, which are local 
until declared Global?  The whole Local/Global/default thing is a bit of 
a mess, isn't it?  Compatibility is a b!tch.

> Does creating a typeclass hint at level 0 that wraps all hypotheses for you
> work?  (Does it fire before assumptions?  Does it fire before assumptions
> if you make it a local hint extern and stick it after all the variables?)

I tried a few such things.  Seems to me that level 0 hints aren't so 
special as to trigger resolution in more cases.  Are they supposed to 
be?  Again, I don't know if this is documented (probably not), but it 
appears that holes only trigger automatic resolution when the type of 
the hole is a declared Class, regardless of whether there are hints for 
that type at whatever level, 0 or otherwise.  Of course, once you're in 
the midst of resolution, new holes trigger hints just fine.  It's 
starting the process that appears confined to holes with declared Class 
types, or explicitly calling typeclasses eauto.  Also, the exact type of 
the hole has to be declared a class - not something convertible, even if 
declared Typeclasses Transparent.

-- Jonathan

> On Thu, Jun 30, 2016, 8:28 AM Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
>
> > On 06/29/2016 10:06 PM, Jonathan Leivent wrote:
> > > On 06/29/2016 01:05 PM, Jonathan Leivent wrote:
> > > > On 06/29/2016 12:38 PM, Matthieu Sozeau wrote:
> > > > > Hi Jonathan,
> > > > >
> > > > >     short answer is not currently. I would advise to make an
> > > > > abbreviation
> > > > > class eqC instead. The fact that local hypotheses of
> > > > > typeclass type are automatically considered for resolution is a
> > > > > feature. It
> > > > > could be an option of individual class declarations
> > > > > to not do that: only explicit Instances/Existing Instances for that
> > > > > class
> > > > > would be considered. We'd certainly need to devise a
> > > > > way to declare when a local binder (in fun (x : C foo) y => t) or a
> > > > > goal
> > > > > hypothesis (e.g. after intro H) should be considered though.
> > > > > Best,
> > > > > -- Matthieu
> > > > Thanks, Matthieu.
> > > >
> > > > What do you mean by an "abbreviation class eqC"?
> > > Here's a guess - instead of "Existing Class eq", I tried this:
> > >
> > > Class eqC {T}(a b : T) := equals : eq a b.
> > > Hint Resolve equals : typeclass_instances.
> > >
> > > with some specific Instances of eqC.
> > >
> > > However, this seems to require the explicit use of "typeclass eauto" -
> > > a hole of eq type won't get filled automatically, unlike what was
> > > happening in the Existing Class eq case (and happening too often). I
> > > would like to have the holes corresponding to the instances of eqC
> > > automatically filled in.  Is there some other way to do this?
> > >
> > > -- Jonathan
> > I found an ugly workaround: use Existing Class eq, and wrap any
> > subsequent hypothesis-like declaration that one does not want to be
> > considered an instance, then unwrap it in a definition.  This works
> > because complete definitions are not automatically considered instances
> > of the Existing Class - although, is that a bug?  Why aren't definitions
> > considered just declarations with proofs? Anyway, that's how it works
> > (though none of this is in the refman or typeclassestut, or anywhere I
> > googled) - so the workaround is:
> >
> > Existing Class eq.
> >
> > Variable T : Type.
> >
> > Structure NonInstance X := { unwrap_noninstance : X }.
> >
> > Axiom eqT_ : NonInstance (forall a b : T, a = b).
> > Definition eqT := unwrap_noninstance _ eqT_.
> >
> > Print HintDb typeclass_instances.
> >
> > (* neither eqT_ nor eqT appear:
> > Discriminated database
> > Unfoldable variable definitions: all
> > Unfoldable constant definitions: all
> > Cut: emp
> > For any goal ->
> > *)
> >
> > For Axioms, the NonInstance wrapper seems like a somewhat plausible
> > workaround, but it is probably too ugly for section Variables or module
> > Parameters, as one would have to wrap the corresponding actual parameters.
> >
> > I think I am stuck using "Existing Class eq" if the objective is to have
> > at least some eq holes automatically filled.  I tried limiting the scope
> > of Existing Class eq by wrapping it in a section or module - but that
> > doesn't limit it.  And "Local Existing Class" is not legal.  This makes
> > "Existing Class" a dangerous thing to use in a shared module, especially
> > on ubiquitous types like eq.
> >
> > How about this for an enhancement: allow the "Instance foo ... : T ...
> > := ..." syntax for T even when it is not previously declared a class.
> > Currently, this produces the error "T is not a declared type class".
> > This would make T into an existing class in a limited capacity, so that
> > it only accepts such explicitly declared instances.
> >
> > Although I also think "Local Existing Class" is worth adding as well.
> >
> > -- Jonathan