Zulip Chat Archive

Stream: maths

Topic: Some numerology


view this post on Zulip Patrick Massot (Sep 20 2019 at 21:44):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 21:45):

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

view this post on Zulip Floris van Doorn (Sep 20 2019 at 22:06):

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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 22:09):

the -n seems unnecessary

view this post on Zulip Floris van Doorn (Sep 20 2019 at 22:15):

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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 22:19):

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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 22:23):

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'))

view this post on Zulip Mario Carneiro (Sep 20 2019 at 22:25):

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'))

view this post on Zulip Patrick Massot (Sep 21 2019 at 08:15):

Thanks Floris and Mario!

view this post on Zulip Kevin Buzzard (Sep 21 2019 at 13:00):

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?

view this post on Zulip Johan Commelin (Sep 21 2019 at 13:01):

int.to_nat is not maths right?

view this post on Zulip Kevin Buzzard (Sep 21 2019 at 13:04):

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

view this post on Zulip Johan Commelin (Sep 21 2019 at 13:04):

It's far from strict

view this post on Zulip Kevin Buzzard (Sep 21 2019 at 13:04):

So yes, it's not maths.

view this post on Zulip Johan Commelin (Sep 21 2019 at 13:04):

I tend to prefer nat_abs

view this post on Zulip Kevin Buzzard (Sep 21 2019 at 13:04):

I thought strict meant "working with lt not le"

view this post on Zulip Johan Commelin (Sep 21 2019 at 13:04):

Also, we now have the lift tactic

view this post on Zulip Kevin Buzzard (Sep 21 2019 at 13:04):

nat_abs is the maths one, right?

view this post on Zulip Mario Carneiro (Sep 21 2019 at 18:31):

I assume it is int.to_nat_lt_to_nat

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 07:42):

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) :=

view this post on Zulip Mario Carneiro (Sep 23 2019 at 07:45):

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]

view this post on Zulip Mario Carneiro (Sep 23 2019 at 07:45):

this goes in data.int.basic

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 07:54):

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

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 07:55):

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

view this post on Zulip Mario Carneiro (Sep 23 2019 at 08:15):

I don't know how well mono handles side conditions

view this post on Zulip Simon Hudon (Sep 23 2019 at 12:59):

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

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:31):

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 :-/

view this post on Zulip Chris Hughes (Sep 23 2019 at 20:15):

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 _ _

view this post on Zulip Patrick Massot (Sep 23 2019 at 20:16):

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

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 20:31):

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.

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 20:32):

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.

view this post on Zulip Floris van Doorn (Sep 23 2019 at 20:38):

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

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 22:03):

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

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 22:04):

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

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 22:06):

aah got it cache-olean

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 22:18):

#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.

view this post on Zulip Kevin Buzzard (Sep 24 2019 at 01:35):

(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]

view this post on Zulip Kevin Buzzard (Sep 24 2019 at 01:35):

(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}

view this post on Zulip Kevin Buzzard (Sep 24 2019 at 01:35):

(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 }

view this post on Zulip Kevin Buzzard (Sep 24 2019 at 01:35):

(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).

view this post on Zulip Kevin Buzzard (Sep 24 2019 at 01:35):

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

view this post on Zulip Johan Commelin (Sep 24 2019 at 04:32):

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


Last updated: May 06 2021 at 19:30 UTC