Some numerology

Stream: maths

[Patrick Massot]

I have a little riddle for people who like numbers in Lean.

example (p : ℕ) (n : ℤ) (hp : 1 < p) (h : (p : ℚ) ^ -n < p) : (p : ℚ)^-n ≤ 1

[Patrick Massot]

Of course the question is not about the math proof, it's about convincing Lean

[Floris van Doorn]

import data.rat algebra.field_power

example (p : ℕ) (n : ℤ) (hp : 1 < p) (h : (p : ℚ) ^ -n < p) : (p : ℚ)^-n ≤ 1 :=
begin
  have h2p : (1 : ℚ) ≤ p, { exact_mod_cast le_of_lt hp },
  have h3p : (0 : ℚ) < p := lt_of_lt_of_le (by norm_num) h2p,
  have : 0 ≤ n,
  { rw [← not_lt], intro h2,
    have hn : 1 ≤ -n, { rw [le_neg], apply int.le_of_lt_add_one, exact h2 },
    apply not_le.mpr h, convert fpow_le_of_le h2p hn, rw [fpow_one] },
  rw [fpow_neg, div_le_iff (fpow_pos_of_pos h3p _), one_mul],
  apply one_le_fpow_of_nonneg h2p this
end

[Mario Carneiro]

the -n seems unnecessary

[Floris van Doorn]

Using Mario's comment, I golfed it to

example (p : ℕ) (n : ℤ) (hp : 1 < p) (h : (p : ℚ) ^ n < p) : (p : ℚ)^n ≤ 1 :=
begin
  have h2p : (1 : ℚ) ≤ p, { exact_mod_cast le_of_lt hp },
  apply fpow_le_one_of_nonpos h2p, rw [← not_lt], intro h2, rw [← int.add_one_le_iff] at h2,
  apply not_le.mpr h, convert fpow_le_of_le h2p h2, rw [zero_add, fpow_one]
end

[Mario Carneiro]

import data.rat algebra.field_power

example (p : ℕ) (n : ℤ) (hp : 1 ≤ p) (h : (p : ℚ) ^ n < p) : (p : ℚ)^n ≤ 1 :=
begin
  have hp' : 1 ≤ (p : ℚ), {norm_cast, exact hp},
  have : n ≤ 0,
  { refine le_of_not_lt (λ h', not_le_of_lt h _),
    simpa using fpow_le_of_le hp' (int.add_one_le_iff.2 h') },
  { simpa using fpow_le_of_le hp' this }
end

[Mario Carneiro]

the golfy version is

example (p : ℕ) (n : ℤ) (hp : 1 ≤ p) (h : (p : ℚ) ^ n < p) : (p : ℚ)^n ≤ 1 :=
have hp' : 1 ≤ (p : ℚ), by exact_mod_cast hp,
by simpa using fpow_le_of_le hp' (le_of_not_lt $ λ h' : 0 < n, not_le_of_lt h $
  by simpa using fpow_le_of_le hp' (int.add_one_le_iff.2 h'))

[Mario Carneiro]

if I cheat by simplifying the statement some more:

example (p : ℚ) (n : ℤ) (hp : 1 ≤ p) (h : p ^ n < p) : p ^ n ≤ 1 :=
by simpa using fpow_le_of_le hp (le_of_not_lt $ λ h' : 0 < n, not_le_of_lt h $
  by simpa using fpow_le_of_le hp (int.add_one_le_iff.2 h'))

[Patrick Massot]

Thanks Floris and Mario!

[Kevin Buzzard]

Here's one I ran into the other day:

example (a b : ℤ) (hb : b > 0) : a < b → int.to_nat a < int.to_nat b := sorry

Should that be in mathlib? Is it there already?

[Johan Commelin]

int.to_nat is not maths right?

[Kevin Buzzard]

It sends negative things to 0, that's why this is true. This should be called to_nat_strict_mono or something.

[Johan Commelin]

It's far from strict

[Kevin Buzzard]

So yes, it's not maths.

[Johan Commelin]

I tend to prefer nat_abs

[Kevin Buzzard]

I thought strict meant "working with lt not le"

[Johan Commelin]

Also, we now have the lift tactic

[Kevin Buzzard]

nat_abs is the maths one, right?

[Mario Carneiro]

I assume it is int.to_nat_lt_to_nat

[Kevin Buzzard]

I can't find that in mathlib. Johan -- this all started with me trying to prove

def int.Ioo_fin_equiv (a b : ℤ) : set.Ioo a b ≃ fin (int.to_nat $ b - a - 1) :=

The size of {a<x<b} really is to_nat. But I could prove something like

example (a b : ℤ) (h : a < b) : set.Ioo a b ≃ fin (int.nat_abs $ b - a - 1) :=

[Mario Carneiro]

theorem le_to_nat (a : ℤ) : a ≤ to_nat a :=
by rw [to_nat_eq_max]; apply le_max_left

@[simp] theorem to_nat_le {a : ℤ} {n : ℕ} : to_nat a ≤ n ↔ a ≤ n :=
by rw [(coe_nat_le_coe_nat_iff _ _).symm, to_nat_eq_max, max_le_iff];
   exact and_iff_left (coe_zero_le _)

@[simp] theorem lt_to_nat {n : ℕ} {a : ℤ} : n < to_nat a ↔ (n : ℤ) < a :=
le_iff_le_iff_lt_iff_lt.1 to_nat_le

theorem to_nat_le_to_nat {a b : ℤ} (h : a ≤ b) : to_nat a ≤ to_nat b :=
by rw to_nat_le; exact le_trans h (le_to_nat b)

theorem to_nat_lt_to_nat {a b : ℤ} (hb : 0 < b) (h : a < b) : to_nat a < to_nat b :=
by rw lt_to_nat; cases a; [exact h, exact hb]

[Mario Carneiro]

this goes in data.int.basic

[Kevin Buzzard]

I was unsure whether the idea was to develop the theory of to_nat any more, or whether one should use the "superior" nat_abs which is more mathematically appealing in some weird way

[Kevin Buzzard]

Is there some monotonicity tactic which needs to know about to_nat_lt_to_nat ? @Simon Hudon ?

[Mario Carneiro]

I don't know how well mono handles side conditions

[Simon Hudon]

I think mono could help here. What it does is that it tries assumption on the side condition while selecting a lemma. If it fails with assumption it just means that the lemma is more expensive to apply. The lemma with the fewest remaining side condition is selected. If there's only one candidate, you're just going to get a dump of all the side conditions that mono can't handle

[Kevin Buzzard]

def int.Ioo_fin_equiv (a b : ℤ) : set.Ioo a b ≃ fin (int.to_nat $ b - a - 1) :=
{ to_fun := λ s, ⟨int.to_nat (s.val - a - 1), begin
    cases s with s hs,
    show int.to_nat (s - a - 1) < int.to_nat (b - a - 1),
    cases hs with has hsb,
    have h1 : b - a - 1 > 0,
      linarith,
    apply int.to_nat_lt_to_nat _ _ h1,
    convert (sub_lt_sub_iff_right (a + 1)).2 hsb using 1; ring,
  end⟩,
  inv_fun := λ t, ⟨t.val + a + 1, begin
    split,
      apply int.lt_of_add_one_le,
      rw add_assoc,
      apply le_add_of_nonneg_left,
      simp,
    suffices : (t.val : ℤ) < b - a - 1,
      convert add_lt_add_left this (a + 1) using 1; ring,
    have t2 := t.2,
    convert int.coe_nat_lt_coe_nat_of_lt t2,
    rw int.to_nat_eq_max,
    rw max_eq_left,
    apply le_of_lt,
    have h : 0 < int.to_nat (b - a - 1),
      refine lt_of_le_of_lt (by simp) t2,
    rw lt_iff_not_ge',
    intro h2,
    apply lt_irrefl 0,
    convert h,
    replace h2 := (int.to_nat_le _ _).2 h2,
    symmetry, rwa nat.le_zero_iff at h2,
  end⟩,
  left_inv := begin rintro ⟨s, sa, sb⟩,
    suffices : ↑(int.to_nat (s - (a + 1))) + a + 1 = s,
      exact subtype.eq (by simpa using this),
    rw (int.to_nat_of_nonneg _), simp,
    linarith,
  end,
  right_inv := begin
    rintro ⟨s, hs⟩,
    dsimp,
    rw fin.ext_iff,
    dsimp,
    conv in (↑s + a + 1 + -a + -1 : ℤ) begin ring end,
    simp,
  end }

I really hope this can be seriously golfed. I just muddle through with stuff like this; there are a couple of non-terminal simps :-/

[Chris Hughes]

import data.equiv.basic data.int.basic data.set.intervals

def int.Ico_fin_equiv (a b : ℤ) : set.Ico a b ≃ fin (int.to_nat $ b - a) :=
calc set.Ico a b ≃ set.Ico 0 (b - a) :
  ⟨λ x, ⟨x.1 - a, sub_nonneg.2 x.2.1, add_lt_add_right x.2.2 _⟩,
  λ x, ⟨x.1 + a, le_add_of_nonneg_left x.2.1, lt_sub_iff_add_lt.1 x.2.2⟩,
  λ _, by simp, λ _, by simp⟩
 ... ≃ fin (int.to_nat $ b - a) :
  ⟨λ x, ⟨x.1.to_nat, int.coe_nat_lt.1 $
    by rw [int.to_nat_of_nonneg x.2.1, int.to_nat_of_nonneg (le_trans x.2.1 (le_of_lt x.2.2))];
      exact x.2.2⟩,
  λ x, ⟨x.1, int.coe_nat_nonneg _, begin
    have := int.coe_nat_lt.2 x.2,
    rwa [int.to_nat_of_nonneg] at this,
    cases b - a;
    simp only [int.to_nat, int.coe_nat_lt, nat.not_lt_zero, *] at *
  end⟩,
  λ x, by simp [int.to_nat_of_nonneg x.2.1],
  λ x, by simp⟩

def int.Ioo_fin_equiv (a b : ℤ) : set.Ioo a b ≃ fin (int.to_nat $ b - (a + 1)) :=
calc set.Ioo a b ≃ set.Ico (a + 1) b : equiv.set.of_eq (by simp [set.ext_iff, int.add_one_le_iff])
... ≃ _ : int.Ico_fin_equiv _ _

def int.Ioc_fin_equiv (a b : ℤ) : set.Ioc a b ≃ fin (int.to_nat $ b - a) :=
calc set.Ioc a b ≃ set.Ioo a (b + 1) : equiv.set.of_eq (by simp [set.ext_iff, int.lt_add_one_iff])
... ≃ fin (int.to_nat $ (b + 1) - (a + 1)) : int.Ioo_fin_equiv _ _
... ≃ fin (int.to_nat $ b - a) : ⟨fin.cast (by simp), fin.cast (by simp),
  λ _, fin.eq_of_veq rfl, λ _, fin.eq_of_veq rfl⟩

def int.Icc_fin_equiv (a b : ℤ) : set.Icc a b ≃ fin (int.to_nat $ b + 1 - a) :=
calc set.Icc a b ≃ set.Ico a (b + 1) : equiv.set.of_eq (by simp [set.ext_iff, int.lt_add_one_iff])
... ≃ fin (int.to_nat $ b + 1 - a) : int.Ico_fin_equiv _ _

[Patrick Massot]

Kevin, it is now your duty to PR this before it disappear from sight.

[Kevin Buzzard]

I'll have to remember how to PR stuff. I have to Skype interview someone in 30 minutes and I want to clean up the kitchen before that :-/ I'll get my act together after that.

[Kevin Buzzard]

That's very nice Chris. I just chose the equiv I needed, but if you prove the more convenient one first the rest can happen relatively simply.

[Floris van Doorn]

I feel like various steps in Chris's proof need to be separated out in their own lemmas when we PR this to mathlib.

[Kevin Buzzard]

sigh how do you do update-mathlib when you're editing mathlib, again?

[Kevin Buzzard]

I can't find it in the docs :-/

[Kevin Buzzard]

aah got it cache-olean

[Kevin Buzzard]

#1479 is the of_nat lemmas. I haven't done the equiv yet; I can see at least some of what can come off, my issue is simply that I don't know the import hierarchy so I just don't know where these lemmas go.

[Kevin Buzzard]

(3) Does this give anyone else an assertion violation?

import data.set.intervals

def set.Ico_equiv_add (a b n : ℤ) : set.Ico (a + n) (b + n) ≃ set.Ico a b :=
{ to_fun := λ s, ⟨s.1 - n, _⟩,
  inv_fun := λ t, ⟨t.1 + n, _, _⟩,
  left_inv := λ s, by simp,
  right_inv := λ t, by simp }

[added 19th Oct 2019 -- I also seem to need to import data.equiv.basic now but I can still get the assertion violation]

[Kevin Buzzard]

(1) I thought I'd try it myself after I realised what I should be proving.

example (a b : ℤ) : set.Ico a b ≃ fin (int.to_nat $ b - a) :=
{ to_fun := λ s, ⟨int.to_nat (s.val - a),
    int.to_nat_lt_to_nat (sub_pos.2 $ lt_of_le_of_lt s.2.1 s.2.2) $ sub_lt_sub_right s.2.2 _⟩,
  inv_fun := λ t, ⟨(t.val : ℤ) + a, ⟨
    le_add_of_nonneg_left $ int.of_nat_nonneg _, add_lt_of_lt_sub_right
    $ int.lt_to_nat.1 t.2⟩⟩,
  left_inv := λ ⟨s, has, hsb⟩, subtype.eq $
    show ↑(int.to_nat (s - a)) + a = s,
    begin rw int.to_nat_of_nonneg _, ring, linarith end,
  right_inv := begin
    rintro ⟨t, ht⟩,
    suffices : int.to_nat (↑t + a - a) = t,
      simp [this],
    rw add_sub_cancel,
    exact int.to_nat_coe_nat t,
    end}

[Kevin Buzzard]

(4)

def set.Ico_equiv_add (a b n : ℤ) : set.Ico (a + n) (b + n) ≃ set.Ico a b :=
{ to_fun := λ s, ⟨s.1 - n, le_sub_right_of_add_le s.2.1, sub_lt_iff_lt_add.2 s.2.2⟩,
  inv_fun := λ t, ⟨t.1 + n, add_le_add_right t.2.1 _, add_lt_add_right t.2.2 _⟩,
  left_inv := λ _, by simp,
  right_inv := λ _, by simp }

[Kevin Buzzard]

(2)

def set.Ico_equiv_sub (a b n : ℤ) : set.Ico a b ≃ set.Ico (a - n) (b - n) :=
{ to_fun := λ s, ⟨s.1 - n, sub_le_sub_right s.2.1 _, sub_lt_sub_right s.2.2 _⟩,
  inv_fun := λ t, ⟨t.1 + n, le_add_of_sub_right_le t.2.1, add_lt_of_lt_sub_right t.2.2⟩,
  left_inv := λ s, by simp,
  right_inv := λ t, by simp }

example (a b : ℤ) : set.Ico a b ≃ set.Ico 0 (b - a) := by convert set.Ico_equiv_sub a b a; simp

I was inspired to do the result Chris had; I should have used + not - for the sign of n. We're proving that the counting measure is invariant :-) (and hence must be the Haar measure).

[Kevin Buzzard]

(5) [meh, that'll teach me to post when offline; messages have appeared in random order]

[Johan Commelin]

Sorting is hard... every computer scientist knows that :stuck_out_tongue_wink: