(*|
========
 Quiz 2
========

.. raw:: html

   <label class="reveal-solutions"><input type="checkbox">Reveal solutions</label>

Grading scheme
==============

- +1 for correct answers
- -0.5 for incorrect answers

.. coq:: none
|*)

From Stdlib Require Import Bool Arith List.
Import ListNotations.

(*|
Binary search trees
===================

We define trees as in the lab:
|*)

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

(*|
.. coq:: none
|*)

Fixpoint bst (tr : tree) (s : nat -> Prop) : Prop :=
  match tr with
  | Leaf => forall x, not (s x)
  | Node d l r =>
      s d /\
      bst l (fun x => s x /\ x < d) /\
      bst r (fun x => s x /\ d < x)
  end.

(*|
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:

.. exercise:: Singleton

   Is the following a binary search tree?
|*)

Definition lf :=
  Leaf.

(*|
   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal bst lf (fun _ => False).
Proof. firstorder. Qed.

(*|
.. exercise:: Left comb

   Is the following a binary search tree?
|*)

Definition lcomb :=
  Node 0 Leaf (Node 1 Leaf (Node 2 Leaf Leaf)).

(*|
   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

From Stdlib Require Import Lia.
Goal bst lcomb (fun x => 0 <= x <= 2).
Proof. cbv; intuition; lia. Qed.

(*|
.. exercise:: Right comb

   Is the following a binary search tree?
|*)

Definition rcomb :=
  Node 0 (Node 1 (Node 2 Leaf Leaf) Leaf) Leaf.

(*|
   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal forall s, ~ bst rcomb s.
Proof. cbv; lia. Qed.

(*|
.. exercise:: Left fold

   Is the following a binary search tree?
|*)

   Fixpoint fl (l: list nat) (tr: tree) : tree :=
     match l with
     | [] => tr
     | hd :: tl => fl tl (Node hd Leaf tr)
     end.

   Definition lc :=
     fl [0;1;2;3;4] Leaf.

(*|
   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal forall s, ~ bst lc s.
Proof. cbv; lia. Qed.

(*|
.. exercise:: Right fold

   Is the following a binary search tree?
|*)

   Fixpoint fr (l: list nat) (tr: tree) : tree :=
     match l with
     | [] => tr
     | hd :: tl => Node hd (fr tl tr) Leaf
     end.

   Definition rc :=
     fr [0;1;2;3;4] Leaf.

(*|
   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal forall s, ~ bst rc s.
Proof. cbv; lia. Qed.

(*|
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.

(*|
.. exercise:: Top soundness

   Is `is_bst_yes` sound?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal ~ sound is_bst_yes.
Proof.
  intros Hs.
  destruct (Hs (Node 0 (Node 1 Leaf Leaf) Leaf)) as [s Ht].
  all: cbv in *; lia.
Qed.

(*|
.. exercise:: Top completeness

   Is `is_bst_yes` complete?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal complete is_bst_yes.
Proof. firstorder. Qed.

(*|
Consider the following definition:
|*)

Definition is_bst_no (tr: tree) :=
  False.

(*|
.. exercise:: Bottom soundness

   Is `is_bst_no` sound?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal sound is_bst_no.
Proof. firstorder. Qed.

(*|
.. exercise:: Bottom completeness

   Is `is_bst_no` complete?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal ~ complete is_bst_no.
Proof.
  intros Hs.
  apply (Hs Leaf).
  exists (fun _ => False); firstorder.
Qed.

(*|
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.

(*|
.. exercise:: Fixpoint soundness

   Is `is_bst_fx` sound?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal ~ sound is_bst_fx.
Proof.
  intros Hs.
  destruct (Hs (Node 1
                  (Node 0
                     Leaf
                     (Node 2 Leaf Leaf))
                  Leaf)) as [s Ht].
  all: cbv in *; lia.
Qed.

(*|
.. exercise:: Fixpoint completeness

   Is `is_bst_fx` complete?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal complete is_bst_fx.
Proof.
  unfold complete; induction tr; intros [s Ht].
  - reflexivity.
  - simpl in *.
    destruct Ht as (Hd & H1 & H2).
    specialize (IHtr1 ltac:(eauto)).
    specialize (IHtr2 ltac:(eauto)).
    destruct tr1, tr2; simpl in *; intuition.
Qed.

(*|
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.

(*|
.. exercise:: Inductive soundness

   Is `is_bst_ind` sound?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Lemma bst_iff :
  forall tr s1 s2,
    (forall x, s1 x <-> s2 x) ->
    (bst tr s1 <-> bst tr s2).
Proof.
  induction tr; simpl; intros s1 s2 Ht.
  - firstorder.
  - rewrite Ht, IHtr1, IHtr2.
    reflexivity.
    all: simpl; intros; rewrite Ht; reflexivity.
Qed.

Lemma is_bst_ind'_sound tr s:
  is_bst_ind' tr s ->
  bst tr s.
Proof.
  induction 1; simpl.
  - firstorder.
  - rewrite (bst_iff l), (bst_iff r), Hs.
    + intuition eauto.
    + firstorder lia.
    + firstorder lia.
Qed.

Goal sound is_bst_ind.
Proof.
  intros tr [s Hs%is_bst_ind'_sound]; eauto.
Qed.

(*|
.. exercise:: Inductive completeness

   Is `is_bst_ind` complete?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Lemma is_bst_ind'_complete tr: forall s,
    bst tr s ->
    is_bst_ind' tr s.
Proof.
  induction tr; simpl.
  - econstructor; firstorder.
  - intros s (Hd & H1 & H2).
    econstructor; eauto; simpl; try lia.
    intros x; assert (x = d \/ x < d \/ d < x) by lia.
    intuition (subst; eauto).
Qed.

Goal complete is_bst_ind.
Proof.
  intros tr [s Hs%is_bst_ind'_complete]; red; eauto.
Qed.

(*|
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):

.. exercise:: `tree1`

   .. coq::
|*)

Definition tree1 :=
  Node 3 (Node 4 Leaf Leaf)
    (Node 5 (Node 2 Leaf Leaf) Leaf).

(*|
   Does `member 4 tree1` return the right result?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal member 4 tree1 = false. Proof. reflexivity. Qed.

(*|
.. exercise:: `tree2`

   .. coq::
|*)

Definition tree2 :=
  Node 3 (Node 4 Leaf Leaf)
    (Node 2 Leaf (Node 4 Leaf Leaf)).

(*|
   Does `member 4 tree2` return the right result?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal member 4 tree2 = true. Proof. reflexivity. Qed.

(*|
.. exercise:: `tree3`

   .. coq::
|*)

Definition tree3 :=
  Node 3 Leaf (Node 5 Leaf Leaf).

(*|
   Does `member 4 tree3` return the right result?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal member 4 tree3 = false. Proof. reflexivity. Qed.