moving algebra out of core

Stream: general

[Johan Commelin]

Starting a new thread for this project.
Can someone explain me: when I build core

cd build/releases
cmake ../../src
make

How is this aware of any .lean files in core? I grepped through all the Makefiles, and they don't seem to mention lean files anywhere.

[Johan Commelin]

Or does it not care, but will you only notice once you run the tests if you've changed/moved a bunch of lean files?

[Yury G. Kudryashov]

Here is the relevant part of CMakeLists.txt:

add_custom_target(
    standard_lib ALL
    COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS}
    DEPENDS bin_lean
    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
    )

add_custom_target(
    leanpkg ALL
    COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS}
    DEPENDS standard_lib
    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../leanpkg"
)

[Yury G. Kudryashov]

It just runs this command. It doesn't care what it does.

[Johan Commelin]

/me should learn cmake

[Yury G. Kudryashov]

BTW, @Gabriel Ebner do you want me to look at lean buildsystem? A few years ago I contributed several patches to cmake and to KDE cmake files.

[Bryan Gin-ge Chen]

If you only plan to edit Lean files, you can just mess around in library after compiling a binary from the latest commit.

[Yury G. Kudryashov]

In particular, writing build files to source tree is generally a bad idea. If I have two build directories with different configuration, then I expect these two builds to be completely independent.

[Bryan Gin-ge Chen]

Oh, maybe this post by Jason will help? It could be an alternate way to play around with library without having to build Lean.

[Johan Commelin]

But I guess I will have to touch .cpp as well. Cut norm_num away.

[Yury G. Kudryashov]

What should core know about natural and integer numbers? Only definitions of operations? Something else?

[Johan Commelin]

lean#224 is the first step

[Johan Commelin]

That PR removes all the CPP involving norm_num.

[Johan Commelin]

A follow-up PR should strip most algebra from the core library. But that lean code is pretty tangled )-;

[Kenny Lau]

/me is somewhat surprised that Lean code is faster than cpp code

[Johan Commelin]

That's fine

[Gabriel Ebner]

Yury G. Kudryashov said:

BTW, Gabriel Ebner do you want me to look at lean buildsystem? A few years ago I contributed several patches to cmake and to KDE cmake files.

Are you talking about removing the part that copies lean to bin/lean? I've already gotten used to this horrible hack. I don't think that there's an immediate need to change it. See also previous discussion here: https://github.com/leanprover/lean/issues/1918

[Gabriel Ebner]

Yury G. Kudryashov said:

What should core know about natural and integer numbers? Only definitions of operations? Something else?

It needs a few lemmas for the equation compiler. If you write match n with 314 := a | 42 := b | _ := c end, then it needs to prove that 314 ≠ 42. The definitions of natural numbers (including exponentiation) are also required for the VM (because they are overriden) and the tactic framework.

[Mario Carneiro]

@Kenny Lau The reason it's faster is because the C++ is using instance search and norm_num is (now) aggressively caching. It turns out that actual number crunching was nothing compared to finding typeclasses

[Johan Commelin]

This is what we need to unclutter:
import_graph.pdf

[Johan Commelin]

@Mario Carneiro Do you know by heart whether something like init.meta.well_founded_tactics has to stay in core?

[Mario Carneiro]

that tactic is a mess, I'd like to see it gone

[Mario Carneiro]

it should be assumption

[Johan Commelin]

What does that mean for this project...

[Mario Carneiro]

It can definitely be removed from core

[Johan Commelin]

Ok, I'll try my best

[Mario Carneiro]

It is used by lean magic currently: if you leave off the using_well_founded clause in a well founded recursive definition, it will call the tactic in well_founded_tactics in order to solve the size decreasing theorem

[Mario Carneiro]

that needs to be changed to another tactic, and I recommend assumption

[Johan Commelin]

Does that mean a lot of proofs in mathlib will have to be fixed?

[Mario Carneiro]

It does mean a regression for well founded definitions that currently are using the tactic to prove the size decreasing theorem; they will need to put the using_well_founded clause in and reference well_founded_tactic explicitly

[Johan Commelin]

And does lean need to be changed before well_founded_tactics can be removed? You seem to suggest that lean depends on it.

[Mario Carneiro]

Well founded definitions like this are extremely rare in mathlib, and even when they are used the result isn't great, because it does recursion on T.sizeof which has few lemmas

[Mario Carneiro]

well_founded_tactics.default is referenced by lean

[Mario Carneiro]

and it uses default construction of well_founded_tactics, resulting in the use of well_founded_tactics.default_dec_tac

[Mario Carneiro]

So if you change the default value of well_founded_tactics.dec_tac to assumption, you should be able to remove default_dec_tac

[Mario Carneiro]

Another option is to use a def_replacer here, so that users can mark their own default dec_tac, changing the global default

[Johan Commelin]

This sounds orthogonal to norm_num, but maybe not to moving algebra out of core.

[Mario Carneiro]

well_founded_tactics.default_dec_tac is basically a poor man's linarith

[Johan Commelin]

lean#229 is a wip PR that compiles

[Johan Commelin]

I would like some advice on the way forward.

[Johan Commelin]

Previously init.data.nat.lemmas imported init.algebra.functions and hence the entire algebraic hierarchy in core.
Now init.algebra.functions only imports init.algebra.order, and hence init.algebra.{group,field,ordered_ring} etc can all be moved out of core.

[Johan Commelin]

I had to prove something like 20 lemmas specifically for nat and int that would otherwise follow from an ordered_(semi)ring instance.

[Kevin Buzzard]

Wow, so this really is the light at the end of the tunnel?

[Johan Commelin]

Also, nat now has a personal has_dvd instance, and int its own has_sub instance, because they can't get them from comm_semiring resp. add_group.

[Kevin Buzzard]

When you posted that graph earlier I was just thinking that this might be impossible

[Kevin Buzzard]

Nat also has its own has_pow instance though, and this causes lots of problems

[Johan Commelin]

But mine are defeq to what you would get otherwise

[Kevin Buzzard]

I was hoping you'd say that :-)

[Johan Commelin]

So, for lean#229 should I now remove all the init.algebra.* stuff from core? Or should I wait for a bit, so that people can look at what the PR looks like now?

[Yury G. Kudryashov]

For me, it would be easier to look at a version with deleted code (as opposed to commented out or not imported anymore).

[Yury G. Kudryashov]

I wonder what should we do with copyrights when we move code to mathlib, especially when we move code out of files (c) Microsoft to files (c) list of authors.

[Patrick Massot]

It would be more polite to ask Leo about this copyright thing.

[Yury G. Kudryashov]

Who volunteers to ask Leo?

[Johan Commelin]

I've removed the unshackled files, but I haven't yet cleaned up commented out code.

[Johan Commelin]

Going to bed now.

[Johan Commelin]

Others should feel absolutely free to also push to this PR branch

[Patrick Massot]

Yury G. Kudryashov said:

Who volunteers to ask Leo?

I volunteer Kevin. But I think it should be pretty easy to explain. We saw that Lean 4 removed a lot of maths from the core library hence we want to do the same, and we have a technical question about headers.

[Kevin Buzzard]

I can certainly do it

[Johan Commelin]

python3 script/gen_constants_cpp.py src/library/constants.txt
# ------------------------------------------------------
Warning: generated function 'get_le_refl_name' is not used in the source code
Warning: generated function 'get_mul_one_name' is not used in the source code
Warning: generated function 'get_mul_zero_name' is not used in the source code
Warning: generated function 'get_zero_le_one_name' is not used in the source code
Warning: generated function 'get_zero_lt_one_name' is not used in the source code
Warning: generated function 'get_zero_mul_name' is not used in the source code

[Johan Commelin]

lean ./tests/lean/run/check_constants.lean | grep error | sed 's/\/home.*error/error/'
# ------------------------------------------------------
error: identifier 'add_comm_group' is not a constant, namespace nor attribute
error: identifier 'add_comm_semigroup' is not a constant, namespace nor attribute
error: identifier 'add_group' is not a constant, namespace nor attribute
error: identifier 'add_monoid' is not a constant, namespace nor attribute
error: identifier 'distrib' is not a constant, namespace nor attribute
error: identifier 'field' is not a constant, namespace nor attribute
error: identifier 'int.bit0_nonneg' is not a constant, namespace nor attribute
error: identifier 'int.bit0_pos' is not a constant, namespace nor attribute
error: identifier 'int.bit1_nonneg' is not a constant, namespace nor attribute
error: identifier 'int.bit1_pos' is not a constant, namespace nor attribute
error: identifier 'int.nat_abs_bit0_step' is not a constant, namespace nor attribute
error: identifier 'int.nat_abs_bit1_nonneg_step' is not a constant, namespace nor attribute
error: identifier 'int.ne_neg_of_ne' is not a constant, namespace nor attribute
error: identifier 'int.ne_neg_of_pos' is not a constant, namespace nor attribute
error: identifier 'int.ne_of_nat_ne_nonneg_case' is not a constant, namespace nor attribute
error: identifier 'int.neg_ne_of_pos' is not a constant, namespace nor attribute
error: identifier 'int.neg_ne_zero_of_ne' is not a constant, namespace nor attribute
error: identifier 'int.one_nonneg' is not a constant, namespace nor attribute
error: identifier 'int.one_pos' is not a constant, namespace nor attribute
error: identifier 'int.zero_ne_neg_of_ne' is not a constant, namespace nor attribute
error: identifier 'int.zero_nonneg' is not a constant, namespace nor attribute
error: identifier 'left_distrib' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_ring' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_semiring' is not a constant, namespace nor attribute
error: identifier 'monoid' is not a constant, namespace nor attribute
error: identifier 'mul_one' is not a constant, namespace nor attribute
error: identifier 'mul_zero' is not a constant, namespace nor attribute
error: identifier 'mul_zero_class' is not a constant, namespace nor attribute
error: identifier 'right_distrib' is not a constant, namespace nor attribute
error: identifier 'ring' is not a constant, namespace nor attribute
error: identifier 'semiring' is not a constant, namespace nor attribute
error: identifier 'zero_le_one' is not a constant, namespace nor attribute
error: identifier 'zero_lt_one' is not a constant, namespace nor attribute
error: identifier 'zero_mul' is not a constant, namespace nor attribute

[Johan Commelin]

How much of these constants do we really want to keep in core?

[Johan Commelin]

All the int.* stuff should probably stay. But whatever comes after that, I would rather see the end of it.

[Johan Commelin]

We can have nat.left_distrib and int.left_distrib in core, and the general left_distrib in mathlib.

[Johan Commelin]

@Gabriel Ebner @Mario Carneiro Do we want to keep all those constants? I at least want ordered_monoid out of core. Which means that I need to reprove things like neg_of_neg_pos for int if we want to keep all the int.*. How important is that?

[Gabriel Ebner]

I don't see any way to remove the stuff about integers. This is required by the equation compiler to prove that -42 ≠ 358.

[Johan Commelin]

Ok

[Johan Commelin]

I'll reprove the ordered ring stuff for int

[Johan Commelin]

Ok, now the list looks like this

lean ./tests/lean/run/check_constants.lean | grep error | sed 's/\/home.*error/error/'
# -------------------------------------
error: identifier 'add_comm_group' is not a constant, namespace nor attribute
error: identifier 'add_comm_semigroup' is not a constant, namespace nor attribute
error: identifier 'add_group' is not a constant, namespace nor attribute
error: identifier 'add_monoid' is not a constant, namespace nor attribute
error: identifier 'distrib' is not a constant, namespace nor attribute
error: identifier 'field' is not a constant, namespace nor attribute
error: identifier 'left_distrib' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_ring' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_semiring' is not a constant, namespace nor attribute
error: identifier 'monoid' is not a constant, namespace nor attribute
error: identifier 'mul_one' is not a constant, namespace nor attribute
error: identifier 'mul_zero' is not a constant, namespace nor attribute
error: identifier 'mul_zero_class' is not a constant, namespace nor attribute
error: identifier 'right_distrib' is not a constant, namespace nor attribute
error: identifier 'ring' is not a constant, namespace nor attribute
error: identifier 'semiring' is not a constant, namespace nor attribute
error: identifier 'zero_le_one' is not a constant, namespace nor attribute
error: identifier 'zero_lt_one' is not a constant, namespace nor attribute
error: identifier 'zero_mul' is not a constant, namespace nor attribute

[Johan Commelin]

@Gabriel Ebner How do I tell lean that we want to move this out of core?

[Gabriel Ebner]

You've already removed it from constants.txt?

[Johan Commelin]

No, I've not

[Johan Commelin]

I'll rerun the python script

[Johan Commelin]

python3 script/gen_constants_cpp.py src/library/constants.txt
# -----------------------------------
Warning: generated function 'get_le_refl_name' is not used in the source code
Warning: generated function 'get_mul_one_name' is not used in the source code
Warning: generated function 'get_mul_zero_name' is not used in the source code
Warning: generated function 'get_zero_le_one_name' is not used in the source code
Warning: generated function 'get_zero_lt_one_name' is not used in the source code
Warning: generated function 'get_zero_mul_name' is not used in the source code

[Johan Commelin]

Is that bad?

[Johan Commelin]

I've pushed what I have so far

[Gabriel Ebner]

You need to remove more.

[Johan Commelin]

Ok, I should do this manually? Not using some script?

[Gabriel Ebner]

The contents of constants.txt are human-edited.

[Johan Commelin]

Ok, I pushed again

[Johan Commelin]

Errors during make:

/home/jmc/data/math/lean/src/library/app_builder.cpp: In member function ‘lean::expr lean::app_builder::mk_partial_left_distrib(const lean::expr&)’:
/home/jmc/data/math/lean/src/library/app_builder.cpp:742:77: error: ‘get_distrib_name’ was not declared in this scope; did you mean ‘get_string_name’?
  742 |         auto A_distrib = m_ctx.mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A));
      |                                                                             ^~~~~~~~~~~~~~~~
      |                                                                             get_string_name
/home/jmc/data/math/lean/src/library/app_builder.cpp:747:43: error: ‘get_left_distrib_name’ was not declared in this scope; did you mean ‘get_left_comm_name’?
  747 |         return ::lean::mk_app(mk_constant(get_left_distrib_name(), {lvl}), A, *A_distrib);
      |                                           ^~~~~~~~~~~~~~~~~~~~~
      |                                           get_left_comm_name
/home/jmc/data/math/lean/src/library/app_builder.cpp: In member function ‘lean::expr lean::app_builder::mk_partial_right_distrib(const lean::expr&)’:
/home/jmc/data/math/lean/src/library/app_builder.cpp:752:77: error: ‘get_distrib_name’ was not declared in this scope; did you mean ‘get_string_name’?
  752 |         auto A_distrib = m_ctx.mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A));
      |                                                                             ^~~~~~~~~~~~~~~~
      |                                                                             get_string_name
/home/jmc/data/math/lean/src/library/app_builder.cpp:757:43: error: ‘get_right_distrib_name’ was not declared in this scope; did you mean ‘get_iff_intro_name’?
  757 |         return ::lean::mk_app(mk_constant(get_right_distrib_name(), {lvl}), A, *A_distrib);
      |                                           ^~~~~~~~~~~~~~~~~~~~~~
      |                                           get_iff_intro_name

[Johan Commelin]

I'm confused about the internals of lean

[Gabriel Ebner]

Ok, so apparently you removed left_distrib, right_distrib, and distrib even though they're used.

[Gabriel Ebner]

Mmmh, you might want to clean up app_builder.h and app_builder.cpp.

[Gabriel Ebner]

I can also clean up if you're scared.

[Johan Commelin]

@Gabriel Ebner Yes, please go ahead.

[Johan Commelin]

I can help again with fixing the tests.

[Johan Commelin]

But this part, I don't really know what to do.

[Gabriel Ebner]

Done: https://github.com/leanprover-community/lean/pull/229/commits/245b721f98fd11f565dfe8f985cc86381f896e4d

[Johan Commelin]

Thanks!

[Johan Commelin]

:head_bandage: There are 66 failing tests :sad:

[Johan Commelin]

Where do I actually find this test

1 - style_check (Failed)

[Gabriel Ebner]

This is a python script. Apparently I included util.h twice in app_builder.cpp. Just delete the second occurrence.

[Johan Commelin]

What should I do with a test like this

variable R : Type
variable [ring R]

example : -(-(1:R)) = 1 :=
begin
  trace_state,
  exact neg_neg 1,
end

#check - -(1:R)

[Yury G. Kudryashov]

What is it supposed to check?

[Johan Commelin]

https://github.com/leanprover/lean/issues/1862

[Johan Commelin]

There's lots of tests like that.

[Johan Commelin]

They test for a specific bug report.

[Yury G. Kudryashov]

I'd declare a custom class with extends has_neg and an axiom neg_neg.

[Kevin Buzzard]

wooah, I try to prove it with trivial. What even is that?

[Johan Commelin]

Yury G. Kudryashov said:

I'd declare a custom class with extends has_neg and an axiom neg_neg.

I see. That seems like a reasonable approach.

[Johan Commelin]

In case anyone wants to contribute:

        588 - leanruntest_auto_quote1.lean (Failed)
        609 - leanruntest_bin_tree.lean (Failed)
        640 - leanruntest_cc_ac1.lean (Failed)
        641 - leanruntest_cc_ac2.lean (Failed)
        642 - leanruntest_cc_ac3.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        645 - leanruntest_cc_ac_bug.lean (Failed)
        687 - leanruntest_conv_tac1.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        742 - leanruntest_dsimp_options.lean (Failed)
        744 - leanruntest_dsimp_proj.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        794 - leanruntest_eq_cases_on.lean (Failed)
        815 - leanruntest_exhaustive_vm_impl_test.lean (Failed)
        830 - leanruntest_funext_tactic.lean (Failed)
        836 - leanruntest_handthen.lean (Failed)
        848 - leanruntest_hinst_lemma1.lean (Failed)
        849 - leanruntest_hinst_lemmas1.lean (Failed)
        892 - leanruntest_interactive1.lean (Failed)
        894 - leanruntest_intros_defeq_canonizer_bug.lean (Failed)
        929 - leanruntest_local_attribute.lean (Failed)
        935 - leanruntest_mario_type_context.lean (Failed)
        977 - leanruntest_mrw.lean (Failed)
        987 - leanruntest_name_resolution_with_params_bug.lean (Failed)
        994 - leanruntest_nat_sub_ematch.lean (Failed)
        1053 - leanruntest_psum_wf_rec.lean (Failed)
        1089 - leanruntest_rw1.lean (Failed)
        1095 - leanruntest_sebastien_coe_simp.lean (Failed)
        1110 - leanruntest_show_goal.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1128 - leanruntest_simp_lemmas_with_mvars.lean (Failed)
        1139 - leanruntest_simp_tc_err.lean (Failed)
        1142 - leanruntest_simp_zeta.lean (Failed)
        1152 - leanruntest_smt_assert_define.lean (Failed)
        1154 - leanruntest_smt_ematch1.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1162 - leanruntest_smt_tests.lean (Failed)
        1211 - leanruntest_term_app2.lean (Failed)
        1224 - leanruntest_u_eq_max_u_v.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)
        1287 - leanittest_goal_info.lean (Failed)

[Johan Commelin]

I just pushed a fix of 10 tests. (Not included on the list above.)

[Bryan Gin-ge Chen]

Looks like your local path snuck into the test output: https://github.com/leanprover-community/lean/pull/229/files#diff-9aa4d9cb8974761857542a0004292d74R1

[Johan Commelin]

Ooh, I though I had fixed that.

[Johan Commelin]

Should be fixed now

[Johan Commelin]

I've broken runtest 1442: https://github.com/leanprover/lean/issues/1442

protected def rel : ℤ × ℤ → ℤ × ℤ → Prop
| ⟨n₁, d₁⟩ ⟨n₂, d₂⟩ := n₁ * d₂ = n₂ * d₁

private def mul' : ℤ × ℤ → ℤ × ℤ → ℤ × ℤ
| ⟨n₁, d₁⟩ ⟨n₂, d₂⟩ := ⟨n₁ * n₂, d₁ * d₂⟩

example : ∀(a b c d : ℤ × ℤ), rel a c → rel b d → rel (mul' a b) (mul' c d) :=
λ⟨n₁, d₁⟩ ⟨n₂, d₂⟩ ⟨n₃, d₃⟩ ⟨n₄, d₄⟩,
  assume (h₁ : n₁ * d₃ = n₃ * d₁) (h₂ : n₂ * d₄ = n₄ * d₂),
  show (n₁ * n₂) * (d₃ * d₄) = (n₃ * n₄) * (d₁ * d₂),
    by cc

This is specifically about cc, afaict.
What should I do?

[Mario Carneiro]

do you have the proof that * is commutative and associative?

[Gabriel Ebner]

Have you read my comment? I'm pretty sure it's this:

(by cc : a + b = b + a) requires instances for is_associative (+) and is_commutative (+). Add them back (locally?). Same goes for ac_refl.

[Johan Commelin]

Ok, thanks

[Johan Commelin]

Hmm, how should I make this one happy?

universe variables u

-- jmc added this
class ring (α : Type u) extends has_mul α, has_add α :=
(add_comm : ∀ a b : α, a + b = b + a)
(add_assoc : ∀ a b c : α, a + b + c = a + (b + c))

variables {α : Type u}
variables [ring α]
open tactic

-- jmc added this
instance aa : is_associative α (+) := ⟨ring.add_assoc⟩
instance ac : is_commutative α (+) := ⟨ring.add_comm⟩
constant ma : is_associative α (*)
constant lc : is_left_cancel α (+)
constant rc : is_right_cancel α (+)
constant ld : is_left_distrib α (*) (+)
constant rd : is_right_distrib α (*) (+)

example (x1 x2 x3 x4 x5 x6 : α) : x1*x4 = x1 → x3*x6 = x5*x5 → x5 = x4 → x6 = x2 → x1 = x1*(x6*x3) :=
by cc

example (y1 y2 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y2 + y1) → x3*x6 = x5*x5 → x5 = x4 → x6 = x2 → (y2 + y1) = (y1 + y2)*(x6*x3) :=
by cc

example (y1 y2 y3 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y3 + y1) → x3*x6 = x5*x5 → x5 = x4 → x6 = x2 → y2 = y3 → (y2 + y1) = (y1 + y3)*(x6*x3) :=
by cc

[Johan Commelin]

There's a whole bunch of tests using smt and eblast etc. And I have no idea what those are.

[Johan Commelin]

I've pushed what I've done so far. That's it for tonight. I think most of the remaining tests require some help.

[Johan Commelin]

We're now down to 20 failing tests:

        559 - leanruntest_aexp.lean (Failed)
        642 - leanruntest_cc_ac3.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        815 - leanruntest_exhaustive_vm_impl_test.lean (Failed)
~~        987 - leanruntest_name_resolution_with_params_bug.lean (Failed)~~
        994 - leanruntest_nat_sub_ematch.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
~~        1128 - leanruntest_simp_lemmas_with_mvars.lean (Failed)~~
        1152 - leanruntest_smt_assert_define.lean (Failed)
        1154 - leanruntest_smt_ematch1.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1162 - leanruntest_smt_tests.lean (Failed)
~~        1211 - leanruntest_term_app2.lean (Failed)~~
~~        1224 - leanruntest_u_eq_max_u_v.lean (Failed)~~
        1247 - leanruntest_using_smt2.lean (Failed)

[Johan Commelin]

Down to 16

[Johan Commelin]

Down to 10

        559 - leanruntest_aexp.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
~~        815 - leanruntest_exhaustive_vm_impl_test.lean (Failed)~~
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

[Johan Commelin]

I'm removing gcd from core. Is that ok? Or is this something that should strictly stay there for VM reasons?

[Mario Carneiro]

I don't think so. It does seem a bit out of place, come to think of it

[Johan Commelin]

@Mario Carneiro Ok, then I feel good about removing it from the exhaustive_vm_impl_test.

[Johan Commelin]

@Mario Carneiro @Gabriel Ebner Do we want all these smt and eblast tests on ring and field if we are moving those structures out of core? I have no idea what smt and eblast do. I've been able to fix a bunch of tests by changing add_comm to nat.add_comm. But now I'm stuck.

[Mario Carneiro]

You should be able to locally define ring and field in the test(s)

[Johan Commelin]

That's not enough, right?

[Johan Commelin]

You also need a ton of supporting lemmas

[Mario Carneiro]

they work based on attributes like simp does

[Mario Carneiro]

the lemmas don't have to be proven

[Johan Commelin]

That's what I mean

[Johan Commelin]

Aha

[Johan Commelin]

But still. It would mean that these tests become quite a bit longer

[Mario Carneiro]

I guess it depends on the test

[Johan Commelin]

For 56 tests I could do it (-;

[Mario Carneiro]

I mean, is it something that is actually integration testing all these attributes in a library, or is it some particular feature of smt

[Johan Commelin]

I can also dump init/algebra in tests/lean/run/algebra and import stuff.

[Johan Commelin]

Mario Carneiro said:

I mean, is it something that is actually integration testing all these attributes in a library, or is it some particular feature of smt

How would I know?

[Johan Commelin]

These tests are mostly a mystery to me.

[Mario Carneiro]

which one are you looking at now?

[Johan Commelin]

It's code, and if it compiles I'm happy. They mostly don't contain comments explaining what they test.

[Johan Commelin]

Any of

        559 - leanruntest_aexp.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

[Johan Commelin]

I've fixed all the others

[Mario Carneiro]

aexp.lean doesn't have any algebra in it

[Johan Commelin]

Right... so why is it failing?

[Mario Carneiro]

what errors are you getting? #mwe

[Johan Commelin]

tactic failed, there are unsolved goals
state:
8 goals
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ℕ,
a_3 : asimp_const a_a = val a_2
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : uname,
a_3 : asimp_const a_a = var a_2
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = plus a_2 a_3
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = times a_2 a_3
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ℕ,
a_3 : asimp_const a_a = val a_2
⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : uname,
a_3 : asimp_const a_a = var a_2
⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = plus a_2 a_3
⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = times a_2 a_3
⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

[Johan Commelin]

@Mario Carneiro You say that it doesn't have any algebra in it. But it is building expressions with * and +.

[Johan Commelin]

I think it is applying those to nats. And core no longer knows that nat is a comm_semiring. But all the relevant lemmas are there.

[Johan Commelin]

Adding the ematch attribute to nat.zero_mul, nat.zero_add, nat.add_zero, nat.mul_zero didn't help.

[Mario Carneiro]

It's weird; I think the theorem being proven is actually true without any axioms about nat

[Mario Carneiro]

the only thing that should be necessary is that value has + * 0 1

[Mario Carneiro]

I thought it was simplifying 0 + x = x and so on but that's not actually needed

[Mario Carneiro]

but the proof method is really bizarre

[Mario Carneiro]

don't try this at home, kids

[Mario Carneiro]

I just managed to prove the theorem manually using no theorems at all about value

[Mario Carneiro]

What is the state after eblast?

[Johan Commelin]

1 goal
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ℕ,
a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a_2, asimp_const a_a},
 {val a, asimp_const a_a_1},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {a_2 + a, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

[Mario Carneiro]

As a quick primer on how to read the state, each of the lists in "equalities" are collections of terms that smt knows how to prove are equal, and the collection as a whole is closed under taking subterms. What was supposed to happen was that since aval a_a s and a_2 are in the same group, and aval a_a_1 s and a are as well, it will deduce that a_2 + a and aval a_a s + aval a_a_1 s are also in the same group, closing the goal. However, they are in different groups. Maybe the typeclass instance on them is different? I suspect that one is addition on nat and the other is addition on value, and the @[reducible] annotation on value is confusing things

[Mario Carneiro]

You could try replacing value with nat everywhere and see if that fixes things

[Mario Carneiro]

although if so this might just be an actual bug

[Johan Commelin]

Mario Carneiro said:

You could try replacing value with nat everywhere and see if that fixes things

Yup, now the error is gone

[Mario Carneiro]

What do the two terms I mentioned look like with pp.all?

[Johan Commelin]

@Mario Carneiro you mean this ¿?

a_ih_a_1 : @eq.{1} nat (imp.aval (imp.asimp_const a_a_1) s) (imp.aval a_a_1 s)
facts:
{@eq.{1} nat (imp.aval (imp.asimp_const a_a_1) s) (imp.aval a_a_1 s),
 @eq.{1} nat (imp.aval (imp.asimp_const a_a) s) (imp.aval a_a s)}
equalities: {{imp.aval a_a s, imp.aval (imp.asimp_const a_a) s}, {imp.aval a_a_1 s, imp.aval (imp.asimp_const a_a_1) s}}

[Mario Carneiro]

after eblast

[Johan Commelin]

How do I print them?

[Johan Commelin]

goals accomplished

[Mario Carneiro]

oh, I mean in the broken version

[Mario Carneiro]

I mean, sure we could change the statement and fix the test, but that kind of defeats the purpose of having a test

[Johan Commelin]

a_3 : @eq.{1} imp.aexp (imp.asimp_const a_a) (imp.aexp.val a_2)
facts:
{@eq.{1} imp.aexp (imp.asimp_const a_a) (imp.aexp.val a_2),
 @eq.{1} imp.aexp (imp.asimp_const a_a_1) (imp.aexp.val a),
 @eq.{1} imp.value (imp.aval (imp.asimp_const a_a_1) s) (imp.aval a_a_1 s),
 @eq.{1} imp.value (imp.aval (imp.asimp_const a_a) s) (imp.aval a_a s)}
equalities:
{{imp.aexp.val a, imp.asimp_const a_a_1},
 {imp.aexp.val a_2, imp.asimp_const a_a},
 {imp.aval a_a s, imp.aval (imp.aexp.val a_2) s, a_2, imp.aval (imp.asimp_const a_a) s},
 {imp.aval (imp.asimp_const a_a), imp.aval (imp.aexp.val a_2)},
 {imp.asimp_const._match_1 (imp.asimp_const a_a), imp.asimp_const._match_1 (imp.aexp.val a_2)},
 {imp.aval a_a_1 s, imp.aval (imp.aexp.val a) s, a, imp.aval (imp.asimp_const a_a_1) s},
 {imp.aval (imp.asimp_const a_a_1), imp.aval (imp.aexp.val a)},
 {imp.aval (imp.asimp_const (imp.aexp.plus a_a a_a_1)),
  imp.aval (imp.aexp.val (@has_add.add.{0} nat nat.has_add a_2 a))},
 {@has_add.add.{0} nat nat.has_add a_2 a,
  imp.aval (imp.asimp_const (imp.aexp.plus a_a a_a_1)) s,
  imp.aval (imp.aexp.val (@has_add.add.{0} nat nat.has_add a_2 a)) s},
 {imp.aexp.val (@has_add.add.{0} nat nat.has_add a_2 a),
  imp.asimp_const (imp.aexp.plus a_a a_a_1),
  imp.asimp_const._match_1 (imp.asimp_const a_a) (imp.asimp_const a_a_1),
  imp.asimp_const._match_1 (imp.aexp.val a_2) (imp.aexp.val a)},
 {@has_add.add.{0} imp.value nat.has_add (imp.aval a_a s) (imp.aval a_a_1 s), imp.aval (imp.aexp.plus a_a a_a_1) s}}

[Mario Carneiro]

@has_add.add.{0} nat nat.has_add a_2 a
@has_add.add.{0} imp.value nat.has_add (imp.aval a_a s) (imp.aval a_a_1 s)

[Johan Commelin]

Mario Carneiro said:

I mean, sure we could change the statement and fix the test, but that kind of defeats the purpose of having a test

Depends on what we're testing, I guess.

[Mario Carneiro]

the adds are indeed different

[Johan Commelin]

So, what do we do now?

[Mario Carneiro]

hm, here's a version of the proof that captures the successful state just before close runs:

lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
 induction a,
 destruct (asimp_const a_a_1),
{ destruct (asimp_const a_a),
  { ematch, ematch,
    smt_tactic.ematch >> smt_tactic.trace_state },
  all_goals {admit}},
all_goals {admit}
end

equalities:
...
 {@has_add.add.{0} imp.value nat.has_add (imp.aval a_a s) (imp.aval a_a_1 s),
  @has_add.add.{0} nat nat.has_add a_2 a,
  imp.aval (imp.aexp.plus a_a a_a_1) s}}

[Johan Commelin]

I have no idea what that means :oops:

[Johan Commelin]

I feel a bit like I'm a proxy between the master and the machine...

[Mario Carneiro]

I've used smt a grand total of 0 times ever, but I know the theory

[Mario Carneiro]

there is a commented out trace option for smt, what does that show?

[Johan Commelin]

pp.all or not?

[Johan Commelin]

With pp.all you'll get a crapton of shit

[Mario Carneiro]

Use my version of the proof

[Mario Carneiro]

just posted above

[Mario Carneiro]

it stops at the first interesting point

[Johan Commelin]

aexp.lean:65:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a_2) s = a_2
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a) s = a
[smt.ematch] instance [imp.asimp_const.equations._eqn_3], generation: 1
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance [imp.aval.equations._eqn_3], generation: 1
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a_2) s = a_2
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a) s = a
[smt.ematch] instance, generation: 1, after preprocessing
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance, generation: 1, after preprocessing
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s

aexp.lean:65:12: information trace output
[smt.ematch] instance [imp.asimp_const._match_1.equations._eqn_1], generation: 2
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)
[smt.ematch] instance, generation: 2, after preprocessing
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)

[Johan Commelin]

And

aexp.lean:66:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 3
aval (val (a_2 + a)) s = a_2 + a
[smt.ematch] instance, generation: 3, after preprocessing
aval (val (a_2 + a)) s = a_2 + a
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ℕ,
a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a, asimp_const a_a_1},
 {val a_2, asimp_const a_a},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {a_2 + a, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

[Mario Carneiro]

For comparison, here is my version:

aexp.lean:64:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a) s = a
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a_2) s = a_2
[smt.ematch] instance [imp.asimp_const.equations._eqn_3], generation: 1
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance [imp.aval.equations._eqn_3], generation: 1
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a) s = a
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a_2) s = a_2
[smt.ematch] instance, generation: 1, after preprocessing
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance, generation: 1, after preprocessing
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s
aexp.lean:64:12: information trace output
[smt.ematch] instance [imp.asimp_const._match_1.equations._eqn_1], generation: 2
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)
[smt.ematch] instance, generation: 2, after preprocessing
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)
aexp.lean:65:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 3
aval (val (a_2 + a)) s = a_2 + a
[smt.ematch] instance, generation: 3, after preprocessing
aval (val (a_2 + a)) s = a_2 + a
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ℕ,
a_3 : asimp_const a_a = val a_2
facts:
{aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s,
 asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a_2, asimp_const a_a},
 {val a, asimp_const a_a_1},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {aval (asimp_const a_a_1), aval (val a)},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s,
  aval (asimp_const (plus a_a a_a_1)) s,
  aval (val (a_2 + a)) s,
  a_2 + a,
  aval (plus a_a a_a_1) s}}
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

[Johan Commelin]

Am I supposed to solve some problem now? I still have no clue what I'm looking for.

[Johan Commelin]

I think that I would like to learn about SMT, but maybe not while trying to get algebra out of core (-;

[Mario Carneiro]

I'm just diffing

[Mario Carneiro]

I'm ~60% sure you've uncovered a bug in smt, but given that I don't know what we should do about it

[Mario Carneiro]

no one uses it or knows how it works

[Johan Commelin]

And smt is 96% C++, I guess

[Mario Carneiro]

Aha, I think this might be relevant:

lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
  smt_tactic.get_lemmas >>= smt_tactic.trace,
end

{[imp.asimp_const.equations._eqn_1, patterns: {{asimp_const (val ?x_0)}}],
...
 [imp.asimp_const._match_1.equations._eqn_4, patterns: {{asimp_const._match_1 (val ?x_0) (times ?x_1 ?x_2)}}],
 [one_mul, patterns: {{1 * ?x_2}}],
 [zero_add, patterns: {{0 + ?x_2}}],
 [add_zero, patterns: {{?x_2 + 0}}],
 [imp.aval.equations._eqn_4, patterns: {{aval (times ?x_0 ?x_1) ?x_2}}],
 [mul_one, patterns: {{?x_2 * 1}}],
 [imp.aval.equations._eqn_3, patterns: {{aval (plus ?x_0 ?x_1) ?x_2}}],
 [zero_mul, patterns: {{0 * ?x_2}}],
 [mul_zero, patterns: {{?x_2 * 0}}],
 [nat.add_sub_add_left, patterns: {{?x_0 + ?x_1 - (?x_0 + ?x_2)}}],
 [nat.add_sub_add_right, patterns: {{?x_0 + ?x_1 - (?x_2 + ?x_1)}}],
 [min_eq_right, patterns: {{min ?x_2 ?x_3}}],
 [min_eq_left, patterns: {{min ?x_2 ?x_3}}]}

[Mario Carneiro]

I assume if you run the same thing most of those theorems won't be listed

[Mario Carneiro]

Try adding

attribute [ematch] zero_add add_zero mul_one zero_mul mul_zero
  nat.add_sub_add_left nat.add_sub_add_right min_eq_right min_eq_left

and see if it fixes the issue

[Mario Carneiro]

and then remove lemmas until it breaks again

[Johan Commelin]

@Mario Carneiro I'm back. (Had to put my daughter in bed.) With those attributes, the goal is still

1 goal
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ℕ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ℕ,
a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a_2, asimp_const a_a},
 {val a, asimp_const a_a_1},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {a_2 + a, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

just before end.

[Mario Carneiro]

Oh, I missed a couple: nat.add_sub_cancel nat.add_sub_cancel_left

[Johan Commelin]

Too bad, peanut spread...
It's still unhappy.

[Mario Carneiro]

What do you get for this:

attribute [ematch] zero_add add_zero mul_one zero_mul mul_zero
  nat.add_sub_add_left nat.add_sub_add_right min_eq_right min_eq_left
  nat.add_sub_cancel nat.add_sub_cancel_left
lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
  smt_tactic.get_lemmas >>= smt_tactic.trace,
end

{[imp.asimp_const.equations._eqn_1, patterns: {{asimp_const (val ?x_0)}}],
 [imp.asimp_const.equations._eqn_2, patterns: {{asimp_const (var ?x_0)}}],
 [imp.aval.equations._eqn_1, patterns: {{aval (val ?x_0) ?x_1}}],
 [imp.aval.equations._eqn_2, patterns: {{aval (var ?x_0) ?x_1}}],
 [imp.asimp_const._match_1.equations._eqn_5, patterns: {{asimp_const._match_1 (var ?x_0) ?x_1}}],
 [imp.asimp_const._match_2.equations._eqn_5, patterns: {{asimp_const._match_2 (var ?x_0) ?x_1}}],
 [imp.asimp_const.equations._eqn_3, patterns: {{asimp_const (plus ?x_0 ?x_1)}}],
 [imp.asimp_const.equations._eqn_4, patterns: {{asimp_const (times ?x_0 ?x_1)}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1 - ?x_1}}],
 [imp.asimp_const._match_2.equations._eqn_2, patterns: {{asimp_const._match_2 (val ?x_0) (var ?x_1)}}],
 [imp.asimp_const._match_1.equations._eqn_2, patterns: {{asimp_const._match_1 (val ?x_0) (var ?x_1)}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1 - ?x_0}}],
 [imp.asimp_const._match_2.equations._eqn_6, patterns: {{asimp_const._match_2 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_2.equations._eqn_7, patterns: {{asimp_const._match_2 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_7, patterns: {{asimp_const._match_1 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_6, patterns: {{asimp_const._match_1 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_1, patterns: {{asimp_const._match_1 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_1, patterns: {{asimp_const._match_2 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_4, patterns: {{asimp_const._match_2 (val ?x_0) (times ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_3, patterns: {{asimp_const._match_1 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_2.equations._eqn_3, patterns: {{asimp_const._match_2 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_4, patterns: {{asimp_const._match_1 (val ?x_0) (times ?x_1 ?x_2)}}],
 [one_mul, patterns: {{1 * ?x_2}}],
 [zero_add, patterns: {{0 + ?x_2}}],
 [add_zero, patterns: {{?x_2 + 0}}],
 [imp.aval.equations._eqn_4, patterns: {{aval (times ?x_0 ?x_1) ?x_2}}],
 [mul_one, patterns: {{?x_2 * 1}}],
 [imp.aval.equations._eqn_3, patterns: {{aval (plus ?x_0 ?x_1) ?x_2}}],
 [zero_mul, patterns: {{0 * ?x_2}}],
 [mul_zero, patterns: {{?x_2 * 0}}],
 [nat.add_sub_add_left, patterns: {{?x_0 + ?x_1 - (?x_0 + ?x_2)}}],
 [nat.add_sub_add_right, patterns: {{?x_0 + ?x_1 - (?x_2 + ?x_1)}}],
 [min_eq_right, patterns: {{min ?x_2 ?x_3}}],
 [min_eq_left, patterns: {{min ?x_2 ?x_3}}]}

[Johan Commelin]

aexp.lean:69:2: information trace output
{[imp.asimp_const.equations._eqn_1, patterns: {{asimp_const (val ?x_0)}}],
 [imp.asimp_const.equations._eqn_2, patterns: {{asimp_const (var ?x_0)}}],
 [imp.aval.equations._eqn_1, patterns: {{aval (val ?x_0) ?x_1}}],
 [imp.aval.equations._eqn_2, patterns: {{aval (var ?x_0) ?x_1}}],
 [nat.mul_one, patterns: {{?x_0 * 1}}],
 [nat.zero_add, patterns: {{0 + ?x_0}}],
 [imp.asimp_const._match_1.equations._eqn_5, patterns: {{asimp_const._match_1 (var ?x_0) ?x_1}}],
 [nat.add_zero, patterns: {{?x_0 + 0}}],
 [nat.one_mul, patterns: {{1 * ?x_0}}],
 [imp.asimp_const._match_2.equations._eqn_5, patterns: {{asimp_const._match_2 (var ?x_0) ?x_1}}],
 [imp.asimp_const.equations._eqn_3, patterns: {{asimp_const (plus ?x_0 ?x_1)}}],
 [imp.asimp_const.equations._eqn_4, patterns: {{asimp_const (times ?x_0 ?x_1)}}],
 [nat.mul_zero, patterns: {{?x_0 * 0}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1 - ?x_1}}],
 [imp.asimp_const._match_2.equations._eqn_2, patterns: {{asimp_const._match_2 (val ?x_0) (var ?x_1)}}],
 [nat.zero_mul, patterns: {{0 * ?x_0}}],
 [imp.asimp_const._match_1.equations._eqn_2, patterns: {{asimp_const._match_1 (val ?x_0) (var ?x_1)}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1 - ?x_0}}],
 [imp.asimp_const._match_2.equations._eqn_6, patterns: {{asimp_const._match_2 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_2.equations._eqn_7, patterns: {{asimp_const._match_2 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_7, patterns: {{asimp_const._match_1 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_6, patterns: {{asimp_const._match_1 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_1, patterns: {{asimp_const._match_1 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_1, patterns: {{asimp_const._match_2 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_4, patterns: {{asimp_const._match_2 (val ?x_0) (times ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_3, patterns: {{asimp_const._match_1 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_2.equations._eqn_3, patterns: {{asimp_const._match_2 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_4, patterns: {{asimp_const._match_1 (val ?x_0) (times ?x_1 ?x_2)}}],
 [imp.aval.equations._eqn_4, patterns: {{aval (times ?x_0 ?x_1) ?x_2}}],
 [imp.aval.equations._eqn_3, patterns: {{aval (plus ?x_0 ?x_1) ?x_2}}],
 [nat.add_sub_add_left, patterns: {{?x_0 + ?x_1 - (?x_0 + ?x_2)}}],
 [nat.add_sub_add_right, patterns: {{?x_0 + ?x_1 - (?x_2 + ?x_1)}}],
 [min_eq_right, patterns: {{min ?x_2 ?x_3}}],
 [min_eq_left, patterns: {{min ?x_2 ?x_3}}]}

[Mario Carneiro]

oh, you are using nat.mul_one instead of mul_one et al

[Johan Commelin]

mul_one doesn't exist

[Mario Carneiro]

try replicating mul_one in this file, i.e. define a dummy ring and the lemmas

[Mario Carneiro]

Here's my theory: ematch isn't actually smart enough to realize that @has_add.add nat nat.has_add and @has_add.add value nat.has_add are the same thing, but when it tries to apply one of these typeclass theorems it is forced to unfold value in order to make the second thing typecheck, and then it all works

[Johan Commelin]

Like this:

class semiring (α : Type) extends has_zero α, has_one α, has_add α, has_mul α.

instance foo : semiring ℕ :=
{ zero := 0,
  one := 1,
  add := (+),
  mul := (*) }

section
variables {α : Type} [semiring α] (a : α)

lemma zero_add : (0:α) + a = a := sorry
lemma add_zero : a + 0 = a := sorry
lemma zero_mul : (0:α) * a = 0 := sorry
lemma mul_zero : a * 0 = 0 := sorry
lemma one_mul : (1:α) * a = a := sorry
lemma mul_one : a * 1 = a := sorry

end

[Mario Carneiro]

Mark them all @[ematch], otherwise yes

[Johan Commelin]

attribute [ematch] zero_add add_zero mul_one zero_mul mul_zero
  nat.add_sub_add_left nat.add_sub_add_right min_eq_right min_eq_left
  nat.add_sub_cancel nat.add_sub_cancel_left

lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
  smt_tactic.get_lemmas >>= smt_tactic.trace,
end

aexp.lean:91:0: error
tactic failed, there are unsolved goals
state:
a : aexp,
s : state
⊢ aval (asimp_const a) s = aval a s

[Mario Carneiro]

you get no output?

[Mario Carneiro]

You should go back to the original test, that was just diagnostics

[Johan Commelin]

a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a, asimp_const a_a_1},
 {val a_2, asimp_const a_a},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {aval a_a s, aval a_a s + aval a_a_1 s - aval a_a_1 s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval a_a_1 s, aval a_a s + aval a_a_1 s - aval a_a s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {has_add.add (aval a_a s), has_add.add a_2},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s, a_2 + a},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

⊢ aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

[Mario Carneiro]

nooo

[Mario Carneiro]

WTH aval a_a s + aval a_a_1 s literally appears in two equality classes

[Mario Carneiro]

it must be the two versions of it

[Mario Carneiro]

Okay, my curiosity is satisfied. Let's just replace value with nat for the PR and maybe file an issue about this for later

[Johan Commelin]

Are you ready for the next test?

[Mario Carneiro]

heh, I hope it's the same story 8 times

[Mario Carneiro]

cc_ac5.lean - is this one not fixed with ac instances for + and * ?

[Johan Commelin]

niverse variables u

class ring (α : Type u) extends has_mul α, has_add α :=
(add_comm : ∀ a b : α, a + b = b + a)
(add_assoc : ∀ a b c : α, a + b + c = a + (b + c))

variables {α : Type u}
variables [ring α]
open tactic

instance aa : is_associative α (+) := ⟨ring.add_assoc⟩
instance ac : is_commutative α (+) := ⟨ring.add_comm⟩
constant ma : is_associative α (*)
constant lc : is_left_cancel α (+)
constant rc : is_right_cancel α (+)
constant ld : is_left_distrib α (*) (+)
constant rd : is_right_distrib α (*) (+)

example (x1 x2 x3 x4 x5 x6 : α) : x1*x4 = x1 → x3*x6 = x5*x5 → x5 = x4 → x6 = x2 → x1 = x1*(x6*x3) :=
by cc

example (y1 y2 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y2 + y1) → x3*x6 = x5*x5 → x5 = x4 → x6 = x2 → (y2 + y1) = (y1 + y2)*(x6*x3) :=
by cc

example (y1 y2 y3 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y3 + y1) → x3*x6 = x5*x5 → x5 = x4 → x6 = x2 → y2 = y3 → (y2 + y1) = (y1 + y3)*(x6*x3) :=
by cc

is what I have so far

[Johan Commelin]

cc fails on all three tests.

[Mario Carneiro]

it's a commutative ring

[Johan Commelin]

Nope it's not. The [ring \a] was from the original test.

[Johan Commelin]

Also, adding commutativity of * doesn't make cc happy.

[Mario Carneiro]

not in my copy

[Johan Commelin]

Oh, weird.

[Mario Carneiro]

If you use

instance ma : is_associative α (*) := ⟨sorry⟩
instance mc : is_commutative α (*) := ⟨sorry⟩

instead of constant ma : is_associative ... it works

[Mario Carneiro]

I think lean likes to be able to unfold instances to constructors

[Johan Commelin]

Aha

[Mario Carneiro]

even if there isn't anything past that

[Mario Carneiro]

you could use an axiom in place of the sorry

[Johan Commelin]

Ok, thanks. That worked. 2 down, 8 to go.

[Johan Commelin]

leanruntest_cpdt.lean

[Mario Carneiro]

oh boy, rsimp

[Mario Carneiro]

this one uses smt, so it might be the same bug

[Mario Carneiro]

it's also practically the same problem

[Mario Carneiro]

what error do you get?

[Johan Commelin]

/- "Proving in the Large" chapter of CPDT -/

inductive exp : Type
| Const (n : nat) : exp
| Plus (e1 e2 : exp) : exp
| Mult (e1 e2 : exp) : exp

open exp

def eeval : exp → nat
| (Const n)    := n
| (Plus e1 e2) := eeval e1 + eeval e2
| (Mult e1 e2) := eeval e1 * eeval e2

def times (k : nat) : exp → exp
| (Const n)    := Const (k * n)
| (Plus e1 e2) := Plus (times e1) (times e2)
| (Mult e1 e2) := Mult (times e1) e2

def reassoc : exp → exp
| (Const n)    := (Const n)
| (Plus e1 e2) :=
  let e1' := reassoc e1 in
  let e2' := reassoc e2 in
  match e2' with
  | (Plus e21 e22) := Plus (Plus e1' e21) e22
  | _              := Plus e1' e2'
  end
| (Mult e1 e2) :=
  let e1' := reassoc e1 in
  let e2' := reassoc e2 in
  match e2' with
  | (Mult e21 e22) := Mult (Mult e1' e21) e22
  | _              := Mult e1' e2'
  end

@[simp]
lemma nat.mul_left_comm : ∀ (n m k : ℕ), n * (m * k) = m * (n * k) := sorry

attribute [simp] nat.left_distrib nat.right_distrib times reassoc eeval nat.mul_comm nat.mul_assoc

theorem eeval_times (k e) : eeval (times k e) = k * eeval e :=
by induction e; simp [*]

theorem reassoc_correct (e) : eeval (reassoc e) = eeval e :=
by induction e; simp [*]; cases (reassoc e_e2); rsimp

The first one is happy.

[Johan Commelin]

tactic failed, there are unsolved goals
state:
e_e1 e_e2 : exp,
e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1,
e1 e2 : exp,
e_ih_e2 : eeval (Plus e1 e2) = eeval e_e2
⊢ eeval (Plus (Plus (reassoc e_e1) e1) e2) = eeval e_e1 + eeval e_e2

[Mario Carneiro]

you left off mul_left_comm

[Johan Commelin]

It's tagged simp just above

[Mario Carneiro]

oh wait nvm

[Johan Commelin]

ematch_attr_to_defs
------------------------
universe variables u
variable {α : Type u}

def app : list α → list α → list α
| []     l := l
| (h::t) l := h :: app t l

/- Mark the app equational lemmas as ematching rules -/
attribute [ematch] app

@[ematch] lemma app_nil_right (l : list α) : app l [] = l :=
begin [smt]
  induction l,
  ematch,
end

@[ematch] lemma app_assoc (l₁ l₂ l₃ : list α) : app (app l₁ l₂) l₃ = app l₁ (app l₂ l₃) :=
begin [smt]
  induction l₁,
  ematch,
  ematch
end

def len : list α → nat
| []       := 0
| (a :: l) := len l + 1

attribute [ematch] len nat.add_zero nat.zero_add

@[simp] lemma len_app (l₁ l₂ : list α) : len (app l₁ l₂) = len l₁ + len l₂ :=
begin [smt]
  induction l₁,
  {ematch, ematch},
  {ematch, ematch}
end

This one is also confusing me.

[Mario Carneiro]

I think we should just file the ematch based tests away

[Mario Carneiro]

I remember there was some bug in ematch that we found 2 years ago and couldn't do anything about, something to do with multiple typeclasses causing problems for category theory, and we basically banned ematch based proofs from mathlib then

[Johan Commelin]

I managed to fix another test in the mean time

[Johan Commelin]

The list is now

        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

[Johan Commelin]

How about this

universe variables u

class comm_semiring (α : Type*) extends has_zero α, has_add α, has_one α, has_mul α.

lemma zero_add {α : Type*} [comm_semiring α] (a : α) : (0:α) + a = a := sorry
lemma add_zero {α : Type*} [comm_semiring α] (a : α) : a + 0 = a := sorry

def ex {α : Type u} [comm_semiring α] (a : α) : 0 + a = a :=
zero_add a

-- local attribute [-simp] zero_add add_zero
attribute [simp] ex

example (a b : nat) : 0 + 0 + a = a :=
by simp -- !!! FAILS :shock:

-- local attribute [-ematch] zero_add add_zero
attribute [ematch] ex

example (a b : nat) : 0 + 0 + a = a :=
by using_smt $ smt_tactic.eblast -- fails :not_surprised:

[Johan Commelin]

Ooh, nvm... nat is not a comm_semiring

[Johan Commelin]

That one's fixed.

[Johan Commelin]

        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

[Mario Carneiro]

is cpdt fixed with a fake ring instance?

[Mario Carneiro]

from the names it looks like everything that remains is ematch related, so let's just comment out these tests

[Mario Carneiro]

Is ematch2.lean not fixed with a fake instance?

[Johan Commelin]

The last blast in ematch2:

tactic failed, there are unsolved goals
state:
α : Type u,
p m n q : ℕ,
xs : tuple α m,
ys : tuple α n,
zs : tuple α p,
ws : tuple α q,
a : p = n + m,
a_1 : zs == xs ++ ys
⊢ zs ++ ws == xs ++ (ys ++ ws)

[Mario Carneiro]

I think it needs add_assoc on nat

[Mario Carneiro]

try attribute [ematch] nat.add_assoc

[Mario Carneiro]

oh crap, I just realized the implications of the @[no_rsimp] attribute

[Johan Commelin]

From the end of cpdt:

class semiring (α : Type) extends has_mul α, has_add α, has_one α, has_zero α.

instance foo : semiring nat :=
{ zero := 0, one := 1, add := (+), mul := (*) }

variables {α : Type} [semiring α] (a b c : α)

lemma left_distrib : a * (b + c) = a * b + a * c := sorry
lemma right_distrib : (a + b) * c = a * c + b * c := sorry
lemma mul_comm : a * b = b * a := sorry
lemma mul_assoc : a * b * c = a * (b * c) := sorry
lemma mul_left_comm : a * (b * c) = b * (a * c) := sorry

attribute [simp] left_distrib right_distrib times reassoc eeval mul_comm mul_assoc mul_left_comm

theorem eeval_times (k e) : eeval (times k e) = k * eeval e :=
by induction e; simp [*]

theorem reassoc_correct (e) : eeval (reassoc e) = eeval e :=
by induction e; simp [*]; cases (reassoc e_e2); rsimp -- still fails

[Johan Commelin]

Mario Carneiro said:

try attribute [ematch] nat.add_assoc

This didn't help.

[Mario Carneiro]

What do you get in cpdt with set_option trace.smt true?

[Mario Carneiro]

I think the second block is the first one that fails

[Johan Commelin]

test ematch2 is now fixed. smt_ematch2 is still a problem.
Let me look at cpdt again.

[Johan Commelin]

 Freeze display
Tactic State
1 goal
e : exp
⊢ eeval (reassoc e) = eeval e
cpdt.lean:58:3: error
tactic failed, there are unsolved goals
state:
e_e1 e_e2 : exp,
e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1,
e1 e2 : exp,
e_ih_e2 : eeval (Plus e1 e2) = eeval e_e2
⊢ eeval (Plus (Plus (reassoc e_e1) e1) e2) = eeval e_e1 + eeval e_e2
cpdt.lean:58:48: information trace output
[smt.intro] e_e1 : exp
[smt.intro] e_e2 : exp
[smt.fact] new facts: {eeval (reassoc e_e1) = eeval e_e1}
[smt.intro] e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1
[smt.intro] n : ℕ
[smt.fact] new facts: {eeval (Const n) = eeval e_e2}
[smt.intro] e_ih_e2 : eeval (Const n) = eeval e_e2
[smt.ematch] new ground fact: bnot ff = tt
[smt.ematch] new ground fact: bnot tt = ff
[smt.ematch] new ground fact: bxor ff tt = tt
[smt.ematch] new ground fact: bxor tt ff = tt
[smt.ematch] new ground fact: ff || tt = tt
[smt.ematch] new ground fact: bxor ff ff = ff
[smt.ematch] new ground fact: 0 = 0
[smt.ematch] new ground fact: tt && ff = ff
[smt.ematch] new ground fact: ff || ff = ff
[smt.ematch] new ground fact: tt && tt = tt
[smt.ematch] new ground fact: bxor tt tt = ff
[smt.ematch] new ground fact: nat.bodd 1 = tt
[smt.ematch] new ground fact: nat.bodd 0 = ff
[smt.ematch] new ground fact: ↥ff = false
[smt.fact] new facts: {↥ff}
[smt.ematch] new ground fact: ↥tt = true
[smt.fact] new facts: {↥tt}
[smt.ematch] new ground fact: int.sign 1 = 1
[smt.ematch] new ground fact: int.sign 0 = 0
[smt.ematch] new ground fact: nat.pred 0 = 0
[smt.ematch] new ground fact: nat.div2 0 = 0
[smt.ematch] new ground fact: nat.div2 1 = 0
[smt.ematch] new ground fact: nat.bodd 2 = ff
[smt.ematch] new ground fact: nat.bit ff 0 = 0
[smt.ematch] new ground fact: nat.div2 2 = 1
[smt.ematch] new ground fact: ↑tt = true
[smt.fact] new facts: {↑tt}
[smt.ematch] new ground fact: ↑ff = false
[smt.fact] new facts: {↑ff}
[smt.ematch] new ground fact: int.sign (-1) = -1
[smt.ematch] instance [bor_self], generation: 1
ff || ff = ff
[smt.ematch] instance [band_self], generation: 1
tt && tt = tt
[smt.ematch] instance [bxor_ff], generation: 1
bxor ff ff = ff
[smt.ematch] instance [bxor_ff], generation: 1
bxor tt ff = tt
[smt.ematch] instance [bnot_bnot], generation: 1
bnot (bnot tt) = tt
[smt.ematch] instance [bnot_bnot], generation: 1
bnot (bnot ff) = ff
[smt.ematch] instance [bor_ff], generation: 1
ff || ff = ff
[smt.ematch] instance [eeval.equations._eqn_1], generation: 1
eeval (Const n) = n
[smt.ematch] instance [tt_band], generation: 1
tt && ff = ff
[smt.ematch] instance [tt_band], generation: 1
tt && tt = tt
[smt.ematch] instance [ff_bxor], generation: 1
bxor ff ff = ff
[smt.ematch] instance [ff_bxor], generation: 1
bxor ff tt = tt
[smt.ematch] instance [ff_bor], generation: 1
ff || ff = ff
[smt.ematch] instance [ff_bor], generation: 1
ff || tt = tt
[smt.ematch] instance [band_tt], generation: 1
tt && tt = tt
[smt.ematch] instance [bxor_self], generation: 1
bxor ff ff = ff
[smt.ematch] instance [bxor_self], generation: 1
bxor tt tt = ff
[smt.ematch] instance [band_ff], generation: 1
tt && ff = ff
[smt.ematch] instance [bor_tt], generation: 1
ff || tt = tt
[smt.ematch] instance [tt_bxor], generation: 1
bxor tt tt = bnot tt
[smt.ematch] instance [tt_bxor], generation: 1
bxor tt ff = bnot ff
[smt.ematch] instance [bxor_tt], generation: 1
bxor tt tt = bnot tt
[smt.ematch] instance [bxor_tt], generation: 1
bxor ff tt = bnot ff
[smt.ematch] instance [reassoc._match_1.equations._eqn_1], generation: 1
reassoc._match_1 (reassoc e_e1) (Const n) (Const n) = Plus (reassoc e_e1) (Const n)
[smt.ematch] instance [bnot_eq_true_eq_eq_ff], generation: 1
bnot ff = tt = (ff = ff)
[smt.ematch] instance [bnot_eq_ff_eq_eq_tt], generation: 1
bnot tt = ff = (tt = tt)
[smt.ematch] instance [bxor_coe_iff], generation: 1
↥(bxor ff ff) ↔ xor ↥ff ↥ff
[smt.ematch] instance [bxor_coe_iff], generation: 1
↥(bxor tt tt) ↔ xor ↥tt ↥tt
[smt.ematch] instance [bxor_coe_iff], generation: 1
↥(bxor ff tt) ↔ xor ↥ff ↥tt
[smt.ematch] instance [bxor_coe_iff], generation: 1
↥(bxor tt ff) ↔ xor ↥tt ↥ff
[smt.ematch] instance [band_coe_iff], generation: 1
↥(tt && ff) ↔ ↥tt ∧ ↥ff
[smt.ematch] instance [band_coe_iff], generation: 1
↥(tt && tt) ↔ ↥tt ∧ ↥tt
[smt.ematch] instance [bor_coe_iff], generation: 1
↥(ff || ff) ↔ ↥ff ∨ ↥ff
[smt.ematch] instance [bor_coe_iff], generation: 1
↥(ff || tt) ↔ ↥ff ∨ ↥tt
[smt.ematch] instance [band_eq_true_eq_eq_tt_and_eq_tt], generation: 1
tt && tt = tt = (tt = tt ∧ tt = tt)
[smt.ematch] instance [band_eq_false_eq_eq_ff_or_eq_ff], generation: 1
tt && ff = ff = (tt = ff ∨ ff = ff)
[smt.ematch] instance [bor_eq_true_eq_eq_tt_or_eq_tt], generation: 1
ff || tt = tt = (ff = tt ∨ tt = tt)
[smt.ematch] instance [bor_eq_false_eq_eq_ff_and_eq_ff], generation: 1
ff || ff = ff = (ff = ff ∧ ff = ff)
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt ff = tt
[smt.ematch] instance, generation: 1, after preprocessing
bnot (bnot tt) = tt
[smt.ematch] instance, generation: 1, after preprocessing
bnot (bnot ff) = ff
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
eeval (Const n) = n
[smt.ematch] instance, generation: 1, after preprocessing
tt && ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
ff || tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt tt = ff
[smt.ematch] instance, generation: 1, after preprocessing
tt && ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
ff || tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt tt = bnot tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt ff = bnot ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt tt = bnot tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff tt = bnot ff
[smt.ematch] instance, generation: 1, after preprocessing
reassoc._match_1 (reassoc e_e1) (Const n) (Const n) = Plus (reassoc e_e1) (Const n)
[smt.ematch] instance, generation: 1, after preprocessing
bnot ff = tt = (ff = ff)
[smt.fact] new facts: {ff = ff, bnot ff = tt}
[smt.ematch] instance, generation: 1, after preprocessing
bnot tt = ff = (tt = tt)
[smt.fact] new facts: {tt = tt, bnot tt = ff}
[smt.ematch] instance, generation: 1, after preprocessing
↥(bxor ff ff) ↔ xor ↥ff ↥ff
[smt.fact] new facts: {↥(bxor ff ff), xor ↥ff ↥ff}
[smt.ematch] instance, generation: 1, after preprocessing
↥(bxor tt tt) ↔ xor ↥tt ↥tt
[smt.fact] new facts: {↥(bxor tt tt), xor ↥tt ↥tt}
[smt.ematch] instance, generation: 1, after preprocessing
↥(bxor ff tt) ↔ xor ↥ff ↥tt
[smt.fact] new facts: {↥(bxor ff tt), xor ↥ff ↥tt}
[smt.ematch] instance, generation: 1, after preprocessing
↥(bxor tt ff) ↔ xor ↥tt ↥ff
[smt.fact] new facts: {↥(bxor tt ff), xor ↥tt ↥ff}
[smt.ematch] instance, generation: 1, after preprocessing
↥(tt && ff) ↔ ↥tt ∧ ↥ff
[smt.fact] new facts: {↥tt ∧ ↥ff, ↥(tt && ff)}
[smt.ematch] instance, generation: 1, after preprocessing
↥(tt && tt) ↔ ↥tt ∧ ↥tt
[smt.fact] new facts: {↥tt ∧ ↥tt, ↥(tt && tt)}
[smt.ematch] instance, generation: 1, after preprocessing
↥(ff || ff) ↔ ↥ff ∨ ↥ff
[smt.fact] new facts: {↥ff ∨ ↥ff, ↥(ff || ff)}
[smt.ematch] instance, generation: 1, after preprocessing
↥(ff || tt) ↔ ↥ff ∨ ↥tt
[smt.fact] new facts: {↥ff ∨ ↥tt, ↥(ff || tt)}
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt = (tt = tt ∧ tt = tt)
[smt.fact] new facts: {tt = tt ∧ tt = tt, tt && tt = tt}
[smt.ematch] instance, generation: 1, after preprocessing
tt && ff = ff = (false ∨ ff = ff)
[smt.fact] new facts: {false ∨ ff = ff, tt && ff = ff}
[smt.ematch] instance, generation: 1, after preprocessing
ff || tt = tt = (false ∨ tt = tt)
[smt.fact] new facts: {false ∨ tt = tt, ff || tt = tt}
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff = (ff = ff ∧ ff = ff)
[smt.fact] new facts: {ff = ff ∧ ff = ff, ff || ff = ff}
[smt.ematch] instance [eeval.equations._eqn_2], generation: 2
eeval (Plus (reassoc e_e1) (Const n)) = eeval (reassoc e_e1) + eeval (Const n)
[smt.ematch] instance, generation: 2, after preprocessing
eeval (Plus (reassoc e_e1) (Const n)) = eeval (reassoc e_e1) + eeval (Const n)
[smt.fact] new facts: {eeval (reassoc._match_1 (reassoc e_e1) (Const n) (Const n)) = eeval e_e1 + eeval e_e2}
cpdt.lean:58:48: information trace output
[smt.intro] e_e1 : exp
[smt.intro] e_e2 : exp
[smt.fact] new facts: {eeval (reassoc e_e1) = eeval e_e1}
[smt.intro] e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1
[smt.intro] e1 : exp
[smt.intro] e2 : exp
[smt.fact] new facts: {eeval (Plus e1 e2) = eeval e_e2}
[smt.intro] e_ih_e2 : eeval (Plus e1 e2) = eeval e_e2
[smt.ematch] new ground fact: bnot ff = tt
[smt.ematch] new ground fact: bnot tt = ff
[smt.ematch] new ground fact: bxor ff tt = tt
[smt.ematch] new ground fact: bxor tt ff = tt
[smt.ematch] new ground fact: ff || tt = tt
[smt.ematch] new ground fact: bxor ff ff = ff
[smt.ematch] new ground fact: 0 = 0
[smt.ematch] new ground fact: tt && ff = ff
[smt.ematch] new ground fact: ff || ff = ff
[smt.ematch] new ground fact: tt && tt = tt
[smt.ematch] new ground fact: bxor tt tt = ff
[smt.ematch] new ground fact: nat.bodd 1 = tt
[smt.ematch] new ground fact: nat.bodd 0 = ff
[smt.ematch] new ground fact: ↥ff = false
[smt.fact] new facts: {↥ff}
[smt.ematch] new ground fact: ↥tt = true
[smt.fact] new f

[Johan Commelin]

@Gabriel Ebner How do you feel about commenting out the remaining tests?

[Johan Commelin]

We are talking about

99% tests passed, 5 tests failed out of 1359

Total Test time (real) = 169.26 sec

The following tests FAILED:
        688 - leanruntest_cpdt.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

[Gabriel Ebner]

Yeah, ematching tests -> remove

[Gabriel Ebner]

cpdt -> remove

[Gabriel Ebner]

using_smt2 -> is everything broken? That would be bad. If it's just two examples or so -> remove the examples.

[Johan Commelin]

Ok, I'll do that

[Johan Commelin]

Done and pushed.
But locally it still says

The following tests FAILED:
        688 - leanruntest_cpdt.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)

even though I removed those tests from tests/lean/run/*

[Gabriel Ebner]

Locally? You need to re-run cmake.

[Johan Commelin]

Aha

[Johan Commelin]

I've pushed... this PR is now touching 106 files :shock:

[Gabriel Ebner]

To come back to your question from the other thread: should we make a release before we merge this PR?

[Johan Commelin]

I think it makes sense. I certainly don't feel brave enough to fix mathlib after the 6 different PR that we now have in core...

[Johan Commelin]

I prefer to take small steps. But I don't have a good overview.

[Johan Commelin]

This has very much been a cargo cult PR from my side

[Gabriel Ebner]

There's still one failing test. I'll then get 3.12 out of the door today, and we can think about 3.13 tomorrow.

[Johan Commelin]

Yes, I just noticed the failing test. It should be fixed now.

[Johan Commelin]

Hooray! Locally it builds without errors and all the (remaining) tests pass!