Zulip Chat Archive

Stream: new members

Topic: Using `dec_trivial` to prove equality


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?

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

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.

Alex J. Best (Dec 29 2020 at 21:22):

What happens if you try rfl or by refl?

Alex J. Best (Dec 29 2020 at 21:22):

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

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!

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

Mario Carneiro (Dec 29 2020 at 21:44):

I see you've used strings. Case closed.

Mario Carneiro (Dec 29 2020 at 21:46):

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

Yakov Pechersky (Dec 29 2020 at 21:46):

board.reduce is equality of finite matrices

Yakov Pechersky (Dec 29 2020 at 21:46):

the #eval part just uses a has_repr

Mario Carneiro (Dec 29 2020 at 21:47):

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

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.

Yakov Pechersky (Dec 29 2020 at 21:47):

Ah I see what you mean

Mario Carneiro (Dec 29 2020 at 21:48):

the kernel can't handle string equality evaluation at all

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

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

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

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.

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.

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

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

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)

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?

Mario Carneiro (Dec 29 2020 at 21:56):

right

Mario Carneiro (Dec 29 2020 at 21:56):

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

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

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

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: Dec 20 2023 at 11:08 UTC