-- 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)) }