# Zulip Chat Archive

## Stream: general

### Topic: int.induction_on

#### Kenny Lau (Apr 19 2018 at 11:34):

Why isn't `int.induction_on`

tagged with eliminator?

#### Mario Carneiro (Apr 19 2018 at 11:35):

it is now

#### Kenny Lau (Apr 19 2018 at 11:35):

lol

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 06:19):

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 (Apr 01 2019 at 06:22):

I've wished for your version a couple times

#### Johan Commelin (Apr 01 2019 at 06:22):

Never got round to PRing it

#### Mario Carneiro (Apr 01 2019 at 06:23):

BTW `Sort`

is the same as `Prop`

. I think you mean `Sort*`

#### Mario Carneiro (Apr 01 2019 at 06:23):

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

#### Johan Commelin (Apr 01 2019 at 06:25):

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

#### Johan Commelin (Apr 01 2019 at 06:28):

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

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:20):

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 (Apr 01 2019 at 07:25):

Is that because of using `Sort`

instead of `Sort*`

?

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:26):

No, I've changed both to `Sort*`

#### Mario Carneiro (Apr 01 2019 at 07:26):

did you use `def`

instead of `theorem`

?

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:26):

Ah yes.

#### Mario Carneiro (Apr 01 2019 at 07:26):

pi vs forall is purely cosmetic

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:27):

So I guess this should always be a `def`

?

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:27):

(so it can generate both proofs and functions)

#### Mario Carneiro (Apr 01 2019 at 07:27):

the result lives in `Sort*`

, so it could be data

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:30):

?? But making it a `theorem`

has the bytecode generation error. Even with `Sort*`

.

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:31):

You can run `reduce`

on it, but not `eval`

.

#### Kevin Buzzard (Apr 01 2019 at 07:34):

Lean does not keep the bytecode for theorems.

#### Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:56):

(deleted)

#### Sebastien Gouezel (Apr 01 2019 at 08:35):

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 (Apr 01 2019 at 10:27):

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

Last updated: May 17 2021 at 21:12 UTC