Julin S (Jan 14 2022 at 09:59): Julin S (Jan 14 2022 at 09:59):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.
Li-yao (Jan 14 2022 at 10:17):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.
Li-yao (Jan 14 2022 at 10:23):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?
Julin S (Jan 14 2022 at 10:31):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.
Li-yao (Jan 14 2022 at 10:48):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.
Li-yao (Jan 14 2022 at 10:52):Julin S said:
Can annotating (that's what it's called, right) the
matchwith 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).
Li-yao (Jan 14 2022 at 10:59):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: Oct 13 2024 at 01:02 UTC