Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem with dependant types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with dependant types


chronological Thread 
  • From: Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>
  • To: Nicolas Magaud <nmagaud AT cse.unsw.edu.au>
  • Cc: casteran AT labri.fr, june andronick <jandronick AT axalto.com>, coq-club AT pauillac.inria.fr, conor AT cs.rhul.ac.uk
  • Subject: Re: [Coq-Club] problem with dependant types
  • Date: Wed, 17 Nov 2004 15:57:39 -0500
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.




 



Archive powered by MhonArc 2.6.16.

Top of Page