Stream: Is there code for X?

Topic: nat.eq_div_of_mul_eq

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


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


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

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

Mario Carneiro (Apr 16 2020 at 13:09):

actually there are closer matches too, it looks like

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


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

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 :-/

Mario Carneiro (Apr 16 2020 at 13:12):

ironically the proof is longer because the names are more cumbersome

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

Mario Carneiro (Apr 16 2020 at 13:13):

and then another 8 for the biconditional version

Kevin Buzzard (Apr 16 2020 at 13:14):

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

Kevin Buzzard (Apr 16 2020 at 13:14):

but I absolutely take your point.

Mario Carneiro (Apr 16 2020 at 13:14):

the biconditional assumes divisibility

Kevin Buzzard (Apr 16 2020 at 13:14):

yes I ran into versions of it

Mario Carneiro (Apr 16 2020 at 13:15):

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

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

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

Kevin Buzzard (Apr 16 2020 at 13:16):

I also had \ne 0 and not 0 <

Mario Carneiro (Apr 16 2020 at 13:17):

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

Mario Carneiro (Apr 16 2020 at 13:18):

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

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.

Mario Carneiro (Apr 16 2020 at 13:22):

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

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?

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

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

Scott Morrison (Apr 16 2020 at 13:53):

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

Scott Morrison (Apr 16 2020 at 13:54):

It would be good to explore other orderings.

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.

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.

Mario Carneiro (Apr 16 2020 at 14:04):

now you're thinking like a CS guy

Mario Carneiro (Apr 16 2020 at 14:06):

yay for less magical thinking and more questioning "how"

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

Kevin Buzzard (Apr 16 2020 at 14:07):

is ML machine learning or something to do with caml?

machine learning

Kevin Buzzard (Apr 16 2020 at 14:08):

I watched someone writing code in Isabelle/HOL once

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

Kevin Buzzard (Apr 16 2020 at 14:09):

where's the fun in that?

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.

Scott Morrison (Apr 16 2020 at 14:09):

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

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.

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.

Kevin Buzzard (Apr 16 2020 at 14:24):

(deleted)

Last updated: May 16 2021 at 05:21 UTC