I was trying to make an `xor`

for a pair of bool vectors and did

```
Require Import Vector.
Import VectorNotations.
(* For a dummy result for use with xorn *)
Fixpoint repeat (n : nat) (val : bool) : Vector.t bool n :=
(match n with
| O => []
| S n' => val :: (repeat n' val)
end)%vector.
Fixpoint xorn {n m : nat} (a : Vector.t bool n)
(b : Vector.t bool m) : Vector.t bool (max n m) :=
(match n, m with
| O, O => [] (* error here *)
| _, O => a
| O, _ => b
| S n', S m' =>
match a, b with
| _, _ => repeat (max n m) true (* dummy result *)
end
end)%vector.
(*
In environment
xorn : forall n m : nat, t bool n -> t bool m -> t bool (Nat.max n m)
n : nat
m : nat
a : t bool n
b : t bool m
The term "[]" has type "t bool 0" while it is expected to have type
"t bool (Nat.max ?n@{n1:=0} ?n0@{m1:=0})".
*)
```

How can this error be fixed?

Output vector has size of the biggest of the two input vectors.

If the vectors are not of the same size, the values of the longer vector are just copied.

It seems I couldn't make coq realize that output vector size is zero when both inputs are of length zero.

I was trying for an output like:

```
+----------------------------------------+----------------------+
| xorn [true; false] [true; false; true] | [false; false; true] |
+----------------------------------------+----------------------+
| xorn [true] [false; false; true] | [true; false; true] |
+----------------------------------------+----------------------+
| xorn [true; false] [false; true] | [true; true] |
+----------------------------------------+----------------------+
| xorn [true; false] [true; false] | [false; false] |
+----------------------------------------+----------------------+
```

Just to see if another example would work, I tried:

```
Fixpoint xorn {n m : nat} (a : Vector.t bool n)
(b : Vector.t bool m) : Vector.t bool (max n m) :=
repeat (max n m) true.
```

and that works okay.

Counterintuitively, dependent pattern-matching is quite counterintuitive, and a more friendly interface than raw `match`

is provided by the Equations plugin.

```
From Equations Require Import Equations.
Require Import Vector.
Import VectorNotations.
(* For a dummy result for use with xorn *)
Fixpoint repeat (n : nat) (val : bool) : Vector.t bool n :=
(match n with
| O => []
| S n' => val :: (repeat n' val)
end)%vector.
Equations xorn {n m : nat} (a : Vector.t bool n) (b : Vector.t bool m) : Vector.t bool (max n m) :=
xorn (x :: a) (y :: b) := xorb x y :: xorn a b ;
xorn [] b := b ;
xorn a [] := a.
```

Just to understand how coq works, how could it look like without using `Equations`

?

I also tried xor for two vectors of the same length like

```
Definition xor' {n : nat} (a b : Vector.t bool n) : Vector.t bool n :=
(match a, b with
| [], [] => []
| x::xs, y::ys =>
match x, y with
| true, true => false
| false, false => false
| _, _ => true
end
end)%vector.
(*
Non exhaustive pattern-matching: no clause found for patterns [], _ :: _
*)
```

but got error.

This time coq could find that the remaining patterns would never happen.

In this case a "raw" solution is actually not too bad, but it's kind of a fluke:

```
Fixpoint xorn {n m : nat} (a : Vector.t bool n)
(b : Vector.t bool m) : Vector.t bool (max n m) :=
match a, b with
| x :: xs, y :: ys => xorb x y :: xorn xs ys
| x :: xs, [] => x :: xs
| [], ys => ys
end.
```

Why does this version `xorn`

work? And why is it a fluke?

I tried replacing the `x :: xs`

from the second branch of the `match`

with just `a`

and got this error:

```
Fixpoint xorn' {n m : nat} (a : Vector.t bool n)
(b : Vector.t bool m) : Vector.t bool (max n m) :=
match a, b with
| x :: xs, y :: ys => xorb x y :: xorn xs ys
| x :: xs, [] => a
| [], ys => ys (* error here *)
end.
(*
In environment
xorn' : forall n m : nat, t bool n -> t bool m -> t bool (Nat.max n m)
n : nat
m : nat
a : t bool n
b : t bool m
The term "b" has type "t bool m" while it is expected to have type
"t bool (Nat.max ?n@{n1:=0} ?n0@{m:=m; m1:=m})".
*)
```

I suppose this is something related?

Can annotating (that's what it's called, right) the `match`

with an explicit return or something similar produce much of a change? Had tried simply copying the return type there but that didn't work.

This is a convenient function to define because the arguments `a`

and `b`

have indices that are distinct variables `n`

and `m`

. For example, this contrasts with a version of `xorn`

with the same lengths `Vector.t bool n -> Vector.t bool n -> Vector.t bool n`

, or the `head`

function `head : Vector.t A (S n) -> A`

, which are quite trickier to define.

Julin S said:

Can annotating (that's what it's called, right) the

`match`

with an explicit return or something similar produce much of a change? Had tried simply copying the return type there but that didn't work.

`a`

doesn't fit because the expected type changes in each branch. Instead, you can do

```
| (_ :: _) as a, [] => a
```

If you just leave the pattern as `_, []`

it desugars to two branches, one `(_ :: _), [] => _`

, expecting `Vector.t bool (max (S n0) 0)`

, where `n0`

is the length of the tail of `a`

and one branch `[], [] => _`

, expecting `Vector.t bool (max 0 0)`

. In any case, `a`

still has type `Vector.t bool n`

, which is unrelated to `S n0`

as far as the typechecker is concerned, which is why you have to use the values from the patterns (or use the convoy pattern to smuggle more things from the context).

In case you haven't read it, the book CPDT is standard recommended reading on the topic. http://adam.chlipala.net/cpdt/html/Cpdt.MoreDep.html

Last updated: Jan 29 2023 at 01:02 UTC