Require Import Relations. Class MModel := { Box : Type; rel : relation Box }. Notation "b1 'inside' b2" := (rel b2 b1) (at level 99). Definition MProp {M : MModel} := Box -> Prop. Definition apl {M : MModel} (p : MProp) (w : Box) := p w. Definition mnot {M : MModel} (p : MProp) := fun w => ~ (apl p w). Definition mand {M : MModel} (p q : MProp) := fun w => (apl p w) /\ (apl q w). Definition mor {M : MModel} (p q : MProp) := fun w => (apl p w) \/ (apl q w). Definition mimplies {M : MModel} (p q : MProp) := fun w => (apl p w) -> (apl q w). Definition mequiv {M : MModel} (p q : MProp) := fun w => (apl p w) <-> (apl q w). Definition box {M : MModel} (p : MProp) := fun w => forall w1, (rel w w1) -> (apl p w1). Definition dia {M : MModel} (p : MProp) := fun w => exists w1, (rel w w1) /\ (apl p w1). Definition MValid {M : MModel} (p : MProp) := forall w, apl p w. Notation "~ p" := (mnot p). Notation "p /\ q" := (mand p q). Notation "p \/ q" := (mor p q). Notation "p -> q" := (mimplies p q). Notation "p <-> q" := (mequiv p q). Notation "'[]' p" := (box p) (at level 50). Notation "'<>' p" := (dia p) (at level 50). Notation "p 'in' 'Box' w" := (apl p w) (at level 99). Ltac Box_Intro := match goal with | |- (apl (box ?p) ?w) => let w := fresh "b" in let R := fresh "B" in intro w at top; intro R at top | |- _ => fail 1 "Goal is not a []-formula." end. Ltac box_elim H w := match type of H with | (apl (box ?p) ?w') => let H1 := fresh "H" in cut (apl p w);[intros H1 | apply (H w); first [assumption | fail 2 "Nested box-condition cannot be varified" ] ] | _ => fail 1 "Formula is not a []-formula." end. Tactic Notation "Box_Elim" "in" hyp(H) "into" "Box" constr(b) := box_elim H b. Ltac dia_e H := match type of H with | (apl (dia ?p) ?w) => let w := fresh "b" in let R := fresh "B" in destruct H as [w [R H]]; move w at top; move R at top | _ => fail 1 "Formula is not a <>-formula." end. Tactic Notation "Diamond_Elim" "in" hyp(H) := dia_e H. Ltac dia_i w := match goal with | |- (apl (dia ?p) ?w') => exists w; split; [first [assumption | fail 2 "Nested box-condition cannot be varified" ] | idtac] | |- _ => fail 1 "Goal is not a <>-formula." end. Tactic Notation "Diamond_Intro" "into" "Box" constr(b) := dia_i b. Ltac start := match goal with [|- (MValid _)] => intro b end. Require Import Classical. Lemma MNNPP {M : MModel} (p : MProp) : MValid (~~p -> p). Proof. start. do 2 red; intros. apply NNPP in H. assumption. Qed. Ltac PBC := let H := fresh "H" in apply MNNPP; intro H. Ltac Iff_Intro := red; match goal with | |- mequiv ?P ?Q ?b => split; [ replace (forall _:(apl P b), (apl Q b)) with (apl (mimplies P Q) b) by trivial | replace (forall _:(apl Q b), (apl P b)) with (apl (mimplies Q P) b) by trivial] | |- _ => fail 1 "Goal not an Iff-formula" end.