(** Introduction to Formal Reasoning (G52IFR)
    Nicolai Kraus and Nuo Li
    Tutorial 7 : compilers and trees **)

Section Tutorial7.


Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List.
Load Arith.



(** very restricted expressions
    why are they restricted? *)
Inductive Expr : Set :=
| Const : bool -> Expr
| Xor   : Expr -> Expr -> Expr
| Id    : Expr -> Expr.

(* And an evaluator which evaluates these
   boolean expressions. *)
Fixpoint eval (e : Expr) : bool :=





(* Machine code for Boolean expressions.*)
Inductive Op : Set :=
  | Push : bool -> Op
  | XorC : Op
  | IdC : Op.


Definition Code : Set := list Op.

Definition Stack : Set := list bool.



(* and a function which executes the machine code. *)
Fixpoint run (st : Stack)(p : Code) : bool :=


(* We want to implement
   compile : Expr -> Code
   and prove it correct. *)


Fixpoint compile_naive (e : Expr) : Code :=




Lemma compile_lemma : forall e:Expr, forall st: Stack, 
  forall code: Code,
  run st ((compile_naive e) ++ code) = run ((eval e) :: st) code.




Theorem compileOk : forall e:Expr, 
  run nil (compile_naive e) = eval e.
intros.






(** General exercises with trees *)

Set Implicit Arguments.

(* Binary trees with leaves labelled
   with elements of a given set A. *)


Inductive BinTree (A : Set) : Set :=
  | leaf : A -> BinTree A
  | node : BinTree A -> BinTree A -> BinTree A.



(** count the number of elements in a tree *)
Fixpoint count (A : Set) (t : BinTree A) : nat := 




(** we want to flatten the tree, i.e. we want
    to make a list of all elements in the tree *)

Fixpoint flatten (A : Set) (t : BinTree A) : list A :=




(** We want to prove that the length of (flatten t) 
    is equal to the number of elements in t *)

Theorem flattenCount : forall (A: Set) (t: BinTree A),
  (length (flatten t)) = count t.




End Tutorial7.