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

# 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()

# 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()

# 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)),
    )
)