The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I believe having the pretyper "in the tactic monad" is indeed the right way to go for increased modularity and expressiveness. Things like what Jonathan is looking at are validating this view, though it would seem that among the many Coq programmers, he is the sole customer for this type of things. On the other hand, if it helps tactic makers, I don't think most users need to be concerned about this sort of things.

Of course, for Coq, this is probably unworkable. Pretyping is the most sensitive part of Coq and making everything subtly different in unpredictable ways is probably not worth the huge effort this would represent.

For the records, something along those lines have been done by Gaëtan Gilbert for Dedukti last year (code here: https://github.com/SkySkimmer/dedukti ) and could go as far as implementing the Sozeau&Zillani unification algorithm on top of a safe "kernel" which I found very impressive.

On 10 March 2016 at 02:05, Matthieu Sozeau <mattam AT mattam.org> wrote:

You are basically asking for putting the pretyper in the tactic monad

here, so that refine could return multiple successes, right? 

I think Arnaud had some ideas about this.

-- Matthieu

On Thu, Mar 10, 2016 at 1:08 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

I meant something more like this:

Class Foo : Type.

Instance foo_a : Foo.

Instance foo_b : Foo.

Goal True.
try (refine (let x := _ : Foo in _);
       let y := eval unfold x in x in idtac y; fail).

The above prints only foo_b, because that is the most recent definition
(since their costs are the same).  Using costs, one can make it so that
foo_a is printed, but not foo_b.  But, is there a way to have something
print both foo_a and foo_b?

-- Jonathan

On 03/09/2016 06:49 PM, Vadim Zaliva wrote:
> How about something like this:
>
> Instance Zmult_op : monoid_binop Z | 1 := Zmult.
> Instance Zplus_op : monoid_binop Z | 2 := Zplus.
>
> (from
> http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf
> )
>
> Vadim
>
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060
> Skype: vzaliva
>
>
> On Wed, Mar 9, 2016 at 1:38 PM, Jonathan Leivent <jonikelee AT gmail.com>
> wrote:
>
>> Suppose one has multiple typeclass instances of the same exact class (same
>> exact parameterization).  Is there a way to get to more of them other than
>> just the most recently declared one with the highest priority?
>>
>> -- Jonathan
>>
>>