feat(builtin/Nat): multiplication axioms and theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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.

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})

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)) {

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));
+}
+}

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);
+}

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<substitution> fo_unify(expr e1, expr e2) {
     substitution s;
     unsigned i1, i2;