Zulip Chat Archive

Stream: general

Topic: int.induction_on


view this post on Zulip Kenny Lau (Apr 19 2018 at 11:34):

Why isn't int.induction_on tagged with eliminator?

view this post on Zulip Mario Carneiro (Apr 19 2018 at 11:35):

it is now

view this post on Zulip Kenny Lau (Apr 19 2018 at 11:35):

lol

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 01 2019 at 06:22):

I've wished for your version a couple times

view this post on Zulip Johan Commelin (Apr 01 2019 at 06:22):

Never got round to PRing it

view this post on Zulip Mario Carneiro (Apr 01 2019 at 06:23):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 01 2019 at 06:25):

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

view this post on Zulip Johan Commelin (Apr 01 2019 at 06:28):

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

view this post on Zulip 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''

view this post on Zulip Chris Hughes (Apr 01 2019 at 07:25):

Is that because of using Sort instead of Sort*?

view this post on Zulip Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:26):

No, I've changed both to Sort*

view this post on Zulip Mario Carneiro (Apr 01 2019 at 07:26):

did you use def instead of theorem?

view this post on Zulip Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:26):

Ah yes.

view this post on Zulip Mario Carneiro (Apr 01 2019 at 07:26):

pi vs forall is purely cosmetic

view this post on Zulip Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:27):

So I guess this should always be a def?

view this post on Zulip Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:27):

(so it can generate both proofs and functions)

view this post on Zulip Mario Carneiro (Apr 01 2019 at 07:27):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:30):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:31):

You can run reduce on it, but not eval.

view this post on Zulip Kevin Buzzard (Apr 01 2019 at 07:34):

Lean does not keep the bytecode for theorems.

view this post on Zulip Abhimanyu Pallavi Sudhir (Apr 01 2019 at 07:56):

(deleted)

view this post on Zulip 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 := ...

view this post on Zulip 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