-- vim:ts=4:syntax=off

#include "basiclib"


-------------
--	"AND": --
-------------
AND (A:Type,B:Type): Type == Record(fst:A,snd:B);

ANDIntro(A:Type,B:Type,a:A,b:B):AND(A,B) == [a,b];
ANDElim1(A:Type,B:Type,p:AND(A,B)):A     == p.fst;
ANDElim2(A:Type,B:Type,p:AND(A,B)):B     == p.snd;

-- An example proof that A&B => B&A

flip(A:Type,B:Type,p:AND(A,B)):AND(B,A) ==
    ANDIntro(B,A,ANDElim2(A,B,p),ANDElim1(A,B,p));

-------------
--	"OR":  --
-------------
OR(A:Type, B:Type) : Type == Union(inl:A, inr:B);

ORIntro1(A:Type,B:Type,a:A):OR(A,B) == union (inl==a);

ORIntro2(A:Type,B:Type,b:B):OR(A,B) == union (inr==b);
ORElim  (A:Type,B:Type,C:Type, f: (a:A)->C, g: (b:B)->C, p:OR(A,B)) : C
  == if (p case inl) then f(p.inl) else g(p.inr) ;

-- The example that ((A\/B)=>C) => (A=>C)&(B=>C)

andOr(A:Type, B:Type, C:Type, p: (x: OR(A,B)) -> C) :
     AND((a:A)->C, (b:B) ->C)
     == ANDIntro((a:A)->C,
                 (b:B)->C,
                 (a:A):C +-> p (ORIntro1(A,B,a)),
                 (b:B):C +-> p (ORIntro2(A,B,b)));

------------
-- "NOT": --
------------
-- The unencapsulated negation type: NOT

exfalso : (e: Exit, B: Type) -> B;  -- No body; this function returns ERROR

NOT(A:Type) : Type == (a:A)-> Exit;

notIntro (A:Type, p: (a:A) -> Exit) : NOT(A) == p;
notElim  (A:Type, p:NOT(A), q:A):  Exit      == p (q) ;

contraRule: (A:Type, B:Type, p:NOT(A), q:A) -> B
        == exfalso (notElim (A,p,q), B);

-- Example ((A=>B)&(A=>~B))=>(A=>C)

contraAx (A:Type, B:Type, C:Type, p: AND((a:A)->B, (a:A)->NOT(B))) :
	(a:A)->C
    ==
    {   X: Type == (a:A)->B;         -- used below as
        Y: Type == (a:A)->NOT(B);    -- abbreviations

      (a:A):C +->
      contraRule(B,C,
				(ANDElim2(X, Y, p))(a),
				(ANDElim1(X, Y, p))(a))
    }