(*** Semantics WS 2011 ***) (*** Coq Part of Assignment 3 ***) Require Import List. (*** Exercise 3.1 ***) Goal forall X:Prop, ~X <-> ~~~X. (*** Exercise 3.2(a) ***) Goal False <-> forall Z:Prop, Z. (*** Exercise 3.2(b) ***) Goal forall X:Prop, ~X <-> forall Z:Prop, X -> Z. (*** Exercise 3.2(c) ***) Goal forall X:Type, forall x y:X, x = y <-> forall p:X -> Prop, p x -> p y. (*** Exercise 3.2(d) ***) Goal forall X Y:Prop, X /\ Y <-> forall Z:Prop, (X -> Y -> Z) -> Z. (*** Exercise 3.2(e) ***) Goal forall X Y:Prop, X \/ Y <-> forall Z:Prop, (X -> Z) -> (Y -> Z) -> Z. (*** Exercise 3.3(a) ***) Goal forall X Y:Prop, ~(X \/ Y) <-> ~X /\ ~Y. (*** Exercise 3.3(b) ***) Goal forall X Y Z:Prop, (X \/ (Y /\ Z)) <-> (X \/ Y) /\ (X \/ Z). (*** Exercise 3.4 ***) Goal (forall X:Prop, ~~X -> X) -> (forall X:Prop, X \/ ~X). (*** Exercise 3.5(a) ***) Goal forall p:nat -> Prop, forall x:nat, p 0 -> (forall x:nat, p x -> p (S x)) -> p x. (*** Exercise 3.5(b) ***) Goal forall X:Type, forall p:list X -> Prop, forall xs:list X, p nil -> (forall x:X, forall xs:list X, p xs -> p (x :: xs)) -> p xs. (*** The following code is from the lecture on compiler correctness and is relevant for some of the last problems on the assignment. ***) Inductive binop : Type := Plus | Times. Inductive exp : Type := | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. Definition evalBinop (b : binop) : nat -> nat -> nat := match b with | Plus => plus | Times => mult end. Fixpoint evalExp (e : exp) : nat := match e with | Const n => n | Binop b e1 e2 => (evalBinop b) (evalExp e1) (evalExp e2) end. Definition test : exp := Binop Times (Binop Plus (Const 2) (Const 3)) (Const 4). Compute evalExp test. (* Stack machine *) Inductive instr : Type := | iConst : nat -> instr | iBinop : binop -> instr. Definition prog := list instr. Definition stack := list nat. Definition runInstr (i : instr) (s : stack) : option stack := match i with | iConst n => Some (n :: s) | iBinop b => match s with | arg1 :: arg2 :: s' => Some ((evalBinop b) arg1 arg2 :: s') | _ => None end end. Fixpoint runProg (p : prog) (s : stack) : option stack := match p with | nil => Some s | i :: p' => match runInstr i s with | None => None | Some s' => runProg p' s' end end. (* Compiler *) Fixpoint compile (e : exp) : prog := match e with | Const n => iConst n :: nil | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil end. Compute compile test. Compute runProg (compile test) nil. (* Correctness *) Lemma compile_correct' e p s: runProg (compile e ++ p) s = runProg p (evalExp e :: s). Proof. revert p s. induction e ; intros p s. simpl. reflexivity. simpl. rewrite <- app_assoc. rewrite IHe2. rewrite <- app_assoc. rewrite IHe1. simpl. reflexivity. Qed. Theorem compile_correct e s : runProg (compile e) s = Some (evalExp e :: s). Proof. rewrite <- (app_nil_r (compile e)). rewrite compile_correct'. simpl. reflexivity. Qed.