(*

                   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.

*)

Inductive Tree (A : Type) :=
  | Empty : Tree A
  | Node : A -> Tree A -> Tree A -> Tree A.

Inductive InTree {A : Type} (x : A) : Tree A -> Prop :=
  | AtNode : forall (y : A) (tl tr : Tree A), x=y \/ InTree x tl \/ InTree x tr -> InTree x (Node _ y tl tr).

Lemma InTreeEmpty {A : Type} : forall (t : Tree A), (forall (x : A), ~InTree x t) <-> t = Empty _.
Proof.
intro; split; intro.
case_eq t; intros.
trivial.
rewrite H0 in H.
specialize H with a.
assert (H1 : InTree a (Node _ a t0 t1)).
apply AtNode.
left.
apply eq_refl.
contradiction.
unfold "~"; intros.
rewrite H in H0.
inversion H0.
Qed.

(*

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).

Class Setoid (A : Type) := {
  sig :> SetoidSig A;
  refl : forall (x : A), x==x;
  sym : forall (x y : A), x==y -> y==x;
  trans : forall (x y z : A), x==y -> y==z -> x==z
}.

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

Instance PermSetoidSig (A : Type) : SetoidSig (Tree A) := {|
  equiv := fun (t1 t2 : Tree A) => forall (x : A), InTree x t1 <-> InTree x t2
|}.

Instance PermSetoid (A : Type) : Setoid (Tree A) := {|
  sig := PermSetoidSig A
|}.
Proof.
unfold "=="; simpl; intros.
reflexivity.
unfold "=="; simpl; intros.
symmetry.
trivial.
unfold "=="; simpl; intros.
rewrite H, H0.
reflexivity.
Qed.