-- File: logic2

-- This file introduces more lemmas for predicate logic.
-- These lemmas are not included in the thesis, and are divided into three
-- groups.
-- 1) Introduction and elimination principles for ExP, ExQ, ExR, ExK
-- 2) Reflexivity, elimination, symmetry and transitivity for <=>, <==>, <===> 
-- 3) Miscellaneous

Path "../lol"
Load "logic"

--------------------------------------------------------------------
-- Introduction and elimination principles for ExP, ExQ, ExR, ExK --
--------------------------------------------------------------------

-- The next lemma is used by the ExistsI tactic.
Prove ExK_i : @X:*s.@P:*s->*p. P X -> (ExK) P
Use ExistsI ExK_i

-- The next lemma is used by the ExistsE tactic.
Prove ExK_e : @P:*s->*p.@R:*p. (ExK) P -> (@X:*s. P X -> R) -> R
Use ExistsE ExK_e

-- The next lemma is used by the ExistsI tactic.
Prove ExP_i : @X:*p.@P:*p->*p. P X -> (ExP) P
Use ExistsI ExP_i

-- The next lemma is used by the ExistsE tactic.
Prove ExP_e : @P:*p->*p.@R:*p. (ExP) P -> (@X:*p. P X -> R) -> R
Use ExistsE ExP_e

-- The next lemma is used by the ExistsI tactic.
Prove ExQ_i : @A:*s.@X:A->*p.@P:(A->*p)->*p. P X -> (ExQ) P
Use ExistsI ExQ_i

-- The next lemma is used by the ExistsE tactic.
Prove ExQ_e : @A:*s.@P:(A->*p)->*p.@R:*p. (ExQ) P -> (@X:A->*p. P X -> R) -> R
Use ExistsE ExQ_e


-- The next lemma is used by the ExistsI tactic.
Prove ExR_i : @A,B:*s.@X:A->B->*p.@P:(A->B->*p)->*p. P X -> (ExR) P
Use ExistsI ExR_i

-- The next lemma is used by the ExistsE tactic.
Prove ExR_e : @A,B:*s.@P:(A->B->*p)->*p.@R:*p. (ExR) P -> 
                      (@X:A->B->*p. P X -> R) -> R
Use ExistsE ExR_e


-------------------------------------------------------------------------------
-- Reflexivity, elimination, symmetry and transitivity for <=>, <==>, <===>  --
-------------------------------------------------------------------------------

Prove Bimpl_refl : @P:*p. P<=>P

Use Refl Bimpl_refl

Prove Bimpl_elim_r : @P,Q:*p.@R:*p->*p. P<=>Q -> R P -> R Q

Use Lewrite Bimpl_elim_r

Prove Bimpl_elim_l : @P,Q:*p.@R:*p->*p. P<=>Q -> R Q -> R P

Use Rewrite Bimpl_elim_l

Prove Bimpl_sym : @P,Q:*p. (P<=>Q) -> (Q<=>P)

Prove Bimpl_trans : @P,Q,R:*p. (P<=>Q) -> (Q<=>R) -> (P<=>R)

Prove BimplQ_refl : @A:*s.@P:A->*p. P<==>P

Use Refl BimplQ_refl

Prove BimplQ_elim_r : @A:*s. @P,Q:A->*p.@R:(A->*p)->*p. P<==>Q -> R P -> R Q

Use Lewrite BimplQ_elim_r

Prove BimplQ_elim_l : @A:*s. @P,Q:A->*p.@R:(A->*p)->*p. P<==>Q -> R Q -> R P

Use Rewrite BimplQ_elim_l

Prove BimplQ_sym : @A:*s. @P,Q:A->*p. (P<==>Q) -> (Q<==>P)

Prove BimplQ_trans : @A:*s.@P,Q,R:A->*p. (P<==>Q) -> (Q<==>R) -> (P<==>R)

Prove BimplR_refl : @A,B:*s.@P:A->B->*p. P<===>P

Use Refl BimplR_refl

Prove BimplR_elim_r : @A,B:*s. @P,Q:A->B->*p.@R:(A->B->*p)->*p. 
                      P<===>Q -> R P -> R Q

Use Lewrite BimplR_elim_r

Prove BimplR_elim_l : @A,B:*s. @P,Q:A->B->*p.@R:(A->B->*p)->*p. 
                      P<===>Q -> R Q -> R P

Use Rewrite BimplR_elim_l

Prove BimplR_sym : @A,B:*s. @P,Q:A->B->*p. (P<===>Q) -> (Q<===>P)

Prove BimplR_trans : @A,B:*s.@P,Q,R:A->B->*p. 
                     (P<===>Q) -> (Q<===>R) -> (P<===>R)


-------------------
-- Miscellaneous --
-------------------

Prove is_arrow_ : @A,B:*s.@f,g:A->B. f=g -> @x:A. f x = g x

Prove Or_assoc2 : @P,Q,R:*p. (P\/Q)\/R <=> P\/Q\/R