Int and Nat subtraction

Stream: new members

[Kajani Kaunda]

Hello Good people,

I need some help solving this lemma:

import Mathlib

lemma lemma_int_nat_subtractions (a b : ℤ) (h : b ≤ a)
: (a - b).toNat = a.toNat - b.toNat :=
by sorry

The code intends to prove that for two integers a and b, if a is greater than or equal to b, the natural number representation of their difference (a - b) is equal to the difference of their individual natural number representations (a.toNat - b.toNat).

Many thanks in advance.

[Aaron Liu]

Does grind work

[Kajani Kaunda]

Aaron Liu said:

Does grind work

I did not try that...

[Kajani Kaunda]

Kajani Kaunda said:

Aaron Liu said:

Does grind work

I did not try that...

import Mathlib

lemma lemma_a (a b : ℤ) (h : b ≤ a)

: (a - b).toNat = a.toNat - b.toNat :=

by grind --sorry

Grind failed. I hope I applied it correctly though!

[Aaron Liu]

Oh I have a counterexample with a := 1 and b := -1

[Kajani Kaunda]

Aaron Liu said:

Oh I have a counterexample with a := 1 and b := -1

mmm, so maybe we need another hypothesis that 0 <= b, yes?

[Aaron Liu]

maybe, if you add that hypothesis does grind work

[Kajani Kaunda]

Aaron Liu said:

maybe, if you add that hypothesis does grind work

Just tested it, ...

import Mathlib

lemma lemma_a (a b : ℤ) (h : b ≤ a) ( hz : 0 ≤ b)
: (a - b).toNat = a.toNat - b.toNat :=
by grind --sorry

and grind works!

[Jakub Nowak]

Or just cutsat or omega works too.

[Kajani Kaunda]

@Aaron Liu Great! thank you so much @ ! Now let me see if I can make good use of this lemma! I really appreciate your helping me!

[Kajani Kaunda]

Jakub Nowak said:

Or just cutsat or omega works too.

Oh! that's good to know! Thank you too @Jakub Nowak

[Riccardo Brasca]

Note that plausible immediately finds a counterexample to your original statement.

[Kajani Kaunda]

Riccardo Brasca said:

Note that plausible immediately find a counterexample to your original statement.

plausible, first time hearing about that...I will use that

[Jakub Nowak]

Hm, maybe hint should try plausible too, and report if it finds counterexample?

[Kajani Kaunda]

and what is the syntax for "plausible" ? I see "hint" is something like: Hint Resolve my_theorem_name : some_hint_database_name

[Riccardo Brasca]

import Mathlib

lemma lemma_int_nat_subtractions (a b : ℤ) (h : b ≤ a) :
    (a - b).toNat = a.toNat - b.toNat := by
  plausible

[Jakub Nowak]

Both hint and plausible are just tactics. You need import Mathlib for them.

[Kajani Kaunda]

Riccardo Brasca said:

import Mathlib

lemma lemma_int_nat_subtractions (a b : ℤ) (h : b ≤ a) :
    (a - b).toNat = a.toNat - b.toNat := by
  plausible

Ah, I see! I need a definitive book on Lean 4 syntax!

[Kajani Kaunda]

Wow! you guys have just made my life so much easier tenfold! Thank you to you all! But I will be back in a flash if I get stuck on anything else - after first trying out a few things of course!!