michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add support for disequalities in calculational proofs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-02 22:47:45 -08:00
parent 6329d1828d
commit cf35e7bed7
3 changed files with 26 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/builtin/kernel.lean
View file

@ -177,6 +177,15 @@ Theorem Refute {a : Bool} (H : ¬ a → false) : a
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. := 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 Theorem Trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c
:= Subst H1 H2. := Subst H1 H2.

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

22
src/frontends/lean/parser_calc.cpp
View file

@ -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); 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() { calc_proof_parser::calc_proof_parser() {
expr imp = mk_implies_fn(); expr imp = mk_implies_fn();
expr eq = mk_homo_eq_fn(); expr eq = mk_homo_eq_fn();
expr iff = mk_iff_fn(); expr iff = mk_iff_fn();
expr neq = mk_constant(g_neq);
add_supported_operator(op_data(imp, 2)); add_supported_operator(op_data(imp, 2));
add_supported_operator(op_data(eq, 3)); add_supported_operator(op_data(eq, 3));
add_supported_operator(op_data(iff, 2)); 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, eq, trans_data(mk_trans_fn(), 6, eq));
add_trans_step(eq, imp, trans_data(mk_constant("EqImpTrans"), 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("ImpEqTrans"), 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("ImpTrans"), 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, iff, trans_data(mk_trans_fn(), 6, iff));
add_trans_step(iff, imp, trans_data(mk_constant("EqImpTrans"), 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("ImpEqTrans"), 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(eq, iff, trans_data(mk_trans_fn(), 6, iff));
add_trans_step(iff, eq, 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<expr> calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const { optional<expr> calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const {