changing gt to gte for integers

Stream: new members

[rzeta0]

I have a hypothesis about an integer a

a : ℤ
hb : a > 2

I'd like to turn this into

a : ℤ
hb : a ≥ 3

based on the idea that the successor to 2 is 3.

How can I do this?

(I've searched Moogle with no success, using search terms including gte of gt, succ, integer)

[Yakov Pechersky]

Does replace hb : a ≥ 3 := by omega work?

[lyphyser]

The best way to solve issues like this is to ask Lean about it:

def foo (a: ℤ) (hb: a > 2): a ≥ 3 := by
  apply?

or rw? instead of apply? if it's about a rewrite

In this case, "exact hb" is the answer, since a < b is defined as (a + 1) <= b and thus b > a is defined as b >= (a + 1)

[rzeta0]

Thanks for the replies.

I'm a beginner and at this point in the course (Heather Macbeth's) we aren't expected to use advanced tactics like omega or asking lean via ?

I think we are expected to search for simpler lemmas like le_or_gt.

---

The exercise is simple to express:

example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by

And the hint is to use a proof by cases, which suggests splitting a into something like a <= 2 and a >2. The first case I can do, the second seems to require me to transition from a>2 to a>=3 by virtue of a being an integer.

[rzeta0]

I'm currently searching moogle for "​gt equals gte successor" and Order.lt_succ_iff_eq_or_lt looks related but the wrong way around, there doesn't appear to be a gt version.

[Damiano Testa]

You should treat x > y as an illusion and imagine that it is y < x: Lean will play along.

[Daniel Weber]

Maybe there's docs#Nat.add_one_le_of_lt ?

[Violeta Hernández]

fyi to talk about successors of natural numbers, just use a + 1

[rzeta0]

Daniel Weber said:

Maybe there's docs#Nat.add_one_le_of_lt ?

unknown tactic?

I think MacBeth's course environment might be lean3? such a shame as this looks ideal.

[Violeta Hernández]

Order.succ is intended for more general circumstances, and Nat.succ is sort of an implementation detail

[Violeta Hernández]

rzeta0 said:

unknown tactic?

You must have forgotten to write down the exact or apply tactic

[rzeta0]

Here is my code thus far.

I'm trying to create a hypothesis hb2 ; >= 3 from hb : a > 2 using add_one_le_of_lt but it is giving an unknown tactic error.

example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by
  obtain ⟨a, h2⟩ := h
  have h3 := le_or_gt a 2
  obtain ha | hb := h3
  · have g1 :=
      calc
        m = 2 * a := by rw [h2]
        _ ≤ 2 * 2 := by rel [ha]
        _ < 5 := by numbers
    apply ne_of_lt
    apply g1
  · have hb2 : a ≥ 3 := by add_one_le_of_lt -- -- < ERROR unknown tactic
    have g2 :=
      calc
        m = 2 * a := by rw [h2]
        _ ≥ 2 * 3 := by rel [hb2]
       _ > 5 := by numbers
    apply g2

numbers is like norm_num

[Ruben Van de Velde]

It appears to be the case that you are missing imports

[Ruben Van de Velde]

And Violeta's answer is correct

[Daniel Weber]

You can use have hb2 : a ≥ 3 := Int.add_one_le_of_lt hb

[rzeta0]

Ruben Van de Velde said:

It appears to be the case that you are missing imports

adding a import Mathlib.Init.Data.Nat.Basic or a import Mathlib.Init.Data.Int.Basic to the existing boilerplate imports doesn't seem to solve it.

I've also changed the code to hb2 : a ≥ 3 := Int.add_one_le_of_lt hb, adding the hb at the end.

[rzeta0]

Here is my code again in plain vanilla lean and not the Heather Macbeth special environment with custom and disabled tactics:

import Mathlib.Tactic -- <-- so far has imported everything I needed

example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by
  obtain ⟨a, h2⟩ := h
  have h3 := le_or_gt a 2
  obtain ha | hb := h3
  · have g1 :=
      calc
        m = 2 * a := by rw [h2]
        _ ≤ 2 * 2 := by rel [ha]
        _ < 5 := by norm_num
    apply ne_of_lt
    apply g1
  · have hb2 : a ≥ 3 := by add_one_le_of_lt hb -- <-- unknown tactic error, same with Int.add_one_le_of_lt
    have g2 :=
      calc
        m = 2 * a := by rw [h2]
        _ ≥ 2 * 3 := by rel [hb2]
       _ > 5 := by norm_num
    apply g2

[Derek Rhodes]

rzeta0 said:

I think MacBeth's course environment might be lean3? such a shame as this looks ideal.

Hi, I hope I'm not intruding, and as a side note, "The Mechanics of Proof" does use Lean4, however there are some tactics that are programmatically excluded to ensure people learn how to use the less powerful ones.

[Derek Rhodes]

oh, nevermind! didn't see the new post.

[rzeta0]

Derek - thanks for the info on Mechanics of Proof.

Launching the code in the online web "live.lean" environment also shows the unknown tactic error.

[Derek Rhodes]

@rzeta0, I just tried out your code on my machine, and found that using apply worked:

have hb2 : a ≥ 3 := by apply Int.add_one_le_of_lt hb

[Derek Rhodes]

add_one_le_of_lt is a theorem, which, if is an equality or an iff, then they can also be rw rewritten, but not used as a tactic, that is by itself in tactic mode.

another way to do it is with term mode like:
have hb2 : a ≥ 3 := Int.add_one_le_of_lt hb

[rzeta0]

Thanks Derek - the use of apply worked. I am a beginner so still learning the syntax but I think I do understand the different between applying a lemma and justifying via a tactic .. i think.

Can I ask why the code doesn't work if I leave out the Int at the beggining of Int.add_one_le_of_lt ?

[rzeta0]

Overall I think Macbeth has a simpler solution in mind as my resulting code seems far too big for this early chapter in her course. Am I missing a mathematical idea?

[Derek Rhodes]

import Std.Data.Int.Basic (edited) will bring the identifiers contained in the Int package into scope. For some reason Int itself is in scope, not sure why.

As for apply, at first it seemed backwards to me because I was used to apply from lisp. Here are two contrived examples, the first is how apply seems to consume the last term of a chain of applications. The second example shows how hypothesis can be applied like functions the way programmers are used to seeing it:

example (a b c : ℕ) (ha: a = 1) (hb: b = 2) (hc: b < c): a < c := by
    have h : a < b → a < c := by sorry

    -- goal ⊢ a < c
    apply h   -- (works backwards through the implication)
    -- goal ⊢ a < b
    addarith [ha, hb]


example (a b c : ℕ) (ha: a = 1) (hb: b = 2) (hc: b < c): a < c := by
    have h : a < b → a < c := by sorry

    have h2 : a < b := by addarith [ha, hb]
    -- (how programmers usually think about function application)
    have h3 := h h2  -- <====
    --
    exact h3

[Derek Rhodes]

oops, I should have said that it is necessary to open Int before using add_one_le_of_lt hb without the Int. prefix

and that the import should be import Std.Data.Int.Basic instead.

[Kyle Miller]

@Derek Rhodes "Apply" is as in "by applying theorem foo, we see it suffices to show..." in a written proof.

apply h is more-or-less the same as refine h ?_ ?_ ... ?_ with the correct number of ?_s. It's applying the theorem in the function application sense too, just with as-yet-unknown arguments.

[Derek Rhodes]

Thanks for the insight Kyle, now I have a reason to take a deeper look into refine.

[Kyle Miller]

refine is exact except it allows placeholders that create new goals.

[Derek Rhodes]

ok cool, good to know

[Mario Carneiro]

I'm pretty sure that @Heather Macbeth prefers to use more tactic-based proofs, so probably the proof here is linarith or addarith or similar, rather than referring explicitly to the lemma Int.add_one_le_of_lt by name

[rzeta0]

Mario Carneiro said:

I'm pretty sure that Heather Macbeth prefers to use more tactic-based proofs, so probably the proof here is linarith or addarith or similar, rather than referring explicitly to the lemma Int.add_one_le_of_lt by name

I'd welcome ideas here. I spent quite a few hours trying to find a maths proof that was translatable into the small set of tactics we've covered but I couldn't see it.

[Heather Macbeth]

I think Example 2.3.2 has the lemma you want:

have h3 := le_or_succ_le a 2

produces

h3 : a ≤ 2 ∨ 3 ≤ a

[rzeta0]

Thanks Heather Macbeth - I'll give that a go.

I'm working my way through the course doing every single exercise - doing the last two from the Existence chapter now.

Thank you for creating this course. :smiley:

[rzeta0]

yep - that works beautifully:

example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by
  obtain ⟨a, h2⟩ := h
  -- have h3 := le_or_gt a 2
  have h3 := le_or_succ_le a 2
  obtain ha | hb := h3
  · have g1 :=
      calc
        m = 2 * a := by rw [h2]
        _ ≤ 2 * 2 := by rel [ha]
        _ < 5 := by numbers
    apply ne_of_lt
    apply g1
  · have g2 :=
      calc
        m = 2 * a := by rw [h2]
        _ ≥ 2 * 3 := by rel [hb]
        _ > 5 := by numbers
    apply ne_of_gt
    apply g2