(*** Introduction to Computational Logic, Coq part of Assignment 11 ***) (*** Use Coq to complete the file below. If you have any questions, please use the discussion board. http://www.ps.uni-saarland.de/courses/cl-ss11/forum/ ***) Coercion bool2Prop (x : bool) := if x then True else False. Ltac stauto := (simpl ; tauto). Definition bool2sum (b : bool) : b + ~b := if b as z return z + ~z then inl _ I else inr _ (fun f => f). Definition allb (p : bool -> bool) : bool := andb (p false) (p true). Fixpoint Cascade (A B : Type) (n : nat) : Type := match n with | O => B | S n => A -> Cascade A B n end. Notation "A ^ n --> B" := (Cascade A B n) (at level 20). Fixpoint K (A : Type) {B : Type} (b : B) (n : nat) : A ^ n --> B := match n with | O => b | S n => fun _ => K A b n end. Fixpoint comp {A B C : Type} (f : B -> C) (n : nat) : (A ^ n --> B) -> A ^ n --> C := match n with | O => f | S n => fun g => fun x:A => comp f n (g x) end. Fixpoint comp2 {A B C : Type} (f : B -> B -> C) (n : nat) : (A ^ n --> B) -> (A ^ n --> B) -> A ^ n --> C := match n with | O => f | S n => fun g h => fun x:A => comp2 f n (g x) (h x) end. Fixpoint unfoldR {A B : Type} (n : nat) : (A ^ (S n) --> B) -> A ^ n --> (A -> B) := match n with | O => fun g => g | S n => fun g x => unfoldR n (g x) end. Fixpoint foldM {A B : Type} (n : nat) : forall m, (A ^ n --> (A ^ m --> B)) -> A ^ (n + m) --> B := match n as z return forall m, (A ^ z --> (A ^ m --> B)) -> A ^ (z + m) --> B with | O => fun m g => g | S n => fun m g x => foldM n m (g x) end. Inductive ilist (A : Type) : nat -> Type := | nl : ilist A 0 | cns : forall n, A -> ilist A n -> ilist A (S n). Implicit Arguments nl [A]. Implicit Arguments cns [A n]. Infix "::" := cns (at level 60, right associativity). (*** Idea for hd and tl from Chlipala http://adam.chlipala.net/cpdt/html/MoreDep.html ***) Definition hd {A : Type} {n : nat} (al : ilist A (S n)) : A := match al in (ilist _ n') return match n' with O => True | S n'' => A end with | nl => I | cns n' a ar => a end. Definition tl {A : Type} {n : nat} (al : ilist A (S n)) : ilist A n := match al in (ilist _ n') return match n' with O => True | S n'' => ilist A n'' end with | nl => I | cns n' a ar => ar end. Fixpoint Ap {A B : Type} {n : nat} : forall (f : A ^ n --> B) (al : ilist A n), B := match n with | O => fun b _ => b | S n => fun f al => Ap (f (hd al)) (tl al) end. Lemma Ap_K {A B : Type} (b : B) (n : nat) : forall (al : ilist A n), Ap (K A b n) al = b. induction n. intros al. reflexivity. intros al. simpl. apply IHn. Qed. Definition Feq {A B:Type} {n : nat} (f g : A ^ n --> B) : Prop := forall al:ilist A n, Ap f al = Ap g al. Notation "f == g" := (Feq f g) (at level 11). (*** Exercise 1 ***) Lemma K_correct (A B : Type) (b : B) : K A b O = b /\ forall n x, K A b (S n) x = K A b n. (*** INSERT PROOF SCRIPT ***) (*** Exercise 2 ***) Lemma allb_correct (p : bool -> bool) : allb p <-> forall a, p a. (*** INSERT PROOF SCRIPT ***) Lemma allb3 : forall g:bool ^ 3 --> bool, forall x y, comp allb 2 g x y <-> forall z, g x y z. (*** INSERT PROOF SCRIPT ***) (*** Exercise 3 ***) Lemma Ap_mv {A B : Type} {n : nat} (f : A ^ (S n) --> B) (a : A) (al : ilist A n): (*** COMPLETE THE STATEMENT OF THE LEMMA ***). (*** INSERT PROOF SCRIPT ***) Lemma Ap_comp {A B C : Type} (f : B -> C) (n : nat) : forall (g : A ^ n --> B), (*** COMPLETE THE STATEMENT OF THE LEMMA ***). (*** INSERT PROOF SCRIPT ***) Lemma Ap_comp2 {A B C : Type} (f : B -> B -> C) (n : nat) : forall (g h : A ^ n --> B), (*** COMPLETE THE STATEMENT OF THE LEMMA ***). (*** INSERT PROOF SCRIPT ***) (*** Exercise 4 ***) Lemma Feq_comp_K {A B C : Type} (f : B -> C) (b : B) (n : nat) : (*** COMPLETE THE STATEMENT OF THE LEMMA ***). (*** INSERT PROOF SCRIPT ***) Lemma Feq_comp2_K_comp {A B C : Type} (f : B -> B -> C) (b : B) (n : nat) (h : A ^ n --> B) : (*** COMPLETE THE STATEMENT OF THE LEMMA ***). (*** INSERT PROOF SCRIPT ***) (*** Exercise 5 ***) Lemma implb_negb_orb (a b : bool) : implb a b = orb (negb a) b. (*** INSERT PROOF SCRIPT ***) Lemma Feq_implb_negb_orb (n : nat) (g h : bool ^ n --> bool): comp2 implb n g h == comp2 orb n (comp negb n g) h. (*** INSERT PROOF SCRIPT ***) (*** Exercise 6 ***) Section SomeNat. Variable p:nat -> bool. Inductive safe (n : nat) : Prop := | safeI : p n -> safe n | safeS : safe (S n) -> safe n. Definition somec' : forall n, safe n -> sig p := (*** INSERT DEFINITION ***) Lemma safe_O : forall n, safe n -> safe O. (*** INSERT PROOF SCRIPT ***) Defined. Lemma ex_safe : ex p -> safe O. (*** INSERT PROOF SCRIPT ***) Defined. Definition somec : ex p -> sig p := (*** INSERT DEFINITION ***) End SomeNat. (*** Test your function ***) Compute let p x := match x with 50 => true | 100 => true | _ => false end in match (somec p (ex_intro p 100 I)) with exist n _ => n end.