feat(builtin): automatically generate Lean/C++ interface for builtin theories

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-09 18:09:53 -08:00
parent a339a53f50
commit 411f14415d
73 changed files with 1416 additions and 994 deletions

View file

@ -67,6 +67,20 @@ function(add_theory FILE DEPS)
endif()
endfunction()
# The following command invokes the lean binary to update .cpp/.h interface files
# associated with a .lean file.
function(update_interface FILE DEST ARG)
get_filename_component(BASENAME ${FILE} NAME_WE)
set(CPPFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.cpp")
set(HFILE "${LEAN_SOURCE_DIR}/${DEST}/${BASENAME}_decls.h")
add_custom_command(OUTPUT ${CPPFILE} ${HFILE}
COMMAND ${SHELL_DIR}/lean ${ARG} -q ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${CMAKE_CURRENT_SOURCE_DIR}/name_conv.lua ${CMAKE_CURRENT_SOURCE_DIR}/lean2cpp.lean > ${CPPFILE}
COMMAND ${SHELL_DIR}/lean ${ARG} -q ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${CMAKE_CURRENT_SOURCE_DIR}/name_conv.lua ${CMAKE_CURRENT_SOURCE_DIR}/lean2h.lean > ${HFILE}
DEPENDS ${FILE})
add_custom_target("${BASENAME}_decls" DEPENDS ${CPPFILE})
add_dependencies(builtin ${BASENAME}_decls)
endfunction()
add_kernel_theory("kernel.lean" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua")
add_kernel_theory("Nat.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
@ -75,3 +89,8 @@ add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean")
add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
update_interface("kernel.lean" "kernel" "-n")
update_interface("Nat.lean" "library/arith" "-n")
update_interface("Int.lean" "library/arith" "")
update_interface("Real.lean" "library/arith" "")

View file

@ -61,7 +61,7 @@ axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A
axiom allext {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x)
-- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
:= subst H1 H2
theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
@ -267,12 +267,6 @@ theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false
:= boolext (λ H, absurd (and_eliml H) (and_elimr H))
(λ H, false_elim (a ∧ ¬ a) H)
theorem not_true : (¬ true) == false
:= trivial
theorem not_false : (¬ false) == true
:= trivial
theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ¬ b)
:= case (λ x, (¬ (x ∧ b)) == (¬ x ¬ b))
(case (λ y, (¬ (true ∧ y)) == (¬ true ¬ y)) trivial trivial b)

32
src/builtin/lean2cpp.lean Normal file
View file

@ -0,0 +1,32 @@
(*
-- Auxiliary script for generating .cpp files that define
-- constants defined in Lean
local env = get_environment()
local num_imports = 0
print('/*')
print('Copyright (c) 2013 Microsoft Corporation. All rights reserved.')
print('Released under Apache 2.0 license as described in the file LICENSE.')
print('*/')
print("// Automatically generated file, DO NOT EDIT")
print('#include "kernel/environment.h"')
print('#include "kernel/decl_macros.h"')
print('namespace lean {')
for obj in env:objects() do
if obj:is_begin_import() or obj:is_begin_builtin_import() then
num_imports = num_imports + 1
elseif obj:is_end_import() then
num_imports = num_imports - 1
elseif num_imports == 0 and obj:has_name() and obj:has_type() and not is_explicit(env, obj:get_name()) and not obj:is_builtin() then
local is_fn = env:normalize(obj:get_type()):is_pi()
io.write('MK_CONSTANT(')
name_to_cpp_decl(obj:get_name())
if is_fn then
io.write('_fn')
end
io.write(', ')
name_to_cpp_expr(obj:get_name())
print(');')
end
end
print('}')
*)

71
src/builtin/lean2h.lean Normal file
View file

@ -0,0 +1,71 @@
(*
-- Auxiliary script for generating .h file that declare mk_* and is_* functions for
-- constants defined in Lean
local env = get_environment()
local num_imports = 0
print('/*')
print('Copyright (c) 2013 Microsoft Corporation. All rights reserved.')
print('Released under Apache 2.0 license as described in the file LICENSE.')
print('*/')
print("// Automatically generated file, DO NOT EDIT")
print('#include "kernel/expr.h"')
print('namespace lean {')
for obj in env:objects() do
if obj:is_begin_import() or obj:is_begin_builtin_import() then
num_imports = num_imports + 1
elseif obj:is_end_import() then
num_imports = num_imports - 1
elseif num_imports == 0 and obj:has_name() and obj:has_type() and not is_explicit(env, obj:get_name()) and not obj:is_builtin() then
local ty = env:normalize(obj:get_type())
local is_fn = ty:is_pi()
local arity = 0
while ty:is_pi() do
n, d, ty = ty:fields()
arity = arity + 1
end
local is_th = obj:is_theorem() or obj:is_axiom()
io.write("expr mk_")
name_to_cpp_decl(obj:get_name())
if is_fn then
io.write("_fn");
end
print("();")
io.write("bool is_")
name_to_cpp_decl(obj:get_name())
if is_fn then
io.write("_fn");
end
print("(expr const & e);")
if is_fn and not is_th then
io.write("inline bool is_")
name_to_cpp_decl(obj:get_name())
io.write("(expr const & e) { return is_app(e) && is_");
name_to_cpp_decl(obj:get_name())
print("_fn(arg(e, 0)); }")
end
if is_fn then
io.write("inline expr mk_")
name_to_cpp_decl(obj:get_name())
if is_th then
io.write("_th");
end
io.write("(");
for i = 1, arity do
if i > 1 then
io.write(", ")
end
io.write("expr const & e" .. tostring(i))
end
io.write(") { return mk_app({mk_");
name_to_cpp_decl(obj:get_name())
io.write("_fn()")
for i = 1, arity do
io.write(", e" .. tostring(i))
end
print ("}); }")
end
end
end
print('}')
*)

38
src/builtin/name_conv.lua Normal file
View file

@ -0,0 +1,38 @@
-- Output a C++ statement that creates the given name
function name_to_cpp_expr(n)
function rec(n)
if not n:is_atomic() then
rec(n:get_prefix())
io.write(", ")
end
if n:is_string() then
io.write("\"" .. n:get_string() .. "\"")
else
error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n))
end
end
io.write("name(")
if n:is_atomic() then
rec(n)
else
io.write("{")
rec(n)
io.write("}")
end
io.write(")")
end
-- Output a C++ constant name based on the given hierarchical name
-- It uses '_' to glue the hierarchical name parts
function name_to_cpp_decl(n)
if not n:is_atomic(n) then
name_to_cpp_decl(n:get_prefix())
io.write("_")
end
if n:is_string() then
io.write(n:get_string())
else
error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n))
end
end

Binary file not shown.

View file

@ -44,34 +44,20 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans
m_trans_ops.emplace_front(op1, op2, d);
}
static name g_eq_imp_trans("eq_imp_trans");
static name g_imp_eq_trans("imp_eq_trans");
static name g_imp_trans("imp_trans");
static name g_eq_ne_trans("eq_ne_trans");
static name g_ne_eq_trans("ne_eq_trans");
static name g_neq("neq");
calc_proof_parser::calc_proof_parser() {
expr imp = mk_implies_fn();
expr eq = mk_homo_eq_fn();
expr iff = mk_iff_fn();
expr neq = mk_constant(g_neq);
expr eq = mk_eq_fn();
expr neq = mk_neq_fn();
add_supported_operator(op_data(imp, 2));
add_supported_operator(op_data(eq, 3));
add_supported_operator(op_data(iff, 2));
add_supported_operator(op_data(neq, 3));
add_trans_step(eq, eq, trans_data(mk_trans_fn(), 6, eq));
add_trans_step(eq, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp));
add_trans_step(imp, eq, trans_data(mk_constant(g_imp_eq_trans), 5, imp));
add_trans_step(imp, imp, trans_data(mk_constant(g_imp_trans), 5, imp));
add_trans_step(iff, iff, trans_data(mk_trans_fn(), 6, iff));
add_trans_step(iff, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp));
add_trans_step(imp, iff, trans_data(mk_constant(g_imp_eq_trans), 5, imp));
add_trans_step(eq, iff, trans_data(mk_trans_fn(), 6, iff));
add_trans_step(iff, eq, trans_data(mk_trans_fn(), 6, iff));
add_trans_step(eq, neq, trans_data(mk_constant(g_eq_ne_trans), 6, neq));
add_trans_step(neq, eq, trans_data(mk_constant(g_ne_eq_trans), 6, neq));
add_trans_step(eq, imp, trans_data(mk_eq_imp_trans_fn(), 5, imp));
add_trans_step(imp, eq, trans_data(mk_imp_eq_trans_fn(), 5, imp));
add_trans_step(imp, imp, trans_data(mk_imp_trans_fn(), 5, imp));
add_trans_step(eq, neq, trans_data(mk_eq_ne_trans_fn(), 6, neq));
add_trans_step(neq, eq, trans_data(mk_ne_eq_trans_fn(), 6, neq));
}
optional<expr> calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const {
@ -108,11 +94,11 @@ static expr parse_step_pr(parser_imp & imp, expr const & lhs) {
expr eq_pr = imp.parse_expr();
imp.check_rcurly_next("invalid calculational proof, '}' expected");
// Using axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b.
return imp.save(Subst(imp.save(mk_placeholder(), p),
return imp.save(mk_subst_th(imp.save(mk_placeholder(), p),
imp.save(mk_placeholder(), p),
imp.save(mk_placeholder(), p),
imp.save(mk_placeholder(), p), // let elaborator compute the first four arguments
imp.save(Refl(imp.save(mk_placeholder(), p), lhs), p),
imp.save(mk_refl_th(imp.save(mk_placeholder(), p), lhs), p),
eq_pr), p);
} else {
return imp.parse_expr();

View file

@ -561,11 +561,11 @@ expr parser_imp::parse_led_id(expr const & left) {
}
/** \brief Parse <tt>expr '=' expr</tt>. */
expr parser_imp::parse_eq(expr const & left) {
expr parser_imp::parse_heq(expr const & left) {
auto p = pos();
next();
expr right = parse_expr(g_eq_precedence);
return save(mk_eq(left, right), p);
return save(mk_heq(left, right), p);
}
/** \brief Parse <tt>expr '->' expr</tt>. */
@ -947,7 +947,7 @@ expr parser_imp::mk_app_left(expr const & left, expr const & arg) {
expr parser_imp::parse_led(expr const & left) {
switch (curr()) {
case scanner::token::Id: return parse_led_id(left);
case scanner::token::Eq: return parse_eq(left);
case scanner::token::Eq: return parse_heq(left);
case scanner::token::Arrow: return parse_arrow(left);
case scanner::token::LeftParen: return mk_app_left(left, parse_lparen());
case scanner::token::IntVal: return mk_app_left(left, parse_nat_int());

View file

@ -291,7 +291,7 @@ private:
pos_info const & p);
expr parse_expr_macro(name const & id, pos_info const & p);
expr parse_led_id(expr const & left);
expr parse_eq(expr const & left);
expr parse_heq(expr const & left);
expr parse_arrow(expr const & left);
expr parse_lparen();
void parse_names(buffer<std::pair<pos_info, name>> & result);

View file

@ -234,7 +234,7 @@ class pp_fn {
return is_atomic(arg(e, 1));
else
return false;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::HEq: case expr_kind::Let:
return false;
}
return false;
@ -441,7 +441,7 @@ class pp_fn {
operator_info op = get_operator(e);
if (op) {
return op.get_precedence();
} else if (is_eq(e)) {
} else if (is_heq(e)) {
return g_eq_precedence;
} else if (is_arrow(e)) {
return g_arrow_precedence;
@ -459,7 +459,7 @@ class pp_fn {
operator_info op = get_operator(e);
if (op) {
return op.get_fixity() == fx;
} else if (is_eq(e)) {
} else if (is_heq(e)) {
return fixity::Infix == fx;
} else if (is_arrow(e)) {
return fixity::Infixr == fx;
@ -1022,7 +1022,7 @@ class pp_fn {
}
/** \brief Pretty print the child of an equality. */
result pp_eq_child(expr const & e, unsigned depth) {
result pp_heq_child(expr const & e, unsigned depth) {
if (is_atomic(e)) {
return pp(e, depth + 1);
} else {
@ -1034,11 +1034,11 @@ class pp_fn {
}
/** \brief Pretty print an equality */
result pp_eq(expr const & e, unsigned depth) {
result pp_heq(expr const & e, unsigned depth) {
result p_arg1, p_arg2;
format r_format;
p_arg1 = pp_eq_child(eq_lhs(e), depth);
p_arg2 = pp_eq_child(eq_rhs(e), depth);
p_arg1 = pp_heq_child(heq_lhs(e), depth);
p_arg2 = pp_heq_child(heq_rhs(e), depth);
r_format = group(format{p_arg1.first, space(), g_eq_fmt, line(), p_arg2.first});
return mk_result(r_format, p_arg1.second + p_arg2.second + 1);
}
@ -1121,7 +1121,7 @@ class pp_fn {
case expr_kind::Lambda:
case expr_kind::Pi: r = pp_abstraction(e, depth); break;
case expr_kind::Type: r = pp_type(e); break;
case expr_kind::Eq: r = pp_eq(e, depth); break;
case expr_kind::HEq: r = pp_heq(e, depth); break;
case expr_kind::Let: r = pp_let(e, depth); break;
case expr_kind::MetaVar: r = pp_metavar(e, depth); break;
}

View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/io_state.h"
#include "kernel/decl_macros.h"
#include "kernel/kernel_decls.cpp"
namespace lean {
// =======================================
@ -19,7 +20,6 @@ expr const TypeU = Type(u_lvl);
// =======================================
// Boolean Type
MK_CONSTANT(Bool, "Bool");
expr const Bool = mk_Bool();
expr mk_bool_type() { return mk_Bool(); }
bool is_bool(expr const & t) { return is_Bool(t); }
@ -116,57 +116,6 @@ static register_builtin_fn if_blt("ite", []() { return mk_if_fn(); });
static value::register_deserializer_fn if_ds("ite", [](deserializer & ) { return mk_if_fn(); });
// =======================================
MK_CONSTANT(implies_fn, name("implies"));
MK_CONSTANT(iff_fn, name("iff"));
MK_CONSTANT(and_fn, name("and"));
MK_CONSTANT(or_fn, name("or"));
MK_CONSTANT(not_fn, name("not"));
MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(homo_eq_fn, name("eq"));
// Axioms
MK_CONSTANT(mp_fn, name("mp"));
MK_CONSTANT(discharge_fn, name("discharge"));
MK_CONSTANT(case_fn, name("case"));
MK_CONSTANT(refl_fn, name("refl"));
MK_CONSTANT(subst_fn, name("subst"));
MK_CONSTANT(abst_fn, name("funext"));
MK_CONSTANT(htrans_fn, name("htrans"));
MK_CONSTANT(hsymm_fn, name("hsymm"));
// Theorems
MK_CONSTANT(eta_fn, name("eta"));
MK_CONSTANT(imp_antisym_fn, name("iffintro"));
MK_CONSTANT(trivial, name("trivial"));
MK_CONSTANT(false_elim_fn, name("false_elim"));
MK_CONSTANT(absurd_fn, name("absurd"));
MK_CONSTANT(em_fn, name("em"));
MK_CONSTANT(double_neg_fn, name("doubleneg"));
MK_CONSTANT(double_neg_elim_fn, name("doubleneg_elim"));
MK_CONSTANT(mt_fn, name("mt"));
MK_CONSTANT(contrapos_fn, name("contrapos"));
MK_CONSTANT(absurd_elim_fn, name("absurd_elim"));
MK_CONSTANT(eq_mp_fn, name("eqmp"));
MK_CONSTANT(not_imp1_fn, name("not_imp_eliml"));
MK_CONSTANT(not_imp2_fn, name("not_imp_elimr"));
MK_CONSTANT(conj_fn, name("and_intro"));
MK_CONSTANT(conjunct1_fn, name("and_eliml"));
MK_CONSTANT(conjunct2_fn, name("and_elimr"));
MK_CONSTANT(disj1_fn, name("or_introl"));
MK_CONSTANT(disj2_fn, name("or_intror"));
MK_CONSTANT(disj_cases_fn, name("or_elim"));
MK_CONSTANT(refute_fn, name("refute"));
MK_CONSTANT(symm_fn, name("symm"));
MK_CONSTANT(trans_fn, name("trans"));
MK_CONSTANT(congr1_fn, name("congr1"));
MK_CONSTANT(congr2_fn, name("congr2"));
MK_CONSTANT(congr_fn, name("congr"));
MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
MK_CONSTANT(forall_elim_fn, name("forall_elim"));
MK_CONSTANT(forall_intro_fn, name("forall_intro"));
MK_CONSTANT(exists_elim_fn, name("exists_elim"));
MK_CONSTANT(exists_intro_fn, name("exists_intro"));
void import_kernel(environment const & env, io_state const & ios) {
env->import("kernel", ios);
}

View file

@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "kernel/io_state.h"
#include "kernel/kernel_decls.h"
namespace lean {
// See src/builtin/kernel.lean for signatures.
@ -32,191 +33,12 @@ bool is_true(expr const & e);
/** \brief Return true iff \c e is the Lean false value. */
bool is_false(expr const & e);
expr mk_if_fn();
bool is_if_fn(expr const & e);
inline bool is_if(expr const & e) { return is_app(e) && is_if_fn(arg(e, 0)); }
inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); }
inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); }
inline expr mk_bool_if(expr const & c, expr const & t, expr const & e) { return mk_if(mk_bool_type(), c, t, e); }
inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool_if(c, t, e); }
expr mk_implies_fn();
bool is_implies_fn(expr const & e);
inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app(mk_implies_fn(), e1, e2); }
inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
expr mk_iff_fn();
bool is_iff_fn(expr const & e);
inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); }
inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app(mk_iff_fn(), e1, e2); }
inline expr Iff(expr const & e1, expr const & e2) { return mk_iff(e1, e2); }
expr mk_and_fn();
bool is_and_fn(expr const & e);
inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); }
inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
expr mk_or_fn();
bool is_or_fn(expr const & e);
inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); }
inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); }
inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); }
expr mk_not_fn();
bool is_not_fn(expr const & e);
inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); }
inline expr Not(expr const & e) { return mk_not(e); }
expr mk_forall_fn();
bool is_forall_fn(expr const & e);
inline bool is_forall(expr const & e) { return is_app(e) && is_forall_fn(arg(e, 0)); }
inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); }
inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); }
expr mk_exists_fn();
bool is_exists_fn(expr const & e);
inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); }
inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
// inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_eq(A, l, r); }
expr mk_homo_eq_fn();
bool is_homo_eq_fn(expr const & e);
inline bool is_homo_eq(expr const & e) { return is_app(e) && is_homo_eq_fn(arg(e, 0)); }
inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }
expr mk_mp_fn();
inline expr MP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mp_fn(), a, b, H1, H2); }
expr mk_discharge_fn();
inline expr Discharge(expr const & a, expr const & b, expr const & H) { return mk_app(mk_discharge_fn(), a, b, H); }
expr mk_case_fn();
inline expr Case(expr const & P, expr const & H1, expr const & H2, expr const & a) { return mk_app(mk_case_fn(), P, H1, H2, a); }
expr mk_refl_fn();
inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); }
expr mk_subst_fn();
inline expr Subst(expr const & A, expr const & a, expr const & b, expr const & P, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, a, b, P, H1, H2}); }
expr mk_eta_fn();
inline expr Eta(expr const & A, expr const & B, expr const & f) { return mk_app(mk_eta_fn(), A, B, f); }
expr mk_imp_antisym_fn();
inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
expr mk_abst_fn();
inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, expr const & H) { return mk_app({mk_abst_fn(), A, B, f, g, H}); }
expr mk_hsymm_fn();
inline expr HSymm(expr const & A, expr const & B, expr const & a, expr const & b, expr const & H1) { return mk_app({mk_hsymm_fn(), A, B, a, b, H1}); }
expr mk_htrans_fn();
inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) {
return mk_app({mk_htrans_fn(), A, B, C, a, b, c, H1, H2});
}
expr mk_trivial();
#define Trivial mk_trivial()
expr mk_true_ne_false();
#define TrueNeFalse mk_true_ne_false();
expr mk_em_fn();
inline expr EM(expr const & a) { return mk_app(mk_em_fn(), a); }
expr mk_false_elim_fn();
inline expr FalseElim(expr const & a, expr const & H) { return mk_app(mk_false_elim_fn(), a, H); }
expr mk_absurd_fn();
inline expr Absurd(expr const & a, expr const & H1, expr const & H2) { return mk_app(mk_absurd_fn(), a, H1, H2); }
expr mk_double_neg_fn();
inline expr DoubleNeg(expr const & a) { return mk_app(mk_double_neg_fn(), a); }
expr mk_double_neg_elim_fn();
inline expr DoubleNegElim(expr const & P, expr const & H) { return mk_app(mk_double_neg_elim_fn(), P, H); }
expr mk_mt_fn();
inline expr MT(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_mt_fn(), a, b, H1, H2); }
expr mk_contrapos_fn();
inline expr Contrapos(expr const & a, expr const & b, expr const & H) { return mk_app(mk_contrapos_fn(), a, b, H); }
expr mk_false_imp_any_fn();
inline expr FalseImpAny(expr const & a) { return mk_app(mk_false_imp_any_fn(), a); }
expr mk_absurd_elim_fn();
inline expr AbsurdElim(expr const & a, expr const & c, expr const & H1, expr const & H2) {
return mk_app(mk_absurd_elim_fn(), a, c, H1, H2);
}
expr mk_eq_mp_fn();
inline expr EqMP(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_eq_mp_fn(), a, b, H1, H2); }
expr mk_not_imp1_fn();
inline expr NotImp1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp1_fn(), a, b, H); }
expr mk_not_imp2_fn();
inline expr NotImp2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_not_imp2_fn(), a, b, H); }
expr mk_conj_fn();
inline expr Conj(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_conj_fn(), a, b, H1, H2); }
expr mk_conjunct1_fn();
inline expr Conjunct1(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct1_fn(), a, b, H); }
expr mk_conjunct2_fn();
inline expr Conjunct2(expr const & a, expr const & b, expr const & H) { return mk_app(mk_conjunct2_fn(), a, b, H); }
expr mk_disj1_fn();
inline expr Disj1(expr const & a, expr const & H, expr const & b) { return mk_app(mk_disj1_fn(), a, H, b); }
expr mk_disj2_fn();
inline expr Disj2(expr const & b, expr const & a, expr const & H) { return mk_app(mk_disj2_fn(), b, a, H); }
expr mk_disj_cases_fn();
inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); }
expr mk_refute_fn();
inline expr Refute(expr const & a, expr const & H) { return mk_app({mk_refute_fn(), a, H}); }
expr mk_symm_fn();
inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); }
expr mk_trans_fn();
inline expr Trans(expr const & A, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) { return mk_app({mk_trans_fn(), A, a, b, c, H1, H2}); }
expr mk_eqt_elim_fn();
inline expr EqTElim(expr const & a, expr const & H) { return mk_app(mk_eqt_elim_fn(), a, H); }
expr mk_eqt_intro_fn();
inline expr EqTIntro(expr const & a, expr const & H) { return mk_app(mk_eqt_intro_fn(), a, H); }
expr mk_congr1_fn();
inline expr Congr1(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & H) { return mk_app({mk_congr1_fn(), A, B, f, g, a, H}); }
expr mk_congr2_fn();
inline expr Congr2(expr const & A, expr const & B, expr const & a, expr const & b, expr const & f, expr const & H) { return mk_app({mk_congr2_fn(), A, B, a, b, f, H}); }
expr mk_congr_fn();
inline expr Congr(expr const & A, expr const & B, expr const & f, expr const & g, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_congr_fn(), A, B, f, g, a, b, H1, H2}); }
expr mk_forall_elim_fn();
inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); }
expr mk_forall_intro_fn();
inline expr ForallIntro(expr const & A, expr const & P, expr const & H) { return mk_app(mk_forall_intro_fn(), A, P, H); }
expr mk_exists_elim_fn();
inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr const & H1, expr const & H2) { return mk_app({mk_exists_elim_fn(), A, P, B, H1, H2}); }
expr mk_exists_intro_fn();
inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); }
class io_state;
void import_kernel(environment const & env, io_state const & ios);
}

View file

@ -142,13 +142,13 @@ expr mk_app(unsigned n, expr const * as) {
to_app(r)->m_hash = hash_args(new_n, m_args);
return r;
}
expr_eq::expr_eq(expr const & lhs, expr const & rhs):
expr_cell(expr_kind::Eq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()),
expr_heq::expr_heq(expr const & lhs, expr const & rhs):
expr_cell(expr_kind::HEq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()),
m_lhs(lhs),
m_rhs(rhs) {
}
expr_eq::~expr_eq() {}
void expr_eq::dealloc(buffer<expr_cell*> & todelete) {
expr_heq::~expr_heq() {}
void expr_heq::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_rhs, todelete);
dec_ref(m_lhs, todelete);
delete(this);
@ -246,7 +246,7 @@ void expr_cell::dealloc() {
case expr_kind::MetaVar: delete static_cast<expr_metavar*>(it); break;
case expr_kind::Type: delete static_cast<expr_type*>(it); break;
case expr_kind::Constant: static_cast<expr_const*>(it)->dealloc(todo); break;
case expr_kind::Eq: static_cast<expr_eq*>(it)->dealloc(todo); break;
case expr_kind::HEq: static_cast<expr_heq*>(it)->dealloc(todo); break;
case expr_kind::App: static_cast<expr_app*>(it)->dealloc(todo); break;
case expr_kind::Lambda: static_cast<expr_lambda*>(it)->dealloc(todo); break;
case expr_kind::Pi: static_cast<expr_pi*>(it)->dealloc(todo); break;
@ -279,10 +279,10 @@ bool is_arrow(expr const & t) {
}
}
bool is_eq(expr const & e, expr & lhs, expr & rhs) {
if (is_eq(e)) {
lhs = eq_lhs(e);
rhs = eq_rhs(e);
bool is_heq(expr const & e, expr & lhs, expr & rhs) {
if (is_heq(e)) {
lhs = heq_lhs(e);
rhs = heq_rhs(e);
return true;
} else {
return false;
@ -296,7 +296,7 @@ expr copy(expr const & a) {
case expr_kind::Type: return mk_type(ty_level(a));
case expr_kind::Value: return mk_value(static_cast<expr_value*>(a.raw())->m_val);
case expr_kind::App: return mk_app(num_args(a), begin_args(a));
case expr_kind::Eq: return mk_eq(eq_lhs(a), eq_rhs(a));
case expr_kind::HEq: return mk_heq(heq_lhs(a), heq_rhs(a));
case expr_kind::Lambda: return mk_lambda(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Pi: return mk_pi(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
@ -341,7 +341,7 @@ constexpr char g_first_app_size_kind = 32;
constexpr char g_small_app_num_args = 32;
constexpr bool is_small(expr_kind k) { return 0 <= static_cast<char>(k) && static_cast<char>(k) < g_first_app_size_kind; }
static_assert(is_small(expr_kind::Var) && is_small(expr_kind::Constant) && is_small(expr_kind::Value) && is_small(expr_kind::App) &&
is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) && is_small(expr_kind::Eq) &&
is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) && is_small(expr_kind::HEq) &&
is_small(expr_kind::Let) && is_small(expr_kind::MetaVar), "expr_kind is too big");
class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
@ -384,7 +384,7 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
for (unsigned i = 0; i < num_args(a); i++)
write_core(arg(a, i));
break;
case expr_kind::Eq: write_core(eq_lhs(a)); write_core(eq_rhs(a)); break;
case expr_kind::HEq: write_core(heq_lhs(a)); write_core(heq_rhs(a)); break;
case expr_kind::Lambda:
case expr_kind::Pi: s << abst_name(a); write_core(abst_domain(a)); write_core(abst_body(a)); break;
case expr_kind::Let: s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a)); break;
@ -441,9 +441,9 @@ public:
args.push_back(read());
return mk_app(args);
}
case expr_kind::Eq: {
case expr_kind::HEq: {
expr lhs = read();
return mk_eq(lhs, read());
return mk_heq(lhs, read());
}
case expr_kind::Lambda: {
name n = read_name(d);

View file

@ -52,7 +52,7 @@ The main API is divided in the following sections
- Miscellaneous
======================================= */
class expr;
enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, Eq, Let, MetaVar };
enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, HEq, Let, MetaVar };
class local_entry;
/**
\brief A metavariable local context is just a list of local_entries.
@ -142,7 +142,7 @@ public:
friend expr mk_constant(name const & n, optional<expr> const & t);
friend expr mk_value(value & v);
friend expr mk_app(unsigned num_args, expr const * args);
friend expr mk_eq(expr const & l, expr const & r);
friend expr mk_heq(expr const & l, expr const & r);
friend expr mk_lambda(name const & n, expr const & t, expr const & e);
friend expr mk_pi(name const & n, expr const & t, expr const & e);
friend expr mk_type(level const & l);
@ -215,14 +215,14 @@ public:
expr const * end_args() const { return m_args + m_num_args; }
};
/** \brief Heterogeneous equality */
class expr_eq : public expr_cell {
class expr_heq : public expr_cell {
expr m_lhs;
expr m_rhs;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_eq(expr const & lhs, expr const & rhs);
~expr_eq();
expr_heq(expr const & lhs, expr const & rhs);
~expr_heq();
expr const & get_lhs() const { return m_lhs; }
expr const & get_rhs() const { return m_rhs; }
};
@ -392,7 +392,7 @@ inline bool is_var(expr_cell * e) { return e->kind() == expr_kind::Var;
inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Constant; }
inline bool is_value(expr_cell * e) { return e->kind() == expr_kind::Value; }
inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; }
inline bool is_eq(expr_cell * e) { return e->kind() == expr_kind::Eq; }
inline bool is_heq(expr_cell * e) { return e->kind() == expr_kind::HEq; }
inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; }
inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; }
inline bool is_type(expr_cell * e) { return e->kind() == expr_kind::Type; }
@ -404,7 +404,7 @@ inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var;
inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; }
inline bool is_value(expr const & e) { return e.kind() == expr_kind::Value; }
inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; }
inline bool is_eq(expr const & e) { return e.kind() == expr_kind::Eq; }
inline bool is_heq(expr const & e) { return e.kind() == expr_kind::HEq; }
inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; }
inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; }
bool is_arrow(expr const & e);
@ -431,8 +431,8 @@ inline expr mk_app(expr const & e1, expr const & e2) { return mk_app({e1, e2});
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); }
inline expr mk_eq(expr const & l, expr const & r) { return expr(new expr_eq(l, r)); }
inline expr Eq(expr const & l, expr const & r) { return mk_eq(l, r); }
inline expr mk_heq(expr const & l, expr const & r) { return expr(new expr_heq(l, r)); }
inline expr HEq(expr const & l, expr const & r) { return mk_heq(l, r); }
inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline bool is_default_arrow_var_name(name const & n) { return n == "a"; }
@ -464,7 +464,7 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3,
inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); return static_cast<expr_var*>(e); }
inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast<expr_const*>(e); }
inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast<expr_app*>(e); }
inline expr_eq * to_eq(expr_cell * e) { lean_assert(is_eq(e)); return static_cast<expr_eq*>(e); }
inline expr_heq * to_heq(expr_cell * e) { lean_assert(is_heq(e)); return static_cast<expr_heq*>(e); }
inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast<expr_abstraction*>(e); }
inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda(e)); return static_cast<expr_lambda*>(e); }
inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast<expr_pi*>(e); }
@ -475,7 +475,7 @@ inline expr_metavar * to_metavar(expr_cell * e) { lean_assert(is_metavar
inline expr_var * to_var(expr const & e) { return to_var(e.raw()); }
inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); }
inline expr_app * to_app(expr const & e) { return to_app(e.raw()); }
inline expr_eq * to_eq(expr const & e) { return to_eq(e.raw()); }
inline expr_heq * to_heq(expr const & e) { return to_heq(e.raw()); }
inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction(e.raw()); }
inline expr_lambda * to_lambda(expr const & e) { return to_lambda(e.raw()); }
inline expr_pi * to_pi(expr const & e) { return to_pi(e.raw()); }
@ -497,8 +497,8 @@ inline optional<expr> const & const_type(expr_cell * e) { return to_constant(e)
inline value const & to_value(expr_cell * e) { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline expr const & eq_lhs(expr_cell * e) { return to_eq(e)->get_lhs(); }
inline expr const & eq_rhs(expr_cell * e) { return to_eq(e)->get_rhs(); }
inline expr const & heq_lhs(expr_cell * e) { return to_heq(e)->get_lhs(); }
inline expr const & heq_rhs(expr_cell * e) { return to_heq(e)->get_rhs(); }
inline name const & abst_name(expr_cell * e) { return to_abstraction(e)->get_name(); }
inline expr const & abst_domain(expr_cell * e) { return to_abstraction(e)->get_domain(); }
inline expr const & abst_body(expr_cell * e) { return to_abstraction(e)->get_body(); }
@ -530,8 +530,8 @@ inline unsigned num_args(expr const & e) { return to_app(e)->ge
inline expr const & arg(expr const & e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline expr const * begin_args(expr const & e) { return to_app(e)->begin_args(); }
inline expr const * end_args(expr const & e) { return to_app(e)->end_args(); }
inline expr const & eq_lhs(expr const & e) { return to_eq(e)->get_lhs(); }
inline expr const & eq_rhs(expr const & e) { return to_eq(e)->get_rhs(); }
inline expr const & heq_lhs(expr const & e) { return to_heq(e)->get_lhs(); }
inline expr const & heq_rhs(expr const & e) { return to_heq(e)->get_rhs(); }
inline name const & abst_name(expr const & e) { return to_abstraction(e)->get_name(); }
inline expr const & abst_domain(expr const & e) { return to_abstraction(e)->get_domain(); }
inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); }
@ -545,7 +545,7 @@ inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)
inline bool has_metavar(expr const & e) { return e.has_metavar(); }
bool is_eq(expr const & e, expr & lhs, expr & rhs);
bool is_heq(expr const & e, expr & lhs, expr & rhs);
// =======================================
// =======================================
@ -653,15 +653,15 @@ template<typename F> expr update_let(expr const & e, F f) {
else
return e;
}
template<typename F> expr update_eq(expr const & e, F f) {
template<typename F> expr update_heq(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &)>::type,
std::pair<expr, expr>>::value,
"update_eq: return type of f is not pair<expr, expr>");
expr const & old_l = eq_lhs(e);
expr const & old_r = eq_rhs(e);
"update_heq: return type of f is not pair<expr, expr>");
expr const & old_l = heq_lhs(e);
expr const & old_r = heq_rhs(e);
std::pair<expr, expr> p = f(old_l, old_r);
if (!is_eqp(p.first, old_l) || !is_eqp(p.second, old_r))
return mk_eq(p.first, p.second);
return mk_heq(p.first, p.second);
else
return e;
}

View file

@ -64,7 +64,7 @@ class expr_eq_fn {
if (!apply(arg(a, i), arg(b, i)))
return false;
return true;
case expr_kind::Eq: return apply(eq_lhs(a), eq_lhs(b)) && apply(eq_rhs(a), eq_rhs(b));
case expr_kind::HEq: return apply(heq_lhs(a), heq_lhs(b)) && apply(heq_rhs(a), heq_rhs(b));
case expr_kind::Lambda: // Remark: we ignore get_abs_name because we want alpha-equivalence
case expr_kind::Pi: return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
case expr_kind::Type: return ty_level(a) == ty_level(b);

View file

@ -85,9 +85,9 @@ class for_each_fn {
}
goto begin_loop;
}
case expr_kind::Eq:
todo.emplace_back(eq_rhs(e), offset);
todo.emplace_back(eq_lhs(e), offset);
case expr_kind::HEq:
todo.emplace_back(heq_rhs(e), offset);
todo.emplace_back(heq_lhs(e), offset);
goto begin_loop;
case expr_kind::Lambda:
case expr_kind::Pi:

View file

@ -38,7 +38,7 @@ protected:
return true;
case expr_kind::Var:
return var_idx(e) >= offset;
case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
break;
}
@ -76,8 +76,8 @@ protected:
case expr_kind::App:
result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
break;
case expr_kind::Eq:
result = apply(eq_lhs(e), offset) || apply(eq_rhs(e), offset);
case expr_kind::HEq:
result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset);
break;
case expr_kind::Lambda:
case expr_kind::Pi:
@ -166,7 +166,7 @@ class free_var_range_fn {
return 0;
case expr_kind::Var:
return var_idx(e) + 1;
case expr_kind::MetaVar: case expr_kind::App: case expr_kind::Eq:
case expr_kind::MetaVar: case expr_kind::App: case expr_kind::HEq:
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
break;
}
@ -199,8 +199,8 @@ class free_var_range_fn {
for (auto const & c : args(e))
result = std::max(result, apply(c));
break;
case expr_kind::Eq:
result = std::max(apply(eq_lhs(e)), apply(eq_rhs(e)));
case expr_kind::HEq:
result = std::max(apply(heq_lhs(e)), apply(heq_rhs(e)));
break;
case expr_kind::Lambda:
case expr_kind::Pi:
@ -258,7 +258,7 @@ protected:
return true; // assume that any free variable can occur in the metavariable
case expr_kind::Var:
return var_idx(e) >= offset + m_low && var_idx(e) < offset + m_high;
case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let:
break;
}
@ -297,8 +297,8 @@ protected:
case expr_kind::App:
result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
break;
case expr_kind::Eq:
result = apply(eq_lhs(e), offset) || apply(eq_rhs(e), offset);
case expr_kind::HEq:
result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset);
break;
case expr_kind::Lambda:
case expr_kind::Pi:

View file

@ -0,0 +1,96 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/environment.h"
#include "kernel/decl_macros.h"
namespace lean {
MK_CONSTANT(Bool, name("Bool"));
MK_CONSTANT(TypeU, name("TypeU"));
MK_CONSTANT(not_fn, name("not"));
MK_CONSTANT(or_fn, name("or"));
MK_CONSTANT(and_fn, name("and"));
MK_CONSTANT(implies_fn, name("implies"));
MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(eq_fn, name("eq"));
MK_CONSTANT(neq_fn, name("neq"));
MK_CONSTANT(em_fn, name("em"));
MK_CONSTANT(case_fn, name("case"));
MK_CONSTANT(refl_fn, name("refl"));
MK_CONSTANT(subst_fn, name("subst"));
MK_CONSTANT(funext_fn, name("funext"));
MK_CONSTANT(allext_fn, name("allext"));
MK_CONSTANT(substp_fn, name("substp"));
MK_CONSTANT(eta_fn, name("eta"));
MK_CONSTANT(trivial, name("trivial"));
MK_CONSTANT(absurd_fn, name("absurd"));
MK_CONSTANT(eqmp_fn, name("eqmp"));
MK_CONSTANT(boolcomplete_fn, name("boolcomplete"));
MK_CONSTANT(false_elim_fn, name("false_elim"));
MK_CONSTANT(imp_trans_fn, name("imp_trans"));
MK_CONSTANT(imp_eq_trans_fn, name("imp_eq_trans"));
MK_CONSTANT(eq_imp_trans_fn, name("eq_imp_trans"));
MK_CONSTANT(not_not_eq_fn, name("not_not_eq"));
MK_CONSTANT(not_not_elim_fn, name("not_not_elim"));
MK_CONSTANT(mt_fn, name("mt"));
MK_CONSTANT(contrapos_fn, name("contrapos"));
MK_CONSTANT(absurd_elim_fn, name("absurd_elim"));
MK_CONSTANT(not_imp_eliml_fn, name("not_imp_eliml"));
MK_CONSTANT(not_imp_elimr_fn, name("not_imp_elimr"));
MK_CONSTANT(resolve1_fn, name("resolve1"));
MK_CONSTANT(and_intro_fn, name("and_intro"));
MK_CONSTANT(and_eliml_fn, name("and_eliml"));
MK_CONSTANT(and_elimr_fn, name("and_elimr"));
MK_CONSTANT(or_introl_fn, name("or_introl"));
MK_CONSTANT(or_intror_fn, name("or_intror"));
MK_CONSTANT(or_elim_fn, name("or_elim"));
MK_CONSTANT(refute_fn, name("refute"));
MK_CONSTANT(symm_fn, name("symm"));
MK_CONSTANT(trans_fn, name("trans"));
MK_CONSTANT(ne_symm_fn, name("ne_symm"));
MK_CONSTANT(eq_ne_trans_fn, name("eq_ne_trans"));
MK_CONSTANT(ne_eq_trans_fn, name("ne_eq_trans"));
MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
MK_CONSTANT(congr1_fn, name("congr1"));
MK_CONSTANT(congr2_fn, name("congr2"));
MK_CONSTANT(congr_fn, name("congr"));
MK_CONSTANT(exists_elim_fn, name("exists_elim"));
MK_CONSTANT(exists_intro_fn, name("exists_intro"));
MK_CONSTANT(boolext_fn, name("boolext"));
MK_CONSTANT(iff_intro_fn, name("iff_intro"));
MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
MK_CONSTANT(or_comm_fn, name("or_comm"));
MK_CONSTANT(or_assoc_fn, name("or_assoc"));
MK_CONSTANT(or_id_fn, name("or_id"));
MK_CONSTANT(or_falsel_fn, name("or_falsel"));
MK_CONSTANT(or_falser_fn, name("or_falser"));
MK_CONSTANT(or_truel_fn, name("or_truel"));
MK_CONSTANT(or_truer_fn, name("or_truer"));
MK_CONSTANT(or_tauto_fn, name("or_tauto"));
MK_CONSTANT(and_comm_fn, name("and_comm"));
MK_CONSTANT(and_id_fn, name("and_id"));
MK_CONSTANT(and_assoc_fn, name("and_assoc"));
MK_CONSTANT(and_truer_fn, name("and_truer"));
MK_CONSTANT(and_truel_fn, name("and_truel"));
MK_CONSTANT(and_falsel_fn, name("and_falsel"));
MK_CONSTANT(and_falser_fn, name("and_falser"));
MK_CONSTANT(and_absurd_fn, name("and_absurd"));
MK_CONSTANT(not_and_fn, name("not_and"));
MK_CONSTANT(not_and_elim_fn, name("not_and_elim"));
MK_CONSTANT(not_or_fn, name("not_or"));
MK_CONSTANT(not_or_elim_fn, name("not_or_elim"));
MK_CONSTANT(not_iff_fn, name("not_iff"));
MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim"));
MK_CONSTANT(not_implies_fn, name("not_implies"));
MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim"));
MK_CONSTANT(not_congr_fn, name("not_congr"));
MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro"));
MK_CONSTANT(not_forall_fn, name("not_forall"));
MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim"));
MK_CONSTANT(not_exists_fn, name("not_exists"));
MK_CONSTANT(not_exists_elim_fn, name("not_exists_elim"));
MK_CONSTANT(exists_unfold1_fn, name("exists_unfold1"));
MK_CONSTANT(exists_unfold2_fn, name("exists_unfold2"));
MK_CONSTANT(exists_unfold_fn, name("exists_unfold"));
}

273
src/kernel/kernel_decls.h Normal file
View file

@ -0,0 +1,273 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/expr.h"
namespace lean {
expr mk_Bool();
bool is_Bool(expr const & e);
expr mk_TypeU();
bool is_TypeU(expr const & e);
expr mk_not_fn();
bool is_not_fn(expr const & e);
inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
inline expr mk_not(expr const & e1) { return mk_app({mk_not_fn(), e1}); }
expr mk_or_fn();
bool is_or_fn(expr const & e);
inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); }
inline expr mk_or(expr const & e1, expr const & e2) { return mk_app({mk_or_fn(), e1, e2}); }
expr mk_and_fn();
bool is_and_fn(expr const & e);
inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
inline expr mk_and(expr const & e1, expr const & e2) { return mk_app({mk_and_fn(), e1, e2}); }
expr mk_implies_fn();
bool is_implies_fn(expr const & e);
inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app({mk_implies_fn(), e1, e2}); }
expr mk_exists_fn();
bool is_exists_fn(expr const & e);
inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); }
inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); }
expr mk_eq_fn();
bool is_eq_fn(expr const & e);
inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)); }
inline expr mk_eq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eq_fn(), e1, e2, e3}); }
expr mk_neq_fn();
bool is_neq_fn(expr const & e);
inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); }
inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
expr mk_em_fn();
bool is_em_fn(expr const & e);
inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); }
expr mk_case_fn();
bool is_case_fn(expr const & e);
inline expr mk_case_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_case_fn(), e1, e2, e3, e4}); }
expr mk_refl_fn();
bool is_refl_fn(expr const & e);
inline expr mk_refl_th(expr const & e1, expr const & e2) { return mk_app({mk_refl_fn(), e1, e2}); }
expr mk_subst_fn();
bool is_subst_fn(expr const & e);
inline expr mk_subst_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_subst_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_funext_fn();
bool is_funext_fn(expr const & e);
inline expr mk_funext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_funext_fn(), e1, e2, e3, e4, e5}); }
expr mk_allext_fn();
bool is_allext_fn(expr const & e);
inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); }
expr mk_substp_fn();
bool is_substp_fn(expr const & e);
inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_eta_fn();
bool is_eta_fn(expr const & e);
inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); }
expr mk_trivial();
bool is_trivial(expr const & e);
expr mk_absurd_fn();
bool is_absurd_fn(expr const & e);
inline expr mk_absurd_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_absurd_fn(), e1, e2, e3}); }
expr mk_eqmp_fn();
bool is_eqmp_fn(expr const & e);
inline expr mk_eqmp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eqmp_fn(), e1, e2, e3, e4}); }
expr mk_boolcomplete_fn();
bool is_boolcomplete_fn(expr const & e);
inline expr mk_boolcomplete_th(expr const & e1) { return mk_app({mk_boolcomplete_fn(), e1}); }
expr mk_false_elim_fn();
bool is_false_elim_fn(expr const & e);
inline expr mk_false_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_false_elim_fn(), e1, e2}); }
expr mk_imp_trans_fn();
bool is_imp_trans_fn(expr const & e);
inline expr mk_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_imp_eq_trans_fn();
bool is_imp_eq_trans_fn(expr const & e);
inline expr mk_imp_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_eq_imp_trans_fn();
bool is_eq_imp_trans_fn(expr const & e);
inline expr mk_eq_imp_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_imp_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_not_not_eq_fn();
bool is_not_not_eq_fn(expr const & e);
inline expr mk_not_not_eq_th(expr const & e1) { return mk_app({mk_not_not_eq_fn(), e1}); }
expr mk_not_not_elim_fn();
bool is_not_not_elim_fn(expr const & e);
inline expr mk_not_not_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_not_not_elim_fn(), e1, e2}); }
expr mk_mt_fn();
bool is_mt_fn(expr const & e);
inline expr mk_mt_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_mt_fn(), e1, e2, e3, e4}); }
expr mk_contrapos_fn();
bool is_contrapos_fn(expr const & e);
inline expr mk_contrapos_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_contrapos_fn(), e1, e2, e3, e4}); }
expr mk_absurd_elim_fn();
bool is_absurd_elim_fn(expr const & e);
inline expr mk_absurd_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_absurd_elim_fn(), e1, e2, e3, e4}); }
expr mk_not_imp_eliml_fn();
bool is_not_imp_eliml_fn(expr const & e);
inline expr mk_not_imp_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_eliml_fn(), e1, e2, e3}); }
expr mk_not_imp_elimr_fn();
bool is_not_imp_elimr_fn(expr const & e);
inline expr mk_not_imp_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_imp_elimr_fn(), e1, e2, e3}); }
expr mk_resolve1_fn();
bool is_resolve1_fn(expr const & e);
inline expr mk_resolve1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_resolve1_fn(), e1, e2, e3, e4}); }
expr mk_and_intro_fn();
bool is_and_intro_fn(expr const & e);
inline expr mk_and_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_and_intro_fn(), e1, e2, e3, e4}); }
expr mk_and_eliml_fn();
bool is_and_eliml_fn(expr const & e);
inline expr mk_and_eliml_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_eliml_fn(), e1, e2, e3}); }
expr mk_and_elimr_fn();
bool is_and_elimr_fn(expr const & e);
inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_elimr_fn(), e1, e2, e3}); }
expr mk_or_introl_fn();
bool is_or_introl_fn(expr const & e);
inline expr mk_or_introl_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_introl_fn(), e1, e2, e3}); }
expr mk_or_intror_fn();
bool is_or_intror_fn(expr const & e);
inline expr mk_or_intror_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_intror_fn(), e1, e2, e3}); }
expr mk_or_elim_fn();
bool is_or_elim_fn(expr const & e);
inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_refute_fn();
bool is_refute_fn(expr const & e);
inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_refute_fn(), e1, e2}); }
expr mk_symm_fn();
bool is_symm_fn(expr const & e);
inline expr mk_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_symm_fn(), e1, e2, e3, e4}); }
expr mk_trans_fn();
bool is_trans_fn(expr const & e);
inline expr mk_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_ne_symm_fn();
bool is_ne_symm_fn(expr const & e);
inline expr mk_ne_symm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_ne_symm_fn(), e1, e2, e3, e4}); }
expr mk_eq_ne_trans_fn();
bool is_eq_ne_trans_fn(expr const & e);
inline expr mk_eq_ne_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_eq_ne_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_ne_eq_trans_fn();
bool is_ne_eq_trans_fn(expr const & e);
inline expr mk_ne_eq_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_ne_eq_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_eqt_elim_fn();
bool is_eqt_elim_fn(expr const & e);
inline expr mk_eqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_elim_fn(), e1, e2}); }
expr mk_congr1_fn();
bool is_congr1_fn(expr const & e);
inline expr mk_congr1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr1_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_congr2_fn();
bool is_congr2_fn(expr const & e);
inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_congr2_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_congr_fn();
bool is_congr_fn(expr const & e);
inline expr mk_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_congr_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
expr mk_exists_elim_fn();
bool is_exists_elim_fn(expr const & e);
inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_exists_elim_fn(), e1, e2, e3, e4, e5}); }
expr mk_exists_intro_fn();
bool is_exists_intro_fn(expr const & e);
inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); }
expr mk_boolext_fn();
bool is_boolext_fn(expr const & e);
inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); }
expr mk_iff_intro_fn();
bool is_iff_intro_fn(expr const & e);
inline expr mk_iff_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_iff_intro_fn(), e1, e2, e3, e4}); }
expr mk_eqt_intro_fn();
bool is_eqt_intro_fn(expr const & e);
inline expr mk_eqt_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_eqt_intro_fn(), e1, e2}); }
expr mk_or_comm_fn();
bool is_or_comm_fn(expr const & e);
inline expr mk_or_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_or_comm_fn(), e1, e2}); }
expr mk_or_assoc_fn();
bool is_or_assoc_fn(expr const & e);
inline expr mk_or_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_or_assoc_fn(), e1, e2, e3}); }
expr mk_or_id_fn();
bool is_or_id_fn(expr const & e);
inline expr mk_or_id_th(expr const & e1) { return mk_app({mk_or_id_fn(), e1}); }
expr mk_or_falsel_fn();
bool is_or_falsel_fn(expr const & e);
inline expr mk_or_falsel_th(expr const & e1) { return mk_app({mk_or_falsel_fn(), e1}); }
expr mk_or_falser_fn();
bool is_or_falser_fn(expr const & e);
inline expr mk_or_falser_th(expr const & e1) { return mk_app({mk_or_falser_fn(), e1}); }
expr mk_or_truel_fn();
bool is_or_truel_fn(expr const & e);
inline expr mk_or_truel_th(expr const & e1) { return mk_app({mk_or_truel_fn(), e1}); }
expr mk_or_truer_fn();
bool is_or_truer_fn(expr const & e);
inline expr mk_or_truer_th(expr const & e1) { return mk_app({mk_or_truer_fn(), e1}); }
expr mk_or_tauto_fn();
bool is_or_tauto_fn(expr const & e);
inline expr mk_or_tauto_th(expr const & e1) { return mk_app({mk_or_tauto_fn(), e1}); }
expr mk_and_comm_fn();
bool is_and_comm_fn(expr const & e);
inline expr mk_and_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_and_comm_fn(), e1, e2}); }
expr mk_and_id_fn();
bool is_and_id_fn(expr const & e);
inline expr mk_and_id_th(expr const & e1) { return mk_app({mk_and_id_fn(), e1}); }
expr mk_and_assoc_fn();
bool is_and_assoc_fn(expr const & e);
inline expr mk_and_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_and_assoc_fn(), e1, e2, e3}); }
expr mk_and_truer_fn();
bool is_and_truer_fn(expr const & e);
inline expr mk_and_truer_th(expr const & e1) { return mk_app({mk_and_truer_fn(), e1}); }
expr mk_and_truel_fn();
bool is_and_truel_fn(expr const & e);
inline expr mk_and_truel_th(expr const & e1) { return mk_app({mk_and_truel_fn(), e1}); }
expr mk_and_falsel_fn();
bool is_and_falsel_fn(expr const & e);
inline expr mk_and_falsel_th(expr const & e1) { return mk_app({mk_and_falsel_fn(), e1}); }
expr mk_and_falser_fn();
bool is_and_falser_fn(expr const & e);
inline expr mk_and_falser_th(expr const & e1) { return mk_app({mk_and_falser_fn(), e1}); }
expr mk_and_absurd_fn();
bool is_and_absurd_fn(expr const & e);
inline expr mk_and_absurd_th(expr const & e1) { return mk_app({mk_and_absurd_fn(), e1}); }
expr mk_not_and_fn();
bool is_not_and_fn(expr const & e);
inline expr mk_not_and_th(expr const & e1, expr const & e2) { return mk_app({mk_not_and_fn(), e1, e2}); }
expr mk_not_and_elim_fn();
bool is_not_and_elim_fn(expr const & e);
inline expr mk_not_and_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_and_elim_fn(), e1, e2, e3}); }
expr mk_not_or_fn();
bool is_not_or_fn(expr const & e);
inline expr mk_not_or_th(expr const & e1, expr const & e2) { return mk_app({mk_not_or_fn(), e1, e2}); }
expr mk_not_or_elim_fn();
bool is_not_or_elim_fn(expr const & e);
inline expr mk_not_or_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_or_elim_fn(), e1, e2, e3}); }
expr mk_not_iff_fn();
bool is_not_iff_fn(expr const & e);
inline expr mk_not_iff_th(expr const & e1, expr const & e2) { return mk_app({mk_not_iff_fn(), e1, e2}); }
expr mk_not_iff_elim_fn();
bool is_not_iff_elim_fn(expr const & e);
inline expr mk_not_iff_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_iff_elim_fn(), e1, e2, e3}); }
expr mk_not_implies_fn();
bool is_not_implies_fn(expr const & e);
inline expr mk_not_implies_th(expr const & e1, expr const & e2) { return mk_app({mk_not_implies_fn(), e1, e2}); }
expr mk_not_implies_elim_fn();
bool is_not_implies_elim_fn(expr const & e);
inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_implies_elim_fn(), e1, e2, e3}); }
expr mk_not_congr_fn();
bool is_not_congr_fn(expr const & e);
inline expr mk_not_congr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_congr_fn(), e1, e2, e3}); }
expr mk_eq_exists_intro_fn();
bool is_eq_exists_intro_fn(expr const & e);
inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); }
expr mk_not_forall_fn();
bool is_not_forall_fn(expr const & e);
inline expr mk_not_forall_th(expr const & e1, expr const & e2) { return mk_app({mk_not_forall_fn(), e1, e2}); }
expr mk_not_forall_elim_fn();
bool is_not_forall_elim_fn(expr const & e);
inline expr mk_not_forall_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_forall_elim_fn(), e1, e2, e3}); }
expr mk_not_exists_fn();
bool is_not_exists_fn(expr const & e);
inline expr mk_not_exists_th(expr const & e1, expr const & e2) { return mk_app({mk_not_exists_fn(), e1, e2}); }
expr mk_not_exists_elim_fn();
bool is_not_exists_elim_fn(expr const & e);
inline expr mk_not_exists_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_not_exists_elim_fn(), e1, e2, e3, e4}); }
expr mk_exists_unfold1_fn();
bool is_exists_unfold1_fn(expr const & e);
inline expr mk_exists_unfold1_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_unfold1_fn(), e1, e2, e3, e4}); }
expr mk_exists_unfold2_fn();
bool is_exists_unfold2_fn(expr const & e);
inline expr mk_exists_unfold2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_unfold2_fn(), e1, e2, e3, e4}); }
expr mk_exists_unfold_fn();
bool is_exists_unfold_fn(expr const & e);
inline expr mk_exists_unfold_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_unfold_fn(), e1, e2, e3}); }
}

View file

@ -56,8 +56,8 @@ struct max_sharing_fn::imp {
cache(r);
return r;
}
case expr_kind::Eq : {
expr r = update_eq(a, [=](expr const & l, expr const & r) { return std::make_pair(apply(l), apply(r)); });
case expr_kind::HEq : {
expr r = update_heq(a, [=](expr const & l, expr const & r) { return std::make_pair(apply(l), apply(r)); });
cache(r);
return r;
}

View file

@ -309,13 +309,13 @@ class normalizer::imp {
}
break;
}
case expr_kind::Eq: {
expr new_lhs = normalize(eq_lhs(a), s, k);
expr new_rhs = normalize(eq_rhs(a), s, k);
case expr_kind::HEq: {
expr new_lhs = normalize(heq_lhs(a), s, k);
expr new_rhs = normalize(heq_rhs(a), s, k);
if (is_value(new_lhs) && is_value(new_rhs) && !is_closure(new_lhs) && !is_closure(new_rhs) && typeid(to_value(new_lhs)) == typeid(to_value(new_rhs))) {
r = mk_bool_value(new_lhs == new_rhs);
} else {
r = mk_eq(new_lhs, new_rhs);
r = mk_heq(new_lhs, new_rhs);
}
break;
}

View file

@ -156,12 +156,12 @@ public:
pop_rs(num);
break;
}
case expr_kind::Eq:
if (check_index(f, 0) && !visit(eq_lhs(e), offset))
case expr_kind::HEq:
if (check_index(f, 0) && !visit(heq_lhs(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(eq_rhs(e), offset))
if (check_index(f, 1) && !visit(heq_rhs(e), offset))
goto begin_loop;
r = update_eq(e, rs(-2), rs(-1));
r = update_heq(e, rs(-2), rs(-1));
pop_rs(2);
break;
case expr_kind::Pi: case expr_kind::Lambda:

View file

@ -22,9 +22,9 @@ expr replace_visitor::visit_app(expr const & e, context const & ctx) {
lean_assert(is_app(e));
return update_app(e, [&](expr const & c) { return visit(c, ctx); });
}
expr replace_visitor::visit_eq(expr const & e, context const & ctx) {
lean_assert(is_eq(e));
return update_eq(e, [&](expr const & l, expr const & r) { return std::make_pair(visit(l, ctx), visit(r, ctx)); });
expr replace_visitor::visit_heq(expr const & e, context const & ctx) {
lean_assert(is_heq(e));
return update_heq(e, [&](expr const & l, expr const & r) { return std::make_pair(visit(l, ctx), visit(r, ctx)); });
}
expr replace_visitor::visit_abst(expr const & e, context const & ctx) {
lean_assert(is_abstraction(e));
@ -80,7 +80,7 @@ expr replace_visitor::visit(expr const & e, context const & ctx) {
case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared);
case expr_kind::MetaVar: return save_result(e, visit_metavar(e, ctx), shared);
case expr_kind::App: return save_result(e, visit_app(e, ctx), shared);
case expr_kind::Eq: return save_result(e, visit_eq(e, ctx), shared);
case expr_kind::HEq: return save_result(e, visit_heq(e, ctx), shared);
case expr_kind::Lambda: return save_result(e, visit_lambda(e, ctx), shared);
case expr_kind::Pi: return save_result(e, visit_pi(e, ctx), shared);
case expr_kind::Let: return save_result(e, visit_let(e, ctx), shared);

View file

@ -31,7 +31,7 @@ protected:
virtual expr visit_var(expr const &, context const &);
virtual expr visit_metavar(expr const &, context const &);
virtual expr visit_app(expr const &, context const &);
virtual expr visit_eq(expr const &, context const &);
virtual expr visit_heq(expr const &, context const &);
virtual expr visit_abst(expr const &, context const &);
virtual expr visit_lambda(expr const &, context const &);
virtual expr visit_pi(expr const &, context const &);

View file

@ -176,7 +176,7 @@ class type_checker::imp {
}
case expr_kind::Type:
return mk_type(ty_level(e) + 1);
case expr_kind::Eq:
case expr_kind::HEq:
// cheap when we are just inferring types
if (m_infer_only)
return mk_bool_type();
@ -241,10 +241,10 @@ class type_checker::imp {
f_t = check_pi(f_t, e, ctx);
}
}
case expr_kind::Eq:
case expr_kind::HEq:
lean_assert(!m_infer_only);
infer_type_core(eq_lhs(e), ctx);
infer_type_core(eq_rhs(e), ctx);
infer_type_core(heq_lhs(e), ctx);
infer_type_core(heq_rhs(e), ctx);
return save_result(e, mk_bool_type(), shared);
case expr_kind::Lambda:
if (!m_infer_only) {
@ -422,7 +422,7 @@ public:
// Catch easy cases
switch (e.kind()) {
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Type: return false;
case expr_kind::Eq: return true;
case expr_kind::HEq: return true;
default: break;
}
expr t = infer_type(e, ctx, menv, nullptr);

View file

@ -67,10 +67,10 @@ expr update_let(expr const & let, optional<expr> const & t, expr const & v, expr
return mk_let(let_name(let), t, v, b);
}
expr update_eq(expr const & eq, expr const & l, expr const & r) {
if (is_eqp(eq_lhs(eq), l) && is_eqp(eq_rhs(eq), r))
expr update_heq(expr const & eq, expr const & l, expr const & r) {
if (is_eqp(heq_lhs(eq), l) && is_eqp(heq_rhs(eq), r))
return eq;
else
return mk_eq(l, r);
return mk_heq(l, r);
}
}

View file

@ -43,5 +43,5 @@ expr update_let(expr const & let, optional<expr> const & t, expr const & v, expr
\remark Return \c eq if the given lhs and rhs are (pointer) equal to the ones in \c eq.
*/
expr update_eq(expr const & eq, expr const & l, expr const & r);
expr update_heq(expr const & eq, expr const & l, expr const & r);
}

View file

@ -0,0 +1,20 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/environment.h"
#include "kernel/decl_macros.h"
namespace lean {
MK_CONSTANT(Int, name("Int"));
MK_CONSTANT(Int_ge_fn, name({"Int", "ge"}));
MK_CONSTANT(Int_lt_fn, name({"Int", "lt"}));
MK_CONSTANT(Int_gt_fn, name({"Int", "gt"}));
MK_CONSTANT(Int_sub_fn, name({"Int", "sub"}));
MK_CONSTANT(Int_neg_fn, name({"Int", "neg"}));
MK_CONSTANT(Int_mod_fn, name({"Int", "mod"}));
MK_CONSTANT(Int_divides_fn, name({"Int", "divides"}));
MK_CONSTANT(Int_abs_fn, name({"Int", "abs"}));
MK_CONSTANT(Nat_sub_fn, name({"Nat", "sub"}));
MK_CONSTANT(Nat_neg_fn, name({"Nat", "neg"}));
}

View file

@ -0,0 +1,50 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/expr.h"
namespace lean {
expr mk_Int();
bool is_Int(expr const & e);
expr mk_Int_ge_fn();
bool is_Int_ge_fn(expr const & e);
inline bool is_Int_ge(expr const & e) { return is_app(e) && is_Int_ge_fn(arg(e, 0)); }
inline expr mk_Int_ge(expr const & e1, expr const & e2) { return mk_app({mk_Int_ge_fn(), e1, e2}); }
expr mk_Int_lt_fn();
bool is_Int_lt_fn(expr const & e);
inline bool is_Int_lt(expr const & e) { return is_app(e) && is_Int_lt_fn(arg(e, 0)); }
inline expr mk_Int_lt(expr const & e1, expr const & e2) { return mk_app({mk_Int_lt_fn(), e1, e2}); }
expr mk_Int_gt_fn();
bool is_Int_gt_fn(expr const & e);
inline bool is_Int_gt(expr const & e) { return is_app(e) && is_Int_gt_fn(arg(e, 0)); }
inline expr mk_Int_gt(expr const & e1, expr const & e2) { return mk_app({mk_Int_gt_fn(), e1, e2}); }
expr mk_Int_sub_fn();
bool is_Int_sub_fn(expr const & e);
inline bool is_Int_sub(expr const & e) { return is_app(e) && is_Int_sub_fn(arg(e, 0)); }
inline expr mk_Int_sub(expr const & e1, expr const & e2) { return mk_app({mk_Int_sub_fn(), e1, e2}); }
expr mk_Int_neg_fn();
bool is_Int_neg_fn(expr const & e);
inline bool is_Int_neg(expr const & e) { return is_app(e) && is_Int_neg_fn(arg(e, 0)); }
inline expr mk_Int_neg(expr const & e1) { return mk_app({mk_Int_neg_fn(), e1}); }
expr mk_Int_mod_fn();
bool is_Int_mod_fn(expr const & e);
inline bool is_Int_mod(expr const & e) { return is_app(e) && is_Int_mod_fn(arg(e, 0)); }
inline expr mk_Int_mod(expr const & e1, expr const & e2) { return mk_app({mk_Int_mod_fn(), e1, e2}); }
expr mk_Int_divides_fn();
bool is_Int_divides_fn(expr const & e);
inline bool is_Int_divides(expr const & e) { return is_app(e) && is_Int_divides_fn(arg(e, 0)); }
inline expr mk_Int_divides(expr const & e1, expr const & e2) { return mk_app({mk_Int_divides_fn(), e1, e2}); }
expr mk_Int_abs_fn();
bool is_Int_abs_fn(expr const & e);
inline bool is_Int_abs(expr const & e) { return is_app(e) && is_Int_abs_fn(arg(e, 0)); }
inline expr mk_Int_abs(expr const & e1) { return mk_app({mk_Int_abs_fn(), e1}); }
expr mk_Nat_sub_fn();
bool is_Nat_sub_fn(expr const & e);
inline bool is_Nat_sub(expr const & e) { return is_app(e) && is_Nat_sub_fn(arg(e, 0)); }
inline expr mk_Nat_sub(expr const & e1, expr const & e2) { return mk_app({mk_Nat_sub_fn(), e1, e2}); }
expr mk_Nat_neg_fn();
bool is_Nat_neg_fn(expr const & e);
inline bool is_Nat_neg(expr const & e) { return is_app(e) && is_Nat_neg_fn(arg(e, 0)); }
inline expr mk_Nat_neg(expr const & e1) { return mk_app({mk_Nat_neg_fn(), e1}); }
}

View file

@ -0,0 +1,45 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/environment.h"
#include "kernel/decl_macros.h"
namespace lean {
MK_CONSTANT(Nat, name("Nat"));
MK_CONSTANT(Nat_ge_fn, name({"Nat", "ge"}));
MK_CONSTANT(Nat_lt_fn, name({"Nat", "lt"}));
MK_CONSTANT(Nat_gt_fn, name({"Nat", "gt"}));
MK_CONSTANT(Nat_id_fn, name({"Nat", "id"}));
MK_CONSTANT(Nat_succ_nz_fn, name({"Nat", "succ_nz"}));
MK_CONSTANT(Nat_succ_inj_fn, name({"Nat", "succ_inj"}));
MK_CONSTANT(Nat_add_zeror_fn, name({"Nat", "add_zeror"}));
MK_CONSTANT(Nat_add_succr_fn, name({"Nat", "add_succr"}));
MK_CONSTANT(Nat_mul_zeror_fn, name({"Nat", "mul_zeror"}));
MK_CONSTANT(Nat_mul_succr_fn, name({"Nat", "mul_succr"}));
MK_CONSTANT(Nat_le_def_fn, name({"Nat", "le_def"}));
MK_CONSTANT(Nat_induction_fn, name({"Nat", "induction"}));
MK_CONSTANT(Nat_pred_nz_fn, name({"Nat", "pred_nz"}));
MK_CONSTANT(Nat_discriminate_fn, name({"Nat", "discriminate"}));
MK_CONSTANT(Nat_add_zerol_fn, name({"Nat", "add_zerol"}));
MK_CONSTANT(Nat_add_succl_fn, name({"Nat", "add_succl"}));
MK_CONSTANT(Nat_add_comm_fn, name({"Nat", "add_comm"}));
MK_CONSTANT(Nat_add_assoc_fn, name({"Nat", "add_assoc"}));
MK_CONSTANT(Nat_mul_zerol_fn, name({"Nat", "mul_zerol"}));
MK_CONSTANT(Nat_mul_succl_fn, name({"Nat", "mul_succl"}));
MK_CONSTANT(Nat_mul_onel_fn, name({"Nat", "mul_onel"}));
MK_CONSTANT(Nat_mul_oner_fn, name({"Nat", "mul_oner"}));
MK_CONSTANT(Nat_mul_comm_fn, name({"Nat", "mul_comm"}));
MK_CONSTANT(Nat_distributer_fn, name({"Nat", "distributer"}));
MK_CONSTANT(Nat_distributel_fn, name({"Nat", "distributel"}));
MK_CONSTANT(Nat_mul_assoc_fn, name({"Nat", "mul_assoc"}));
MK_CONSTANT(Nat_add_inj_fn, name({"Nat", "add_inj"}));
MK_CONSTANT(Nat_add_eqz_fn, name({"Nat", "add_eqz"}));
MK_CONSTANT(Nat_le_intro_fn, name({"Nat", "le_intro"}));
MK_CONSTANT(Nat_le_elim_fn, name({"Nat", "le_elim"}));
MK_CONSTANT(Nat_le_refl_fn, name({"Nat", "le_refl"}));
MK_CONSTANT(Nat_le_zero_fn, name({"Nat", "le_zero"}));
MK_CONSTANT(Nat_le_trans_fn, name({"Nat", "le_trans"}));
MK_CONSTANT(Nat_le_add_fn, name({"Nat", "le_add"}));
MK_CONSTANT(Nat_le_antisym_fn, name({"Nat", "le_antisym"}));
}

View file

@ -0,0 +1,119 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/expr.h"
namespace lean {
expr mk_Nat();
bool is_Nat(expr const & e);
expr mk_Nat_ge_fn();
bool is_Nat_ge_fn(expr const & e);
inline bool is_Nat_ge(expr const & e) { return is_app(e) && is_Nat_ge_fn(arg(e, 0)); }
inline expr mk_Nat_ge(expr const & e1, expr const & e2) { return mk_app({mk_Nat_ge_fn(), e1, e2}); }
expr mk_Nat_lt_fn();
bool is_Nat_lt_fn(expr const & e);
inline bool is_Nat_lt(expr const & e) { return is_app(e) && is_Nat_lt_fn(arg(e, 0)); }
inline expr mk_Nat_lt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_lt_fn(), e1, e2}); }
expr mk_Nat_gt_fn();
bool is_Nat_gt_fn(expr const & e);
inline bool is_Nat_gt(expr const & e) { return is_app(e) && is_Nat_gt_fn(arg(e, 0)); }
inline expr mk_Nat_gt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_gt_fn(), e1, e2}); }
expr mk_Nat_id_fn();
bool is_Nat_id_fn(expr const & e);
inline bool is_Nat_id(expr const & e) { return is_app(e) && is_Nat_id_fn(arg(e, 0)); }
inline expr mk_Nat_id(expr const & e1) { return mk_app({mk_Nat_id_fn(), e1}); }
expr mk_Nat_succ_nz_fn();
bool is_Nat_succ_nz_fn(expr const & e);
inline expr mk_Nat_succ_nz_th(expr const & e1) { return mk_app({mk_Nat_succ_nz_fn(), e1}); }
expr mk_Nat_succ_inj_fn();
bool is_Nat_succ_inj_fn(expr const & e);
inline expr mk_Nat_succ_inj_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_succ_inj_fn(), e1, e2, e3}); }
expr mk_Nat_add_zeror_fn();
bool is_Nat_add_zeror_fn(expr const & e);
inline expr mk_Nat_add_zeror_th(expr const & e1) { return mk_app({mk_Nat_add_zeror_fn(), e1}); }
expr mk_Nat_add_succr_fn();
bool is_Nat_add_succr_fn(expr const & e);
inline expr mk_Nat_add_succr_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_succr_fn(), e1, e2}); }
expr mk_Nat_mul_zeror_fn();
bool is_Nat_mul_zeror_fn(expr const & e);
inline expr mk_Nat_mul_zeror_th(expr const & e1) { return mk_app({mk_Nat_mul_zeror_fn(), e1}); }
expr mk_Nat_mul_succr_fn();
bool is_Nat_mul_succr_fn(expr const & e);
inline expr mk_Nat_mul_succr_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_succr_fn(), e1, e2}); }
expr mk_Nat_le_def_fn();
bool is_Nat_le_def_fn(expr const & e);
inline expr mk_Nat_le_def_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_le_def_fn(), e1, e2}); }
expr mk_Nat_induction_fn();
bool is_Nat_induction_fn(expr const & e);
inline expr mk_Nat_induction_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_fn(), e1, e2, e3, e4}); }
expr mk_Nat_pred_nz_fn();
bool is_Nat_pred_nz_fn(expr const & e);
inline expr mk_Nat_pred_nz_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_pred_nz_fn(), e1, e2}); }
expr mk_Nat_discriminate_fn();
bool is_Nat_discriminate_fn(expr const & e);
inline expr mk_Nat_discriminate_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_discriminate_fn(), e1, e2, e3, e4}); }
expr mk_Nat_add_zerol_fn();
bool is_Nat_add_zerol_fn(expr const & e);
inline expr mk_Nat_add_zerol_th(expr const & e1) { return mk_app({mk_Nat_add_zerol_fn(), e1}); }
expr mk_Nat_add_succl_fn();
bool is_Nat_add_succl_fn(expr const & e);
inline expr mk_Nat_add_succl_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_succl_fn(), e1, e2}); }
expr mk_Nat_add_comm_fn();
bool is_Nat_add_comm_fn(expr const & e);
inline expr mk_Nat_add_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_add_comm_fn(), e1, e2}); }
expr mk_Nat_add_assoc_fn();
bool is_Nat_add_assoc_fn(expr const & e);
inline expr mk_Nat_add_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_assoc_fn(), e1, e2, e3}); }
expr mk_Nat_mul_zerol_fn();
bool is_Nat_mul_zerol_fn(expr const & e);
inline expr mk_Nat_mul_zerol_th(expr const & e1) { return mk_app({mk_Nat_mul_zerol_fn(), e1}); }
expr mk_Nat_mul_succl_fn();
bool is_Nat_mul_succl_fn(expr const & e);
inline expr mk_Nat_mul_succl_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_succl_fn(), e1, e2}); }
expr mk_Nat_mul_onel_fn();
bool is_Nat_mul_onel_fn(expr const & e);
inline expr mk_Nat_mul_onel_th(expr const & e1) { return mk_app({mk_Nat_mul_onel_fn(), e1}); }
expr mk_Nat_mul_oner_fn();
bool is_Nat_mul_oner_fn(expr const & e);
inline expr mk_Nat_mul_oner_th(expr const & e1) { return mk_app({mk_Nat_mul_oner_fn(), e1}); }
expr mk_Nat_mul_comm_fn();
bool is_Nat_mul_comm_fn(expr const & e);
inline expr mk_Nat_mul_comm_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_mul_comm_fn(), e1, e2}); }
expr mk_Nat_distributer_fn();
bool is_Nat_distributer_fn(expr const & e);
inline expr mk_Nat_distributer_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_distributer_fn(), e1, e2, e3}); }
expr mk_Nat_distributel_fn();
bool is_Nat_distributel_fn(expr const & e);
inline expr mk_Nat_distributel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_distributel_fn(), e1, e2, e3}); }
expr mk_Nat_mul_assoc_fn();
bool is_Nat_mul_assoc_fn(expr const & e);
inline expr mk_Nat_mul_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_assoc_fn(), e1, e2, e3}); }
expr mk_Nat_add_inj_fn();
bool is_Nat_add_inj_fn(expr const & e);
inline expr mk_Nat_add_inj_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_inj_fn(), e1, e2, e3, e4}); }
expr mk_Nat_add_eqz_fn();
bool is_Nat_add_eqz_fn(expr const & e);
inline expr mk_Nat_add_eqz_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_eqz_fn(), e1, e2, e3}); }
expr mk_Nat_le_intro_fn();
bool is_Nat_le_intro_fn(expr const & e);
inline expr mk_Nat_le_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_intro_fn(), e1, e2, e3, e4}); }
expr mk_Nat_le_elim_fn();
bool is_Nat_le_elim_fn(expr const & e);
inline expr mk_Nat_le_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_le_elim_fn(), e1, e2, e3}); }
expr mk_Nat_le_refl_fn();
bool is_Nat_le_refl_fn(expr const & e);
inline expr mk_Nat_le_refl_th(expr const & e1) { return mk_app({mk_Nat_le_refl_fn(), e1}); }
expr mk_Nat_le_zero_fn();
bool is_Nat_le_zero_fn(expr const & e);
inline expr mk_Nat_le_zero_th(expr const & e1) { return mk_app({mk_Nat_le_zero_fn(), e1}); }
expr mk_Nat_le_trans_fn();
bool is_Nat_le_trans_fn(expr const & e);
inline expr mk_Nat_le_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_le_trans_fn(), e1, e2, e3, e4, e5}); }
expr mk_Nat_le_add_fn();
bool is_Nat_le_add_fn(expr const & e);
inline expr mk_Nat_le_add_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_add_fn(), e1, e2, e3, e4}); }
expr mk_Nat_le_antisym_fn();
bool is_Nat_le_antisym_fn(expr const & e);
inline expr mk_Nat_le_antisym_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_antisym_fn(), e1, e2, e3, e4}); }
}

View file

@ -0,0 +1,17 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/environment.h"
#include "kernel/decl_macros.h"
namespace lean {
MK_CONSTANT(Real, name("Real"));
MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
MK_CONSTANT(Real_ge_fn, name({"Real", "ge"}));
MK_CONSTANT(Real_lt_fn, name({"Real", "lt"}));
MK_CONSTANT(Real_gt_fn, name({"Real", "gt"}));
MK_CONSTANT(Real_sub_fn, name({"Real", "sub"}));
MK_CONSTANT(Real_neg_fn, name({"Real", "neg"}));
MK_CONSTANT(Real_abs_fn, name({"Real", "abs"}));
}

View file

@ -0,0 +1,38 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
*/
// Automatically generated file, DO NOT EDIT
#include "kernel/expr.h"
namespace lean {
expr mk_Real();
bool is_Real(expr const & e);
expr mk_nat_to_real_fn();
bool is_nat_to_real_fn(expr const & e);
inline bool is_nat_to_real(expr const & e) { return is_app(e) && is_nat_to_real_fn(arg(e, 0)); }
inline expr mk_nat_to_real(expr const & e1) { return mk_app({mk_nat_to_real_fn(), e1}); }
expr mk_Real_ge_fn();
bool is_Real_ge_fn(expr const & e);
inline bool is_Real_ge(expr const & e) { return is_app(e) && is_Real_ge_fn(arg(e, 0)); }
inline expr mk_Real_ge(expr const & e1, expr const & e2) { return mk_app({mk_Real_ge_fn(), e1, e2}); }
expr mk_Real_lt_fn();
bool is_Real_lt_fn(expr const & e);
inline bool is_Real_lt(expr const & e) { return is_app(e) && is_Real_lt_fn(arg(e, 0)); }
inline expr mk_Real_lt(expr const & e1, expr const & e2) { return mk_app({mk_Real_lt_fn(), e1, e2}); }
expr mk_Real_gt_fn();
bool is_Real_gt_fn(expr const & e);
inline bool is_Real_gt(expr const & e) { return is_app(e) && is_Real_gt_fn(arg(e, 0)); }
inline expr mk_Real_gt(expr const & e1, expr const & e2) { return mk_app({mk_Real_gt_fn(), e1, e2}); }
expr mk_Real_sub_fn();
bool is_Real_sub_fn(expr const & e);
inline bool is_Real_sub(expr const & e) { return is_app(e) && is_Real_sub_fn(arg(e, 0)); }
inline expr mk_Real_sub(expr const & e1, expr const & e2) { return mk_app({mk_Real_sub_fn(), e1, e2}); }
expr mk_Real_neg_fn();
bool is_Real_neg_fn(expr const & e);
inline bool is_Real_neg(expr const & e) { return is_app(e) && is_Real_neg_fn(arg(e, 0)); }
inline expr mk_Real_neg(expr const & e1) { return mk_app({mk_Real_neg_fn(), e1}); }
expr mk_Real_abs_fn();
bool is_Real_abs_fn(expr const & e);
inline bool is_Real_abs(expr const & e) { return is_app(e) && is_Real_abs_fn(arg(e, 0)); }
inline expr mk_Real_abs(expr const & e1) { return mk_app({mk_Real_abs_fn(), e1}); }
}

View file

@ -13,9 +13,11 @@ Author: Leonardo de Moura
#include "library/kernel_bindings.h"
#include "library/arith/int.h"
#include "library/arith/nat.h"
#include "library/arith/Int_decls.cpp"
namespace lean {
MK_CONSTANT(Int, "Int");
expr mk_nat_to_int_fn();
expr const Int = mk_Int();
expr mk_int_type() { return mk_Int(); }
@ -84,16 +86,16 @@ public:
constexpr char int_add_name[] = "add";
struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
typedef int_bin_op<int_add_name, int_add_eval> int_add_value;
MK_BUILTIN(int_add_fn, int_add_value);
static value::register_deserializer_fn int_add_ds("int_add", [](deserializer & ) { return mk_int_add_fn(); });
static register_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_int_add_fn(); });
MK_BUILTIN(Int_add_fn, int_add_value);
static value::register_deserializer_fn int_add_ds("int_add", [](deserializer & ) { return mk_Int_add_fn(); });
static register_builtin_fn g_int_add_value(name({"Int", "add"}), []() { return mk_Int_add_fn(); });
constexpr char int_mul_name[] = "mul";
struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
MK_BUILTIN(int_mul_fn, int_mul_value);
static value::register_deserializer_fn int_mul_ds("int_mul", [](deserializer & ) { return mk_int_mul_fn(); });
static register_builtin_fn int_mul_blt(name({"Int", "mul"}), []() { return mk_int_mul_fn(); });
MK_BUILTIN(Int_mul_fn, int_mul_value);
static value::register_deserializer_fn int_mul_ds("int_mul", [](deserializer & ) { return mk_Int_mul_fn(); });
static register_builtin_fn int_mul_blt(name({"Int", "mul"}), []() { return mk_Int_mul_fn(); });
constexpr char int_div_name[] = "div";
struct int_div_eval {
@ -105,9 +107,9 @@ struct int_div_eval {
};
};
typedef int_bin_op<int_div_name, int_div_eval> int_div_value;
MK_BUILTIN(int_div_fn, int_div_value);
static value::register_deserializer_fn int_div_ds("int_div", [](deserializer & ) { return mk_int_div_fn(); });
static register_builtin_fn int_div_blt(name({"Int", "div"}), []() { return mk_int_div_fn(); });
MK_BUILTIN(Int_div_fn, int_div_value);
static value::register_deserializer_fn int_div_ds("int_div", [](deserializer & ) { return mk_Int_div_fn(); });
static register_builtin_fn int_div_blt(name({"Int", "div"}), []() { return mk_Int_div_fn(); });
class int_le_value : public const_value {
public:
@ -121,18 +123,9 @@ public:
}
virtual void write(serializer & s) const { s << "int_le"; }
};
MK_BUILTIN(int_le_fn, int_le_value);
static value::register_deserializer_fn int_le_ds("int_le", [](deserializer & ) { return mk_int_le_fn(); });
static register_builtin_fn int_le_blt(name({"Int", "le"}), []() { return mk_int_le_fn(); });
MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
MK_CONSTANT(int_neg_fn, name({"Int", "neg"}));
MK_CONSTANT(int_mod_fn, name({"Int", "mod"}));
MK_CONSTANT(int_divides_fn, name({"Int", "divides"}));
MK_CONSTANT(int_abs_fn, name({"Int", "abs"}));
MK_CONSTANT(int_ge_fn, name({"Int", "ge"}));
MK_CONSTANT(int_lt_fn, name({"Int", "lt"}));
MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
MK_BUILTIN(Int_le_fn, int_le_value);
static value::register_deserializer_fn int_le_ds("int_le", [](deserializer & ) { return mk_Int_le_fn(); });
static register_builtin_fn int_le_blt(name({"Int", "le"}), []() { return mk_Int_le_fn(); });
/**
\brief Semantic attachment for the Nat to Int coercion.
@ -153,9 +146,6 @@ MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
static value::register_deserializer_fn nat_to_int_ds("nat_to_int", [](deserializer & ) { return mk_nat_to_int_fn(); });
static register_builtin_fn nat_to_int_blt("nat_to_int", []() { return mk_nat_to_int_fn(); });
MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
void import_int(environment const & env, io_state const & ios) {
env->import("Int", ios);
}

View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "util/numerics/mpz.h"
#include "kernel/expr.h"
#include "kernel/builtin.h"
#include "library/arith/Int_decls.h"
namespace lean {
/** \brief Integer numbers type */
@ -22,68 +23,16 @@ inline expr iVal(int v) { return mk_int_value(v); }
bool is_int_value(expr const & e);
mpz const & int_value_numeral(expr const & e);
/** \brief Addition, Int::add : Int -> Int -> Int */
expr mk_int_add_fn();
inline expr iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn(), e1, e2); }
/** \brief Subtraction, Int::sub : Int -> Int -> Int */
expr mk_int_sub_fn();
inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); }
/** \brief Unary minus, Int::neg : Int -> Int */
expr mk_int_neg_fn();
inline expr iNeg(expr const & e) { return mk_app(mk_int_neg_fn(), e); }
/** \brief Multiplication, Int::mul : Int -> Int -> Int */
expr mk_int_mul_fn();
inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); }
/** \brief Integer division, Int::mul : Int -> Int -> Int */
expr mk_int_div_fn();
inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); }
/** \brief Modulus, Int::mul : Int -> Int -> Int */
expr mk_int_mod_fn();
inline expr iMod(expr const & e1, expr const & e2) { return mk_app(mk_int_mod_fn(), e1, e2); }
/** \brief Divides predicate, Int::mul : Int -> Int -> Bool */
expr mk_int_divides_fn();
inline expr iDivides(expr const & e1, expr const & e2) { return mk_app(mk_int_divides_fn(), e1, e2); }
/** \brief Absolute value function, Int::abs : Int -> Int */
expr mk_int_abs_fn();
inline expr iAbs(expr const & e) { return mk_app(mk_int_abs_fn(), e); }
/** \brief Less than or equal to, Int::le : Int -> Int -> Bool */
expr mk_int_le_fn();
inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); }
/** \brief Greater than or equal to, Int::ge : Int -> Int -> Bool */
expr mk_int_ge_fn();
inline expr iGe(expr const & e1, expr const & e2) { return mk_app(mk_int_ge_fn(), e1, e2); }
/** \brief Less than, Int::lt : Int -> Int -> Bool */
expr mk_int_lt_fn();
inline expr iLt(expr const & e1, expr const & e2) { return mk_app(mk_int_lt_fn(), e1, e2); }
/** \brief Greater than, Int::gt : Int -> Int -> Bool */
expr mk_int_gt_fn();
inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); }
/** \brief If-then-else for integers */
inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); }
/** \brief Coercion from natural to integer */
expr mk_Int_add_fn();
inline expr mk_Int_add(expr const & e1, expr const & e2) { return mk_app(mk_Int_add_fn(), e1, e2); }
expr mk_Int_mul_fn();
inline expr mk_Int_mul(expr const & e1, expr const & e2) { return mk_app(mk_Int_mul_fn(), e1, e2); }
expr mk_Int_div_fn();
inline expr mk_Int_div(expr const & e1, expr const & e2) { return mk_app(mk_Int_div_fn(), e1, e2); }
expr mk_Int_le_fn();
inline expr mk_Int_le(expr const & e1, expr const & e2) { return mk_app(mk_Int_le_fn(), e1, e2); }
expr mk_nat_to_int_fn();
inline expr n2i(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
/** \brief Subtraction (for naturals), Nat::sub : Nat -> Nat -> Int */
expr mk_nat_sub_fn();
inline expr nSub(expr const & e1, expr const & e2) { return mk_app(mk_nat_sub_fn(), e1, e2); }
/** \brief Unary minus (for naturals), Nat::neg : Nat -> Int */
expr mk_nat_neg_fn();
inline expr nNeg(expr const & e1, expr const & e2) { return mk_app(mk_nat_neg_fn(), e1, e2); }
inline expr mk_nat_to_int(expr const & e) { return mk_app(mk_nat_to_int_fn(), e); }
class environment;
/**

View file

@ -12,9 +12,9 @@ Author: Leonardo de Moura
#include "kernel/decl_macros.h"
#include "library/kernel_bindings.h"
#include "library/arith/nat.h"
#include "library/arith/Nat_decls.cpp"
namespace lean {
MK_CONSTANT(Nat, "Nat");
expr const Nat = mk_Nat();
expr mk_nat_type() { return mk_Nat(); }
@ -78,17 +78,17 @@ constexpr char nat_add_name[] = "add";
/** \brief Evaluator for + : Nat -> Nat -> Nat */
struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
typedef nat_bin_op<nat_add_name, nat_add_eval> nat_add_value;
MK_BUILTIN(nat_add_fn, nat_add_value);
static value::register_deserializer_fn nat_add_ds("nat_add", [](deserializer & ) { return mk_nat_add_fn(); });
static register_builtin_fn nat_add_blt(name({"Nat", "add"}), []() { return mk_nat_add_fn(); });
MK_BUILTIN(Nat_add_fn, nat_add_value);
static value::register_deserializer_fn nat_add_ds("nat_add", [](deserializer & ) { return mk_Nat_add_fn(); });
static register_builtin_fn nat_add_blt(name({"Nat", "add"}), []() { return mk_Nat_add_fn(); });
constexpr char nat_mul_name[] = "mul";
/** \brief Evaluator for * : Nat -> Nat -> Nat */
struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
typedef nat_bin_op<nat_mul_name, nat_mul_eval> nat_mul_value;
MK_BUILTIN(nat_mul_fn, nat_mul_value);
static value::register_deserializer_fn nat_mul_ds("nat_mul", [](deserializer & ) { return mk_nat_mul_fn(); });
static register_builtin_fn nat_mul_blt(name({"Nat", "mul"}), []() { return mk_nat_mul_fn(); });
MK_BUILTIN(Nat_mul_fn, nat_mul_value);
static value::register_deserializer_fn nat_mul_ds("nat_mul", [](deserializer & ) { return mk_Nat_mul_fn(); });
static register_builtin_fn nat_mul_blt(name({"Nat", "mul"}), []() { return mk_Nat_mul_fn(); });
/**
\brief Semantic attachment for less than or equal to operator with type
@ -106,14 +106,9 @@ public:
}
virtual void write(serializer & s) const { s << "nat_le"; }
};
MK_BUILTIN(nat_le_fn, nat_le_value);
static value::register_deserializer_fn nat_le_ds("nat_le", [](deserializer & ) { return mk_nat_le_fn(); });
static register_builtin_fn nat_le_blt(name({"Nat", "le"}), []() { return mk_nat_le_fn(); });
MK_CONSTANT(nat_ge_fn, name({"Nat", "ge"}));
MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"}));
MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"}));
MK_CONSTANT(nat_id_fn, name({"Nat", "id"}));
MK_BUILTIN(Nat_le_fn, nat_le_value);
static value::register_deserializer_fn nat_le_ds("nat_le", [](deserializer & ) { return mk_Nat_le_fn(); });
static register_builtin_fn nat_le_blt(name({"Nat", "le"}), []() { return mk_Nat_le_fn(); });
void import_nat(environment const & env, io_state const & ios) {
env->import("Nat", ios);

View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
#include "kernel/builtin.h"
#include "util/numerics/mpz.h"
#include "library/arith/Nat_decls.h"
namespace lean {
/** \brief Natural numbers type */
@ -22,36 +23,12 @@ inline expr nVal(unsigned v) { return mk_nat_value(v); }
bool is_nat_value(expr const & e);
mpz const & nat_value_numeral(expr const & e);
/** \brief Addition, Nat::add : Nat -> Nat -> Nat */
expr mk_nat_add_fn();
inline expr nAdd(expr const & e1, expr const & e2) { return mk_app(mk_nat_add_fn(), e1, e2); }
/** \brief Multiplication, Nat::mul : Nat -> Nat -> Nat */
expr mk_nat_mul_fn();
inline expr nMul(expr const & e1, expr const & e2) { return mk_app(mk_nat_mul_fn(), e1, e2); }
/** \brief Less than or equal to, Nat::le : Nat -> Nat -> Bool */
expr mk_nat_le_fn();
inline expr nLe(expr const & e1, expr const & e2) { return mk_app(mk_nat_le_fn(), e1, e2); }
/** \brief Greater than or equal to, Nat::ge : Nat -> Nat -> Bool */
expr mk_nat_ge_fn();
inline expr nGe(expr const & e1, expr const & e2) { return mk_app(mk_nat_ge_fn(), e1, e2); }
/** \brief Less than, Nat::lt : Nat -> Nat -> Bool */
expr mk_nat_lt_fn();
inline expr nLt(expr const & e1, expr const & e2) { return mk_app(mk_nat_lt_fn(), e1, e2); }
/** \brief Greater than, Nat::gt : Nat -> Nat -> Bool */
expr mk_nat_gt_fn();
inline expr nGt(expr const & e1, expr const & e2) { return mk_app(mk_nat_gt_fn(), e1, e2); }
/** \brief Identity function for natural numbers, Nat::id : Nat -> Nat */
expr mk_nat_id_fn();
inline expr nId(expr const & e) { return mk_app(mk_nat_id_fn(), e); }
/** \brief If-then-else for natural numbers */
inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(Nat, c, t, e); }
expr mk_Nat_add_fn();
inline expr mk_Nat_add(expr const & e1, expr const & e2) { return mk_app(mk_Nat_add_fn(), e1, e2); }
expr mk_Nat_mul_fn();
inline expr mk_Nat_mul(expr const & e1, expr const & e2) { return mk_app(mk_Nat_mul_fn(), e1, e2); }
expr mk_Nat_le_fn();
inline expr mk_Nat_le(expr const & e1, expr const & e2) { return mk_app(mk_Nat_le_fn(), e1, e2); }
class environment;
/** \brief Import Natural number library in the given environment (if it has not been imported already). */

View file

@ -14,9 +14,9 @@ Author: Leonardo de Moura
#include "library/arith/real.h"
#include "library/arith/int.h"
#include "library/arith/nat.h"
#include "library/arith/Real_decls.cpp"
namespace lean {
MK_CONSTANT(Real, "Real");
expr const Real = mk_Real();
expr mk_real_type() { return mk_Real(); }
@ -85,18 +85,18 @@ constexpr char real_add_name[] = "add";
/** \brief Evaluator for + : Real -> Real -> Real */
struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; };
typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
MK_BUILTIN(real_add_fn, real_add_value);
static value::register_deserializer_fn real_add_ds("real_add", [](deserializer & ) { return mk_real_add_fn(); });
static register_builtin_fn real_add_blt(name({"Real", "add"}), []() { return mk_real_add_fn(); });
MK_BUILTIN(Real_add_fn, real_add_value);
static value::register_deserializer_fn real_add_ds("real_add", [](deserializer & ) { return mk_Real_add_fn(); });
static register_builtin_fn real_add_blt(name({"Real", "add"}), []() { return mk_Real_add_fn(); });
constexpr char real_mul_name[] = "mul";
/** \brief Evaluator for * : Real -> Real -> Real */
struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; };
typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
MK_BUILTIN(real_mul_fn, real_mul_value);
static value::register_deserializer_fn real_mul_ds("real_mul", [](deserializer & ) { return mk_real_mul_fn(); });
static register_builtin_fn real_mul_blt(name({"Real", "mul"}), []() { return mk_real_mul_fn(); });
MK_BUILTIN(Real_mul_fn, real_mul_value);
static value::register_deserializer_fn real_mul_ds("real_mul", [](deserializer & ) { return mk_Real_mul_fn(); });
static register_builtin_fn real_mul_blt(name({"Real", "mul"}), []() { return mk_Real_mul_fn(); });
constexpr char real_div_name[] = "div";
/** \brief Evaluator for / : Real -> Real -> Real */
@ -109,9 +109,9 @@ struct real_div_eval {
};
};
typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
MK_BUILTIN(real_div_fn, real_div_value);
static value::register_deserializer_fn real_div_ds("real_div", [](deserializer & ) { return mk_real_div_fn(); });
static register_builtin_fn real_div_blt(name({"Real", "div"}), []() { return mk_real_div_fn(); });
MK_BUILTIN(Real_div_fn, real_div_value);
static value::register_deserializer_fn real_div_ds("real_div", [](deserializer & ) { return mk_Real_div_fn(); });
static register_builtin_fn real_div_blt(name({"Real", "div"}), []() { return mk_Real_div_fn(); });
/**
\brief Semantic attachment for less than or equal to operator with type
@ -129,9 +129,9 @@ public:
}
virtual void write(serializer & s) const { s << "real_le"; }
};
MK_BUILTIN(real_le_fn, real_le_value);
static value::register_deserializer_fn real_le_ds("real_le", [](deserializer & ) { return mk_real_le_fn(); });
static register_builtin_fn real_le_btl(name({"Real", "le"}), []() { return mk_real_le_fn(); });
MK_BUILTIN(Real_le_fn, real_le_value);
static value::register_deserializer_fn real_le_ds("real_le", [](deserializer & ) { return mk_Real_le_fn(); });
static register_builtin_fn real_le_btl(name({"Real", "le"}), []() { return mk_Real_le_fn(); });
class int_to_real_value : public const_value {
public:
@ -149,14 +149,6 @@ MK_BUILTIN(int_to_real_fn, int_to_real_value);
static value::register_deserializer_fn int_to_real_ds("int_to_real", [](deserializer & ) { return mk_int_to_real_fn(); });
static register_builtin_fn int_to_real_blt("int_to_real", []() { return mk_int_to_real_fn(); });
MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
MK_CONSTANT(real_abs_fn, name({"Real", "abs"}));
MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
void import_real(environment const & env, io_state const & ios) {
env->import("Real", ios);
}

View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "util/numerics/mpq.h"
#include "kernel/expr.h"
#include "kernel/builtin.h"
#include "library/arith/Real_decls.h"
namespace lean {
/** \brief Real numbers type */
@ -22,48 +23,14 @@ inline expr rVal(int v) { return mk_real_value(v); }
bool is_real_value(expr const & e);
mpq const & real_value_numeral(expr const & e);
/** \brief Addition, Real::add : Real -> Real -> Real */
expr mk_real_add_fn();
inline expr rAdd(expr const & e1, expr const & e2) { return mk_app(mk_real_add_fn(), e1, e2); }
/** \brief Subtraction, Real::sub : Real -> Real -> Real */
expr mk_real_sub_fn();
inline expr rSub(expr const & e1, expr const & e2) { return mk_app(mk_real_sub_fn(), e1, e2); }
/** \brief Unary minus, Real::neg : Real -> Real */
expr mk_real_neg_fn();
inline expr rNeg(expr const & e) { return mk_app(mk_real_neg_fn(), e); }
/** \brief Multiplication, Real::mul : Real -> Real -> Real */
expr mk_real_mul_fn();
inline expr rMul(expr const & e1, expr const & e2) { return mk_app(mk_real_mul_fn(), e1, e2); }
/** \brief Division, Real::mul : Real -> Real -> Real */
expr mk_real_div_fn();
inline expr rDiv(expr const & e1, expr const & e2) { return mk_app(mk_real_div_fn(), e1, e2); }
/** \brief Absolute value function, Real::abs : Real -> Real */
expr mk_real_abs_fn();
inline expr rAbs(expr const & e) { return mk_app(mk_real_abs_fn(), e); }
/** \brief Less than or equal to, Real::le : Real -> Real -> Bool */
expr mk_real_le_fn();
inline expr rLe(expr const & e1, expr const & e2) { return mk_app(mk_real_le_fn(), e1, e2); }
/** \brief Greater than or equal to, Real::ge : Real -> Real -> Bool */
expr mk_real_ge_fn();
inline expr rGe(expr const & e1, expr const & e2) { return mk_app(mk_real_ge_fn(), e1, e2); }
/** \brief Less than, Real::lt : Real -> Real -> Bool */
expr mk_real_lt_fn();
inline expr rLt(expr const & e1, expr const & e2) { return mk_app(mk_real_lt_fn(), e1, e2); }
/** \brief Greater than, Real::gt : Real -> Real -> Bool */
expr mk_real_gt_fn();
inline expr rGt(expr const & e1, expr const & e2) { return mk_app(mk_real_gt_fn(), e1, e2); }
/** \brief If-then-else for reals */
inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(Real, c, t, e); }
expr mk_Real_add_fn();
inline expr mk_Real_add(expr const & e1, expr const & e2) { return mk_app(mk_Real_add_fn(), e1, e2); }
expr mk_Real_mul_fn();
inline expr mk_Real_mul(expr const & e1, expr const & e2) { return mk_app(mk_Real_mul_fn(), e1, e2); }
expr mk_Real_div_fn();
inline expr mk_Real_div(expr const & e1, expr const & e2) { return mk_app(mk_Real_div_fn(), e1, e2); }
expr mk_Real_le_fn();
inline expr mk_Real_le(expr const & e1, expr const & e2) { return mk_app(mk_Real_le_fn(), e1, e2); }
class environment;
/** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */
@ -71,10 +38,7 @@ void import_real(environment const & env, io_state const & ios);
/** \brief Coercion from int to real */
expr mk_int_to_real_fn();
inline expr i2r(expr const & e) { return mk_app(mk_int_to_real_fn(), e); }
/** \brief Coercion from nat to real */
expr mk_nat_to_real_fn();
inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); }
inline expr mk_int_to_real(expr const & e) { return mk_app(mk_int_to_real_fn(), e); }
/** \brief Import the coercions \c i2r and \c n2r. The Integer and (basic) Real libraries are also imported. */
void import_int_to_real_coercions(environment const & env);

View file

@ -30,7 +30,4 @@ inline expr And(std::initializer_list<expr> const & l) { return mk_and(l.size(),
inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_rop(mk_or_fn(), False, num_args, args); }
inline expr Or(std::initializer_list<expr> const & l) { return mk_or(l.size(), l.begin()); }
inline expr mk_iff(unsigned num_args, expr const * args) { return mk_bin_rop(mk_iff_fn(), True, num_args, args); }
inline expr Iff(std::initializer_list<expr> const & l) { return mk_iff(l.size(), l.begin()); }
}

View file

@ -43,7 +43,7 @@ class deep_copy_fn {
new_args.push_back(apply(old_arg));
return save_result(a, mk_app(new_args), sh);
}
case expr_kind::Eq: return save_result(a, mk_eq(apply(eq_lhs(a)), apply(eq_rhs(a))), sh);
case expr_kind::HEq: return save_result(a, mk_heq(apply(heq_lhs(a)), apply(heq_rhs(a))), sh);
case expr_kind::Lambda: return save_result(a, mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
case expr_kind::Pi: return save_result(a, mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
case expr_kind::Let: return save_result(a, mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))), sh);

View file

@ -621,7 +621,7 @@ class elaborator::imp {
}
void process_eq(context const & ctx, expr & a) {
if (is_eq(a) && m_use_normalizer) {
if (is_heq(a) && m_use_normalizer) {
a = normalize(ctx, a);
}
}
@ -840,16 +840,17 @@ class elaborator::imp {
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption);
}
imitation = mk_lambda(arg_types, mk_app(imitation_args));
} else if (is_eq(b)) {
} else if (is_heq(b)) {
// Imitation for equality
// Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), (h_1 x_1 ... x_{num_a}) = (h_2 x_1 ... x_{num_a})
// New constraints (h_1 a_1 ... a_{num_a}) == eq_lhs(b)
// (h_2 a_1 ... a_{num_a}) == eq_rhs(b)
expr h_1 = new_state.m_menv->mk_metavar(ctx);
expr h_2 = new_state.m_menv->mk_metavar(ctx);
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), eq_lhs(b), new_assumption);
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), eq_rhs(b), new_assumption);
imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1), mk_app_vars(add_lift(h_2, 0, num_a - 1), num_a - 1)));
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), heq_lhs(b), new_assumption);
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), heq_rhs(b), new_assumption);
imitation = mk_lambda(arg_types, mk_heq(mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1),
mk_app_vars(add_lift(h_2, 0, num_a - 1), num_a - 1)));
} else if (is_abstraction(b)) {
// Imitation for lambdas and Pis
// Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}),
@ -1063,7 +1064,7 @@ class elaborator::imp {
void imitate_equality(expr const & a, expr const & b, unification_constraint const & c) {
lean_assert(is_metavar(a));
static_cast<void>(b); // this line is just to avoid a warning, b is only used in an assertion
lean_assert(is_eq(b));
lean_assert(is_heq(b));
lean_assert(!is_assigned(a));
lean_assert(has_local_context(a));
// imitate
@ -1074,7 +1075,7 @@ class elaborator::imp {
context ctx_m = m_state.m_menv->get_context(m);
expr h1 = m_state.m_menv->mk_metavar(ctx_m);
expr h2 = m_state.m_menv->mk_metavar(ctx_m);
expr imitation = mk_eq(h1, h2);
expr imitation = mk_heq(h1, h2);
justification new_jst(new imitation_justification(c));
push_new_constraint(true, ctx_m, m, imitation, new_jst);
}
@ -1137,7 +1138,7 @@ class elaborator::imp {
} else if (is_app(b) && !has_metavar(arg(b, 0))) {
imitate_application(a, b, c);
return true;
} else if (is_eq(b)) {
} else if (is_heq(b)) {
imitate_equality(a, b, c);
return true;
}

View file

@ -9,13 +9,13 @@ Author: Leonardo de Moura
namespace lean {
bool is_eq_heq(expr const & e) {
return is_eq(e) || is_homo_eq(e);
return is_heq(e) || is_eq(e);
}
expr_pair eq_heq_args(expr const & e) {
lean_assert(is_eq(e) || is_homo_eq(e));
if (is_eq(e))
return expr_pair(eq_lhs(e), eq_rhs(e));
lean_assert(is_heq(e) || is_eq(e));
if (is_heq(e))
return expr_pair(heq_lhs(e), heq_rhs(e));
else
return expr_pair(arg(e, 2), arg(e, 3));
}

View file

@ -37,11 +37,11 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
return is_lt(arg(a, i), arg(b, i), use_hash);
}
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Eq:
if (eq_lhs(a) != eq_lhs(b))
return is_lt(eq_lhs(a), eq_lhs(b), use_hash);
case expr_kind::HEq:
if (heq_lhs(a) != heq_lhs(b))
return is_lt(heq_lhs(a), heq_lhs(b), use_hash);
else
return is_lt(eq_rhs(a), eq_rhs(b), use_hash);
return is_lt(heq_rhs(a), heq_rhs(b), use_hash);
case expr_kind::Lambda: // Remark: we ignore get_abs_name because we want alpha-equivalence
case expr_kind::Pi:
if (abst_domain(a) != abst_domain(b))

View file

@ -62,7 +62,7 @@ optional<substitution> fo_unify(expr e1, expr e2) {
}
}
break;
case expr_kind::Eq:
case expr_kind::HEq:
lean_unreachable(); break; // LCOV_EXCL_LINE
case expr_kind::Lambda: case expr_kind::Pi:
todo.emplace_back(abst_body(e1), abst_body(e2));

View file

@ -322,8 +322,8 @@ static int expr_mk_app(lua_State * L) {
return push_expr(L, mk_app(args));
}
static int expr_mk_eq(lua_State * L) {
return push_expr(L, mk_eq(to_expr(L, 1), to_expr(L, 2)));
static int expr_mk_heq(lua_State * L) {
return push_expr(L, mk_heq(to_expr(L, 1), to_expr(L, 2)));
}
static int expr_mk_lambda(lua_State * L) {
@ -437,7 +437,7 @@ static int expr_ ## P(lua_State * L) { \
EXPR_PRED(is_constant)
EXPR_PRED(is_var)
EXPR_PRED(is_app)
EXPR_PRED(is_eq)
EXPR_PRED(is_heq)
EXPR_PRED(is_lambda)
EXPR_PRED(is_pi)
EXPR_PRED(is_abstraction)
@ -450,12 +450,8 @@ EXPR_PRED(has_metavar)
EXPR_PRED(is_not)
EXPR_PRED(is_and)
EXPR_PRED(is_or)
EXPR_PRED(is_if)
EXPR_PRED(is_iff)
EXPR_PRED(is_implies)
EXPR_PRED(is_forall)
EXPR_PRED(is_exists)
EXPR_PRED(is_homo_eq)
/**
\brief Iterator (closure base function) for application args. See \c expr_args
@ -502,7 +498,7 @@ static int expr_fields(lua_State * L) {
case expr_kind::Type: return push_level(L, ty_level(e));
case expr_kind::Value: return to_value(e).push_lua(L);
case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2;
case expr_kind::Eq: push_expr(L, eq_lhs(e)); push_expr(L, eq_rhs(e)); return 2;
case expr_kind::HEq: push_expr(L, heq_lhs(e)); push_expr(L, heq_rhs(e)); return 2;
case expr_kind::Lambda:
case expr_kind::Pi:
push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3;
@ -617,7 +613,7 @@ static const struct luaL_Reg expr_m[] = {
{"is_var", safe_function<expr_is_var>},
{"is_constant", safe_function<expr_is_constant>},
{"is_app", safe_function<expr_is_app>},
{"is_eq", safe_function<expr_is_eq>},
{"is_heq", safe_function<expr_is_heq>},
{"is_lambda", safe_function<expr_is_lambda>},
{"is_pi", safe_function<expr_is_pi>},
{"is_abstraction", safe_function<expr_is_abstraction>},
@ -644,12 +640,8 @@ static const struct luaL_Reg expr_m[] = {
{"is_not", safe_function<expr_is_not>},
{"is_and", safe_function<expr_is_and>},
{"is_or", safe_function<expr_is_or>},
{"is_if", safe_function<expr_is_if>},
{"is_iff", safe_function<expr_is_iff>},
{"is_implies", safe_function<expr_is_implies>},
{"is_forall", safe_function<expr_is_forall>},
{"is_exists", safe_function<expr_is_exists>},
{"is_home_eq", safe_function<expr_is_homo_eq>},
{0, 0}
};
@ -669,8 +661,8 @@ static void open_expr(lua_State * L) {
SET_GLOBAL_FUN(expr_mk_var, "mk_var");
SET_GLOBAL_FUN(expr_mk_var, "Var");
SET_GLOBAL_FUN(expr_mk_app, "mk_app");
SET_GLOBAL_FUN(expr_mk_eq, "mk_eq");
SET_GLOBAL_FUN(expr_mk_eq, "Eq");
SET_GLOBAL_FUN(expr_mk_heq, "mk_heq");
SET_GLOBAL_FUN(expr_mk_heq, "HEq");
SET_GLOBAL_FUN(expr_mk_lambda, "mk_lambda");
SET_GLOBAL_FUN(expr_mk_pi, "mk_pi");
SET_GLOBAL_FUN(expr_mk_arrow, "mk_arrow");
@ -690,7 +682,7 @@ static void open_expr(lua_State * L) {
SET_ENUM("Type", expr_kind::Type);
SET_ENUM("Value", expr_kind::Value);
SET_ENUM("App", expr_kind::App);
SET_ENUM("Eq", expr_kind::Eq);
SET_ENUM("HEq", expr_kind::HEq);
SET_ENUM("Lambda", expr_kind::Lambda);
SET_ENUM("Pi", expr_kind::Pi);
SET_ENUM("Let", expr_kind::Let);

View file

@ -18,7 +18,7 @@ bool is_atomic(expr const & e) {
case expr_kind::Type: case expr_kind::MetaVar:
return true;
case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi:
case expr_kind::Eq: case expr_kind::Let:
case expr_kind::HEq: case expr_kind::Let:
return false;
}
return false;
@ -55,10 +55,10 @@ struct print_expr_fn {
}
}
void print_eq(expr const & a, context const & c) {
print_child(eq_lhs(a), c);
void print_heq(expr const & a, context const & c) {
print_child(heq_lhs(a), c);
out() << " == ";
print_child(eq_rhs(a), c);
print_child(heq_rhs(a), c);
}
void print_app(expr const & e, context const & c) {
@ -114,8 +114,8 @@ struct print_expr_fn {
case expr_kind::App:
print_app(a, c);
break;
case expr_kind::Eq:
print_eq(a, c);
case expr_kind::HEq:
print_heq(a, c);
break;
case expr_kind::Lambda:
out() << "fun " << abst_name(a) << " : ";

View file

@ -117,11 +117,11 @@ bool fo_match::match_type(expr const & p, expr const & t, unsigned, subst_map &)
return p == t;
}
bool fo_match::match_eq(expr const & p, expr const & t, unsigned o, subst_map & s) {
bool fo_match::match_heq(expr const & p, expr const & t, unsigned o, subst_map & s) {
lean_trace("fo_match", tout << "match_eq : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
if (!is_eq(t))
if (!is_heq(t))
return false;
return match_main(eq_lhs(p), eq_lhs(t), o, s) && match_main(eq_rhs(p), eq_rhs(t), o, s);
return match_main(heq_lhs(p), heq_lhs(t), o, s) && match_main(heq_rhs(p), heq_rhs(t), o, s);
}
bool fo_match::match_let(expr const & p, expr const & t, unsigned o, subst_map & s) {
@ -176,8 +176,8 @@ bool fo_match::match_main(expr const & p, expr const & t, unsigned o, subst_map
return match_pi(p, t, o, s);
case expr_kind::Type:
return match_type(p, t, o, s);
case expr_kind::Eq:
return match_eq(p, t, o, s);
case expr_kind::HEq:
return match_heq(p, t, o, s);
case expr_kind::Let:
return match_let(p, t, o, s);
case expr_kind::MetaVar:

View file

@ -22,7 +22,7 @@ private:
bool match_lambda(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_pi(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_type(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_eq(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_heq(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_let(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_metavar(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_main(expr const & p, expr const & t, unsigned o, subst_map & s);

View file

@ -47,7 +47,7 @@ pair<expr, expr> rewrite_lambda_type(environment const & env, context & ctx, exp
expr const & new_ty = result_ty.first;
expr const & ty_v = ti(v, ctx);
if (ty == new_ty) {
return make_pair(v, Refl(ty_v, v));
return make_pair(v, mk_refl_th(ty_v, v));
} else {
name const & n = abst_name(v);
expr const & body = abst_body(v);
@ -55,10 +55,10 @@ pair<expr, expr> rewrite_lambda_type(environment const & env, context & ctx, exp
expr const & new_v = mk_lambda(n, new_ty, body);
expr const & ty_ty = ti(ty, ctx);
lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types
expr const & proof = Subst(ty_ty, ty, new_ty,
expr const & proof = mk_subst_th(ty_ty, ty, new_ty,
Fun({Const("T"), ty_ty},
mk_eq(v, mk_lambda(n, Const("T"), body))),
Refl(ty_v, v), pf_ty);
mk_heq(v, mk_lambda(n, Const("T"), body))),
mk_refl_th(ty_v, v), pf_ty);
return make_pair(new_v, proof);
}
}
@ -83,7 +83,7 @@ pair<expr, expr> rewrite_lambda_body(environment const & env, context & ctx, exp
expr const & new_body = result_body.first;
expr const & ty_v = ti(v, ctx);
if (body == new_body) {
return make_pair(v, Refl(ty_v, v));
return make_pair(v, mk_refl_th(ty_v, v));
} else {
name const & n = abst_name(v);
expr const & ty = abst_domain(v);
@ -91,7 +91,7 @@ pair<expr, expr> rewrite_lambda_body(environment const & env, context & ctx, exp
expr const & new_v = mk_lambda(n, ty, new_body);
expr const & ty_body = ti(body, extend(ctx, n, ty));
lean_assert_eq(ty_body, ti(new_body, ctx)); // TODO(soonhok): generalize for hetreogeneous types
expr const & proof = Abst(ty, mk_lambda(n, ty, ty_body), v, new_v, mk_lambda(n, ty, pf_body));
expr const & proof = mk_funext_th(ty, mk_lambda(n, ty, ty_body), v, new_v, mk_lambda(n, ty, pf_body));
return make_pair(new_v, proof);
}
}
@ -128,18 +128,18 @@ pair<expr, expr> rewrite_lambda(environment const & env, context & ctx, expr con
expr const & ty_new_v1 = ti(v, ctx);
expr const & new_v2 = mk_lambda(n, new_ty, new_body);
// proof1 : v = new_v1
expr const & proof1 = Subst(ty_ty, ty, new_ty,
expr const & proof1 = mk_subst_th(ty_ty, ty, new_ty,
Fun({Const("T"), ty_ty},
mk_eq(v, mk_lambda(n, Const("T"), body))),
Refl(ty_v, v),
mk_heq(v, mk_lambda(n, Const("T"), body))),
mk_refl_th(ty_v, v),
pf_ty);
// proof2 : new_v1 = new_v2
expr const & proof2 = Subst(ty_body, body, new_body,
expr const & proof2 = mk_subst_th(ty_body, body, new_body,
Fun({Const("e"), ty_body},
mk_eq(new_v1, mk_lambda(n, new_ty, Const("e")))),
Refl(ty_new_v1, new_v1),
mk_heq(new_v1, mk_lambda(n, new_ty, Const("e")))),
mk_refl_th(ty_new_v1, new_v1),
pf_body);
expr const & proof = Trans(ty_v, v, new_v1, new_v2, proof1, proof2);
expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
return make_pair(new_v2, proof);
}
@ -166,10 +166,10 @@ pair<expr, expr> rewrite_pi_type(environment const & env, context & ctx, expr co
expr const & new_v = mk_pi(n, new_ty, body);
expr const & ty_ty = ti(ty, ctx);
expr const & ty_v = ti(v, ctx);
expr const & proof = Subst(ty_ty, ty, new_ty,
expr const & proof = mk_subst_th(ty_ty, ty, new_ty,
Fun({Const("T"), ty_ty},
mk_eq(v, mk_pi(n, Const("T"), body))),
Refl(ty_v, v),
mk_heq(v, mk_pi(n, Const("T"), body))),
mk_refl_th(ty_v, v),
pf);
return make_pair(new_v, proof);
}
@ -198,10 +198,10 @@ pair<expr, expr> rewrite_pi_body(environment const & env, context & ctx, expr co
expr const & new_v = mk_pi(n, ty, new_body);
expr const & ty_body = ti(body, extend(ctx, n, ty));
expr const & ty_v = ti(v, ctx);
expr const & proof = Subst(ty_body, body, new_body,
expr const & proof = mk_subst_th(ty_body, body, new_body,
Fun({Const("e"), ty_body},
mk_eq(v, mk_pi(n, ty, Const("e")))),
Refl(ty_v, v),
mk_heq(v, mk_pi(n, ty, Const("e")))),
mk_refl_th(ty_v, v),
pf);
return make_pair(new_v, proof);
}
@ -237,17 +237,17 @@ pair<expr, expr> rewrite_pi(environment const & env, context & ctx, expr const &
expr const & new_v1 = mk_pi(n, new_ty, body);
expr const & ty_new_v1 = ti(v, ctx);
expr const & new_v2 = mk_pi(n, new_ty, new_body);
expr const & proof1 = Subst(ty_ty, ty, new_ty,
expr const & proof1 = mk_subst_th(ty_ty, ty, new_ty,
Fun({Const("T"), ty_ty},
mk_eq(v, mk_pi(n, Const("T"), body))),
Refl(ty_v, v),
mk_heq(v, mk_pi(n, Const("T"), body))),
mk_refl_th(ty_v, v),
pf_ty);
expr const & proof2 = Subst(ty_body, body, new_body,
expr const & proof2 = mk_subst_th(ty_body, body, new_body,
Fun({Const("e"), ty_body},
mk_eq(new_v1, mk_pi(n, new_ty, Const("e")))),
Refl(ty_new_v1, new_v1),
mk_heq(new_v1, mk_pi(n, new_ty, Const("e")))),
mk_refl_th(ty_new_v1, new_v1),
pf_body);
expr const & proof = Trans(ty_v, v, new_v1, new_v2, proof1, proof2);
expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
return make_pair(new_v2, proof);
}
@ -264,19 +264,19 @@ pair<expr, expr> rewrite_pi(environment const & env, context & ctx, expr const &
\return pair of v' = (lhs' = rhs), and proof of v = v'
*/
pair<expr, expr> rewrite_eq_lhs(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_lhs) {
lean_assert(is_eq(v));
lean_assert(is_heq(v));
type_inferer ti(env);
expr const & lhs = eq_lhs(v);
expr const & rhs = eq_rhs(v);
expr const & lhs = heq_lhs(v);
expr const & rhs = heq_rhs(v);
expr const & new_lhs = result_lhs.first;
expr const & pf = result_lhs.second;
expr const & new_v = mk_eq(new_lhs, rhs);
expr const & new_v = mk_heq(new_lhs, rhs);
expr const & ty_lhs = ti(lhs, ctx);
expr const & ty_v = ti(v, ctx);
expr const & proof = Subst(ty_lhs, lhs, new_lhs,
expr const & proof = mk_subst_th(ty_lhs, lhs, new_lhs,
Fun({Const("x"), ty_lhs},
mk_eq(v, mk_eq(Const("x"), rhs))),
Refl(ty_v, v),
mk_heq(v, mk_heq(Const("x"), rhs))),
mk_refl_th(ty_v, v),
pf);
return make_pair(new_v, proof);
}
@ -294,19 +294,19 @@ pair<expr, expr> rewrite_eq_lhs(environment const & env, context & ctx, expr con
\return pair of v' = (lhs = rhs'), and proof of v = v'
*/
pair<expr, expr> rewrite_eq_rhs(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_rhs) {
lean_assert(is_eq(v));
lean_assert(is_heq(v));
type_inferer ti(env);
expr const & lhs = eq_lhs(v);
expr const & rhs = eq_rhs(v);
expr const & lhs = heq_lhs(v);
expr const & rhs = heq_rhs(v);
expr const & new_rhs = result_rhs.first;
expr const & pf = result_rhs.second;
expr const & new_v = mk_eq(rhs, new_rhs);
expr const & new_v = mk_heq(rhs, new_rhs);
expr const & ty_rhs = ti(rhs, ctx);
expr const & ty_v = ti(v, ctx);
expr const & proof = Subst(ty_rhs, rhs, new_rhs,
expr const & proof = mk_subst_th(ty_rhs, rhs, new_rhs,
Fun({Const("x"), ty_rhs},
mk_eq(v, mk_eq(lhs, Const("x")))),
Refl(ty_v, v),
mk_heq(v, mk_heq(lhs, Const("x")))),
mk_refl_th(ty_v, v),
pf);
return make_pair(new_v, proof);
}
@ -326,31 +326,31 @@ pair<expr, expr> rewrite_eq_rhs(environment const & env, context & ctx, expr con
\return pair of v' = (lhs' = rhs'), and proof of v = v'
*/
pair<expr, expr> rewrite_eq(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_lhs, pair<expr, expr> const & result_rhs) {
lean_assert(is_eq(v));
lean_assert(is_heq(v));
type_inferer ti(env);
expr const & lhs = eq_lhs(v);
expr const & rhs = eq_rhs(v);
expr const & lhs = heq_lhs(v);
expr const & rhs = heq_rhs(v);
expr const & new_lhs = result_lhs.first;
expr const & pf_lhs = result_lhs.second;
expr const & new_rhs = result_rhs.first;
expr const & pf_rhs = result_rhs.second;
expr const & new_v1 = mk_eq(new_lhs, rhs);
expr const & new_v2 = mk_eq(new_lhs, new_rhs);
expr const & new_v1 = mk_heq(new_lhs, rhs);
expr const & new_v2 = mk_heq(new_lhs, new_rhs);
expr const & ty_lhs = ti(lhs, ctx);
expr const & ty_rhs = ti(rhs, ctx);
expr const & ty_v = ti(v, ctx);
expr const & ty_new_v1 = ti(new_v1, ctx);
expr const & proof1 = Subst(ty_lhs, lhs, new_lhs,
expr const & proof1 = mk_subst_th(ty_lhs, lhs, new_lhs,
Fun({Const("x"), ty_lhs},
mk_eq(v, mk_eq(Const("x"), rhs))),
Refl(ty_v, v),
mk_heq(v, mk_heq(Const("x"), rhs))),
mk_refl_th(ty_v, v),
pf_lhs);
expr const & proof2 = Subst(ty_rhs, rhs, new_rhs,
expr const & proof2 = mk_subst_th(ty_rhs, rhs, new_rhs,
Fun({Const("x"), ty_rhs},
mk_eq(v, mk_eq(lhs, Const("x")))),
Refl(ty_new_v1, new_v1),
mk_heq(v, mk_heq(lhs, Const("x")))),
mk_refl_th(ty_new_v1, new_v1),
pf_rhs);
expr const & proof = Trans(ty_v, v, new_v1, new_v2, proof1, proof2);
expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
return make_pair(new_v2, proof);
}
@ -379,10 +379,10 @@ pair<expr, expr> rewrite_let_type(environment const & env, context & ctx, expr c
expr const & new_v = mk_let(n, new_ty, val, body);
expr const & ty_ty = ti(ty, ctx);
expr const & ty_v = ti(v, ctx);
expr const & proof = Subst(ty_ty, ty, new_ty,
expr const & proof = mk_subst_th(ty_ty, ty, new_ty,
Fun({Const("x"), ty_ty},
mk_eq(v, mk_let(n, Const("x"), val, body))),
Refl(ty_v, v),
mk_heq(v, mk_let(n, Const("x"), val, body))),
mk_refl_th(ty_v, v),
pf);
return make_pair(new_v, proof);
} else {
@ -414,10 +414,10 @@ pair<expr, expr> rewrite_let_value(environment const & env, context & ctx, expr
expr const & new_v = mk_let(n, ty, new_val, body);
expr const & ty_val = ti(val, ctx);
expr const & ty_v = ti(v, ctx);
expr const & proof = Subst(ty_val, val, new_val,
expr const & proof = mk_subst_th(ty_val, val, new_val,
Fun({Const("x"), ty_val},
mk_eq(v, mk_let(n, ty, Const("x"), body))),
Refl(ty_v, v),
mk_heq(v, mk_let(n, ty, Const("x"), body))),
mk_refl_th(ty_v, v),
pf);
return make_pair(new_v, proof);
}
@ -447,10 +447,10 @@ pair<expr, expr> rewrite_let_body(environment const & env, context & ctx, expr c
expr const & new_v = mk_let(n, ty, val, new_body);
expr const & ty_body = ti(body, extend(ctx, n, ty, body));
expr const & ty_v = ti(v, ctx);
expr const & proof = Subst(ty_body, body, new_body,
expr const & proof = mk_subst_th(ty_body, body, new_body,
Fun({Const("e"), ty_body},
mk_eq(v, mk_let(n, ty, val, Const("e")))),
Refl(ty_v, v),
mk_heq(v, mk_let(n, ty, val, Const("e")))),
mk_refl_th(ty_v, v),
pf);
return make_pair(new_v, proof);
}
@ -483,22 +483,22 @@ pair<expr, expr> rewrite_app(environment const & env, context & ctx, expr const
bool f_changed = f != new_f;
if (f_changed) {
if (arg(v, i) != results[i].first) {
// Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi
// congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi
// (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f
// a = g b
pf = Congr(f_ty_domain, f_ty_body, f, new_f, e_i, new_e_i, pf, pf_e_i);
pf = mk_congr_th(f_ty_domain, f_ty_body, f, new_f, e_i, new_e_i, pf, pf_e_i);
} else {
// Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi
// congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi
// (x : A) B x) (a : A) (H : f = g), f a = g a
pf = Congr1(f_ty_domain, f_ty_body, f, new_f, e_i, pf);
pf = mk_congr1_th(f_ty_domain, f_ty_body, f, new_f, e_i, pf);
}
} else {
if (arg(v, i) != results[i].first) {
// Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b
pf = Congr2(f_ty_domain, f_ty_body, e_i, new_e_i, f, pf_e_i);
// congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b
pf = mk_congr2_th(f_ty_domain, f_ty_body, e_i, new_e_i, f, pf_e_i);
} else {
// Refl
pf = Refl(ti(f(e_i), ctx), f(e_i));
// refl
pf = mk_refl_th(ti(f(e_i), ctx), f(e_i));
}
}
f = f (e_i);
@ -527,12 +527,12 @@ theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & bod
m_pattern = abst_body(m_pattern);
m_num_args++;
}
if (!is_eq(m_pattern)) {
if (!is_heq(m_pattern)) {
lean_trace("rewriter", tout << "Theorem " << m_type << " is not in the form of "
<< "Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs" << endl;);
}
m_rhs = eq_rhs(m_pattern);
m_pattern = eq_lhs(m_pattern);
m_rhs = heq_rhs(m_pattern);
m_pattern = heq_lhs(m_pattern);
lean_trace("rewriter", tout << "Number of Arg = " << m_num_args << endl;);
}
@ -631,7 +631,7 @@ pair<expr, expr> then_rewriter_cell::operator()(environment const & env, context
expr const & ty = type_inferer(env)(v, ctx);
if (v != new_result.first) {
result = make_pair(new_result.first,
Trans(ty, v, result.first, new_result.first, result.second, new_result.second));
mk_trans_th(ty, v, result.first, new_result.first, result.second, new_result.second));
}
}
return result;
@ -661,7 +661,7 @@ pair<expr, expr> try_rewriter_cell::operator()(environment const & env, context
}
// If the execution reaches here, it means every rewriter failed.
expr const & t = type_inferer(env)(v, ctx);
return make_pair(v, Refl(t, v));
return make_pair(v, mk_refl_th(t, v));
}
ostream & try_rewriter_cell::display(ostream & out) const {
out << "Try_RW({";
@ -705,7 +705,7 @@ pair<expr, expr> lambda_type_rewriter_cell::operator()(environment const & env,
return rewrite_lambda_type(env, ctx, v, result_ty);
} else {
// nothing changed
return make_pair(v, Refl(ti(v, ctx), v));
return make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
ostream & lambda_type_rewriter_cell::display(ostream & out) const {
@ -733,7 +733,7 @@ pair<expr, expr> lambda_body_rewriter_cell::operator()(environment const & env,
} else {
// nothing changed
type_inferer ti(env);
return make_pair(v, Refl(ti(v, ctx), v));
return make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
ostream & lambda_body_rewriter_cell::display(ostream & out) const {
@ -774,7 +774,7 @@ pair<expr, expr> pi_type_rewriter_cell::operator()(environment const & env, cont
} else {
// nothing changed
type_inferer ti(env);
return make_pair(v, Refl(ti(v, ctx), v));
return make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
ostream & pi_type_rewriter_cell::display(ostream & out) const {
@ -802,7 +802,7 @@ pair<expr, expr> pi_body_rewriter_cell::operator()(environment const & env, cont
} else {
// nothing changed
type_inferer ti(env);
return make_pair(v, Refl(ti(v, ctx), v));
return make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
ostream & pi_body_rewriter_cell::display(ostream & out) const {
@ -842,7 +842,7 @@ pair<expr, expr> let_type_rewriter_cell::operator()(environment const & env, con
return rewrite_let_type(env, ctx, v, result_ty);
} else {
type_inferer ti(env);
return make_pair(v, Refl(ti(v, ctx), v));
return make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
ostream & let_type_rewriter_cell::display(ostream & out) const {
@ -865,7 +865,7 @@ pair<expr, expr> let_value_rewriter_cell::operator()(environment const & env, co
return rewrite_let_value(env, ctx, v, result_val);
} else {
type_inferer ti(env);
return make_pair(v, Refl(ti(v, ctx), v));
return make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
ostream & let_value_rewriter_cell::display(ostream & out) const {
@ -890,7 +890,7 @@ pair<expr, expr> let_body_rewriter_cell::operator()(environment const & env, con
return rewrite_let_body(env, ctx, v, result_body);
} else {
type_inferer ti(env);
return make_pair(v, Refl(ti(v, ctx), v));
return make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
ostream & let_body_rewriter_cell::display(ostream & out) const {
@ -931,7 +931,7 @@ success_rewriter_cell::success_rewriter_cell():rewriter_cell(rewriter_kind::Succ
success_rewriter_cell::~success_rewriter_cell() { }
pair<expr, expr> success_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
expr const & t = type_inferer(env)(v, ctx);
return make_pair(v, Refl(t, v));
return make_pair(v, mk_refl_th(t, v));
}
ostream & success_rewriter_cell::display(ostream & out) const {
out << "Success_RW()";
@ -951,7 +951,7 @@ pair<expr, expr> repeat_rewriter_cell::operator()(environment const & env, conte
break;
expr const & ty = ti(v, ctx);
result = make_pair(new_result.first,
Trans(ty, v, result.first, new_result.first, result.second, new_result.second));
mk_trans_th(ty, v, result.first, new_result.first, result.second, new_result.second));
}
} catch (rewriter_exception &) {
return result;

View file

@ -382,14 +382,14 @@ class apply_rewriter_fn {
result = rewrite_app(env, ctx, v, results);
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
if (result.first != tmp.first) {
tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
result = tmp;
}
}
break;
case expr_kind::Eq: {
expr const & lhs = eq_lhs(v);
expr const & rhs = eq_rhs(v);
case expr_kind::HEq: {
expr const & lhs = heq_lhs(v);
expr const & rhs = heq_rhs(v);
std::pair<expr, expr> result_lhs = apply(env, ctx, lhs);
std::pair<expr, expr> result_rhs = apply(env, ctx, rhs);
expr const & new_lhs = result_lhs.first;
@ -408,12 +408,12 @@ class apply_rewriter_fn {
result = rewrite_eq_rhs(env, ctx, v, result_rhs);
} else {
// nothing changed
result = std::make_pair(v, Refl(ti(v, ctx), v));
result = std::make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
if (result.first != tmp.first) {
tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
result = tmp;
}
}
@ -439,12 +439,12 @@ class apply_rewriter_fn {
result = rewrite_lambda_body(env, ctx, v, result_body);
} else {
// nothing changed
result = std::make_pair(v, Refl(ti(v, ctx), v));
result = std::make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
if (result.first != tmp.first) {
tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
result = tmp;
}
}
@ -471,12 +471,12 @@ class apply_rewriter_fn {
result = rewrite_pi_body(env, ctx, v, result_body);
} else {
// nothing changed
result = std::make_pair(v, Refl(ti(v, ctx), v));
result = std::make_pair(v, mk_refl_th(ti(v, ctx), v));
}
}
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
if (result.first != tmp.first) {
tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
result = tmp;
}
}
@ -489,7 +489,7 @@ class apply_rewriter_fn {
expr new_v = v;
expr ty_v = ti(v, ctx);
expr pf = Refl(ty_v, v);
expr pf = mk_refl_th(ty_v, v);
bool changed = false;
if (ty) {
@ -507,7 +507,7 @@ class apply_rewriter_fn {
if (val != result_val.first) {
result = rewrite_let_value(env, ctx, new_v, result_val);
if (changed) {
pf = Trans(ty_v, v, new_v, result.first, pf, result.second);
pf = mk_trans_th(ty_v, v, new_v, result.first, pf, result.second);
} else {
pf = result.second;
}
@ -520,7 +520,7 @@ class apply_rewriter_fn {
if (body != result_body.first) {
result = rewrite_let_body(env, ctx, new_v, result_body);
if (changed) {
pf = Trans(ty_v, v, new_v, result.first, pf, result.second);
pf = mk_trans_th(ty_v, v, new_v, result.first, pf, result.second);
} else {
pf = result.second;
}
@ -531,7 +531,7 @@ class apply_rewriter_fn {
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
if (result.first != tmp.first) {
tmp.second = Trans(ty_v, v, result.first, tmp.first, result.second, tmp.second);
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
result = tmp;
}
}

View file

@ -44,7 +44,7 @@ tactic conj_tactic(bool all) {
for (auto nc : proof_info) {
name const & n = nc.first;
expr const & c = nc.second;
new_m.insert(n, Conj(arg(c, 1), arg(c, 2), find(m, name(n, 1)), find(m, name(n, 2))));
new_m.insert(n, mk_and_intro_th(arg(c, 1), arg(c, 2), find(m, name(n, 1)), find(m, name(n, 2))));
new_m.erase(name(n, 1));
new_m.erase(name(n, 2));
}
@ -104,9 +104,9 @@ tactic conj_hyp_tactic(bool all) {
expr const & H_1 = mk_constant(name(H_name, 1));
expr const & H_2 = mk_constant(name(H_name, 2));
if (occurs(H_1, pr))
pr = Let_simp(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
pr = Let_simp(H_1, mk_and_eliml_th(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
if (occurs(H_2, pr))
pr = Let_simp(H_2, Conjunct2(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
pr = Let_simp(H_2, mk_and_elimr_th(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
}
new_m.insert(goal_name, pr);
}
@ -161,7 +161,7 @@ optional<proof_state> disj_hyp_tactic_core(name const & goal_name, name const &
expr pr2 = find(m, name(goal_name, 2));
pr1 = Fun(hyp_name, arg(Href, 1), pr1);
pr2 = Fun(hyp_name, arg(Href, 2), pr2);
new_m.insert(goal_name, DisjCases(arg(Href, 1), arg(Href, 2), conclusion, mk_constant(hyp_name), pr1, pr2));
new_m.insert(goal_name, mk_or_elim_th(arg(Href, 1), arg(Href, 2), conclusion, mk_constant(hyp_name), pr1, pr2));
new_m.erase(name(goal_name, 1));
new_m.erase(name(goal_name, 2));
return pb(new_m, a);
@ -241,12 +241,12 @@ optional<proof_state_pair> disj_tactic(proof_state const & s, name gname) {
proof_builder pb = s.get_proof_builder();
proof_builder new_pb1 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m);
new_m.insert(gname, Disj1(arg(*conclusion, 1), find(m, gname), arg(*conclusion, 2)));
new_m.insert(gname, mk_or_introl_th(arg(*conclusion, 1), find(m, gname), arg(*conclusion, 2)));
return pb(new_m, a);
});
proof_builder new_pb2 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m);
new_m.insert(gname, Disj2(arg(*conclusion, 2), arg(*conclusion, 1), find(m, gname)));
new_m.insert(gname, mk_or_intror_th(arg(*conclusion, 2), arg(*conclusion, 1), find(m, gname)));
return pb(new_m, a);
});
proof_state s1(precision::Over, new_gs1, s.get_menv(), new_pb1, s.get_cex_builder());
@ -296,7 +296,7 @@ tactic absurd_tactic() {
expr a = arg(p1.second, 1);
for (auto const & p2 : g.get_hypotheses()) {
if (p2.second == a) {
expr pr = AbsurdElim(a, c, mk_constant(p2.first), mk_constant(p1.first));
expr pr = mk_absurd_elim_th(a, c, mk_constant(p2.first), mk_constant(p1.first));
proofs.emplace_front(gname, pr);
return optional<goal>(); // remove goal
}

View file

@ -215,7 +215,7 @@ tactic trivial_tactic() {
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional<goal> {
expr const & c = env->normalize(g.get_conclusion(), context(), true);
if (c == True) {
proofs.emplace_front(gname, Trivial);
proofs.emplace_front(gname, mk_trivial());
return optional<goal>();
} else {
return some(g);

View file

@ -71,12 +71,12 @@ static void tst3() {
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
env->add_definition("a", Int, iAdd(iVal(1), iVal(2)));
env->add_definition("a", Int, mk_Int_add(iVal(1), iVal(2)));
std::cout << env << "\n";
expr t = iAdd(Const("a"), iVal(1));
expr t = mk_Int_add(Const("a"), iVal(1));
std::cout << t << " --> " << normalize(t, env) << "\n";
lean_assert(normalize(t, env) == iVal(4));
env->add_definition("b", Int, iMul(iVal(2), Const("a")));
env->add_definition("b", Int, mk_Int_mul(iVal(2), Const("a")));
std::cout << "b --> " << normalize(Const("b"), env) << "\n";
lean_assert(normalize(Const("b"), env) == iVal(6));
try {
@ -111,21 +111,21 @@ static void tst4() {
std::cout << "tst4\n";
environment env; init_test_frontend(env);
env->add_definition("a", Int, iVal(1), true); // add opaque definition
expr t = iAdd(Const("a"), iVal(1));
expr t = mk_Int_add(Const("a"), iVal(1));
std::cout << t << " --> " << normalize(t, env) << "\n";
lean_assert(normalize(t, env) == t);
env->add_definition("b", Int, iAdd(Const("a"), iVal(1)));
expr t2 = iSub(Const("b"), iVal(9));
env->add_definition("b", Int, mk_Int_add(Const("a"), iVal(1)));
expr t2 = mk_Int_sub(Const("b"), iVal(9));
std::cout << t2 << " --> " << normalize(t2, env) << "\n";
lean_assert_eq(normalize(t2, env, context()),
iSub(iAdd(Const("a"), iVal(1)), iVal(9)));
mk_Int_sub(mk_Int_add(Const("a"), iVal(1)), iVal(9)));
}
static void tst5() {
environment env; init_test_frontend(env);
env->add_definition("a", Int, iVal(1), true); // add opaque definition
try {
std::cout << type_check(iAdd(Const("a"), Int), env) << "\n";
std::cout << type_check(mk_Int_add(Const("a"), Int), env) << "\n";
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
@ -163,10 +163,6 @@ static void tst7() {
environment env; init_test_frontend(env);
env->add_var("a", Int);
env->add_var("b", Int);
expr t = If(Int, True, Const("a"), Const("b"));
std::cout << t << " --> " << normalize(t, env) << "\n";
std::cout << type_check(t, env) << "\n";
std::cout << "Environment\n" << env;
}
static void tst8() {
@ -208,11 +204,11 @@ static void tst10() {
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
env->add_definition("b", Int, iAdd(a, a));
env->add_definition("b", Int, mk_Int_add(a, a));
lean_assert(env->get_object("b").get_weight() == 2);
env->add_definition("c", Int, iAdd(a, b));
env->add_definition("c", Int, mk_Int_add(a, b));
lean_assert(env->get_object("c").get_weight() == 3);
env->add_definition("d", Int, iAdd(b, b));
env->add_definition("d", Int, mk_Int_add(b, b));
lean_assert(env->get_object("d").get_weight() == 3);
}

View file

@ -76,8 +76,8 @@ static unsigned depth2(expr const & e) {
std::accumulate(begin_args(e), end_args(e), 0,
[](unsigned m, expr const & arg){ return std::max(depth2(arg), m); })
+ 1;
case expr_kind::Eq:
return std::max(depth2(eq_lhs(e)), depth2(eq_rhs(e))) + 1;
case expr_kind::HEq:
return std::max(depth2(heq_lhs(e)), depth2(heq_rhs(e))) + 1;
case expr_kind::Lambda: case expr_kind::Pi:
return std::max(depth2(abst_domain(e)), depth2(abst_body(e))) + 1;
case expr_kind::Let:
@ -135,8 +135,8 @@ static unsigned count_core(expr const & a, expr_set & s) {
case expr_kind::App:
return std::accumulate(begin_args(a), end_args(a), 1,
[&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
case expr_kind::Eq:
return count_core(eq_lhs(a), s) + count_core(eq_rhs(a), s) + 1;
case expr_kind::HEq:
return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s) + 1;
case expr_kind::Lambda: case expr_kind::Pi:
return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
case expr_kind::Let:
@ -295,7 +295,7 @@ static void tst13() {
}
static void tst14() {
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
check_serializer(t);
std::cout << t << "\n";
expr l = mk_let("a", none_expr(), Const("b"), Var(0));
@ -329,9 +329,9 @@ static void tst15() {
lean_assert(has_metavar(f(a, a, m)));
lean_assert(has_metavar(f(a, m, a, a)));
lean_assert(!has_metavar(f(a, a, a, a)));
lean_assert(!has_metavar(Eq(a, f(a))));
lean_assert(has_metavar(Eq(m, f(a))));
lean_assert(has_metavar(Eq(a, f(m))));
lean_assert(!has_metavar(HEq(a, f(a))));
lean_assert(has_metavar(HEq(m, f(a))));
lean_assert(has_metavar(HEq(a, f(m))));
}
static void check_copy(expr const & e) {
@ -346,7 +346,7 @@ static void tst16() {
expr a = Const("a");
check_copy(iVal(10));
check_copy(f(a));
check_copy(Eq(f(a), a));
check_copy(HEq(f(a), a));
check_copy(mk_metavar("M"));
check_copy(mk_lambda("x", a, Var(0)));
check_copy(mk_pi("x", a, Var(0)));

View file

@ -75,11 +75,11 @@ static void tst4() {
lean_assert(fn(Fun({x, Type()}, Var(0))) == 0);
lean_assert(fn(Fun({x, Var(0)}, Var(0))) == 1);
lean_assert(fn(Fun({x, Var(0)}, Var(2))) == 2);
lean_assert(fn(Fun({x, Var(0)}, Eq(Var(2), Var(1)))) == 2);
lean_assert(fn(Fun({x, Var(0)}, HEq(Var(2), Var(1)))) == 2);
lean_assert(fn(Pi({x, Type()}, Var(0))) == 0);
lean_assert(fn(Pi({x, Var(0)}, Var(0))) == 1);
lean_assert(fn(Pi({x, Var(0)}, Var(2))) == 2);
lean_assert(fn(Pi({x, Var(0)}, Eq(Var(2), Var(1)))) == 2);
lean_assert(fn(Pi({x, Var(0)}, HEq(Var(2), Var(1)))) == 2);
context ctx;
ctx = extend(ctx, name("x"), Bool);
ctx = extend(ctx, name("y"), Bool);

View file

@ -275,7 +275,7 @@ static void tst14() {
expr y = Const("y");
env->add_var("h", Pi({N, Type()}, N >> (N >> N)));
expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a));
(Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(a));
metavar_env menv2 = menv.copy();
menv2->assign(m1, h(Var(4), Var(1), Var(3)));
normalizer norm(env);
@ -288,10 +288,10 @@ static void tst14() {
lean_assert(menv2->instantiate_metavars(norm(F1)) ==
norm(menv2->instantiate_metavars(F1)));
expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a, m2)))(M);
(Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(a, m2)))(M);
std::cout << norm(F2) << "\n";
expr F3 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(b, m2)))(M);
(Fun({{x, N}, {y, N}}, HEq(f(m1), y)))(b, m2)))(M);
std::cout << norm(F3) << "\n";
}

View file

@ -76,8 +76,8 @@ unsigned count_core(expr const & a, expr_set & s) {
case expr_kind::App:
return std::accumulate(begin_args(a), end_args(a), 1,
[&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
case expr_kind::Eq:
return count_core(eq_lhs(a), s) + count_core(eq_rhs(a), s) + 1;
case expr_kind::HEq:
return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s) + 1;
case expr_kind::Lambda: case expr_kind::Pi:
return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1;
case expr_kind::Let:
@ -197,9 +197,9 @@ static void tst3() {
env->add_var("a", Bool);
expr t1 = Const("a");
expr t2 = Const("a");
expr e = Eq(t1, t2);
expr e = HEq(t1, t2);
std::cout << e << " --> " << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == Eq(t1, t2));
lean_assert(normalize(e, env) == HEq(t1, t2));
}
static void tst4() {
@ -286,7 +286,7 @@ static void tst8() {
expr P = Const("P");
expr v0 = Var(0);
expr v1 = Var(1);
expr F = mk_forall(Int, mk_lambda("x", Int, Not(mk_lambda("x", Int, mk_exists(Int, mk_lambda("y", Int, P(v1, v0))))(v0))));
expr F = mk_pi("x", Int, Not(mk_lambda("x", Int, mk_exists(Int, mk_lambda("y", Int, P(v1, v0))))(v0)));
normalizer proc(env);
expr N1 = proc(F);
expr N2 = proc(deep_copy(F));

View file

@ -80,7 +80,7 @@ static void tst2() {
static void tst3() {
environment env;
init_test_frontend(env);
expr f = Fun("a", Bool, Eq(Const("a"), True));
expr f = Fun("a", Bool, HEq(Const("a"), True));
std::cout << type_check(f, env) << "\n";
lean_assert(type_check(f, env) == mk_arrow(Bool, Bool));
expr t = mk_let("a", none_expr(), True, Var(0));
@ -90,7 +90,7 @@ static void tst3() {
static void tst4() {
environment env;
init_test_frontend(env);
expr a = Eq(iVal(1), iVal(2));
expr a = HEq(iVal(1), iVal(2));
expr pr = mk_lambda("x", a, Var(0));
std::cout << type_check(pr, env) << "\n";
}
@ -105,7 +105,7 @@ static void tst5() {
expr prop = P;
expr pr = H;
for (unsigned i = 1; i < n; i++) {
pr = Conj(P, prop, H, pr);
pr = mk_and_intro_th(P, prop, H, pr);
prop = And(P, prop);
}
}
@ -191,8 +191,8 @@ static void tst10() {
expr t1 = Let({{a, f(b)}, {a, f(a)}}, f(a));
expr t2 = f(f(f(b)));
std::cout << t1 << " --> " << normalize(t1, env) << "\n";
expr prop = Eq(t1, t2);
expr proof = Refl(Int, t1);
expr prop = HEq(t1, t2);
expr proof = mk_refl_th(Int, t1);
env->add_theorem("simp_eq", prop, proof);
std::cout << env->get_object("simp_eq").get_name() << "\n";
}
@ -215,8 +215,8 @@ static void tst11() {
t3 = f(t3, t3);
}
lean_assert(t1 != t2);
env->add_theorem("eqs1", Eq(t1, t2), Refl(Int, t1));
env->add_theorem("eqs2", Eq(t1, t3), Refl(Int, t1));
env->add_theorem("eqs1", HEq(t1, t2), mk_refl_th(Int, t1));
env->add_theorem("eqs2", HEq(t1, t3), mk_refl_th(Int, t1));
}
static expr mk_big(unsigned depth) {
@ -257,7 +257,7 @@ static void tst13() {
env->add_var("f", Type() >> Type());
expr f = Const("f");
std::cout << type_check(f(Bool), env) << "\n";
std::cout << type_check(f(Eq(True, False)), env) << "\n";
std::cout << type_check(f(HEq(True, False)), env) << "\n";
}
static void tst14() {
@ -383,8 +383,8 @@ static void tst18() {
lean_assert(type_of(f(a, a)) == Int);
lean_assert(type_of(f(a)) == Int >> Int);
lean_assert(is_bool(type_of(And(a, f(a)))));
lean_assert(type_of(Fun({a, Int}, iAdd(a, iVal(1)))) == Int >> Int);
lean_assert(type_of(Let({a, iVal(10)}, iAdd(a, b))) == Int);
lean_assert(type_of(Fun({a, Int}, mk_Int_add(a, iVal(1)))) == Int >> Int);
lean_assert(type_of(Let({a, iVal(10)}, mk_Int_add(a, b))) == Int);
lean_assert(type_of(Type()) == Type(level() + 1));
lean_assert(type_of(Bool) == Type());
lean_assert(type_of(Pi({a, Type()}, Type(level() + 2))) == Type(level() + 3));
@ -399,7 +399,7 @@ static expr mk_big(unsigned val, unsigned depth) {
if (depth == 0)
return iVal(val);
else
return iAdd(mk_big(val*2, depth-1), mk_big(val*2 + 1, depth-1));
return mk_Int_add(mk_big(val*2, depth-1), mk_big(val*2 + 1, depth-1));
}
static void tst19() {

View file

@ -22,28 +22,28 @@ static void tst0() {
env->add_var("n", Nat);
expr n = Const("n");
lean_assert_eq(mk_nat_type(), Nat);
lean_assert_eq(norm(nMul(nVal(2), nVal(3))), nVal(6));
lean_assert_eq(norm(nLe(nVal(2), nVal(3))), True);
lean_assert_eq(norm(nLe(nVal(5), nVal(3))), False);
lean_assert_eq(norm(nLe(nVal(2), nVal(3))), True);
lean_assert_eq(norm(nLe(n, nVal(3))), nLe(n, nVal(3)));
lean_assert_eq(norm(mk_Nat_mul(nVal(2), nVal(3))), nVal(6));
lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True);
lean_assert_eq(norm(mk_Nat_le(nVal(5), nVal(3))), False);
lean_assert_eq(norm(mk_Nat_le(nVal(2), nVal(3))), True);
lean_assert_eq(norm(mk_Nat_le(n, nVal(3))), mk_Nat_le(n, nVal(3)));
env->add_var("x", Real);
expr x = Const("x");
lean_assert_eq(mk_real_type(), Real);
lean_assert_eq(norm(rMul(rVal(2), rVal(3))), rVal(6));
lean_assert_eq(norm(rDiv(rVal(2), rVal(0))), rVal(0));
lean_assert_eq(norm(rLe(rVal(2), rVal(3))), True);
lean_assert_eq(norm(rLe(rVal(5), rVal(3))), False);
lean_assert_eq(norm(rLe(rVal(2), rVal(3))), True);
lean_assert_eq(norm(rLe(x, rVal(3))), rLe(x, rVal(3)));
lean_assert_eq(norm(mk_Real_mul(rVal(2), rVal(3))), rVal(6));
lean_assert_eq(norm(mk_Real_div(rVal(2), rVal(0))), rVal(0));
lean_assert_eq(norm(mk_Real_le(rVal(2), rVal(3))), True);
lean_assert_eq(norm(mk_Real_le(rVal(5), rVal(3))), False);
lean_assert_eq(norm(mk_Real_le(rVal(2), rVal(3))), True);
lean_assert_eq(norm(mk_Real_le(x, rVal(3))), mk_Real_le(x, rVal(3)));
env->add_var("i", Int);
expr i = Const("i");
lean_assert_eq(norm(i2r(i)), i2r(i));
lean_assert_eq(norm(i2r(iVal(2))), rVal(2));
lean_assert_eq(norm(mk_int_to_real(i)), mk_int_to_real(i));
lean_assert_eq(norm(mk_int_to_real(iVal(2))), rVal(2));
lean_assert_eq(mk_int_type(), Int);
lean_assert_eq(norm(n2i(n)), n2i(n));
lean_assert_eq(norm(n2i(nVal(2))), iVal(2));
lean_assert_eq(norm(iDiv(iVal(2), iVal(0))), iVal(0));
lean_assert_eq(norm(mk_nat_to_int(n)), mk_nat_to_int(n));
lean_assert_eq(norm(mk_nat_to_int(nVal(2))), iVal(2));
lean_assert_eq(norm(mk_Int_div(iVal(2), iVal(0))), iVal(0));
}
static void tst1() {
@ -58,76 +58,76 @@ static void tst1() {
static void tst2() {
environment env;
init_test_frontend(env);
expr e = iAdd(iVal(10), iVal(30));
expr e = mk_Int_add(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == iVal(40));
std::cout << type_check(mk_int_add_fn(), env) << "\n";
std::cout << type_check(mk_Int_add_fn(), env) << "\n";
lean_assert(type_check(e, env) == Int);
lean_assert(type_check(mk_app(mk_int_add_fn(), iVal(10)), env) == (Int >> Int));
lean_assert(type_check(mk_app(mk_Int_add_fn(), iVal(10)), env) == (Int >> Int));
lean_assert(is_int_value(normalize(e, env)));
expr e2 = Fun("a", Int, iAdd(Const("a"), iAdd(iVal(10), iVal(30))));
expr e2 = Fun("a", Int, mk_Int_add(Const("a"), mk_Int_add(iVal(10), iVal(30))));
std::cout << e2 << " --> " << normalize(e2, env) << "\n";
lean_assert(type_check(e2, env) == mk_arrow(Int, Int));
lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(40))));
lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_add(Const("a"), iVal(40))));
}
static void tst3() {
environment env;
init_test_frontend(env);
expr e = iMul(iVal(10), iVal(30));
expr e = mk_Int_mul(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == iVal(300));
std::cout << type_check(mk_int_mul_fn(), env) << "\n";
std::cout << type_check(mk_Int_mul_fn(), env) << "\n";
lean_assert(type_check(e, env) == Int);
lean_assert(type_check(mk_app(mk_int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int));
lean_assert(type_check(mk_app(mk_Int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int));
lean_assert(is_int_value(normalize(e, env)));
expr e2 = Fun("a", Int, iMul(Const("a"), iMul(iVal(10), iVal(30))));
expr e2 = Fun("a", Int, mk_Int_mul(Const("a"), mk_Int_mul(iVal(10), iVal(30))));
std::cout << e2 << " --> " << normalize(e2, env) << "\n";
lean_assert(type_check(e2, env) == (Int >> Int));
lean_assert(normalize(e2, env) == Fun("a", Int, iMul(Const("a"), iVal(300))));
lean_assert(normalize(e2, env) == Fun("a", Int, mk_Int_mul(Const("a"), iVal(300))));
}
static void tst4() {
environment env;
init_test_frontend(env);
expr e = iSub(iVal(10), iVal(30));
expr e = mk_Int_sub(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
lean_assert(normalize(e, env, context(), true) == iVal(-20));
std::cout << type_check(mk_int_sub_fn(), env) << "\n";
std::cout << type_check(mk_Int_sub_fn(), env) << "\n";
lean_assert(type_check(e, env) == Int);
lean_assert(type_check(mk_app(mk_int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int));
lean_assert(type_check(mk_app(mk_Int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int));
lean_assert(is_int_value(normalize(e, env, context(), true)));
expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30))));
expr e2 = Fun("a", Int, mk_Int_sub(Const("a"), mk_Int_sub(iVal(10), iVal(30))));
std::cout << e2 << " --> " << normalize(e2, env) << "\n";
lean_assert(type_check(e2, env) == (Int >> Int));
lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, iAdd(Const("a"), iVal(20))));
lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, mk_Int_add(Const("a"), iVal(20))));
}
static void tst5() {
environment env;
init_test_frontend(env);
env->add_var(name("a"), Int);
expr e = Eq(iVal(3), iVal(4));
expr e = HEq(iVal(3), iVal(4));
std::cout << e << " --> " << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == False);
lean_assert(normalize(Eq(Const("a"), iVal(3)), env) == Eq(Const("a"), iVal(3)));
lean_assert(normalize(HEq(Const("a"), iVal(3)), env) == HEq(Const("a"), iVal(3)));
}
static void tst6() {
std::cout << "tst6\n";
std::cout << mk_int_add_fn().raw() << "\n";
std::cout << mk_int_add_fn().raw() << "\n";
std::cout << mk_Int_add_fn().raw() << "\n";
std::cout << mk_Int_add_fn().raw() << "\n";
#ifndef __APPLE__
thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_int_add_fn().raw() << "\n"; });
thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_Int_add_fn().raw() << "\n"; });
t1.join();
thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_int_add_fn().raw() << "\n"; });
thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_Int_add_fn().raw() << "\n"; });
t2.join();
#endif
std::cout << mk_int_add_fn().raw() << "\n";
std::cout << mk_Int_add_fn().raw() << "\n";
}
int main() {

View file

@ -18,7 +18,7 @@ static void tst1() {
expr z = Const("z");
local_context lctx{mk_lift(0, 1), mk_inst(0, a)};
expr m = mk_metavar("a", lctx);
expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), Eq(x, m)))));
expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), HEq(x, m)))));
expr G = deep_copy(F);
lean_assert(F == G);
lean_assert(!is_eqp(F, G));

View file

@ -95,7 +95,7 @@ static void tst2() {
expr F = m1(g(m2, m3(a)), m4(nVal(0)));
std::cout << F << "\n";
std::cout << checker.check(F, context(), menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m1, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
@ -138,7 +138,7 @@ static void tst3() {
expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a));
std::cout << F << "\n";
std::cout << checker.check(F, context(), menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m2, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
@ -183,7 +183,7 @@ static void tst4() {
expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b);
std::cout << F << "\n";
std::cout << checker.check(F, context(), menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m3, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
elb.next();
@ -257,10 +257,10 @@ static void tst6() {
env->add_var("f", Int >> (Int >> Int));
env->add_var("a", Int);
env->add_var("b", Int);
env->add_axiom("H1", Eq(f(a, f(a, b)), a));
env->add_axiom("H2", Eq(a, b));
expr V = Subst(m1, m2, m3, m4, H1, H2);
expr expected = Eq(f(a, f(b, b)), a);
env->add_axiom("H1", HEq(f(a, f(a, b)), a));
env->add_axiom("H2", HEq(a, b));
expr V = mk_subst_th(m1, m2, m3, m4, H1, H2);
expr expected = HEq(f(a, f(b, b)), a);
expr given = checker.check(V, context(), menv, ucs);
ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
@ -339,17 +339,17 @@ static void tst8() {
env->add_var("a", Bool);
env->add_var("b", Bool);
env->add_var("c", Bool);
env->add_axiom("H1", Eq(a, b));
env->add_axiom("H2", Eq(b, c));
success(Trans(_, _, _, _, H1, H2), Trans(Bool, a, b, c, H1, H2), env);
success(Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)),
Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1)), env);
success(Symm(_, _, _, Trans(_, _ , _ , _ , Symm(_, _, _, H2), Symm(_, _, _, H1))),
Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), env);
env->add_axiom("H1", HEq(a, b));
env->add_axiom("H2", HEq(b, c));
success(mk_trans_th(_, _, _, _, H1, H2), mk_trans_th(Bool, a, b, c, H1, H2), env);
success(mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)),
mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1)), env);
success(mk_symm_th(_, _, _, mk_trans_th(_, _ , _ , _ , mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))),
mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), env);
env->add_axiom("H3", a);
expr H3 = Const("H3");
success(EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3)),
EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3)),
success(mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3)),
mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3)),
env);
}
@ -370,19 +370,19 @@ static void tst9() {
expr fact = Const("fact");
env->add_var("a", Nat);
env->add_var("b", Nat);
env->add_definition("fact", Bool, Eq(a, b));
env->add_definition("fact", Bool, HEq(a, b));
env->add_axiom("H", fact);
success(Congr2(_, _, _, _, f, H),
Congr2(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env);
success(mk_congr2_th(_, _, _, _, f, H),
mk_congr2_th(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env);
env->add_var("g", Pi({n, Nat}, vec(n) >> Nat));
expr g = Const("g");
env->add_axiom("H2", Eq(f, g));
env->add_axiom("H2", HEq(f, g));
expr H2 = Const("H2");
success(Congr(_, _, _, _, _, _, H2, H),
Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
success(Congr(_, _, _, _, _, _, Refl(_, f), H),
Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, f, a, b, Refl(Pi({n, Nat}, vec(n) >> Nat), f), H), env);
success(Refl(_, a), Refl(Nat, a), env);
success(mk_congr_th(_, _, _, _, _, _, H2, H),
mk_congr_th(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
success(mk_congr_th(_, _, _, _, _, _, mk_refl_th(_, f), H),
mk_congr_th(Nat, Fun({n, Nat}, vec(n) >> Nat), f, f, a, b, mk_refl_th(Pi({n, Nat}, vec(n) >> Nat), f), H), env);
success(mk_refl_th(_, a), mk_refl_th(Nat, a), env);
}
static void tst10() {
@ -402,11 +402,11 @@ static void tst10() {
expr z = Const("z");
success(Fun({{x, _}, {y, _}}, f(x, y)),
Fun({{x, Nat}, {y, R >> Nat}}, f(x, y)), env);
success(Fun({{x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))),
Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env);
success(Fun({{x, _}, {y, _}, {z, _}}, HEq(f(x, y), f(x, z))),
Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, HEq(f(x, y), f(x, z))), env);
expr A = Const("A");
success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))),
Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env);
success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, HEq(f(x, y), f(x, z))),
Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, HEq(f(x, y), f(x, z))), env);
}
static void tst11() {
@ -464,11 +464,11 @@ static void tst13() {
Fun({{A, Type()}, {x, A}}, f(A, x)), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(A, x)),
Fun({{A, Type()}, {B, Type()}, {x, A}}, f(A, x)), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, Eq(f(B, x), f(_, x))),
Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, Eq(f(B, x), f(_, x))),
Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env);
unsolved(Fun({{A, _}, {B, _}, {x, _}}, Eq(f(B, x), f(_, x))), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, HEq(f(B, x), f(_, x))),
Fun({{A, Type()}, {B, Type()}, {x, B}}, HEq(f(B, x), f(B, x))), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, HEq(f(B, x), f(_, x))),
Fun({{A, Type()}, {B, Type()}, {x, B}}, HEq(f(B, x), f(B, x))), env);
unsolved(Fun({{A, _}, {B, _}, {x, _}}, HEq(f(B, x), f(_, x))), env);
}
static void tst14() {
@ -495,20 +495,20 @@ static void tst14() {
env);
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g(_,
Fun({{x, _}, {y, _}}, Eq(f(_, x), f(_, y))),
Fun({{x, _}, {y, _}}, HEq(f(_, x), f(_, y))),
Fun({{x, N}, {y, Bool}}, True))),
Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g((N >> (Bool >> Bool)),
Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))),
Fun({{x, N}, {y, Bool}}, HEq(f(N, x), f(Bool, y))),
Fun({{x, N}, {y, Bool}}, True))), env);
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g(_,
Fun({{x, N}, {y, _}}, Eq(f(_, x), f(_, y))),
Fun({{x, N}, {y, _}}, HEq(f(_, x), f(_, y))),
Fun({{x, _}, {y, Bool}}, True))),
Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g((N >> (Bool >> Bool)),
Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))),
Fun({{x, N}, {y, Bool}}, HEq(f(N, x), f(Bool, y))),
Fun({{x, N}, {y, Bool}}, True))), env);
}
@ -550,29 +550,29 @@ static void tst16() {
env->add_var("a", Bool);
env->add_var("b", Bool);
env->add_var("c", Bool);
success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}},
Trans(_, _, _, _, H1, H2)),
Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}},
Trans(Bool, a, b, c, H1, H2)),
success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}},
mk_trans_th(_, _, _, _, H1, H2)),
Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}},
mk_trans_th(Bool, a, b, c, H1, H2)),
env);
expr H3 = Const("H3");
success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))),
Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))),
success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))),
Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))),
env);
environment env2;
init_test_frontend(env2);
success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))),
success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}},
mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))),
env2);
expr A = Const("A");
success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)))),
Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
Symm(A, c, a, Trans(A, c, b, a, Symm(A, b, c, H2), Symm(A, a, b, H1)))),
success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, HEq(a, b)}, {H2, HEq(b, c)}},
mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)))),
Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, HEq(a, b)}, {H2, HEq(b, c)}},
mk_symm_th(A, c, a, mk_trans_th(A, c, b, a, mk_symm_th(A, b, c, H2), mk_symm_th(A, a, b, H1)))),
env2);
}
@ -682,7 +682,7 @@ void tst21() {
expr b = Const("b");
expr m1 = menv->mk_metavar();
expr l = m1(b, a);
expr r = Fun({x, N}, f(x, Eq(a, b)));
expr r = Fun({x, N}, f(x, HEq(a, b)));
elaborator elb(env, menv, context(), l, r);
while (true) {
try {
@ -715,8 +715,8 @@ void tst22() {
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");
expr l = f(m1(a), iAdd(m3, iAdd(iVal(1), iVal(1))));
expr r = f(m2(b), iAdd(iVal(1), iVal(2)));
expr l = f(m1(a), mk_Int_add(m3, mk_Int_add(iVal(1), iVal(1))));
expr r = f(m2(b), mk_Int_add(iVal(1), iVal(2)));
elaborator elb(env, menv, context(), l, r);
while (true) {
try {
@ -745,8 +745,8 @@ void tst23() {
expr f = Const("f");
expr m1 = menv->mk_metavar();
expr m2 = menv->mk_metavar();
expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1)));
expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x)));
expr l = Fun({{x, N}, {y, N}}, HEq(y, f(x, m1)));
expr r = Fun({{x, N}, {y, N}}, HEq(m2, f(m1, x)));
elaborator elb(env, menv, context(), l, r);
while (true) {
try {
@ -832,13 +832,13 @@ void tst26() {
expr a = Const("a");
env->add_var("a", Type(level()+1));
expr m1 = menv->mk_metavar();
expr F = Eq(g(m1, a), a);
expr F = HEq(g(m1, a), a);
std::cout << F << "\n";
std::cout << checker.check(F, context(), menv, ucs) << "\n";
elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next();
std::cout << s->instantiate_metavars(F) << "\n";
lean_assert_eq(s->instantiate_metavars(F), Eq(g(Type(level()+1), a), a));
lean_assert_eq(s->instantiate_metavars(F), HEq(g(Type(level()+1), a), a));
}
void tst27() {

View file

@ -34,10 +34,10 @@ static void tst1() {
lt(Const("a"), Const("b"), true);
lt(Const("a"), Const("a"), false);
lt(Var(1), Const("a"), true);
lt(Eq(Var(0), Var(1)), Eq(Var(1), Var(1)), true);
lt(Eq(Var(1), Var(0)), Eq(Var(1), Var(1)), true);
lt(Eq(Var(1), Var(1)), Eq(Var(1), Var(1)), false);
lt(Eq(Var(2), Var(1)), Eq(Var(1), Var(1)), false);
lt(HEq(Var(0), Var(1)), HEq(Var(1), Var(1)), true);
lt(HEq(Var(1), Var(0)), HEq(Var(1), Var(1)), true);
lt(HEq(Var(1), Var(1)), HEq(Var(1), Var(1)), false);
lt(HEq(Var(2), Var(1)), HEq(Var(1), Var(1)), false);
lt(Const("f")(Var(0)), Const("f")(Var(0), Const("a")), true);
lt(Const("f")(Var(0), Const("a"), Const("b")), Const("f")(Var(0), Const("a")), false);
lt(Const("f")(Var(0), Const("a")), Const("g")(Var(0), Const("a")), true);

View file

@ -30,13 +30,13 @@ static void tst1() {
expr x = Const("x");
expr y = Const("y");
expr N = Const("N");
expr F = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a)))));
expr F = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(HEq(x, f(y, a)))));
check(fmt(F), "fun x : (Pi x : N, (x#0 -> x#1)), (let y := f a in (f (x#1 == (f y#0 a))))");
check(fmt(env->get_object("N")), "variable N : Type");
context ctx;
ctx = extend(ctx, "x", f(a));
ctx = extend(ctx, "y", f(Var(0), N >> N));
ctx = extend(ctx, "z", N, Eq(Var(0), Var(1)));
ctx = extend(ctx, "z", N, HEq(Var(0), Var(1)));
check(fmt(ctx), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1]");
check(fmt(ctx, f(Var(0), Var(2))), "f z#0 x#2");
check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1] |- f z#0 x#2");

View file

@ -15,10 +15,10 @@ static void tst1() {
max_sharing_fn max_fn;
expr a1 = Const("a");
expr a2 = Const("a");
expr F1 = Eq(a1, a2);
lean_assert(!is_eqp(eq_lhs(F1), eq_rhs(F1)));
expr F1 = HEq(a1, a2);
lean_assert(!is_eqp(heq_lhs(F1), heq_rhs(F1)));
expr F2 = max_fn(F1);
lean_assert(is_eqp(eq_lhs(F2), eq_rhs(F2)));
lean_assert(is_eqp(heq_lhs(F2), heq_rhs(F2)));
expr x = Const("x");
expr y = Const("y");
expr f = Const("f");

View file

@ -273,7 +273,7 @@ static void match_let_tst1() {
static void match_let_tst2() {
cout << "--- match_let_tst2() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l = mk_let("a", Type(), Const("b"), Var(0));
subst_map s;
bool result = test_match(l, t, 0, s);
@ -283,7 +283,7 @@ static void match_let_tst2() {
static void match_let_tst3() {
cout << "--- match_let_tst3() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l1 = mk_let("a", Var(0), Const("b"), Var(0));
expr l2 = mk_let("a", Int, Const("b"), Var(0));
subst_map s;
@ -295,7 +295,7 @@ static void match_let_tst3() {
static void match_let_tst4() {
cout << "--- match_let_tst4() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l1 = mk_let("a", Nat, Const("b"), Var(0));
expr l2 = mk_let("a", Int, Const("b"), Var(0));
subst_map s;
@ -306,7 +306,7 @@ static void match_let_tst4() {
static void match_let_tst5() {
cout << "--- match_let_tst5() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l1 = mk_let("a", Int, Var(3), Var(0));
expr l2 = mk_let("a", Int, Const("b"), Const("b"));
subst_map s;
@ -317,7 +317,7 @@ static void match_let_tst5() {
static void match_let_tst6() {
cout << "--- match_let_tst6() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l1 = mk_let("a", Var(0), Var(1), Var(0));
expr l2 = mk_let("a", Int, Const("b"), Const("b"));
subst_map s;
@ -328,7 +328,7 @@ static void match_let_tst6() {
static void match_let_tst7() {
cout << "--- match_let_tst7() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l1 = mk_let("a", Var(0), Var(1), Var(0));
expr l2 = mk_let("a", Int, Const("b"), Var(0));
subst_map s;
@ -341,7 +341,7 @@ static void match_let_tst7() {
static void match_let_tst8() {
cout << "--- match_let_tst8() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l1 = mk_let("a", Nat, Var(1), Var(0));
expr l2 = mk_let("a", Int, Const("b"), Var(0));
subst_map s;
@ -352,7 +352,7 @@ static void match_let_tst8() {
static void match_let_tst9() {
cout << "--- match_let_tst9() ---" << endl;
expr t = Eq(Const("a"), Const("b"));
expr t = HEq(Const("a"), Const("b"));
expr l1 = mk_let("a", Var(0), Var(0), Var(0));
expr l2 = mk_let("a", Nat, Const("b"), Const("a"));
subst_map s;
@ -367,7 +367,7 @@ static void match_eq_tst1() {
expr f = Const("f");
expr a = Const("a");
subst_map s;
bool result = test_match(mk_eq(x, a), mk_eq(f, a), 0, s);
bool result = test_match(mk_heq(x, a), mk_heq(f, a), 0, s);
lean_assert_eq(result, true);
lean_assert_eq(s.find(0)->second, f);
lean_assert_eq(s.size(), 1);
@ -379,7 +379,7 @@ static void match_eq_tst2() {
expr f = Const("f");
expr a = Const("a");
subst_map s;
bool result = test_match(mk_eq(nAdd(x, a), x), mk_eq(nAdd(f, a), f), 0, s);
bool result = test_match(mk_heq(mk_Nat_add(x, a), x), mk_heq(mk_Nat_add(f, a), f), 0, s);
lean_assert_eq(result, true);
lean_assert_eq(s.find(0)->second, f);
lean_assert_eq(s.size(), 1);
@ -391,7 +391,7 @@ static void match_eq_tst3() {
expr f = Const("f");
expr a = Const("a");
subst_map s;
bool result = test_match(mk_eq(nAdd(x, a), x), f, 0, s);
bool result = test_match(mk_heq(mk_Nat_add(x, a), x), f, 0, s);
lean_assert_eq(result, false);
lean_assert_eq(s.empty(), true);
}

View file

@ -32,11 +32,11 @@ static void theorem_rewriter1_tst() {
// Result : (b + a, ADD_COMM a b)
expr a = Const("a"); // a : Nat
expr b = Const("b"); // b : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env; init_test_frontend(env);
@ -48,13 +48,13 @@ static void theorem_rewriter1_tst() {
rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body);
context ctx;
pair<expr, expr> result = add_comm_thm_rewriter(env, ctx, a_plus_b);
expr concl = mk_eq(a_plus_b, result.first);
expr concl = mk_heq(a_plus_b, result.first);
expr proof = result.second;
cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a));
lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a));
lean_assert_eq(proof, Const("ADD_COMM")(a, b));
env->add_theorem("New_theorem1", concl, proof);
}
@ -66,9 +66,9 @@ static void theorem_rewriter2_tst() {
// Result : (a, ADD_ID a)
expr a = Const("a"); // a : at
expr zero = nVal(0); // zero : Nat
expr a_plus_zero = nAdd(a, zero);
expr a_plus_zero = mk_Nat_add(a, zero);
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -79,13 +79,13 @@ static void theorem_rewriter2_tst() {
rewriter add_id_thm_rewriter = mk_theorem_rewriter(add_id_thm_type, add_id_thm_body);
context ctx;
pair<expr, expr> result = add_id_thm_rewriter(env, ctx, a_plus_zero);
expr concl = mk_eq(a_plus_zero, result.first);
expr concl = mk_heq(a_plus_zero, result.first);
expr proof = result.second;
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(a_plus_zero, a));
lean_assert_eq(concl, mk_heq(a_plus_zero, a));
lean_assert_eq(proof, Const("ADD_ID")(a));
env->add_theorem("New_theorem2", concl, proof);
}
@ -99,14 +99,14 @@ static void then_rewriter1_tst() {
expr a = Const("a"); // a : Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_zero = nAdd(a, zero);
expr zero_plus_a = nAdd(zero, a);
expr a_plus_zero = mk_Nat_add(a, zero);
expr zero_plus_a = mk_Nat_add(zero, a);
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -120,15 +120,15 @@ static void then_rewriter1_tst() {
rewriter then_rewriter1 = mk_then_rewriter(add_comm_thm_rewriter, add_id_thm_rewriter);
context ctx;
pair<expr, expr> result = then_rewriter1(env, ctx, zero_plus_a);
expr concl = mk_eq(zero_plus_a, result.first);
expr concl = mk_heq(zero_plus_a, result.first);
expr proof = result.second;
cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl;
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(zero_plus_a, a));
lean_assert(proof == Trans(Nat, zero_plus_a, a_plus_zero, a,
lean_assert_eq(concl, mk_heq(zero_plus_a, a));
lean_assert(proof == mk_trans_th(Nat, zero_plus_a, a_plus_zero, a,
Const("ADD_COMM")(zero, a), Const("ADD_ID")(a)));
env->add_theorem("New_theorem3", concl, proof);
@ -147,22 +147,22 @@ static void then_rewriter2_tst() {
expr a = Const("a"); // a : Nat
expr zero = nVal(0); // zero : Nat
expr zero_plus_a = nAdd(zero, a);
expr a_plus_zero = nAdd(a, zero);
expr zero_plus_a_plus_zero = nAdd(zero, nAdd(a, zero));
expr zero_plus_a_plus_zero_ = nAdd(nAdd(zero, a), zero);
expr zero_plus_a = mk_Nat_add(zero, a);
expr a_plus_zero = mk_Nat_add(a, zero);
expr zero_plus_a_plus_zero = mk_Nat_add(zero, mk_Nat_add(a, zero));
expr zero_plus_a_plus_zero_ = mk_Nat_add(mk_Nat_add(zero, a), zero);
expr add_assoc_thm_type = Pi("x", Nat,
Pi("y", Nat,
Pi("z", Nat,
Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))),
nAdd(nAdd(Const("x"), Const("y")), Const("z"))))));
HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))),
mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z"))))));
expr add_assoc_thm_body = Const("ADD_ASSOC");
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -181,17 +181,17 @@ static void then_rewriter2_tst() {
add_id_thm_rewriter});
context ctx;
pair<expr, expr> result = then_rewriter2(env, ctx, zero_plus_a_plus_zero);
expr concl = mk_eq(zero_plus_a_plus_zero, result.first);
expr concl = mk_heq(zero_plus_a_plus_zero, result.first);
expr proof = result.second;
cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl;
cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl;
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a));
lean_assert(proof == Trans(Nat, zero_plus_a_plus_zero, a_plus_zero, a,
Trans(Nat, zero_plus_a_plus_zero, zero_plus_a, a_plus_zero,
Trans(Nat, zero_plus_a_plus_zero, zero_plus_a_plus_zero_, zero_plus_a,
lean_assert_eq(concl, mk_heq(zero_plus_a_plus_zero, a));
lean_assert(proof == mk_trans_th(Nat, zero_plus_a_plus_zero, a_plus_zero, a,
mk_trans_th(Nat, zero_plus_a_plus_zero, zero_plus_a, a_plus_zero,
mk_trans_th(Nat, zero_plus_a_plus_zero, zero_plus_a_plus_zero_, zero_plus_a,
Const("ADD_ASSOC")(zero, a, zero), Const("ADD_ID")(zero_plus_a)),
Const("ADD_COMM")(zero, a)),
Const("ADD_ID")(a)));
@ -208,20 +208,20 @@ static void orelse_rewriter1_tst() {
expr a = Const("a"); // a : Nat
expr b = Const("b"); // b : Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_assoc_thm_type = Pi("x", Nat,
Pi("y", Nat,
Pi("z", Nat,
Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))),
nAdd(nAdd(Const("x"), Const("y")), Const("z"))))));
HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))),
mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z"))))));
expr add_assoc_thm_body = Const("ADD_ASSOC");
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -238,7 +238,7 @@ static void orelse_rewriter1_tst() {
add_id_thm_rewriter});
context ctx;
pair<expr, expr> result = add_assoc_or_comm_thm_rewriter(env, ctx, a_plus_b);
expr concl = mk_eq(a_plus_b, result.first);
expr concl = mk_heq(a_plus_b, result.first);
expr proof = result.second;
cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl;
@ -246,7 +246,7 @@ static void orelse_rewriter1_tst() {
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a));
lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a));
lean_assert_eq(proof, Const("ADD_COMM")(a, b));
env->add_theorem("New_theorem5", concl, proof);
}
@ -259,16 +259,16 @@ static void orelse_rewriter2_tst() {
expr a = Const("a"); // a : Nat
expr b = Const("b"); // b : Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_assoc_thm_type = Pi("x", Nat,
Pi("y", Nat,
Pi("z", Nat,
Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))),
nAdd(nAdd(Const("x"), Const("y")), Const("z"))))));
HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))),
mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z"))))));
expr add_assoc_thm_body = Const("ADD_ASSOC");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -304,20 +304,20 @@ static void try_rewriter1_tst() {
expr a = Const("a"); // a : Nat
expr b = Const("b"); // b : Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_assoc_thm_type = Pi("x", Nat,
Pi("y", Nat,
Pi("z", Nat,
Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))),
nAdd(nAdd(Const("x"), Const("y")), Const("z"))))));
HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))),
mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z"))))));
expr add_assoc_thm_body = Const("ADD_ASSOC");
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -333,7 +333,7 @@ static void try_rewriter1_tst() {
add_id_thm_rewriter});
context ctx;
pair<expr, expr> result = add_try_rewriter(env, ctx, a_plus_b);
expr concl = mk_eq(a_plus_b, result.first);
expr concl = mk_heq(a_plus_b, result.first);
expr proof = result.second;
cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl;
@ -341,7 +341,7 @@ static void try_rewriter1_tst() {
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(a_plus_b, a_plus_b));
lean_assert_eq(concl, mk_heq(a_plus_b, a_plus_b));
lean_assert_eq(proof, Const("refl")(Nat, a_plus_b));
env->add_theorem("New_theorem6", concl, proof);
}
@ -355,20 +355,20 @@ static void try_rewriter2_tst() {
expr a = Const("a"); // a : Nat
expr b = Const("b"); // b : Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_assoc_thm_type = Pi("x", Nat,
Pi("y", Nat,
Pi("z", Nat,
Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))),
nAdd(nAdd(Const("x"), Const("y")), Const("z"))))));
HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))),
mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z"))))));
expr add_assoc_thm_body = Const("ADD_ASSOC");
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -385,7 +385,7 @@ static void try_rewriter2_tst() {
add_id_thm_rewriter});
context ctx;
pair<expr, expr> result = add_try_rewriter(env, ctx, a_plus_b);
expr concl = mk_eq(a_plus_b, result.first);
expr concl = mk_heq(a_plus_b, result.first);
expr proof = result.second;
cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl;
@ -393,7 +393,7 @@ static void try_rewriter2_tst() {
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a));
lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a));
lean_assert_eq(proof, Const("ADD_COMM")(a, b));
env->add_theorem("try2", concl, proof);
}
@ -410,11 +410,11 @@ static void app_rewriter1_tst() {
expr f3 = Const("f3"); // f : Nat -> Nat -> Nat -> Nat
expr f4 = Const("f4"); // f : Nat -> Nat -> Nat -> Nat -> Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env; init_test_frontend(env);
@ -436,32 +436,32 @@ static void app_rewriter1_tst() {
expr v = f1(nVal(0));
pair<expr, expr> result = app_try_comm_rewriter(env, ctx, v);
expr concl = mk_eq(v, result.first);
expr concl = mk_heq(v, result.first);
expr proof = result.second;
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, f1(nVal(0))));
lean_assert_eq(proof, Refl(Nat, f1(nVal(0))));
lean_assert_eq(concl, mk_heq(v, f1(nVal(0))));
lean_assert_eq(proof, mk_refl_th(Nat, f1(nVal(0))));
env->add_theorem("app_rewriter1", concl, proof);
cout << "====================================================" << std::endl;
v = f1(a_plus_b);
result = app_try_comm_rewriter(env, ctx, v);
concl = mk_eq(v, result.first);
concl = mk_heq(v, result.first);
proof = result.second;
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, f1(b_plus_a)));
lean_assert_eq(concl, mk_heq(v, f1(b_plus_a)));
lean_assert_eq(proof,
Const("congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b)));
env->add_theorem("app_rewriter2", concl, proof);
cout << "====================================================" << std::endl;
v = f4(nVal(0), a_plus_b, nVal(0), b_plus_a);
result = app_try_comm_rewriter(env, ctx, v);
concl = mk_eq(v, result.first);
concl = mk_heq(v, result.first);
proof = result.second;
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, f4(nVal(0), b_plus_a, nVal(0), a_plus_b)));
lean_assert_eq(concl, mk_heq(v, f4(nVal(0), b_plus_a, nVal(0), a_plus_b)));
// Congr Nat (fun _ : Nat, Nat) (f4 0 (Nat::add a b) 0) (f4 0 (Nat::add b a) 0) (Nat::add b a) (Nat::add a b) (Congr1 Nat (fun _ : Nat, (Nat -> Nat)) (f4 0 (Nat::add a b)) (f4 0 (Nat::add b a)) 0 (Congr2 Nat (fun _ : Nat, (Nat -> Nat -> Nat)) (Nat::add a b) (Nat::add b a) (f4 0) (ADD_COMM a b))) (ADD_COMM b a)
lean_assert_eq(proof,
@ -489,22 +489,22 @@ static void repeat_rewriter1_tst() {
expr a = Const("a"); // a : Nat
expr zero = nVal(0); // zero : Nat
expr zero_plus_a = nAdd(zero, a);
expr a_plus_zero = nAdd(a, zero);
expr zero_plus_a_plus_zero = nAdd(zero, nAdd(a, zero));
expr zero_plus_a_plus_zero_ = nAdd(nAdd(zero, a), zero);
expr zero_plus_a = mk_Nat_add(zero, a);
expr a_plus_zero = mk_Nat_add(a, zero);
expr zero_plus_a_plus_zero = mk_Nat_add(zero, mk_Nat_add(a, zero));
expr zero_plus_a_plus_zero_ = mk_Nat_add(mk_Nat_add(zero, a), zero);
expr add_assoc_thm_type = Pi("x", Nat,
Pi("y", Nat,
Pi("z", Nat,
Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))),
nAdd(nAdd(Const("x"), Const("y")), Const("z"))))));
HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))),
mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z"))))));
expr add_assoc_thm_body = Const("ADD_ASSOC");
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -523,14 +523,14 @@ static void repeat_rewriter1_tst() {
rewriter repeat_rw = mk_repeat_rewriter(or_rewriter);
context ctx;
pair<expr, expr> result = repeat_rw(env, ctx, zero_plus_a_plus_zero);
expr concl = mk_eq(zero_plus_a_plus_zero, result.first);
expr concl = mk_heq(zero_plus_a_plus_zero, result.first);
expr proof = result.second;
cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl;
cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl;
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a));
lean_assert_eq(concl, mk_heq(zero_plus_a_plus_zero, a));
env->add_theorem("repeat_thm1", concl, proof);
}
@ -547,22 +547,22 @@ static void repeat_rewriter2_tst() {
expr a = Const("a"); // a : Nat
expr zero = nVal(0); // zero : Nat
expr zero_plus_a = nAdd(zero, a);
expr a_plus_zero = nAdd(a, zero);
expr zero_plus_a_plus_zero = nAdd(zero, nAdd(a, zero));
expr zero_plus_a_plus_zero_ = nAdd(nAdd(zero, a), zero);
expr zero_plus_a = mk_Nat_add(zero, a);
expr a_plus_zero = mk_Nat_add(a, zero);
expr zero_plus_a_plus_zero = mk_Nat_add(zero, mk_Nat_add(a, zero));
expr zero_plus_a_plus_zero_ = mk_Nat_add(mk_Nat_add(zero, a), zero);
expr add_assoc_thm_type = Pi("x", Nat,
Pi("y", Nat,
Pi("z", Nat,
Eq(nAdd(Const("x"), nAdd(Const("y"), Const("z"))),
nAdd(nAdd(Const("x"), Const("y")), Const("z"))))));
HEq(mk_Nat_add(Const("x"), mk_Nat_add(Const("y"), Const("z"))),
mk_Nat_add(mk_Nat_add(Const("x"), Const("y")), Const("z"))))));
expr add_assoc_thm_body = Const("ADD_ASSOC");
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
expr add_id_thm_type = Pi("x", Nat,
Eq(nAdd(Const("x"), zero), Const("x")));
HEq(mk_Nat_add(Const("x"), zero), Const("x")));
expr add_id_thm_body = Const("ADD_ID");
environment env; init_test_frontend(env);
@ -582,14 +582,14 @@ static void repeat_rewriter2_tst() {
rewriter repeat_rw = mk_repeat_rewriter(try_rw);
context ctx;
pair<expr, expr> result = repeat_rw(env, ctx, zero_plus_a_plus_zero);
expr concl = mk_eq(zero_plus_a_plus_zero, result.first);
expr concl = mk_heq(zero_plus_a_plus_zero, result.first);
expr proof = result.second;
cout << "Theorem: " << add_assoc_thm_type << " := " << add_assoc_thm_body << std::endl;
cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl;
cout << "Theorem: " << add_id_thm_type << " := " << add_id_thm_body << std::endl;
cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a));
lean_assert_eq(concl, mk_heq(zero_plus_a_plus_zero, a));
env->add_theorem("repeat_thm2", concl, proof);
}
@ -605,11 +605,11 @@ static void depth_rewriter1_tst() {
expr f3 = Const("f3"); // f : Nat -> Nat -> Nat -> Nat
expr f4 = Const("f4"); // f : Nat -> Nat -> Nat -> Nat -> Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env; init_test_frontend(env);
@ -629,13 +629,13 @@ static void depth_rewriter1_tst() {
cout << "RW = " << depth_rewriter << std::endl;
expr v = nAdd(f1(nAdd(a, b)), f3(a, b, nAdd(a, b)));
expr v = mk_Nat_add(f1(mk_Nat_add(a, b)), f3(a, b, mk_Nat_add(a, b)));
pair<expr, expr> result = depth_rewriter(env, ctx, v);
expr concl = mk_eq(v, result.first);
expr concl = mk_heq(v, result.first);
expr proof = result.second;
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, nAdd(f3(a, b, nAdd(b, a)), f1(nAdd(b, a)))));
lean_assert_eq(concl, mk_heq(v, mk_Nat_add(f3(a, b, mk_Nat_add(b, a)), f1(mk_Nat_add(b, a)))));
env->add_theorem("depth_rewriter1", concl, proof);
cout << "====================================================" << std::endl;
}
@ -652,11 +652,11 @@ static void lambda_body_rewriter_tst() {
expr f3 = Const("f3"); // f : Nat -> Nat -> Nat -> Nat
expr f4 = Const("f4"); // f : Nat -> Nat -> Nat -> Nat -> Nat
expr zero = nVal(0); // zero : Nat
expr a_plus_b = nAdd(a, b);
expr b_plus_a = nAdd(b, a);
expr a_plus_b = mk_Nat_add(a, b);
expr b_plus_a = mk_Nat_add(b, a);
expr add_comm_thm_type = Pi("x", Nat,
Pi("y", Nat,
Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
environment env; init_test_frontend(env);
@ -673,27 +673,27 @@ static void lambda_body_rewriter_tst() {
rewriter lambda_rewriter = mk_lambda_body_rewriter(add_comm_thm_rewriter);
context ctx;
cout << "RW = " << lambda_rewriter << std::endl;
expr v = mk_lambda("x", Nat, nAdd(b, a));
expr v = mk_lambda("x", Nat, mk_Nat_add(b, a));
pair<expr, expr> result = lambda_rewriter(env, ctx, v);
expr concl = mk_eq(v, result.first);
expr concl = mk_heq(v, result.first);
expr proof = result.second;
cout << "v = " << v << std::endl;
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, b))));
lean_assert_eq(concl, mk_heq(v, mk_lambda("x", Nat, mk_Nat_add(a, b))));
env->add_theorem("lambda_rewriter1", concl, proof);
// Theorem: Pi(x y : N), x + y = y + x := ADD_COMM x y
// Term : fun (x : Nat), (x + a)
// Result : fun (x : Nat), (a + x)
v = mk_lambda("x", Nat, nAdd(Var(0), a));
v = mk_lambda("x", Nat, mk_Nat_add(Var(0), a));
result = lambda_rewriter(env, ctx, v);
concl = mk_eq(v, result.first);
concl = mk_heq(v, result.first);
proof = result.second;
cout << "v = " << v << std::endl;
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, Var(0)))));
lean_assert_eq(concl, mk_heq(v, mk_lambda("x", Nat, mk_Nat_add(a, Var(0)))));
env->add_theorem("lambda_rewriter2", concl, proof);
cout << "====================================================" << std::endl;
}
@ -711,7 +711,7 @@ static void lambda_type_rewriter_tst() {
env->add_var("b", Nat);
expr vec = Const("vec");
env->add_var("vec", Type() >> (Nat >> Type())); // vec : Type -> Nat -> Type
expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, Eq(nAdd(Const("x"), Const("y")), nAdd(Const("y"), Const("x")))));
expr add_comm_thm_type = Pi("x", Nat, Pi("y", Nat, HEq(mk_Nat_add(Const("x"), Const("y")), mk_Nat_add(Const("y"), Const("x")))));
expr add_comm_thm_body = Const("ADD_COMM");
env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z
rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body);
@ -719,14 +719,14 @@ static void lambda_type_rewriter_tst() {
rewriter depth_rewriter = mk_depth_rewriter(try_rewriter);
rewriter lambda_rewriter = mk_lambda_type_rewriter(depth_rewriter);
expr v = mk_lambda("x", vec(Nat, nAdd(a, b)), Var(0));
expr v = mk_lambda("x", vec(Nat, mk_Nat_add(a, b)), Var(0));
pair<expr, expr> result = lambda_rewriter(env, ctx, v);
expr concl = mk_eq(v, result.first);
expr concl = mk_heq(v, result.first);
expr proof = result.second;
cout << "v = " << v << std::endl;
cout << "Concl = " << concl << std::endl
<< "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, mk_lambda("x", vec(Nat, nAdd(b, a)), Var(0))));
lean_assert_eq(concl, mk_heq(v, mk_lambda("x", vec(Nat, mk_Nat_add(b, a)), Var(0))));
env->add_theorem("lambda_type_rewriter", concl, proof);
cout << "====================================================" << std::endl;
}

View file

@ -12,11 +12,11 @@ using namespace lean;
static void tst1() {
expr a = Const("a");
expr b = Const("b");
expr eq1 = Eq(a, b);
expr eq2 = update_eq(eq1, a, a);
expr eq3 = update_eq(eq1, a, b);
lean_assert(eq_lhs(eq3) == a);
lean_assert(eq_rhs(eq3) == b);
expr eq1 = HEq(a, b);
expr eq2 = update_heq(eq1, a, a);
expr eq3 = update_heq(eq1, a, b);
lean_assert(heq_lhs(eq3) == a);
lean_assert(heq_rhs(eq3) == b);
lean_assert(is_eqp(eq1, eq3));
}

View file

@ -26,8 +26,8 @@ local ok, msg = pcall(function() child:add_definition("val3", Const("Int"), Cons
assert(not ok)
print(msg)
assert(child:normalize(Const("val2")) == Const("val2"))
child:add_theorem("Th1", Eq(iVal(0), iVal(0)), Const("trivial"))
child:add_axiom("H1", Eq(Const("x"), iVal(0)))
child:add_theorem("Th1", HEq(iVal(0), iVal(0)), Const("trivial"))
child:add_axiom("H1", HEq(Const("x"), iVal(0)))
assert(child:has_object("H1"))
local ctx = context(context(), "x", Const("Int"), iVal(10))
assert(child:normalize(Var(0), ctx) == iVal(10))

View file

@ -1,9 +1,9 @@
e = context_entry("a", Const("a"))
n = e:get_body()
check_error(function() mk_eq(n, Const("a")) end)
check_error(function() mk_heq(n, Const("a")) end)
print(Const("a") < Const("b"))
check_error(function() mk_app(Const("a")) end)
print(mk_eq(Const("a"), Const("b")))
print(mk_heq(Const("a"), Const("b")))
print(mk_pi("x", Const("N"), Var(0)))
print(Pi("x", Const("N"), Const("x")))
assert(mk_pi("x", Const("N"), Var(0)) == Pi("x", Const("N"), Const("x")))

View file

@ -22,7 +22,7 @@ function print_leaves(e, ctx)
print("abstraction var name: " .. tostring(name))
print_leaves(domain, ctx)
print_leaves(body, ctx:extend(name, domain))
elseif k == expr_kind.Eq then
elseif k == expr_kind.HEq then
local lhs, rhs = e:fields()
print_leaves(lhs, ctx)
print_leaves(rhs, ctx)
@ -43,6 +43,6 @@ local x, y, z = Consts("x, y, z")
assert(is_expr(f))
local F = fun(h, mk_arrow(N, N),
Let(x, h(a), Eq(f(x), h(x))))
Let(x, h(a), HEq(f(x), h(x))))
print(F)
print_leaves(F, context())

View file

@ -25,7 +25,7 @@ assert(mk_metavar("M"):is_metavar())
assert(mk_real_value(mpq(10)):is_value())
assert(not F:has_metavar())
assert(f(mk_metavar("M")):has_metavar())
assert(Eq(a, b):is_eq())
assert(HEq(a, b):is_heq())
assert(F:num_args() == 3)
assert(F:arg(0) == f)
assert(F:arg(1) == g(x, a))

View file

@ -16,7 +16,7 @@ function must_unify(t1, t2)
assert(s:apply(t1) == s:apply(t2))
end
Bool = Const("Bool")
must_unify(Eq(a, m1), Eq(m2, m2))
must_unify(HEq(a, m1), HEq(m2, m2))
must_unify(Type(), m1)
must_unify(fun(x, Bool, x), fun(x, Bool, m1))
must_unify(Pi(x, Bool, x), Pi(x, Bool, m1))