The Coq mailing list

[casteran AT labri.fr]

Hi Yves,


Selon Yves Bertot 
<Yves.Bertot AT sophia.inria.fr>:

> This message may be redundant with Pierre Castéran's answers, but I did
> try to stay very close to your development so that it may still be useful.


Not at all :-)

I think both approaches will make a beautiful case study on dependant
types. By the way, I improved slightly the approach of using
recursion principles for vectors of equal length.
Once vector_double_rect defined, and used to define the mapping
of a binary operation to vectors of length n, it is easy to use
it to prove June's theorem. This makes a very short
proof, and all the machinery about vectors of length 0 and  (S n)
remains encapsulated in the derivation of vector_double-rect.


Lemma nth_op : forall  (A:Set)(bin_op : A -> A -> A)
      (n:nat)  (v1 v2: vector A  (S n)) i  a b,
      vector_nth i v1 = Some a ->
      vector_nth i v2 = Some b ->
      vector_nth i (vector_bin_op A bin_op _ v1 v2) = Some (bin_op a b).
Proof.
 intros A bin_op n v1 v2; pattern (S n),v1,v2.
 apply vector_double_rect.
 simpl.
 destruct i; discriminate 1.
 destruct i; simpl;auto.
 injection 1; injection 2;intros; subst a; subst b; auto.
Qed.



Pierre




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.