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

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

Section OR_AND_Exist.

Require Export minimal.

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

(* a notation for Forall *)

Notation "\-/ p" := (Forall ? p) (at level 6, right associativity).

(* A few abbreviations *)


(* AND noted & *)
Definition AND := [p,q:proposition] 
    \-/[r:proposition] (p => q => r) => r.
(* status *)   Infix 4 "&" AND.

(* OR noted V *)
Definition OR := [p,q:proposition] 
    \-/[r:proposition] (p => r) => (q => r) => r.
(* status *)   Infix 4 "V" OR.

Definition Exist := [A:Set][P: A ->proposition] 
    \-/[p:proposition] (\-/[a:A]((P a) => p)) => p.


(* -------------------- Two handy lemmas -------------------- *)

Lemma rule_Forall2: (A: Set)(P:A -> proposition)(q:proposition) 
        |- (\-/[x:A](q => (P x))) -> |- q => \-/P.
Intros. 
Apply MP with (Forall A [x:A](q => (P x))).
Apply Forall2. 
Trivial.
Qed.

Lemma Forall_P_then_Q:  (A: Set)(P,Q:A -> proposition)(a:A) 
    |- (P a) => (\-/[b:A]((P b) => (Q b))) => (Q a).
Proof.
Intros. 
Apply rule_C.
Apply Forall1 with P:=[a:A](P a) => (Q a).
Qed.

(* ==================== Proof of the basic properties of OR ==================== *)

Lemma OR0: (p,q,r:proposition) |- (p => r) => (q => r) => (p V q) => r.
Proof.
Intros. 
Apply rule_C2.
Unfold OR.
Apply Forall_P_then_Q with P:=[r:proposition]p => r Q:=[r:proposition](q => r) => r.
Qed.

Lemma OR1: (p,q:proposition) |- p => (p V q).
Proof.
Intros. 
Unfold OR.
Apply MP with \-/[r:proposition] (p => (p => r) => (q => r) => r).
Apply  Forall2 with P:=[r:proposition](p => r) => (q => r) => r.
Apply ForallRule. Intros. 
Apply rule_C.
Apply MP with x => (q => x) => x.
Apply B.
Apply Hilbert_K.
Qed.

Lemma OR2: (p,q:proposition) |- q => (p V q).
Proof.
Intros. 
Unfold OR.
Apply MP with \-/[r:proposition] (q => (p => r) => (q => r) => r).
Apply Forall2 with P:=[r:proposition](p => r) => (q => r) => r.
Apply ForallRule. Intros.
Apply rule_Drop.
Apply rule_C. 
Apply I.
Qed.

(* ==================== Proof of the basic properties of AND ==================== *)

Lemma  AND0: (p,q:proposition) |- p => q => (p & q).
Proof.
Intros.
Unfold AND.
Apply Cut_rule with \-/[r:proposition] (q => (p => q => r) => r).
Apply MP with \-/[r:proposition] (p => q => (p => q => r) => r).
Apply Forall2 with P:=[r:proposition] (q => (p => q => r) => r).
Apply ForallRule. Intros.
Apply rule_C2. Apply rule_C.
Apply I.
Apply Forall2 with P:=[r:proposition] ((p => q => r) => r).
Qed.

Lemma AND1: (p,q:proposition) |- (p & q) => p.
Proof.
Intros. 
Unfold AND.
Apply Cut_rule with (p => q => p) => p.
Apply Forall1 with a:=p P:=[r:proposition](p => q => r) => r.
Apply MP with p => q => p.
Apply CI.
Apply Hilbert_K.
Qed.

Lemma AND2: (p,q:proposition) |- (p & q) => q.
Proof.
Intros. 
Unfold AND.
Apply Cut_rule with (p => q => q) => q.
Apply Forall1 with P:=[r:proposition](p => q => r) => r.
Apply MP with p => q => q.
Apply CI.
Apply KI.
Qed.

(* ==================== Proof of the basic properties for Exist ==================== *)

Lemma Exist1: (A: Set)(P:A -> proposition)(a:A) |- (P a) => (Exist A P).
Proof.
Intros. 
Unfold Exist.
Apply rule_Forall2 with P:=[p:proposition](\-/[a0:A](P a0) => p) => p.
Apply ForallRule. Intro q. 
Apply Forall_P_then_Q with Q:=[a:A]q.
Qed.

Lemma Exist2: (A: Set)(P:A -> proposition)(q:proposition) 
        |- (\-/[x:A]((P x) => q)) => (Exist A P) => q.
Proof.
Intros. 
Unfold Exist.
Apply Forall_P_then_Q 
    with P:=[p:proposition]\-/[a:A]((P a) => p) Q:=[p:proposition]p.
Qed.

End OR_AND_Exist.