# Zulip Chat Archive

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

#### Kenny Lau (Feb 23 2019 at 10:33):

so... for nat?

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

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?

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

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 rw [nat.sub_sub, ←nat.add_sub_assoc, nat.add_sub_cancel_left], 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

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

Thanks.

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

Should probably be `protected`

as well

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

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

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

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`

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

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

That is surely proven already

#### 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 (@has_add.add (zmod 4) (@add_semigroup.to_has_add (zmod 4) (@add_comm_semigroup.to_add_semigroup (zmod 4) (zmod.add_comm_semigroup 4))) 1 (@has_add.add (zmod 4) (@add_semigroup.to_has_add (zmod 4) (@add_comm_semigroup.to_add_semigroup (zmod 4) (zmod.add_comm_semigroup 4))) 1 (@has_add.add (zmod 4) (@add_semigroup.to_has_add (zmod 4) (@add_comm_semigroup.to_add_semigroup (zmod 4) (zmod.add_comm_semigroup 4))) 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) (@distrib.to_has_add (zmod 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

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

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

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

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 (@has_add.add (zmod 4) (@distrib.to_has_add (zmod 4) (@ring.to_distrib (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4)))) (@has_add.add (zmod 4) (@distrib.to_has_add (zmod 4) (@ring.to_distrib (zmod 4) (@comm_ring.to_ring (zmod 4) (zmod.comm_ring 4)))) (@has_add.add (zmod 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) (@distrib.to_has_add (zmod 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

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

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)

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

(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

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

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

already exist in mathlib?

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

What about

def factor {m : Type u → Type v} [monad m] {α : Type u} : list (m α) → m (list α) | [] := return [] | (a :: rest) := do a ← a, rest ← factor rest, return $ (a :: rest)

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

and finally

def min {α : Type u} (l : list α) [has_lt α] [@decidable_rel α has_lt.lt] : option α := ...

#### Mario Carneiro (Mar 31 2019 at 09:45):

`split_on`

: I think not, but you haven't given the definition.`factor`

: This is`traverse`

from the traversable library, as well as`monad.sequence`

in core.`min`

: Not this particular function, but you can build it with`fold`

easily enough. Also I would probably have assumed an`le`

not an`lt`

if it were there

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

Do we want `min`

and `max`

(with `le`

, I agree) in mathlib? Or should I just stick it at the point of use (needed for a tactic).

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

`split_on`

was defined as

def split_on_aux {α : Type u} [decidable_eq α] (a : α) : list α → list α → list (list α) | [] l := [l.reverse] | (h :: t) l := if h = a then l.reverse :: (split_on_aux t []) else split_on_aux t (h :: l) def split_on {α : Type u} [decidable_eq α] (a : α) : list α → list (list α) | l := split_on_aux a l []

#### Mario Carneiro (Mar 31 2019 at 09:52):

I think `foldl1`

would be good, and you could get `min`

and `max`

and variations easily from that

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

With a few basic properties, can `split_on`

go in the library?

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

Sorry, what did you have in mind as `foldl1`

?

#### Mario Carneiro (Mar 31 2019 at 10:00):

def list.foldl1 {α} (f : α → α → α) : list α → option α | [] := none | (a::l) := some (list.foldl f a l) def list.foldr1 {α} (f : α → α → α) : list α → option α | [] := none | (a::l) := match list.foldr1 l with | none := a | (some b) := f a b end

#### Scott Morrison (Mar 31 2019 at 10:04):

Great. Why that name, though?

#### Mario Carneiro (Mar 31 2019 at 10:04):

I think it's the haskell name

#### Mario Carneiro (Mar 31 2019 at 10:04):

it means "fold at least one"

#### Mario Carneiro (Mar 31 2019 at 10:05):

Here's how you can do `split_on`

without the list postprocessing:

def split_on_aux {α : Type u} [decidable_eq α] (a : α) : list α → (list α → list α) → list (list α) | [] f := [f []] | (h :: t) f := if h = a then f [] :: split_on_aux t id else split_on_aux t (λ l, f (h :: l)) def split_on {α : Type u} [decidable_eq α] (a : α) (l : list α) : list (list α) := split_on_aux a l id

#### Scott Morrison (Mar 31 2019 at 10:07):

ta!

#### Mario Carneiro (Mar 31 2019 at 10:09):

It would also be nice to have the inverse operation (`splice`

? `riffle`

?) and prove inverse

#### Scott Morrison (Mar 31 2019 at 10:17):

working on it :-)

#### Scott Morrison (Mar 31 2019 at 10:17):

we already have `intersperse`

in core for the inverse

#### Scott Morrison (Mar 31 2019 at 10:17):

it's only a one sided inverse

#### Scott Morrison (Mar 31 2019 at 10:20):

sorry, it's `intercalate`

.

#### Scott Morrison (Mar 31 2019 at 10:20):

lemma split_on_spec {α : Type u} [decidable_eq α] (a : α) (as : list α) : list.intercalate [a] (as.split_on a) = as := sorry

#### Mario Carneiro (Mar 31 2019 at 10:25):

The inverse also holds in the other direction if you assume the intercalants have no `a`

#### Mario Carneiro (Mar 31 2019 at 10:25):

I guess there is also a `split_on`

that splits with a list argument

#### Mario Carneiro (Mar 31 2019 at 10:26):

although it's more complicated and should probably be a separate function

#### Mario Carneiro (Mar 31 2019 at 10:26):

or even a list predicate? ok I'll stop now

#### Scott Morrison (Mar 31 2019 at 10:42):

Yeah, proving the spec doesn't seem the easiest thing in the world, in any case.

#### Scott Morrison (Mar 31 2019 at 10:42):

Can I PR the def separately? I really only need it for tactics at the moment. :-)

#### Mario Carneiro (Mar 31 2019 at 12:06):

yeah, it's going in a different file anyway

#### Mario Carneiro (Mar 31 2019 at 12:07):

`data.list.defs`

#### Scott Morrison (Mar 31 2019 at 23:40):

@Mario Carneiro, I'm curious now --- why do you think the version of `split_on_aux`

that passes a function around it better than the list postprocessing version? Is it really more efficient than call `list.reverse`

? The VM still needs to evaluate all the functions you've stacked up.

#### Scott Morrison (Mar 31 2019 at 23:41):

I'm asking because proving properties seems (likely to be?) easier with the post-processing version.

#### Mario Carneiro (Mar 31 2019 at 23:41):

they are both linear time. It's hard to say

#### Mario Carneiro (Mar 31 2019 at 23:42):

You can also use `dlist`

instead of a `list -> list`

accumulator, which amounts to the same thing but has some additional constraints that are relevant for the proof

#### Scott Morrison (Mar 31 2019 at 23:44):

I see. For the sake of proofs the easiest implementation is more like: "find the position `n`

of the first `a`

, if there is one, then return `(take n) :: split_on (drop (n+1))`

.

#### Scott Morrison (Mar 31 2019 at 23:44):

That's also linear time, I think, although obviously with a worse constant.

#### Mario Carneiro (Mar 31 2019 at 23:45):

I would avoid an implementation like that because of the index manipulation

#### Mario Carneiro (Mar 31 2019 at 23:45):

(for proving things)

#### Scott Morrison (Mar 31 2019 at 23:46):

interesting, okay. In any case, I'm not planning on proving anything here; but I was considering offering it to a student.

#### Mario Carneiro (Mar 31 2019 at 23:54):

you want to do this proof by induction on the list; you should assume in the proof that the function has the form `\lam r, l ++ r`

for some `l`

, and then use append assoc and stuff to proceed to the subcase in the inductive hypothesis

#### Scott Morrison (Apr 02 2019 at 00:44):

-- Surely this is in the library? lemma foo {β : Type} [add_monoid β] (x : β) (h : ∀ y, x + y = y) : x = 0 := by simpa using h 0

#### Scott Morrison (Apr 02 2019 at 02:48):

And where do I find these?

lemma foo {a b : ℝ} (h : a + b = 0) (wa : a ≥ 0) (wb : b ≥ 0) : a = 0 := sorry lemma turkle {a : ℝ} (h : a * a = 0) : a = 0 := sorry

#### Scott Morrison (Apr 02 2019 at 02:52):

... hmm, why didn't `library_search`

find

`lemma bar {a : ℝ} : a * a ≥ 0 := mul_self_nonneg a`

#### Scott Morrison (Apr 02 2019 at 02:59):

I'm really struggling finding lemmas today:

lemma or.self {P : Prop} (h : P ∨ P) : P := by cases h; exact h

is surely already somewhere?

#### Reid Barton (Apr 02 2019 at 03:01):

`or_self`

#### Scott Morrison (Apr 02 2019 at 03:03):

ah, which you have to use as `(or_self _).1`

#### Scott Morrison (Oct 09 2019 at 09:55):

example (a b : ℕ) (h : 0 < b) : a = (a / b) * b + (a % b) := sorry

?

#### Mario Carneiro (Oct 09 2019 at 09:58):

`nat.mod_add_div`

#### Mario Carneiro (Oct 09 2019 at 09:59):

we should probably make all four variations on this, people never know which one to expect

#### Mario Carneiro (Oct 09 2019 at 09:59):

you don't need the side condition

#### Scott Morrison (Oct 09 2019 at 10:01):

maybe all 8 variations... I tried swapping both the `*`

and the `+`

, but didn't think of reversing the `=`

...

#### Scott Morrison (Oct 09 2019 at 10:02):

I really should add that to `library_search`

.

#### Mario Carneiro (Oct 09 2019 at 10:02):

that's standard mathlib practice

#### Mario Carneiro (Oct 09 2019 at 10:02):

I thought that commuting was already done by `library_search`

?

#### Scott Morrison (Oct 09 2019 at 10:07):

no, not yet

#### Scott Morrison (Oct 09 2019 at 10:07):

it will apply either direction of an `iff`

#### Scott Morrison (Oct 09 2019 at 10:08):

I think if it fails, it should just call `symmetry`

and try again...

#### Scott Morrison (Oct 09 2019 at 10:09):

Ooof, just to be confusing we have `nat.mod_add_div`

, but `euclidean_domain.div_add_mod`

...

#### Scott Morrison (Oct 09 2019 at 10:11):

and we have helpful lemmas like

@[simp] theorem mod_add_mod (m n k : ℤ) : (m % n + k) % n = (m + k) % n @[simp] theorem add_mod_mod (m n k : ℤ) : (m + n % k) % k = (m + n) % k

but without the corresponding versions on `nat`

.

#### Scott Morrison (Oct 09 2019 at 10:12):

nor apparently the multiplicative versions anywhere

#### Mario Carneiro (Oct 09 2019 at 10:19):

Most of those kinds of theorems are hidden behind the `modeq`

definition

#### Mario Carneiro (Oct 09 2019 at 10:19):

it makes more sense to view that as a congruence lemma for `nat.modeq`

#### Scott Morrison (Oct 09 2019 at 11:29):

I have never managed to do anything under `modeq`

. The thing I wanted to prove was

lemma foo (n k : ℕ) : k ≡ ((k / 2^n) + (k % 2^n)) [MOD 2^n - 1] :=

using the following proof:

- rewrite the
`k`

on the left hand side using`k = (k / 2^n) * 2^n + k % 2^n`

- now replace the
`* 2^n`

with`* 1`

, since we are working mod`2^n - 1`

. - simplify away
`(k / 2^n) * 1`

to`k / 2^n`

, and we're done.

But once we're inside the `modeq`

I can't use `simp`

, or `rw`

, or `conv`

, and so I don't know how to express this proof... :-(

#### Chris Hughes (Oct 09 2019 at 11:29):

work with `zmod`

instead?

#### Johan Commelin (Oct 09 2019 at 11:33):

I agree that we need to be able to write nice `calc`

style proofs working modulo some ideal/element.

#### Johan Commelin (Oct 09 2019 at 11:34):

I remember that this was quite painful when I was writing Witt vectors.

#### Johan Commelin (Oct 09 2019 at 11:35):

You need to remind Lean all the time that the quotient map is a ring hom. No content at all. Should be transparent.

#### Mario Carneiro (Oct 09 2019 at 11:47):

import data.nat.modeq lemma foo (n k : ℕ) : k ≡ ((k / 2^n) + (k % 2^n)) [MOD 2^n - 1] := begin conv {to_rhs, rw [← nat.mod_add_div k (2^n), add_comm]}, refine nat.modeq.modeq_add _ (by refl), conv {to_rhs, skip, rw ← one_mul (k/2^n)}, refine nat.modeq.modeq_mul _ (by refl), symmetry, rw [nat.modeq.modeq_iff_dvd, int.coe_nat_sub], exact nat.pow_pos dec_trivial _ end

#### Mario Carneiro (Oct 09 2019 at 11:48):

that basically follows your proof sketch

#### Scott Morrison (Oct 09 2019 at 22:09):

Thanks.

#### Scott Morrison (Oct 22 2019 at 23:54):

A better proof of

example (a : ℕ) : ¬ (a < a - 1) := begin intro h₁, have h₂ : a - 1 ≤ a, { erw nat.pred_le_iff, exact nat.le_succ _ }, exact lt_irrefl _ (lt_of_lt_of_le h₁ h₂), end

?

#### Mario Carneiro (Oct 22 2019 at 23:56):

example (a : ℕ) : ¬ (a < a - 1) := not_lt_of_ge $ nat.sub_le _ _

#### 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 conv { to_lhs, rw [← nat.mod_add_div k (2^n), add_comm] }, 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, { rw [← int.mod_add_div k (2^n), add_comm] }, 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
```

readily available somewhere?

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

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

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: May 14 2021 at 21:11 UTC