I was trying to use the Bvector module from the standard library.

Bvector is defined like:

```
Definition Bvector := Vector.t bool.
Definition Bnil := @Vector.nil bool.
Definition Bcons := @Vector.cons bool.
```

I tried a function that checks if the length of a Bvector is zero like:

```
Require Import Bvector.
Definition isEmpty {n : nat} (vec : Bvector n) : bool :=
match vec with
| Bnil => true
| Bcons _ _ => false
end.
```

But got this error: `Unknown constructor: Bcons.`

Yet doing a `Check`

on `Bcons`

works:

```
Check Bcons.
(*
Bcons : bool -> forall n : nat, Vector.t bool n -> Vector.t bool (S n)
*)
```

Is it that we can't do pattern matching on Bcons since it's just an alias of `Vector.t bool`

?

If that was the case, why doesn't the use of `Bnil`

throw error?

Also doing

```
Definition isEmpty {n : nat} (vec : Bvector n) : bool :=
match vec with
| Bnil => true
end.
```

works and coq doesn't complain about non-exhaustive pattern matching. Why is that?

it's treating Bnil in that pattern as a fresh variable

Oh.. so in the second example's case, `Bnil`

just becomes another name for `vec`

..

Trying with a `Bvector.`

prefix didn't work either.

```
Check Bvector.Bnil.
(* Bnil : t bool 0 *)
Check Bvector.Bcons.
(* Bcons : bool -> forall n : nat, t bool n -> t bool (S n) *)
Definition isEmpty {n : nat} (vec : Bvector n) : bool :=
match vec with
| Bvector.Bnil => true
| Bvector.Bcons x xs => false
end.
(* Unknown constructor: Bvector.nil *)
```

I wonder what makes the `Bvector.nil`

'invisible' inside the function definition?

patterns are syntactic, definitions are not unfolded

Okay, so to pattern match we got to use the real `Vector.nil`

and `Vector.cons`

itself. Thanks.

Changed the `Bnil`

and `Bcons`

to their `Vector.t`

equivalents and it worked.

```
Definition isEmpty {n : nat} (vec : Bvector n) : bool :=
match vec with
| Vector.nil => true
| Vector.cons _ x xs => false
end.
Compute isEmpty Bnil. (* true : bool *)
Compute isEmpty (Bcons true 0 Bnil). (* false : bool *)
Compute isEmpty (Bcons false 1 (Bcons true 0 Bnil)). (* false : bool *)
```

Ju-sh has marked this topic as resolved.

Ju-sh has marked this topic as unresolved.

Ju-sh has marked this topic as resolved.

I got something similar while trying to reverse a `Bvector`

with

```
Fixpoint revBV {n : nat} (vec : Bvector n) : Bvector n :=
match vec with
| []%vector => []%vector (* vec *)
| (x::xs)%vector => append (revBV xs) [x]%vector
end.
```

Error was

```
In environment
revBV : forall n : nat, Bvector n -> Bvector n
n : nat
vec : Bvector n
x : bool
n0 : nat
xs : t bool n0
The term "(revBV n0 xs ++ [x])%vector" has type "t bool (n0 + 1)"
while it is expected to have type "Bvector (S n0)".
```

How can I modify this reverse function to make it right? Like for letting coq know that `t bool (n0 + 1)`

is same as `Bvector (S n0)`

.

You have a (frequent) problem here: `n0 + 1`

and `S n0`

are only propositionally equal (you can prove by induction on `n0`

that `n0 + 1 = S n0`

), not convertible for Coq's conversion. So either you will need to rewrite along that equation, or you could change its type to return some `Bvector (rev n)`

where `rev 0 := 0`

and `rev (S n) := n + 1`

.

How can this specific example be fixed?

Is it using the `match ... return`

construct of coq?

@Kenji Maillard Or does that function has to take proofs as arguments?

For the rev on nat solution, it looks like you need to help a bit Coq with a return statement indeed:

```
Require Import Vector.
Require Import Bvector.
Fixpoint revNat (n : nat) : nat := match n with 0 => 0 | S n => revNat n + 1 end.
Fixpoint revBV {n : nat} (vec : Bvector n) : Bvector (revNat n) :=
match vec in Vector.t _ k return Bvector (revNat k) with
| []%vector => []%vector (* vec *)
| (x::xs)%vector => append (revBV xs) [x]%vector
end.
```

For the solution using rewrite, you don't need a return clause, but the resulting function might get stuck on the proof you are rewriting with

```
Require Import Vector.
Require Import Bvector.
Import EqNotations.
Fixpoint revBV {n : nat} (vec : Bvector n) : Bvector n :=
match vec with
| []%vector => []%vector (* vec *)
| (x::xs)%vector => rew (PeanoNat.Nat.add_1_r _) in append (revBV xs) [x]%vector
end.
```

Thanks!

Bit of an unfamiliar territory for me (still quite new to coq), but this is a start.

Last updated: Oct 03 2023 at 20:01 UTC