The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-13 17:54 GMT+02:00 Jonathan <jonikelee AT gmail.com>:

On 07/13/2014 08:29 AM, Ömer Sinan Ağacan wrote:

The important difference here between lists and vectors is that the Vector
type has a dependent index, not just a parameter (which is all list has).

What's difference between index and parameter?

Type parameters aren't so special - many languages have them.  Take the list type, which is parameterized but not indexed.  The parameter A just says the same exact thing about all instances of list A - that the elements are of type A.  Nothing hard there.

But, now consider Vector.t.  This type functor has two arguments - one behaves exactly the same way as A in list A, but the other doesn't.  Given an instance of Vector.t A n, while it is true that all of its elements are of the type A, it isn't constructed out of other vectors of the same Vector.t A n type.  It is constructed out of vectors with the same parameter A but with a lower index n.  This despite the fact that all of those vectors were defined by the same single Vector.t definition (which is called a "family" , which I guess means that indexes are "family values" - which perhaps explains why they appear to the right of the ":" ;)

To distinguish between the kind of arguments that act like A vs. those that act like n, we call those like A parameters and those like n indexes.  There's a rough way of spotting them in the definitions - the parameters come before the ":" in the definition and the indexes come after:

Inductive t A : nat → Type := (*<- it's the preceding ":" between "A" and "nat" that is important *)
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n → t A (S n).

where this "t" is Vector.t (this definition is from Coq.Vectors.VectorDef).

I said "rough way" above because it's possible to get the behavior of an index from something appearing before the ":" by doing this:

Inductive t A (n:nat) : Type := (*<- n is now a "parameter", syntactically at least *)
  |nil : n=0 -> t A n
  |cons : forall (h:A) (n':nat), S n'=n -> t A n' -> t A n.

I would argue here (probably somewhat controversially) that n is still an index and not a parameter, even though it appears before the ":", and so all constructors share the same value of n.  Some (most, probably almost all) people will define the difference between index and parameter based on which side of ":" they appear. To me, the distinguishing feature is that n can vary within the definition of a single instance of Vector.t A n, while A doesn't. Or, more precisely, if the type term "Vector.t A n" appears in Coq, and you have an instance of it and match against it (or case analyze it in a proof script), are you going to uncover information about A and/or n, or not?  In the case of A, not - they're all the same, whatever A is it is throughout.  In the case of n, you will uncover information you didn't know about n before - in this case whether it is 0 or the successor of some other nat.  That's not much info, but it is something (quite important, actually).  And it is this "uncovering info" aspect that forces one to use more complex variants of Coq's match construct to cope.

Here's another alteration to help illustrate things:

Inductive t : Type -> nat -> Type := (*<- everything is an index *)
  |nil : forall (A : Type), t A 0
  |cons : forall (A : Type) (h : A) (n : nat), t A n -> t A (S n).

This beastie is very different from the two above - because the type of the element can now vary within a single instance.  So, when one writes "Vector.t Foo 42", the "Foo" only applies to the outermost "cons" cell, just as the 42 does.  The remaining cons cells carry their own type in the constructor A "slot", just as they carry their own n.  They could all be "Foo", but there's nothing forcing them to be that.

I guess you meant:

Inductive t : Type -> nat -> Type := (*<- everything is an index *)
  |nil : forall (A : Type), t A 0
  |cons : forall (A B : Type) (h : A) (n : nat), t B n -> t A (S n).

Otherwise, all cons will have the same 'A' argument.
Still, Coq will not consider it as a parameter, which can be sometimes annoying when performing induction: the information that this type is the same for all calls to cons must be carried along the induction.
Basically, "forall (a:t nat), P a" may need to be generalized in "forall (A:Type) (a:t A), A = nat -> P a".
 

I'm still open for suggestions to implement it using vectors and refine.

I am no expert on using refine to build a whole function, or on the Program construct, which is somewhat related (Program is like a combo of syntactic sugar on refine, and some very nifty tactics that try to solve holes for you).  I have tried things with both, and there seems to be much dark magic involved in getting them to do precisely what you want, especially in the presence of recursion. There's also the dreaded "guardedness" issue - which basically means that by using refine or Program, one can write things that don't terminate, and Coq won't tell you until you try to process that final "Defined." - and then it will complain in ways that don't always make much sense (at least to me).  Sure, there's the "Guarded" tactic, but when and where to use it?  And, yes, they can lose info about things, if you're not careful.

For non mutual recursion, I tend to put the applied recursive calls inside of the refine. Typically:

refine (fix foo (x : bar) := match bar with Bar y => let foo_bar := foo y in _ | Baz y => let foo_baz := foo y in _ end);
(*now, removal of "foo" in all branches [due to the ';' at the end of the previous tactic] so that it won’t bother anymore*)
clear foo.
(*now testing guardedness [I do not remember if it has to be done for each branch]*)
Guarded.
(*Now we are clear, we should not have to check guardedness anymore*)
 
Ok, that is easy to say, but I also have met cases where finding the correct refine term to do that is not that easy to write.
Still, it works pretty well for most of the cases.

For mutual recursion, you can basically do the same thing:

Fixpoint foo (x:a) : A
with bar (y:b) : B
with baz (z:c) : C.
(** foo **)
refine (…); clear foo bar baz.
Guarded.
Proof.
…
(** bar **)
refine (…); clear foo bar baz.
Guarded.
Proof.
…
(** baz **)
refine (…); clear foo bar baz.
Guarded.
Proof.
…
Defined.

-- Jonathan

--
.../Sedrikov\...