The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>]

Hi,
 I suggest a different solution to the problem. In my opinion the use 
of a dependent inductive definition for vectors is what causes the 
trouble. It is not necessary. Instead we should represent vectors are 
tuples, that is, as iterated products. By the way, this is the usual way 
to define them informally.
 The tuple <a1,...,an> is just (a1, (a2, (...., (an-1, an)...))).
This means definining (Tuple A 0) as a set with only one element <>, 
let's say unit;
and Tuple A (S n) as A*(Tuple A n).
This is a higher order recursion on nat:

Fixpoint Tuple (A:Set)(n:nat){struct n}: Set :=
match n with
 0 => unit
| (S n') => (A*(Tuple A n'))%type
end.

If you use this definition all the problems disappear.
The definition of the mapping of a binary function on tuples is as easy 
as the similar definition of for a unary function.
Actually, as you can see from the last definition on the attached file, 
you can even define the mapping on tuples of a k-ary function for 
arbitrary k.
I challenge you to do the same using the inductive Vector (or listn) 
definition!

The trick is to define currying and uncurrying, showing the equivalence of
  Tuple A n -> B  with A -> ... -> A -> B  (n arguments of type A).
I suspect that these functions would also be very difficult to define 
for inductive Vectors.

I use the definition of matrices as tuples of tuples and the 
transposition operation on them. This is also easy to define. I tried to 
look for transposition in Nicolas Magaud development to see if it can 
easily be defined using inductive vectors but I couldn't find it. 
Nicolas, is there such a function in your formalization.

In conclusion, the moral is this: when defining listn_bin_op you have 
three arguments, n l1 l2, that have the same recursive structure. You 
have to choose to do induction on one of them and then proceed by 
inversion on the others. This is because Coq actually doesn't know that 
the inductive structure is the same. With tuples you have only one 
structured element, n, and the others are taken care of by the Fixpoint 
definition of tuples.

We should also remark, when using the libraries Eqdep and JMeg as 
suggested by Yves Bertot and Boris Yakobowski, that these contain 
axioms, so if you import them you are not using the pure type theory 
anymore. One more reason to do things differently.

Cheers,
 Venanzio



Require Import Arith.

Fixpoint Tuple (A:Set)(n:nat){struct n}: Set :=
match n with
  0 => unit
| (S n') => (A*(Tuple A n'))%type
end.

Fixpoint tuple_proj (A:Set)(n:nat){struct n}:
  forall (t:Tuple A n)(i:nat), i<n -> A :=
match n return forall (t:Tuple A n)(i:nat), i<n -> A with
  O => fun t i h => False_rec A (lt_n_O i h)
| (S n') => fun t i =>
            match i return i<(S n') -> A with
              O => fun _ => fst t
            | (S i') => fun h => tuple_proj A n' (snd t) i' (lt_S_n i' n' h)
            end
end.

Implicit Arguments tuple_proj [A n].

Section Unary_Operation.

Variables (A B:Set) (f: A->B).

Fixpoint tuple_map (n:nat): Tuple A n -> Tuple B n :=
match n return Tuple A n -> Tuple B n with
  O => fun _ => tt
| (S n') => fun x => let (a,x'):=x in (f a, tuple_map n' x')
end.

Lemma proj_of_tuple_map :
  forall (n:nat)(t:Tuple A n)(i:nat)(h:i<n),
    tuple_proj (tuple_map n t) i h = f (tuple_proj t i h).
Proof.
intro n; elim n.
intros t i h; elim (lt_n_O i h).
intros n' IHn' t.
case t; intros a t' i; change (Tuple A n') in t'; case i.
intros; simpl; trivial.
intros i' hi; simpl; apply IHn'.
Qed.

End Unary_Operation.

Implicit Arguments tuple_map [A B n].

Section Binary_Operation.

Variables (A B C:Set) (g: A->B->C).

Fixpoint tuple_bin_map (n:nat): Tuple A n -> Tuple B n -> Tuple C n :=
match n return Tuple A n -> Tuple B n -> Tuple C n with
  O => fun _ _ => tt
| (S n') => fun x y => let (a,x'):=x in
                       let (b,y'):=y in
                       (g a b, tuple_bin_map n' x' y')
end.

Lemma proj_of_tuple_bin_map :
  forall (n:nat)(t1:Tuple A n)(t2:Tuple B n)(i:nat)(h:i<n),
    tuple_proj (tuple_bin_map n t1 t2) i h
    = g (tuple_proj t1 i h) (tuple_proj t2 i h).
Proof.
intro n; elim n.
intros t1 t2 i h; elim (lt_n_O i h).
intros n' IHn' t1 t2.
case t1; intros a t1'; change (Tuple A n') in t1'; 
case t2; intros b t2'; change (Tuple B n') in t2'.
intro i;   case i.
intros; simpl; trivial.
intros i' hi; simpl; apply IHn'.
Qed.

End Binary_Operation.

Fixpoint curry_set (A:Set)(n:nat)(B:Set){struct n}: Set :=
match n with
  0 => B
| (S n') => A -> (curry_set A n' B)
end.

Fixpoint curry_pair (A:Set)(a:A)(n:nat)(B:Set){struct n}:
  curry_set A n B -> curry_set A n (A*B) :=
match n return curry_set A n B -> curry_set A n (A*B) with
  O => fun b => (a,b)
| (S n') => fun f x => (curry_pair A a n' B (f x))
end.

Fixpoint tuple (A:Set)(n:nat){struct n}: curry_set A n (Tuple A n) :=
match n return curry_set A n (Tuple A n) with
  0 => tt
| (S n') => fun a => curry_pair A a n' (Tuple A n') (tuple A n')
end.

Implicit Arguments tuple [A].

Fixpoint curry (A:Set)(n:nat)(B:Set){struct n}:
  (Tuple A n -> B) -> curry_set A n B :=
match n return (Tuple A n -> B) -> curry_set A n B with
  O => fun f => f tt
| (S n') => fun f a => curry A n' B (fun x => f (a,x))
end.

Implicit Arguments curry [A n B].

Fixpoint uncurry (A:Set)(n:nat)(B:Set){struct n}:
  curry_set A n B -> Tuple A n -> B :=
match n return curry_set A n B -> Tuple A n -> B with
  O => fun b _ => b
| (S n') => fun f x => let (a,x'):=x in (uncurry A n' B (f a) x')
end.

Implicit Arguments uncurry [A B].

Section Matrices.

Variable A:Set.

Definition Matrix (n m:nat): Set :=
  Tuple (Tuple A m) n.

Fixpoint constant_tuple (X:Set)(x:X)(n:nat){struct n}: Tuple X n :=
match n return Tuple X n with
  O => tt
| (S n') => (x, constant_tuple X x n')
end.

Implicit Arguments constant_tuple [X].

Fixpoint add_column (n m:nat){struct n}:
  Tuple A n -> Matrix n m -> Matrix n (S m) :=
match n return Tuple A n -> Matrix n m -> Matrix n (S m) with
  O => fun _ _ => tt
| (S n') => fun x M => let (a,x'):=x in
                       let (v,M'):=M in
                       ((a,v), add_column n' m x' M')
end.

Fixpoint transpose (n m:nat){struct n}: Matrix n m -> Matrix m n :=
match n return Matrix n m -> Matrix m n with
  O => fun _ => constant_tuple tt m
| (S n') => fun M => let (v,M'):=M in add_column m n' v (transpose n' m M')
end.

End Matrices.

Implicit Arguments add_column [A n m].
Implicit Arguments transpose [A n m].

Section n_ary_Operation.

Variables A B:Set.

Definition tuple_matrix_map:
  forall k:nat, curry_set A k B ->
  forall n:nat, Matrix A k n -> Tuple B n :=
fun k f n M => tuple_map (uncurry k f) (transpose M).

Definition tuple_n_map:
  forall k:nat, curry_set A k B ->
  forall n:nat, curry_set (Tuple A n) k (Tuple B n) :=
fun k f n => curry (tuple_matrix_map k f n).

End n_ary_Operation.