(* Tutorial 9, 5/12/12 Questions for the exam previous exam *) Section ex5. Require Import Coq.Arith.Plus. Fixpoint double (n : nat) {struct n} : nat := match n with | 0 => 0 | S m => S (S (double m)) end. (* It provides the following lemmas: Lemma plus_0_l : forall n, 0 + n = n. Lemma plus_0_r : forall n, n + 0 = n. Lemma plus_comm : forall n m, n + m = m + n. Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. *) Lemma double_lem : forall n:nat, double n = n+n. intro n. induction n; simpl. reflexivity. rewrite IHn. pattern (n + S n). rewrite plus_comm. simpl. reflexivity. Qed. Goal forall (i j k:nat), i*(j+k) = i*j + i*k. intro i. induction i; simpl. intros. reflexivity. intros j k. rewrite IHi. simpl. rewrite -> plus_assoc. pattern (j + k + i * j). rewrite <- plus_assoc. pattern (k + i * j). rewrite plus_comm. rewrite plus_assoc. rewrite plus_assoc. reflexivity. Qed. End ex5. Section ex4. (* 20 points *) (* Prove that the following sets are isomorphic: *) Open Scope type_scope. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. Definition Four1 := bool + bool. Definition Four2 := bool * bool. Definition phi1 : Four1 -> Four2 := fun f1 => match f1 with | inl b => (true, b) | inr b => (false, b) end. Definition psi1 : Four2 -> Four1 := fun f2 => match f2 with | (true, true) => inl true | (true, false) => inl false | (false, true) => inr true | (false, false) => inr false end. Goal forall x : Four1, psi1 (phi1 x) = x. intro x. destruct x; simpl. destruct b; simpl; reflexivity. destruct b; reflexivity. Qed. Goal forall x:Four2, phi1(psi1 x) = x. intro x. destruct x. destruct b; destruct b0; reflexivity. Qed. Variables A B : Set. Definition S := A * (A + B). Definition T := B * A + A * A. Definition phi : S -> T := fun s => match s with | (a , inl a') => inr (a , a') | (a , inr b') => inl (b', a ) end. Definition psi : T -> S := fun t => match t with | inl (b , a) => (a , inr b) | inr (a , a') => (a , inl a') end. Lemma inv : forall s : S, psi(phi s) = s. intro s. destruct s as [a ab]. destruct ab as [a' | b']. simpl. reflexivity. simpl. reflexivity. Qed. (** prove other direction *) End ex4.