lean2/tests/lua/tc_bug1.lua

local env = environment()
local N   = Const("N")
local p   = Const("p")
local q   = Const("q")
local a   = Const("a")
local b   = Const("b")
local f   = Const("f")
local H1  = Const("H1")
local H2  = Const("H2")
local And = Const("and")
local and_intro = Const("and_intro")
local A   = Local("A", Bool)
local B   = Local("B", Bool)
local C   = Local("C", Bool)
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_var_decl("p", mk_arrow(N, N, Bool)))
env = add_decl(env, mk_var_decl("q", mk_arrow(N, Bool)))
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_var_decl("b", N))
env = add_decl(env, mk_var_decl("and", mk_arrow(Bool, Bool, Bool)))
env = add_decl(env, mk_var_decl("and_intro", Pi({A, B}, mk_arrow(A, B, And(A, B)))))
env = add_decl(env, mk_var_decl("foo_intro",  Pi({A, B, C}, mk_arrow(B, B))))
env = add_decl(env, mk_var_decl("foo_intro2", Pi({A, B, C}, mk_arrow(B, B))))
env = add_decl(env, mk_axiom("Ax1", q(a)))
env = add_decl(env, mk_axiom("Ax2", q(a)))
env = add_decl(env, mk_axiom("Ax3", q(b)))
local Ax1 = Const("Ax1")
local Ax2 = Const("Ax2")
local Ax3 = Const("Ax3")
local foo_intro  = Const("foo_intro")
local foo_intro2 = Const("foo_intro2")
local ng  = name_generator("foo")
local tc  = type_checker(env, ng)
local m1  = mk_metavar("m1", Bool)
print("before is_def_eq")
assert(not tc:is_def_eq(and_intro(m1, q(a)), and_intro(q(a), q(b))))
assert(not tc:next_cnstr())
local tc  = type_checker(env, ng)
assert(tc:is_def_eq(foo_intro(m1, q(a), q(a), Ax1), foo_intro(q(a), q(a), q(a), Ax2)))
local c = tc:next_cnstr()
assert(c)
assert(not tc:next_cnstr())
assert(c:lhs() == m1)
assert(c:rhs() == q(a))
local tc  = type_checker(env, ng)
assert(not tc:next_cnstr())
print(tostring(foo_intro) .. " : " .. tostring(tc:check(foo_intro)))
print(tostring(foo_intro2) .. " : " .. tostring(tc:check(foo_intro2)))
assert(tc:is_def_eq(foo_intro, foo_intro2))
print("before is_def_eq2")
assert(tc:is_def_eq(foo_intro(m1, q(a), q(b), Ax1), foo_intro2(q(a), q(a), q(a), Ax2)))
assert(not tc:next_cnstr())
local tc  = type_checker(env, ng)
print("before failure")
assert(not pcall(function() print(tc:check(and_intro(m1, q(a), Ax1, Ax3))) end))
assert(not tc:next_cnstr())
print("before success")
print(tc:check(and_intro(m1, q(a), Ax1, Ax2)))
assert(tc:next_cnstr())
assert(not tc:next_cnstr())