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

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


Require Export propositional.

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

Notation "|- p" := (theorem p) (at level 7).
Infix RIGHTA 5 "=>" Imp.
Infix 4 "&" AND.
Notation "\-/ p" := (Forall ? p) (at level 5, right associativity).

(* =====================  Forall Lemmas ======================= *)

(* (\-/x,y) Q(x,y) => Q(a,b)  *)

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

(* (\-/x(\-/y Q(x,y))) => (\-/y(\-/x Q(x,y))) *)

Lemma ForallForall: (A: Set) (Q:A->A->proposition)
    |- (\-/[x:A](\-/(Q x))) => (\-/[y:A](\-/[x:A] (Q x y))).
Proof.
Intros.
Apply MP 
with (\-/[y:A] ((\-/[x:A](\-/(Q x))) => ([y:A](\-/[x:A] (Q x y)) y))).
Apply Forall2 with q:= (\-/[x:A](\-/(Q x))) P:=[y:A](\-/[x:A](Q x y)).
Apply ForallRule.  Intro.
Apply MP with \-/[x1:A]((\-/[x0:A] (\-/(Q x0))) => (Q x1 x)).
Apply Forall2 with q:=(\-/[x0:A](\-/(Q x0))) P:= [x0:A](Q x0 x).
Apply ForallRule. Intro.
Apply Forallx_Forally.
Qed.

(* Q(a,b)  =>  (Exist x,y) Q(x,y) *)

Lemma Existy_Existx: (A: Set) (Q:A->A->proposition)(a,b:A) 
    |- (Q a b) => (Exist A [y1:A](Exist A [x1:A](Q x1 y1))).
Proof.
Intros. Apply Cut_rule with (Exist A [x1:A](Q x1 b)). Apply Exist1 with P:=[x1:A](Q x1 b).
Apply Exist1 with P:=[y1:A](Exist A [x1:A](Q x1 y1)) a:=b.
Qed.

(* (Exist x (Exist y Q(x,y))) => (Exist y (Exist x Q(x,y))) *)

Lemma ExistExist: (A: Set) (Q:A->A->proposition)
    |- (Exist A  [x:A](Exist A  (Q x))) => (Exist A  [y:A](Exist A  [x:A] (Q x y))).
Proof.
Intros. Apply MP with (\-/[x:A] (Exist A  (Q x)) => (Exist A  [y:A](Exist A  [x:A](Q x y)))).
Apply Exist2 with P:=[x:A](Exist A  (Q x)) q:=(Exist A  [y:A](Exist A  [x:A](Q x y))).
Apply ForallRule. Intro.
Apply MP with \-/[y0:A]  (Q x y0) => (Exist A  [y:A](Exist A  [x0:A](Q x0 y))).
Apply Exist2 with P:=(Q x) q:=(Exist A  [y:A](Exist A  [x0:A](Q x0 y))).
Apply ForallRule. Intro. Apply Existy_Existx.
Qed.

(* (Exist x (\-/y Q(x,y))) => (\-/y (Exist x Q(x,y))) *)

Lemma ExistForall: (A: Set) (Q:A->A->proposition)
    |- (Exist A  [x:A](\-/(Q x))) => (\-/[y:A](Exist A  [x:A] (Q x y))).
Proof.
Intros. Apply MP with \-/[x:A](\-/(Q x)) => (\-/[y:A](Exist A  [x:A](Q x y))).
Apply Exist2 with P:=[x:A](\-/(Q x)) q:=(\-/[y:A](Exist A  [x:A](Q x y))).
Apply ForallRule. Intro a. Apply MP with \-/[y:A](\-/(Q a)) => (Exist A  [x:A](Q x y)).
Apply Forall2 with q:= (\-/(Q a)) P:=[y:A](Exist A  [x:A](Q x y)).
Apply ForallRule. Intro b. Apply Cut_rule with (Q a b). Apply Forall1. 
Apply Exist1 with P:=[x:A](Q x b). 
Qed.


End Predicates_logic.