The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

In the Iris library, we have some type classes that have a boolean 
premise (for example, an expression being physically atomic, which we 
can easily solve by computation).

If we want to handle this the way you suggested, we have to declare 
Is_true : bool -> Prop as an Existing Class, which causes other 
problems. For example, when having normal Is_true premises of other 
lemmas, the ssreflect rewrite tactic will fail (because it cannot find a 
type class instance) instead of generating a goal.

Enrico's suggestion could work, and sounds better than our current 
workaround in Ralf's initial message in this thread.

On 11/16/2016 02:47 PM, Matthieu Sozeau wrote:
> I'm curious about the actual use cases of using such non-class premises
> around, I'd be happy to hear about others. We can still go back on this
> cleanup.
> -- Matthieu
>
> On Wed, Nov 16, 2016 at 2:40 PM Matthieu Sozeau 
> <mattam AT mattam.org
> <mailto:mattam AT mattam.org>>
>  wrote:
>
>     The goal is to be able to recognize what is and what isn't a class
>     goal from its type.
>     When doing resolution during refinement we need that information.
>     One can also argue that if you put Hint Extern (_ = _) =>
>     reflexivity : typeclass_instances
>     in your file then you can expect Definition foo : 0 = 0 := _. to
>     typecheck.
>     -- Matthieu
>
>
>     On Wed, Nov 16, 2016 at 2:33 PM Enrico Tassi 
> <enrico.tassi AT inria.fr
>     
> <mailto:enrico.tassi AT inria.fr>>
>  wrote:
>
>         On Wed, Nov 16, 2016 at 01:23:04PM +0000, Matthieu Sozeau wrote:
>         > This is a deliberate change to avoid "wrong" instances which
>         generate
>         > non-class goals from polluting search.
>         > You just need to declare the head as a class using Existing
>         Class eq for
>         > example here, because you're really
>         > treating it as a class. Sorry for not updating the CHANGES
>         yet, the refman
>         > has been updated though.
>
>         What you propose seems a bit too drastic, Existing Class marks
>         Eq as class "forever".  A lighter work around could be the following
>
>           Class Foo (x : nat).
>           Class TCPremise (P : Prop).
>           Instance foo x : TCPremise (x = 2) -> Foo x.
>           Hint Extern 0 (TCPremise (_ = _)) => reflexivity :
>         typeclass_instances.
>
>         But frankly the use case of Ralf seems reasonable, and the
>         contortion
>         above pretty ugly.
>
>         Can you explain what you mean by "wrong" instances, exactly?
>
>         Best,
>         --
>         Enrico Tassi