The Coq mailing list

[casteran AT labri.fr]

Hello June,

> > (* (by the way, I didn't manage to define listn_bin_op with Fixpoint and
> > "match ... in..." like the listn_un_op definition ..........) *)


 It seems that defining functions which work in parallel on two
vectors are worth having a generic definition, like :


Definition vector_double_rec :
      forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Set),
        P 0 Vnil Vnil ->
        (forall n (l1 l2 : vector A n) a b, P n l1 l2 ->
             P (S n) (Vcons a l1) (Vcons  b l2)) ->
       forall n (l1 l2 : vector A n), P n l1 l2.
 induction n.
 intros; rewrite (zero_nil _ l1); rewrite (zero_nil _ l2).
 auto.
 intros l1 l2; rewrite (decomp _ _ l1);rewrite (decomp _ _ l2).
 apply H0.
 auto.
Defined.



Definition vector_bin_op2 (A:Set)(bin_op: A -> A -> A) n v1 v2 : vector A n :=
   vector_double_rec A  (fun n v1 v2 => vector A n)
                        Vnil
                        (fun n v1 v2 a b r => Vcons (bin_op a b) r) n v1 v2.


Notice that, in order to work properly in computations,
 these functions need the replacement
of the two "Admitted" by the proofs of Pierre and Laurent.
I quote the message from Laurent, where you can find all the necessary
references.



Pierre



Hi,

>
>  Below is a simple proof that the only vector of length 0 is
> Vnil. But this proof uses the axiom JMeq_eq. Is there any axiom-free
> proof of the same result ?
>

It is always the same trick as explained by Pierre Letouze:

http://coq.inria.fr/mailing-lists/coqclub/200404/msg00002.html

It is also used in the definition of monomials in my buchberger
development:

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Buchberger/index.html

You first define a variant of the identity function to get rid of the
dependency:

Definition vector_id : forall n : nat, vector bool n -> vector bool n.
intros n; case n.
intros H'; exact (Vnil bool).
intros n1 H'; exact H'.
Defined.

Prove that it is indeed the identity


Theorem vector_id_is_id : forall n (v: vector bool n), v = vector_id n v.
intros n v; case v; simpl in |- *; auto.
Qed.

And the trick is done

Theorem vector_eq_0 : forall v : vector bool 0, v = Vnil bool.
intros v; exact (vector_id_is_id 0 v).
Qed.



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




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