The Coq mailing list

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

Thanks to both of you.

To address Vincent suggestions of other definitions, I strongly agree, but I have to use that one in my case :D Having a side proof is most of the time a better solution (at least for me)

Le mer. 10 oct. 2018 à 16:16, Vincent Laporte <vincent.laporte AT gmail.com> a écrit :

Hi Vincent,

As a complement to Dominique’s suggestion, here is an other
implementation that do not require any (interactive) proof of false: you
can provide dummy values (of any inhabited type) in unreachable
branches. Also, by generalizing the recursive call before destructing
the second argument, you get a chance to type-check it again in the
final branch.

Fixpoint vprod (n: nat) (v: vec nat n) : vec nat n → nat :=
  match v with
  | vnil => λ _, 0
  | vcons n' h t =>
    λ v',
    match v' in vec _ i return match i with O => unit | S j => (vec nat
j → nat) → nat end with
    | vnil => tt
    | vcons _ h' t' => λ rec, h * h' + rec t'
    end (vprod n' t)
  end.

Also, there are other definitions of the type vec that are much more
convenient to work with (e.g., a list packed with a proof that its size
is n).

Cheers,
--
Vincent.