more inductions for int

Stream: Is there code for X?

[Joachim Breitner]

I (think I) currently need the int-equivalents of nat.le_induction and nat.decreasing_induction. I’d add them unless someone tells me that my abilities to search for existing lemmas have proven insufficient.

[Joachim Breitner]

I guess they are just specializations of https://leanprover-community.github.io/mathlib_docs/data/int/basic.html#int.induction_on%27

[Eric Wieser]

Ouch, that has nasty equation lemmas

[Patrick Johnson]

Both lemmas follow directly from int.induction_on'

import tactic

lemma int.le_induction {P : ℤ → Sort*} {m n}
  (h₁ : P m) (h₂ : ∀ n, m ≤ n → P n → P (n + 1)) :
  m ≤ n → P n :=
begin
  revert P, apply int.induction_on' n m,
  { exact λ _ h _ _, h },
  { exact λ _ h₁ ih P h₂ h₃ _, h₃ _ h₁ (ih h₂ h₃ h₁) },
  { rintro k h₁ ih P h₂ h₃ h₄, have h₅ := h₁.trans h₄, exfalso, contrapose! h₅, apply sub_one_lt },
end

lemma int.decreasing_induction {P : ℤ → Sort*} {m n : ℤ}
  (h₁ : ∀ n, P (n + 1) → P n) (h₂ : m ≤ n) (h₃ : P n) : P m :=
begin
  revert P h₂, apply int.induction_on' m n,
  { exact λ _ _ _, id },
  { rintro k h₁ ih P h₂ h₃ h₄, have h₅ := h₂.trans h₁, exfalso, contrapose! h₅, apply lt_add_one },
  { rintro k h₁ ih P h₂ h₃ h₄, apply h₃, rw sub_add_cancel, apply ih h₁ h₃ h₄ },
end

I think the bias is against adding new induction principles if they follow from existing ones (see this for example).

[Johan Commelin]

In LTE I recently added

-- src/for_mathlib/triangle_shift.lean L426L433
@[elab_as_eliminator] protected lemma _root_.int.induction_on_iff {p : ℤ → Prop}
  (i : ℤ) (hz : p 0) (h : ∀ i : ℤ, p i ↔ p (i + 1)) : p i :=
begin
  induction i using int.induction_on with i IH i IH,
  { exact hz },
  { rwa ← h },
  { rw h, simpa only [sub_add_cancel], }
end

[Kevin Buzzard]

Another thing that's missing is something which is definitionally nat.rec but uses +1 instead of succ. I would like to see this one in mathlib but it definitely follows from something which is already there :-)

[Eric Wieser]

match n with | 0 := _ | (n + 1) := _ end is one way to spell that recursor, but I guess that's annoying

[Michael Stoll]

I have written a "multiplicative induction" principle, since I needed it for my work on the Hilbert symbol:

/-!
### Establish an induction principle for multiplicatively closed properties

If `P : ℕ → Prop` satisfies `P 0`, `P 1`, `P p` for every prime number `p`
and `∀ (m n : ℕ), P m → P n → P (m*n)`, then `P n` holds for all `n : ℕ`.

Similarly for `P : ℤ → Prop`, with `P (-1)` added for good measure.
-/

section multiplicative_induction

/-- The principle of multiplicative induction for natural numbers -/
theorem nat_multiplicative_induction (P : ℕ → Prop) (h0 : P 0) (h1 : P 1) (hp : ∀ (p : ℕ), p.prime → P p)
  (hmult : ∀ (m n : ℕ), P m → P n → P (m*n)) (n : ℕ) : P n :=
begin
  by_cases h : n = 0,
  { -- easy case `n = 0`
    rw h,
    exact h0, },
  -- now `n > 0`; take its factors
  let nf : multiset ℕ := n.factors,
  have nfp : (∀ p ∈ nf, nat.prime p) :=
  by { intro p, simp [nf], exact nat.prime_of_mem_factors, },
  have hp' : (∀ p ∈ nf, P p) := by { intros p hyp, exact hp p (nfp p hyp), },
  have hn : nf.prod = n := by { simp [nf], exact nat.prod_factors h, },
  rw ← hn,
  exact multiset.prod_induction P nf hmult h1 hp',
end

/-- The principle of multiplicative induction for natural numbers -/
theorem int_multiplicative_induction (P : ℤ → Prop) (h0 : P 0) (h1 : P 1) (hn1 : P (-1))
  (hp : ∀ (p : ℕ), p.prime → P p)
  (hmult : ∀ (m n : ℤ), P m → P n → P (m*n)) (n : ℤ) : P n :=
begin
  -- reduce to the case of natural numbers
  let P' : ℕ → Prop := (λ n, P ↑n),
  have hmult' : (∀ (m n : ℕ), P' m → P' n → P' (m*n)) :=
  by { simp [P'], intros m n, exact hmult m n, },
  -- this gives us the statement for `|n|`
  have hP' := nat_multiplicative_induction P' (by assumption_mod_cast) (by assumption_mod_cast)
                (by assumption_mod_cast) hmult' n.nat_abs,
  simp [P'] at hP', -- gives `P ↑n.nat_abs`
  -- split according to sign
  cases int.nat_abs_eq n with hn hn,
  { -- `n = ↑n.nat_abs`
    rw [hn],
    exact hP' },
  { -- `n = -↑n.nat_abs`
    rw hn,
    rw (by ring : -(n.nat_abs : ℤ) = (-1)*↑n.nat_abs),
    exact hmult (-1) ↑n.nat_abs hn1 hP', },
end

end multiplicative_induction

Would it make sense to include that?

[Johan Commelin]

Yes, those look useful to me. Note that the second docstring should say integers instead of natural numbers

[Ruben Van de Velde]

lemma induction_on_primes {P : ℕ → Prop} (h₀ : P 0) (h₁ : P 1)
  (h : ∀ p a : ℕ, p.prime → P a → P (p * a)) (n : ℕ) : P n :=

[Johan Commelin]

Ooh, does that already exist?

[Ruben Van de Velde]

Yup: docs#induction_on_primes which is based on docs#unique_factorization_monoid.induction_on_prime

[Ruben Van de Velde]

Not sure why one is "prime" and the other "primes"

[Michael Stoll]

But note that my main assumption is different (multiplicative closure instead of closure under multiplication by a prime).

[Michael Stoll]

And I really needed the version for integers.

[Ruben Van de Velde]

The nat one is pretty similar:

theorem nat_multiplicative_induction (P : ℕ → Prop) (h0 : P 0) (h1 : P 1) (hp : ∀ (p : ℕ), p.prime → P p)
  (hmult : ∀ (m n : ℕ), P m → P n → P (m*n)) (n : ℕ) : P n :=
induction_on_primes h0 h1 (λ p a pp ha, hmult _ _ (hp _ pp) ha) n

[Michael Stoll]

OK, that simplifies things a bit...

[Damiano Testa]

Michael, one thing that I have learned using mathlib, is that if I can prove a result in n lines, someone in this chat can prove it in 1.

[Yaël Dillies]

... by induction :rofl:

[Damiano Testa]

The library already contains a lot of results and someone will certainly know the exact one that is closest to the one you want and will be able to tell you.

[Michael Stoll]

Yeah, but it would really help to have a way of finding these oneself quickly!

[Michael Stoll]

(deleted)

[Damiano Testa]

This is what this chat is for!

[Yaël Dillies]

And the naming convention!

[Damiano Testa]

With time, you will be able to prove your results in n/2 lines...

[Michael Stoll]

I find that what is holding me up the most is
(1) getting Lean to prove the obvious
(2) figuring out where to find what I need in mathlib

[Michael Stoll]

Is there work under way addressing these issues?

[Michael Stoll]

Regarding (1), I would imagine some amount of (most likely AI-supported) heuristic proof search that goes more than one level deep.

[Damiano Testa]

When I was even more of a beginner than now, I found tidy very useful.

[Ruben Van de Velde]

int is perhaps worth adding, though:

theorem int_multiplicative_induction (P : ℤ → Prop) (h0 : P 0) (h1 : P 1) (hn1 : P (-1))
  (hp : ∀ (p : ℕ), p.prime → P p)
  (hmult : ∀ (m n : ℤ), P m → P n → P (m*n)) (n : ℤ) : P n :=
begin
  have hp' : ∀ p : ℤ, prime p → P p,
  { intros p pp,
    have : P p.nat_abs := hp _ (int.prime_iff_nat_abs_prime.mp pp),
    obtain hp'|hp' := int.nat_abs_eq p; rw hp',
    { exact this },
    { rw ←neg_one_mul,
      apply hmult _ _ hn1 this } },
  exact unique_factorization_monoid.induction_on_prime n h0
    (λ x hx, (int.is_unit_eq_one_or hx).elim (λ h, h.symm ▸ h1) (λ h, h.symm ▸ hn1))
    (λ a p haz pp hpa, hmult _ _ (hp' _ pp) hpa),
/- Or more painful:
  induction h : n.nat_abs using nat_multiplicative_induction with k ih generalizing n,
  { rwa int.eq_zero_of_nat_abs_eq_zero h, },
  { simp only [int.nat_abs_eq_iff, int.coe_nat_zero, int.coe_nat_succ, zero_add] at h,
    obtain rfl|rfl := h; assumption },
  { exact hp' n (int.prime_iff_nat_abs_prime.mpr (h.symm ▸ ih)), },
  { rw ←int.sign_mul_nat_abs n_1,
    apply hmult,
    { obtain hs|rfl|hs := lt_trichotomy 0 n_1,
      { rwa int.sign_eq_one_of_pos hs, },
      { rwa int.sign_zero },
      { rwa int.sign_eq_neg_one_of_neg hs } },
    { rw [h, int.coe_nat_mul],
      apply hmult,
      apply ᾰ,
      apply int.nat_abs_of_nat,
      apply ᾰ_1,
      apply int.nat_abs_of_nat } },
-/
end

[Heather Macbeth]

Michael Stoll said:

(2) figuring out where to find what I need in mathlib

Maybe it's Stockholm system, but all of us, even the "experts", have got very used to this human-based library search. It's so fast (and sociable) that it becomes less urgent to find automated alternatives.

[Michael Stoll]

I frequently try suggest, but I find it rarely to be helpful. Sometimes it comes up with exact ...and then I'm happy, but mostly I get a long list of useless stuff. E.g., when the goal is an equality, you get a list of results that can in principle prove an equality, but which are completely unrelated to the shape of the terms involved. (This could be related to the fact(?) that suggest sorts the results by length of lemma name, which tends to put unspecific ones first. Perhaps this could be changed so that the most specific ones appear on top?)

[Yaël Dillies]

There is suggest ... using ... which filters out the results to the ones that use the hypotheses you give in the second ...

[Eric Wieser]

Often I find that using Zulip is faster than waiting for library_search on my machine

[Michael Stoll]

@Ruben Van de Velde My proof was not that much longer (minus the comment lines) :smile:

[Yaël Dillies]

Nobody can know the full library, but you sure can know your own little folder by heart.

[Michael Stoll]

I find myself not remembering the names of lemmas that I used yesterday. Maybe this is just old age approaching...

[Yaël Dillies]

I can recite you everything that's under order., combinatorics., analysis.convex.. I have no idea what's under measure_theory. however.

[Yaël Dillies]

The idea is that you can then know about any bit of the library by asking the right person.

[Eric Rodriguez]

There's docs#nat.rec_on_prime_pow too, created as I was unaware (until today!) of the induction that Ruben mentioned

[Eric Rodriguez]

(there's some other spellings below that, too, which are helpful)

[Yaël Dillies]

I started a list of all ℕ recursors in the module docstring of file#data/nat/basic to avoid this precise situation. Please add yours!

[Eric Rodriguez]

Surely we should only put the ones in that file there? I'm happy to plop them there regardless :shrug:🏻‍♀️

[Ruben Van de Velde]

Michael Stoll said:

Ruben Van de Velde My proof was not that much longer (minus the comment lines) :smile:

Yeah, it wasn't as easy to derive from the general result as I'd hoped; it didn't really like the ∀ (p : ℕ), nat.prime p → P ↑p formulation. If that formulation is more useful for you, it's probably different enough to add to mathlib

[Yaël Dillies]

At the time I could only those in the file, but if there more just create a section gathering them all

[Damiano Testa]

Michael, in case it is helpful, I have used your proof of nat_multiplicative_induction and simply rewrote it in a more Lean-friendly way. I always find looking at the diffs in these proofs useful. Note, in particular, that I hold my breath and do not tell Lean on what to apply the lemmas, but wait for Lean to let me know what it wants. All the have and let have disappeared (and of course their content reappears when Lean wants it).

theorem nat_multiplicative_induction (P : ℕ → Prop) (h0 : P 0) (h1 : P 1) (hp : ∀ (p : ℕ), p.prime → P p)
  (hmult : ∀ (m n : ℕ), P m → P n → P (m*n)) (n : ℕ) : P n :=
begin
  cases n,
  { -- easy case `n = 0`
    assumption },
  -- now `n > 0`; take its factors
  convert multiset.prod_induction P n.succ.factors hmult h1 _,
  { simpa only [multiset.coe_prod] using (nat.prod_factors (n.succ_ne_zero)).symm },
  { exact λ p hyp, hp p (nat.prime_of_mem_factors hyp) }
end

[Michael Stoll]

BTW, I just found docs#nat.rec_on_mul .

[Michael Stoll]

@Damiano Testa I guess it's a question whether one should try to write in a "Lean-friendly" or a "human-friendly" way. While developing a proof, I guess the latter makes more sense. For the former, you need experience to know what Lean prefers. Is there any documentation on this?

[Damiano Testa]

My approach is that if the statement has a proof that is "obvious", then I go for the quickest available proof that I can find. If the statement has some content, then I prefer a more discursive proof (better even if with comments, like you did).

[Damiano Testa]

I would categorize these induction statements as "obvious": once you know what to prove, you simply do it.

[Michael Stoll]

A search for "int.rec_on" doesn't seem to produce anything, though.

[Kevin Buzzard]

There's int.induction_on