The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 7 Nov 2013 00:55:46 +0200,
Ilmārs Cīrulis 
<ilmars.cirulis AT gmail.com>
 a écrit :

> I made my first tries in using Classes and Equivalences (Setoids,
> maybe). It can be seen at the same GitHub repository in the file
> matrices.v. But I have hole in the vect_fold_Proper, which I have
> made Admitted. Can anyone help to fill it, please?
> 
> Also, is there any hints how to use such Setoids more effectively or
> idiomatic?
> (I'm already trying first advanced rewrites, but they're not yet on
> Github.)

I tried to read what you did, but it was way too complex for me.
First, why do you use "Fix (fin_lt_wf len)" for vect_fold where you
could do a simple induction with the raw "fix" tactic on the index you
are using, that is something like:
"fix vect_fold index : index <= len -> … :=
 match index as i return i <= len -> … with
 | O => fun (H : O <= len) => …
 | S i => fun (H : S i <= len) => let rec := vect_fold i _(*i<=len*) …
                                  in …
 end"
Then I am used to "…_fold : ∀ A B (f : A → B → B) (b : B), … A -> B"
but your definition returns a "… A" which I do not really see what it
represents.

By adjusting with my first point, vect_fold_Proper should be easier to
deal with, I think.
> 
> 
> On Tue, Nov 5, 2013 at 11:24 PM, Ilmārs Cīrulis
> <ilmars.cirulis AT gmail.com>wrote:
> 
> > Thanks to all for great hints. :) (And apologies for late answer.)
> >
> > So I removed nz_type and made fin as this Definition fin l := {n |
> > n <= l}, ignoring the idea of empty vectors.
> > Also I proved that Theorem fin_t1 {l} (n m: fin l): n = m <->
> > projT1 n = projT1 m. It made everything much easier (thanks to
> > Cedric Auger).
> >
> >