nat.eq_div_of_mul_eq

Stream: Is there code for X?

[Kevin Buzzard]

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]

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]

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]

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]

actually there are closer matches too, it looks like

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

ironically the proof is longer because the names are more cumbersome

[Mario Carneiro]

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]

and then another 8 for the biconditional version

[Kevin Buzzard]

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

[Kevin Buzzard]

but I absolutely take your point.

[Mario Carneiro]

the biconditional assumes divisibility

[Mario Carneiro]

pretty sure it's already available

[Kevin Buzzard]

yes I ran into versions of it

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I also had \ne 0 and not 0 <

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

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

[Johan Commelin]

Mario Carneiro said:

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

Isn't that tactic called suggest?

[Mario Carneiro]

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]

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]

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

[Scott Morrison]

It would be good to explore other orderings.

[Kevin Buzzard]

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]

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]

now you're thinking like a CS guy

[Mario Carneiro]

yay for less magical thinking and more questioning "how"

[Reid Barton]

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

[Kevin Buzzard]

is ML machine learning or something to do with caml?

[Reid Barton]

machine learning

[Kevin Buzzard]

I watched someone writing code in Isabelle/HOL once

[Kevin Buzzard]

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]

where's the fun in that?

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

(deleted)