87 lines
2.2 KiB
Python
87 lines
2.2 KiB
Python
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)
|