(*** Semantics, Coq part of Assignment 13 ***) (*** Use Coq to complete the file below. If you have any questions, please use the discussion board. http://www.ps.uni-saarland.de/courses/sem-ws13-forum ***) (*** Semantics, Coq part of Assignment 13 ***) (*** Use Coq to complete the file below. If you have any questions, please use the discussion board. http://www.ps.uni-saarland.de/courses/sem-ws13-forum ***) (* * Exercise 13.1 *) Definition nat_elim (A : nat -> Type) (n : nat) (s1 : A 0) (s2 : forall n, A n -> A (S n)) : A n := (*** FILL IN HERE ***) (* * Exercise 13.2 *) Inductive sigma (A : Type) (B : A -> Type) : Type := | pair (a : A) (b : B a). Arguments pair {A B} a b. Module DepPair. Definition pi1 A B (p : sigma A B) : A := (*** FILL IN HERE ***) Definition pi2 A B (p : sigma A B) : B (pi1 A B p) := (*** FILL IN HERE ***) End DepPair. (* * Exercise 13.3 *) Inductive times (A B : Type) : Type := | npair (a : A) (b : B). Module NDepPair. Definition pi1 {A B} (p : times A B) : A := (*** FILL IN HERE ***) Definition pi2 {A B} (p : times A B) : B := (*** FILL IN HERE ***) Definition times_elim A B C (p : times A B) (f : A -> B -> C) : C := (*** FILL IN HERE ***) End NDepPair. (* * Exercise 13.4 *) Definition eq {A : Type} : A -> A -> Prop := fun a b => forall P : A -> Prop, P b -> P a. Definition refl {A : Type} (a : A) : eq a a := fun P pa => pa. Definition sigma_elim {A B} (p : sigma A B) (P : sigma A B -> Type) (s : forall a b, P (pair a b)) : P p := (*** FILL IN HERE ***) Module Sigma. Definition pi1 {A B} (p : sigma A B) : A := (*** FILL IN HERE ***) Definition pi2 {A B} (p : sigma A B) : B (pi1 p) := (*** FILL IN HERE ***) Definition eta {A B} (p : sigma A B) : eq p (pair (pi1 p) (pi2 p)) := (*** FILL IN HERE ***) Definition sigma_ind {A B} (p : sigma A B) (P : sigma A B -> Prop) (s : forall a b, P (pair a b)) : P p := (*** FILL IN HERE ***) End Sigma.