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

Require Export or_and_exist.

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

Notation "|- p" := (theorem p) (at level 7).
Infix RIGHTA 5 "=>" Imp.
Infix 4 "&" AND.

Definition FALSE :=(Forall proposition [p:proposition] p).
Definition TRUE:=(Exist proposition [p:proposition] p).
Definition Not:=[p:proposition] (p => FALSE).

Notation "¬ p" := (Not p) (at level 3).

(* ==================== False Lemmas ======================= *)


Definition FF:=(p:proposition) |- p.
Definition NOT:=[P:Prop](P -> FF).

Lemma False_Imp_everything: (p:proposition) |-  FALSE => p.
Proof.
Intros. Unfold  FALSE. Apply Forall1 with P:=[p:proposition]p.
Qed.

Lemma Everything_Imp_True: (p:proposition) |- p => TRUE.
Proof.
Intros. Unfold TRUE. Apply Exist1 with P:=[p:proposition]p.
Qed.

Lemma NOTFalse: (NOT |- FALSE).
Proof.
Unfold FALSE NOT. Unfold FF. Intros. Apply MP with  FALSE. Apply  False_Imp_everything. Assumption.
Qed.

Lemma FalseFF: (|-  FALSE) -> FF.
Proof.
Unfold FF  FALSE.
Intros.
Apply MP with (Forall proposition [p:proposition]p).
Apply Forall1 with P:=[p:proposition]p.
Assumption.
Qed.

Lemma FFFalse: FF -> |-  FALSE.
Proof.
Unfold FF  FALSE.
Intros.
Apply ForallRule with P:=[p:proposition]p. 
Assumption.
Qed.


Lemma NOTNot: (p:proposition) (|- ¬p) -> (NOT |- p).
Unfold NOT.
Intros. 
Apply FalseFF.
Apply MP with p; Assumption.
Qed.

Lemma theorem_True: |- TRUE.
Proof.
Unfold TRUE. Apply MP with TRUE => TRUE.
Apply Exist1 with P := [p:proposition]p. Apply I.
Qed.

Lemma NotNot: (p:proposition) |- p => ¬¬p.
Proof.
Intros. Unfold Not. Apply rule_C. Apply I.
Qed.

Lemma Contraposition: (p,q:proposition) 
    |- (p => q) => (¬q) => ¬p.
Proof.
Intros.
Unfold Not.
Apply CB. 
Qed.

Lemma rule_Contrapos1: (p,q:proposition)
    |- p => q -> |- ¬q => ¬p.
Proof.
Intros. 
Apply MP with p=>q. Apply Contraposition. Assumption.
Qed.

Lemma rule_Contrapos2: (p,q:proposition)
    |- p => q -> |- ¬q -> |- ¬p.
Proof.
Intros.
Apply MP with (Not q).
Apply MP with p => q.
Apply Contraposition.
Trivial.
Trivial.
Qed.

End False_logic.