The Coq mailing list

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

Sorry for double post (to Cedric).

On Mon, Nov 25, 2013 at 10:33 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Is there any good example of standard way to define setoids with aim to use setoid rewrite, f_equiv and maybe something else too?

I'm doing it right now in such way:

- Definition of equivalence relation as instance of equivalence

- Definition of setoid using Build_Setoid

- Many instances of Proper for many functions

On Wed, Nov 13, 2013 at 5:58 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Thanks for long explanation, really!

Type fin len -> A is because it allows different "degrees of folding" - if you want use only first 3 elements, for example, or maybe all elements of vector (this is first part of the type).

Sorry for late answers. I have a job (and studies with life too) which takes a much time out of my "Coq time".

On Thu, Nov 7, 2013 at 11:51 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

2013/11/7 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?

In the context I gave, 'fix' is not a tactic, it is a construction language, as well as 'fun'. Though, there is also a tactic called 'fix <n>.' which is more or less "refine (fix <fresh_name> <arg_1> … <arg_n> {struct <arg_n>} := _).", it is a very low level tactic which I do not recommend, as it does not ensure guardedness condition, until you reach Qed. "induction" tactic is better for that, there are cases where one might want to use the 'fix' tactic, because "induction" does not work, but this is rather uncommon, and you can always deal with it using "induction" tactic combined with some tricks. Basically, the cases where one might want to use "fix" tactic are:
– mutual induction ("induction" tactic cannot directly deal with it easily).
– define computable functions embedding some proofs

But even in these cases, I would recommend to do a "refine (fix f x := match x with C x => _ (f x) | … end); clear f." (or use a "fix" tactic followed by immediate destructuration of the recursive argument, then generalizing over applications of the recursive function to the structurally smaller arguments, immediately followed by a "clear <name_of_recursive_function>."). This way, you should avoid unauthorized recursive calls. This is rather heavy to use, that is why I do not recommend "fix" tactic, unless you know what you do (the 'fix' construction is less dangerous, as you explicitely provide a term, so you know what you are doing).

For the return part, it is explained in many tutorials.

 match index with

 | O => fun (H : O <= len) => …
 | S i => fun (H : S i <= len) => let rec := vect_fold i _(*i<=len*) …
                                  in …

Take a look at the first branch, its type is "O<=len -> …" and the second branch has type "S i <= len -> …" where "i" is some existential variable not defined outside the "match …"
So the two branches do not have the same type, and one of the branch is not even typable per se. So we have to say that the type of the branch you chose is a function of the argument you pattern match against.
That is, one could define

let return_type := fun selector => match selector with O => O <= len -> … | S i => S i <= len -> … end

Then you could say that each branch is of type "return_type len" where "index = O" in the first branch and "index = S i" in the second.
That is, you can help the type checker by stating:

 match index with
 | O => (fun (H : O <= len) => …) : return_type index
 | S i => (fun (H : S i <= len) => let rec := vect_fold i _(*i<=len*) …
                                  in …) : return_type index

There all seems to work fine: both branches have the same type. Still there is a problem. Individually, the type checker does not agree with "return_type index = O<=len->…" and "return_type index = S i <= len->…".
Why? Because "index" is not bound to "O" in the first branch, and not bound to "S i" in the second, so you have to bind it manually (well, Coq type checker because smarter over the time, so I do not know up to which point it can type check correctly this kind of _expression_).

So you would require something like:

 match index with
 | O => (fun (H : O <= len) => …) : return_type index
 | S i => (fun (H : S i <= len) => let rec := vect_fold i _(*i<=len*) …
                                  in …) : return_type index
 end, binding index to i in return_type i

This syntax is not the one used by Coq, rather it put this between "match" and "with":

 match index as i return return_type i with
 | O => (fun (H : O <= len) => …) : return_type index
 | S i => (fun (H : S i <= len) => let rec := vect_fold i _(*i<=len*) …
                                  in …) : return_type index

Now with this information, we do not really need to type each branch as we did, and we can unfold and reduce the return clause, leading to:

 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 …

(in fact you should even be able to remove the "(H: …)", keeping only H, without its type.)

I did not explained all, as there can also be a "match … as … in … return … with … end" construction which is even more general ("match … in … return … with … end" is internally used when you do a "rewrite", "Print eq_ind", "Print eq_rec." "Print eq_rect." will give you more insight). Beside the rewrite case, "match … in … return … with … end" is rather uncommon.

So in conclusion, this is a way to be able to type check something a weird as:

if b then 18 else "a"%ascii::nil

such an _expression_ cannot be of type "nat", and it cannot be of type "list ascii" either.
BUT it can be of type: "if b then nat else list ascii" (and its generalization over "b" is "∀ b, if b then nat else list ascii").
I let you try to make it typecheck (hoping that Coq is not yet smart enough to be able to do it without indication, else it might not be an interesting exercise).

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

Even so, that seems strange. I would have expected a "A -> A" as final type, or "fin len -> fin len" or "vect A len -> A" or "vect A len -> fin len", but not "fin len -> A".
 

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

--
.../Sedrikov\...