Zulip Chat Archive

Stream: general

Topic: Rewrite with add_sub doesn't work


Yufan Lou (Feb 21 2020 at 08:28):

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 (Feb 21 2020 at 08:30):

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 (Feb 21 2020 at 08:31):

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 (Feb 21 2020 at 08:31):

You need to use nat.add_sub

Yufan Lou (Feb 21 2020 at 08:32):

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 (Feb 21 2020 at 08:33):

Right, because nat is not an additive group

Mario Carneiro (Feb 21 2020 at 08:33):

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

Mario Carneiro (Feb 21 2020 at 08:34):

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

Yufan Lou (Feb 21 2020 at 08:34):

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

Mario Carneiro (Feb 21 2020 at 08:34):

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

Mario Carneiro (Feb 21 2020 at 08:35):

It's nat.add_sub_of_le

Yufan Lou (Feb 21 2020 at 08:36):

rw ←nat.add_sub_assoc worked too thx

Mario Carneiro (Feb 21 2020 at 08:36):

add_sub_assoc says something else

Yufan Lou (Feb 21 2020 at 08:38):

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

Mario Carneiro (Feb 21 2020 at 08:38):

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

Yufan Lou (Feb 21 2020 at 08:40):

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

Mario Carneiro (Feb 21 2020 at 08:40):

import data.nat.basic

Yufan Lou (Feb 21 2020 at 08:40):

open nat doesn't give me a lot huh

Mario Carneiro (Feb 21 2020 at 08:41):

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

Mario Carneiro (Feb 21 2020 at 08:41):

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

Mario Carneiro (Feb 21 2020 at 08:41):

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

Yufan Lou (Feb 21 2020 at 08:42):

ahh i see

Kevin Buzzard (Feb 21 2020 at 09:29):

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

Kevin Buzzard (Feb 21 2020 at 09:29):

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

Kevin Buzzard (Feb 21 2020 at 09:30):

It has a much more up to date lean and mathlib


Last updated: Dec 20 2023 at 11:08 UTC