## Stream: general

### Topic: int.induction_on

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

Why isn't int.induction_on tagged with eliminator?

it is now

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?

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.

(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