Zulip Chat Archive

Stream: new members

Topic: Using `dec_trivial` to prove equality


view this post on Zulip Yakov Pechersky (Dec 29 2020 at 19:53):

I have two complex terms that via #eval are equal. I'm trying to prove that these terms are equal via ... = ... := dec_trivial. Yet I get

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

Is that really the case, or am I down a forsaken path?

view this post on Zulip Julian Berman (Dec 29 2020 at 21:11):

in case you didn't try it, I'm pretty sure I've seen that exact error message once and restarting lean made it go away somehow

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:20):

This occurs even with leanproject build which is a wrapper for lean --make src, and I got the same error.

view this post on Zulip Alex J. Best (Dec 29 2020 at 21:22):

What happens if you try rfl or by refl?

view this post on Zulip Alex J. Best (Dec 29 2020 at 21:22):

It might help to say a little more about what the terms are?

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:38):

rfl has the same issue. You can see the files and output at https://github.com/Julian/lean-across-the-board/blob/list/src/guarini.lean. The list branch compiles cleanly except for that one statement, so you can clone and try it out!

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:44):

Kernel evaluation doesn't scale very well; it can't handle numbers larger than ~20. You should use norm_num for better evaluation

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:44):

I see you've used strings. Case closed.

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:46):

Oh I see, this is what all that verified parser stuff was about

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:46):

board.reduce is equality of finite matrices

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:46):

the #eval part just uses a has_repr

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:47):

The final statement makes reference to guarini_algebraic which is a list of strings

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:47):

The proofs above show that doing moves exactly specified by (start_square, end_square) provably give the ending_position.

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:47):

Ah I see what you mean

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:48):

the kernel can't handle string equality evaluation at all

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:48):

I'm not sure exactly how the parser is implemented but I would assume it eventually boils down to a string and/or character equality test

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:49):

You might have some luck with the reverse: constructing the string and proving it is equal to a given string literal

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:50):

so if your parser is invertible that might be an alternative way to get the kernel to believe that the parser would evaluate to X without actually running it

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:50):

Aha, I had hoped the parser part itself wasn't a necessary part of the proof, that somehow the string -> description structure would just work.

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:51):

It's not invertible because chess notation is fuzzy, it's many to one dependent on board state unfortunately.

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:51):

If you can prove that part separately, you might be able to remove it from the dec_trivial

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:51):

Here we only need the chess notation to evaluate to "parsed chess notation" in some reasonable inductive type

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:52):

the kernel can probably handle working with the latter (it may sweat a bit but it shouldn't timeout)

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 21:54):

So two proofs, that each thing in the list of strings parses to a valid description, and that a different one that the list of description does the correct sequence?

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:56):

right

view this post on Zulip Mario Carneiro (Dec 29 2020 at 21:56):

the first one you can prove by simp or so, and the second with rfl

view this post on Zulip Mario Carneiro (Dec 29 2020 at 22:07):

It's also an option to pre-evaluate the parser to build the list of descriptions, and insert that directly into the theorem statement using a tactic, if you don't care about proving that the parsing goes to plan

view this post on Zulip Yakov Pechersky (Dec 29 2020 at 22:19):

Yes, I'd have to write that tactic though, and I've kept delaying learning about how to do that

view this post on Zulip Mario Carneiro (Dec 29 2020 at 23:35):

That's actually the easier option. You just call eval_expr to evaluate the expression as you would with #eval, then reflect to insert it into the theorem statement. The option using simp is likely to be more complicated because you will have to simplify a ton of things and even then you will probably get stuck at some decision procedure or other


Last updated: May 16 2021 at 05:21 UTC