Using `dec_trivial` to prove equality

Stream: new members

[Yakov Pechersky]

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]

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]

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

[Alex J. Best]

What happens if you try rfl or by refl?

[Alex J. Best]

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

[Yakov Pechersky]

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]

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]

I see you've used strings. Case closed.

[Mario Carneiro]

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

[Yakov Pechersky]

board.reduce is equality of finite matrices

[Yakov Pechersky]

the #eval part just uses a has_repr

[Mario Carneiro]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Ah I see what you mean

[Mario Carneiro]

the kernel can't handle string equality evaluation at all

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yakov Pechersky]

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]

right

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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