(*** 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-ss12/forum/
***)

Set Implicit Arguments. Unset Strict Implicit.
Require Import Bool List Omega Setoid Recdef.
Notation "[ a , .. , b ]" := (a :: .. (b :: nil) ..).
Coercion bool2Prop (x : bool) : Prop := if x then True else False.

Definition var := nat.

Inductive form : Type :=
| Var : var -> form
| Imp : form -> form -> form
| Fal : form.

Definition Not (s : form) : form :=
Imp s Fal.

Definition FK (s t : form) : form :=
Imp s (Imp t s).

Definition FS (s t u : form) : form :=
(Imp (Imp s (Imp t u))
(Imp (Imp s t)
(Imp s u))).

Definition FE (s : form) : form :=
Imp Fal s.

Definition FDN (s : form) : form :=
Imp (Not (Not s)) s.

Definition context := list form.

Inductive mem (X : Type) (x : X) : list X -> Prop :=
| memH xs : mem x (x::xs)
| memT y xs : mem x xs -> mem x (y::xs).

Fixpoint eq_nat (x y : nat) : bool :=
match x, y with
| 0, 0 => true
| S x', S y' => eq_nat x' y'
| _, _ => false
end.

(*** From Week 11 ***)
(** Boolean Reflection *)

Lemma negb_ref (x : bool) :
negb x <-> ~x.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma andb_ref x y :
x && y <-> x /\ y.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma orb_ref x y :
x || y <-> x \/ y.

Proof. destruct x ; simpl ; tauto. Qed.

Lemma implb_ref x y :
implb x y <-> x -> y.

Proof. destruct x ; simpl ; tauto. Qed.

Definition inb (x : nat) (xs : list nat) : bool :=
if in_dec eq_nat_dec x xs then true else false.

Lemma inb_ref x A :
inb x A <-> In x A.

Proof. unfold inb. destruct (in_dec eq_nat_dec x A) ; simpl ; tauto. Qed.

Lemma forallb_ref X f A :
forallb f A <-> forall x : X, In x A -> f x.

Proof. induction A ; simpl. now firstorder.
rewrite andb_ref, IHA. split.
intros [B C] x [D|D]. congruence. now auto.
firstorder. Qed.

(** Boolean Satisfiability *)

Definition assignment := list var.

Fixpoint eval (a : assignment) (s : form) : bool :=
match s with
| Var x => inb x a
| Imp s t => implb (eval a s) (eval a t)
| Fal => false
end.

Definition eva (a : assignment) (G : list form) : bool :=
forallb (eval a) G.

Definition sat (G : list form) : Prop := 
exists a, eva a G.

Inductive nd : list form -> form -> Prop :=
| ndA G s :
  nd (s::G) s
| ndW G s t :
  nd G s -> nd (t::G) s
| ndII G s t :
  nd (s::G) t -> nd G (Imp s t)
| ndIE G s t :
  nd G (Imp s t) -> nd G s -> nd G t
| ndE G s :
  nd G Fal -> nd G s.

Lemma nd_sound G s a :
nd G s -> eva a G -> eval a s.

Proof. intros A B ; induction A ; simpl in *|-*.
(* ndA *) now destruct (eval a s) ; simpl ; auto. 
(* ndW *) now destruct (eval a t) ; simpl in B ; auto.
(* ndII *) now destruct (eval a s) ; simpl in *|- ; auto.
(* nd IE *) now destruct (eval a s) ; simpl in *|- ; auto.
(* ndC *) now destruct (eval a s) ; simpl in *|- ; auto. Qed.

Definition x := Var 0.
Definition y := Var 1.
Definition z := Var 2.

Lemma indep1 : ~nd [x] Fal.
Proof. intros B.
assert (C:eva [0] [x]). simpl. tauto.
assert (D:~eval [0] Fal). simpl. tauto.
apply D. now apply nd_sound with (G := [x]).
Qed.

Lemma indep2 : ~nd [Not x] Fal.
Proof. intros B.
assert (C:eva nil [Not x]). simpl. tauto.
assert (D:~eval nil Fal). simpl. tauto.
apply D. now apply nd_sound with (G := [Not x]).
Qed.

(*** Prop versions ***)
Fixpoint forcesP (W : list assignment) (a : assignment) (s : form) : Prop :=
match s with
| Var x => In x a
| Imp s t => forall a', In a' W -> incl a a' -> forcesP W a' s -> forcesP W a' t
| Fal => False
end.

Definition forces'P (W : list assignment) (a : assignment) (G : list form) : Prop :=
forall s, In s G -> forcesP W a s.

Lemma monotone_forcesP (W : list assignment) (a a' : assignment) (s : form) :
In a' W -> incl a a' -> forcesP W a s -> forcesP W a' s.
Proof. intros A' B C. destruct s.
simpl. apply B. exact C.
intros a'' A'' B' C'. apply C; try assumption.
now apply incl_tran with (m := a').
contradiction C.
Qed.

Lemma soundnessKP (W : list assignment) G s : nd G s ->
forall a, In a W -> forces'P W a G -> forcesP W a s.
Proof. intros D. induction D; try now firstorder.
intros a A B a' A' B' C.
apply IHD. assumption.
intros u [E|E].
rewrite <- E. assumption.
apply monotone_forcesP with (a := a); try assumption.
apply B. assumption.
Qed.

(*** Boolean versions ***)
Definition inclb (a a':list nat) : bool :=
forallb (fun x => inb x a') a.

Lemma inclb_ref (a a':list nat) :
inclb a a' <-> incl a a'.
Proof. induction a. simpl. unfold incl. now firstorder.
simpl. case_eq (inb a a'); simpl. intros A.
assert (B:In a a'). apply inb_ref. rewrite A; simpl; tauto.
rewrite IHa. unfold incl. simpl. split.
intros C b [D|D]. rewrite <- D. assumption. now apply C.
now firstorder.
intros A. split. tauto.
assert (B:~In a a'). rewrite <- inb_ref. rewrite A. simpl; tauto.
unfold incl; simpl. now firstorder.
Qed.

Notation "w --> w'" := (implb w w').
Notation "w <= w'" := (inclb w w').

Fixpoint forces (W : list assignment) (w : assignment) (s : form) : bool :=
match s with
| Var x => inb x w
| Imp s t => forallb (fun w' => (w <= w') --> (forces W w' s) --> (forces W w' t)) W
| Fal => false
end.

Definition forces' (W : list assignment) (w : assignment) (G : list form) : bool :=
forallb (forces W w) G.

Lemma forces_ref W w s : forces W w s <-> forcesP W w s.
Proof. revert w. induction s; intros w. simpl. now apply inb_ref.
simpl. rewrite forallb_ref. split.
intros A a. specialize (A a).
rewrite implb_ref in A. rewrite implb_ref in A. rewrite inclb_ref in A. now firstorder.
intros A a. specialize (A a).
rewrite implb_ref. rewrite implb_ref. rewrite inclb_ref. now firstorder.
simpl. tauto. Qed.

Lemma forces'_ref W w G : forces' W w G <-> forces'P W w G.
Proof. induction G. simpl. unfold forces'P. simpl. now firstorder.
simpl. rewrite andb_ref. unfold forces'P. simpl. unfold forces'P in IHG. split.
intros [A B] s [C|C]. rewrite <- C. rewrite <- forces_ref. assumption. now firstorder.
intros A. split. rewrite forces_ref. now firstorder.
now firstorder.
Qed.

Lemma monotone_forces (W : list assignment) (w w' : assignment) (s : form) :
In w' W -> w <= w' -> forces W w s -> forces W w' s.
Proof. rewrite inclb_ref. rewrite forces_ref. rewrite forces_ref. now apply monotone_forcesP. Qed.

Lemma soundnessK (W : list assignment) G s : nd G s ->
forall w, In w W -> forces' W w G -> forces W w s.
Proof. intros A w. rewrite forces'_ref. rewrite forces_ref. now apply soundnessKP. Qed.

(*** Example Applications ***)
Lemma unprovable_DN : ~nd nil (Imp (Not (Not x)) x).
Proof. intros D.
pose (W := [nil,[0]]).
assert (Wnil:In nil W). left. reflexivity.
assert (A:forces' W nil nil). simpl. tauto.
exact (soundnessK D Wnil A).
Qed.

Lemma unprovable_DN' : ~nd [Not (Not x)] x.
Proof. intros D. apply unprovable_DN. now apply ndII. Qed.

Definition indep s := ~nd nil s /\ ~nd nil (Not s).

Lemma unprovable_nDN : ~nd nil (Not (Imp (Not (Not x)) x)).
Proof. intros D.
pose (W := [@nil nat]).
assert (Wnil:In nil W). left. reflexivity.
assert (A:forces' W nil nil). simpl. tauto.
exact (soundnessK D Wnil A).
Qed.

Lemma indep_DN : indep (Imp (Not (Not x)) x).
Proof. split. apply unprovable_DN. apply unprovable_nDN. Qed.

(*** Exercise 11.11 ***)
Lemma unprovable_PWM : ~nd nil (Imp (Imp (Not x) y) (Imp (Imp (Not (Not x)) y) y)).


Lemma unprovable_nPWM : ~nd nil (Not (Imp (Imp (Not x) y) (Imp (Imp (Not (Not x)) y) y))).


Lemma indep_PWM : indep (Imp (Imp (Not x) y) (Imp (Imp (Not (Not x)) y) y)).