Julin S (Nov 24 2021 at 17:40): 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?
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?
Gaëtan Gilbert (Nov 24 2021 at 17:44):it's treating Bnil in that pattern as a fresh variable
Julin S (Nov 24 2021 at 17:45):Oh.. so in the second example's case, Bnil just becomes another name for vec..
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?
Gaëtan Gilbert (Nov 24 2021 at 17:51):patterns are syntactic, definitions are not unfolded
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.
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 *)
Ju-sh has marked this topic as resolved.
Notification Bot (Nov 24 2021 at 17:57):Ju-sh has marked this topic as unresolved.
Notification Bot (Nov 24 2021 at 18:25):Ju-sh has marked this topic as resolved.
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).
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.
Julin S (Nov 24 2021 at 19:14):How can this specific example be fixed?
Is it using the match ... return construct of coq?
Julin S (Nov 24 2021 at 19:23):@Kenji Maillard Or does that function has to take proofs as arguments?
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.
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!
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: Oct 13 2024 at 01:02 UTC