Stream: Coq users

Topic: ✔ Pattern matching on `Bcons`


view this post on Zulip Julin S (Nov 24 2021 at 17:40):

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?

view this post on Zulip Julin S (Nov 24 2021 at 17:43):

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?

view this post on Zulip Gaëtan Gilbert (Nov 24 2021 at 17:44):

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

view this post on Zulip Julin S (Nov 24 2021 at 17:45):

Oh.. so in the second example's case, Bnil just becomes another name for vec..

view this post on Zulip Julin S (Nov 24 2021 at 17:48):

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?

view this post on Zulip Gaëtan Gilbert (Nov 24 2021 at 17:51):

patterns are syntactic, definitions are not unfolded

view this post on Zulip Julin S (Nov 24 2021 at 17:54):

Okay, so to pattern match we got to use the real Vector.nil and Vector.cons itself. Thanks.

view this post on Zulip Julin S (Nov 24 2021 at 17:55):

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 *)

view this post on Zulip Notification Bot (Nov 24 2021 at 17:55):

Ju-sh has marked this topic as resolved.

view this post on Zulip Notification Bot (Nov 24 2021 at 17:57):

Ju-sh has marked this topic as unresolved.

view this post on Zulip Notification Bot (Nov 24 2021 at 18:25):

Ju-sh has marked this topic as resolved.

view this post on Zulip Julin S (Nov 24 2021 at 18:30):

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).

view this post on Zulip Kenji Maillard (Nov 24 2021 at 18:40):

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.

view this post on Zulip Julin S (Nov 24 2021 at 19:14):

How can this specific example be fixed?
Is it using the match ... return construct of coq?

view this post on Zulip Julin S (Nov 24 2021 at 19:23):

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

view this post on Zulip Kenji Maillard (Nov 24 2021 at 19:23):

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.

view this post on Zulip Kenji Maillard (Nov 24 2021 at 19:26):

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.

view this post on Zulip Julin S (Nov 25 2021 at 04:31):

Thanks!

view this post on Zulip Julin S (Nov 25 2021 at 04:31):

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


Last updated: Feb 04 2023 at 21:02 UTC