arithmetic hell

Stream: new members

[Jalex Stark]

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]

Try field_simp [ha, hb, hc], ring

[Jalex Stark]

beautiful

[Kevin Buzzard]

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

[Kevin Buzzard]

there are different little tricks for different situations

[Jalex Stark]

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

[Kevin Buzzard]

I don't think so

[Jalex Stark]

okay good that doesn't sound fun

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Jalex Stark]

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]

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]

(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]

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

[Kevin Buzzard]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Johan Commelin]

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.