## Stream: new members

### Topic: help finding a lemma

#### Scott Morrison (Feb 23 2019 at 10:33):

Where is (a - b) - (c - b) = a - c? (With the appropriate inequality as a hypothesis)

so... for nat?

Sure.

#### Scott Morrison (Feb 23 2019 at 10:34):

(Sorry, yes, I should have said that!)

#### Scott Morrison (Feb 23 2019 at 10:36):

Is this meant to be called sub_sub_sub_right or something?

#### Scott Morrison (Feb 23 2019 at 10:37):

by analogy with nat.add_sub_add_right : ∀ (n k m : ℕ), n + k - (m + k) = n - m

#### Chris Hughes (Feb 23 2019 at 10:41):

The group version is called sub_sub_sub_cancel_right. I would rather be consistent with that.

#### Scott Morrison (Feb 23 2019 at 10:49):

Sure! But does it exist already?

Surely?

#### Chris Hughes (Feb 23 2019 at 10:50):

#find ((_ - _) - (_ - _) = _) didn't return anything about naturals.

#### Scott Morrison (Feb 23 2019 at 10:51):

And while we're at it: a \le b \imp (a - c) \le (b-c)?

#### Chris Hughes (Feb 23 2019 at 10:51):

nat.sub_le_sub_left is there.

#### Chris Hughes (Feb 23 2019 at 10:52):

sorry right

#### Scott Morrison (Feb 23 2019 at 10:55):

Ok:

lemma sub_sub_sub_cancel_right {a b c : ℕ} (h₂ : c ≤ b) : (a - c) - (b - c) = a - b :=
begin
exact h₂
end


looks okay? Can I put that in data/nat/basic.lean?

#### Chris Hughes (Feb 23 2019 at 10:57):

Yes. Can't you rw ←nat.add_sub_assoc h₂ and put the proof on one line

Thanks.

#### Chris Hughes (Feb 23 2019 at 10:59):

Should probably be protected as well

Why is that?

#### Kevin Buzzard (Feb 23 2019 at 11:12):

One could go through every lemma proved for add comm groups and reprove it for nat with the appropriate inequalities added as hypotheses if necessary.

#### Scott Morrison (Feb 23 2019 at 11:13):

That sounds like a good exercise for someone. :-)

#### Scott Morrison (Feb 23 2019 at 11:14):

I _hate_ having to deal with stupid inequalities. At the moment I'm staring at

h₂ : a < m,
h₃ : m ≤ a
⊢ false


and trying to remember implementation details of lt and le...

#### Scott Morrison (Feb 23 2019 at 11:16):

I guess exact not_lt_of_ge h₃ h₂ is not so bad. But where is my duh tactic for these? Can we just import linarith at the beginning of time?

#### Scott Morrison (Feb 23 2019 at 11:17):

How about a lemma that says "two lists are equal if they are both ordered according to a strict order, and they have the same members"?

#### Kevin Buzzard (Feb 23 2019 at 11:18):

linarith

#### Kevin Buzzard (Feb 23 2019 at 11:19):

oh you know linarith. Does it not work? whenever I'm doing undergraduate analysis it's the first thing I import after data.real.basic

#### Kevin Buzzard (Feb 23 2019 at 11:20):

you could also prove a < a with lt_of_lt_of_le I guess

#### Mario Carneiro (Feb 23 2019 at 11:42):

The two lists are equal thing is eq_of_sorted_of_perm

#### Scott Morrison (Feb 23 2019 at 11:52):

@Kevin Buzzard, the problem here is that I'm filling in gaps I'm finding back in data.list, data.finset and data.multiset, where it's presumably too early to import linarith.

#### Scott Morrison (Feb 23 2019 at 11:52):

And there's no linarith? mode that prints out a proof term for you. :-)

Oh I see!

#### Mario Carneiro (Feb 23 2019 at 12:07):

I want a tactic that explores short tactic scripts and gives you a short proof if one exists

#### Rob Lewis (Feb 23 2019 at 12:36):

I promise you don't want to see the proof terms that linarith generates. :)

def f (a : ℤ) (ha : a < 1) : a < 1 :=
by linarith

#print f


#### Scott Morrison (Feb 23 2019 at 22:44):

What is lemma nat.le_pred_of_lt (h : a < b) : a ≤ b - 1 actually called?

#### Chris Hughes (Feb 23 2019 at 22:46):

nat.pred_le_iff

#### Scott Morrison (Feb 23 2019 at 22:50):

oh, but that's still only half of it

#### Scott Morrison (Feb 23 2019 at 22:51):

actually, @Chris Hughes, I think that one is irrelevant here

#### Chris Hughes (Feb 23 2019 at 22:55):

Yeah, it's pred_le not le_pred

#### Scott Morrison (Feb 24 2019 at 03:47):

How is one meant to prove

lemma nat.ge_one_of_gt {n m : ℕ} (h : m > n) : m ≥ 1 :=
le_trans ((le_add_iff_nonneg_left _).2 (nat.zero_le _)) h


That proof is obviously lame.

#### Mario Carneiro (Feb 24 2019 at 03:54):

I would have gone for lt_trans (nat.zero_le _) h

#### Mario Carneiro (Feb 24 2019 at 03:55):

also, stop using ge and gt so much

#### Scott Morrison (Feb 24 2019 at 04:12):

Hmm.. I used ge and gt here for the sake of naming.

#### Scott Morrison (Feb 24 2019 at 04:12):

Would you name it lemma nat.one_le_of_lt {n m : ℕ} (h : n < m) : 1 \le m :=?

#### Scott Morrison (Feb 24 2019 at 04:13):

Somehow that seems harder to parse. (Because the subject of the phrase is embedded in the middle "one is le than ARGUMENT of lt", rather than "ARGUMENT is ge one of gt".)

#### Scott Morrison (Feb 24 2019 at 04:30):

Grah, I hate (Lean's lack of support for) the natural numbers so much.

#### Scott Morrison (Feb 24 2019 at 04:30):

What is the easiest proof of false, given a : n + 1 ≤ n?

#### Andrew Ashworth (Feb 24 2019 at 04:44):

example (n : ℕ) : ¬(n + 1 ≤ n) := not_le_of_gt (nat.lt_succ_self _)

#### Scott Morrison (Feb 24 2019 at 04:46):

Thanks, @Andrew Ashworth.

#### Jesse Michael Han (Feb 24 2019 at 04:53):

there's also a nat lemma that says exactly what you want

example : (n : ℕ) : ¬(n + 1 ≤ n) := nat.not_succ_le_self _


(of course linarith works, but the proof term is hideous)

#### Scott Morrison (Feb 26 2019 at 10:14):

Do we have lemma mul_mod (a b n : ℕ) : (a * b) % n = (a % n) * (b % n) % n := sorry?

#### Patrick Massot (Feb 26 2019 at 10:15):

I would look into data/nat/modeq.lean

#### Scott Morrison (Feb 26 2019 at 10:37):

Doesn't seem to be there. It seems a pain to prove, actually.

#### Scott Morrison (Feb 26 2019 at 10:37):

I'd be surprised if it hasn't been needed yet

#### Scott Morrison (Feb 26 2019 at 10:37):

similarly for add_mod.

#### Mario Carneiro (Feb 26 2019 at 10:42):

It follows from some stuff about modeq

#### Mario Carneiro (Feb 26 2019 at 10:43):

it is roughly modeq_mul mod_modeq mod_modeq

okay, I see.

#### Patrick Massot (Feb 26 2019 at 10:43):

Why not descending all this to $Z/n$?

#### Scott Morrison (Feb 26 2019 at 10:44):

modeq seems supremely painful to use ... rather than just having a new type for N/nN and Z/nZ

#### Scott Morrison (Feb 26 2019 at 10:44):

has someone done N/nZ and Z/nZ?

#### Patrick Massot (Feb 26 2019 at 10:44):

Prove that $a \% n = b \% n$ iff $\pi(a) = \pi(b)$ where $\pi$ goes down from $Z$ to $Z/n$

#### Mario Carneiro (Feb 26 2019 at 10:44):

there is a type for Z/nZ

#### Mario Carneiro (Feb 26 2019 at 10:44):

like Patrick said

#### Mario Carneiro (Feb 26 2019 at 10:45):

zmod

#### Mario Carneiro (Feb 26 2019 at 10:46):

zmod.eq_iff_modeq_nat

#### Scott Morrison (Feb 26 2019 at 11:01):

Thanks!

... so at the end of the day I get a hypothesis 1 = 1 + (1 + (1 + 4 * ↑n)) (here we are in zmod 4) and I want to prove false...

#### Mario Carneiro (Feb 26 2019 at 11:01):

I think you can change 4 with 0

#### Mario Carneiro (Feb 26 2019 at 11:02):

there's probably a better way though

#### Mario Carneiro (Feb 26 2019 at 11:02):

cast_self_eq_zero?

#### Scott Morrison (Feb 26 2019 at 11:03):

I can't seem to get that to rewrite. Because the 4 here is the actual numeral, not the cast of the 4 in \nat+

#### Scott Morrison (Feb 26 2019 at 11:04):

change 4 with 0 at w doesn't seem to have any effect

#### Mario Carneiro (Feb 26 2019 at 11:07):

change 4 with ((4:N+):N) might work

#### Mario Carneiro (Feb 26 2019 at 11:08):

Or just go back to nats from this point

#### Scott Morrison (Feb 26 2019 at 11:08):

How do I go back to nats? That's what I'm missing, I think.

#### Scott Morrison (Feb 26 2019 at 11:09):

Here's a MWE:

lemma foo (n : ℕ) (h : @eq (zmod 4) 1
1
1
1
(@has_mul.mul (zmod 4)
(@mul_zero_class.to_has_mul (zmod 4)
(@semiring.to_mul_zero_class (zmod 4)
(@ring.to_semiring (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4)))))
4
(@coe nat (zmod 4)
(@coe_to_lift nat (zmod 4)
(@coe_base nat (zmod 4)
(@nat.cast_coe (zmod 4) (zmod.has_zero 4) (zmod.has_one 4)
(@ring.to_distrib (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4)))))))
n)))))) : false :=
begin

end


#### Mario Carneiro (Feb 26 2019 at 11:15):

this works:

  simp [show (4:zmod 4) = 0, from @zmod.cast_self_eq_zero 4] at h,
cases h


woah... okay.

#### Scott Morrison (Feb 26 2019 at 11:17):

Is there any way we can make that more ergonomic?

#### Scott Morrison (Feb 26 2019 at 11:18):

It seems like the sort of thing you'd hope simp to do unassisted.

#### Scott Morrison (Feb 26 2019 at 11:20):

or are we just doomed because the 4 here is a numeral?

#### Mario Carneiro (Feb 26 2019 at 11:22):

That's one of the things that the cast tactic is supposed to do

#### Mario Carneiro (Feb 26 2019 at 11:22):

I forget who was working on that

#### Mario Carneiro (Feb 26 2019 at 11:23):

simp can't do this unassisted because the cast goes the wrong direction... It wants to get rid of up arrows not put them in

#### Scott Morrison (Feb 26 2019 at 11:24):

The lemma @[simp] lemma cast_self_eq_zero' {n : ℕ} {h : n > 0} : (n : zmod ⟨n, h⟩) = 0 :=

#### Scott Morrison (Feb 26 2019 at 11:24):

seems to work... except that the 0 ends up in the wrong version of zmod 4, somehow...

#### Scott Morrison (Feb 26 2019 at 11:24):

so afterwards rw [zero_mul] fails, but erw [zero_mul] succeeds...

#### Scott Morrison (Feb 26 2019 at 11:26):

(or rather, it _doesn't_ work in the MWE example I posted, but mysteriously does work in my bigger example!)

grah

#### Mario Carneiro (Feb 26 2019 at 11:30):

this is the main downside of zmod compared to modeq - you have to worry about positivity

#### Scott Morrison (Feb 26 2019 at 11:33):

such a nightmare... I got most of the way through our 2nd years first problem sheet, and then this blew up in my face :-)

#### Scott Morrison (Feb 26 2019 at 11:34):

Here's another MWE, where I can get a simp lemma working, but then have to erw later instead of simp:

@[simp] lemma zmod.cast_self_eq_zero' {n : ℕ} {h : n > 0} : (n : zmod ⟨n, h⟩) = 0 :=
zmod.cast_self_eq_zero

lemma bar (n : ℕ) (w : @eq (zmod 4)
1
(@distrib.to_has_add (zmod 4) (@ring.to_distrib (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4))))
(@distrib.to_has_add (zmod 4) (@ring.to_distrib (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4))))
(@distrib.to_has_add (zmod 4) (@ring.to_distrib (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4))))
(@coe nat (zmod 4)
(@coe_to_lift nat (zmod 4)
(@coe_base nat (zmod 4)
(@nat.cast_coe (zmod 4) (zmod.has_zero 4) (zmod.has_one 4)
(@ring.to_distrib (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4)))))))
(@has_mul.mul nat nat.has_mul 4 n))
1)
1)
1)) : false :=
begin
simp at w,
erw [zero_mul] at w,
simp at w,
cases w,
end


#### Kevin Buzzard (Feb 26 2019 at 11:34):

This happened to me all the time when I was doing problem sheet questions.

#### Kevin Buzzard (Feb 26 2019 at 11:35):

The Lean devs focus on theorems not examples, and sometimes examples are far harder than you'd like.

#### Mario Carneiro (Feb 26 2019 at 11:35):

the best solution is to stop doing problem sheet questions :P

I'm sold...

#### Kevin Buzzard (Feb 26 2019 at 11:35):

I know you're not interested in this aspect of Lean :-) But my students are.

#### Kevin Buzzard (Feb 26 2019 at 11:35):

As you said a day or two ago, examples are for the educators.

#### Scott Morrison (Feb 26 2019 at 11:36):

(For context, I was actually trying to write a "an undergraduate could do this" proof that there are infinitely many 4n+3 primes.)

#### Mario Carneiro (Feb 26 2019 at 11:37):

when you say "an undergraduate could do this" do you mean you wrote it in a deliberately inefficient way to find out how to recover?

#### Mario Carneiro (Feb 26 2019 at 11:37):

That's a theorem I want in mathlib btw

#### Mario Carneiro (Feb 26 2019 at 11:38):

aha, you wanted to prove that a 4n+3 prime is not equal to 1?

#### Scott Morrison (Feb 26 2019 at 11:44):

I was just proving a lemma, that a 4n+3 number has a 4n+3 prime factor:

#### Scott Morrison (Feb 26 2019 at 11:44):

https://gist.github.com/semorrison/a43a508646169efe1d1b3bda1e142140

#### Mario Carneiro (Feb 26 2019 at 11:48):

I think it would help to not call the number 4*k+3 and instead call it k' such that k' % 4 = 3

#### Mario Carneiro (Feb 26 2019 at 11:48):

or maybe k' == 3 [MOD 4]

#### Scott Morrison (Feb 26 2019 at 11:49):

or maybe (k' : zmod 4) = 1, since modeq is horrible to use :-)

#### Mario Carneiro (Feb 26 2019 at 11:49):

it's a relation between nats. This matters more than you seem to think

#### Scott Morrison (Feb 26 2019 at 11:49):

It's just that the relation is almost-but-not-actually equality

#### Scott Morrison (Feb 26 2019 at 11:50):

so you find yourself wanting to rewrite using it, but you can't

#### Mario Carneiro (Feb 26 2019 at 11:50):

You can use it in calc blocks and apply transitivity lemmas and so on

#### Mario Carneiro (Feb 26 2019 at 11:50):

but it's true, the congruences you can use are controlled

#### Mario Carneiro (Feb 26 2019 at 11:51):

(hm, overlapping meanings of "congruence" here)

(sure)

#### Mario Carneiro (Feb 26 2019 at 11:51):

when you use zmod, you have to deal with coercions and how they affect everything else

#### Mario Carneiro (Feb 26 2019 at 11:51):

it's the same problem in a different notation

#### Scott Morrison (Feb 26 2019 at 11:52):

I think it would help to not call the number 4*k+3 and instead call it k' such that k' % 4 = 3

Can you explain the motivation here? I can imagine this is worth trying, but I don't have an intuition ahead of time.

#### Mario Carneiro (Feb 26 2019 at 11:52):

you don't care about k here. it's just some multiplier

#### Mario Carneiro (Feb 26 2019 at 11:53):

So this is exposing all that structure, the 4 and the 3 and the plus, to be rearranged by simp and friends and that will be bad news

okay

#### Mario Carneiro (Feb 26 2019 at 11:54):

the point of definitions is to hide and idiomize irrelevant structure for the task at hand

#### Johan Commelin (Feb 26 2019 at 11:55):

That's a theorem I want in mathlib btw

It's a trivial corollary of Chebotarev's density theorem.

#### Mario Carneiro (Feb 26 2019 at 11:56):

oh, actually I realize I misread it now... I was thinking about another theorem about 4*k+3 primes

#### Mario Carneiro (Feb 26 2019 at 11:56):

Maybe the two square theorem? That's about 4*k+1 primes though

#### Mario Carneiro (Feb 26 2019 at 11:57):

I don't know Chebotarev's density theorem, but it also follows from Dirichlet's theorem which I have some experience with

#### Johan Commelin (Feb 26 2019 at 12:01):

Chebotarev's density theorem generalizes all the others. It's a very nice result in analytic number theory, but it's also quite hard to prove (-;
Let's do Cauchy first...

#### Patrick Massot (Feb 26 2019 at 12:16):

the best solution is to stop doing problem sheet questions :P

This was also my conclusion after reading Kevin's adventures. In my course I use only exercises designed specifically for Lean.

#### Andrew Ashworth (Feb 26 2019 at 12:25):

It is very exciting to hear about this sort of thing. So far, what do your students think of Lean and formal proofs?

#### Patrick Massot (Feb 26 2019 at 12:41):

It's hard to say. They like to pretend things are clear in their head, but they have difficulties explaining them to the machine. But actually things are not clear in their heads, and they also don't know how to explain them on paper.

#### Patrick Massot (Feb 26 2019 at 12:43):

Also I had a non-optimal start because I didn't realize how far they were from being able to understand proofs (I hadn't seen a first year student for seven years, and even back then I was teaching stuff that did not require very precise reasonning)

#### Scott Morrison (Mar 31 2019 at 09:28):

Does

def split_on {α : Type u} [decidable_eq α] (a : α) : list α → list (list α)


#### Scott Morrison (Mar 31 2019 at 09:28):

def factor {m : Type u → Type v} [monad m] {α : Type u} : list (m α) → m (list α)
| []          := return []


#### Reid Barton (Oct 22 2019 at 23:57):

dang too slow
example (a : ℕ) : ¬ (a < a - 1) := not_lt_of_ge (nat.pred_le a)

#### Kenny Lau (Oct 23 2019 at 00:55):

example (a : ℕ) : ¬ (a < a - 1) := by omega


#### Scott Morrison (Nov 09 2019 at 10:57):

I tried this problem again, using push_cast from #1464, but still can't get there:

import tactic.norm_cast
import data.zmod.basic

example (n k : ℕ) : (k : zmod (2^n - 1)) = ((k / 2^n + k % 2^n : ℕ) : zmod (2^n - 1)) :=
begin
push_cast,
congr,
convert one_mul _,
norm_cast,
conv { to_lhs, congr, congr, change 2, },
sorry
end


Anyone see how to finish this, or have an alternative suggestion to approach this in zmod land?

#### Scott Morrison (Nov 09 2019 at 10:57):

This stuff is still too awkward! :-)

#### Reid Barton (Nov 09 2019 at 15:56):

This is hard in part because of the strange definition of zmod

#### Reid Barton (Nov 09 2019 at 15:58):

You probably will have to treat n = 0 separately. Or just don't use zmod

#### Reid Barton (Nov 09 2019 at 16:03):

example (n : ℕ) (k : ℤ) : k ≡ k / 2^n + k % 2^n [ZMOD (2^n - 1)] :=
begin
transitivity,
apply int.modeq.modeq_iff_dvd.mpr,
use -(k / 2 ^ n),
set A := k / 2 ^ n,
set B := k % 2 ^ n,
ring,
end


#### Scott Morrison (May 14 2020 at 14:47):

Is

example (a b c : ℕ) (h : 0 < b) : (a + b * c) / b = a / b + c :=
begin
sorry
end


#### Reid Barton (May 14 2020 at 14:52):

lib/lean/library/init/data/nat/lemmas.lean:theorem add_mul_div_right (x y : ℕ) {z : ℕ} (H : z > 0) : (x + y * z) / z = x / z + y :=


#### Reid Barton (May 14 2020 at 14:52):

or more relevantly add_mul_div_left

#### Reid Barton (May 14 2020 at 14:53):

I'm disappointed my technique of grepping for a / b + didn't directly work

#### Jalex Stark (May 14 2020 at 15:30):

did library_search fail? if so, is it because of that hypothesis z > 0 instead of 0< z? The latter is what I'm told mathlib is supposed to prefer, so maybe we should fix this?

#### Shing Tak Lam (May 14 2020 at 15:33):

library_search finds it when i just tried it.

Also I think this lemma is in core lean, not mathlib btw.

#### Kevin Buzzard (May 14 2020 at 21:39):

The z>0 thing should still be changed though

#### Bryan Gin-ge Chen (May 14 2020 at 21:44):

More broadly, lean#200 is on fixing lint errors on the core library. We should probably hold off on tackling that in earnest until after lean#229 (Johan's big alegbra removal PR) is merged though.

#### Scott Morrison (May 15 2020 at 01:30):

I failed to find it using library_search just because I had (a + b * c) /b, rather than (a + c * b)/b. Clearly I should have tried that variation too.

#### Scott Morrison (May 15 2020 at 01:31):

library_search is aggressive enough about using apply that 0 < z and z > 0 is not an obstacle.

#### Reid Barton (May 15 2020 at 01:31):

Both versions are in the library though.

oh...

#### Scott Morrison (May 15 2020 at 01:31):

okay, I will look again.

#### Reid Barton (May 15 2020 at 01:33):

I just pasted the wrong one first

Last updated: Dec 20 2023 at 11:08 UTC