(* Quiz 5                      *)
(* Name:                       *)
(* Matric number:              *)

(* The following lines are similar to "#include" in C; just keep them here *)
Require Import Classical.
Axiom dep_extensionality:
 forall (A: Type) (B: A -> Type) (f g : forall x: A, B x),  (forall x, f x = g x) -> f = g.
Implicit Arguments dep_extensionality.
Lemma extensionality:
 forall (A B: Type) (f g : A -> B),  (forall x, f x = g x) -> f = g.
Proof. intros; apply dep_extensionality; auto. Qed.
Implicit Arguments extensionality.
Tactic Notation "extensionality" := 
  (match goal with | |- ?f = ?g => apply (extensionality f g); intro end).
Tactic Notation "extensionality" ident(x) := 
  (match goal with | |- ?f = ?g => apply (extensionality f g); intro x end).
Require Import Omega.
Axiom prop_ext: ClassicalFacts.prop_extensionality.
Implicit Arguments prop_ext.
Tactic Notation "spec" hyp(H) :=
  match type of H with ?a -> _ => 
    let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end.
Tactic Notation "spec" hyp(H) constr(a) :=
  (generalize (H a); clear H; intro H). 
Tactic Notation "spec" hyp(H) constr(a) constr(b) :=
  (generalize (H a b); clear H; intro H).
 Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) :=
  (generalize (H a b c); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
  (generalize (H a b c d); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) :=
  (generalize (H a b c d e); clear H; intro H).
Tactic Notation "LEM" constr(phi) :=
  (destruct (classic (phi))).
(* end #include section *)

Parameter world : Type.

Parameter R : world -> world -> Prop.

Definition Proposition : Type := world -> Prop.

Definition holds_in (w : world)  (phi : Proposition) : Prop :=
  phi w.

Notation "w ||- phi" := (holds_in w phi) (at level 30).

Definition Top : Proposition :=
  fun w => True.

Definition Bot : Proposition :=
  fun w => False.

Definition Neg (phi : Proposition) : Proposition :=
  fun w => ~ (w ||- phi).
Notation "! phi" := (Neg phi) (at level 16).

Definition And (phi psi : Proposition) : Proposition :=
  fun w => (w ||- phi) /\ (w ||- psi).
Notation "phi && psi" := (And phi psi).

Definition Or (phi psi : Proposition) : Proposition :=
  fun w => (w ||- phi) \/ (w ||- psi).
Notation "phi || psi" := (Or phi psi).

Definition Impl (phi psi : Proposition) : Proposition :=
  fun w => (w ||- phi) -> (w ||- psi).
Notation "phi --> psi" := (Impl phi psi) (at level 20, right associativity).

Definition Box (phi : Proposition) : Proposition :=
  fun w => forall w', R w w' -> (w' ||- phi).

Notation "[] phi" := (Box phi) (at level 15).

Definition Diamond (phi : Proposition) : Proposition :=
  fun w => exists w', R w w' /\ (w' ||- phi).

Notation "<> phi" := (Diamond phi) (at level 15).



Definition valid (phi: Proposition) : Prop :=
  forall w, w ||- phi.
Notation "|= phi" := (valid phi) (at level 30).



Section Example.

Parameter p : Proposition.

Parameter x1 x2 x3: world.

Hypothesis Kripke_example: 
     R x2 x2 /\ R x2 x1 /\ 
     R x2 x3 /\ R x3 x2 /\ R x3 x1 /\ 
     (x1 ||- p) /\  
     (x2 ||- ! p)   /\
     (x3 ||- p).
        

Lemma QuizProblem1: x2 ||- <> <> p.
Proof.
admit.
Qed.

Lemma QuizProblem2: ~ |= p --> [] [] p.
Proof.
admit.
Qed.

End Example.

(* You don't need to know the inner details of how this works. *)
Lemma EQ_Proposition : forall P Q,
(forall w, w ||- P <-> w ||- Q) -> P = Q.
Proof.
  intros.
  unfold Proposition.
  apply extensionality.
  intro.
  apply prop_ext.
  spec H x.
  tauto.
Qed.
Tactic Notation "EQ_Proposition" :=
  (intros; apply EQ_Proposition; intro w).

(* A synthetic definition: we can define new Propositions using the old ones, like this. *)
Definition Dbl_Impl (phi psi : Proposition) : Proposition :=
  (phi --> psi) && (psi --> phi).
Notation "phi <--> psi" := (Dbl_Impl phi psi) (at level 20).

(* Let's use the new EQ_Proposition tactic to show that this is equal to the definition 
    where we write everything out.  You do need to make sure you understand
    how to use the new tactic.  *)

Lemma DblImplExample : forall phi psi, 
  (phi <--> psi)   =   (fun w => (w ||- phi) <-> (w ||- psi)).
Proof.
intros.
EQ_Proposition.  
(* The first real step to prove an equality of Propositions 
   is the EQ_Proposition tactic. *)
tauto.
Qed.

(* Let's lift LEM to the modal logic; note that we do LEM relative to each world. *)
Lemma modal_LEM : forall phi,
  |= (phi || ! phi).
Proof.
  intros.
  intro.
  LEM (w ||- phi).
  left.
  trivial.
  right.
  trivial.
Qed.

(* For convienence I define this tactic to help. *)
Tactic Notation "ML_LEM" constr(w) constr(phi) :=
  (destruct (modal_LEM (phi) (w))).

(* Double negation -- and a demo of how to use the new tactic. *)
Lemma modal_NNPP: forall phi,
  phi = ! (! phi).
Proof.
  EQ_Proposition.
  ML_LEM w phi.
  split; auto.
  repeat intro.
  contradiction H1.
  split; intro.
  contradiction H.
  contradiction H0.
Qed.

Lemma K : forall phi psi,
  |= ([] (phi --> psi)) --> [] phi --> [] psi.
Proof.
  intros.
  do 5 intro.
  spec H w' H1.
  apply H.
  apply H0.
  trivial.
Qed.

Lemma QuizProblem3:
forall phi psi,
|= <>(phi && psi) --> (<> phi && <> psi).
Proof.
admit.
Qed.


(* Correspondence *)

Lemma QuizProblem4:
(forall w1 w2, R w1 w2 -> w1 = w2)
->
(forall phi, |= <> phi --> phi).

Proof.
admit.
Qed.