Zulip Chat Archive

Stream: new members

Topic: help finding a lemma


view this post on Zulip Scott Morrison (Feb 23 2019 at 10:33):

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

view this post on Zulip Kenny Lau (Feb 23 2019 at 10:33):

so... for nat?

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:34):

Sure.

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:34):

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

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:36):

Is this meant to be called sub_sub_sub_right or something?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:49):

Sure! But does it exist already?

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:49):

Surely?

view this post on Zulip Chris Hughes (Feb 23 2019 at 10:50):

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

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:51):

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

view this post on Zulip Chris Hughes (Feb 23 2019 at 10:51):

nat.sub_le_sub_left is there.

view this post on Zulip Chris Hughes (Feb 23 2019 at 10:52):

sorry right

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:59):

Thanks.

view this post on Zulip Chris Hughes (Feb 23 2019 at 10:59):

Should probably be protected as well

view this post on Zulip Scott Morrison (Feb 23 2019 at 10:59):

Why is that?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Feb 23 2019 at 11:13):

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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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"?

view this post on Zulip Kevin Buzzard (Feb 23 2019 at 11:18):

linarith

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 23 2019 at 11:20):

you could also prove a < a with lt_of_lt_of_le I guess

view this post on Zulip Mario Carneiro (Feb 23 2019 at 11:42):

The two lists are equal thing is eq_of_sorted_of_perm

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Feb 23 2019 at 11:52):

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

view this post on Zulip Kevin Buzzard (Feb 23 2019 at 11:53):

Oh I see!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 23 2019 at 22:44):

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

view this post on Zulip Chris Hughes (Feb 23 2019 at 22:46):

nat.pred_le_iff

view this post on Zulip Scott Morrison (Feb 23 2019 at 22:50):

oh, but that's still only half of it

view this post on Zulip Scott Morrison (Feb 23 2019 at 22:51):

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

view this post on Zulip Chris Hughes (Feb 23 2019 at 22:55):

Yeah, it's pred_le not le_pred

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 24 2019 at 03:54):

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

view this post on Zulip Mario Carneiro (Feb 24 2019 at 03:55):

also, stop using ge and gt so much

view this post on Zulip Scott Morrison (Feb 24 2019 at 04:12):

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

view this post on Zulip 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 :=?

view this post on Zulip 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".)

view this post on Zulip Scott Morrison (Feb 24 2019 at 04:30):

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

view this post on Zulip Scott Morrison (Feb 24 2019 at 04:30):

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

view this post on Zulip Andrew Ashworth (Feb 24 2019 at 04:44):

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

view this post on Zulip Scott Morrison (Feb 24 2019 at 04:46):

Thanks, @Andrew Ashworth.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:15):

I would look into data/nat/modeq.lean

view this post on Zulip Scott Morrison (Feb 26 2019 at 10:37):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 10:37):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 10:37):

similarly for add_mod.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:42):

It follows from some stuff about modeq

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:43):

it is roughly modeq_mul mod_modeq mod_modeq

view this post on Zulip Scott Morrison (Feb 26 2019 at 10:43):

okay, I see.

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:43):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 26 2019 at 10:44):

has someone done N/nZ and Z/nZ?

view this post on Zulip Patrick Massot (Feb 26 2019 at 10:44):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:44):

there is a type for Z/nZ

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:44):

like Patrick said

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:45):

zmod

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:45):

That is surely proven already

view this post on Zulip Mario Carneiro (Feb 26 2019 at 10:46):

zmod.eq_iff_modeq_nat

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:01):

I think you can change 4 with 0

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:02):

there's probably a better way though

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:02):

cast_self_eq_zero?

view this post on Zulip 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+

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:04):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:07):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:08):

Or just go back to nats from this point

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:08):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:17):

woah... okay.

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:17):

Is there any way we can make that more ergonomic?

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:18):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:20):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:22):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:22):

I forget who was working on that

view this post on Zulip 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

view this post on Zulip 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 :=

view this post on Zulip 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...

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:24):

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

view this post on Zulip 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!)

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:26):

grah

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:30):

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

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:34):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:35):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:35):

I'm sold...

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:35):

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

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 11:35):

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

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:37):

That's a theorem I want in mathlib btw

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:38):

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

view this post on Zulip 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:

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:44):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:48):

or maybe k' == 3 [MOD 4]

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:49):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:49):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:49):

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

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:50):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:50):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:50):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:51):

(hm, overlapping meanings of "congruence" here)

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:51):

(sure)

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:51):

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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:51):

it's the same problem in a different notation

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:52):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 26 2019 at 11:54):

okay

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:54):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 11:56):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Mar 31 2019 at 09:28):

Does

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

already exist in mathlib?

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Mar 31 2019 at 09:31):

and finally

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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 []

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 31 2019 at 09:53):

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

view this post on Zulip Scott Morrison (Mar 31 2019 at 09:54):

Sorry, what did you have in mind as foldl1?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:04):

Great. Why that name, though?

view this post on Zulip Mario Carneiro (Mar 31 2019 at 10:04):

I think it's the haskell name

view this post on Zulip Mario Carneiro (Mar 31 2019 at 10:04):

it means "fold at least one"

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:07):

ta!

view this post on Zulip Mario Carneiro (Mar 31 2019 at 10:09):

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

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:17):

working on it :-)

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:17):

we already have intersperse in core for the inverse

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:17):

it's only a one sided inverse

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:20):

sorry, it's intercalate.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 10:25):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 10:25):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 10:26):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 10:26):

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

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:42):

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

view this post on Zulip Scott Morrison (Mar 31 2019 at 10:42):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 12:06):

yeah, it's going in a different file anyway

view this post on Zulip Mario Carneiro (Mar 31 2019 at 12:07):

data.list.defs

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 31 2019 at 23:41):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 23:41):

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

view this post on Zulip 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

view this post on Zulip 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)).

view this post on Zulip Scott Morrison (Mar 31 2019 at 23:44):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 23:45):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 23:45):

(for proving things)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Apr 02 2019 at 03:01):

or_self

view this post on Zulip Scott Morrison (Apr 02 2019 at 03:03):

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

view this post on Zulip Scott Morrison (Oct 09 2019 at 09:55):

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

?

view this post on Zulip Mario Carneiro (Oct 09 2019 at 09:58):

nat.mod_add_div

view this post on Zulip Mario Carneiro (Oct 09 2019 at 09:59):

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

view this post on Zulip Mario Carneiro (Oct 09 2019 at 09:59):

you don't need the side condition

view this post on Zulip 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 =...

view this post on Zulip Scott Morrison (Oct 09 2019 at 10:02):

I really should add that to library_search.

view this post on Zulip Mario Carneiro (Oct 09 2019 at 10:02):

that's standard mathlib practice

view this post on Zulip Mario Carneiro (Oct 09 2019 at 10:02):

I thought that commuting was already done by library_search?

view this post on Zulip Scott Morrison (Oct 09 2019 at 10:07):

no, not yet

view this post on Zulip Scott Morrison (Oct 09 2019 at 10:07):

it will apply either direction of an iff

view this post on Zulip Scott Morrison (Oct 09 2019 at 10:08):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 09 2019 at 10:12):

nor apparently the multiplicative versions anywhere

view this post on Zulip Mario Carneiro (Oct 09 2019 at 10:19):

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

view this post on Zulip Mario Carneiro (Oct 09 2019 at 10:19):

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

view this post on Zulip 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:

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

view this post on Zulip Chris Hughes (Oct 09 2019 at 11:29):

work with zmod instead?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 09 2019 at 11:34):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 09 2019 at 11:48):

that basically follows your proof sketch

view this post on Zulip Scott Morrison (Oct 09 2019 at 22:09):

Thanks.

view this post on Zulip 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

?

view this post on Zulip Mario Carneiro (Oct 22 2019 at 23:56):

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

view this post on Zulip Reid Barton (Oct 22 2019 at 23:57):

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

view this post on Zulip Kenny Lau (Oct 23 2019 at 00:55):

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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Nov 09 2019 at 10:57):

This stuff is still too awkward! :-)

view this post on Zulip Reid Barton (Nov 09 2019 at 15:56):

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

view this post on Zulip Reid Barton (Nov 09 2019 at 15:58):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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 :=

view this post on Zulip Reid Barton (May 14 2020 at 14:52):

or more relevantly add_mul_div_left

view this post on Zulip Reid Barton (May 14 2020 at 14:53):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 14 2020 at 21:39):

The z>0 thing should still be changed though

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 15 2020 at 01:31):

Both versions are in the library though.

view this post on Zulip Scott Morrison (May 15 2020 at 01:31):

oh...

view this post on Zulip Scott Morrison (May 15 2020 at 01:31):

okay, I will look again.

view this post on Zulip Reid Barton (May 15 2020 at 01:33):

I just pasted the wrong one first


Last updated: May 14 2021 at 21:11 UTC