fix(hott,frontends/lean,library,library/tactic): make sure we can still compile the HoTT library

hott/algebra/category/constructions/discrete.hlean

@@ -14,8 +14,7 @@ open eq is_trunc iso bool functor
 namespace category
 
   definition precategory_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : precategory A :=
-  precategory.mk
-    (λ (a b : A), a = b)
+  @precategory.mk _ _ (@is_trunc_eq _ _ H)
     (λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p)
     (λ (a : A), refl a)
     (λ (a b c d : A) (p : c = d) (q : b = c) (r : a = b), con.assoc r q p)

hott/algebra/group.hlean

@@ -19,15 +19,6 @@ variable {A : Type}
 structure has_mul [class] (A : Type) :=
 (mul : A → A → A)
 
-structure has_add [class] (A : Type) :=
-(add : A → A → A)
-
-structure has_one [class] (A : Type) :=
-(one : A)
-
-structure has_zero [class] (A : Type) :=
-(zero : A)
-
 structure has_inv [class] (A : Type) :=
 (inv : A → A)
 

hott/init/default.hlean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jakob von Raumer
 
 prelude
 import init.datatypes init.reserved_notation init.tactic init.logic
-import init.bool init.num init.priority init.relation init.wf
+import init.bool init.num init.relation init.wf
 import init.types
 import init.trunc init.path init.equiv init.util
 import init.ua init.funext

hott/init/num.hlean

@@ -12,28 +12,6 @@ definition pos_num.is_inhabited [instance] : inhabited pos_num :=
 inhabited.mk pos_num.one
 
 namespace pos_num
-  definition is_one (a : pos_num) : bool :=
-  pos_num.rec_on a tt (λn r, ff) (λn r, ff)
-
-  definition pred (a : pos_num) : pos_num :=
-  pos_num.rec_on a one (λn r, bit0 n) (λn r, cond (is_one n) one (bit1 r))
-
-  definition size (a : pos_num) : pos_num :=
-  pos_num.rec_on a one (λn r, succ r) (λn r, succ r)
-
-  definition add (a b : pos_num) : pos_num :=
-  pos_num.rec_on a
-    succ
-    (λn f b, pos_num.rec_on b
-      (succ (bit1 n))
-      (λm r, succ (bit1 (f m)))
-      (λm r, bit1 (f m)))
-    (λn f b, pos_num.rec_on b
-      (bit1 n)
-      (λm r, bit1 (f m))
-      (λm r, bit0 (f m)))
-    b
-
   notation a + b := add a b
 
   definition mul (a b : pos_num) : pos_num :=
@@ -80,9 +58,6 @@ namespace num
   definition size (a : num) : num :=
   num.rec_on a (pos one) (λp, pos (size p))
 
-  definition add (a b : num) : num :=
-  num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
-
   definition mul (a b : num) : num :=
   num.rec_on a zero (λpa, num.rec_on b zero (λpb, pos (pos_num.mul pa pb)))
 

hott/init/priority.hlean

@@ -1,9 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.datatypes
-definition std.priority.default : num := 1000
-definition std.priority.max     : num := 4294967295

hott/init/reserved_notation.hlean

@@ -9,6 +9,66 @@ import init.datatypes
 notation `assume` binders `,` r:(scoped f, f) := r
 notation `take`   binders `,` r:(scoped f, f) := r
 
+structure has_zero [class] (A : Type) := (zero : A)
+structure has_one [class] (A : Type) := (one : A)
+structure has_add [class] (A : Type)  := (add : A → A → A)
+
+definition zero [reducible] {A : Type} [s : has_zero A] : A := has_zero.zero A
+definition one  [reducible] {A : Type} [s : has_one A] : A := has_one.one A
+definition add  [reducible] {A : Type} [s : has_add A] : A → A → A := has_add.add
+definition bit0 [reducible] {A : Type} [s  : has_add A] (a  : A)                 : A := add a a
+definition bit1 [reducible] {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one
+
+definition num_has_zero [reducible] [instance] : has_zero num :=
+has_zero.mk num.zero
+
+definition num_has_one [reducible] [instance] : has_one num :=
+has_one.mk (num.pos pos_num.one)
+
+definition pos_num_has_one [reducible] [instance] : has_one pos_num :=
+has_one.mk (pos_num.one)
+
+namespace pos_num
+  open bool
+  definition is_one (a : pos_num) : bool :=
+  pos_num.rec_on a tt (λn r, ff) (λn r, ff)
+
+  definition pred (a : pos_num) : pos_num :=
+  pos_num.rec_on a one (λn r, bit0 n) (λn r, bool.rec_on (is_one n) (bit1 r) one)
+
+  definition size (a : pos_num) : pos_num :=
+  pos_num.rec_on a one (λn r, succ r) (λn r, succ r)
+
+  definition add (a b : pos_num) : pos_num :=
+  pos_num.rec_on a
+    succ
+    (λn f b, pos_num.rec_on b
+      (succ (bit1 n))
+      (λm r, succ (bit1 (f m)))
+      (λm r, bit1 (f m)))
+    (λn f b, pos_num.rec_on b
+      (bit1 n)
+      (λm r, bit1 (f m))
+      (λm r, bit0 (f m)))
+    b
+end pos_num
+
+definition pos_num_has_add [reducible] [instance] : has_add pos_num :=
+has_add.mk pos_num.add
+
+namespace num
+  open pos_num
+
+  definition add (a b : num) : num :=
+  num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
+end num
+
+definition num_has_add [reducible] [instance] : has_add num :=
+has_add.mk num.add
+
+definition std.priority.default : num := 1000
+definition std.priority.max     : num := 4294967295
+
 /-
   Global declarations of right binding strength
 
@@ -17,7 +77,6 @@ notation `take`   binders `,` r:(scoped f, f) := r
 
   When hovering over a symbol, use "C-c C-k" to see how to input it.
 -/
-
 definition std.prec.max   : num := 1024 -- the strength of application, identifiers, (, [, etc.
 definition std.prec.arrow : num := 25
 

hott/init/types.hlean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
 -/
 
 prelude
-import .num .wf
+import init.num init.wf
 
 -- Empty type
 -- ----------

src/frontends/lean/elaborator.cpp

@@ -1585,7 +1585,14 @@ expr elaborator::visit_prenum(expr const & e, constraint_seq & cs) {
     mpz const & v  = prenum_value(e);
     tag e_tag      = e.get_tag();
     levels ls      = levels(mk_meta_univ(m_ngen.next()));
-    expr A         = m_full_context.mk_meta(m_ngen, none_expr(), e_tag);
+    // Remark: In HoTT mode, we only partially support the new encoding for numerals.
+    // We fix A to num, and we rely on coercions to cast them to other types.
+    // This is quite different from the approach used in the standard library
+    expr A;
+    if (is_standard(env()))
+        A = m_full_context.mk_meta(m_ngen, none_expr(), e_tag);
+    else
+        A = mk_constant(get_num_name()).set_tag(e_tag);
     bool is_strict = true;
     bool inst_imp  = true;
     if (v.is_neg())

src/frontends/lean/notation_cmd.cpp

@@ -41,7 +41,14 @@ static unsigned parse_precedence_core(parser & p) {
     if (p.curr_is_numeral()) {
         return p.parse_small_nat();
     } else {
-        environment env = open_prec_aliases(p.env());
+        environment env = p.env();
+        if (!is_standard(env)) {
+            // TODO(Leo): remove this if we decide to implement
+            // arithmetical notation using type classes in the HoTT
+            // library.
+            env = open_num_notation(p.env());
+        }
+        env = open_prec_aliases(env);
         parser::local_scope scope(p, env);
         expr pre_val = p.parse_expr(get_max_prec());
         pre_val  = mk_typed_expr(mk_constant(get_num_name()), pre_val);

src/frontends/lean/parser.cpp

@@ -1537,17 +1537,32 @@ expr parser::parse_id() {
     return id_to_expr(id, p);
 }
 
-expr parser::parse_numeral_expr() {
+expr parser::parse_numeral_expr(bool user_notation) {
     auto p = pos();
     mpz n = get_num_val().get_numerator();
     next();
     if (!m_has_num)
         m_has_num = has_num_decls(m_env);
-    if (!*m_has_num) {
+    list<expr> vals;
+    if (user_notation)
+        vals = get_mpz_notation(m_env, n);
+    if (!*m_has_num && !vals) {
         throw parser_error("numeral cannot be encoded as expression, environment does not contain "
                            "the auxiliary declarations zero, one, bit0 and bit1", p);
     }
-    return mk_prenum(n);
+    if (!vals) {
+        return save_pos(mk_prenum(n), p);
+    } else {
+        buffer<expr> cs;
+        if (*m_has_num)
+            cs.push_back(save_pos(mk_prenum(n), p));
+        for (expr const & c : vals)
+            cs.push_back(copy_with_new_pos(c, p));
+        if (cs.size() == 1)
+            return cs[0];
+        else
+            return save_pos(mk_choice(cs.size(), cs.data()), p);
+    }
 }
 
 expr parser::parse_decimal_expr() {
@@ -1830,7 +1845,7 @@ expr parser::parse_tactic_opt_id_list() {
 expr parser::parse_tactic_option_num() {
     auto p = pos();
     if (curr_is_numeral()) {
-        expr n = parse_numeral_expr(); // TODO(Leo): it should be a num
+        expr n = parse_numeral_expr(false);
         return mk_app(save_pos(mk_constant(get_option_some_name()), p), n, p);
     } else {
         return save_pos(mk_constant(get_option_none_name()), p);

src/frontends/lean/parser.h

@@ -214,7 +214,7 @@ class parser {
     expr parse_led_notation(expr left);
     expr parse_nud();
     bool curr_starts_expr();
-    expr parse_numeral_expr();
+    expr parse_numeral_expr(bool user_notation = true);
     expr parse_decimal_expr();
     expr parse_string_expr();
     expr parse_binder_core(binder_info const & bi, unsigned rbp);

src/library/constants.cpp

@@ -36,6 +36,8 @@ name const * g_false_rec = nullptr;
 name const * g_funext = nullptr;
 name const * g_has_zero = nullptr;
 name const * g_has_one = nullptr;
+name const * g_has_zero_zero = nullptr;
+name const * g_has_one_one = nullptr;
 name const * g_has_add = nullptr;
 name const * g_heq = nullptr;
 name const * g_heq_refl = nullptr;
@@ -188,6 +190,8 @@ void initialize_constants() {
     g_funext = new name{"funext"};
     g_has_zero = new name{"has_zero"};
     g_has_one = new name{"has_one"};
+    g_has_zero_zero = new name{"has_zero", "zero"};
+    g_has_one_one = new name{"has_one", "one"};
     g_has_add = new name{"has_add"};
     g_heq = new name{"heq"};
     g_heq_refl = new name{"heq", "refl"};
@@ -341,6 +345,8 @@ void finalize_constants() {
     delete g_funext;
     delete g_has_zero;
     delete g_has_one;
+    delete g_has_zero_zero;
+    delete g_has_one_one;
     delete g_has_add;
     delete g_heq;
     delete g_heq_refl;
@@ -493,6 +499,8 @@ name const & get_false_rec_name() { return *g_false_rec; }
 name const & get_funext_name() { return *g_funext; }
 name const & get_has_zero_name() { return *g_has_zero; }
 name const & get_has_one_name() { return *g_has_one; }
+name const & get_has_zero_zero_name() { return *g_has_zero_zero; }
+name const & get_has_one_one_name() { return *g_has_one_one; }
 name const & get_has_add_name() { return *g_has_add; }
 name const & get_heq_name() { return *g_heq; }
 name const & get_heq_refl_name() { return *g_heq_refl; }

src/library/constants.h

@@ -38,6 +38,8 @@ name const & get_false_rec_name();
 name const & get_funext_name();
 name const & get_has_zero_name();
 name const & get_has_one_name();
+name const & get_has_zero_zero_name();
+name const & get_has_one_one_name();
 name const & get_has_add_name();
 name const & get_heq_name();
 name const & get_heq_refl_name();

src/library/constants.txt

@@ -31,6 +31,8 @@ false.rec
 funext
 has_zero
 has_one
+has_zero.zero
+has_one.one
 has_add
 heq
 heq.refl

src/library/num.cpp

@@ -112,4 +112,12 @@ optional<mpz> to_num_core(expr const & e) {
     else
         return optional<mpz>();
 }
+
+bool is_num_leaf_constant(name const & n) {
+    return
+        n == get_zero_name() ||
+        n == get_one_name() ||
+        n == get_has_zero_zero_name() ||
+        n == get_has_one_one_name();
+}
 }

src/library/num.h

@@ -33,6 +33,13 @@ optional<mpz> to_num(expr const & e);
 /** \brief If the given expression is a numeral encode the num and pos_num types, return the encoded numeral */
 optional<mpz> to_num_core(expr const & e);
 
+/** \brief Return true iff n is zero/one/has_zero.zero/has_one.one.
+    These constants are used to encode numerals, and some tactics may have to treat them in a special way.
+
+    \remark This kind of hard-coded solution is not ideal. One alternative solution is to have yet another
+    annotation to let user mark constants that should be treated in a different way by some tactics. */
+bool is_num_leaf_constant(name const & n);
+
 void initialize_num();
 void finalize_num();
 }

src/library/tactic/rewrite_tactic.cpp

@@ -490,19 +490,7 @@ public:
             constraint_seq cs;
             expr p1 = m_tc.whnf(p, cs);
             expr t1 = m_tc.whnf(t, cs);
-            if (!cs && (p1 != p || t1 != t) && ctx.match(p1, t1)) {
-                return true;
-            } else if (!has_expr_metavar(p1)) {
-                // special support for numerals
-                if (auto p2 = unfold_num_app(m_tc.env(), p1)) {
-                    // unfold nested projection
-                    if (auto p3 = unfold_app(m_tc.env(), *p2)) {
-                        p3 = m_tc.whnf(*p3, cs);
-                        return !cs && p1 != *p3 && ctx.match(*p3, t1);
-                    }
-                }
-            }
-            return false;
+            return !cs && (p1 != p || t1 != t) && ctx.match(p1, t1);
         } catch (exception&) {
             return false;
         }
@@ -1600,7 +1588,10 @@ class rewrite_fn {
         } else {
             auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_reducible_pred(m_env);
             return mk_simple_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) {
-                    return is_projection(m_env, n) || aux_pred(n);
+                    // Remark: the condition !is_num_leaf_constant(n) is a little bit hackish.
+                    // It is here to allow us to match terms such as (@zero nat nat_has_zero) with nat.zero.
+                    // The idea is to treat zero and has_zero.zero as reducible terms and unfold them here.
+                    return (is_projection(m_env, n) || aux_pred(n)) && !is_num_leaf_constant(n);
                 });
         }
     }