(*** Semantics WS 2011 ***) (*** Coq Part of Assignment 2 ***) (*** Exercise 2.1 ***) (*** Define swap ***) Goal forall (X Y : Type) (p : X * Y), swap (swap p) = p. (*** Insert Proof ***) Fixpoint iter (n : nat) {X : Type} (f : X -> X) (x : X) : X := match n with | O => x | S n' => f (iter n' f x) end. (*** Exercise 2.2 ***) Goal forall m n : nat, m*n = iter m (plus n) 0. (*** Insert Proof ***) (*** Exercise 2.3 ***) (*** Define power ***) Goal forall x n : nat, power x n = iter n (mult x) 1. (*** Insert Proof ***) Fixpoint rev {X:Type} (l:list X) : list X := match l with | nil => nil | cons x l' => app (rev l') (x :: nil) end. Lemma app_nil (X : Type) (xs : list X) : app xs nil = xs. Proof. induction xs ; simpl. reflexivity. rewrite IHxs. reflexivity. Qed. (*** Exercise 2.4 ***) Lemma app_asso (X : Type) (xs ys zs : list X) : app (app xs ys) zs = app xs (app ys zs). (*** Insert Proof ***) Lemma length_app (X : Type) (xs ys : list X) : length (app xs ys) = (length xs) + (length ys). (*** Insert Proof ***) Lemma rev_app (X : Type) (xs ys : list X) : rev (app xs ys) = app (rev ys) (rev xs). (*** Insert Proof ***) Lemma rev_rev (X : Type) (xs : list X) : rev (rev xs) = xs. (*** Insert Proof ***) Lemma add_O (x : nat) : x + O = x. Proof. induction x ; simpl. reflexivity. rewrite IHx. reflexivity. Qed. Lemma add_S (x y : nat) : x + (S y) = S (x + y). Proof. induction x ; simpl. reflexivity. rewrite IHx. reflexivity. Qed. (*** Exercise 2.5 ***) Fixpoint lengthi {X : Type} (xs : list X) (a : nat) := match xs with | nil => a | cons _ xr => lengthi xr (S a) end. Lemma lengthi_length {X : Type} (xs : list X) (a : nat) : lengthi xs a = (length xs) + a. (*** Insert Proof ***) Lemma length_lengthi {X : Type} (xs : list X) : length xs = lengthi xs O. (*** Insert Proof ***) (*** Exercise 2.6 ***) Definition pred (n : nat) : option nat := (*** Insert Definition ***) (*** Exercise 2.7 ***) Inductive void := . Definition fin n := iter n option void. Definition f (b : bool) : fin 2 := (*** Insert Definition ***) Definition g (f : fin 2) : bool := (*** Insert Definition ***) Goal forall b, g (f b) = b. (*** Insert Proof ***) Goal forall x, f (g x) = x. (*** Insert Proof ***) (*** Exercise 2.8 ***) Goal forall X:Type, forall x y z:X, x = y -> y = z -> x = z. (*** Insert Proof ***)