The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Le 10/10/2018 à 15:37, Vincent Siles a écrit :
> 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
> .

The problem is that n is a *shared* dependent parameter in both
v1 and v2. When you proceed by pattern matching on v2 (after v1),
the n parameter is not free of constraints ... Let me suggest
the following solution:

Fixpoint vprod_rec (n : nat) m (v1 : vec nat n) (v2: vec nat m) : n = m
-> nat .
Proof.
  refine (match v1 in vec _ n0, v2 in vec _ m0 return n0 = m0 -> nat with
    | vnil, vnil => fun _ => 0
    | vnil, vcons _ _ _ => fun H => _
    | vcons _ _ _, vnil => fun H => _
    | vcons _ hd1 tl1, vcons _ hd2 tl2 => fun H => (hd1 * hd2) +
vprod_rec _ _ tl1 tl2 _
  end).
  + exfalso; discriminate.
  + exfalso; discriminate.
  + inversion H; trivial.
Defined.

Definition vprod n v1 v2 := vprod_rec n _ v1 v2 eq_refl.