Long runtime on dag-like terms

[gebner]

Since a few weeks ago, the proof for the char.zero_lt_d800 theorem in the core library has almost a trillion subterms if we count them as a tree:

open expr native

attribute [inline] bool.decidable_eq state.monad return

section
local attribute [inline] cmp cmp_using expr.decidable_rel
meta def mk_fast_expr_map {α} : rb_map expr α :=
rb_map.mk_core _ cmp
end

meta def expr.daglike_size (e : expr) : ℕ :=
let empty_set : rb_set expr := mk_fast_expr_map in
(e.fold empty_set $ λ e _ sts, sts.insert e).size

@[inline] private meta def set_size {α β} (a : α) (b : β) : state (rb_map α β) β :=
do m ← state.read, state.write $ m.insert a b, return b

private meta def treelike_size_core : expr → state (rb_map expr ℕ) ℕ | e :=
do m ← state.read, match m.find e with some s := return s | none := match e with
| (app a b) := do sa ← treelike_size_core a, sb ← treelike_size_core b, return $ sa + sb
| (elet _ t v b) := do st ← treelike_size_core t, sv ← treelike_size_core v,
                       sb ← treelike_size_core b, return $ st + sv + sb
| (pi _ _ d b) := do sd ← treelike_size_core d, sb ← treelike_size_core b, return $ sd + sb
| (lam _ _ d b) := do sd ← treelike_size_core d, sb ← treelike_size_core b, return $ sd + sb
| e := return 1
end >>= set_size e end

meta def expr.treelike_size (e : expr) : ℕ :=
(treelike_size_core e mk_fast_expr_map).1

#eval `(5+5+5+5+5+5+5).daglike_size
#eval `(5+5+5+5+5+5+5).treelike_size

open tactic

#eval do env ← get_env, decl ← returnex $ env.get ``char.zero_lt_d800,
trace $ "dag-like subterms: " ++ repr decl.value.daglike_size,
trace $ "tree-like subterms: " ++ repr (decl.value.treelike_size / 10^9) ++ " billion"
-- dag-like subterms: 344
-- tree-like subterms: 761 billion

Accordingly, tc fails to type-check this theorem in reasonable time (I waited for 10 minutes although I suspect it would take much much longer). I have put the exported text file in a gist: lean init/data/char/basic.lean --export=char_zero_lt_d800.txt --only-export=char.zero_lt_d800.

[leodemoura]

Smart unfolding has indirectly fixed this issue. char.zero_lt_d800 proof is now really small when we count it as a tree. To elaborate this lemma, we have to solve the unification problem

succ ?x =?= 0xd800

which requires us to unfold bit0, bit1, add and nat.add. Before smart unfolding, when we had to unfold a nat.add application, we would expose the internal recursors used to compile nat.add, and get an ugly term. Now, with smart unfolding, we get the following solution:

?x := 
(nat.add 27648
     (nat.add 13824
        (nat.add 6912
           (nat.add 3456
              (nat.add 1728
                 (nat.add 864 (nat.add 432 (nat.add 216 (nat.add 108 (nat.add 54 (nat.add 27 (nat.add 26 0))))))))))))

We can produce the original ugly proof using:

set_option type_context.smart_unfolding false
lemma bad_zero_lt_d800 : 0 < 0xd800 :=
nat.zero_lt_succ _

[leodemoura]

Remark: even with smart unfolding and a smaller zero_lt_d800, tc still has to check that the following two terms are definitionally equal:

succ
(nat.add 27648
     (nat.add 13824
        (nat.add 6912
           (nat.add 3456
              (nat.add 1728
                 (nat.add 864 (nat.add 432 (nat.add 216 (nat.add 108 (nat.add 54 (nat.add 27 (nat.add 26 0))))))))))))
=?=
0xd800

One may argue that we should not have proofs that generate this kind of check in the init folder, since a simple type checker will not be able to verify them. The tactic.comp_val generates a proof that is much easier to check. However, we cannot use it here since the tactic framework has not been defined yet. A possible workaround is to just copy the proof generated by tactic.comp_val.

lemma zero_lt_d800 : 0 < 0xd800 :=
nat.zero_lt_bit0 $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $
nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $
nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit0_ne_zero $ nat.bit1_ne_zero 13