(*

                   COSC 5V90 - Fall 2016
                         FINAL EXAM
                     December 07, 2016
                       9:00am-10:30am
                          MCD 205

Make sure that you read all questions and hints carefully!!!

*)

Require Import Setoid.

(*

Question 1:
a) Define a data type of binary trees with elements from A as follows. There should 
   be an empty tree and at each inner node of the tree an element of type A is stored. 
   Example of a tree with nat elements (E denotes the empty tree):
           0
         /   \
        1     2
       / \   / \
      2   E E   E
     / \
    E   E
   Hint: - Use Empty : forall (A : Type), Tree A as the constructor for the empty tree.
b) Define a property, i.e., a date type of kind Prop, InTree so that InTree x t for
   an element x of type A and a tree t with elements from A can be proven iff x is
   somewhere in the tree. For example, if t is the tree from a), then InTree 2 t can be
   shown, i.e., there is an element p of type InTree 2 t, but InTree 4 t cannot be shown.
   Hint: - No additional functions or other means are needed.
         - One case, i.e., one constructor, is sufficient. 
c) Prove the following fact about empty trees. The property states that a tree is empty 
   iff it does not contain any elements.
   Hint: - Split the <->, i.e., show each implication separately.
         - In the proof of -> do a case distinction on t (use case_eq t). In the
           non-empty case for t assert and show that t has an element and use this
           to contradict the assumption (t has no elements).
         - Start the proof of <- with unfold "~"; intros.

*)

Lemma InTreeEmpty {A : Type} : forall (t : Tree A), (forall (x : A), ~InTree x t) <-> t = Empty _.
Proof.
Admitted.

(*

Question 2:
a) Define a class Setoid A for every type A that uses a SetoidSig A and requires that
   equiv is an equivalence relation.
   Hint: - Use :> in order to make SetoidSig A a substructure of Setoid A.
         - An equivalence relation == is 
           + reflexive, i.e., x==x for all x,
           + symmetric, i.e., x==y implies y==x for all x and y,
           + transitive, i.e., x==y and y==z implies x==z for all x, y and z.

*)

Class SetoidSig (A : Type) := {
  equiv : A -> A -> Prop
}.

Infix "==" := (equiv) (at level 50).

(*
b) Make Tree A an instance of Setoid (and SetoidSig). Two trees t1, t2 are considered
   equivalent t1==t2 iff they contain exactly the same elements, i.e., 
   InTree x t1 <-> InTree x t2 for all x.
   Hint: - Start the proof of each of the three properties of an equivalence relation
           by unfold "=="; simpl; intros.
*)