The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Oh, my stupid. Of course, "fin"s are only one step away from natural numbers. It really was very easy, so big thanks! The "fix" tactic was kinda new for me even if I had seen it when using Print command (I suppose that I had to learn about it before learning general recursion :) ). 

What does the "as i return" part do if I may ask?

Now I made "vect_fold" more general according to your suggestion. 

Why so strange return type? Because at first it was made with type "fin len -> A", then I saw that is the same as "vect A len".

On Thu, Nov 7, 2013 at 4:49 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:

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).
> >
> >