(*** Introduction to Computational Logic, Coq part of Assignment 13 ***) (*** Use Coq to experiment with 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). (*** 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 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. (*** 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). (*** 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). (*** 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. (*** Boolean Logic ***) Section BL. 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). 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_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). Definition bfeqc (n:nat) (g h : bool ^ n --> bool) : {a:ilist bool n|Ap g a <> Ap h a} + {forall a:ilist bool n, Ap g a = Ap h a}. induction n as [|n IHn]. destruct g; destruct h ; try tauto. left. exists nl. discriminate. left. exists nl. discriminate. destruct (IHn (g false) (h false)) as [ [a H]|H]. left. exists (false::a). exact H. destruct (IHn (g true) (h true)) as [ [a H']|H']. left. exists (true::a). exact H'. right. intros a. simpl. destruct (hd a). apply H'. apply H. Defined. (*** If (Beqc s t) reduces to 'inleft ...', then s and t are not equivalent. ***) (*** If (Beqc s t) reduces to 'inright ...', then s and t are equivalent. ***) Definition Beqc {n:nat} (s t : B n) : {a:ilist bool n|Ap [[s]] a <> Ap [[t]] a} + {forall a:ilist bool n, Ap [[s]] a = Ap [[t]] a}. exact (bfeqc n [[s]] [[t]]). Defined. Definition bfvalc (n:nat) (g : bool ^ n --> bool) : {a:ilist bool n|~ Ap g a} + {forall a:ilist bool n, Ap g a}. destruct (bfeqc n g (K bool true n)) as [ [a H] | H]. left. exists a. intros H'. apply H. rewrite Ap_K. destruct (Ap g a). reflexivity. contradiction H'. right. intros a. rewrite H, Ap_K. exact I. Defined. (*** If (Bvalc s) reduces to 'inleft ...', then s is not valid. ***) (*** If (Bvalc s) reduces to 'inright ...', then s is valid. ***) Definition Bvalc {n:nat} (s : B n) : {a:ilist bool n|~ Ap [[s]] a} + {forall a:ilist bool n, Ap [[s]] a}. exact (bfvalc n [[s]]). Defined. (*** Exercise 1 ***) (*** Which of 9 given formulas in B 2 are equivalent. ***) (*** You do not need to type in all 9 * 8 = 72 possible pairs. You can type in any you are not sure about. Make sure you understand why each pair is or is not equivalent. ***) (*** (a) x_0 and (b) # are not equivalent: ***) Compute (Beqc F02 #). (*** (c) # ==> # and (d) x_0 ==> x_0 are equivalent: ***) Compute (Beqc (# ==> #) (F02 ==> F02)). (*** ... ***) (*** Exercise 2 ***) (*** Which of 5 given formulas in B 2 are valid. ***) (*** (a) x_0 ***) Compute (Bvalc F02). (*** ... ***) End BL. (*** Quantified Boolean Logic ***) Section QBF. Inductive Q (n : nat) : Type := | Q_Var : Fin n -> Q n | Q_Fal : Q n | Q_Imp : Q n -> Q n -> Q n | Q_All : Q (S n) -> Q n. Implicit Arguments Q_Var [n]. Local Coercion Q_Var : Fin >-> Q. Implicit Arguments Q_Fal [n]. Implicit Arguments Q_Imp [n]. Local Notation "#" := Q_Fal. Local Notation "s ==> t" := (Q_Imp s t) (at level 90, right associativity). Local Notation "'ALL' x , s " := (Q_All x s) (at level 100). Definition allb (p : bool -> bool) : bool := andb (p false) (p true). Definition All (n:nat) (g:bool ^ (S n) --> bool) : bool ^ n --> bool := comp allb n (unfoldR n g). Fixpoint Q_Den {n : nat} (s : Q n) : bool ^ n --> bool := match s with | Q_Var k => P k | Q_Fal => K bool false n | Q_Imp s1 s2 => Impl n (Q_Den s1) (Q_Den s2) | Q_All s1 => All n (Q_Den s1) end. Implicit Arguments Q_Den [n]. Local Notation "[[ s ]]" := (Q_Den s). (*** Exercise 3 ***) (*** Compute the values of 6 formulas in Q 0 ***) (*** (a) forall x_0, x_0 ***) Compute [[ALL 0, F01]]. (*** ... ***)