Zulip Chat Archive

Stream: new members

Topic: arithmetic hell


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

view this post on Zulip Sebastien Gouezel (May 15 2020 at 21:19):

Try field_simp [ha, hb, hc], ring

view this post on Zulip Jalex Stark (May 15 2020 at 21:20):

beautiful

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

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

there are different little tricks for different situations

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

view this post on Zulip Kevin Buzzard (May 15 2020 at 21:22):

I don't think so

view this post on Zulip Jalex Stark (May 15 2020 at 21:22):

okay good that doesn't sound fun

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

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

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

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

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

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

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

view this post on Zulip Jalex Stark (May 15 2020 at 21:26):

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (May 15 2020 at 21:40):

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

view this post on Zulip Jalex Stark (May 15 2020 at 21:42):

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

view this post on Zulip Jalex Stark (May 15 2020 at 21:42):

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

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