diff --git a/doc/lean/expr.md b/doc/lean/expr.md index 905353c7e..94922e781 100644 --- a/doc/lean/expr.md +++ b/doc/lean/expr.md @@ -57,49 +57,3 @@ definition inc (x : Nat) : Nat := x + 1 eval inc (inc (inc 2)) eval max (inc 2) 2 = 3 ``` - -## Heterogeneous equality - -For technical reasons, in Lean, we have heterogenous and homogeneous equality. In a nutshell, heterogenous is mainly used internally, and -homogeneous are used externally when writing programs and specifications in Lean. -Heterogenous equality allows us to compare elements of any type, and homogenous equality is just a definition on top of the heterogenous equality that expects arguments of the same type. -The expression `t == s` is a heterogenous equality that is true iff `t` and `s` have the same interpretation. -In the following example, we evaluate the expressions `1 == 2` and `2 == 2`. The first evaluates to `false` and the second to `true`. - -```lean -eval 1 == 2 -eval 2 == 2 -``` - -Since we can compare elements of different types, the following -expression is type correct, but Lean normalizer/evaluator will *not* -reduce it. - -```lean -eval 2 == true -``` - -We strongly discourage users from directly using heterogeneous equality. The main problem is that it is very easy to -write nonsensical expressions like the one above. The expression `t = s` is a homogeneous equality. -It expects `t` and `s` to have the same type. Thus, the expression `2 = true` is type incorrect in Lean. -The symbol `=` is just notation. Internally, homogeneous equality is defined as: - -``` -definition eq {A : (Type U)} (x y : A) : Bool := x == y -infix 50 = : eq -``` - -The curly braces indicate that the first argument of `eq` is implicit. The symbol `=` is just a syntax sugar for `eq`. -In the following example, we use the `set_option` command to force Lean to display implicit arguments and -disable notation when pretty printing expressions. - -```lean -set_option pp::implicit true -set_option pp::notation false -check 1 = 2 - --- restore default configuration -set_option pp::implicit false -set_option pp::notation true -check 1 = 2 -``` diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 16dd5d3e3..56d2f1a90 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -93,7 +93,7 @@ add_theory("if_then_else.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") 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") +## add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") update_interface("kernel.olean" "kernel" "-n") update_interface("Nat.olean" "library/arith" "-n") diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index a524307ce..688ead72c 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -1,34 +1,39 @@ import macros -universe U ≥ 1 +universe U ≥ 1 +universe U' >= U + 1 variable Bool : Type -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions builtin true : Bool builtin false : Bool -definition TypeU := (Type U) +definition TypeU := (Type U) +definition TypeU' := (Type U') + +builtin eq {A : (Type U')} (a b : A) : Bool +infix 50 = : eq definition not (a : Bool) := a → false notation 40 ¬ _ : not definition or (a b : Bool) := ¬ a → b - infixr 30 || : or infixr 30 \/ : or infixr 30 ∨ : or definition and (a b : Bool) := ¬ (a → ¬ b) - infixr 35 && : and infixr 35 /\ : and infixr 35 ∧ : and +definition neq {A : TypeU} (a b : A) := ¬ (a = b) +infix 50 ≠ : neq + definition implies (a b : Bool) := a → b -definition iff (a b : Bool) := a == b - +definition iff (a b : Bool) := a = b infixr 25 <-> : iff infixr 25 ↔ : iff @@ -42,38 +47,30 @@ infixr 25 ↔ : iff -- want to treat exists as a constant. definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x : A, ¬ (P x)) -definition eq {A : TypeU} (a b : A) := a == b - -infix 50 = : eq - -definition neq {A : TypeU} (a b : A) := ¬ (a = b) - -infix 50 ≠ : neq - theorem em (a : Bool) : a ∨ ¬ a := assume Hna : ¬ a, Hna axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a -axiom refl {A : TypeU} (a : A) : a = a +axiom refl {A : TypeU'} (a : A) : a = a -axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b +axiom subst {A : TypeU'} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b -- Function extensionality -axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x == g x) : f == g +axiom funext {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g -- Forall extensionality -axiom allext {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x) +axiom allext {A : TypeU} {B C : A → Bool} (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 -theorem 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 -- We will mark not as opaque later theorem not_intro {a : Bool} (H : a → false) : ¬ a := H -theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f +theorem eta {A : TypeU'} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f := funext (λ x : A, refl (f x)) theorem trivial : true @@ -157,10 +154,10 @@ theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c theorem refute {a : Bool} (H : ¬ a → false) : a := or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1)) -theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a +theorem symm {A : TypeU'} {a b : A} (H : a = b) : b = a := subst (refl a) H -theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c +theorem trans {A : TypeU'} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H1 H2 infixl 100 ⋈ : trans @@ -174,39 +171,20 @@ theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := subst H1 H2 -theorem heq_congr {A : TypeU} {a b c d : A} (H1 : a == c) (H2 : b == d) : (a == b) = (c == d) -:= calc (a == b) = (c == b) : { H1 } - ... = (c == d) : { H2 } - -theorem heq_congrl {A : TypeU} {a : A} (b : A) {c : A} (H : a == c) : (a == b) = (c == b) -:= heq_congr H (refl b) - -theorem heq_congrr {A : TypeU} (a : A) {b d : A} (H : b == d) : (a == b) = (a == d) -:= heq_congr (refl a) H - theorem eqt_elim {a : Bool} (H : a = true) : a := (symm H) ◂ trivial theorem eqf_elim {a : Bool} (H : a = false) : ¬ a := not_intro (λ Ha : a, H ◂ Ha) -theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a +theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a := substp (fun h : (∀ x : A, B x), f a = h a) (refl (f a)) H --- We must use heterogenous equality in this theorem because (f a) : (B a) and (f b) : (B b) -theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H : a = b) : f a == f b -:= substp (fun x : A, f a == f x) (refl (f a)) H - -theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f = g) (H2 : a = b) : f a == g b -:= subst (congr2 f H2) (congr1 b H1) - --- Simpler version of congr2 theorem for arrows (i.e., non-dependent types) -theorem scongr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b +theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b := substp (fun x : A, f a = f x) (refl (f a)) H --- Simpler version of congr theorem for arrows (i.e., non-dependent types) -theorem scongr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b -:= subst (scongr2 f H2) (congr1 b H1) +theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b +:= subst (congr2 f H2) (congr1 b H1) -- Recall that exists is defined as ¬ ∀ x : A, ¬ P x theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B @@ -241,7 +219,7 @@ theorem eqf_intro {a : Bool} (H : ¬ a) : a = false theorem neq_elim {A : TypeU} {a b : A} (H : a ≠ b) : a = b ↔ false := eqf_intro H -theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a +theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a) := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a)) (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b)) @@ -490,7 +468,7 @@ theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : a ∧ b ↔ c ∧ d := and_congrr (λ H, H_ac) H_bd -theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) ↔ p ∨ ∀ x, φ x +theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, p ∨ φ x) = (p ∨ ∀ x, φ x) := boolext (assume H : (∀ x, p ∨ φ x), or_elim (em p) @@ -503,10 +481,10 @@ theorem forall_or_distributer {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, (λ H1 : p, or_introl H1 (φ x)) (λ H2 : (∀ x, φ x), or_intror p (H2 x))) -theorem forall_or_distributel {A : TypeU} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) ↔ (∀ x, φ x) ∨ p +theorem forall_or_distributel {A : Type} (p : Bool) (φ : A → Bool) : (∀ x, φ x ∨ p) = ((∀ x, φ x) ∨ p) := calc (∀ x, φ x ∨ p) = (∀ x, p ∨ φ x) : allext (λ x, or_comm (φ x) p) - ... = (p ∨ ∀ x, φ x) : forall_or_distributer p φ - ... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x) + ... = (p ∨ ∀ x, φ x) : forall_or_distributer p φ + ... = ((∀ x, φ x) ∨ p) : or_comm p (∀ x, φ x) theorem forall_and_distribute {A : TypeU} (φ ψ : A → Bool) : (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x) := boolext diff --git a/src/builtin/name_conv.lua b/src/builtin/name_conv.lua index d287e7035..3a31c7e29 100644 --- a/src/builtin/name_conv.lua +++ b/src/builtin/name_conv.lua @@ -1,4 +1,8 @@ -- Output a C++ statement that creates the given name +function sanitize(s) + s, _ = string.gsub(s, "'", "_") + return s +end function name_to_cpp_expr(n) function rec(n) if not n:is_atomic() then @@ -6,7 +10,8 @@ function name_to_cpp_expr(n) io.write(", ") end if n:is_string() then - io.write("\"" .. n:get_string() .. "\"") + local s = n:get_string() + io.write("\"" .. sanitize(s) .. "\"") else error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n)) end @@ -31,7 +36,8 @@ function name_to_cpp_decl(n) io.write("_") end if n:is_string() then - io.write(n:get_string()) + local s = n:get_string() + io.write(sanitize(s)) else error("numeral hierarchical names are not supported in the C++ interface: " .. tostring(n)) end diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 7fe8f45c5..5541edf69 100644 Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ diff --git a/src/builtin/obj/if_then_else.olean b/src/builtin/obj/if_then_else.olean index 46188ccf4..c085ab55a 100644 Binary files a/src/builtin/obj/if_then_else.olean and b/src/builtin/obj/if_then_else.olean differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index b8ea3249b..319707dc5 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/frontends/lean/notation.h b/src/frontends/lean/notation.h index 6c3cd0f82..d057ff76b 100644 --- a/src/frontends/lean/notation.h +++ b/src/frontends/lean/notation.h @@ -7,7 +7,6 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -constexpr unsigned g_eq_precedence = 50; constexpr unsigned g_arrow_precedence = 25; constexpr unsigned g_app_precedence = std::numeric_limits::max(); } diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index b54a919de..2419f6d25 100644 --- a/src/frontends/lean/parser_calc.cpp +++ b/src/frontends/lean/parser_calc.cpp @@ -44,10 +44,18 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans m_trans_ops.emplace_front(op1, op2, d); } +static expr get_value_op(expr const & op) { + if (is_value(op)) + return mk_constant(to_value(op).get_name()); + else + return op; +} + + calc_proof_parser::calc_proof_parser() { - expr imp = mk_implies_fn(); - expr eq = mk_eq_fn(); - expr neq = mk_neq_fn(); + expr imp = get_value_op(mk_implies_fn()); + expr eq = get_value_op(mk_eq_fn()); + expr neq = get_value_op(mk_neq_fn()); add_supported_operator(op_data(imp, 2)); add_supported_operator(op_data(eq, 3)); diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index aae8a19c0..e7ebd38cd 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -563,14 +563,6 @@ expr parser_imp::parse_led_id(expr const & left) { } } -/** \brief Parse expr '=' expr. */ -expr parser_imp::parse_heq(expr const & left) { - auto p = pos(); - next(); - expr right = parse_expr(g_eq_precedence); - return save(mk_heq(left, right), p); -} - /** \brief Parse expr '->' expr. */ expr parser_imp::parse_arrow(expr const & left) { auto p = pos(); @@ -949,7 +941,6 @@ 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_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()); @@ -979,7 +970,6 @@ unsigned parser_imp::curr_lbp() { return g_app_precedence; } } - case scanner::token::Eq : return g_eq_precedence; case scanner::token::Arrow : return g_arrow_precedence; case scanner::token::LeftParen: case scanner::token::IntVal: case scanner::token::DecimalVal: case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder: diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h index f3f7b714b..14d8e3b70 100644 --- a/src/frontends/lean/parser_imp.h +++ b/src/frontends/lean/parser_imp.h @@ -291,7 +291,6 @@ 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_heq(expr const & left); expr parse_arrow(expr const & left); expr parse_lparen(); void parse_names(buffer> & result); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index ef09849cf..d625cbf70 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -64,7 +64,6 @@ Author: Leonardo de Moura namespace lean { static format g_Type_fmt = highlight_builtin(format("Type")); -static format g_eq_fmt = format("=="); static format g_lambda_n_fmt = highlight_keyword(format("\u03BB")); static format g_Pi_n_fmt = highlight_keyword(format("\u2200")); static format g_lambda_fmt = highlight_keyword(format("fun")); @@ -234,7 +233,7 @@ class pp_fn { return is_atomic(arg(e, 1)); else return false; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::HEq: case expr_kind::Let: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: return false; } return false; @@ -441,8 +440,6 @@ class pp_fn { operator_info op = get_operator(e); if (op) { return op.get_precedence(); - } else if (is_heq(e)) { - return g_eq_precedence; } else if (is_arrow(e)) { return g_arrow_precedence; } else if (is_lambda(e) || is_pi(e) || is_let(e) || is_exists(e)) { @@ -459,8 +456,6 @@ class pp_fn { operator_info op = get_operator(e); if (op) { return op.get_fixity() == fx; - } else if (is_heq(e)) { - return fixity::Infix == fx; } else if (is_arrow(e)) { return fixity::Infixr == fx; } else { @@ -1021,28 +1016,6 @@ class pp_fn { return mk_pair(group(r_format), r_weight); } - /** \brief Pretty print the child of an equality. */ - result pp_heq_child(expr const & e, unsigned depth) { - if (is_atomic(e)) { - return pp(e, depth + 1); - } else { - if (g_eq_precedence < get_operator_precedence(e)) - return pp(e, depth + 1); - else - return pp_child_with_paren(e, depth); - } - } - - /** \brief Pretty print an equality */ - result pp_heq(expr const & e, unsigned depth) { - result p_arg1, p_arg2; - format r_format; - 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); - } - result pp_choice(expr const & e, unsigned depth) { lean_assert(is_choice(e)); unsigned num = get_num_choices(e); @@ -1121,7 +1094,6 @@ 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::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; } diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 16a3bacc3..e5f552051 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -22,7 +22,6 @@ static name g_pi_name("forall"); static name g_let_name("let"); static name g_in_name("in"); static name g_arrow_name("->"); -static name g_eq_name("=="); static name g_exists_name("exists"); static name g_Exists_name("Exists"); static name g_exists_unicode("\u2203"); @@ -237,8 +236,6 @@ scanner::token scanner::read_b_symbol(char prev) { m_name_val = name(m_buffer.c_str()); if (m_name_val == g_arrow_name) return token::Arrow; - else if (m_name_val == g_eq_name) - return token::Eq; else return token::Id; } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 2d66bc6c7..b9be760b2 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -141,17 +141,6 @@ expr mk_app(unsigned n, expr const * as) { to_app(r)->m_hash = hash_args(new_n, m_args); return r; } -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_heq::~expr_heq() {} -void expr_heq::dealloc(buffer & todelete) { - dec_ref(m_rhs, todelete); - dec_ref(m_lhs, todelete); - delete(this); -} expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b): expr_cell(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar()), m_name(n), @@ -245,7 +234,6 @@ void expr_cell::dealloc() { case expr_kind::MetaVar: delete static_cast(it); break; case expr_kind::Type: delete static_cast(it); break; case expr_kind::Constant: static_cast(it)->dealloc(todo); break; - case expr_kind::HEq: static_cast(it)->dealloc(todo); break; case expr_kind::App: static_cast(it)->dealloc(todo); break; case expr_kind::Lambda: static_cast(it)->dealloc(todo); break; case expr_kind::Pi: static_cast(it)->dealloc(todo); break; @@ -285,7 +273,6 @@ expr copy(expr const & a) { case expr_kind::Type: return mk_type(ty_level(a)); case expr_kind::Value: return mk_value(static_cast(a.raw())->m_val); case expr_kind::App: return mk_app(num_args(a), begin_args(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)); @@ -330,7 +317,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(k) && static_cast(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::HEq) && + is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) && is_small(expr_kind::Let) && is_small(expr_kind::MetaVar), "expr_kind is too big"); class expr_serializer : public object_serializer { @@ -373,7 +360,6 @@ class expr_serializer : public object_serializer const & t); friend expr mk_value(value & v); friend expr mk_app(unsigned num_args, expr const * args); - 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); @@ -213,18 +211,6 @@ public: expr const * begin_args() const { return m_args; } expr const * end_args() const { return m_args + m_num_args; } }; -/** \brief Heterogeneous equality */ -class expr_heq : public expr_cell { - expr m_lhs; - expr m_rhs; - friend class expr_cell; - void dealloc(buffer & todelete); -public: - 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; } -}; /** \brief Super class for lambda abstraction and pi (functional spaces). */ class expr_abstraction : public expr_cell { name m_name; @@ -391,7 +377,6 @@ 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_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; } @@ -403,7 +388,6 @@ 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_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); @@ -430,8 +414,6 @@ 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_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"; } @@ -463,7 +445,6 @@ 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(e); } inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast(e); } inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast(e); } -inline expr_heq * to_heq(expr_cell * e) { lean_assert(is_heq(e)); return static_cast(e); } inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast(e); } inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda(e)); return static_cast(e); } inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast(e); } @@ -474,7 +455,6 @@ 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_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()); } @@ -496,8 +476,6 @@ inline optional 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(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 & 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(); } @@ -529,8 +507,6 @@ 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 & 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(); } @@ -650,18 +626,6 @@ template expr update_let(expr const & e, F f) { else return e; } -template expr update_heq(expr const & e, F f) { - static_assert(std::is_same::type, - std::pair>::value, - "update_heq: return type of f is not pair"); - expr const & old_l = heq_lhs(e); - expr const & old_r = heq_rhs(e); - std::pair p = f(old_l, old_r); - if (!is_eqp(p.first, old_l) || !is_eqp(p.second, old_r)) - return mk_heq(p.first, p.second); - else - return e; -} template expr update_metavar(expr const & e, name const & n, F f) { static_assert(std::is_same::type, local_entry>::value, "update_metavar: return type of f(local_entry) is not local_entry"); diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index 87259e256..84cde041c 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -64,7 +64,6 @@ class expr_eq_fn { if (!apply(arg(a, i), arg(b, i))) return false; return true; - 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); diff --git a/src/kernel/for_each_fn.h b/src/kernel/for_each_fn.h index 37ebad1ac..c95e947f5 100644 --- a/src/kernel/for_each_fn.h +++ b/src/kernel/for_each_fn.h @@ -85,10 +85,6 @@ class for_each_fn { } goto begin_loop; } - 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: todo.emplace_back(abst_body(e), offset + 1); diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 55d049865..5a791eac5 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -40,7 +40,7 @@ protected: return true; case expr_kind::Var: return var_idx(e) >= offset; - case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: + case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: break; } @@ -78,9 +78,6 @@ 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::HEq: - result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset); - break; case expr_kind::Lambda: case expr_kind::Pi: result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1); @@ -170,7 +167,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::HEq: + case expr_kind::MetaVar: case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: break; } @@ -203,9 +200,6 @@ class free_var_range_fn { for (auto const & c : args(e)) result = std::max(result, apply(c)); break; - case expr_kind::HEq: - result = std::max(apply(heq_lhs(e)), apply(heq_rhs(e))); - break; case expr_kind::Lambda: case expr_kind::Pi: result = std::max(apply(abst_domain(e)), dec(apply(abst_body(e)))); @@ -287,7 +281,7 @@ protected: return true; // assume that any free variable can occur in the metavariable case expr_kind::Var: return in_interval(var_idx(e), offset); - case expr_kind::App: case expr_kind::HEq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: + case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: break; } @@ -326,9 +320,6 @@ 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::HEq: - result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset); - break; case expr_kind::Lambda: case expr_kind::Pi: result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1); diff --git a/src/kernel/kernel.cpp b/src/kernel/kernel.cpp index af14c71dd..cabbb071a 100644 --- a/src/kernel/kernel.cpp +++ b/src/kernel/kernel.cpp @@ -16,6 +16,8 @@ namespace lean { // Bultin universe variables m and u static level u_lvl(name("U")); expr const TypeU = Type(u_lvl); +static level up_lvl(name("U'")); +expr const TypeUp = Type(up_lvl); // ======================================= // ======================================= @@ -78,6 +80,42 @@ bool is_false(expr const & e) { } // ======================================= +// ======================================= +// Equality +static name g_eq_name("eq"); +static format g_eq_fmt(g_eq_name); +/** + \brief Semantic attachment for if-then-else operator with type + Pi (A : Type), Bool -> A -> A -> A +*/ +class eq_fn_value : public value { + expr m_type; + static expr mk_type() { + expr A = Const("A"); + // Pi (A: TypeUp), A -> A -> Bool + return Pi({A, TypeUp}, (A >> (A >> Bool))); + } +public: + eq_fn_value():m_type(mk_type()) {} + virtual ~eq_fn_value() {} + virtual expr get_type() const { return m_type; } + virtual name get_name() const { return g_eq_name; } + virtual optional normalize(unsigned num_args, expr const * args) const { + if (num_args == 4 && is_value(args[2]) && is_value(args[3]) && typeid(to_value(args[2])) == typeid(to_value(args[3]))) { + return some_expr(mk_bool_value(args[2] == args[3])); + } else { + return none_expr(); + } + } + virtual void write(serializer & s) const { s << "eq"; } +}; +MK_BUILTIN(eq_fn, eq_fn_value); +MK_IS_BUILTIN(is_eq_fn, mk_eq_fn()); +static register_builtin_fn eq_blt("eq", []() { return mk_eq_fn(); }); +static value::register_deserializer_fn eq_ds("eq", [](deserializer & ) { return mk_eq_fn(); }); +// ======================================= + + void import_kernel(environment const & env, io_state const & ios) { env->import("kernel", ios); } diff --git a/src/kernel/kernel.h b/src/kernel/kernel.h index c7113bec0..fe9dba7c3 100644 --- a/src/kernel/kernel.h +++ b/src/kernel/kernel.h @@ -11,6 +11,7 @@ Author: Leonardo de Moura namespace lean { // See src/builtin/kernel.lean for signatures. extern expr const TypeU; +extern expr const TypeUp; /** \brief Return the Lean Boolean type. */ expr mk_bool_type(); @@ -33,6 +34,11 @@ 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_eq_fn(); +bool is_eq_fn(expr const & e); +inline expr mk_eq(expr const & A, expr const & lhs, expr const & rhs) { return mk_app(mk_eq_fn(), A, lhs, rhs); } +inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)); } + inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); } inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); } inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); } diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 046b726ff..225c577a1 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -8,14 +8,14 @@ Released under Apache 2.0 license as described in the file LICENSE. namespace lean { MK_CONSTANT(Bool, name("Bool")); MK_CONSTANT(TypeU, name("TypeU")); +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(neq_fn, name("neq")); MK_CONSTANT(implies_fn, name("implies")); MK_CONSTANT(iff_fn, name("iff")); 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")); @@ -53,16 +53,11 @@ 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(heq_congr_fn, name("heq_congr")); -MK_CONSTANT(heq_congrl_fn, name("heq_congrl")); -MK_CONSTANT(heq_congrr_fn, name("heq_congrr")); MK_CONSTANT(eqt_elim_fn, name("eqt_elim")); MK_CONSTANT(eqf_elim_fn, name("eqf_elim")); MK_CONSTANT(congr1_fn, name("congr1")); MK_CONSTANT(congr2_fn, name("congr2")); MK_CONSTANT(congr_fn, name("congr")); -MK_CONSTANT(scongr2_fn, name("scongr2")); -MK_CONSTANT(scongr_fn, name("scongr")); MK_CONSTANT(exists_elim_fn, name("exists_elim")); MK_CONSTANT(exists_intro_fn, name("exists_intro")); MK_CONSTANT(boolext_fn, name("boolext")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 3190b0c7a..034acbbd8 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -9,6 +9,8 @@ expr mk_Bool(); bool is_Bool(expr const & e); expr mk_TypeU(); bool is_TypeU(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)); } @@ -21,6 +23,10 @@ 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_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_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)); } @@ -33,14 +39,6 @@ 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}); } @@ -151,15 +149,6 @@ inline expr mk_eq_ne_trans_th(expr const & e1, expr const & e2, expr const & e3, 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_heq_congr_fn(); -bool is_heq_congr_fn(expr const & e); -inline expr mk_heq_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_heq_congr_fn(), e1, e2, e3, e4, e5, e6, e7}); } -expr mk_heq_congrl_fn(); -bool is_heq_congrl_fn(expr const & e); -inline expr mk_heq_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrl_fn(), e1, e2, e3, e4, e5}); } -expr mk_heq_congrr_fn(); -bool is_heq_congrr_fn(expr const & e); -inline expr mk_heq_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_heq_congrr_fn(), e1, e2, e3, e4, e5}); } 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}); } @@ -175,12 +164,6 @@ inline expr mk_congr2_th(expr const & e1, expr const & e2, expr const & e3, expr 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_scongr2_fn(); -bool is_scongr2_fn(expr const & e); -inline expr mk_scongr2_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_scongr2_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_scongr_fn(); -bool is_scongr_fn(expr const & e); -inline expr mk_scongr_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_scongr_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}); } diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index cbe3de1f2..98c618255 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -56,11 +56,6 @@ struct max_sharing_fn::imp { cache(r); return 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; - } case expr_kind::Lambda: case expr_kind::Pi: { expr r = update_abst(a, [=](expr const & t, expr const & b) { return std::make_pair(apply(t), apply(b)); }); diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index b1652d53e..794f4b6ad 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -309,16 +309,6 @@ class normalizer::imp { } break; } - 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_heq(new_lhs, new_rhs); - } - break; - } case expr_kind::Let: { expr v = normalize(let_value(a), s, k); { diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index c78f84ce8..bdf0175e0 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -156,14 +156,6 @@ public: pop_rs(num); break; } - case expr_kind::HEq: - if (check_index(f, 0) && !visit(heq_lhs(e), offset)) - goto begin_loop; - if (check_index(f, 1) && !visit(heq_rhs(e), offset)) - goto begin_loop; - r = update_heq(e, rs(-2), rs(-1)); - pop_rs(2); - break; case expr_kind::Pi: case expr_kind::Lambda: if (check_index(f, 0) && !visit(abst_domain(e), offset)) goto begin_loop; diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index d177ab780..9c3a3a2c1 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -22,10 +22,6 @@ 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_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)); return update_abst(e, [&](expr const & t, expr const & b) { @@ -80,7 +76,6 @@ 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::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); diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index ac74a9afb..cbad6c3ac 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -31,7 +31,6 @@ 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_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 &); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 09866ab89..08c2e7e36 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -48,7 +48,7 @@ class type_checker::imp { return u; if (has_metavar(u) && m_menv && m_uc) { justification jst = mk_type_expected_justification(ctx, s); - m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst)); + m_uc->push_back(mk_convertible_constraint(ctx, e, TypeUp, jst)); return u; } u = normalize(e, ctx, true); @@ -176,10 +176,6 @@ class type_checker::imp { } case expr_kind::Type: return mk_type(ty_level(e) + 1); - case expr_kind::HEq: - // cheap when we are just inferring types - if (m_infer_only) - return mk_bool_type(); case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: break; // expensive cases @@ -241,11 +237,6 @@ class type_checker::imp { f_t = check_pi(f_t, e, ctx); } } - case expr_kind::HEq: - lean_assert(!m_infer_only); - 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) { expr d = infer_type_core(abst_domain(e), ctx); @@ -423,8 +414,6 @@ public: switch (e.kind()) { case expr_kind::Lambda: case expr_kind::Type: return false; - case expr_kind::HEq: - return true; case expr_kind::Pi: return is_proposition(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)), menv); default: diff --git a/src/kernel/update_expr.cpp b/src/kernel/update_expr.cpp index 1bbacf582..67a4b67bc 100644 --- a/src/kernel/update_expr.cpp +++ b/src/kernel/update_expr.cpp @@ -66,11 +66,4 @@ expr update_let(expr const & let, optional const & t, expr const & v, expr else return mk_let(let_name(let), t, v, b); } - -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_heq(l, r); -} } diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index a8921fe6b..fd357bf9d 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -43,7 +43,6 @@ class deep_copy_fn { new_args.push_back(apply(old_arg)); return save_result(a, mk_app(new_args), 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); diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 2cea1b5a8..29cab995a 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -620,18 +620,11 @@ class elaborator::imp { } } - void process_eq(context const & ctx, expr & a) { - if (is_heq(a) && m_use_normalizer) { - a = normalize(ctx, a); - } - } - expr normalize_step(context const & ctx, expr const & a) { expr new_a = a; process_let(new_a); process_var(ctx, new_a); process_app(ctx, new_a); - process_eq(ctx, new_a); return new_a; } @@ -840,17 +833,6 @@ 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_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), 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}), @@ -1058,28 +1040,6 @@ class elaborator::imp { } } - /** - \brief Similar to imitate_abstraction, but b is a heterogeneous equality. - */ - void imitate_equality(expr const & a, expr const & b, unification_constraint const & c) { - lean_assert(is_metavar(a)); - static_cast(b); // this line is just to avoid a warning, b is only used in an assertion - lean_assert(is_heq(b)); - lean_assert(!is_assigned(a)); - lean_assert(has_local_context(a)); - // imitate - push_active(c); - // Create a fresh meta variable for the lhs and rhs of b. - // The new metavariables have the same context of a. - expr m = mk_metavar(metavar_name(a)); - 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_heq(h1, h2); - justification new_jst(new imitation_justification(c)); - push_new_constraint(true, ctx_m, m, imitation, new_jst); - } - /** \brief Process a constraint ctx |- a == b where \c a is of the form ?m[(inst:i t), ...]. We perform a "case split", @@ -1138,9 +1098,6 @@ class elaborator::imp { } else if (is_app(b) && !has_metavar(arg(b, 0))) { imitate_application(a, b, c); return true; - } else if (is_heq(b)) { - imitate_equality(a, b, c); - return true; } } return false; @@ -1179,16 +1136,16 @@ class elaborator::imp { // We approximate and only consider the most useful ones. justification new_jst(new destruct_justification(c)); if (is_bool(a)) { - expr choices[3] = { Bool, Type(), TypeU }; - push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst)); + expr choices[4] = { Bool, Type(), TypeU, TypeUp }; + push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst)); return true; } else if (m_env->is_ge(ty_level(a), m_U)) { - expr choices[2] = { a, Type(ty_level(a) + 1) }; - push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst)); + expr choices[3] = { a, Type(ty_level(a) + 1), TypeUp }; + push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst)); return true; } else { - expr choices[3] = { a, Type(ty_level(a) + 1), TypeU }; - push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst)); + expr choices[4] = { a, Type(ty_level(a) + 1), TypeU }; + push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst)); return true; } } else { @@ -1253,6 +1210,10 @@ class elaborator::imp { expr choices[4] = { TypeU, Type(level() + 1), Type(), Bool }; push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst)); return true; + } else if (b == TypeUp) { + expr choices[5] = { TypeUp, TypeU, Type(level() + 1), Type(), Bool }; + push_active(mk_choice_constraint(get_context(c), a, 5, choices, new_jst)); + return true; } else { level const & lvl = ty_level(b); lean_assert(!lvl.is_bottom()); @@ -1376,6 +1337,8 @@ class elaborator::imp { expr_pair p1 = get_equality_args(a); expr_pair p2 = get_equality_args(b); justification new_jst(new destruct_justification(c)); + if (is_eq(a) && is_eq(b)) + push_new_eq_constraint(ctx, arg(a, 1), arg(b, 1), new_jst); push_new_eq_constraint(ctx, p1.first, p2.first, new_jst); push_new_eq_constraint(ctx, p1.second, p2.second, new_jst); return true; diff --git a/src/library/equality.cpp b/src/library/equality.cpp index 94e5f4b90..4a0734a77 100644 --- a/src/library/equality.cpp +++ b/src/library/equality.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura namespace lean { bool is_equality(expr const & e) { - return is_eq(e) || is_iff(e) || is_heq(e); + return is_eq(e) || is_iff(e); } bool is_equality(expr const & e, expr & lhs, expr & rhs) { @@ -21,10 +21,6 @@ bool is_equality(expr const & e, expr & lhs, expr & rhs) { lhs = arg(e, 1); rhs = arg(e, 2); return true; - } else if (is_heq(e)) { - lhs = heq_lhs(e); - rhs = heq_rhs(e); - return true; } else { return false; } @@ -35,8 +31,6 @@ expr_pair get_equality_args(expr const & e) { return mk_pair(arg(e, 2), arg(e, 3)); } else if (is_iff(e)) { return mk_pair(arg(e, 1), arg(e, 2)); - } else if (is_heq(e)) { - return mk_pair(heq_lhs(e), heq_rhs(e)); } else { lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index e355cb0ff..6340cbc89 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -37,11 +37,6 @@ 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::HEq: - if (heq_lhs(a) != heq_lhs(b)) - return is_lt(heq_lhs(a), heq_lhs(b), use_hash); - else - 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)) diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp index fa9434727..1f3df7b5e 100644 --- a/src/library/fo_unify.cpp +++ b/src/library/fo_unify.cpp @@ -62,8 +62,6 @@ optional fo_unify(expr e1, expr e2) { } } break; - 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)); todo.emplace_back(abst_domain(e1), abst_domain(e2)); diff --git a/src/library/hop_match.cpp b/src/library/hop_match.cpp index 83e9f42dd..5956a1fb1 100644 --- a/src/library/hop_match.cpp +++ b/src/library/hop_match.cpp @@ -216,8 +216,6 @@ class hop_match_fn { } return true; } - case expr_kind::HEq: - lean_unreachable(); break; // LCOV_EXCL_LINE case expr_kind::Lambda: case expr_kind::Pi: return match(abst_domain(p), abst_domain(t), ctx, ctx_size) && diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 6ec5ec503..d061b28d3 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -323,10 +323,6 @@ static int expr_mk_app(lua_State * L) { return push_expr(L, mk_app(args)); } -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) { return push_expr(L, mk_lambda(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3))); } @@ -438,7 +434,6 @@ static int expr_ ## P(lua_State * L) { \ EXPR_PRED(is_constant) EXPR_PRED(is_var) EXPR_PRED(is_app) -EXPR_PRED(is_heq) EXPR_PRED(is_lambda) EXPR_PRED(is_pi) EXPR_PRED(is_abstraction) @@ -500,7 +495,6 @@ 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::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; @@ -633,6 +627,10 @@ static int expr_abst_body(lua_State * L) { return push_expr(L, abst_body(to_expr(L, 1))); } +static int expr_mk_eq(lua_State * L) { + return push_expr(L, mk_eq(to_expr(L, 1), to_expr(L, 2), to_expr(L, 3))); +} + static const struct luaL_Reg expr_m[] = { {"__gc", expr_gc}, // never throws {"__tostring", safe_function}, @@ -643,7 +641,6 @@ static const struct luaL_Reg expr_m[] = { {"is_var", safe_function}, {"is_constant", safe_function}, {"is_app", safe_function}, - {"is_heq", safe_function}, {"is_lambda", safe_function}, {"is_pi", safe_function}, {"is_abstraction", safe_function}, @@ -697,8 +694,6 @@ 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_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"); @@ -708,6 +703,7 @@ static void open_expr(lua_State * L) { SET_GLOBAL_FUN(expr_pi, "Pi"); SET_GLOBAL_FUN(expr_let, "Let"); SET_GLOBAL_FUN(expr_type, "mk_type"); + SET_GLOBAL_FUN(expr_mk_eq, "mk_eq"); SET_GLOBAL_FUN(expr_type, "Type"); SET_GLOBAL_FUN(expr_mk_metavar, "mk_metavar"); SET_GLOBAL_FUN(expr_pred, "is_expr"); @@ -718,7 +714,6 @@ 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("HEq", expr_kind::HEq); SET_ENUM("Lambda", expr_kind::Lambda); SET_ENUM("Pi", expr_kind::Pi); SET_ENUM("Let", expr_kind::Let); diff --git a/src/library/printer.cpp b/src/library/printer.cpp index d4c1e1e7a..f820cfba9 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -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::HEq: case expr_kind::Let: + case expr_kind::Let: return false; } return false; @@ -55,12 +55,6 @@ struct print_expr_fn { } } - void print_heq(expr const & a, context const & c) { - print_child(heq_lhs(a), c); - out() << " == "; - print_child(heq_rhs(a), c); - } - void print_app(expr const & e, context const & c) { print_child(arg(e, 0), c); for (unsigned i = 1; i < num_args(e); i++) { @@ -114,9 +108,6 @@ struct print_expr_fn { case expr_kind::App: print_app(a, c); break; - case expr_kind::HEq: - print_heq(a, c); - break; case expr_kind::Lambda: out() << "fun " << abst_name(a) << " : "; print_child(abst_domain(a), c); diff --git a/src/library/rewriter/fo_match.cpp b/src/library/rewriter/fo_match.cpp index 21c99587b..29e3decf6 100644 --- a/src/library/rewriter/fo_match.cpp +++ b/src/library/rewriter/fo_match.cpp @@ -117,13 +117,6 @@ bool fo_match::match_type(expr const & p, expr const & t, unsigned, subst_map &) return p == t; } -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_heq(t)) - return false; - 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) { lean_trace("fo_match", tout << "match_let : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE if (!is_let(t)) { @@ -176,8 +169,6 @@ 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::HEq: - return match_heq(p, t, o, s); case expr_kind::Let: return match_let(p, t, o, s); case expr_kind::MetaVar: diff --git a/src/library/rewriter/fo_match.h b/src/library/rewriter/fo_match.h index edf2e5ecf..579c696c9 100644 --- a/src/library/rewriter/fo_match.h +++ b/src/library/rewriter/fo_match.h @@ -22,7 +22,6 @@ 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_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); diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index f9362a4fd..0b52602c8 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/src/library/rewriter/rewriter.cpp @@ -51,14 +51,17 @@ pair rewrite_lambda_type(environment const & env, context & ctx, exp } else { name const & n = abst_name(v); expr const & body = abst_body(v); - expr const & pf_ty = result_ty.second; + // expr const & pf_ty = result_ty.second; 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 = mk_subst_th(ty_ty, ty, new_ty, - Fun({Const("T"), ty_ty}, - mk_heq(v, mk_lambda(n, Const("T"), body))), - mk_refl_th(ty_v, v), pf_ty); + expr proof; +#if 0 // TODO(Leo): we don't have heterogeneous equality anymore + = mk_subst_th(ty_ty, ty, new_ty, + Fun({Const("T"), ty_ty}, + mk_heq(v, mk_lambda(n, Const("T"), body))), + mk_refl_th(ty_v, v), pf_ty); +#endif return make_pair(new_v, proof); } } @@ -111,35 +114,38 @@ pair rewrite_lambda_body(environment const & env, context & ctx, exp body') \return pair of v' = \f$(\lambda n : ty'. body')\f$, and proof of v = v' */ -pair rewrite_lambda(environment const & env, context & ctx, expr const & v, pair const & result_ty, pair const & result_body) { +pair rewrite_lambda(environment const & env, context & /* ctx */, expr const & v, pair const & result_ty, pair const & result_body) { lean_assert(is_lambda(v)); type_inferer ti(env); name const & n = abst_name(v); - expr const & ty = abst_domain(v); - expr const & body = abst_body(v); + // expr const & ty = abst_domain(v); + // expr const & body = abst_body(v); expr const & new_ty = result_ty.first; - expr const & pf_ty = result_ty.second; + // expr const & pf_ty = result_ty.second; expr const & new_body = result_body.first; - expr const & pf_body = result_body.second; - expr const & ty_ty = ti(ty, ctx); - expr const & ty_body = ti(body, ctx); - expr const & ty_v = ti(v, ctx); - expr const & new_v1 = mk_lambda(n, new_ty, body); - expr const & ty_new_v1 = ti(v, ctx); + // expr const & pf_body = result_body.second; + // expr const & ty_ty = ti(ty, ctx); + // expr const & ty_body = ti(body, ctx); + // expr const & ty_v = ti(v, ctx); + // expr const & new_v1 = mk_lambda(n, new_ty, body); + // 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 = mk_subst_th(ty_ty, ty, new_ty, + + expr proof; +#if 0 // TODO(Leo): we don't have heterogeneous equality anymore + expr proof1 = mk_subst_th(ty_ty, ty, new_ty, Fun({Const("T"), ty_ty}, 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 = mk_subst_th(ty_body, body, new_body, + expr proof2 = mk_subst_th(ty_body, body, new_body, Fun({Const("e"), ty_body}, mk_heq(new_v1, mk_lambda(n, new_ty, Const("e")))), mk_refl_th(ty_new_v1, new_v1), pf_body); expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2); +#endif return make_pair(new_v2, proof); } @@ -155,22 +161,25 @@ pair rewrite_lambda(environment const & env, context & ctx, expr con rewritten type of ty and pf_ty the proof of (ty = ty') \return pair of v' = \f$(\Pi n : ty'. body)\f$, and proof of v = v' */ -pair rewrite_pi_type(environment const & env, context & ctx, expr const & v, pair const & result_ty) { +pair rewrite_pi_type(environment const & env, context & /* ctx */, expr const & v, pair const & result_ty) { lean_assert(is_pi(v)); type_inferer ti(env); name const & n = abst_name(v); - expr const & ty = abst_domain(v); + // expr const & ty = abst_domain(v); expr const & body = abst_body(v); expr const & new_ty = result_ty.first; - expr const & pf = result_ty.second; + // expr const & pf = result_ty.second; 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 = mk_subst_th(ty_ty, ty, new_ty, + // expr const & ty_ty = ti(ty, ctx); + // expr const & ty_v = ti(v, ctx); + expr proof; +#if 0 // TODO(Leo): HEq is gone + = mk_subst_th(ty_ty, ty, new_ty, Fun({Const("T"), ty_ty}, mk_heq(v, mk_pi(n, Const("T"), body))), mk_refl_th(ty_v, v), pf); +#endif return make_pair(new_v, proof); } @@ -187,22 +196,25 @@ pair rewrite_pi_type(environment const & env, context & ctx, expr co body') \return pair of v' = \f$(\Pi n : ty. body')\f$, and proof of v = v' */ -pair rewrite_pi_body(environment const & env, context & ctx, expr const & v, pair const & result_body) { +pair rewrite_pi_body(environment const & env, context & /* ctx */, expr const & v, pair const & result_body) { lean_assert(is_pi(v)); type_inferer ti(env); name const & n = abst_name(v); expr const & ty = abst_domain(v); - expr const & body = abst_body(v); + // expr const & body = abst_body(v); expr const & new_body = result_body.first; - expr const & pf = result_body.second; + // expr const & pf = result_body.second; 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 & ty_body = ti(body, extend(ctx, n, ty)); + // expr const & ty_v = ti(v, ctx); + expr proof; +#if 0 // TODO(Leo): HEq is gone expr const & proof = mk_subst_th(ty_body, body, new_body, Fun({Const("e"), ty_body}, mk_heq(v, mk_pi(n, ty, Const("e")))), mk_refl_th(ty_v, v), pf); +#endif return make_pair(new_v, proof); } @@ -221,22 +233,24 @@ pair rewrite_pi_body(environment const & env, context & ctx, expr co body') \return pair of v' = \f$(\Pi n : ty'. body')\f$, and proof of v = v' */ -pair rewrite_pi(environment const & env, context & ctx, expr const & v, pair const & result_ty, pair const & result_body) { +pair rewrite_pi(environment const & env, context & /*ctx*/, expr const & v, pair const & result_ty, pair const & result_body) { lean_assert(is_pi(v)); type_inferer ti(env); name const & n = abst_name(v); - expr const & ty = abst_domain(v); - expr const & body = abst_body(v); + // expr const & ty = abst_domain(v); + // expr const & body = abst_body(v); expr const & new_ty = result_ty.first; - expr const & pf_ty = result_ty.second; + // expr const & pf_ty = result_ty.second; expr const & new_body = result_body.first; - expr const & pf_body = result_body.second; - expr const & ty_ty = ti(ty, ctx); - expr const & ty_body = ti(body, ctx); - expr const & ty_v = ti(v, ctx); - expr const & new_v1 = mk_pi(n, new_ty, body); - expr const & ty_new_v1 = ti(v, ctx); + // expr const & pf_body = result_body.second; + // expr const & ty_ty = ti(ty, ctx); + // expr const & ty_body = ti(body, ctx); + // expr const & ty_v = ti(v, ctx); + // 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 proof; +#if 0 // TODO(Leo): HEq is gone expr const & proof1 = mk_subst_th(ty_ty, ty, new_ty, Fun({Const("T"), ty_ty}, mk_heq(v, mk_pi(n, Const("T"), body))), @@ -248,109 +262,7 @@ pair rewrite_pi(environment const & env, context & ctx, expr const & mk_refl_th(ty_new_v1, new_v1), pf_body); expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2); - return make_pair(new_v2, proof); -} - -/** - \brief For a Eq term v = (lhs = rhs) and the rewriting result for - lhs, it constructs a new rewriting result for v' = (lhs' = rhs) - with the proof of v = v'. - - \param env environment - \param ctx context - \param v (lhs = rhs) - \param result_lhs rewriting result of lhs -- pair of lhs' - rewritten term of lhs and pf_lhs the proof of (lhs = lhs') - \return pair of v' = (lhs' = rhs), and proof of v = v' -*/ -pair rewrite_eq_lhs(environment const & env, context & ctx, expr const & v, pair const & result_lhs) { - lean_assert(is_heq(v)); - type_inferer ti(env); - 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_heq(new_lhs, rhs); - expr const & ty_lhs = ti(lhs, ctx); - expr const & ty_v = ti(v, ctx); - expr const & proof = mk_subst_th(ty_lhs, lhs, new_lhs, - Fun({Const("x"), ty_lhs}, - mk_heq(v, mk_heq(Const("x"), rhs))), - mk_refl_th(ty_v, v), - pf); - return make_pair(new_v, proof); -} - -/** - \brief For a Eq term v = (lhs = rhs)and the rewriting - result for rhs, it constructs a new rewriting result for v' - = (lhs = rhs') with the proof of v = v'. - - \param env environment - \param ctx context - \param v (lhs = rhs) - \param result_rhs rewriting result of rhs -- pair of rhs' - rewritten term of rhs and pf_rhs the proof of (rhs = rhs') - \return pair of v' = (lhs = rhs'), and proof of v = v' -*/ -pair rewrite_eq_rhs(environment const & env, context & ctx, expr const & v, pair const & result_rhs) { - lean_assert(is_heq(v)); - type_inferer ti(env); - 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_heq(rhs, new_rhs); - expr const & ty_rhs = ti(rhs, ctx); - expr const & ty_v = ti(v, ctx); - expr const & proof = mk_subst_th(ty_rhs, rhs, new_rhs, - Fun({Const("x"), ty_rhs}, - mk_heq(v, mk_heq(lhs, Const("x")))), - mk_refl_th(ty_v, v), - pf); - return make_pair(new_v, proof); -} - -/** - \brief For a Eq term v = (lhs = rhs)and the rewriting result for - lhs and rhs, it constructs a new rewriting result for v' = (lhs' = - rhs') with the proof of v = v'. - - \param env environment - \param ctx context - \param v (lhs = rhs) - \param result_lhs rewriting result of lhs -- pair of lhs' - rewritten term of lhs and pf_lhs the proof of (lhs = lhs') - \param result_rhs rewriting result of rhs -- pair of rhs' - rewritten term of rhs and pf_rhs the proof of (rhs = rhs') - \return pair of v' = (lhs' = rhs'), and proof of v = v' -*/ -pair rewrite_eq(environment const & env, context & ctx, expr const & v, pair const & result_lhs, pair const & result_rhs) { - lean_assert(is_heq(v)); - type_inferer ti(env); - 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_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 = mk_subst_th(ty_lhs, lhs, new_lhs, - Fun({Const("x"), ty_lhs}, - mk_heq(v, mk_heq(Const("x"), rhs))), - mk_refl_th(ty_v, v), - pf_lhs); - expr const & proof2 = mk_subst_th(ty_rhs, rhs, new_rhs, - Fun({Const("x"), ty_rhs}, - mk_heq(v, mk_heq(lhs, Const("x")))), - mk_refl_th(ty_new_v1, new_v1), - pf_rhs); - expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2); +#endif return make_pair(new_v2, proof); } @@ -366,24 +278,27 @@ pair rewrite_eq(environment const & env, context & ctx, expr const & rewritten type of ty and \c pf_ty the proof of (ty = ty') \return pair of v' = (let n : ty' = val in body), and proof of v = v' */ -pair rewrite_let_type(environment const & env, context & ctx, expr const & v, pair const & result_ty) { +pair rewrite_let_type(environment const & env, context & /* ctx */, expr const & v, pair const & result_ty) { lean_assert(is_let(v)); type_inferer ti(env); if (!let_type(v)) { name const & n = let_name(v); - expr const & ty = *let_type(v); + // expr const & ty = *let_type(v); expr const & val = let_value(v); expr const & body = let_body(v); expr const & new_ty = result_ty.first; - expr const & pf = result_ty.second; + // expr const & pf = result_ty.second; 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 & ty_ty = ti(ty, ctx); + // expr const & ty_v = ti(v, ctx); + expr proof; +#if 0 // TODO(Leo): HEq is gone expr const & proof = mk_subst_th(ty_ty, ty, new_ty, Fun({Const("x"), ty_ty}, mk_heq(v, mk_let(n, Const("x"), val, body))), mk_refl_th(ty_v, v), pf); +#endif return make_pair(new_v, proof); } else { throw rewriter_exception(); @@ -402,23 +317,26 @@ pair rewrite_let_type(environment const & env, context & ctx, expr c rewritten term of val and \c pf_val the proof of (val = val') \return pair of v' = (let n : ty = val' in body), and proof of v = v' */ -pair rewrite_let_value(environment const & env, context & ctx, expr const & v, pair const & result_value) { +pair rewrite_let_value(environment const & env, context & /* ctx */, expr const & v, pair const & result_value) { lean_assert(is_let(v)); type_inferer ti(env); name const & n = let_name(v); optional const & ty = let_type(v); - expr const & val = let_value(v); + // expr const & val = let_value(v); expr const & body = let_body(v); expr const & new_val = result_value.first; - expr const & pf = result_value.second; + // expr const & pf = result_value.second; 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 & ty_val = ti(val, ctx); + // expr const & ty_v = ti(v, ctx); + expr proof; + #if 0 // TODO(Leo): HEq is gone expr const & proof = mk_subst_th(ty_val, val, new_val, Fun({Const("x"), ty_val}, mk_heq(v, mk_let(n, ty, Const("x"), body))), mk_refl_th(ty_v, v), pf); + #endif return make_pair(new_v, proof); } @@ -435,23 +353,26 @@ pair rewrite_let_value(environment const & env, context & ctx, expr body') \return pair of v' = (let n : ty = val in body'), and proof of v = v' */ -pair rewrite_let_body(environment const & env, context & ctx, expr const & v, pair const & result_body) { +pair rewrite_let_body(environment const & env, context & /* ctx */, expr const & v, pair const & result_body) { lean_assert(is_let(v)); type_inferer ti(env); name const & n = let_name(v); optional const & ty = let_type(v); expr const & val = let_value(v); - expr const & body = let_body(v); + // expr const & body = let_body(v); expr const & new_body = result_body.first; - expr const & pf = result_body.second; + // expr const & pf = result_body.second; 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 & ty_body = ti(body, extend(ctx, n, ty, body)); + // expr const & ty_v = ti(v, ctx); + expr proof; +#if 0 // TODO(Leo): HEq is gone expr const & proof = mk_subst_th(ty_body, body, new_body, Fun({Const("e"), ty_body}, mk_heq(v, mk_let(n, ty, val, Const("e")))), mk_refl_th(ty_v, v), pf); +#endif return make_pair(new_v, proof); } @@ -527,6 +448,7 @@ theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & bod m_pattern = abst_body(m_pattern); m_num_args++; } +#if 0 // HEq is gone 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;); @@ -535,6 +457,7 @@ theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & bod m_pattern = heq_lhs(m_pattern); lean_trace("rewriter", tout << "Number of Arg = " << m_num_args << endl;); +#endif } theorem_rewriter_cell::~theorem_rewriter_cell() { } pair theorem_rewriter_cell::operator()(environment const &, context &, expr const & v) const throw(rewriter_exception) { diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h index f0f9fd0f2..ef4552722 100644 --- a/src/library/rewriter/rewriter.h +++ b/src/library/rewriter/rewriter.h @@ -43,9 +43,6 @@ std::pair rewrite_lambda(environment const & env, context & ctx, exp std::pair rewrite_pi_type(environment const & env, context & ctx, expr const & v, std::pair const & result_ty); std::pair rewrite_pi_body(environment const & env, context & ctx, expr const & v, std::pair const & result_body); std::pair rewrite_pi(environment const & env, context & ctx, expr const & v, std::pair const & result_ty, std::pair const & result_body); -std::pair rewrite_eq_lhs(environment const & env, context & ctx, expr const & v, std::pair const & result_lhs); -std::pair rewrite_eq_rhs(environment const & env, context & ctx, expr const & v, std::pair const & result_rhs); -std::pair rewrite_eq(environment const & env, context & ctx, expr const & v, std::pair const & result_lhs, std::pair const & result_rhs); std::pair rewrite_let_type(environment const & env, context & ctx, expr const & v, std::pair const & result_ty); std::pair rewrite_let_value(environment const & env, context & ctx, expr const & v, std::pair const & result_value); std::pair rewrite_let_body(environment const & env, context & ctx, expr const & v, std::pair const & result_body); @@ -387,37 +384,6 @@ class apply_rewriter_fn { } } break; - case expr_kind::HEq: { - expr const & lhs = heq_lhs(v); - expr const & rhs = heq_rhs(v); - std::pair result_lhs = apply(env, ctx, lhs); - std::pair result_rhs = apply(env, ctx, rhs); - expr const & new_lhs = result_lhs.first; - expr const & new_rhs = result_rhs.first; - if (lhs != new_lhs) { - if (rhs != new_rhs) { - // lhs & rhs changed - result = rewrite_eq(env, ctx, v, result_lhs, result_rhs); - } else { - // only lhs changed - result = rewrite_eq_lhs(env, ctx, v, result_lhs); - } - } else { - if (rhs != new_rhs) { - // only rhs changed - result = rewrite_eq_rhs(env, ctx, v, result_rhs); - } else { - // nothing changed - result = std::make_pair(v, mk_refl_th(ti(v, ctx), v)); - } - } - std::pair tmp = m_rw(env, ctx, result.first); - if (result.first != tmp.first) { - tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second); - result = tmp; - } - } - break; case expr_kind::Lambda: { name const & n = abst_name(v); expr const & ty = abst_domain(v); diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 80e29f123..66a753561 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -180,10 +180,6 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset, return is_permutation(abst_domain(lhs), abst_domain(rhs), offset, p) && is_permutation(abst_body(lhs), abst_body(rhs), offset+1, p); - case expr_kind::HEq: - return - is_permutation(heq_lhs(lhs), heq_lhs(rhs), offset, p) && - is_permutation(heq_rhs(lhs), heq_rhs(rhs), offset, p); case expr_kind::App: if (num_args(lhs) == num_args(rhs)) { for (unsigned i = 0; i < num_args(lhs); i++) { diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index aa63f08da..6a8f04faf 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -76,8 +76,6 @@ 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::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 +133,6 @@ 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::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 +291,7 @@ static void tst13() { } static void tst14() { - expr t = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), Const("a"), Const("b")); check_serializer(t); std::cout << t << "\n"; expr l = mk_let("a", none_expr(), Const("b"), Var(0)); @@ -329,9 +325,6 @@ 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(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 +339,6 @@ static void tst16() { expr a = Const("a"); check_copy(iVal(10)); check_copy(f(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))); diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp index 662ce8297..e851928e1 100644 --- a/src/tests/kernel/free_vars.cpp +++ b/src/tests/kernel/free_vars.cpp @@ -75,11 +75,9 @@ 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)}, 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)}, HEq(Var(2), Var(1)))) == 2); context ctx; ctx = extend(ctx, name("x"), Bool); ctx = extend(ctx, name("y"), Bool); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index ce3184640..57773b667 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -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}}, HEq(f(m1), y)))(a)); + (Fun({{x, N}, {y, N}}, mk_eq(N, f(m1), y)))(a)); metavar_env menv2 = menv.copy(); menv2->assign(m1, h(Var(4), Var(1), Var(3))); normalizer norm(env); @@ -287,12 +287,6 @@ static void tst14() { std::cout << norm(menv2->instantiate_metavars(F1)) << "\n"; 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}}, 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}}, HEq(f(m1), y)))(b, m2)))(M); - std::cout << norm(F3) << "\n"; } static void tst15() { diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index e38967e1c..2d4479496 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -76,8 +76,6 @@ 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::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 +195,9 @@ static void tst3() { env->add_var("a", Bool); expr t1 = Const("a"); expr t2 = Const("a"); - expr e = HEq(t1, t2); + expr e = mk_eq(Bool, t1, t2); std::cout << e << " --> " << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == HEq(t1, t2)); + lean_assert(normalize(e, env) == mk_eq(Bool, t1, t2)); } static void tst4() { diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index baf5fdfd2..be662c902 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -80,7 +80,7 @@ static void tst2() { static void tst3() { environment env; init_test_frontend(env); - expr f = Fun("a", Bool, HEq(Const("a"), True)); + expr f = Fun("a", Bool, mk_eq(Bool, 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 = HEq(iVal(1), iVal(2)); + expr a = mk_eq(Int, iVal(1), iVal(2)); expr pr = mk_lambda("x", a, Var(0)); std::cout << type_check(pr, env) << "\n"; } @@ -191,7 +191,7 @@ 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 = HEq(t1, t2); + expr prop = mk_eq(Int, 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", HEq(t1, t2), mk_refl_th(Int, t1)); - env->add_theorem("eqs2", HEq(t1, t3), mk_refl_th(Int, t1)); + env->add_theorem("eqs1", mk_eq(Int, t1, t2), mk_refl_th(Int, t1)); + env->add_theorem("eqs2", mk_eq(Int, 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(HEq(True, False)), env) << "\n"; + std::cout << type_check(f(mk_eq(Bool, True, False)), env) << "\n"; } static void tst14() { diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index 41bafb6d5..70e1caac2 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -110,10 +110,10 @@ static void tst5() { environment env; init_test_frontend(env); env->add_var(name("a"), Int); - expr e = HEq(iVal(3), iVal(4)); + expr e = mk_eq(Int, iVal(3), iVal(4)); std::cout << e << " --> " << normalize(e, env) << "\n"; lean_assert(normalize(e, env) == False); - lean_assert(normalize(HEq(Const("a"), iVal(3)), env) == HEq(Const("a"), iVal(3))); + lean_assert(normalize(mk_eq(Int, Const("a"), iVal(3)), env) == mk_eq(Int, Const("a"), iVal(3))); } static void tst6() { diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp index dce67335d..1d554c020 100644 --- a/src/tests/library/deep_copy.cpp +++ b/src/tests/library/deep_copy.cpp @@ -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")), HEq(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")), f(x, m))))); expr G = deep_copy(F); lean_assert(F == G); lean_assert(!is_eqp(F, G)); diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index 6d81fd912..4a7607020 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -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", HEq(f(a, f(a, b)), a)); - env->add_axiom("H2", HEq(a, b)); + env->add_axiom("H1", mk_eq(Int, f(a, f(a, b)), a)); + env->add_axiom("H2", mk_eq(Int, a, b)); expr V = mk_subst_th(m1, m2, m3, m4, H1, H2); - expr expected = HEq(f(a, f(b, b)), a); + expr expected = mk_eq(Int, 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,8 +339,8 @@ static void tst8() { env->add_var("a", Bool); env->add_var("b", Bool); env->add_var("c", Bool); - env->add_axiom("H1", HEq(a, b)); - env->add_axiom("H2", HEq(b, c)); + env->add_axiom("H1", mk_eq(Bool, a, b)); + env->add_axiom("H2", mk_eq(Bool, 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); @@ -362,7 +362,11 @@ static void tst9() { env->add_var("vec", Nat >> Type()); expr n = Const("n"); expr vec = Const("vec"); - env->add_var("f", Pi({n, Nat}, vec(n) >> Nat)); + std::cout << "step1\n"; + expr z = Const("z"); + env->add_var("z", Nat); + env->add_var("f", Pi({n, Nat}, vec(z) >> Nat)); + std::cout << "step2\n"; expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); @@ -370,18 +374,18 @@ static void tst9() { expr fact = Const("fact"); env->add_var("a", Nat); env->add_var("b", Nat); - env->add_definition("fact", Bool, HEq(a, b)); + env->add_definition("fact", Bool, mk_eq(Nat, a, b)); env->add_axiom("H", fact); 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)); + mk_congr2_th(Nat, vec(z) >> Nat, a, b, f, H), env); + env->add_var("g", Pi({n, Nat}, vec(z) >> Nat)); expr g = Const("g"); - env->add_axiom("H2", HEq(f, g)); + env->add_axiom("H2", mk_eq(Pi({n, Nat}, vec(z) >> Nat), f, g)); expr H2 = Const("H2"); success(mk_congr_th(_, _, _, _, _, _, H2, H), - mk_congr_th(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env); + mk_congr_th(Nat, vec(z) >> 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); + mk_congr_th(Nat, vec(z) >> Nat, f, f, a, b, mk_refl_th(Pi({n, Nat}, vec(z) >> Nat), f), H), env); success(mk_refl_th(_, a), mk_refl_th(Nat, a), env); } @@ -402,11 +406,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, _}}, HEq(f(x, y), f(x, z))), - Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, HEq(f(x, y), f(x, z))), env); + success(Fun({{x, _}, {y, _}, {z, _}}, mk_eq(_, f(x, y), f(x, z))), + Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, mk_eq(R, f(x, y), f(x, z))), env); expr A = Const("A"); - 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); + success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, mk_eq(_, f(x, y), f(x, z))), + Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, mk_eq(R, f(x, y), f(x, z))), env); } static void tst11() { @@ -464,11 +468,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, _}}, 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); + success(Fun({{A, Type()}, {B, Type()}, {x, _}}, mk_eq(_, f(B, x), f(_, x))), + Fun({{A, Type()}, {B, Type()}, {x, B}}, mk_eq(B, f(B, x), f(B, x))), env); + success(Fun({{A, Type()}, {B, Type()}, {x, _}}, mk_eq(B, f(B, x), f(_, x))), + Fun({{A, Type()}, {B, Type()}, {x, B}}, mk_eq(B, f(B, x), f(B, x))), env); + unsolved(Fun({{A, _}, {B, _}, {x, _}}, mk_eq(_, f(B, x), f(_, x))), env); } static void tst14() { @@ -493,23 +497,6 @@ static void tst14() { success(Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(_, Bool, N)), Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(Type(), Bool, N)), env); - success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, - g(_, - 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}}, 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, _}}, 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}}, HEq(f(N, x), f(Bool, y))), - Fun({{x, N}, {y, Bool}}, True))), env); } static void tst15() { @@ -550,28 +537,28 @@ static void tst16() { env->add_var("a", Bool); env->add_var("b", Bool); env->add_var("c", Bool); - success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}}, + success(Fun({{H1, mk_eq(_, a, b)}, {H2, mk_eq(_, b, c)}}, mk_trans_th(_, _, _, _, H1, H2)), - Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}}, + Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}}, mk_trans_th(Bool, a, b, c, H1, H2)), env); expr H3 = Const("H3"); - success(Fun({{H1, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}}, + success(Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, 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}}, + Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, 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, HEq(a, b)}, {H2, HEq(b, c)}, {H3, a}}, + success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, mk_eq(_, a, b)}, {H2, mk_eq(_, 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}}, + Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, 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, HEq(a, b)}, {H2, HEq(b, c)}}, + success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, mk_eq(_, a, b)}, {H2, mk_eq(_, 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)}}, + Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, mk_eq(A, a, b)}, {H2, mk_eq(A, 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 +669,7 @@ void tst21() { expr b = Const("b"); expr m1 = menv->mk_metavar(); expr l = m1(b, a); - expr r = Fun({x, N}, f(x, HEq(a, b))); + expr r = Fun({x, N}, f(x, mk_eq(_, a, b))); elaborator elb(env, menv, context(), l, r); while (true) { try { @@ -745,8 +732,8 @@ void tst23() { expr f = Const("f"); expr m1 = menv->mk_metavar(); expr m2 = menv->mk_metavar(); - expr l = Fun({{x, N}, {y, N}}, HEq(y, f(x, m1))); - expr r = Fun({{x, N}, {y, N}}, HEq(m2, f(m1, x))); + expr l = Fun({{x, N}, {y, N}}, mk_eq(_, y, f(x, m1))); + expr r = Fun({{x, N}, {y, N}}, mk_eq(_, m2, f(m1, x))); elaborator elb(env, menv, context(), l, r); while (true) { try { @@ -832,13 +819,14 @@ void tst26() { expr a = Const("a"); env->add_var("a", Type(level()+1)); expr m1 = menv->mk_metavar(); - expr F = HEq(g(m1, a), a); + expr m2 = menv->mk_metavar(); + expr F = mk_eq(m2, 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), HEq(g(Type(level()+1), a), a)); + lean_assert_eq(s->instantiate_metavars(F), mk_eq(Type(level()+1), g(Type(level()+1), a), a)); } void tst27() { diff --git a/src/tests/library/expr_lt.cpp b/src/tests/library/expr_lt.cpp index 52fbfeefe..6723455de 100644 --- a/src/tests/library/expr_lt.cpp +++ b/src/tests/library/expr_lt.cpp @@ -34,10 +34,6 @@ static void tst1() { lt(Const("a"), Const("b"), true); lt(Const("a"), Const("a"), false); lt(Var(1), Const("a"), true); - 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); diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp index 1f7d14d04..8775deb37 100644 --- a/src/tests/library/formatter.cpp +++ b/src/tests/library/formatter.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/abstract.h" #include "kernel/formatter.h" +#include "kernel/kernel.h" #include "library/printer.h" using namespace lean; @@ -30,16 +31,12 @@ 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(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, 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"); + check(fmt(ctx, f(Var(0), Var(2))), "f y#0 #2"); + check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N)] |- f y#0 #2"); } int main() { diff --git a/src/tests/library/max_sharing.cpp b/src/tests/library/max_sharing.cpp index f614a789f..eb0ff6936 100644 --- a/src/tests/library/max_sharing.cpp +++ b/src/tests/library/max_sharing.cpp @@ -15,14 +15,11 @@ static void tst1() { max_sharing_fn max_fn; expr a1 = Const("a"); expr a2 = Const("a"); - expr F1 = HEq(a1, a2); - lean_assert(!is_eqp(heq_lhs(F1), heq_rhs(F1))); - expr F2 = max_fn(F1); - lean_assert(is_eqp(heq_lhs(F2), heq_rhs(F2))); expr x = Const("x"); expr y = Const("y"); expr f = Const("f"); expr N = Const("N"); + expr F1, F2; F1 = f(Fun({x, N}, f(x, x)), Fun({y, N}, f(y, y))); lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2))); F2 = max_fn(F1); diff --git a/src/tests/library/rewriter/fo_match.cpp b/src/tests/library/rewriter/fo_match.cpp index c2a1d1a42..fdfb4dd83 100644 --- a/src/tests/library/rewriter/fo_match.cpp +++ b/src/tests/library/rewriter/fo_match.cpp @@ -273,7 +273,7 @@ static void match_let_tst1() { static void match_let_tst2() { cout << "--- match_let_tst2() ---" << endl; - expr t = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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 = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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 = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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 = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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 = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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 = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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 = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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 = HEq(Const("a"), Const("b")); + expr t = mk_eq(Const("A"), 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_heq(x, a), mk_heq(f, a), 0, s); + bool result = test_match(mk_eq(Const("A"), x, a), mk_eq(Const("A"), 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_heq(mk_Nat_add(x, a), x), mk_heq(mk_Nat_add(f, a), f), 0, s); + bool result = test_match(mk_eq(Nat, mk_Nat_add(x, a), x), mk_eq(Nat, 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_heq(mk_Nat_add(x, a), x), f, 0, s); + bool result = test_match(mk_eq(Nat, mk_Nat_add(x, a), x), f, 0, s); lean_assert_eq(result, false); lean_assert_eq(s.empty(), true); } diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index 40b919815..01ce4fd27 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -21,6 +21,9 @@ Author: Soonho Kong #include "frontends/lean/frontend.h" using namespace lean; +#if 0 +// TODO(Leo): migrate to homogeneous equality + using std::cout; using std::pair; using lean::endl; @@ -54,7 +57,7 @@ static void theorem_rewriter1_tst() { cout << "Theorem: " << add_comm_thm_type << " := " << add_comm_thm_body << std::endl; cout << " " << concl << " := " << proof << std::endl; - lean_assert_eq(concl, mk_heq(a_plus_b, b_plus_a)); + lean_assert_eq(concl, mk_eq(Nat, a_plus_b, b_plus_a)); lean_assert_eq(proof, Const("ADD_COMM")(a, b)); env->add_theorem("New_theorem1", concl, proof); } @@ -749,3 +752,9 @@ int main() { lambda_type_rewriter_tst(); return has_violations() ? 1 : 0; } +#else +int main() { + save_stack_info(); + return has_violations() ? 1 : 0; +} +#endif diff --git a/src/tests/library/update_expr.cpp b/src/tests/library/update_expr.cpp index da79317fc..339b0f74e 100644 --- a/src/tests/library/update_expr.cpp +++ b/src/tests/library/update_expr.cpp @@ -12,12 +12,6 @@ using namespace lean; static void tst1() { expr a = Const("a"); expr b = Const("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)); } static void tst2() { diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean index d06359e9b..a5061e5e6 100644 --- a/tests/lean/abst.lean +++ b/tests/lean/abst.lean @@ -1,5 +1,5 @@ import Int. -axiom PlusComm(a b : Int) : a + b == b + a. +axiom PlusComm(a b : Int) : a + b = b + a. variable a : Int. check (funext (fun x : Int, (PlusComm a x))). set_option pp::implicit true. diff --git a/tests/lean/abst.lean.expected.out b/tests/lean/abst.lean.expected.out index 756d9b203..e6b2744e5 100644 --- a/tests/lean/abst.lean.expected.out +++ b/tests/lean/abst.lean.expected.out @@ -3,7 +3,7 @@ Imported 'Int' Assumed: PlusComm Assumed: a -funext (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a) +funext (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) = (λ x : ℤ, x + a) Set: lean::pp::implicit @funext ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) : - (λ x : ℤ, a + x) == (λ x : ℤ, x + a) + @eq (∀ x : ℤ, (λ x : ℤ, ℤ) x) (λ x : ℤ, a + x) (λ x : ℤ, x + a) diff --git a/tests/lean/arith6.lean.expected.out b/tests/lean/arith6.lean.expected.out index 2d033f583..d61b0bc2f 100644 --- a/tests/lean/arith6.lean.expected.out +++ b/tests/lean/arith6.lean.expected.out @@ -8,8 +8,8 @@ false true true Assumed: x -3 + -1 * (x * (3 div x)) == 0 -x + -1 * (3 * (x div 3)) == 0 +3 + -1 * (x * (3 div x)) = 0 +x + -1 * (3 * (x div 3)) = 0 false Set: lean::pp::notation Int::divides 3 x diff --git a/tests/lean/bad10.lean b/tests/lean/bad10.lean index da7a67274..b63d67390 100644 --- a/tests/lean/bad10.lean +++ b/tests/lean/bad10.lean @@ -2,7 +2,7 @@ set_option pp::implicit true. set_option pp::colors false. variable N : Type. -definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ := -substp (fun x : N, f (f a) == _) (refl (f (f _))) H. +definition T (a : N) (f : _ -> _) (H : f a = a) : f (f _) = f _ := +substp (fun x : N, f (f a) = _) (refl (f (f _))) H. print environment 1. diff --git a/tests/lean/bad10.lean.expected.out b/tests/lean/bad10.lean.expected.out index 294ea7e02..ebe78d77b 100644 --- a/tests/lean/bad10.lean.expected.out +++ b/tests/lean/bad10.lean.expected.out @@ -4,5 +4,5 @@ Set: pp::colors Assumed: N Defined: T -definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) := - @substp N (f a) a (λ x : N, f (f a) == f (f a)) (@refl N (f (f a))) H +definition T (a : N) (f : N → N) (H : @eq N (f a) a) : @eq N (f (f a)) (f (f a)) := + @substp N (f a) a (λ x : N, @eq N (f (f a)) (f (f a))) (@refl N (f (f a))) H diff --git a/tests/lean/bad9.lean b/tests/lean/bad9.lean index 7c2d62dd7..9415c1797 100644 --- a/tests/lean/bad9.lean +++ b/tests/lean/bad9.lean @@ -3,6 +3,6 @@ set_option pp::colors false. variable N : Type. check -fun (a : N) (f : N -> N) (H : f a == a), -let calc1 : f a == a := substp (fun x : N, f a == _) (refl (f a)) H +fun (a : N) (f : N -> N) (H : f a = a), +let calc1 : f a = a := substp (fun x : N, f a = _) (refl (f a)) H in calc1. \ No newline at end of file diff --git a/tests/lean/bad9.lean.expected.out b/tests/lean/bad9.lean.expected.out index 6f73ca340..5fc7aefc7 100644 --- a/tests/lean/bad9.lean.expected.out +++ b/tests/lean/bad9.lean.expected.out @@ -3,6 +3,6 @@ Set: lean::pp::implicit Set: pp::colors Assumed: N -λ (a : N) (f : N → N) (H : f a == a), - let calc1 : f a == a := @substp N (f a) a (λ x : N, f a == x) (@refl N (f a)) H in calc1 : - ∀ (a : N) (f : N → N), f a == a → f a == a +λ (a : N) (f : N → N) (H : @eq N (f a) a), + let calc1 : @eq N (f a) a := @substp N (f a) a (λ x : N, @eq N (f a) x) (@refl N (f a)) H in calc1 : + ∀ (a : N) (f : N → N), @eq N (f a) a → @eq N (f a) a diff --git a/tests/lean/bug.lean b/tests/lean/bug.lean index 53adf653f..a525b9897 100644 --- a/tests/lean/bug.lean +++ b/tests/lean/bug.lean @@ -1 +1 @@ -check fun (A A' : (Type U)) (H : A == A'), symm H +check fun (A A' : (Type U')) (H : A = A'), symm H diff --git a/tests/lean/bug.lean.expected.out b/tests/lean/bug.lean.expected.out index 1cb3b57f1..8d20643d3 100644 --- a/tests/lean/bug.lean.expected.out +++ b/tests/lean/bug.lean.expected.out @@ -1,11 +1,10 @@ Set: pp::colors Set: pp::unicode Failed to solve -A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU - bug.lean:1:44: Type of argument 1 must be convertible to the expected type in the application of - @symm +A : (Type U'), A' : (Type U') ⊢ ?M::4 ≺ (Type U') + bug.lean:1:37: Type of argument 1 must be convertible to the expected type in the application of + @eq with arguments: ?M::0 A A' - H diff --git a/tests/lean/cast1.lean b/tests/lean/cast1.lean deleted file mode 100644 index 3519518ae..000000000 --- a/tests/lean/cast1.lean +++ /dev/null @@ -1,19 +0,0 @@ -import cast. -import Int. - -variable vector : Type -> Nat -> Type -axiom N0 (n : Nat) : n + 0 = n -theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) := - congr (refl (vector T)) (N0 n) -variable f (n : Nat) (v : vector Int n) : Int -variable m : Nat -variable v1 : vector Int (m + 0) --- The following application will fail because (vector Int (m + 0)) and (vector Int m) --- are not definitionally equal. -check f m v1 --- The next one succeeds using the "casting" operator. --- We can do it, because (V0 Int m) is a proof that --- (vector Int (m + 0)) and (vector Int m) are propositionally equal. --- That is, they have the same interpretation in the lean set theoretic --- semantics. -check f m (cast (V0 Int m) v1) diff --git a/tests/lean/cast1.lean.expected.out b/tests/lean/cast1.lean.expected.out deleted file mode 100644 index 2f4c4d0fd..000000000 --- a/tests/lean/cast1.lean.expected.out +++ /dev/null @@ -1,18 +0,0 @@ - Set: pp::colors - Set: pp::unicode - Imported 'cast' - Imported 'Int' - Assumed: vector - Assumed: N0 - Proved: V0 - Assumed: f - Assumed: m - Assumed: v1 -cast1.lean:13:7: error: type mismatch at application - f m v1 -Function type: - ∀ (n : ℕ), vector ℤ n → ℤ -Arguments types: - m : ℕ - v1 : vector ℤ (m + 0) -f m (cast (V0 ℤ m) v1) : ℤ diff --git a/tests/lean/cast2.lean b/tests/lean/cast2.lean deleted file mode 100644 index 14a8242bf..000000000 --- a/tests/lean/cast2.lean +++ /dev/null @@ -1,7 +0,0 @@ -import cast -variable A : Type -variable B : Type -variable A' : Type -variable B' : Type -axiom H : (A -> B) = (A' -> B') -variable a : A diff --git a/tests/lean/cast2.lean.expected.out b/tests/lean/cast2.lean.expected.out deleted file mode 100644 index 7fed7f298..000000000 --- a/tests/lean/cast2.lean.expected.out +++ /dev/null @@ -1,9 +0,0 @@ - Set: pp::colors - Set: pp::unicode - Imported 'cast' - Assumed: A - Assumed: B - Assumed: A' - Assumed: B' - Assumed: H - Assumed: a diff --git a/tests/lean/cast3.lean b/tests/lean/cast3.lean deleted file mode 100644 index 5013dcce0..000000000 --- a/tests/lean/cast3.lean +++ /dev/null @@ -1,24 +0,0 @@ -import cast - -variables A A' B B' : Type -variable x : A -eval cast (refl A) x -eval x = (cast (refl A) x) -variable b : B -definition f (x : A) : B := b -axiom H : (A -> B) = (A' -> B) -variable a' : A' -eval (cast H f) a' -axiom H2 : (A -> B) = (A' -> B') -definition g (x : B') : Nat := 0 -eval g ((cast H2 f) a') -check g ((cast H2 f) a') - -eval (cast H2 f) a' - -variables A1 A2 A3 : Type -axiom Ha : A1 = A2 -axiom Hb : A2 = A3 -variable a : A1 -eval (cast Hb (cast Ha a)) -check (cast Hb (cast Ha a)) diff --git a/tests/lean/cast3.lean.expected.out b/tests/lean/cast3.lean.expected.out deleted file mode 100644 index d78ef34af..000000000 --- a/tests/lean/cast3.lean.expected.out +++ /dev/null @@ -1,28 +0,0 @@ - Set: pp::colors - Set: pp::unicode - Imported 'cast' - Assumed: A - Assumed: A' - Assumed: B - Assumed: B' - Assumed: x -cast (refl A) x -x == cast (refl A) x - Assumed: b - Defined: f - Assumed: H - Assumed: a' -cast H (λ x : A, b) a' - Assumed: H2 - Defined: g -0 -g (cast H2 f a') : ℕ -cast H2 (λ x : A, b) a' - Assumed: A1 - Assumed: A2 - Assumed: A3 - Assumed: Ha - Assumed: Hb - Assumed: a -cast Hb (cast Ha a) -cast Hb (cast Ha a) : A3 diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean deleted file mode 100644 index ab3423e82..000000000 --- a/tests/lean/cast4.lean +++ /dev/null @@ -1,13 +0,0 @@ -import cast -set_option pp::colors false - -check fun (A A': TypeM) - (B : A -> TypeM) - (B' : A' -> TypeM) - (f : forall x : A, B x) - (g : forall x : A', B' x) - (a : A) - (b : A') - (H2 : f == g) - (H3 : a == b), - hcongr H2 H3 diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out deleted file mode 100644 index b17a52c1b..000000000 --- a/tests/lean/cast4.lean.expected.out +++ /dev/null @@ -1,22 +0,0 @@ - Set: pp::colors - Set: pp::unicode - Imported 'cast' - Set: pp::colors -λ (A A' : TypeM) - (B : A → TypeM) - (B' : A' → TypeM) - (f : ∀ x : A, B x) - (g : ∀ x : A', B' x) - (a : A) - (b : A') - (H2 : f == g) - (H3 : a == b), - hcongr H2 H3 : - ∀ (A A' : TypeM) - (B : A → TypeM) - (B' : A' → TypeM) - (f : ∀ x : A, B x) - (g : ∀ x : A', B' x) - (a : A) - (b : A'), - f == g → a == b → f a == g b diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean index bc90085ba..ee6b506d7 100644 --- a/tests/lean/elab7.lean +++ b/tests/lean/elab7.lean @@ -2,7 +2,7 @@ variables A B C : (Type U) variable P : A -> Bool variable F1 : A -> B -> C variable F2 : A -> B -> C -variable H : forall (a : A) (b : B), (F1 a b) == (F2 a b) +variable H : forall (a : A) (b : B), (F1 a b) = (F2 a b) variable a : A check eta (F2 a) check funext (fun a : A, diff --git a/tests/lean/elab7.lean.expected.out b/tests/lean/elab7.lean.expected.out index 69d44125c..4241f5122 100644 --- a/tests/lean/elab7.lean.expected.out +++ b/tests/lean/elab7.lean.expected.out @@ -9,9 +9,8 @@ Assumed: H Assumed: a eta (F2 a) : (λ x : B, F2 a x) = F2 a -funext (λ a : A, symm (eta (F1 a)) ⋈ (funext (λ b : B, H a b) ⋈ eta (F2 a))) : - (λ x : A, F1 x) == (λ x : A, F2 x) -funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1) +funext (λ a : A, symm (eta (F1 a)) ⋈ (funext (λ b : B, H a b) ⋈ eta (F2 a))) : (λ x : A, F1 x) = (λ x : A, F2 x) +funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) = (λ (x : A) (x::1 : B), F2 x x::1) Proved: T1 Proved: T2 Proved: T3 diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean index 95e37cf59..01999f540 100644 --- a/tests/lean/eq3.lean +++ b/tests/lean/eq3.lean @@ -1,11 +1,8 @@ -import cast variable Vector : Nat -> Type variable n : Nat variable v1 : Vector n variable v2 : Vector (n + 0) variable v3 : Vector (0 + n) -axiom H1 : v1 == v2 -axiom H2 : v2 == v3 -check htrans H1 H2 -set_option pp::implicit true -check htrans H1 H2 +axiom cast {A B : TypeU} : A = B -> A -> B +axiom H1 : v1 = cast (congr2 Vector (Nat::add_zeror n)) v2 +axiom H2 : v2 = cast (congr2 Vector (Nat::add_comm 0 n)) v3 diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out index 7916c74a6..211df19f5 100644 --- a/tests/lean/eq3.lean.expected.out +++ b/tests/lean/eq3.lean.expected.out @@ -1,13 +1,10 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' Assumed: Vector Assumed: n Assumed: v1 Assumed: v2 Assumed: v3 + Assumed: cast Assumed: H1 Assumed: H2 -htrans H1 H2 : v1 == v3 - Set: lean::pp::implicit -@htrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3 diff --git a/tests/lean/eq4.lean b/tests/lean/eq4.lean index bc350f2dc..7767741f5 100644 --- a/tests/lean/eq4.lean +++ b/tests/lean/eq4.lean @@ -1,8 +1,4 @@ import Int -eval 1 == true -eval 1 == 1.0 -eval 1 == nat_to_int 1 -eval true == 1.0 -eval Nat::add == 1 -eval Nat::add == Nat::mul -eval Int::add == Int::mul +import Real +eval 1 = 1.0 +eval 1 = nat_to_int 1 diff --git a/tests/lean/eq4.lean.expected.out b/tests/lean/eq4.lean.expected.out index f825c0158..adbf26673 100644 --- a/tests/lean/eq4.lean.expected.out +++ b/tests/lean/eq4.lean.expected.out @@ -1,10 +1,6 @@ Set: pp::colors Set: pp::unicode Imported 'Int' -1 == ⊤ -1 == 1 -1 == 1 -⊤ == 1 -Nat::add == 1 -Nat::add == Nat::mul -Int::add == Int::mul + Imported 'Real' +⊤ +⊤ diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out index 5f0ab3b77..466f89f5c 100644 --- a/tests/lean/find.lean.expected.out +++ b/tests/lean/find.lean.expected.out @@ -1,8 +1,8 @@ Set: pp::colors Set: pp::unicode Imported 'find' -theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a -theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H : a = b) : f a == f b -theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f = g) (H2 : a = b) : f a == g b +theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a +theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b +theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo' find.lean:4:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture diff --git a/tests/lean/mod1.lean b/tests/lean/mod1.lean index 71e40b48d..69e69fc5e 100644 --- a/tests/lean/mod1.lean +++ b/tests/lean/mod1.lean @@ -1,11 +1,11 @@ -import cast -import cast +import specialfn +import specialfn (* local env = environment() -- create new environment parse_lean_cmds([[ - import cast - import cast - check @cast + import specialfn + import specialfn + check sin ]], env) *) -check @cast \ No newline at end of file +check sin \ No newline at end of file diff --git a/tests/lean/mod1.lean.expected.out b/tests/lean/mod1.lean.expected.out index 53dcc67b2..9e7ea9153 100644 --- a/tests/lean/mod1.lean.expected.out +++ b/tests/lean/mod1.lean.expected.out @@ -1,6 +1,6 @@ Set: pp::colors Set: pp::unicode - Imported 'cast' - Imported 'cast' -@cast : ∀ (A B : TypeU), A == B → A → B -@cast : ∀ (A B : TypeU), A == B → A → B + Imported 'specialfn' + Imported 'specialfn' +sin : ℝ → ℝ +sin : ℝ → ℝ diff --git a/tests/lean/norm1.lean b/tests/lean/norm1.lean index 8ebbc8d91..51cd346a2 100644 --- a/tests/lean/norm1.lean +++ b/tests/lean/norm1.lean @@ -7,7 +7,7 @@ variable H : (N -> N -> N) -> N eval fun f : N -> N, (fun x y : N, g x) (f a) eval fun (a : N) (f : N -> N) (g : (N -> N) -> N -> N) (h : N -> N -> N), (fun (x : N) (y : N) (z : N), h x y) (g (fun x : N, f (f x)) (f a)) (f a) -eval fun (a b : N) (g : Bool -> N), (fun x y : Bool, g x) (a == b) +eval fun (a b : N) (g : Bool -> N), (fun x y : Bool, g x) (a = b) eval fun (a : Type) (b : a -> Type) (g : (Type U) -> Bool), (fun x y : (Type U), g x) (forall x : a, b x) eval fun f : N -> N, (fun x y z : N, g x) (f a) eval fun f g : N -> N, (fun x y z : N, g x) (f a) diff --git a/tests/lean/norm1.lean.expected.out b/tests/lean/norm1.lean.expected.out index 168dab14e..b599037aa 100644 --- a/tests/lean/norm1.lean.expected.out +++ b/tests/lean/norm1.lean.expected.out @@ -7,7 +7,7 @@ Assumed: H λ (f : N → N) (y : N), g (f a) λ (a : N) (f : N → N) (g : (N → N) → N → N) (h : N → N → N) (z : N), h (g (λ x : N, f (f x)) (f a)) (f a) -λ (a b : N) (g : Bool → N) (y : Bool), g (a == b) +λ (a b : N) (g : Bool → N) (y : Bool), g (a = b) λ (a : Type) (b : a → Type) (g : (Type U) → Bool) (y : (Type U)), g (∀ x : a, b x) λ (f : N → N) (y z : N), g (f a) λ (f g : N → N) (y z : N), g (f a) diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean deleted file mode 100644 index 71cac8fa1..000000000 --- a/tests/lean/norm_bug1.lean +++ /dev/null @@ -1,27 +0,0 @@ -import cast -set_option pp::colors false - -check fun (A A': TypeM) - (a : A) - (b : A') - (L2 : A' == A), - let b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b - in L3 - -check fun (A A': TypeM) - (B : A -> TypeM) - (B' : A' -> TypeM) - (f : forall x : A, B x) - (g : forall x : A', B' x) - (a : A) - (b : A') - (H2 : f == g) - (H3 : a == b), - let L1 : A == A' := type_eq H3, - L2 : A' == A := symm L1, - b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b, - L4 : a == b' := htrans H3 L3, - L5 : f a == f b' := congr2 f L4 - in L5 diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out deleted file mode 100644 index 88450f4e5..000000000 --- a/tests/lean/norm_bug1.lean.expected.out +++ /dev/null @@ -1,32 +0,0 @@ - Set: pp::colors - Set: pp::unicode - Imported 'cast' - Set: pp::colors -λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast_eq L2 b in L3 : - ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b -λ (A A' : TypeM) - (B : A → TypeM) - (B' : A' → TypeM) - (f : ∀ x : A, B x) - (g : ∀ x : A', B' x) - (a : A) - (b : A') - (H2 : f == g) - (H3 : a == b), - let L1 : A == A' := type_eq H3, - L2 : A' == A := symm L1, - b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b, - L4 : a == b' := htrans H3 L3, - L5 : f a == f b' := congr2 f L4 - in L5 : - ∀ (A A' : TypeM) - (B : A → TypeM) - (B' : A' → TypeM) - (f : ∀ x : A, B x) - (g : ∀ x : A', B' x) - (a : A) - (b : A') - (H2 : f == g) - (H3 : a == b), - f a == f (cast (symm (type_eq H3)) b) diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out index 3a2e3c11f..d55ad4ef5 100644 --- a/tests/lean/tst1.lean.expected.out +++ b/tests/lean/tst1.lean.expected.out @@ -26,7 +26,7 @@ definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n := λ (i : N) (H : i < n), f (v1 i H) (v2 i H) select (update (const three ⊥) two ⊤) two two_lt_three : Bool -if (two == two) then ⊤ else ⊥ +if (two = two) then ⊤ else ⊥ update (const three ⊥) two ⊤ : vector Bool three -------- @@ -46,4 +46,4 @@ map normal form --> f (v1 i H) (v2 i H) update normal form --> -λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) then d else v j H +λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j = i) then d else v j H diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out index 02af3b075..9830b2040 100644 --- a/tests/lean/tst11.lean.expected.out +++ b/tests/lean/tst11.lean.expected.out @@ -6,7 +6,7 @@ ⊤ Assumed: a a ⊕ a ⊕ a -@subst : ∀ (A : TypeU) (a b : A) (P : A → Bool), P a → a = b → P b +@subst : ∀ (A : TypeU') (a b : A) (P : A → Bool), P a → a = b → P b Proved: EM2 EM2 : ∀ a : Bool, a ∨ ¬ a EM2 a : a ∨ ¬ a diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out index 6c7a9feea..81e287196 100644 --- a/tests/lean/tst17.lean.expected.out +++ b/tests/lean/tst17.lean.expected.out @@ -4,4 +4,4 @@ Assumed: g ∀ a b : Type, ∃ c : Type, g a b = f c ∀ a b : Type, ∃ c : Type, g a b = f c : Bool -∀ (a b : Type), (∀ (x : Type), g a b == f x → ⊥) → ⊥ +∀ (a b : Type), (∀ (x : Type), g a b = f x → ⊥) → ⊥ diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out index 54c801e6f..71a1b8a37 100644 --- a/tests/lean/tst4.lean.expected.out +++ b/tests/lean/tst4.lean.expected.out @@ -10,9 +10,7 @@ Assumed: EqNice @EqNice N n1 n2 @f N n1 n2 : N -@congr : - ∀ (A : TypeU) (B : A → TypeU) (f g : ∀ x : A, B x) (a b : A), - @eq (∀ x : A, B x) f g → @eq A a b → f a == g b +@congr : ∀ (A B : TypeU') (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b) @f N n1 n2 Assumed: a Assumed: b @@ -23,7 +21,7 @@ axiom H1 : @eq N a b ∧ @eq N b c theorem Pr : @eq N (g a) (g c) := @congr N - (λ x : N, N) + N g g a diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index 637330a1a..2470132f0 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -6,7 +6,7 @@ Set: lean::pp::implicit variable h : N → N → N theorem congrH {a1 a2 b1 b2 : N} (H1 : @eq N a1 b1) (H2 : @eq N a2 b2) : @eq N (h a1 a2) (h b1 b2) := - @congr N (λ x : N, N) (h a1) (h b1) a2 b2 (@congr N (λ x : N, N → N) h h a1 b1 (@refl (N → N → N) h) H1) H2 + @congr N N (h a1) (h b1) a2 b2 (@congr N (N → N) h h a1 b1 (@refl (N → N → N) h) H1) H2 Set: lean::pp::implicit variable h : N → N → N theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 b2 := congr (congr (refl h) H1) H2 @@ -15,7 +15,7 @@ theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 theorem Example1 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @eq N d c) : @eq N (h a b) (h c b) := @or_elim (@eq N a b ∧ @eq N b c) (@eq N a d ∧ @eq N d c) - (h a b == h c b) + (@eq N (h a b) (h c b)) H (λ H1 : @eq N a b ∧ @eq N b c, @congrH a diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean deleted file mode 100644 index 034596783..000000000 --- a/tests/lean/type_inf_bug1.lean +++ /dev/null @@ -1,34 +0,0 @@ -import cast -set_option pp::colors false - -check fun (A A': TypeM) - (a : A) - (b : A') - (L2 : A' == A), - let b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b - in L3 - -check fun (A A': TypeM) - (B : A -> TypeM) - (B' : A' -> TypeM) - (f : forall x : A, B x) - (g : forall x : A', B' x) - (a : A) - (b : A') - (H1 : (forall x : A, B x) == (forall x : A', B' x)) - (H2 : f == g) - (H3 : a == b), - let L1 : A == A' := type_eq H3, - L2 : A' == A := symm L1, - b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b, - L4 : a == b' := htrans H3 L3, - L5 : f a == f b' := congr2 f L4, - S1 : (forall x : A', B' x) == (forall x : A, B x) := symm H1, - g' : (forall x : A, B x) := cast S1 g, - L6 : g == g' := cast_eq S1 g, - L7 : f == g' := htrans H2 L6, - L8 : f b' == g' b' := congr1 b' L7, - L9 : f a == g' b' := htrans L5 L8 - in L9 diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out deleted file mode 100644 index 83a7a90ef..000000000 --- a/tests/lean/type_inf_bug1.lean.expected.out +++ /dev/null @@ -1,40 +0,0 @@ - Set: pp::colors - Set: pp::unicode - Imported 'cast' - Set: pp::colors -λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast_eq L2 b in L3 : - ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b -λ (A A' : TypeM) - (B : A → TypeM) - (B' : A' → TypeM) - (f : ∀ x : A, B x) - (g : ∀ x : A', B' x) - (a : A) - (b : A') - (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) - (H2 : f == g) - (H3 : a == b), - let L1 : A == A' := type_eq H3, - L2 : A' == A := symm L1, - b' : A := cast L2 b, - L3 : b == b' := cast_eq L2 b, - L4 : a == b' := htrans H3 L3, - L5 : f a == f b' := congr2 f L4, - S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm H1, - g' : ∀ x : A, B x := cast S1 g, - L6 : g == g' := cast_eq S1 g, - L7 : f == g' := htrans H2 L6, - L8 : f b' == g' b' := congr1 b' L7, - L9 : f a == g' b' := htrans L5 L8 - in L9 : - ∀ (A A' : TypeM) - (B : A → TypeM) - (B' : A' → TypeM) - (f : ∀ x : A, B x) - (g : ∀ x : A', B' x) - (a : A) - (b : A') - (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) - (H2 : f == g) - (H3 : a == b), - f a == cast (symm H1) g (cast (symm (type_eq H3)) b) diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index ba12b6823..be3ffef34 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -25,8 +25,9 @@ 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", HEq(iVal(0), iVal(0)), Const("trivial")) -child:add_axiom("H1", HEq(Const("x"), iVal(0))) +local Int = Const("Int") +child:add_theorem("Th1", mk_eq(Int, iVal(0), iVal(0)), Const("trivial")) +child:add_axiom("H1", mk_eq(Int, 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)) diff --git a/tests/lua/expr5.lua b/tests/lua/expr5.lua index 70f33e198..c4eb92b92 100644 --- a/tests/lua/expr5.lua +++ b/tests/lua/expr5.lua @@ -3,7 +3,6 @@ n = e:get_body() check_error(function() mk_heq(n, Const("a")) end) print(Const("a") < Const("b")) check_error(function() mk_app(Const("a")) end) -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"))) diff --git a/tests/lua/expr6.lua b/tests/lua/expr6.lua index 6124dd912..5dffe0b8b 100644 --- a/tests/lua/expr6.lua +++ b/tests/lua/expr6.lua @@ -22,10 +22,6 @@ 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.HEq then - local lhs, rhs = e:fields() - print_leaves(lhs, ctx) - print_leaves(rhs, ctx) elseif k == expr_kind.Let then local name, ty, val, body = e:fields() print("let var name: " .. tostring(name)) @@ -43,6 +39,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), HEq(f(x), h(x)))) + Let(x, h(a), mk_eq(N, f(x), h(x)))) print(F) print_leaves(F, context()) diff --git a/tests/lua/expr8.lua b/tests/lua/expr8.lua index 4b9257c8b..9be9c8907 100644 --- a/tests/lua/expr8.lua +++ b/tests/lua/expr8.lua @@ -25,7 +25,6 @@ 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(HEq(a, b):is_heq()) assert(F:num_args() == 3) assert(F:arg(0) == f) assert(F:arg(1) == g(x, a)) diff --git a/tests/lua/is_prop1.lua b/tests/lua/is_prop1.lua index b48369629..472b0cdf6 100644 --- a/tests/lua/is_prop1.lua +++ b/tests/lua/is_prop1.lua @@ -21,7 +21,7 @@ assert(env:is_proposition(parse_lean([[true -> false]]))) assert(env:is_proposition(parse_lean([[Nat -> false]]))) assert(not env:is_proposition(parse_lean([[true -> Nat]]))) assert(not env:is_proposition(parse_lean([[Type]]))) -assert(env:is_proposition(parse_lean([[0 == 1]]))) +assert(env:is_proposition(parse_lean([[0 = 1]]))) assert(env:is_proposition(parse_lean([[q]]))) diff --git a/tests/lua/unify1.lua b/tests/lua/unify1.lua index 978e69396..82e7a50a3 100644 --- a/tests/lua/unify1.lua +++ b/tests/lua/unify1.lua @@ -16,7 +16,6 @@ function must_unify(t1, t2) assert(s:apply(t1) == s:apply(t2)) end Bool = Const("Bool") -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))