Zulip Chat Archive

Stream: new members

Topic: Accessing LHS / RHS from equation

Daniel Fabian (May 11 2020 at 13:55):

Is there an easy way to access the LHS / RHS of an equation without rewriting it?

example : (∀ a b c : ℤ, a = b - b ∧ c = -b + b → a = c) :=
begin
    intros a b c h,
    cases h with hab hbc,
end

here, I'd like to do something like,

have h_rhs: hab.right = hbc.left, by { ring },
calc hab.lhs = hab.rhs : hab,
         ... = hbc.rhs : h_rhs,
         ... = hbc.lhs : hbc,

Is that kind of thing possible, or would I have to go and copy the whole sub-expression?

Johan Commelin (May 11 2020 at 13:56):

Do you mean something like conv?

Reid Barton (May 11 2020 at 14:05):

You can define them yourself:

import tactic

@[reducible] def eq.lhs {α : Type*} {x y : α} (e : x = y) : α := x
@[reducible] def eq.rhs {α : Type*} {x y : α} (e : x = y) : α := y

example : (∀ a b c : ℤ, a = b - b ∧ c = -b + b → a = c) :=
begin
    intros a b c h,
    cases h with hab hbc,
    have h_rhs: hab.rhs = hbc.rhs, by { ring },
    calc hab.lhs = hab.rhs : hab
         ... = hbc.rhs : h_rhs
         ... = hbc.lhs : hbc.symm,
end

Reid Barton (May 11 2020 at 14:05):

(I had to fix a few math and syntax errors)

Kevin Buzzard (May 11 2020 at 14:05):

you should charge extra

Daniel Fabian (May 11 2020 at 14:06):

oh wow, I didn't know you could extend the language like that. That's exactly what I was looking for. This is a lot more refactoring-friendly.

Kevin Buzzard (May 11 2020 at 14:07):

Every theorem you prove is extending the language in that way, right?

Kevin Buzzard (May 11 2020 at 14:07):

hbc.rhs is just syntax sugar for eq.rhs hbc, because the type of hbc is eq (something)

Patrick Massot (May 11 2020 at 14:07):

We should have this in mathlib actually. This is a very natural question

Kevin Buzzard (May 11 2020 at 14:08):

yeah this is really cool

Daniel Fabian (May 11 2020 at 14:09):

well, syntax does matter, though. All of lean could just be lambda abstractions without any syntax at all apart from lambda abstractions... and it would not be the same.

Daniel Fabian (May 11 2020 at 14:10):

So yes, proving things can be reused, but it was important to be somehow pretty to write. And .lhs .rhs didn't show up in my intellisense.

Patrick Massot (May 11 2020 at 14:10):

Sure, Reid just added them for you

Johan Commelin (May 11 2020 at 14:11):

But they don't look nice in the tactic state, last time I tried

Reid Barton (May 11 2020 at 14:12):

Yes, the goal to be solved by ring is literally shown as hab.rhs = hbc.rhs.

Reid Barton (May 11 2020 at 14:12):

I thought ring was stuck on this for a while, until I noticed that the goal was false because of various typos

Patrick Massot (May 11 2020 at 14:13):

Daniel, you should also get used to statements like: ∀ a b c : ℤ, a = b - b → c = -b + b → a = c (double implication instead of conjunction). It's way more convenient