Stream: Coq users

Topic: ✔ Error on a simple BST definition


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

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

view this post on Zulip Julin S (Jul 16 2021 at 07:15):

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

view this post on Zulip Notification Bot (Jul 16 2021 at 07:33):

Ju-sh has marked this topic as resolved.


Last updated: Jan 27 2023 at 01:03 UTC