The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/24/2014 03:59 PM, Arnaud Spiwack wrote:
> > Interestingly, the IList code appears to work without the
> > -impredicative-set flag.  Are you sure it needs it?
>
> Yes. You get almost no property without impredicativity (the first version
> I sent was a bit incorrect by the way, the version in the file is better).
> Basically, you don't have the recursor (only fold_right, which is trivial)
> nor induction.

Is it strange at all then that I can get IList.v through the type 
checker without using -impredicative-set, including the recursor and 
induction?

> I think "typeclasses eauto" behaves better than eauto (it is implemented
> quite the same way as +) and it's in v8.4. "typeclasses eauto with core"
> should be, I think, a better version of "solve[eauto]".

I will try that!

> Here goes the proof of injectivity. It's not trivial.

Thanks again!  I can now prove sortedr and sortedl - which provide 
evidence that these ILists retain enough of the structure of lists to 
remain useful.  I haven't been able to make the IList versions of these 
proofs as clear as the list versions - but that's work for another 
time.  Now I'll try proving the rest of the sorted lemmas, then see if 
that, in combination with "typeclasses eauto with core", can make doing 
the Red/Black tree proofs easier.

-- Jonathan