Stream: new members

Topic: arithmetic hell

Jalex Stark (May 15 2020 at 21:15):

Here's something where a very slight extension of abel to groups with 0 would do the trick

example
{a b c : ℚ}
(ha : a ≠ 0)
(hb : b ≠ 0)
(hc : c ≠ 0) :
a = c * (b * (a * (b * (c))⁻¹)) := begin
ring,
end


Sebastien Gouezel (May 15 2020 at 21:19):

Try field_simp [ha, hb, hc], ring

beautiful

Kevin Buzzard (May 15 2020 at 21:20):

It has got to the point where you have to know what you're doing to solve this sort of thing

Kevin Buzzard (May 15 2020 at 21:21):

there are different little tricks for different situations

Jalex Stark (May 15 2020 at 21:22):

should I be doing things like "read the implementation of relevant tactics" to come up with these ideas on my own?

I don't think so

Jalex Stark (May 15 2020 at 21:22):

okay good that doesn't sound fun

Kevin Buzzard (May 15 2020 at 21:22):

It would only be a slight exaggeration to say that I have never read a line of meta code in my life

Bryan Gin-ge Chen (May 15 2020 at 21:23):

It's still a bit unwieldy, but you can filter the tactic docs by tag.

Kevin Buzzard (May 15 2020 at 21:23):

I do just what you're doing -- I post problems I can't solve with the skillset I have, someone points out a new tactic which I hadn't fully understood before, I read the docstring, and then I feel like I've levelled up.

Bryan Gin-ge Chen (May 15 2020 at 21:23):

In this case, field_simp is the 3rd thing that appears when you select "simplification".

Kevin Buzzard (May 15 2020 at 21:24):

For over a year I've known that ring does things without any division and when there is division you have to manually clear the denominators. Then someone wrote a "clear denominators" tactic and because I had done it manually so many times I eagerly added it to my skillset.

Jalex Stark (May 15 2020 at 21:25):

and the clear denominators tactic is exactly field_simp passed with lemmas for each of your denominators being nonzero?

Kevin Buzzard (May 15 2020 at 21:25):

The real power of field_simp is that you can give it the parameters such as ha. Your question was made for field_simp really. A year ago it would have been far more tedious to solve.

Jalex Stark (May 15 2020 at 21:26):

mathematically this feels the same as lifting them all to units ℚ and then using abel

Kevin Buzzard (May 15 2020 at 21:28):

In your example yes, but there could have been additions and Sebastien's proof would still have worked

Jalex Stark (May 15 2020 at 21:36):

apparently you can't literally do it with abel

instance
{α : Type}
[group_with_zero α] :
can_lift α (units α) :=
begin
refine {coe := coe, cond := λ x, x ≠ 0, prf := _},
intros x hx,
exact (units.exists_iff_ne_zero x).mpr hx,
end

example
{a b c : ℚ}
(ha : a ≠ 0)
(hb : b ≠ 0)
(hc : c ≠ 0) :
a = c * (b * (a * (b * (c))⁻¹)) := begin
lift a to units ℚ using ha,
lift b to units ℚ using hb,
lift c to units ℚ using hc,
field_simp, ring,
end


Jalex Stark (May 15 2020 at 21:36):

also I learned that can_lift is the instance you want to prove if you're trying to make a new use of lift, not has_lift

Jalex Stark (May 15 2020 at 21:37):

(obviously this proof is worse than field_simp with arguments, but it's helpful to me to know that this is possible / easy)

Jalex Stark (May 15 2020 at 21:39):

also i love that lift a to units ℚ using ha "uses" ha in the sense of clear ha

Kevin Buzzard (May 15 2020 at 21:40):

It's nice to see a tactic tidying up after itself

Jalex Stark (May 15 2020 at 21:42):

i was looking for a broom but the closest I found was :shower:

Jalex Stark (May 15 2020 at 21:42):

it would probably be a bad thing for most tactics to tidy up after themselves though

Johan Commelin (May 16 2020 at 04:13):

Jalex Stark said:

also I learned that can_lift is the instance you want to prove if you're trying to make a new use of lift, not has_lift

Yup... has_lift already existed when the lift tactic was written by Floris.

Last updated: May 15 2021 at 00:39 UTC