Zulip Chat Archive

Stream: Is there code for X?

Topic: nat.eq_div_of_mul_eq


view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:05):

Is this missing or is my search-fu just weak today?

theorem nat.eq_div_of_mul_eq (a b c : ) : c  0  a * c = b  a = b / c :=
begin
  intros hc hb,
  rw hb,
  rw mul_comm,
  symmetry,
  apply nat.mul_div_cancel_left,
  exact nat.pos_of_ne_zero hc
end

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:07):

theorem nat.eq_div_of_mul_eq (a b c : ) (h : c  0) (e : a * c = b) : a = b / c :=
e  (nat.mul_div_cancel _ (nat.pos_of_ne_zero h)).symm

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:08):

It's not an exact match, but once you get rid of the equality assumption it's essentially just nat.mul_div_cancel

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:09):

Does this go in data.nat.basic or is there a reason it's not there? Often for things that are true for rings/fields/whatever and nat, the general result is in the root namespace and then nat has its own version

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:09):

actually there are closer matches too, it looks like

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:10):

theorem nat.eq_div_of_mul_eq (a b c : ) : c  0  a * c = b  a = b / c :=
λ hc hb, (nat.div_eq_of_eq_mul_left (nat.pos_of_ne_zero hc) hb.symm).symm

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:11):

I think most of these theorems are normalized with the operation on the left side of the equality

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:11):

nat.div_eq_of_eq_mul_left was what I was missing -- I searched for eq_div :-/

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:12):

ironically the proof is longer because the names are more cumbersome

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:13):

We could have more variations, but I think there is something like 8 versions of just this one theorem if you commute the two equalities and the multiplication

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:13):

and then another 8 for the biconditional version

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:14):

the biconditional isn't true for nat because of CS division

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:14):

but I absolutely take your point.

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:14):

the biconditional assumes divisibility

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:14):

pretty sure it's already available

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:14):

yes I ran into versions of it

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:15):

(in general the biconditional assumes whatever it needs to to make it true)

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:15):

What caught me out is that eq_div gave me some positive hits, which made me not look for div_eq

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:16):

we could try making library_search find these but there are a lot of axes of variation

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:16):

I also had \ne 0 and not 0 <

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:17):

I think that most nat theorems try to use 0 < consistently but I could be wrong

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:18):

of course there are theorems like pos_iff_ne_zero to make it not matter which

view this post on Zulip Scott Morrison (Apr 16 2020 at 13:22):

Kevin Buzzard said:

I also had \ne 0 and not 0 <

This is the top of my list for library_search working harder. It's trivial to implement, but a matter of testing performance.

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:22):

What about getting hits even if you get some assumptions wrong or missing?

view this post on Zulip Johan Commelin (Apr 16 2020 at 13:40):

Mario Carneiro said:

What about getting hits even if you get some assumptions wrong or missing?

Isn't that tactic called suggest?

view this post on Zulip Mario Carneiro (Apr 16 2020 at 13:41):

Possibly, but I think it is important to also look at hypotheses and score more highly theorems that don't just match everything

view this post on Zulip Scott Morrison (Apr 16 2020 at 13:52):

suggest returns everything (up to a limit, default 50) that applys against the goal, and sorts the results by (number of remaining goals, number of local hypotheses used to fill arguments).

view this post on Zulip Scott Morrison (Apr 16 2020 at 13:53):

(preferring, of course, matches that leave _few_ remaining goals, and use _many_ local hypotheses)

view this post on Zulip Scott Morrison (Apr 16 2020 at 13:54):

It would be good to explore other orderings.

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 13:59):

Just watching the whole library_search thing evolve over time makes it clear that it's a much harder problem than I had initially realised.

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 14:00):

Like any tactic, I guess you have to decide what it can and can't do, and then make it do what it's supposed to do, but with library_search there seem to be so many near-misses that it looks almost impossible to axiomatise what tricks you actually want it to know.

view this post on Zulip Mario Carneiro (Apr 16 2020 at 14:04):

now you're thinking like a CS guy

view this post on Zulip Mario Carneiro (Apr 16 2020 at 14:06):

yay for less magical thinking and more questioning "how"

view this post on Zulip Reid Barton (Apr 16 2020 at 14:07):

now all you need to do is learn ML and go back to magical thinking and not knowing how

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 14:07):

is ML machine learning or something to do with caml?

view this post on Zulip Reid Barton (Apr 16 2020 at 14:08):

machine learning

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 14:08):

I watched someone writing code in Isabelle/HOL once

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 14:08):

and every now and again they'd have some little lemma of the kind which I find quite fun to prove, and they hit it with a hammer and then went to do something else for 5 minutes

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 14:09):

where's the fun in that?

view this post on Zulip Scott Morrison (Apr 16 2020 at 14:09):

apply is so incredibly fast that we can actually throw a lot of extra lemmas into the solve_by_elim step in suggest (i.e. apply local hypotheses after applying the lemma from the library), as long as we're careful that they are lemmas that cause "linear" (or maybe even quadratic, with tight depth bounds) growth in the time solve_by_elim spends. As long as they all "use up" something in the goal they are basically okay.

view this post on Zulip Scott Morrison (Apr 16 2020 at 14:09):

So certainly things like getting between \ne 0 and 0 < goals is plausible.

view this post on Zulip Scott Morrison (Apr 16 2020 at 14:11):

and it's all set up to add extra lemmas in. solve_by_elim is already very configurable, and @Lucas Allen's PR #2429 (which unfortunately mangled a merge at the moment) exposes that configurability to the user of suggest or library_search.

view this post on Zulip Scott Morrison (Apr 16 2020 at 14:12):

So it's relatively easy to start experimenting with plausible lemmas to add. If we're confortable adding some to "the default set" it will just be a matter of tagging them with @[suggest] or something similar.

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 14:24):

(deleted)


Last updated: May 16 2021 at 05:21 UTC