Zulip Chat Archive

Stream: maths

Topic: more int nat moans and golf plea


view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:02):

example (x y : ) (h1 : nat.coprime (int.nat_abs x) (int.nat_abs y)) (h2 : x ^ 2 + 3 * y ^ 2 = 4) :
(x = 1  x = -1)  (y = 1  y = -1) :=

Sent to me by @Clara List . The mathematician's proof: "h2 trivially implies |x|<=2 and |y|<=1; now check all cases". This line of reasoning should be feasible in Lean, right? How does one do it?

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:04):

I am embarrassed to post my solution. I decided it might be easier to convert everything to nat, but the killer dec_trivial line didn't work anyway:

import algebra.group_power

example (x y : ) (h1 : nat.coprime (int.nat_abs x) (int.nat_abs y)) (h2 : x ^ 2 + 3 * y ^ 2 = 4) :
(x = 1  x = -1)  (y = 1  y = -1) :=
begin
  let x0 := int.nat_abs x,
  let y0 := int.nat_abs y,
  -- now effortfully change to a question about nats
  have Hx : (x0 * x0) = x * x := int.nat_abs_mul_self,
  have Hy : (y0 * y0) = y * y := int.nat_abs_mul_self,
  change x * (x * 1) + 3 * (y * (y * 1)) = 4 at h2,
  rw [mul_one,mul_one] at h2,
  rw [Hx, Hy] at h2,
  change (x0 * x0) + ((3 : ) : ) * (y0 * y0) = (4 : ) at h2,
  rw [int.coe_nat_mul, int.coe_nat_add, int.coe_nat_eq_coe_nat_iff] at h2,
  -- finally got h2 : x0 * x0 + 3 * (y0 * y0) = 4
  -- but mathematicians do not want to waste their time with the last 4 lines
  -- and need training before they can even construct them. What am I missing?

  -- now change the goal in the same way
  suffices : x0 = 1  y0 = 1,
    split,
    { have H : x = x0  x = -x0 := int.nat_abs_eq x,
      rw this.1 at H,
      exact H },
    { have H : y = y0  y = -y0 := int.nat_abs_eq y,
      rw this.2 at H,
      exact H },

  -- It's now a question about nats. I regret doing all that.
  clear Hx Hy,

  have Hx0 : x0 * x0  2 * 2,
    show _  4,
    rw h2,
    exact nat.le_add_right (x0 * x0) (3 * (y0 * y0)),
  have Hy0 : y0 * y0  1 * 1,
    suffices : 3 * (y0 * y0)  4,
      rwa [mul_comm, nat.le_div_iff_mul_le] at this, exact dec_trivial,
    rw h2,
    apply nat.le_add_left,
  rw nat.mul_self_le_mul_self_iff at Hx0,
  rw nat.mul_self_le_mul_self_iff at Hy0,
  have H : nat.coprime x0 y0 := h1,
  revert H,
  revert h2,
  revert Hx0,
  revert Hy0,
  -- goal now
  -- ⊢ y0 ≤ 1 → x0 ≤ 2 → x0 * x0 + 3 * (y0 * y0) = 4 → nat.coprime x0 y0 → x0 = 1 ∧ y0 = 1
  exact dec_trivial, -- AARGH! Fails!
  sorry
end

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:06):

That is pretty horrible and it didn't work either. (1) how to get dec_trivial to work and (2) can it work with ints? I guess we want (x : int) ^ 2 <= N -> int.nat_abs x <= sqrt N or x ^ 2 <= N -> - sqrt N <= x and x <= sqrt N or something. But will this be enough for dec_trivial? Are these in mathlib somewhere? Of course there will be the usual kerfuffle coming from the fact that N is an int instead of a nat (see other nat int thread where I propose a goofy typeclass solution to this)

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:35):

example (n : ℕ) : n ≤ 0 → n = 0 := dec_trivial -- fails. What modification makes this work? I'm sure I've seen people get dec_trivial to check a finite set of nats before

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:36):

revert n

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:39):

gaargh it's still not over

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:41):

example (x : ) (h : int.nat_abs x  0) : int.nat_abs x = 0 :=
begin
  let n := int.nat_abs x,
  change n  0 at h,
  show n = 0,
  revert h,
  revert n,
  -- ⊢ let n : ℕ := int.nat_abs x in n ≤ 0 → n = 0
  exact dec_trivial -- fails
end

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:41):

I could fix this with generalize instead of let but in my actual use case there are 20 lines of manipulating n and x before I want to apply exact dec_trivial. I will work on the generalize trick though.

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:50):

Oh -- here's the problem. OK I'm stuck again :-(

example :  (n : ), n  0  n = 0 := dec_trivial -- type class inference fails
-- ⊢ decidable (∀ (n : ℕ), n ≤ 0 → n = 0)

Oh -- I can fix this with a random import :-/

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:54):

Oh, nope, still can't do it. I think I do need @Chris Hughes now.

import algebra.group_power

example :  (x1 y1 : ), y1  1  x1  2  x1 * x1 + 3 * (y1 * y1) = 4
   nat.coprime x1 y1  x1 = 1  y1 = 1 := dec_trivial
/-
failed to synthesize type class instance for
⊢ decidable
    (∀ (x1 y1 : ℕ),
       y1 ≤ 1 → x1 ≤ 2 → x1 * x1 + 3 * (y1 * y1) = 4 → nat.coprime x1 y1 → x1 = 1 ∧ y1 = 1)
-/

How do I begin to figure out what is not decidable here?

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 09:00):

example :  (y1 : ), y1  1   (x1 : ), x1  2  x1 * x1 + 3 * (y1 * y1) = 4
   nat.coprime x1 y1  x1 = 1  y1 = 1 := dec_trivial

:grinning:

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 09:06):

import algebra.group_power

example (x y : ) (h1 : nat.coprime (int.nat_abs x) (int.nat_abs y)) (h2 : x ^ 2 + 3 * y ^ 2 = 4) :
(x = 1  x = -1)  (y = 1  y = -1) :=
begin
  let x0 := int.nat_abs x,
  let y0 := int.nat_abs y,
  -- now effortfully change to a question about nats
  have Hx : (x0 * x0) = x * x := int.nat_abs_mul_self,
  have Hy : (y0 * y0) = y * y := int.nat_abs_mul_self,
  change x * (x * 1) + 3 * (y * (y * 1)) = 4 at h2,
  rw [mul_one,mul_one] at h2,
  rw [Hx, Hy] at h2,
  change (x0 * x0) + ((3 : ) : ) * (y0 * y0) = (4 : ) at h2,
  rw [int.coe_nat_mul, int.coe_nat_add, int.coe_nat_eq_coe_nat_iff] at h2,
  -- finally got h2 : x0 * x0 + 3 * (y0 * y0) = 4
  -- but mathematicians do not want to waste their time with the last 4 lines
  -- and need training before they can even construct them. What am I missing?

  -- now change the goal in the same way
  suffices : x0 = 1  y0 = 1,
    split,
    { have H : x = x0  x = -x0 := int.nat_abs_eq x,
      rw this.1 at H,
      exact H },
    { have H : y = y0  y = -y0 := int.nat_abs_eq y,
      rw this.2 at H,
      exact H },

  -- now a question about nats. I regret doing all that.
  clear Hx Hy,

  have Hx0 : x0 * x0  2 * 2,
    show _  4,
    rw h2,
    exact nat.le_add_right (x0 * x0) (3 * (y0 * y0)),
  have Hy0 : y0 * y0  1 * 1,
    suffices : 3 * (y0 * y0)  4,
      rwa [mul_comm, nat.le_div_iff_mul_le] at this, exact dec_trivial,
    rw h2,
    apply nat.le_add_left,
  rw nat.mul_self_le_mul_self_iff at Hx0,
  rw nat.mul_self_le_mul_self_iff at Hy0,
  have H : nat.coprime x0 y0 := h1,
  revert H,
  revert h2,
  revert Hy0,
  generalize : y0 = y1,
  revert y1,
  revert Hx0,
  generalize : x0 = x1,
  revert x1,
  exact dec_trivial,
end

Those reverts and generalizes near the end have to be done in pretty much exactly the right order :-)

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 09:36):

OK here is my challenge. This is a concrete example of the sort of thing which my undergraduate mathematicians are reading in their lecture notes and are finding very hard to put into Lean. The following result is extremely easy for a mathematician and I have supplied a 4-line pseudocode proof. How many lines does take an expert Leaner? I would very much like to get this answer down to 4. Even eight lines would be fine at this point -- between each line of code corresponding to the pseudocode it would be fine to have ashow or something, or suffices : ..., by simp or whatever. What I don't want is random bursts of 5 lines of garbage to get Lean to jump from line to line, because on some very concrete level that pseudocode proof looks complete to me and, more to the point, will look complete to most mathematicians.

import data.rat algebra.group_power

example (x y : ) : (x : ) ^ 2 + 2 * y ^ 2 = 3  (x = 1  x = -1)  (y = 1  y = -1) := sorry
/-
Pseudo-code proof
1) Squares are non-negative
2) Hence x ^ 2 <= 3 and y ^ 2 <= 3/2
3) Hence |x| <= 1 and |y| <= 1
4) Now check all cases.
-/

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 09:56):

PS I guess the "and" lines can be split, giving us six lines of pseudocode, and i would even allow for seven if we wanted to get from 2y^2 le 3 to y^2 le 3/2

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 09:57):

The lean issues are getting from rat to int (and when?) and getting dec_trivial to check the cases

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 10:00):

PPS I recommend not going via nat. @Kenny Lau how many lines of tactic mode does it take you to solve my challenge?

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 10:05):

PPPS example (x y : ℤ) : (x : ℚ) ^ 2 + 2 * y ^ 2 = 3 ↔ x ^ 2 + 2 * y ^ 2 = 3 := by simp fails :-(. Why?? PPPPS you will all be pleased to know that I am now going to do 5 hours of admin with Lean chat off.

view this post on Zulip Johannes Hölzl (Sep 28 2018 at 10:13):

I guess for step 2) you can try to use linarith.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 10:16):

it doesn't look very linear to me

view this post on Zulip Rob Lewis (Sep 28 2018 at 10:18):

Step 2 is linear if you treat the squares as atoms. But this isn't the hard part of the proof.

view this post on Zulip Rob Lewis (Sep 28 2018 at 10:18):

example (x y : ) : (x : ) ^ 2 + 2 * y ^ 2 = 3  (x = 1  x = -1)  (y = 1  y = -1) :=
λ h,
have hxn : (x : ) ^ 2  0, from pow_two_nonneg _,
have hyn : (y : ) ^ 2  0, from pow_two_nonneg _,
have hx3 : (x : ) ^ 2  3, by linarith,
have hy3 : (y : ) ^ 2  3/2, by linarith,
_

view this post on Zulip Mario Carneiro (Sep 28 2018 at 10:23):

can you prove (x : ℚ) ^ 2 < 4 and (y : ℚ) ^ 2 < 4 instead by linarith?

view this post on Zulip Rob Lewis (Sep 28 2018 at 10:24):

Yup.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 10:24):

I believe there is a theorem that says a^2 < b^2 <-> a < b

view this post on Zulip Rob Lewis (Sep 28 2018 at 10:24):

I hope there's no theorem that says that on rat.

view this post on Zulip Rob Lewis (Sep 28 2018 at 10:25):

Or int, for that matter.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 10:25):

It should hold on rat, but I'm omitting the nonnegativity assumptions

view this post on Zulip Scott Morrison (Sep 28 2018 at 10:39):

@Rob Lewis, how hard do you think it would be to ask linarith to "try harder", automatically treating subexpressions it doesn't understand as atoms?

view this post on Zulip Mario Carneiro (Sep 28 2018 at 10:40):

isn't that what it's already doing?

view this post on Zulip Scott Morrison (Sep 28 2018 at 10:42):

example (x y : ℕ) (h : 6 + ((x + 4) * x + (6 + 3 * y) * y) = 3) : false :=
by linarith

view this post on Zulip Scott Morrison (Sep 28 2018 at 10:42):

Says no args to linarith.

view this post on Zulip Scott Morrison (Sep 28 2018 at 10:43):

While I'm hoping for something that would first generalize (x + 4) * x and (6 + 3 * y) * y ftw.

view this post on Zulip Scott Morrison (Sep 28 2018 at 10:44):

I guess I can see how to do this, I'm just hoping someone says there's an easier way than what I have in mind. :-)

view this post on Zulip Rob Lewis (Sep 28 2018 at 11:12):

It wouldn't be hard to make it handle things like that. Right now, if it sees an obvious nonlinearity, it will reject that hypothesis. x^2 doesn't count as obvious because it's only checking + and *.

view this post on Zulip Rob Lewis (Sep 28 2018 at 11:15):

@Mario Carneiro I don't think we have the necessary nonnegativity assumptions in Kevin's problem, at least not without some work, which kind of defeats the point. And there's still some pain dealing with casts. Ultimately, I think we need some sort of "cast correction" tactic and integer arithmetic to do that properly.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 11:16):

well, you want to rewrite with a^2 = (abs a)^2 first, and then you have your nonnegativity assumption

view this post on Zulip Rob Lewis (Sep 28 2018 at 11:34):

@Scott Morrison Hmm, let me qualify my last response -- the way linarith handles nats right now makes it slightly harder. I'll think about a clean way to do this.

view this post on Zulip Rob Lewis (Sep 28 2018 at 11:35):

But it's easy to make it handle this:

example (x y : ) (h : 6 + ((x + 4) * x + (6 + 3 * y) * y) = 3) (h' : (x + 4) * x  0)
  (h'' : (6 + 3 * y) * y  0)  : false :=
by linarith

view this post on Zulip Scott Morrison (Sep 28 2018 at 11:47):

That's great. (And the same for nats would be great!)

view this post on Zulip Rob Lewis (Sep 28 2018 at 11:55):

https://github.com/leanprover/mathlib/pull/379

view this post on Zulip Kenny Lau (Sep 28 2018 at 14:35):

PPS I recommend not going via nat. @Kenny Lau how many lines of tactic mode does it take you to solve my challenge?

I respectfully decline for personal reasons.

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:40):

Hi @Kevin Buzzard, with a few(!) additional simp lemmas, some of which are perfectly sensible, and some of which are less so, we can do:

@[tidy] meta def la := `[linarith]
@[tidy] meta def cases_xy := `[cases x; cases y]

example (x y : ℤ) (h1 : nat.coprime (int.nat_abs x) (int.nat_abs y)) (h2 : x ^ 2 + 3 * y ^ 2 = 4) :
  (x = 1 ∨ x = -1) ∧ (y = 1 ∨ y = -1) :=
by tidy

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:41):

That's not exactly what I asked but I agree that this is a big step forward

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:41):

Oh, it isn't? I must have changed it at some point and forgotten I changed it.

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:41):

Let me go find the original :-)

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:41):

I don't care about efficiency, I care about making life easier for beginner mathematicians

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:41):

The equality was over rat

view this post on Zulip Kenny Lau (Sep 29 2018 at 11:42):

how many seconds does it take to compile?

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:42):

Because moving from rat to int is another great example of something which is easy in maths

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:43):

Oh -- this was your original question (exactly), but then you asked a different one I didn't see yet.

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:43):

Oh! Yes you're exactly right

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:43):

I asked a challenge problem later

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:44):

which you have made serious inroads into

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:44):

Are those safe tidy lemmas by the way?

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:45):

@Kenny Lau --- it takes 13 seconds, or 5 seconds after you substitute in the proof tidy provides.

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:45):

It's fine to use linarith in tidy, as long as you don't care about how long things take to run. :-)

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:45):

Scott I think this is the first time I've seen tidy do something which I really did not want to do myself

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:46):

It's completely insane to let tidy case bash on ints or nats unless you know case bashing is the right thing to do.

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:46):

Kenny I don't care how long it takes to run because this is for undergraduates solving cheap problems, not a library

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:48):

I'm hiding here quite a few simp lemmas I had to write before this could work.

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:48):

The dubious one was:

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:48):

meta def dt := `[exact dec_trivial]
@[simp] lemma int.of_nat_eq_neg (n : ℕ) (m : ℤ) (h : m < 0 . dt) : int.of_nat n = m ↔ false := sorry

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:49):

(And here of course by "write" I mean "write the statement of and sorry the proof", as usual. :-)

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:50):

I think I could manage a proof of that one

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:50):

oh -- there's nothing scary with the proof. The scary thing is have the exact dec_trivial autoparam.

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:51):

I've no idea if that is a viable thing to do in a @[simp] lemma. I mean, it works, apparently, but it may be insane for some reason I don't understand. :-)

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:51):

The full set of simp lemmas I needed was

@[simp] lemma nat.coprime_zero (n : ℕ) : nat.coprime n 0 = false := sorry
@[simp] lemma nat.zero_coprime (n : ℕ) : nat.coprime 0 n = false := sorry

local attribute [simp] nat.succ_eq_add_one

@[simp] lemma nat.add_has_add (a b : ℕ) : nat.add a b = a + b := rfl
@[simp] lemma nat.mul_has_mul (a b : ℕ) : nat.mul a b = a * b := rfl
@[simp] lemma nat.pow_has_pow (a b : ℕ) : nat.pow a b = a ^ b := rfl

local attribute [simp] int.of_nat_add
local attribute [simp] int.of_nat_one

@[simp] lemma foo_1 (a b : ℕ) : a + b = a ↔ b = 0 := sorry
@[simp] lemma foo_2 (a b c : ℕ) : a + (b + c) = c ↔ a + b = 0 := sorry

@[simp] lemma nat.square_zero (n : ℕ) : n^2 = 0 ↔ n = 0 := sorry

local attribute [simp] nat.pow_zero
local attribute [simp] nat.pow_one

meta def dt := `[exact dec_trivial]

@[simp] lemma int.of_nat_eq_neg (n : ℕ) (m : ℤ) (h : m < 0 . dt) : int.of_nat n = m ↔ false := sorry
@[simp] lemma int.of_nat_eq_one (n : ℕ) : int.of_nat n = 1 ↔ n = 1 := sorry
@[simp] lemma int.neg_succ_of_nat_eq_nneg (n : ℕ) (m : ℤ) (h : m ≥ 0 . dt) : int.neg_succ_of_nat n = m ↔ false := sorry
@[simp] lemma int.neg_succ_of_nat_eq_minus_one (n : ℕ) : int.neg_succ_of_nat n = -1 ↔ n = 0 := sorry

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:51):

I am supposed to be suggesting a list of projects for third year undergraduate joint maths/computing students and they want the list by Monday. I was going to propose making my number class as one of them

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:52):

Also -- this relies on Robert's latest PR for linarith; it doesn't work with the current mathlib one.

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:52):

I don't mind about that either

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:55):

I'm always surprised by how little is marked with @[simp] in mathlib

view this post on Zulip Mario Carneiro (Sep 29 2018 at 11:55):

I'm sure Kenny doesn't feel the same way

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:55):

Like int.of_nat_one. How is that not a simp lemma?

view this post on Zulip Mario Carneiro (Sep 29 2018 at 11:56):

Isn't that in core?

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:56):

Ah, okay :-)

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:56):

We can still add the attribute, I guess!

view this post on Zulip Mario Carneiro (Sep 29 2018 at 11:56):

At the start of int.basic is

attribute [simp] int.coe_nat_add int.coe_nat_mul int.coe_nat_zero int.coe_nat_one int.coe_nat_succ

view this post on Zulip Mario Carneiro (Sep 29 2018 at 11:57):

I think we need a simp lemma for of_nat -> coe_nat

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:57):

I see. Sounds good!

view this post on Zulip Scott Morrison (Sep 29 2018 at 11:58):

And how about

attribute [simp] nat.pow_zero nat.pow_one

view this post on Zulip Scott Morrison (Sep 30 2018 at 09:45):

I'm curious about

@[simp] theorem int.cast_pow [ring α] (n : ℤ) (m : ℕ) : (↑(n ^ m) : α) = ↑n ^ m :=

view this post on Zulip Scott Morrison (Sep 30 2018 at 09:45):

My instinct would be to simp the other way here!

view this post on Zulip Kenny Lau (Sep 30 2018 at 09:45):

well it's the same as int.cast_mul and int.cast_add and etc

view this post on Zulip Scott Morrison (Sep 30 2018 at 09:45):

Yes. :-)

view this post on Zulip Scott Morrison (Sep 30 2018 at 09:46):

Do you know situations where it's useful to simp in this direction?

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:05):

int.of_nat (n - m)

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:06):

Usually it doesn't matter as long as it is in a consistent direction, but generally speaking it is harder to simp the other way around because it is a kind of "distribution" lemma - the casts on the rhs have to line up for the simp to work, which can be a problem if simp wants to write \u a + b + \u c

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:08):

The recommended technique for bringing your casts together is to assert the form you want and simpa to reduce it to your goal

view this post on Zulip Kenny Lau (Sep 30 2018 at 10:08):

simpa only

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:08):

Chris made a comment to me about all this -- he said the rule of thumb was that simp wants to make the up-arrows as close as possible to the variables

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:09):

That clarified things for me. My main beef is that you need to know the general cast lemmas from nat to blah and then a bunch of different ones for going from nat to int.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:10):

I hope we get the cast tactic for dealing with this

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:11):

My hope was to let everything be a number and let type class inference deal with everything

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:11):

Is this related?

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:12):

Would part of this tactic be the is_actually_an_int typeclass?

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:12):

I wasn't planning on it

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:12):

I'm not sure how those plans interact with the is_int class

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:14):

I am unclear on the details, but I am very clear on what I want the outcome to be: easy passing from (x : rat) ^ 2 + 2 * y ^ 2 = 7 to x ^ 2 + 2 * y ^ 2 = 7 with x y ints, where some of those 2's are nats and some are rats, and some of those 7's are ints are some are rats, and in the future this won't matter.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:15):

Yes, I think this can be done

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:16):

The idea is you point at an equation and say "make this an equation on int" and it figures out the appropriate coercions rewriting this way and that

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:17):

Is this tactic just on a list of things to do, or are there actually plans to develop it? My users would find it extremely helpful.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:17):

somewhere in between

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:18):

I have a fairly concrete idea of how to implement it, but I haven't tried

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:18):

That's great news. I'm really glad it's on your radar in some sense.

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:21):

This is I think the third time when I have managed to pinpoint an issue which is "trivial in maths and hard in Lean", and you solved both the previous ones. The first was that it seemed to be very hard to prove things like "2 + 2 \not= 5" for real numbers in Lean, and then norm_num appeared. The second was that it seemed to be very hard to prove (x+y)^3=x^3+3x^2y+3xy^2+y^3 in Lean and then ring appeared. The reason I find these sorts of questions particularly interesting to focus on is that undergraduate mathematicians take these sorts of things for granted, having no insight into what actually goes in to proving them, but I would rather not try to teach them that insight, I would rather it were just easy.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:23):

usually the hard part with these tactics is just figuring out what you want them to do (and what is not in scope)

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:24):

it's hard to do anything with "I want magic", but "I want a decision procedure for linear inequalities on nat" has a clear enough specification to actually get implemented

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:25):

"the hard part" -- I beg to differ. From where I'm standing, the hard part is that there are an extremely small number of people in the world who are equipped to write these tactics, and they are all busy. And I am not yet one of those people. That's why I wrote the ring blog post, to get some sort of insight into how these things might work. I am also not yet convinced that I will be able to write a convincing grant proposal to pay for a computer scientist to write these tactics for me, because the applications are firmly pedagogical and the big grant funders in the UK are more interested in research.

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:27):

But I saw undergraduates bravely struggling with this sort of thing all summer, and the reason I got up to speed with how casts currently work in Lean is so I could write the code myself which solved their problems in the particular instances they got stuck at.

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:28):

e.g. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Coercions.20N-.3EZ-.3EQ-.3ER-.3EC

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:28):

By the way, it is very easy to write a tactic that does what this cast would do, if you aren't picky about the flexibility

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:29):

It is very easy for you. I have never written meta code and currently I don't have the time to learn.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:29):

you can just define a tactic like `[rw <- int.cast_inj, simp [int.cast_one, int.cast_add, ...]]

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:29):

Also it takes me a long time to learn things, far longer than it takes people like you or Chris or Kenny.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:29):

I mean a "poor mans tactic"

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:31):

I think I've even used essentially this tactic in data.num.lemmas

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:33):

My strategy is different. I encourage Chris and Kenny to learn tactics and next week I will be encouraging many more people to learn Lean and then encouraging the best ones to learn tactics. One might argue that part of the reason that localisations of rings and quadratic reciprocity are now in mathlib is that people near me somehow got persuaded that these were important projects. And for me they are extremely important because they are undergraduate level mathematics, which is something I am hugely trying to push.

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:33):

I don't know to what extent norm_num and ring got written because of rants by me about how mathematicians needed them, but I know for sure that I am extremely grateful for both.

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:40):

Another thing I know for sure is that a bright undergraduate is less busy than a bright PhD student, because it's much easier for the bright undergraduate to coast.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:41):

The rants were definitely a factor :)

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:42):

I try to let the community decide my priorities to some extent, so being loud is not ineffective if you want me to make something for you

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:43):

Thank you Mario for not just writing me off as an asshole.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:44):

you're just a guy with crazy pants

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:44):

My summer students would have been completely lost without ring and norm_num.

view this post on Zulip Patrick Massot (Sep 30 2018 at 10:45):

Don't forget we also rant about the module refactoring and the module tactic

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:45):

I am writing teaching materials and I introduce ring and norm_num at the same time as rw. That's how important they seem to be in practice when doing undergraduate problem sheets in mathematics.

view this post on Zulip Patrick Massot (Sep 30 2018 at 10:46):

The point where module refactoring is the main stumbling block of the perfectoid project is approaching fast.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:46):

it's my top lean priority right now

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:46):

ROFL the slower module refactoring goes the longer I have an excuse for putting off the perfectoid project, which is what I have needed to do over the last week or two

view this post on Zulip Patrick Massot (Sep 30 2018 at 10:47):

With the category theory PR

view this post on Zulip Patrick Massot (Sep 30 2018 at 10:47):

Is 33 open PR our new record?

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:47):

I think second is merging the ever growing zoo of community branches

view this post on Zulip Patrick Massot (Sep 30 2018 at 10:48):

The community (not only you) needs to go through the community repo and delete or rename branches

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:48):

Patrick I was thinking about pushing perfectoids forward by epsilon yesterday but all I managed to do was write down a bit more precisely what needed to be done next. I pushed a commit which was just about ten lines of comments!

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:48):

Again I think that the long term solution for this is training

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:49):

I wonder whether it would be possible to set up a voting system for the PRs

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:49):

so we can prioritize them a bit

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:50):

are thumbs up on a PR visible from the PR list?

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:50):

The risk with that is that if Patrick and I start rallying the troops to vote for the mathsy ones then Simon's work on traversable or other stuff which I don't understand the point of ends up languishing forever.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:51):

that seems fair - you actually have more users

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:51):

I'm not saying there's no point though

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:52):

and what I worry about is that actually in the long term whatever simon is doing might end up being much more important for making stuff work

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:53):

I think I can judge that to some extent, any voting would be a suggestion at best

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:53):

Patrick, I got into the habit of calling my branches kmb_... because I felt it only right that I should take some sort of responsibility for their existence.

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 10:55):

After module refactoring I will go back to them and take a good look at all of the ones I created and then tidy them up. But (in contrast to you) I am not in a hurry for this because I am trying to put together a bunch of cocalc example sheets and a bunch of lean example sheets and in the long term I believe it's in my (and possibly the community's) interests to make the delivery of my course as smooth as possible.

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:56):

yeah, I realize that the module refactoring is going to cause some disruption

view this post on Zulip Mario Carneiro (Sep 30 2018 at 10:59):

In my metamath days the main database set.mm was like 90% of the existing code in the community, so if I do a refactoring and fix everything that's there most people don't feel the change. With mathlib it's probably closer to 60% so I either have to visit everyone's projects or trust that they can fix it themselves

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 11:00):

I am very happy to fix my comm alg stuff and perfectoid stuff myself.

view this post on Zulip Kevin Buzzard (Sep 30 2018 at 11:01):

I understand how all this works much better now. But it's also a reason why I don't want to write anything new right now (that and the far more important reason that I have no time).

view this post on Zulip Patrick Massot (Sep 30 2018 at 11:36):

Sorry, I was captured by my children. My votes are: module refactoring and Scott's PR


Last updated: May 18 2021 at 08:14 UTC