Rewrite with add_sub doesn't work

Stream: general

[Yufan Lou]

I'd like to rewrite the left hand side of length l + (n - length l) = max n (length l) to n, but rw add_sub gives me this error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_3 + (?m_4 - ?m_5)

How may I tell Lean that ?m_3 and ?m_5 should be length l?

[Mario Carneiro]

That's not the problem. Lean would match that if it could, but what lean is not doing a very good job of saying is that + and - in the pattern are not the same as the + and - in your goal

[Mario Carneiro]

because nat subtraction (in your goal) is not the same as subtraction in a group (which is what the theorem you are applying is about)

[Mario Carneiro]

You need to use nat.add_sub

[Yufan Lou]

ah that's why if I try to rw add_sub _ n _ I get a cannot synthesize class instance error for add_group nat

[Mario Carneiro]

Right, because nat is not an additive group

[Mario Carneiro]

However, most theorems about additive groups have analogues on nat, with the same names with nat. in front

[Mario Carneiro]

they usually have extra side conditions about things being less than other things

[Yufan Lou]

I'm using https://leanprover.github.io/live , is the theorem up there yet?

[Mario Carneiro]

I may have guessed the names wrong but all of these theorems are quite old

[Mario Carneiro]

It's nat.add_sub_of_le

[Yufan Lou]

rw ←nat.add_sub_assoc worked too thx

[Mario Carneiro]

add_sub_assoc says something else

[Yufan Lou]

oh nat.add_sub_of_le gets me straight to n nice thx
it didn't show up in the autocomplete tho

[Mario Carneiro]

Even better, nat.sub_add_eq_max is almost exactly your statement, after commuting on the left

[Yufan Lou]

unknown identifier 'nat.sub_add_eq_max' :shrug:‍♂️

[Mario Carneiro]

import data.nat.basic

[Yufan Lou]

open nat doesn't give me a lot huh

[Mario Carneiro]

open nat doesn't do anything except allow you to leave off the nat. on lemmas

[Mario Carneiro]

import loads new files into your session so you have more theorems

[Mario Carneiro]

data.nat.basic is the mathlib file for all the missing nat lemmas

[Yufan Lou]

ahh i see

[Kevin Buzzard]

There is a much newer and better version of Lean online at leanprover-community

[Kevin Buzzard]

https://leanprover-community.github.io/lean-web-editor/

[Kevin Buzzard]

It has a much more up to date lean and mathlib