help finding a lemma

Stream: new members

[Scott Morrison]

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

[Kenny Lau]

so... for nat?

[Scott Morrison]

Sure.

[Scott Morrison]

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

[Scott Morrison]

Is this meant to be called sub_sub_sub_right or something?

[Scott Morrison]

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

[Chris Hughes]

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

[Scott Morrison]

Sure! But does it exist already?

[Scott Morrison]

Surely?

[Chris Hughes]

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

[Scott Morrison]

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

[Chris Hughes]

nat.sub_le_sub_left is there.

[Chris Hughes]

sorry right

[Scott Morrison]

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]

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

[Scott Morrison]

Thanks.

[Chris Hughes]

Should probably be protected as well

[Scott Morrison]

Why is that?

[Kevin Buzzard]

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]

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

[Scott Morrison]

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]

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]

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]

linarith

[Kevin Buzzard]

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]

you could also prove a < a with lt_of_lt_of_le I guess

[Mario Carneiro]

The two lists are equal thing is eq_of_sorted_of_perm

[Scott Morrison]

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

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

[Kevin Buzzard]

Oh I see!

[Mario Carneiro]

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

[Rob Lewis]

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]

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

[Chris Hughes]

nat.pred_le_iff

[Scott Morrison]

oh, but that's still only half of it

[Scott Morrison]

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

[Chris Hughes]

Yeah, it's pred_le not le_pred

[Scott Morrison]

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]

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

[Mario Carneiro]

also, stop using ge and gt so much

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Andrew Ashworth]

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

[Scott Morrison]

Thanks, @Andrew Ashworth.

[Jesse Michael Han]

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]

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

[Patrick Massot]

I would look into data/nat/modeq.lean

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

similarly for add_mod.

[Mario Carneiro]

It follows from some stuff about modeq

[Mario Carneiro]

it is roughly modeq_mul mod_modeq mod_modeq

[Scott Morrison]

okay, I see.

[Patrick Massot]

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

[Scott Morrison]

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

[Scott Morrison]

has someone done N/nZ and Z/nZ?

[Patrick Massot]

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

[Mario Carneiro]

there is a type for Z/nZ

[Mario Carneiro]

like Patrick said

[Mario Carneiro]

zmod

[Mario Carneiro]

That is surely proven already

[Mario Carneiro]

zmod.eq_iff_modeq_nat

[Scott Morrison]

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]

I think you can change 4 with 0

[Mario Carneiro]

there's probably a better way though

[Mario Carneiro]

cast_self_eq_zero?

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

Or just go back to nats from this point

[Scott Morrison]

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

[Scott Morrison]

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]

this works:

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

[Scott Morrison]

woah... okay.

[Scott Morrison]

Is there any way we can make that more ergonomic?

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

I forget who was working on that

[Mario Carneiro]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

grah

[Mario Carneiro]

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

[Scott Morrison]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Scott Morrison]

I'm sold...

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

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]

That's a theorem I want in mathlib btw

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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]

or maybe k' == 3 [MOD 4]

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

(hm, overlapping meanings of "congruence" here)

[Scott Morrison]

(sure)

[Mario Carneiro]

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

[Mario Carneiro]

it's the same problem in a different notation

[Scott Morrison]

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]

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

[Mario Carneiro]

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]

okay

[Mario Carneiro]

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

[Johan Commelin]

That's a theorem I want in mathlib btw

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

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]

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]

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]

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]

Does

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

already exist in mathlib?

[Scott Morrison]

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]

and finally

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

[Mario Carneiro]

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

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]

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]

I think foldl1 would be good, and you could get min and max and variations easily from that

[Scott Morrison]

With a few basic properties, can split_on go in the library?

[Scott Morrison]

Sorry, what did you have in mind as foldl1?

[Mario Carneiro]

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]

Great. Why that name, though?

[Mario Carneiro]

I think it's the haskell name

[Mario Carneiro]

it means "fold at least one"

[Mario Carneiro]

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]

ta!

[Mario Carneiro]

It would also be nice to have the inverse operation (splice? riffle?) and prove inverse

[Scott Morrison]

working on it :-)

[Scott Morrison]

we already have intersperse in core for the inverse

[Scott Morrison]

it's only a one sided inverse

[Scott Morrison]

sorry, it's intercalate.

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

I guess there is also a split_on that splits with a list argument

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

yeah, it's going in a different file anyway

[Mario Carneiro]

data.list.defs

[Scott Morrison]

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

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

(for proving things)

[Scott Morrison]

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

[Mario Carneiro]

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]

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

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]

... hmm, why didn't library_search find
lemma bar {a : ℝ} : a * a ≥ 0 := mul_self_nonneg a

[Scott Morrison]

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]

or_self

[Scott Morrison]

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

[Scott Morrison]

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

?

[Mario Carneiro]

nat.mod_add_div

[Mario Carneiro]

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

[Mario Carneiro]

you don't need the side condition

[Scott Morrison]

maybe all 8 variations... I tried swapping both the * and the +, but didn't think of reversing the =...

[Scott Morrison]

I really should add that to library_search.

[Mario Carneiro]

that's standard mathlib practice

[Mario Carneiro]

I thought that commuting was already done by library_search?

[Scott Morrison]

no, not yet

[Scott Morrison]

it will apply either direction of an iff

[Scott Morrison]

I think if it fails, it should just call symmetry and try again...

[Scott Morrison]

Ooof, just to be confusing we have nat.mod_add_div, but euclidean_domain.div_add_mod...

[Scott Morrison]

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]

nor apparently the multiplicative versions anywhere

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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:

1. rewrite the k on the left hand side using k = (k / 2^n) * 2^n + k % 2^n
2. now replace the * 2^n with * 1, since we are working mod 2^n - 1.
3. 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]

work with zmod instead?

[Johan Commelin]

I agree that we need to be able to write nice calc style proofs working modulo some ideal/element.

[Johan Commelin]

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

[Johan Commelin]

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]

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]

that basically follows your proof sketch

[Scott Morrison]

Thanks.

[Scott Morrison]

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]

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

[Reid Barton]

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

[Kenny Lau]

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

[Scott Morrison]

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]

This stuff is still too awkward! :-)

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

Is

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

readily available somewhere?

[Reid Barton]

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]

or more relevantly add_mul_div_left

[Reid Barton]

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

[Jalex Stark]

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]

library_search finds it when i just tried it.

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

[Kevin Buzzard]

The z>0 thing should still be changed though

[Bryan Gin-ge Chen]

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]

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]

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

[Reid Barton]

Both versions are in the library though.

[Scott Morrison]

oh...

[Scott Morrison]

okay, I will look again.

[Reid Barton]

I just pasted the wrong one first