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

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

Require Export axioms.

Notation "|- p" := (theorem p) (at level 6).
Infix RIGHTA 5 "=>" Imp.

(* ==================== Implicative Lemmas ======================= *)

Lemma I: (p:proposition) |- p => p.
Proof.
Intros. 
Apply MP with p => p => p. 
Apply MP with p => (p => p) => p.
Apply Hilbert_S. Apply Hilbert_K. Apply Hilbert_K.
Qed.

Lemma KI:  (p,q:proposition) |- q => p => p.                    
Proof.
Intros.
Apply MP with p => p .
Apply Hilbert_K.
Apply I.
Qed.

Lemma KS: (p,q,r,t:proposition) 
    |- t => (p => q => r) => (p => q) => p => r.
Proof.
Intros. 
Apply MP with (p => q => r) => (p => q) => p => r.
Apply Hilbert_K. 
Apply Hilbert_S.
Qed.

Lemma SKS: (p,q,r,t:proposition) 
 |- (t => p => q => r) => (t => (p => q) => p => r).
Proof.
Intros. 
Apply MP with t => (p => q => r) => (p => q) => p => r.
Apply Hilbert_S.
Apply KS.
Qed.

Lemma B: (p,q,r:proposition) |- (p => q) => (r => p) => r => q.
Proof.
Intros.
Apply MP with p:=(p => q) => r => p => q.
Apply SKS.
Apply Hilbert_K. 
Qed.

(* p => q , q => r |- p => r *)

Lemma Cut_rule: (p,q,r:proposition) 
    |- p => q -> |- q => r -> |- p => r.
Proof.
Intros.
Apply MP with p => q.
Apply MP with q => r.
Apply B.
Trivial.
Trivial.
Qed.

Lemma BB: (p,q,r,t:proposition) 
	 |- (p => q => r) => p => (t => q) => t => r.
Proof.
Intros.
Apply MP with (q => r) => (t => q) => t => r.
Apply B.
Apply B.
Qed.

Lemma BBS: (p,q,r,s:proposition) 
	|- (p => q => r) => (s => p => q) => s => p => r.
Proof.
Intros.
Apply MP with (p => q => r) => (p => q) => (p => r).
Apply BB.
Apply Hilbert_S.
Qed.

Lemma SBBS: (p,q,r,t:proposition) 
 |- ((p => q => r) => t => p => q) => (p => q => r) => t => p => r.
Proof.
Intros.
Apply MP with (p => q => r) => (t => p => q) => (t => p => r).
Apply Hilbert_S.
Apply BBS.
Qed.

Lemma KK: (p,q,r:proposition) |- (p => (q => (r => q))).
Proof.
Intros.
Apply MP with (q => (r => q)).
Apply Hilbert_K.   
Apply Hilbert_K.   
Qed.

Lemma Hilbert_C: (p,q,r:proposition) |- (p => q => r) => q => p => r.
Proof.
Intros.
Apply MP with (p => q => r) => (q => p => q).
Apply SBBS.
Apply KK.
Qed.

(* p => q => r |- q => p => r *)

Lemma rule_C: (p,q,r:proposition) 
    |- (p => q => r) -> |- q => p => r. 
Proof.
Intros .
Apply MP with (p => q => r).
Apply Hilbert_C.
Apply H.
Qed.

Lemma CI: (p,q: proposition) |- (p => (p => q) => q).
Proof.
Intros.
Apply MP with  (p => q) => p => q.
Apply Hilbert_C.
Apply I.
Qed.

Lemma C2: (p,q,r,s:proposition) |- (p => q => r => s) => p => r => q => s.
Proof.
Intros.
Apply MP with (q => r => s) => r => q => s.
Apply B.
Apply Hilbert_C.
Qed.

Lemma rule_C2: (p,q,r,s:proposition) |- p => q => r => s -> |- p => r => q => s.
Proof.
Intros.
Apply MP with p => q => r => s.
Apply C2.
Trivial.
Qed.

Lemma Cut_rule2: (p,q,r,s:proposition) 
    |- p => q ->  |- s => r => p -> |- s => r => q.
Proof.
Intros. 
Apply Cut_rule with r => p.
Apply H0. 
Apply MP with p => q. Apply B. Apply H.
Qed.

Lemma CB: (p,q,r:proposition) |- (r => p) => (p => q) => r => q.
Proof.
Intros.
Apply MP with (p => q) => (r => p) => r => q.
Apply Hilbert_C.
Apply B.
Qed.

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

Lemma Drop_2nd_hyp: (p,q,r:proposition) |- (p => q) => p => r => q.
Proof.
Intros. Apply Cut_rule with r => p => q. Apply Hilbert_K. Apply Hilbert_C.
Qed.

Lemma rule_Drop: (p,q,r:proposition) |- p => q -> |- p => r => q.
Proof.
Intros. Apply MP with p => q. Apply Drop_2nd_hyp. Assumption.
Qed.

Lemma Cut2 : (p1,p2,q,r:proposition) 
 |- (p1 => p2 => q)  => (q => r) => p1 => p2 => r.
Proof.
Intros.
Apply MP with (q => r) => (p1 => p2 => q) => (p1 => p2 => r).
Apply Hilbert_C.
Apply Cut_rule with (p2 => q) => p2 => r.
Apply B.
Apply B.
Qed.

Lemma CSI: (p,q:proposition) |- (p => p => q) => p => q.
Proof.
Intros.
Apply MP with p => p.
Apply MP with (p => p => q) => (p => p) => p => q.
Apply Hilbert_C.
Apply Hilbert_S.
Apply I.
Qed.

(* p => p => q |- p => q *)

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


End  Minimal_logic.