Proving basic nat arithmetic equality

Stream: new members

[Matei Adriel]

Hello, I am new to lean. I am trying to prove
I am trying to pattern match on c. The zero case is trivial, but I'm not sure how to handle the succ case.

Thanks in advance

[Arthur Paulino]

It's better if you paste code with #backticks instead of pasting images.

example : ∀ {a b c : Nat}, a + c = b + c → a = b := sorry
example {a b c : Nat} : a + c = b + c → a = b := sorry
example {a b c : Nat} (h : a + c = b + c) : a = b := sorry

The bottom one is how you'll see in mathlib more often

[Matei Adriel]

@Arthur Paulino yeah, sorry about that

[Matei Adriel]

theorem subtract_to_equation: ∀{a b c: Nat}, a + c = b + c → a = b := by
  intro a b c acbc
  cases c with
  | zero => simp_all
  | succ pc =>
    have inner: a + pc = b + pc → a = b := subtract_to_equation
    simp_all
    sorry

this is what I have right now

[Matei Adriel]

In particular this feels uncomfortable because the c is in a negative-ish position while the tutorials usually use induction on a positive position

[Arthur Paulino]

A few things:

• Are you aware of what simp_all is doing? I'd go a bit slower at this point in order to attain a better understand what's going on
• You shouldn't be using the theorem to prove itself. It sounds either super hacky or just logically cyclic
• have you tried induction?

[Matei Adriel]

@Arthur Paulino Yes, what I am doing there is basically induction on c. C is just implicit so it doesn't look like it

[Arthur Paulino]

An induction will add an inductive hypothesis to your context:

theorem subtract_to_equation: ∀ {a b c: Nat}, a + c = b + c → a = b := by
  intro a b c acbc
  induction c with
  | zero =>
    simp at acbc
    exact acbc
  | succ pc ih =>
    sorry

[Matei Adriel]

@Arthur Paulino Oo, I didn't know there was a tactic for that (although that's exactly what I was doing before, just not by hand)

[Matei Adriel]

wait, actually

[Matei Adriel]

you are probably right, let me see

[Matei Adriel]

nah, nevermind, it does seem to be doing the same thing

[Kyle Miller]

Arthur Paulino said:

You shouldn't be using the theorem to prove itself. It sounds either super hacky or just logically cyclic

It can be OK -- it's just a recursive function call, and Lean will make sure it's well-founded. It does feel more fiddly than using induction though, since induction gives you the guaranteed safe way to recurse in the form of the induction hypothesis.

[Arthur Paulino]

@Matei Adriel try #check Nat.add_right_cancel and ctrl+click on it

[Arthur Paulino]

@Kyle Miller Is there a toy example of this you can think of? I've never seen it

[Kyle Miller]

Matei Adriel said:

theorem subtract_to_equation: ∀{a b c: Nat}, a + c = b + c → a = b := by
  intro a b c acbc
  cases c with
  | zero => simp_all
  | succ pc =>
    have inner: a + pc = b + pc → a = b := subtract_to_equation
    simp_all
    sorry

this is what I have right now

I'm not checking this in Lean 4, but I think you might be able to do is rewrite your acbc hypothesis to Nat.succ (a + pc) = Nat.succ (b + pc), simplify that to remove the Nat.succ, then do exact inner acbc.

[Matei Adriel]

@Arthur Paulino thanks, didn't know that was a built in thing

@Kyle Miller howdo I "simply that to remove the succ"?

[Kyle Miller]

@Arthur Paulino I just found one in mathlib: https://github.com/leanprover-community/mathlib/blob/master/src/combinatorics/simple_graph/connectivity.lean#L397 (the last line of that lemma is a recursive use of the lemma to do induction)

[Kyle Miller]

@Matei Adriel I'm not sure off the top of my head -- does simp at acbc do it?

[Kyle Miller]

@Matei Adriel Or it might be injection acbc