-- File: logic

-- This file introduces predicate logic.
-- It consists of two parts.
-- 1. Axioms, corresponding to Section 4.5
-- 2. Library, corresponding to Section 4.6

Load "lambdaL"

-----------------------
-----------------------
--                   --
--  1.  A X I O M S  --
--                   --
-----------------------
-----------------------

Def False := @P:*p.P
                                   
Def True := @P:*p.P->P

Def Not := \P:*p. P->False
      
Def (/\) := \P,Q:*p. (@R:*p. (P->Q->R)->R)
InfixR 3 (/\)
-- Name in lemmas: And

Def (\/) := \P,Q:*p. (@R:*p.(P->R)->(Q->R)->R)
InfixR 2 (\/)
-- Name in lemmas: Or

-- Existential quantification over a datatype
Def Ex := \A:*s.\P:A->*p.@Q:*p. (@x:A.P x->Q) -> Q
Implicit 1 Ex
Binder Ex

-- We define existential quantifications over propkinds for three categories
-- of propkinds, viz. over propkinds of the form
--    *p       (exis. quant. over propositions, denoted by ExP), 
--    A->*p    (exis. quant. over predicates, denoted by ExQ,
--              which is polymorphic in A:*s), and
--    A->B->*p (exis. quant. over relations, denoted by ExR, 
--              which is polymorphic in A,B:*s)
-- (See Remark 4.5.2 on page 88)

-- existential quantification over propositions
Def ExP := \P:*p->*p. @Q:*p. (@X:*p. P X -> Q) -> Q
Binder ExP

-- existential quantification over predicates
Def ExQ := \A:*s.\P:(A->*p)->*p. @Q:*p. (@X:(A->*p). P X -> Q) -> Q
Implicit 1 ExQ
Binder ExQ

-- existential quantification over relations
Def ExR := \A,B:*s.\P:(A->B->*p)->*p. @Q:*p. (@X:A->B->*p. P X -> Q) -> Q
Implicit 2 ExR
Binder ExR

-- existential quantification over kind *s
Def ExK := \P:*s->*p. @Q:*p. (@X:*s. P X -> Q) -> Q
Binder ExK

-- Leibniz' equality
Def (=) := \A:*s.\x,y:A. @P:A->*p. P x -> P y
Infix 4 (=)
Implicit 1 (=)
-- prefix name: is

Var classic : @P:*p. Not (Not P) -> P

-- the axiom of extensionality for ordinary functions
Var is_arrow :  @A,B:*s.@f,g:A->B. (@x:A. f x = g x) -> f = g

-- the axiom of extensionality for polymorphic functions
-- We introduce this axiom only for kind *s.
-- (See Remark 4.5.2 on page 88.)
Var is_pi1 : @A:*s->*s. @f,g:(@X:*s. A X). (@X:*s. f X = g X) -> f = g

-- We define Leibniz' equality for prop-constructors for three categories
-- of propkinds, viz. over propkinds of the form
--    *p       (equality of propositions, denoted by <=>),
--    A->*p    (equality of predicates, denoted by <==>,
--              which is polymorphic in A:*s), and
--    A->B->*p (equality of relations, denoted by <===>, 
--              which is polymorphic in A,B:*s).
-- (See Remark 4.5.2 on page 88.)

Def (<=>) := \P,Q:*p. @R:*p->*p. R P -> R Q
Infix 1 (<=>)

Var equiv_prop : @P,Q:*p. (P->Q) -> (Q->P) -> (P<=>Q)

-- Equiv met K = A->*p.
Def (<==>) := \A:*s. \P,Q:A->*p. @R:(A->*p)->*p. R P -> R Q
Implicit 1 (<==>)
Infix 1 (<==>)

-- Equiv met K = A->B->*p.
Def (<===>) := \A,B:*s. \P,Q:A->B->*p. @R:(A->B->*p)->*p. R P -> R Q
Implicit 2 (<===>)
Infix 1 (<===>)

-- The axiom scheme equiv_pred for propkinds is only introduced for
-- unary predicates and relations.
-- (See Remark 4.5.2 on page 88.)
Var equiv_predQ : @A:*s. @P,Q:A->*p. (@a:A. P a <=> Q a) -> P <==> Q

Var equiv_predR : @A,B:*s. @P,Q:A->B->*p. (@a:A.@b:B. P a b <=> Q a b) -> 
                                          P <===> Q


-------------------------
-------------------------
--                     --
--  2.  L I B R A R Y  --
--                     --
-------------------------
-------------------------

Prove ex_falso : @P:*p. False->P

-- Indicate that this lemma must used by the FalseE tactic
Use FalseE ex_falso                           
  
Prove Not_i : @P:*p. (P->False) -> Not P

-- Indicate that this lemma must used by the NotI tactic
Use NotI Not_i

Prove Not_e : @P:*p. Not P -> P -> False

-- Indicate that this lemma must used by the NotE tactic
Use NotE Not_e

Prove true_True : True
           
Prove And_i : @P,Q:*p. P -> Q -> P/\Q

-- Indicate that this lemma must used by the AndI tactic
Use AndI And_i

Prove And_el : @P,Q:*p. P/\Q -> P

-- Indicate that this lemma must used by the AndEL tactic
Use AndEL And_el

Prove And_er : @P,Q:*p. P/\Q -> Q

-- Indicate that this lemma must used by the AndER tactic
Use AndER And_er

Prove And_sym : @P,Q:*p. P/\Q -> Q/\P

Prove And_assoc : @P,Q,R:*p. P/\(Q/\R) -> (P/\Q)/\R

Prove Or_il : @P,Q:*p. P -> P\/Q

-- Indicate that this lemma must used by the OrIL tactic
Use OrIL Or_il

Prove Or_ir : @P,Q:*p. Q -> P\/Q

-- Indicate that this lemma must used by the OrIR tactic
Use OrIR Or_ir

Prove Or_e : @P,Q,R:*p. P\/Q -> (P->R) -> (Q->R) -> R

-- Indicate that this lemma must used by the OrE tactic
Use OrE Or_e

Prove Or_sym : @P,Q:*p. P\/Q -> Q\/P

Prove Or_assoc : @P,Q,R:*p. P\/Q\/R -> (P\/Q)\/R

-- The next lemma is used by the ExistsI tactic. Therefore we should not
-- write Ex x:A. P x, this is not the correct form for this tactic.
Prove Ex_i : @A:*s.@x:A.@P:A->*p. P x -> (Ex) P

Use ExistsI Ex_i

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

Prove is_refl : @A:*s.@x:A. x=x

-- Indicate that this lemma must used by the Refl tactic
Use Refl is_refl

Prove is_elim_r : @A:*s.@x,y:A.@P:A->*p. x=y -> P x -> P y

-- Indicate that this lemma must used by the Lewrite tactic
Use Lewrite is_elim_r

Prove is_elim_l : @A:*s.@x,y:A.@P:A->*p. x=y -> P y -> P x

-- Indicate that this lemma must used by the Rewrite tactic
Use Rewrite is_elim_l

             
Prove is_sym : @A:*s.@x,y:A. x=y -> y=x

Prove is_trans : @A:*s.@x,y,z:A. x=y -> y=z -> x=z


Prove exm : @P:*p. P \/ Not P
   
Prove contrapos : @P,Q:*p.(Not P -> Q) -> (Not Q -> P)

Prove impl__Or : @P,Q:*p. (Not P -> Q) -> P \/ Q

Prove add_negat : @P:*p. (Not P -> P) -> P