## 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?

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: May 16 2021 at 05:21 UTC