(* 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.