from checker import lib, proof, props
from checker.terms import A1, A2, App, Const
from checker.lib.basic import kernel_from_int
from checker.props import Eq

# Prove : true == not false
p = proof.reflexivity(
    props.Eq(
        x=Const("Bool.True"),
        y=App(f=Const("Bool.not"), x=Const("Bool.False"))
    )
)
p.check(to_stdout=True)

# Prove : false == not true
p = proof.reflexivity(
    props.Eq(
        x=Const("Bool.False"),
        y=App(f=Const("Bool.not"), x=Const("Bool.True"))
    )
)
p.check(to_stdout=True)

# Prove : 4 + 1 == 2 + 3
p = proof.reflexivity(
    props.Eq(
        x=A2(Const("Nat.add"), kernel_from_int(4), kernel_from_int(1)),
        y=A2(Const("Nat.add"), kernel_from_int(2), kernel_from_int(3)),
    )
)
p.check(to_stdout=True)

# Prove : 0 + x = x
p = proof.reflexivity(
    props.Eq(
        x=A2(Const("Nat.add"), kernel_from_int(0), Const("x")),
        y=Const("x"),
    )
)
p.check(to_stdout=True)

# Prove : x + 0 = x

# # SHOULD RAISE EXCEPTION
# p = proof.reflexivity(
#     props.Eq(
#         x=A2(Const("Nat.add"), Const("x"), kernel_from_int(0)),
#         y=Const("x"),
#     )
# )
# p.check(to_stdout=True)

case_1 = proof.eq_l(
    proof=proof.reflexivity(
        Eq(
            x = A2(Const("Nat.add"), Const("Nat.Zero"), Const("Nat.Zero")),
            y = Const("Nat.Zero")
        )
    ),
    eq=Eq(x=Const("x"), y=Const("Nat.Zero")),
    statement=Eq(
        x=A2(Const("Nat.add"), Const("x"), Const("Nat.Zero")),
        y=Const("x")
    ),
)
case_1.check(is_lemma=True, to_stdout=True)

case_2 = proof.eq_l(
    proof=proof.eq_l(
        proof=proof.reflexivity(Eq(
            x=A1(Const("Nat.Succ"), Const("n")),
            y=A1(Const("Nat.Succ"), Const("n")),
        )),
        eq=Eq(x=A2(Const("Nat.add"), Const("n"), Const("Nat.Zero")), y=Const("n")),
        statement=Eq(
            x=A2(Const("Nat.add"), A1(Const("Nat.Succ"), Const("n")), Const("Nat.Zero")),
            y=A1(Const("Nat.Succ"), Const("n")),
        ),
    ),
    eq=Eq(x=Const("x"), y=A1(Const("Nat.Succ"), Const("n"))),
    statement=Eq(
        x=A2(Const("Nat.add"), Const("x"), Const("Nat.Zero")),
        y=Const("x"),
    ),
)
case_2.check(is_lemma=True, to_stdout=True)