diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 1e442e053..7086b72c4 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -177,6 +177,15 @@ Theorem Refute {a : Bool} (H : ¬ a → false) : a Theorem Symm {A : TypeU} {a b : A} (H : a == b) : b == a := Subst (Refl a) H. +Theorem NeSymm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a +:= assume H1 : b = a, MP H (Symm H1). + +Theorem EqNeTrans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c +:= Subst H2 (Symm H1). + +Theorem NeEqTrans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c +:= Subst H1 H2. + Theorem Trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c := Subst H1 H2. diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 69ecb664d..12ef425d3 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index 3868b0457..124afe443 100644 --- a/src/frontends/lean/parser_calc.cpp +++ b/src/frontends/lean/parser_calc.cpp @@ -44,22 +44,34 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans m_trans_ops.emplace_front(op1, op2, d); } +static name g_eq_imp_trans("EqImpTrans"); +static name g_imp_eq_trans("ImpEqTrans"); +static name g_imp_trans("ImpTrans"); +static name g_eq_ne_trans("EqNeTrans"); +static name g_ne_eq_trans("NeEqTrans"); +static name g_neq("neq"); + calc_proof_parser::calc_proof_parser() { expr imp = mk_implies_fn(); expr eq = mk_homo_eq_fn(); expr iff = mk_iff_fn(); + expr neq = mk_constant(g_neq); + add_supported_operator(op_data(imp, 2)); add_supported_operator(op_data(eq, 3)); add_supported_operator(op_data(iff, 2)); + add_supported_operator(op_data(neq, 3)); add_trans_step(eq, eq, trans_data(mk_trans_fn(), 6, eq)); - add_trans_step(eq, imp, trans_data(mk_constant("EqImpTrans"), 5, imp)); - add_trans_step(imp, eq, trans_data(mk_constant("ImpEqTrans"), 5, imp)); - add_trans_step(imp, imp, trans_data(mk_constant("ImpTrans"), 5, imp)); + add_trans_step(eq, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp)); + add_trans_step(imp, eq, trans_data(mk_constant(g_imp_eq_trans), 5, imp)); + add_trans_step(imp, imp, trans_data(mk_constant(g_imp_trans), 5, imp)); add_trans_step(iff, iff, trans_data(mk_trans_fn(), 6, iff)); - add_trans_step(iff, imp, trans_data(mk_constant("EqImpTrans"), 5, imp)); - add_trans_step(imp, iff, trans_data(mk_constant("ImpEqTrans"), 5, imp)); + add_trans_step(iff, imp, trans_data(mk_constant(g_eq_imp_trans), 5, imp)); + add_trans_step(imp, iff, trans_data(mk_constant(g_imp_eq_trans), 5, imp)); add_trans_step(eq, iff, trans_data(mk_trans_fn(), 6, iff)); add_trans_step(iff, eq, trans_data(mk_trans_fn(), 6, iff)); + add_trans_step(eq, neq, trans_data(mk_constant(g_eq_ne_trans), 6, neq)); + add_trans_step(neq, eq, trans_data(mk_constant(g_ne_eq_trans), 6, neq)); } optional calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const {