int.induction_on

Stream: general

[Kenny Lau]

Why isn't int.induction_on tagged with eliminator?

[Mario Carneiro]

it is now

[Kenny Lau]

lol

[Abhimanyu Pallavi Sudhir]

I found this a while back and forgot to bring it up: int.induction_on (in data.int.basic) has overtly restrictive hypotheses -- it says
∀ {p : ℤ → Prop} (i : ℤ), p 0 → (∀ i, p i → p (i + 1)) → (∀ i, p i → p (i - 1)) → p i while
∀ {p : ℤ → Sort} (i : ℤ), p 0 → (∀ i ≥ 0, p i → p (i + 1)) → (∀ i ≤ 0, p i → p (i - 1)) → p i is sufficient, which can be proven quite easily:

namespace int

theorem induction_on' {P : ℤ → Sort} (z : ℤ)
: P 0 → (∀ k ≥ 0, P k → P (k + 1)) → (∀ k ≤ 0, P k → P (k - 1)) → P z :=
λ H0 Hs Hp, int.rec_on z
  (λ n, nat.rec_on n H0 (λ m ih, Hs m (of_nat_ge_zero _) ih))
  (λ n, nat.rec_on n
    (by rw [neg_succ_of_nat_coe', int.coe_nat_zero, neg_zero];
      exact Hp 0 (le_refl _) H0)
    (λ m ih, by rw [neg_succ_of_nat_coe']; rw [neg_succ_of_nat_coe] at ih;
      exact Hp _ (neg_nonpos_of_nonneg $ of_nat_ge_zero _) ih))

end int

I guess I should PR this, but there are probably a hundred places where the old theorem is used. Should I make this induction_on' a separate theorem and prove the existing induction_on as a special case?

[Johan Commelin]

I've wished for your version a couple times

[Johan Commelin]

Never got round to PRing it

[Mario Carneiro]

BTW Sort is the same as Prop. I think you mean Sort*

[Mario Carneiro]

I very much doubt the old version is used in a hundred places. Probably 2 or 3

[Johan Commelin]

There is also the version where you assume \for i, i > 0 → (p i → p -i)

[Johan Commelin]

Hmm, that isn't the optimal form, I guess

[Abhimanyu Pallavi Sudhir]

By the way, should I use Pi's instead of foralls? I.e.

namespace int

def bidir_rec_on {C : ℤ → Sort*} (z : ℤ) :
  C 0 → (Π (k : ℤ) (hn : k ≥ 0), C k → C (k + 1)) → (Π (k : ℤ) (hn : k ≤ 0), C k → C (k - 1)) → C z :=
λ H0 Hs Hp, int.rec_on z
  (λ n, nat.rec_on n H0 (λ m ih, Hs m (of_nat_ge_zero _) ih))
  (λ n, nat.rec_on n
    (by rw [neg_succ_of_nat_coe', int.coe_nat_zero, neg_zero];
      exact Hp 0 (le_refl _) H0)
    (λ m ih, by rw [neg_succ_of_nat_coe']; rw [neg_succ_of_nat_coe] at ih;
      exact Hp _ (neg_nonpos_of_nonneg $ of_nat_ge_zero _) ih))

end int

Because this works:

def test : ℤ → ℤ :=
λ z, bidir_rec_on z 1 (λ k hk fk, (2 * fk : ℤ)) (λ k hk fk, 2 * fk)

But this:

def test : ℤ → ℤ :=
λ z, induction_on' z 1 (λ k hk fk, (2 * fk : ℤ)) (λ k hk fk, 2 * fk)

Gives
failed to generate bytecode for 'test' code generation failed, VM does not have code for 'int.induction_on''

[Chris Hughes]

Is that because of using Sort instead of Sort*?

[Abhimanyu Pallavi Sudhir]

No, I've changed both to Sort*

[Mario Carneiro]

did you use def instead of theorem?

[Abhimanyu Pallavi Sudhir]

Ah yes.

[Mario Carneiro]

pi vs forall is purely cosmetic

[Abhimanyu Pallavi Sudhir]

So I guess this should always be a def?

[Abhimanyu Pallavi Sudhir]

(so it can generate both proofs and functions)

[Mario Carneiro]

the result lives in Sort*, so it could be data

[Abhimanyu Pallavi Sudhir]

?? But making it a theorem has the bytecode generation error. Even with Sort*.

[Abhimanyu Pallavi Sudhir]

You can run reduce on it, but not eval.

[Kevin Buzzard]

Lean does not keep the bytecode for theorems.

[Abhimanyu Pallavi Sudhir]

(deleted)

[Sebastien Gouezel]

In your induction', zero could be replaced by any number.

theorem induction_on' {P : ℤ → Sort} {w : ℤ} (z : ℤ)
: P w → (∀ k ≥ w, P k → P (k + 1)) → (∀ k ≤ w, P k → P (k - 1)) → P z := ...

[Abhimanyu Pallavi Sudhir]

Yep,

def bidir_rec_on' {C : ℤ → Sort*} (z : ℤ) (b : ℤ) :
  C b → (∀ k ≥ b, C k → C (k + 1)) → (∀ k ≤ b, C k → C (k - 1)) → C z :=
λ H0 Hs Hp,
begin
  rw ←sub_add_cancel z b,
  induction (z - b),
  { induction a with n ih, { rwa [of_nat_zero, zero_add] },
    rw [of_nat_succ, add_assoc, add_comm 1 b, ←add_assoc],
    exact Hs _ (le_add_of_nonneg_left (of_nat_nonneg _)) ih },
  { induction a with n ih,
    { rw [neg_succ_of_nat_eq, ←of_nat_eq_coe, of_nat_zero, zero_add, neg_add_eq_sub],
      exact Hp _ (le_refl _) H0 },
    { rw [neg_succ_of_nat_coe', nat.succ_eq_add_one, ←neg_succ_of_nat_coe, sub_add_eq_add_sub],
      exact Hp _ (le_of_lt (add_lt_of_neg_of_le (neg_succ_lt_zero _) (le_refl _))) ih } }
end