(*** Semantics WS 2011 ***)
(*** Coq Part of Assignment 2 ***)
(*** Solution ***)
(*** Exercise 2.1 ***)
Definition swap {X Y : Type} (p : prod X Y) : prod Y X :=
match p with (x,y) => (y,x) end.
Goal forall (X Y : Type) (p : X * Y), swap (swap p) = p.
intros X Y p. destruct p. simpl. reflexivity. Qed.
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.
intros m n. induction m ; simpl. reflexivity.
rewrite IHm. reflexivity. Qed.
(*** Exercise 2.3 ***)
Fixpoint power (x n : nat) : nat :=
match n with
| O => 1
| S n' => x * power x n'
end.
Goal forall x n : nat,
power x n = iter n (mult x) 1.
intros x n. induction n ; simpl. reflexivity.
rewrite IHn. reflexivity. Qed.
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).
Proof.
induction xs ; simpl. reflexivity. rewrite IHxs. reflexivity.
Qed.
Lemma length_app (X : Type) (xs ys : list X) :
length (app xs ys) = (length xs) + (length ys).
Proof.
induction xs ; simpl. reflexivity. rewrite IHxs. reflexivity.
Qed.
Lemma rev_app (X : Type) (xs ys : list X) :
rev (app xs ys) = app (rev ys) (rev xs).
Proof.
induction xs ; simpl. rewrite app_nil. reflexivity.
rewrite <- app_asso. rewrite IHxs. reflexivity.
Qed.
Lemma rev_rev (X : Type) (xs : list X) :
rev (rev xs) = xs.
Proof.
induction xs ; simpl. reflexivity. rewrite rev_app.
simpl. rewrite IHxs. reflexivity.
Qed.
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.
Proof.
revert a. induction xs ; intros a' ; simpl. reflexivity.
rewrite IHxs. rewrite add_S. reflexivity.
Qed.
Lemma length_lengthi {X : Type} (xs : list X) :
length xs = lengthi xs O.
Proof.
rewrite lengthi_length. rewrite add_O. reflexivity.
Qed.
(*** Exercise 2.6 ***)
Definition pred (n : nat) : option nat :=
match n with
| O => None
| S n' => Some n'
end.
(*** Exercise 2.7 ***)
Inductive void := .
Definition fin n := iter n option void.
Definition f (b : bool) : fin 2 := if b then Some None else None.
Definition g (f : fin 2) : bool := match f with None => false | _ => true end.
Goal forall b, g (f b) = b.
destruct b ; reflexivity. Qed.
Goal forall x, f (g x) = x.
destruct x ; simpl. destruct i.
destruct v. reflexivity. reflexivity. Qed.
(*** Exercise 2.8 ***)
Goal forall X:Type, forall x y z:X, x = y -> y = z -> x = z.
intros X x y z A B. rewrite A. rewrite B. reflexivity.
Qed.