The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Dear Coq-Clubbers, 

I'm trying to define the product of two vectors of the same size, with something like

Inductive vec (A: Type) : nat -> Type :=

  | vnil  : vec A 0

  | vcons : forall n, A -> vec A n -> vec A (1 + n)

.

Arguments vnil [A].

Arguments vcons [A] n hd tl.

Fixpoint vprod (n: nat) (v1 v2: vec nat n) : nat :=

  match v1 in vec _ n0, v2 in vec _ n0 return nat with

    | vnil, vnil => 0

    | vnil, vcons _ _ _ => False_rect nat _  (* 1 *)

    | vcons _ _ _, vnil => False_rect nat _  (* 1 *)

    | vcons _ hd1 tl1, vcons _ hd2 tl2 => (hd1 * hd2) + vprod _ tl1 tl2 (* 2 *)

  end

.

But I have two issues:

- Impossible branches (* 1 *) fail with 'False_rec nat has type False -> nat instead of nat' if I don't add the _. I usually don't have to do that on impossible branches

- (* 2 *) fails with 

In environment

vprod : forall n : nat, vec nat n -> vec nat n -> nat

n : nat

v1 : vec nat n

v2 : vec nat n

n0 : nat

hd1 : nat

tl1 : vec nat n0

v0 : vec nat (1 + n0)

n1 : nat

hd2 : nat

tl2 : vec nat n1

The term "tl2" has type "vec nat n1"

while it is expected to have type

 "vec nat n0".

 

How can I unify ""n0"" and ""n1"" here so that it types check ? I presume my match statement is buggy

Best,

V.