2 step induction 5

Stream: new members

[Răzvan Flavius Panda]

Trying to prove: https://github.com/hrmacbeth/math2001/blob/e660f42b13ddcb6d12b52ba036d6bd071a0cfb9b/Math2001/06_Induction/03_Two_Step_Induction.lean#L175

Got as far as:

example (m : ℕ) : s m ≡ 2 [ZMOD 5] ∨ s m ≡ 3 [ZMOD 5] := by
  two_step_induction m with k ih1 ih2
  · left
    rw [s]
    numbers
  · right
    rw [s]
    numbers
  · obtain ih1 | ih1 := ih1
    · obtain ih2 | ih2 := ih2
      · calc
          s (k + 1 + 1)
            = 2 * s (k + 1) + 3 * s k := by rw [s]
          _ ≡ 2 * 2 + 3 * 2 [ZMOD 5] := by rel [ih1, ih2]
      · sorry
    · sorry

The issue is that what I got now in calc is 0 [ZMOD 5] but the goal is to prove 3 [ZMOD 5].

[Răzvan Flavius Panda]

Am I doing something silly here or how did I end up in a situation impossible to prove the goal?

[Aaron Liu]

your induction hypothesis is not strong enough

[Aaron Liu]

what you actually want to prove is "forall n : ℕ, if n is even then s n ≡ 2 [ZMOD 5] and if n is odd then s n ≡ 3 [ZMOD 5]"

[Aaron Liu]

then use this to prove your main goal

[Răzvan Flavius Panda]

does not strong enough mean, insufficient to prove the goals?

[Răzvan Flavius Panda]

Aaron Liu said:

what you actually want to prove is "forall n : ℕ, if n is even then s n ≡ 2 [ZMOD 5] and if n is odd then s n ≡ 3 [ZMOD 5]"

How did you end up with this observation?
I mean I can see it's a pattern by eval-ing things but I can't guarantee it would go on forever.

[Aaron Liu]

you see a pattern and then you guess it will go on forever

[Aaron Liu]

then you try proving it in Lean and if it doesn't work you then diagnose the issue and try again

[Aaron Liu]

or well that's what I do

[Aaron Liu]

you should state you induction goal like ∀ n, s (2 * n) ≡ 2 [ZMOD 5] ∧ s (2 * n + 1) ≡ 3 [ZMOD 5]

[Aaron Liu]

then use something like docs#Nat.even_or_odd' to case on even or odd

[Răzvan Flavius Panda]

Was what I tried an unavoidable step on the path of realizing the induction is not strong enough or was there an easier way?

[Aaron Liu]

there is an easier way

[Aaron Liu]

do the whole thing in your head and realize the problem before putting it into Lean

[Aaron Liu]

that's what I did

[Răzvan Flavius Panda]

unfortunately my brain does not come yet with a LEAN compiler

[Răzvan Flavius Panda]

I'll see what I can do about that

[Răzvan Flavius Panda]

Shouldn't this conv => ring work?

      · calc
          s (2 * n)
            = s (2 * n - 2 + 2) := by conv => ring

[Aaron Liu]

what are you expecting conv => ring to do?

[Aaron Liu]

by the way Nat isn't a ring

[Aaron Liu]

subtraction truncates at zero so 1 - 2 = 0

[Răzvan Flavius Panda]

oh

[Aaron Liu]

this means 1 - 2 + 2 = 2

[Aaron Liu]

find a better way

[Aaron Liu]

you shouldn't have to introduce Nat subtraction

[Răzvan Flavius Panda]

My issue is that to expand this into definition: s (2 * n) I need it to be in the form s (something + 2)
The only way I knew to do that was by using -2 + 2.

[Aaron Liu]

no you should induction n

[Aaron Liu]

since n could be zero

[Răzvan Flavius Panda]

Making progress but I got stuck on how to obtain from hypothesis:

**ih** : Int.Even ↑k → s (2 * k) ≡ 2 [ZMOD 5] ∧ s (2 * k + 1) ≡ 3 [ZMOD 5]

[Aaron Liu]

where'd Int.Even k come from?

[Aaron Liu]

drop that

[Răzvan Flavius Panda]

This is what I got:

example (m : ℕ) : s m ≡ 2 [ZMOD 5] ∨ s m ≡ 3 [ZMOD 5] := by
  have h1 : ∀ n, s (2 * n) ≡ 2 [ZMOD 5] ∧ s (2 * n + 1) ≡ 3 [ZMOD 5] := by
    intro n
    obtain h1 | h2 := Int.even_or_odd n
    simple_induction n with k ih
    · constructor
      · calc
          s (2 * 0)
            = 2 := by rw [s]
          _ ≡ 2 [ZMOD 5] := by extra
      · calc
          s (2 * 0 + 1)
            = 3 := by rw [s]
          _ ≡ 3 [ZMOD 5] := by extra
    · sorry

[Aaron Liu]

remove the obtain

[Aaron Liu]

put it after the have

[Răzvan Flavius Panda]

n doesn't exist if I put it before the intro n

[Aaron Liu]

yeah case on m instead

[Răzvan Flavius Panda]

Is this what you mean:

example (m : ℕ) : s m ≡ 2 [ZMOD 5] ∨ s m ≡ 3 [ZMOD 5] := by
  have h1 : ∀ n, s (2 * n) ≡ 2 [ZMOD 5] ∧ s (2 * n + 1) ≡ 3 [ZMOD 5] := by
    obtain h1 | h2 := Int.even_or_odd m
    simple_induction m with k ih

?

[Aaron Liu]

no

[Aaron Liu]

example (m : ℕ) : s m ≡ 2 [ZMOD 5] ∨ s m ≡ 3 [ZMOD 5] := by
  have h1 : ∀ n, s (2 * n) ≡ 2 [ZMOD 5] ∧ s (2 * n + 1) ≡ 3 [ZMOD 5] := by
    intro n
    simple_induction n with k ih
    -- put an amazing proof here
    all_goals sorry
  obtain h2 | h3 := Int.even_or_odd m
  -- continue an amazing proof here
  all_goals sorry

[Aaron Liu]

oh I got it wrong (edited)

[Răzvan Flavius Panda]

Do you see what I am doing wrong here?

example (m : ℕ) : s m ≡ 2 [ZMOD 5] ∨ s m ≡ 3 [ZMOD 5] := by
  have h1 : ∀ n, s (2 * n) ≡ 2 [ZMOD 5] ∧ s (2 * n + 1) ≡ 3 [ZMOD 5] := by
    intro n
    simple_induction n with k ih
    · constructor
      · calc
          s (2 * 0)
            = 2 := by rw [s]
          _ ≡ 2 [ZMOD 5] := by extra
      · calc
          s (2 * 0 + 1)
            = 3 := by rw [s]
          _ ≡ 3 [ZMOD 5] := by extra
    · obtain ⟨ih1, ih2⟩ := ih
      · constructor
        · calc
            s (2 * (k + 1))
              ≡ 2 [ZMOD 5] := by rel [ih1]
        · calc

unexpected token 'calc'; expected ':='

m k : ℕ
ih1 : s (2 * k) ≡ 2 [ZMOD 5]
ih2 : s (2 * k + 1) ≡ 3 [ZMOD 5]
⊢ s (2 * (k + 1)) ≡ 2 [ZMOD 5]

[Răzvan Flavius Panda]

It looks like the previous calc block goal did not close but it looks like should have.

[Ruben Van de Velde]

You should assume that calc with just a single step doesn't work

[Răzvan Flavius Panda]

Is that guaranteed or just unlikely?

[Răzvan Flavius Panda]

My issue is that LEAN does not complain, there is no red squigle for that subgoal.

[Aaron Liu]

it parses weird

[Răzvan Flavius Panda]

I am not even sure how **ih1** : s (2 * k) ≡ 2 [ZMOD 5] managed to apply since it does not look exactly like it could apply.

[Aaron Liu]

I have a way to fix the one line calc

[Aaron Liu]

but I haven't completed it yet

[Răzvan Flavius Panda]

So 1 line calc's can work, I see.

[Aaron Liu]

for now you should just avoid one line calcs

[Răzvan Flavius Panda]

Well, this doesn't work:

        · calc
            s (2 * (k + 1))
            _ = s (2 * (k + 1)) := by rfl
              ≡ 2 [ZMOD 5] := by rel [ih1]

How am I supposed to make it multi-line?

[Răzvan Flavius Panda]

Oh, I placed _ in the wrong place.

[Răzvan Flavius Panda]

And now I get a squiggle on rel so it does not work.

[Răzvan Flavius Panda]

I don't know what to do.rel [ih1] clearly can't rewrite s (2 * (k + 1)) as it would be s (2 * k) even though they are both even arguments and the reply would be in both cases 2 [ZMOD 5]

[Aaron Liu]

well you need to rewrite 2 * (k + 1) into 2 * k + 1 + 1

[Aaron Liu]

these are actually definitionally equal

[Răzvan Flavius Panda]

How would that help, I still need to rel on s (2 * k) or s (2 * k + 1) and it wouldn't match.

[Răzvan Flavius Panda]

Also I tried to rewrite inside s argument using conv => ring and that didn't work. So no idea how to rewrite arguments.

[Aaron Liu]

well once you have s (2 * k + 1 + 1) you can start unfolding the definition of s

[Răzvan Flavius Panda]

Ok, I see, but how do I rewrite inside the s argument? conv => ring doesn't work

[Aaron Liu]

do you know how conv mode works?

[Aaron Liu]

you need to enter the argument you want

[Răzvan Flavius Panda]

No, it was never explained. From what I seen it allows to apply tactics inside other expressions.

[Răzvan Flavius Panda]

Aaron Liu said:

you need to enter the argument you want

How does that look like?

[Aaron Liu]

example {x y : Nat} (h : x = x * y + y) :
    x + x + y + x * (x * y + y) = x + x + y + x * ((x * y + y) * y + y) := by
  conv =>
    enter [1, 2, 2, 1, 1]
    rw [h]

[Aaron Liu]

put your cursor on the numbers and step through the enter command

[Răzvan Flavius Panda]

Well, I understand how your example works. :sweat_smile:

[Răzvan Flavius Panda]

I want something lke this but it's not working:

        · calc
            s (2 * (k + 1))
              = s (2 * k + 2) := by conv =>
                                      enter [2]
                                      ring

[Răzvan Flavius Panda]

I seem to have broken the entire proof, getting squiggles everywhere or tactics in white:

image.png

[Aaron Liu]

that's because you have a one-line calc

[Aaron Liu]

you should fix that first

[Răzvan Flavius Panda]

Ok, so:

        · calc
            s (2 * (k + 1))
              = s (2 * k + 2) := by conv =>
                                      enter [2]
                                      ring
            _ = 2 * s (2 * k + 1) + 3 * s (2 * k) := by rw [s]

The conv is not working as I was hoping it would.

[Răzvan Flavius Panda]

Wanted to focus on the argument and apply ring on it.

[Răzvan Flavius Panda]

Hovering over the 2 in the enter does not focus on anything.

[Aaron Liu]

I think it should focus on the right side of the equality (whereas before it was focusing on the entire equality)

[Aaron Liu]

you can also just have h : 2 * (k + 1) = 2 * k + 2 := rfl and then rewrite using h

[Răzvan Flavius Panda]

I'll take anything that works!

[Răzvan Flavius Panda]

Sub-goal solved.

[Răzvan Flavius Panda]

-- continue an amazing proof here
I like your positivity :smile:

[Răzvan Flavius Panda]

How can I use obtain with:

h1 : ∀ (n : ℕ), s (2 * n) ≡ 2 [ZMOD 5] ∧ s (2 * n + 1) ≡ 3 [ZMOD 5]

the forall prevents me from using: obtain ⟨h11, h12⟩ := h1

[Răzvan Flavius Panda]

This works: obtain ⟨h11, h12⟩ := h1 m

[Răzvan Flavius Panda]

But the goal is problematic:

m : ℕ
h1 : ∀ (n : ℕ), s (2 * n) ≡ 2 [ZMOD 5] ∧ s (2 * n + 1) ≡ 3 [ZMOD 5]
n : ℤ
h2n : ↑m = 2 * n
h11 : s (2 * m) ≡ 2 [ZMOD 5]
h12 : s (2 * m + 1) ≡ 3 [ZMOD 5]
⊢ s m ≡ 2 [ZMOD 5] ∨ s m ≡ 3 [ZMOD 5]

[Răzvan Flavius Panda]

Was hoping to rw h2n at goal.

[Aaron Liu]

you want to show that there exists a n' : ℕ such that n = ↑n' and then obtain with h1 n'

[Răzvan Flavius Panda]

And then exact of h11 or h12 would have closed the goal but if they used n instead of m

[Răzvan Flavius Panda]

I don't know how to prove that. Not even sure what up arrow n means. Is that casting?

Gemini came up with:

theorem exists_nat_for_nonneg_int_term (n : ℤ) (h : 0 ≤ n) : ∃ n' : ℕ, n = ↑n' :=
  -- The witness is `Int.toNat n`
  -- The proof of the property is `(Int.coe_toNat_of_nonneg h).symm`
  ⟨Int.toNat n, (Int.coe_toNat_of_nonneg h).symm⟩

But Int.coe_toNat_of_nonneg is hallucinated.

[Aaron Liu]

@loogle "nonneg", Int.toNat, Nat.cast

[loogle]

:search: Int.toNat_of_nonneg, Int.emod_natAbs_of_nonneg

[Răzvan Flavius Panda]

Had a look, I don't see the up arrow explained.

[Răzvan Flavius Panda]

Oh, I see, it's type coercion. It's like upcasting.

[Răzvan Flavius Panda]

Is this the signature of what you wanted me to prove?

theorem exists_nat_for_nonneg_int_term (n : ℤ) (h : 0 ≤ n) : ∃ n' : ℕ, n = ↑n'

[Răzvan Flavius Panda]