Need help with a recursive function

Stream: general

[Notification Bot]

Aaron Bies has marked this topic as unresolved.

[Aaron Bies]

I'm afraid I'm stuck again,

I tried to prove that shift always returns an odd number unless the input was 0, but I keep getting unexpected occurrence of recursive function and I don't know what it wants me to do.

(I'm sorry this is a lot of code)

my code

import data.int.basic
import tactic

def shift : ℕ → ℕ | n :=
  if h : n > 1 ∧ n % 2 = 0
    then have n / 2 < n :=
      begin
        refine nat.div_lt_self _ _;
        linarith,
      end, shift (n / 2)
    else n

lemma shift_def (n : ℕ) : shift n = if n > 1 ∧ n % 2 = 0 then shift (n / 2) else n :=
by rw shift

lemma shift_base (n : ℕ) : ¬(n > 1 ∧ n % 2 = 0) → shift n = n :=
begin
  intro h,
  rw shift_def,
  rw ite_eq_iff,
  right,
  split,
  { exact h, },
  { refl, }
end

theorem shift_mul_2 (n : ℕ) : shift (2 * n) = shift n :=
begin
  rw shift_def,
  simp,
  intro h1,
  have h2 : n = 0 := by nlinarith,
  rw [h2, shift_def],
  simp,
end

-- Error: unexpected occurrence of recursive function
theorem shift_odd : ∀ (n : ℕ), n = 0 ∨ (shift n) % 2 ≠ 0 | n :=
begin
  by_cases hb : n > 1 ∧ n % 2 = 0,
  {
    cases hb with h1 h2,
    right,

    let k := n / 2,
    have nk : n = 2 * k := begin
      have kd : k = n / 2 := rfl,
      rw kd,
      rw nat.mul_div_cancel',
      rw nat.dvd_iff_mod_eq_zero,
      exact h2,
    end,

    -- aids the proof that recurion is well-founded
    have term : k < n := begin
      refine nat.div_lt_self _ _,
      { nlinarith, },
      { rw [nat.one_lt_bit0_iff], }
    end,

    simp * at *,

    -- recursion happens here
    have rec := shift_odd k,
    rw or_iff_not_imp_left at rec,
    rw shift_mul_2,
    apply rec,

    linarith,
  }, {
    have h := shift_base n hb,
    rw h,
    finish,
  },
end

[Reid Barton]

I suspect finish is using the lemma itself for the same n

[Reid Barton]

There might be similar issues with simp * at *

[Aaron Bies]

Those are good points

[Reid Barton]

I never really understood how to mix the equation compiler and tactic proofs, personally I think it's easier to go about it this way:

theorem shift_odd (n : ℕ) : n = 0 ∨ (shift n) % 2 ≠ 0 :=
begin
  apply nat.strong_induction_on n, intros n rec,
  by_cases hb : n > 1 ∧ n % 2 = 0,
  {
    cases hb with h1 h2,
    right,

    let k := n / 2,
    have nk : n = 2 * k := begin
      have kd : k = n / 2 := rfl,
      rw kd,
      rw nat.mul_div_cancel',
      rw nat.dvd_iff_mod_eq_zero,
      exact h2,
    end,

    -- aids the proof that recurion is well-founded
    have term : k < n := begin
      refine nat.div_lt_self _ _,
      { nlinarith, },
      { rw [nat.one_lt_bit0_iff], }
    end,

    specialize rec k term,

    simp * at *,

    -- recursion happens here
    rw or_iff_not_imp_left at rec,
    rw shift_mul_2,
    apply rec,

    linarith,
  }, {
    have h := shift_base n hb,
    rw h,
    sorry -- obviously follows from hb somehow
  },
end

[Aaron Bies]

oooh I was not aware of nat.strong_induction_on

[Aaron Bies]

Thank you very much!

[Eric Wieser]

induction n using nat.binary_rec might yield a shorter proof, but I haven't tried