The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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