(** 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 := match e with | Const b => b | Xor e1 e2 => xorb (eval e1) (eval e2) | Id e => eval e end. (* Machine code for Boolean expressions. It is for stack *) 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. The machine returns false as default *) Fixpoint run (st : Stack)(p : Code) : bool := match p with | nil => match st with | nil => false | b :: st => b end | op :: p' => match op with | Push b => run (b :: st) p' | XorC => match st with | nil => false | _ :: nil => false | b2 :: b1 :: st' => run ((xorb b1 b2) ::st') p' end | IdC => run st p' end end. (* We want to implement compile : Expr -> Code and prove it correct. *) Fixpoint compile_naive (e : Expr) : Code := match e with | Const b => (Push b) :: nil | Xor b1 b2 => (compile_naive b1) ++ (compile_naive b2) ++ XorC :: nil | Id b => (compile_naive b) ++ IdC :: nil end. Lemma compile_lemma : forall e:Expr, forall st: Stack, forall code: Code, run st ((compile_naive e) ++ code) = run ((eval e) :: st) code. intro e. induction e; simpl. reflexivity. intros. rewrite (app_ass (compile_naive e1) (compile_naive e2 ++ XorC :: nil) code). rewrite IHe1. rewrite app_ass. rewrite IHe2. simpl. reflexivity. intros; simpl. rewrite app_ass. rewrite IHe. simpl. reflexivity. Qed. Theorem compileOk : forall e:Expr, run nil (compile_naive e) = eval e. intros. pattern (compile_naive e). rewrite <- app_nil_r. rewrite compile_lemma. simpl. reflexivity. Qed. (** 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 := match t with | (leaf _) => 1 | (node t1 t2) => (count t1) + (count t2) end. list - non-deterministic monadplus for maybe : simple try and catch Either e a for either e we can define a monad which does for each exception e we return something (** 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 := match t with | leaf a => a :: nil | node t1 t2 => (flatten t1) ++ (flatten t2) end. (** 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. intros. induction t; simpl. reflexivity. (** check the Coq library *) rewrite app_length. rewrite IHt1. rewrite IHt2. reflexivity. Qed. End Tutorial7.