import Prelude.Algebra
import Prelude.Basics
import Prelude.Bool
import Prelude.Cast
import Prelude.Interfaces
import Prelude.Uninhabited

--Task 1
-- Refl {y = x} : x = x
--a)
total eqSym: x = y -> y = x
eqSym Refl = Refl
--b)
total eqTran: x = y -> y = z -> x = z
eqTran Refl Refl = Refl
--c)
total eqCong: {P: a -> b} -> x = y -> P x = P y
eqCong Refl = Refl

--Task 2

--a)
total plusZero: (x: Nat) -> x = x + Z
plusZero Z = Refl
plusZero (S x) = rewrite (plusZero x) in Refl

--b)
total onePlus: (x: Nat) -> S x = x + 1
onePlus Z = Refl
onePlus (S k) = rewrite (onePlus k) in Refl
--c)
total plusOne: (x: Nat) -> S x = 1 + x
plusOne n = Refl

--f!!!)
total plusSucRightSuc : (x : Nat) -> (y : Nat) -> S (x + y) = x + (S y)
plusSucRightSuc Z y = Refl
plusSucRightSuc (S x) y = rewrite (plusSucRightSuc x y) in Refl

--d)
total plusSucTwice: (x: Nat) -> (S x) + (S x) = S (S (x + x))
plusSucTwice x = rewrite (plusSucRightSuc x x) in Refl


--e)
total plusLeftSuccRightSucc: (x: Nat) -> (y: Nat) -> (S x) + (S y) = S (S (x + y))
plusLeftSuccRightSucc x y = rewrite (plusSucRightSuc x y) in Refl

--g)
total plusCom: (x: Nat) -> (y: Nat) -> x + y = y + x
plusCom Z y = plusZero y
plusCom (S x) y =
                rewrite (plusCom x y) in
                rewrite (plusSucRightSuc y x) in Refl

--h)
total plusAssoc: (x: Nat) -> (y: Nat) -> (z: Nat) -> x + (y + z) = (x + y) + z
plusAssoc Z y z = Refl
plusAssoc (S x) y z = rewrite (plusAssoc x y z) in Refl



--3

as : a -> a=a
as x = Refl


--a

total mulZero : (x:Nat) -> Z = x * Z
mulZero Z = Refl
mulZero (S x) = rewrite (mulZero x) in Refl

--b

total zeroMul : (x:Nat) -> Z = Z * x
zeroMul x = Refl

--c

total oneMul : (x:Nat) -> x = 1 * x
oneMul Z = Refl
oneMul (S x) = rewrite (plusZero x) in Refl


--d
total mulOne : (x:Nat) -> x = x * 1
mulOne Z = Refl
mulOne (S x) = rewrite (mulOne x) in Refl

--e

total mulRighSuc : (x: Nat) -> (y: Nat) -> x * (S y) = x + x * y
mulRighSuc Z y = Refl
mulRighSuc (S x) y =
    rewrite mulRighSuc x y in
    rewrite plusAssoc y x (x * y) in
    rewrite plusCom y x in
    rewrite eqSym (plusAssoc x y (x * y)) in
            Refl



total mulCom : (x: Nat) -> (y: Nat) -> x * y = y * x
mulCom Z y = mulZero y
mulCom (S x) y =
    rewrite mulCom x y in
    rewrite eqSym (mulRighSuc y x) in
        Refl



--f
total mulPlusDis2 : (x: Nat) -> (y: Nat) -> (z: Nat) -> (x + y) * z = x * z + y * z
mulPlusDis2 Z x y = Refl
mulPlusDis2 (S x) y z =
    rewrite mulPlusDis2 x y z in
    rewrite plusAssoc z (x * z) (y * z) in
    Refl

total mulAssoc : (x: Nat) -> (y: Nat) -> (z: Nat) -> x * (y * z) = (x * y) * z
mulAssoc Z y z = Refl
mulAssoc (S x) y z =
    rewrite mulAssoc x y z in
    rewrite eqSym (mulPlusDis2 y (x * y) z) in Refl

--g

total mulPlusDis : (x: Nat) -> (y: Nat) -> (z: Nat) -> x * (y + z) = x * y + x * z
mulPlusDis Z y z = Refl

mulPlusDis (S x) y z =
    rewrite (mulPlusDis x y z) in
    rewrite plusAssoc (plus y (mult x y)) z (mult x z) in
    rewrite eqSym (plusAssoc y (mult x y) z) in
    rewrite plusCom (mult x y) z in
    rewrite plusAssoc y z (mult x y) in
    rewrite plusAssoc (plus y z) (mult x y) (mult x z) in
            Refl


qasd : LTE 0 4
qasd = LTEZero

-- Task 4
--a
t1 : LTE 3 5
t1  = (LTESucc (LTESucc  (LTESucc  LTEZero {right = 2} )))

--b
total grLte : LTE x y -> LTE x (S y)
grLte LTEZero = LTEZero
grLte (LTESucc x) = LTESucc ( grLte x)

--c
total grLten : (n : Nat) -> LTE x y -> LTE (x + n) (y + n)
grLten {x = x1} {y = y1} Z x =
    rewrite eqSym (plusZero x1) in
    rewrite eqSym (plusZero y1) in x
grLten {x = x1} {y = y1} (S k) a  =
    rewrite eqSym(plusSucRightSuc x1 k) in
    rewrite eqSym(plusSucRightSuc y1 k) in  LTESucc (grLten k a)

--Task 5

GRT : Nat -> Nat -> Type
GRT left right = LTE (S right) left

total tr : (x : Nat) -> (y :Nat) -> Either (LTE x y) (GRT x y)
tr Z y = Left LTEZero
tr (S k) Z = Right (LTESucc LTEZero)
tr (S a) (S b) = case tr a b of
                    Left x => Left (LTESucc x)
                    Right x => Right (LTESucc x)

--task 6
total sub : Nat -> Nat -> Nat
sub Z y = Z
sub (S x) Z = S x
sub (S x) (S y) = sub x y
subS : (x:Nat) -> (y : Nat) -> sub (S x) (S y) = sub x y
subS x y = Refl

subS2 : (x:Nat)  -> sub x Z = x
subS2 Z = Refl
subS2 (S k) = Refl

subS3 : (x : Nat) -> (y : Nat) -> sub x y = sub (S x) (S y)
subS3 x y  = Refl


--a

total subP1 : LTE x y -> sub x y = Z
subP1 LTEZero = Refl
subP1 (LTESucc x) = rewrite (subP1 x) in Refl

--b
subP2 : sub x y = Z -> LTE x y
subP2 {x = Z} {y = y1} a = LTEZero
{-
subP2 {x = (S x1)} {y = (S y1)} a = LTESucc ( ?r)


--c
subP3 : LTE y x -> y + (sub x y) = x
subP3 {x = x1} LTEZero = rewrite  (subS2 x1) in Refl
--subP3 {x = x1} {y = y1} (LTESucc a) =
-}
main: IO()
main = putStr "Hello"