[Coq-Club] Dependent match on two vectors

[Vincent Siles]

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.

[Dominique Larchey-Wendling]

Post by Vincent Siles
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.

[Vincent Laporte]

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.

[Vincent Siles]

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)

Post by Vincent Laporte
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.

[Dominique Larchey-Wendling]

You could also use vhead and vtail and proceed by structural recursion on n

Definition vhead { A n } (v : vec A (S n)) := match v with vcons _ x _
=> x end.
Definition vtail { A n } (v : vec A (S n)) : vec A n := match v with
vcons _ _ t => t end.

Fixpoint vprod' n : vec nat n -> vec nat n -> nat :=
match n as m return vec nat m -> vec nat m -> nat with
| 0 => fun _ _ => 0
| S n => fun v w => vhead v*vhead w + vprod' _ (vtail v) (vtail w)
end.

Cheers

Dominique

Post by Vincent Siles
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)
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.