exact tactic

Stream: new members

[Joseph O]

I looked at the documentation for exact, but I still cant understand how this works image.png

[Arthur Paulino]

If you check the definition of mul you'll see that m * 1 can be unfolded to m * 0 + m, which can be simplified to 0 + m. Thus, what you have to prove becomes 0 + m = m, which is exactly zero_add

[Jireh Loreaux]

"can be simplified" -> "is definitionally equal to"

[Arthur Paulino]

The exact tactic is flexible enough to unify things that are definitionally equal but aren't spelled in the exact same way

[Joseph O]

Arthur Paulino said:

If you check the definition of mul you'll see that m * 1 can be unfolded to m * 0 + m, which can be simplified to 0 + m. Thus, what you have to prove becomes 0 + m = m, which is exactly zero_add

now my question is where does it simplify this under the hood?

[Notification Bot]

Joseph O has marked this topic as unresolved.