Zulip Chat Archive

Stream: new members

Topic: Proving two inequalities in a single calc line

Gunnar Þór Magnússon (Jan 29 2021 at 19:56):

I'm working through the Lean tutorial and have one example down to a fairly standard triangle inequality calculation. I basically have this:

  calc |u p - u q| = |u p - l - (u q - l)| : by ring
  ...  |u p - l| + |u q - l| : by apply ad_hoc_lemma
  ...  ε/2 + ε/2 : by exact hN p hp; exact hN q hq
  ... = ε : by linarith,

where hN takes an integer p, a proof hp that it is greater than some fixed number, and outputs a proof that |u p - l| <= \epsilon.

My problem is in the third line, which Lean doesn't like. I'd like to apply two inequalities at once, that |u p - l| <= \epsilon and |u q - l| <= \epsilon but can't figure out the syntax to do so. Any hints?

Mario Carneiro (Jan 29 2021 at 20:00):


Mario Carneiro (Jan 29 2021 at 20:01):

You shouldn't be using exact twice; rather you should apply add_le_add, which produces two subgoals, that are then closed by exact

Mario Carneiro (Jan 29 2021 at 20:02):

so that means something like by apply add_le_add; [exact hN p hp, exact hN q hq] or more simply add_le_add (hN p hp) (hN q hq) since this is basically just a term proof, you don't need by anything

Gunnar Þór Magnússon (Jan 29 2021 at 20:06):

Sorry for not posting an mwe. Will do that next time.

But thanks for the hint. That did it. I'm still learning the ins and outs here.

Patrick Massot (Jan 29 2021 at 20:11):

You don't have to remember add_le_add, you can use linarith [hN p hp, hN q hq],

Last updated: Dec 20 2023 at 11:08 UTC