Stream: Coq users

Topic: ✔ Error on a simple BST definition

Julin S (Jul 16 2021 at 06:55):

Hi. I was trying to a search function for a binary search tree as in part 3 of the software fundametals book here.

``````From Coq Require Import String.
Require Import Coq.Arith.PeanoNat.
Require Import Notations.

Notation "a >? b" := (Nat.ltb b a)
(at level 70) : nat_scope.

Definition key := nat.

Inductive tree (V : Type) : Type :=
| E
| T (l : tree V) (k : key) (v : V) (r : tree V).

Arguments E {V}.
Arguments T {V}.

Fixpoint isBound {V : Type} (x : nat) (t : tree V) : bool :=
match t with
| E => false
| T left key val right => if x <? key then (isBound x left)
else if x >? key then (isBound x right)
else true
end.
``````

But I get an error on `isBound` saying

``````The constructor left (in type sumbool) expects 1 argument.
``````

Why is that error showing up? Couldn't figure it out.

Kenji Maillard (Jul 16 2021 at 07:11):

The error says that `left` is a constructor of an inductive defined in your context, namely `sumbool`:

``````Print sumbool.
(* Inductive sumbool (A B : Prop) : Set :=            *)
(*     left : A -> {A} + {B} | right : B -> {A} + {B} *)
(*                                                    *)
(* Arguments sumbool (_ _)%type_scope                 *)
(* Arguments left {A B}%type_scope, [A] _ _           *)
(* Arguments right {A B}%type_scope, _ [B] _          *)
``````

so you cannot use `left` or `right` as identifiers in a pattern of a pattern-match construct (change `left` and `right` to `l`/`r` and everything is fine)

Julin S (Jul 16 2021 at 07:15):

Oh.. so it's because there's already a name `left`. Thanks!

Notification Bot (Jul 16 2021 at 07:33):

Ju-sh has marked this topic as resolved.

Last updated: Jun 25 2024 at 14:01 UTC