30 lines
684 B
Python
30 lines
684 B
Python
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)),
|
|
)
|
|
)
|