basic_proofs.idr

%default total

p_implies_p : p -> p
p_implies_p x = x

data And a b = MkAnd a b

data Or a b = Left a | Right b

p_implies_p_and_p : p -> And p p
p_implies_p_and_p p =
    MkAnd p p

pqr1 : (And p q -> r) -> (p -> q -> r)
pqr1 f p q =
    f (MkAnd p q)

pqr2 : (p -> q -> r) -> (And p q -> r)
pqr2 f (MkAnd p q) =
    f p q

infixl 9 /\
(/\) : Type -> Type -> Type
(/\) = And

infixl 8 \/
(\/) : Type -> Type -> Type
(\/) = Or

infixl 7 <=>
(<=>) : Type -> Type -> Type
a <=> b = (a -> b, b -> a)


distributivity1 : p /\ (q \/ r) -> p /\ q \/ p /\ r
distributivity1 (MkAnd p rest) =
    case rest of
        Left x => Left (MkAnd p x)
        Right x => Right (MkAnd p x)

distributivity2 : p /\ q \/ p /\ r -> p /\ (q \/ r)
distributivity2 x =
    case x of
        Left (MkAnd a b) => MkAnd a (Left b)
        Right (MkAnd a b) => MkAnd a (Right b)

distributivity : p /\ (q \/ r) <=> p /\ q \/ p /\ r
distributivity =
    (distributivity1, distributivity2)


not : Type -> Type
not x =
    x -> Void

doubleNegation : p -> not (not p)
doubleNegation p pToVoid = void (pToVoid p)


deMorganOr1 : not (p \/ q) -> not p /\ not q
deMorganOr1 notPorQ =
    MkAnd (notPorQ . Left) (notPorQ . Right)

deMorganOr2 : not p /\ not q -> not (p \/ q)
deMorganOr2 (MkAnd pToVoid qToVoid) porq =
    case porq of
        Left p => pToVoid p
        Right q => qToVoid q

deMorganOr : not (p \/ q) <=> not p /\ not q
deMorganOr = (deMorganOr1, deMorganOr2)