# Zulip Chat Archive

## Stream: new members

### Topic: Syntax of equality and calculational proofs

#### Brandon Wu (May 19 2020 at 04:29):

Hi, I'm currently working through the "equality and calculational proofs" section (in First-order logic in Lean) of the Logic and Proofs course, but I'm having some trouble understanding the syntax of equality proofs. In particular, I'm a little confused on the use of the rewrite command. The tutorial says that I can "rewrite" the goal of a particular proof (in this case, x = z) to be y = z by using the syntax "rewrite \<- h1 : y = x". My question is, how do you know what rules are applicable and parsable through this method? What makes the use of \<- essential here, as I can't really see how this rule is being "applied" in the first place - in my intuition, I would think that you would consider "eq.subst" or something similar to be the "rule" that you would need to use. Similarly for the usage of "calc", when it says I can write "calc e1 = e2 : justification 1", is "justification 1" literally just a justification, or should I interpret it as a type? Thanks!

#### Mario Carneiro (May 19 2020 at 04:32):

use #backticks to quote code

#### Mario Carneiro (May 19 2020 at 04:34):

how do you know what rules are applicable and parsable through this method?

I'm not sure I understand the question. When you use `rw (h1 : y = x)`

, it will rewrite all occurrences of `y`

to `x`

in the goal; when you use `rw <- (h1 : y = x)`

it rewrites `x`

to `y`

instead. Since the goal is `x = z`

, the first one would have no effect because there are no `y`

's in the goal, but the second will have an effect and result in the new goal `y = z`

#### Mario Carneiro (May 19 2020 at 04:35):

Similarly for the usage of "calc", when it says I can write "calc e1 = e2 : justification 1", is "justification 1" literally just a justification, or should I interpret it as a type?

"justification 1" is a term proof of `e1 = e2`

, by any means you would like

#### Mario Carneiro (May 19 2020 at 04:39):

What makes the use of \<- essential here, as I can't really see how this rule is being "applied" in the first place - in my intuition, I would think that you would consider "eq.subst" or something similar to be the "rule" that you would need to use.

`rw`

uses `eq.subst`

under the hood. But its user level semantics is as I described; it replaces occurrences of the lhs of the input theorem in the goal with the rhs. In order to do that it applies the theorem `eq.rec_on : P a -> a = b -> P b`

, and has to come up with an appropriate value for `P`

such that `P b`

reduces to the goal and `P a`

reduces to what we want the new subgoal to be. (It also has to flip the equality when applying this theorem if you don't use `<-`

here.)

#### Brandon Wu (May 19 2020 at 04:42):

Is `rewrite`

unique to equality proofs, then? It would make more sense to me if these were, in a sense, just "hardcoded" to behave exactly how you would intuitively believe it to. Rewriting a goal of `x = z`

to `y = z`

by knowing that `y = x`

is very intuitively clear.

#### Mario Carneiro (May 19 2020 at 04:43):

yes, `rw h`

only works if `h`

is either an equality or an iff, and in the latter case it applies `propext`

to turn it into an equality anyway

#### Mario Carneiro (May 19 2020 at 04:45):

However the goal doesn't have to be an equality; the interesting case is when you have something like `|- foo (a + bar b) > 7`

and you `rw (h : b = c)`

to get the new goal `|- foo (a + bar c) > 7`

#### Mario Carneiro (May 19 2020 at 04:46):

In your example you don't really need `rw`

as you could use transitivity instead of substitution

Last updated: May 13 2021 at 18:26 UTC