The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> But, is there a way to have something print both foo_a and foo_b?

Axiom A : Type.

Existing Class A.

Axioms a a' : A.

Existing Instances a a'.

Class MultiA {x : A} := dummy : True.

Hint Extern 0 (@MultiA ?x) => idtac x; fail : typeclass_instances.

Goal True.

  try pose (_ : MultiA).

(* a'

a

a'

a

a'

a

a'

a *)

Not sure why there's so much duplication, but can you make this work?

On Wed, Mar 9, 2016 at 8:28 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 03/09/2016 08:15 PM, Jonathan Leivent wrote:

On 03/09/2016 08:05 PM, Matthieu Sozeau wrote:

You are basically asking for putting the pretyper in the tactic monad
here, so that refine could return multiple successes, right?

I wouldn't restrict it to "refine", if that's what you are implying.  Actually, I'm not sure what you're implying.:-[   So, maybe this will clarify my request:

Class Foo : Type := { value : nat }.

Instance foo_a : Foo := {value := 42}.

Instance foo_b : Foo := {value := 7}.

Goal value = 7.
reflexivity.
Qed.

Goal value = 42.
Fail reflexivity.

Could this second goal be provable as well?

No - I can see that won't ever work.  The implicit Foo argument of value is already filled in as foo_b.  OK - then I guess I'm really talking about this goal:

Goal exists f, @value f = 42.

in which case, making refine see multiple successes would work, via "refine (ex_intro _ _ _); reflexivity.".

Although, it would be interesting if the "Goal value = 42" were actually interpreted roughly as "Goal exists f, @value f = 42."  In other words, delaying the implicit arg somehow.

-- Jonathan