proof about recursion with timeout

Stream: general

[Aaron Bies]

Here is a statement that feels totally obvious to me, but I have absolutely no idea how to prove it formally.

Does anyone know how to approach this proof?

def collatz (n : ℕ) : ℕ :=
  if n % 2 = 0 then n / 2 else 3 * n + 1

def collatz_terms_in : ℕ → ℕ → Prop
  | 1 _ := true
  | _ 0 := false
  | n (t + 1) := collatz_terms_in (collatz n) t

-- "if it terminates in t steps, it also terminates in t' steps, with t' > t"
example (n t t' : ℕ) (h1 : collatz_terms_in n t) (h2 : t < t') :
  collatz_terms_in n t' :=
begin
  sorry
end

[Eric Wieser]

I recommend you try to prove the easier version with succ t / t + 1 first

[Eric Wieser]

I imagine you'd find this easier to prove if you replace collatz_terms_in with an inductive proposition, as then I think you'd get the induction principle you need for free

[Eric Wieser]

That is

inductive collatz_terms_in : ℕ → ℕ → Prop
| one (t) : collatz_terms_in 1 t
| of_collatz {n t} (h : collatz_terms_in (collatz n) t) : collatz_terms_in n (t +  1)

[Patrick Johnson]

Using the original definition:

example {n t t' : ℕ}
  (h₁ : collatz_terms_in n t)
  (h₂ : t < t') :
  collatz_terms_in n t' :=
begin
  replace h₂ := le_of_lt h₂, induction' h₂, { assumption },
  change t ≤ t' at h₂, by_cases h₃ : n = 1, { subst n, triv },
  rw collatz_terms_in, apply ih, clear' t' ih h₂,
  induction t with t ih generalizing n,
  { rw collatz_terms_in at h₁, cases h₁, exact h₃ },
  by_cases h₄ : collatz n = 1, { rw h₄, triv },
  rw collatz_terms_in, apply ih, rw collatz_terms_in at h₁,
  repeat { assumption },
end

[Patrick Johnson]

Using Eric's definition:

example {n t t' : ℕ}
  (h₁ : collatz_terms_in n t)
  (h₂ : t < t') :
  collatz_terms_in n t' :=
begin
  replace h₂ := le_of_lt h₂, induction' h₁, { left },
  cases t', { cases h₂ },
  rw nat.succ_le_succ_iff at h₂, right, exact ih h₂,
end

[Aaron Bies]

Thank you, I will try to understand how this works

[Aaron Bies]

What do I have to import for it to find induction'?

[Patrick Johnson]

import tactic.induction

[Kyle Miller]

The theorem is a bit more general if you switch the less-than to a less-than-or-equal.

Here's Patrick's second proof with that change and in more of a mathlib style.

example {n t t' : ℕ}
  (h₁ : collatz_terms_in n t)
  (h₂ : t ≤ t') :
  collatz_terms_in n t' :=
begin
  induction' h₁,
  { constructor },
  { cases t',
    { cases h₂, },
    { rw nat.succ_le_succ_iff at h₂,
      use ih h₂, } }
end

[Kyle Miller]

Here's a different version of Patrick's first proof, using a slightly different induction strategy and using simp to pass the necessary hypotheses to the definition unfoldings:

example {n t t' : ℕ}
  (h₁ : collatz_terms_in n t)
  (h₂ : t ≤ t') :
  collatz_terms_in n t' :=
begin
  induction t' with t' ih generalizing t n,
  { rw [nonpos_iff_eq_zero] at h₂,
    subst t,
    assumption, },
  { by_cases h₃ : n = 1,
    { simp [h₃] },
    { cases t,
      { simpa [collatz_terms_in, h₃, not_false_iff] using h₁ },
      { simp only [collatz_terms_in, h₃, not_false_iff] at ⊢ h₁,
        apply ih h₁,
        simpa [nat.succ_le_succ_iff] using h₂, } } }
end

[Patrick Johnson]

docs#computation.run_for may be useful for this sort of definitions.