dec_trivial slow

Stream: new members

[Bjørn Kjos-Hanssen]

The following Python code finishes in a quarter of a second:

for x in range(100):
    for y in range(100):
        for z in range(100):
            if (143 * x + 91 * y + 77 * z == 2692) and not (x == 6 and y == 10 and z == 12):
                print("Counterexample")

Now, let's try it in Lean:

import algebra.ring.boolean_ring
example:
    ∀ x : fin 10, ∀ y: fin 10,  ∀ z : fin 10,
    143 * x.1 + 91 * y.1 + 77 * z.1 = 2692 ↔ x.1 = 6 ∧ y.1 = 10 ∧ z.1 = 12
:= dec_trivial

Takes forever. What am I missing?

[Kyle Miller]

The Python one evaluates by using a relatively efficient bytecode interpreter but is not a verified computation, but the Lean one (if it terminates) yields a proof while using a much less efficient computation strategy.

[Kyle Miller]

I haven't tested it, but I would expect the following to evaluate relatively quickly:

#eval ((∀ x : fin 10, ∀ y: fin 10,  ∀ z : fin 10,
    143 * x.1 + 91 * y.1 + 77 * z.1 = 2692 ↔ x.1 = 6 ∧ y.1 = 10 ∧ z.1 = 12) : bool)

This is using a more Python-like evaluation (using the VM compiler), and you can't trust the result in the same way as with the example.

[Bjørn Kjos-Hanssen]

Thanks @Kyle Miller That was indeed very fast. If I include the eval in a Lean file I guess it's a "semi-formal" proof :smile:

[Jireh Loreaux]

Untested: is by intros x y z, fin_cases x; fin_cases y; fin_cases z; norm_num faster than dec_trivial?

[Bjørn Kjos-Hanssen]

@Jireh Loreaux thanks that's interesting although it also runs slowly for me.

[Jireh Loreaux]

Yeah, any actual proof will almost certainly be slower than #eval, I was just wondering if it was much faster than dec_trivial.