Systems and
Formalisms Lab

Quiz 2

Grading scheme

Binary search trees

We define trees as in the lab:

Inductive tree :=
| Leaf
| Node (d: nat) (l r: tree).

A tree tr is a binary search tree if there exists an indicator predicate s: nat -> Prop such that bst tr s holds (bst is as defined in the lab).

BST examples

For each example below, indicate whether the tree is a binary search tree:

BST invariant

There are many ways to define the binary search tree invariant.

We say that a candidate definition is_bst is sound if all trees that satisfy is_bst are binary search trees:

Definition sound (is_bst: tree -> Prop) :=
  forall tr, is_bst tr -> exists s, bst tr s.

We say that a definition is_bst is complete if all binary search trees satisfy is_bst:

Definition complete (is_bst: tree -> Prop) :=
  forall tr, (exists s, bst tr s) -> is_bst tr.

For each of the following definitions, indicate whether it is sound and whether it is complete.

Constants

Consider the following definition:

Definition is_bst_yes (tr: tree) :=
  True.

Consider the following definition:

Definition is_bst_no (tr: tree) :=
  False.

Fixpoints

Consider the following definition:

Fixpoint is_bst_fx (tr: tree) :=
  match tr with
  | Leaf | Node _ Leaf Leaf => True
  | Node d Leaf r =>
      match r with Leaf => True | Node dr _ _ => d < dr end
      /\ is_bst_fx r
  | Node d l Leaf =>
      match l with Leaf => True | Node dl _ _ => dl < d end
      /\ is_bst_fx l
  | Node d l r =>
      match r with Leaf => True | Node dr _ _ => d < dr end
      /\ match l with Leaf => True | Node dl _ _ => dl < d end
      /\ is_bst_fx l /\ is_bst_fx r
  end.

Inductives

Consider the following definition:

Inductive is_bst_ind' : forall (tr: tree) (s: nat -> Prop), Prop :=
| is_bst_ind_Leaf s
    (Hs: forall x, s x <-> False):
  is_bst_ind' Leaf s
| is_bst_ind_Node d l r sl sr s
    (Hl: is_bst_ind' l sl)
    (Hr: is_bst_ind' r sr)
    (Hlt: forall xl, sl xl -> xl < d)
    (Hgt: forall xr, sr xr -> d < xr)
    (Hs: forall x, s x <-> x = d \/ sl x \/ sr x):
  is_bst_ind' (Node d l r) s.

Definition is_bst_ind (tr: tree) :=
  exists s, is_bst_ind' tr s.

BST operations

Consider the following operation defined on trees:

Fixpoint member (a: nat) (tr: tree) : bool :=
  match tr with
  | Leaf => false
  | Node v l r =>
      match a ?= v with
      | Lt => member a l
      | Gt => member a r
      | Eq => true
      end
  end.

For each of the following trees, indicate whether member 4 returns the correct result (i.e., returns true when 4 is in the tree, and false when 4 is not in the tree):