(*** Introduction to Computational Logic, Coq part of Assignment 9 ***)
(***
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.
Require Import Bool List.

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.

(** ND System *)
Definition context := list form.

Inductive nd : context -> 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 ndK G s t :
nd G (FK s t).

Proof. apply ndII, ndII, ndW, ndA. Qed.

Lemma ndS G s t u :
nd G (FS s t u).

Proof. apply ndII, ndII, ndII.
apply ndIE with (s:=t). apply ndIE with (s:=s).
now apply ndW, ndW, ndA. now apply ndA.
apply ndIE with (s:=s). now apply ndW, ndA. apply ndA. Qed.

Lemma ndE' G s :
nd G (FE s).

Proof. apply ndII, ndE, ndA. Qed.

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).

Lemma ndMem G s :
mem s G -> nd G s.

Proof. intros A ; induction A. apply ndA. apply ndW, IHA. Qed.

(*** Exercise 9.1 ***)
Goal forall s t, 

Lemma ndApply G s t :

Goal forall G s t,

Goal forall G s t,


(** Hilbert System *)

Inductive hil (G : context) : form -> Prop :=
| hilA s :
  mem s G -> hil G s
| hilK s t :
  hil G (FK s t)
| hilS s t u :
  hil G (FS s t u)
| hilE s :
  hil G (FE s)
| hilMP s t :
  hil G (Imp s t) -> hil G s -> hil G t.

Lemma agree_nd G s :
hil G s -> nd G s.

Proof. intros A. induction A.
(* hilA *) apply ndMem ; assumption.
(* hilK *) now apply ndK.
(* hilS *) now apply ndS.
(* hilDN *) now apply ndE'.
(* hilMP *) apply ndIE with (s:=s) ; assumption. Qed.

Lemma hilW G s t :
hil G s -> hil (t::G) s.

Proof. intros A ; induction A.
now apply hilA, memT, H.
now apply hilK.
now apply hilS.
now apply hilE.
exact (hilMP IHA1 IHA2). Qed.

(*** Exercise 9.2 ***)
Lemma hilAK G s t :

Lemma hilAS G s t u :

Lemma hilI G s :

Lemma ded s G t :


Lemma agree_hil G s :
nd G s -> hil G s.

Proof. intros A ; induction A.
(* ndA *) now apply hilA, memH.
(* ndW *) apply hilW ; assumption.
(* ndII *) exact (ded IHA). 
(* ndIE *) exact (hilMP IHA1 IHA2).
(* ndE *)  exact (hilMP (hilE G s) IHA). Qed.

(** Admissible Rules **)
(** General Weakening **)
Lemma hilGW G G' s : (forall u, mem u G -> mem u G') -> hil G s -> hil G' s.
Proof. intros A B. induction B.
apply hilA. now apply A.
now apply hilK.
now apply hilS.
now apply hilE.
now apply hilMP with (s := s).
Qed.

Lemma ndGW G G' s : (forall u, mem u G -> mem u G') -> nd G s -> nd G' s.
Proof. intros A B. apply agree_nd.
 apply hilGW with (G := G). assumption.
 now apply agree_hil. Qed.

Lemma ndW2 G s t u :
nd (t :: G) u -> nd (t :: s :: G) u.
Proof. apply ndGW. intros v A. inversion A. now apply memH.
now apply memT, memT. Qed.

(*** Apply and Refutation Cases ***)
Lemma ndAp G s t : mem (Imp s t) G -> nd G s -> nd G t.
Proof. intros A B. apply ndIE with (s := s). apply ndMem; assumption. assumption. Qed.

Lemma ndN G s :
nd G s -> nd (Not s::G) Fal.
Proof. intros A. apply ndAp with (s := s). now apply memH. now apply ndW. Qed.

Lemma ndRC G s :
nd (s :: G) Fal -> nd (Not s :: G) Fal -> nd G Fal.
Proof. intros A B. apply ndIE with (s := Not s); now apply ndII. Qed.

(** Classical ND *)
Inductive ndc : context -> form -> Prop :=
| ndcA G s :
  ndc (s::G) s
| ndcW G s t :
  ndc G s -> ndc (t::G) s
| ndcII G s t :
  ndc (s::G) t -> ndc G (Imp s t)
| ndcIE G s t :
  ndc G (Imp s t) -> ndc G s -> ndc G t
| ndcC G s :
  ndc (Not s::G) Fal -> ndc G s.

(*** Exercise 9.3 ***)
Lemma nd_ndc G s : 


(*** Exercise 9.4 ***)
Goal forall G s, 


(** Classical Hilbert *)

Inductive hilc (G : context) : form -> Prop :=
| hilcA s :
  mem s G -> hilc G s
| hilcK s t :
  hilc G (FK s t)
| hilcS s t u :
  hilc G (FS s t u)
| hilcDN s :
  hilc G (FDN s)
| hilcMP s t :
  hilc G (Imp s t) -> hilc G s -> hilc G t.

(** Exercise 9.5: A Proof of Glivenko *)
Lemma ndDN' G s :
nd G s -> nd G (Not (Not s)).

Lemma ndDNDN G s :
nd G (Not (Not (FDN s))).

Lemma ndDNMP G s t :
nd G (Not (Not (Imp s t))) -> nd G (Not (Not s)) -> nd G (Not (Not t)).

Lemma Glivenko G s :
hilc G s -> nd G (Not (Not s)).


(*** Exercise 9.6: Agreement of hilc and ndc ***)
Lemma ndcMem G s :
mem s G -> ndc G s.

Lemma agree_ndc G s :
hilc G s -> ndc G s.

Lemma hilcW G s t :
hilc G s -> hilc (t :: G) s.

Lemma hilcAK G s t :
hilc G s -> hilc G (Imp t s).

Lemma hilcAS G s t u :
hilc G (Imp s (Imp t u)) -> hilc G (Imp s t) -> hilc G (Imp s u).

Lemma hilcI G s :
hilc G (Imp s s).

Lemma dedc s G t :
hilc (s :: G) t -> hilc G (Imp s t).

Lemma agree_hilc G s :
ndc G s -> hilc G s.


(*** Exercise 9.7: hil_hilc using agree_hilc **)
Lemma hil_hilc G s : hil G s -> hilc G s.