Stream: Coq users

Topic: xor of 2 vectors of different sizes


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (Jan 14 2022 at 10:22):

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.

view this post on Zulip 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.

view this post on Zulip Julin S (Jan 14 2022 at 10:29):

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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Li-yao (Jan 14 2022 at 10:52):

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

view this post on Zulip Li-yao (Jan 14 2022 at 10:57):

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

view this post on Zulip 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: Mar 29 2024 at 07:01 UTC