(*** Semantics WS 2011 ***) (*** Coq Part of Assignment 4 ***) (*** Exercise 4.1 ***) Inductive Or (X Y:Prop) : Prop := (*** DEFINITION ***) Goal forall X Y:Prop, Or X Y <-> X \/ Y. (*** PROOF ***) (*** Exercise 4.2 ***) Inductive decp : Prop -> Prop := | decp0 : forall X:Prop, ~X -> decp X | decp1 : forall X:Prop, X -> decp X. Goal forall X:Prop, decp X <-> X \/ ~X. (*** PROOF ***) (*** Exercise 4.3 ***) (*** DEFINITION of Ex ***) Goal forall (X : Type) (p : X -> Prop), Ex X p <-> exists x, p x. (*** PROOF ***) (*** Exercise 4.4 ***) Inductive Eq (X : Type) : X -> X -> Prop := | EqI : forall x, Eq X x x. Goal forall (X : Type) (x y : X) (p : X -> Prop), Eq X x y -> p x -> p y. (*** PROOF ***) Inductive even : nat -> Prop := | evenO : even 0 | evenS : forall n, even n -> even (S (S n)). (*** Exercise 4.5 ***) Goal forall n, even n -> even (pred (pred n)). (*** PROOF ***) Goal forall m n, even m -> even n -> even (m+n). (*** PROOF ***) Goal forall m n, even (m+n) -> even m -> even n. (*** PROOF ***) (*** Exercise 4.6 ***) Fixpoint evenb (n : nat) : bool := match n with | 0 => true | 1 => false | S (S n') => evenb n' end. Goal forall n, (evenb n = true <-> even n) /\ (evenb (S n) = true <-> even (S n)). (*** PROOF ***) (*** Exercise 4.7 ***) Inductive leq : nat -> nat -> Prop := | leqO : forall y, leq 0 y | leqS : forall x y, leq x y -> leq (S x) (S y). Goal forall x y z, leq x y -> leq y z -> leq x z. (*** PROOF ***) (*** Exercise 4.8 ***) Fixpoint leqb (x y : nat) : bool := match x,y with | 0, _ => true | S _, 0 => false | S x', S y' => leqb x' y' end. Goal forall x y, leqb x y = true <-> leq x y. (*** PROOF ***) (*** Exercise 4.9 ***) Fixpoint eq_nat (n m:nat) : bool := (*** DEFINITION ***) Goal forall x y, eq_nat x y = true <-> x = y. (*** PROOF ***) (*** Exercise 4.10 ***) Inductive odd : nat -> Prop := (*** DEFINITION ***) Goal forall x, odd x <-> even (S x). (*** PROOF ***) (*** Exercise 4.11 ***) 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. Inductive rel : exp -> nat -> Prop := (*** DEFINITION ***) Goal forall e n, rel e n <-> evalExp e = n. (*** PROOF ***)