diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index deba26840..3509b2abf 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -29,11 +29,15 @@ Infix 50 > : gt. Definition id (a : Nat) := a. Notation 55 | _ | : id. +Axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b Axiom PlusZero (a : Nat) : a + 0 = a. Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1. -Axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b +Axiom MulZero (a : Nat) : a * 0 = 0. +Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a. Axiom Induction {P : Nat → Bool} (Hb : P 0) (Hi : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a. +Theorem ZeroNeOne : 0 ≠ 1 := Trivial. + Theorem ZeroPlus (a : Nat) : 0 + a = a := Induction (show 0 + 0 = 0, Trivial) (λ (n : Nat) (Hi : 0 + n = n), @@ -76,7 +80,97 @@ Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c in show (n + 1) + (b + c) = ((n + 1) + b) + c, Trans L2 L6) a. -Theorem ZeroNeOne : 0 ≠ 1 := Trivial. +Theorem ZeroMul (a : Nat) : 0 * a = 0 +:= Induction (show 0 * 0 = 0, Trivial) + (λ (n : Nat) (Hi : 0 * n = 0), + let L1 : 0 * (n + 1) = (0 * n) + 0 := MulSucc 0 n, + L2 : 0 * (n + 1) = 0 + 0 := Subst L1 Hi + in show 0 * (n + 1) = 0, L2) + a. + +Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b +:= Induction (show (a + 1) * 0 = a * 0 + 0, + Trans (MulZero (a + 1)) (Symm (Subst (PlusZero (a * 0)) (MulZero a)))) + (λ (n : Nat) (Hi : (a + 1) * n = a * n + n), + let L1 : (a + 1) * (n + 1) = (a + 1) * n + (a + 1) := MulSucc (a + 1) n, + L2 : (a + 1) * (n + 1) = a * n + n + (a + 1) := Subst L1 Hi, + L3 : a * n + n + (a + 1) = a * n + n + a + 1 := PlusAssoc (a * n + n) a 1, + L4 : a * n + n + a = a * n + (n + a) := Symm (PlusAssoc (a * n) n a), + L5 : a * n + n + (a + 1) = a * n + (n + a) + 1 := Subst L3 L4, + L6 : a * n + n + (a + 1) = a * n + (a + n) + 1 := Subst L5 (PlusComm n a), + L7 : a * n + (a + n) = a * n + a + n := PlusAssoc (a * n) a n, + L8 : a * n + n + (a + 1) = a * n + a + n + 1 := Subst L6 L7, + L9 : a * n + a = a * (n + 1) := Symm (MulSucc a n), + L10 : a * n + n + (a + 1) = a * (n + 1) + n + 1 := Subst L8 L9, + L11 : a * (n + 1) + n + 1 = a * (n + 1) + (n + 1) := Symm (PlusAssoc (a * (n + 1)) n 1) + in show (a + 1) * (n + 1) = a * (n + 1) + (n + 1), + Trans (Trans L2 L10) L11) + b. + +Theorem OneMul (a : Nat) : 1 * a = a +:= Induction (show 1 * 0 = 0, Trivial) + (λ (n : Nat) (Hi : 1 * n = n), + let L1 : 1 * (n + 1) = 1 * n + 1 := MulSucc 1 n + in show 1 * (n + 1) = n + 1, Subst L1 Hi) + a. + +Theorem MulOne (a : Nat) : a * 1 = a +:= Induction (show 0 * 1 = 0, Trivial) + (λ (n : Nat) (Hi : n * 1 = n), + let L1 : (n + 1) * 1 = n * 1 + 1 := SuccMul n 1 + in show (n + 1) * 1 = n + 1, Subst L1 Hi) + a. + +Theorem MulComm (a b : Nat) : a * b = b * a +:= Induction (show a * 0 = 0 * a, Trans (MulZero a) (Symm (ZeroMul a))) + (λ (n : Nat) (Hi : a * n = n * a), + let L1 : a * (n + 1) = a * n + a := MulSucc a n, + L2 : (n + 1) * a = n * a + a := SuccMul n a, + L3 : (n + 1) * a = a * n + a := Subst L2 (Symm Hi) + in show a * (n + 1) = (n + 1) * a, Trans L1 (Symm L3)) + b. + + +Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c +:= Induction (let L1 : 0 * (b + c) = 0 := ZeroMul (b + c), + L2 : 0 * b + 0 * c = 0 + 0 := Subst (Subst (Refl (0 * b + 0 * c)) (ZeroMul b)) (ZeroMul c), + L3 : 0 + 0 = 0 := Trivial + in show 0 * (b + c) = 0 * b + 0 * c, Trans L1 (Symm (Trans L2 L3))) + (λ (n : Nat) (Hi : n * (b + c) = n * b + n * c), + let L1 : (n + 1) * (b + c) = n * (b + c) + (b + c) := SuccMul n (b + c), + L2 : (n + 1) * (b + c) = n * b + n * c + (b + c) := Subst L1 Hi, + L3 : n * b + n * c + (b + c) = n * b + n * c + b + c := PlusAssoc (n * b + n * c) b c, + L4 : n * b + n * c + b = n * b + (n * c + b) := Symm (PlusAssoc (n * b) (n * c) b), + L5 : n * b + n * c + b = n * b + (b + n * c) := Subst L4 (PlusComm (n * c) b), + L6 : n * b + (b + n * c) = n * b + b + n * c := PlusAssoc (n * b) b (n * c), + L7 : n * b + (b + n * c) = (n + 1) * b + n * c := Subst L6 (Symm (SuccMul n b)), + L8 : n * b + n * c + b = (n + 1) * b + n * c := Trans L5 L7, + L9 : n * b + n * c + (b + c) = (n + 1) * b + n * c + c := Subst L3 L8, + L10 : (n + 1) * b + n * c + c = (n + 1) * b + (n * c + c) := Symm (PlusAssoc ((n + 1) * b) (n * c) c), + L11 : (n + 1) * b + n * c + c = (n + 1) * b + (n + 1) * c := Subst L10 (Symm (SuccMul n c)), + L12 : n * b + n * c + (b + c) = (n + 1) * b + (n + 1) * c := Trans L9 L11 + in show (n + 1) * (b + c) = (n + 1) * b + (n + 1) * c, + Trans L2 L12) + a. + +Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c +:= let L1 : (a + b) * c = c * (a + b) := MulComm (a + b) c, + L2 : c * (a + b) = c * a + c * b := Distribute c a b, + L3 : (a + b) * c = c * a + c * b := Trans L1 L2 + in Subst (Subst L3 (MulComm c a)) (MulComm c b). + +Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c +:= Induction (let L1 : 0 * (b * c) = 0 := ZeroMul (b * c), + L2 : 0 * b * c = 0 * c := Subst (Refl (0 * b * c)) (ZeroMul b), + L3 : 0 * c = 0 := ZeroMul c + in show 0 * (b * c) = 0 * b * c, Trans L1 (Symm (Trans L2 L3))) + (λ (n : Nat) (Hi : n * (b * c) = n * b * c), + let L1 : (n + 1) * (b * c) = n * (b * c) + (b * c) := SuccMul n (b * c), + L2 : (n + 1) * (b * c) = n * b * c + (b * c) := Subst L1 Hi, + L3 : n * b * c + (b * c) = (n * b + b) * c := Symm (Distribute2 (n * b) b c), + L4 : n * b * c + (b * c) = (n + 1) * b * c := Subst L3 (Symm (SuccMul n b)) + in show (n + 1) * (b * c) = (n + 1) * b * c, Trans L2 L4) + a. SetOpaque ge true. SetOpaque lt true. diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 8bdb60f05..b5e571a5f 100644 Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index ad444dd34..93530aeaf 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 66fb0e063..a3733efbd 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(library kernel_bindings.cpp deep_copy.cpp max_sharing.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp - fo_unify.cpp bin_op.cpp) + fo_unify.cpp bin_op.cpp eq_heq.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index bd6ce6815..17d4cb59d 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "kernel/type_checker.h" #include "kernel/update_expr.h" +#include "library/eq_heq.h" #include "library/elaborator/elaborator.h" #include "library/elaborator/elaborator_justification.h" @@ -1318,6 +1319,36 @@ class elaborator::imp { r = process_metavar(c, b, a, false); if (r != Continue) { return r == Processed; } + if (is_eq_heq(a) && is_eq_heq(b)) { + expr_pair p1 = eq_heq_args(a); + expr_pair p2 = eq_heq_args(b); + justification new_jst(new destruct_justification(c)); + push_new_eq_constraint(ctx, p1.first, p2.first, new_jst); + push_new_eq_constraint(ctx, p1.second, p2.second, new_jst); + return true; + } + + if (a.kind() == b.kind()) { + switch (a.kind()) { + case expr_kind::Pi: { + justification new_jst(new destruct_justification(c)); + push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); + context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); + push_new_constraint(eq, new_ctx, abst_body(a), abst_body(b), new_jst); + return true; + } + case expr_kind::Lambda: { + justification new_jst(new destruct_justification(c)); + push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); + context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); + push_new_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst); + return true; + } + default: + break; + } + } + if (!is_meta_app(a) && !is_meta_app(b) && normalize_head(a, b, c)) { return true; } if (!eq) { @@ -1361,26 +1392,6 @@ class elaborator::imp { m_conflict = justification(new unification_failure_justification(c)); return false; } - case expr_kind::Eq: { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_jst); - push_new_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_jst); - return true; - } - case expr_kind::Pi: { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); - context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); - push_new_constraint(eq, new_ctx, abst_body(a), abst_body(b), new_jst); - return true; - } - case expr_kind::Lambda: { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); - context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); - push_new_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst); - return true; - } case expr_kind::App: if (!is_meta_app(a) && !is_meta_app(b)) { if (num_args(a) == num_args(b)) { diff --git a/src/library/eq_heq.cpp b/src/library/eq_heq.cpp new file mode 100644 index 000000000..fb0098610 --- /dev/null +++ b/src/library/eq_heq.cpp @@ -0,0 +1,22 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/expr_pair.h" +#include "kernel/builtin.h" + +namespace lean { +bool is_eq_heq(expr const & e) { + return is_eq(e) || is_homo_eq(e); +} + +expr_pair eq_heq_args(expr const & e) { + lean_assert(is_eq(e) || is_homo_eq(e)); + if (is_eq(e)) + return expr_pair(eq_lhs(e), eq_rhs(e)); + else + return expr_pair(arg(e, 2), arg(e, 3)); +} +} diff --git a/src/library/eq_heq.h b/src/library/eq_heq.h new file mode 100644 index 000000000..5b92bbda8 --- /dev/null +++ b/src/library/eq_heq.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/expr_pair.h" + +namespace lean { +bool is_eq_heq(expr const & e); +expr_pair eq_heq_args(expr const & e); +} diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp index f2088a346..3e29fb3d5 100644 --- a/src/library/fo_unify.cpp +++ b/src/library/fo_unify.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/fo_unify.h" #include "library/expr_pair.h" #include "library/kernel_bindings.h" +#include "library/eq_heq.h" namespace lean { static void assign(substitution & s, expr const & mvar, expr const & e) { @@ -20,18 +21,6 @@ static bool is_metavar_wo_local_context(expr const & e) { return is_metavar(e) && !metavar_lctx(e); } -static bool is_eq_heq(expr const & e) { - return is_eq(e) || is_homo_eq(e); -} - -static expr_pair eq_heq_args(expr const & e) { - lean_assert(is_eq(e) || is_homo_eq(e)); - if (is_eq(e)) - return expr_pair(eq_lhs(e), eq_rhs(e)); - else - return expr_pair(arg(e, 2), arg(e, 3)); -} - optional fo_unify(expr e1, expr e2) { substitution s; unsigned i1, i2;