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