(*** Introduction to Computational Logic, Coq part of Assignment 12 ***) (*** 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/ ***) (*** Cascaded functions ***) 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 => fun b => f b | 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 => fun b b' => f b b' | S n => fun g h => fun x:A => comp2 f n (g x) (h 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. (*** length indexed lists (lists carrying length) ***) 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]. Notation "s :: t" := (cns s t) (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. Lemma Ap_mv {A B : Type} {n : nat} (g : A ^ (S n) --> B) (a : A) (al : ilist A n): Ap (g a) al = Ap g (cns a al). simpl. reflexivity. Qed. Lemma Ap_comp {A B C : Type} (f : B -> C) (n : nat) : forall (g : A ^ n --> B), forall al:ilist A n, Ap (comp f n g) al = f (Ap g al). induction n. intros g al. reflexivity. intros g al. simpl. apply IHn. Qed. Lemma Ap_comp2 {A B C : Type} (f : B -> B -> C) (n : nat) : forall (g h : A ^ n --> B), forall al:ilist A n, Ap (comp2 f n g h) al = f (Ap g al) (Ap h al). induction n. intros g h al. reflexivity. intros g h 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). Fixpoint append {A : Type} {n m:nat} (a:ilist A n) (b:ilist A m) : ilist A (n + m) := match a with | nl => b | cns n s a => s::(append a b) end. Notation "s ++ t" := (append s t) (at level 60, right associativity). (*** Exercise 1: Study this proof. Make sure you understand the goals at each step. ***) Lemma Ap_append {A B : Type} {n m:nat} (g:A ^ n --> (A ^ m --> B)) (al1:ilist A n) (al2:ilist A m) : Ap (Ap g al1) al2 = Ap (foldM n m g) (al1 ++ al2). revert g. induction al1. intros g. simpl. reflexivity. intros g. simpl. exact (IHal1 (g a)). Qed. (*** Fin ***) Inductive Fin : nat -> Type := | FinO : forall {n}, Fin (S n) | FinS : forall {n}, Fin n -> Fin (S n). Definition Fin0E (k : Fin 0) (A:Type) : A := match k in Fin n return match n with O => A | S _ => True end with | FinO _ => I | FinS _ _ => I end. Definition F01 : Fin 1 := FinO. Definition F02 : Fin 2 := FinO. Definition F12 : Fin 2 := FinS FinO. Definition F03 : Fin 3 := FinO. Definition F13 : Fin 3 := FinS FinO. Definition F23 : Fin 3 := FinS (FinS FinO). Fixpoint FinVal {n : nat} (m : Fin n) : nat := match m with | FinO n' => 0 | FinS n' m' => S (FinVal m') end. (*** Projections ***) Fixpoint P {A : Type} {n : nat} (k : Fin n) : A ^ n --> A := match k in Fin n' return A ^ n' --> A with | FinO n' => fun a => K A a n' | FinS n' k' => fun _ => P k' end. (*** Exercise 4 ***) Lemma Pex1 : comp negb 1 (P F01) == negb. (*** INSERT PROOF SCRIPT ***) Qed. Lemma Pex2 : comp2 implb 2 (P F02) (P F12) == (fun x y => implb x y) \/ comp2 implb 2 (P F02) (P F12) == (fun x y => implb y x). (*** INSERT PROOF SCRIPT ***) Qed. Lemma Pex3 : comp2 implb 2 (P F12) (P F02) == (fun x y => implb x y) \/ comp2 implb 2 (P F12) (P F02) == (fun x y => implb y x). (*** INSERT PROOF SCRIPT ***) Qed. (*** Exercise 5 ***) Fixpoint get {A : Type} {n : nat} (k : Fin n) : ilist A n -> A := (*** INSERT DEFINITION ***) (*** Informative inversion function ***) Definition Fin_Inv {n:nat} (k:Fin n) : match n as z return Fin z -> Type with | O => fun k => False | S n' => fun k => {k'| k = FinS k'} + {k = FinO} end k. (*** INSERT DEFINITION AS A SCRIPT ***) Defined. (*** Exercise 6 ***) Definition predFin {n : nat} (x : Fin n) : option (Fin (pred n)). (*** INSERT DEFINITION AS A SCRIPT ***) Defined. Lemma predFin_correct {n:nat} : predFin (@FinO n) = None /\ forall (k:Fin (S n)), predFin (FinS k) = Some k. (*** INSERT PROOF SCRIPT ***) Qed. (*** Exercise 7 ***) Lemma Fin1 (k:Fin 1) : k = FinO. (*** INSERT PROOF SCRIPT ***) Qed. (*** Boolean Logic ***) Section BEn. Variable n : nat. Inductive B : Type := | B_Var : Fin n -> B | B_Fal : B | B_Imp : B -> B -> B. Local Notation "#" := B_Fal. Local Notation "s ==> t" := (B_Imp s t) (at level 90, right associativity). Definition B_Tru : B := (# ==> #). Definition B_Not (s : B) : B := (s ==> #). Definition B_And (s t:B) : B := (B_Not (s ==> B_Not t)). Definition Impl (g h:bool ^ n --> bool) : bool ^ n --> bool := comp2 implb n g h. Fixpoint B_Den (s : B) : bool ^ n --> bool := match s with | B_Var k => P k | B_Fal => K bool false n | B_Imp s1 s2 => Impl (B_Den s1) (B_Den s2) end. Local Notation "[[ s ]]" := (B_Den s). (*** Exercise 8 ***) Lemma B_NotTru_Fal_ex : (B_Not B_Tru) = B_Fal \/ (B_Not B_Tru) <> B_Fal. (*** INSERT PROOF SCRIPT ***) Qed. Lemma B_NotTru_Fal_ex2 : [[B_Not B_Tru]] == [[B_Fal]] \/ ~ [[B_Not B_Tru]] == [[B_Fal]]. (*** INSERT PROOF SCRIPT ***) Qed. (*** Exercise 9 ***) Definition B_Or (s t : B) : B := (*** INSERT DEFINITION ***) Lemma B_Or_orb (s t : B) : [[B_Or s t]] == (comp2 orb n [[s]] [[t]]). (*** INSERT PROOF SCRIPT ***) Qed. End BEn. Implicit Arguments B_Var [n]. Local Coercion B_Var : Fin >-> B. Implicit Arguments B_Fal [n]. Implicit Arguments B_Imp [n]. Implicit Arguments B_Not [n]. Implicit Arguments B_And [n]. Implicit Arguments B_Den [n]. Local Notation "#" := B_Fal. Local Notation "s ==> t" := (B_Imp s t) (at level 90, right associativity). Local Notation "[[ s ]]" := (B_Den s). (*** Exercise 11 ***) Lemma exg : let g := fun a b c => match a,b,c with true,true,false => false | _,_,_ => true end in {s:B 3|[[s]] == g}. exists (*** INSERT TERM ***) intros a. simpl. destruct (hd a) ; destruct (hd (tl a)) ; destruct (hd (tl (tl a))) ; reflexivity. Qed.