(* Time-stamp: <modified on 28 Apr 2004 at 17:33 by Pierre Lescanne> *)

(****************************************************************************)
(*                              classic.v                                   *)
(*                                                                          *)
(*                             Pierre Lescanne                              *)
(*                                                                          *)
(*		       LIP (ENS-Lyon, CNRS, INRIA)                          *)
(*                                                                          *)
(*                                                                          *)
(* Developed in V7.4   January 2001   ---   March 2004                      *)
(****************************************************************************)
Section Classic.

Require axioms.
Require minimal.
Require or_and_exist.
Require propositional. 
Require false.

(* ======== Syntax ======== *)

Notation "|- p" := (theorem p) (at level 7).
Infix RIGHTA 5 "=>" Imp.
Infix 4 "&" AND.
Infix 4 "V" OR.
Infix RIGHTA 4 "|" Xor.
Notation "¬ p" := (Not p) (at level 3).


Axiom Classic_NotNot: (p:proposition) |- (¬¬p) => p.

Lemma Class_OR_Not: (p,q:proposition) |- ¬(p & q) => ¬p V ¬q.
Proof.
Intros.
Apply Cut_rule with ¬¬(¬p V ¬q).
Apply rule_Contrapos1.
Apply Cut_rule with (¬¬p) & (¬¬q). Apply AND_Not.
Apply rule_glueAND; Apply Classic_NotNot.
Apply Classic_NotNot.
Qed.

Lemma rule_Class_OR_Not: (p,q:proposition) |- ¬(p & q) -> |- (¬p) V (¬q).
Proof.
Intros.
Apply MP with ¬(p & q).
Apply Class_OR_Not.
Assumption.
Qed.

Lemma not_p_then_q: (p,q:proposition) |- (¬p => q) => ¬q => p.
Proof.
Intros. 
Apply Cut_rule with (¬q) => ¬¬p.
Apply Contraposition.
Apply MP with (¬¬p) => p.
Apply B.
Apply Classic_NotNot.
Qed.

Lemma r_not_p_then_q: (p,q,r:proposition) 
    |- r & (¬p) => q -> |- r & ¬q => p.
Proof.
Intros.
Apply rule_Imp_AND. 
Apply Cut_rule with ¬p => q.
Apply rule_rev_AND_Imp.
Assumption.
Apply not_p_then_q.
Qed.

Lemma Class_OR: (p,q:proposition) |- ¬((¬p) & (¬q)) => p V q.
Proof.
Intros. Apply Cut_rule with  (¬¬p) V (¬¬q).
Apply Class_OR_Not.
Apply rule_glueOR;Apply Classic_NotNot.
Qed.

Lemma rule_Class_OR: (p,q:proposition) |- ¬((¬p) & (¬q)) -> |- p V q.
Proof.
Intros. Apply MP with ¬((¬p) & (¬q)).
Apply Class_OR.
Assumption.
Qed.

Lemma Excluded_middle: (p:proposition) |- p V ¬p.
Proof.
Intros. 
Apply rule_Class_OR. Apply MP with ¬FALSE.
Apply rule_Contrapos1.
Apply rule_Imp_AND.
Apply rule_C.
Apply rule_rev_AND_Imp.
Apply Not_p_AND_p.
Unfold Not. Apply I.
Qed.

Lemma Class_OR_with_disjunction: (p,q :proposition) |- p V q => (p & ¬q) V q.
Proof.
Intros. 
Apply Cut_rule with (p V q) & (¬q V q).
Apply rule_AND_Imp.
Apply I.
Apply Cut_rule with TRUE.
Apply Everything_Imp_True.
Apply Cut_rule with ¬(q & ¬q).
Apply Cut_rule with ¬FALSE. Unfold Not. Apply KI.
Apply rule_Contrapos1. Unfold Not.
Apply rule_Imp_AND. Apply CI.
Apply Cut_rule with ¬((¬¬q) & ¬q).
Apply rule_Contrapos1.
Apply rule_AND_right_regular.
Apply Classic_NotNot.
Apply Class_OR.
Apply undist_OR2.
Qed.


(* About Xor *)

Lemma Xor_Imp2: (p,q:proposition) |- (p | q) => p => ¬q.
Proof.
Intros. Unfold Xor.
Apply rule_Imp_AND.
Apply rule_C.
Apply Cut_rule with ¬p V ¬q.
Apply Class_OR_Not.
Apply rule_OR0.
Apply rule_C.
Apply rule_OR0.
Apply Cut_rule2 with FALSE.
Apply False_Imp_everything.
Unfold Not. Apply CI.
Apply rule_C. Apply rule_Drop.
Apply Cut_rule2 with FALSE.
Apply False_Imp_everything.
Unfold Not. Apply I.
Apply rule_Drop. Apply rule_Drop.
Apply I.
Qed.

End Classic.