Syntax of equality and calculational proofs

Stream: new members

[Brandon Wu]

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]

use #backticks to quote code

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

In your example you don't really need rw as you could use transitivity instead of substitution