Tactics for noncommutative rings

Stream: new members

[Heather Macbeth]

In a commutative ring, I can prove identities using the ring tactic:

import tactic.ring
variables {α : Type*} [comm_ring α]

example (a₁ b₁ a₂ b₂ : α) : a₁ * b₁ - a₂ * b₂ = a₁ * (b₁ - b₂) + (a₁ - a₂) * b₂ :=
begin
    ring,
end

The above identity actually holds in noncommutative rings too. The ring tactic doesn't seem to be defined for such rings, but is there a way to have ring spit out the proof it came up with in the commutative case, so that I can re-use it in the noncommutative case?

[Bryan Gin-ge Chen]

I don't think so. The proof it comes up with might use identities that don't hold for noncommutative rings.

[Heather Macbeth]

That's true. But can I get a trace on what ring did anyway, just in case it did it the efficient way (not using the extra hypotheses)?

[Mario Carneiro]

It won't work

[Jalex Stark]

I think if ring did supply traces it would likely be through ring?, e.g. tidy and tidy? do this

[Jalex Stark]

(which it doesn't, I think)

[Mario Carneiro]

the proof ring comes up with is guaranteed not to work for noncommutative rings

[Mario Carneiro]

because the normal form explicitly depends on typeclasses that require commutativity

[Heather Macbeth]

That's unfortunate, but good to know.

[Mario Carneiro]

You might be able to use abel to do the proof instead

[Heather Macbeth]

Out of interest, can I get a trace anyway?

[Mario Carneiro]

with simp to work on monomials

[Mario Carneiro]

sure, you can #print any proof to see it

[Heather Macbeth]

Ah, thanks, that's new to me!

[Heather Macbeth]

abel seems also to apply only to commutative rings?

[Jalex Stark]

variables {α : Type*} [comm_ring α]
example (a₁ b₁ a₂ b₂ : α) : a₁ * b₁ - a₂ * b₂ = a₁ * (b₁ - b₂) + (a₁ - a₂) * b₂ :=
begin
rw [mul_sub, sub_mul],
abel,
end

[Jalex Stark]

abel applies to additive groups

[Jalex Stark]

so if the human deals with multiplication then abel can do the addition

[Jalex Stark]

how do you #print the ring proof?

[Mario Carneiro]

You have to use theorem T instead of example, and then #print T afterward

[Jalex Stark]

thanks!

[Jalex Stark]

(i should have figured that out, sorry)

[Mario Carneiro]

Indeed, a really simple poor man's noncomm_ring is simp only [add_mul, mul_add, sub_eq_add_neg, neg_mul, mul_neg]; abel

[Kevin Buzzard]

Perhaps noncommutative rings are easier to work with. What happens if you just apply distributivity until you can't, then apply associativity until you can't, and then use something like ac_refl?

[Kevin Buzzard]

Yeah, what Mario just said

[Mario Carneiro]

simp will almost work to close abel goals, except that it isn't smart enough to get negatives next to positives

[Jalex Stark]

Here the second proof works but the first doesn't

import tactic


variables {α : Type*} [comm_ring α]
lemma p (a₁ b₁ a₂ b₂ : α) : a₁ * b₁ - a₂ * b₂ = a₁ * (b₁ - b₂) + (a₁ - a₂) * b₂ :=
begin
simp only [add_mul, mul_add, sub_eq_add_neg, neg_mul_neg, neg_mul_eq_mul_neg],
abel,
end

variables {α : Type*} [comm_ring α]
lemma p (a₁ b₁ a₂ b₂ : α) : a₁ * b₁ - a₂ * b₂ = a₁ * (b₁ - b₂) + (a₁ - a₂) * b₂ :=
begin
rw [sub_mul, mul_sub],
abel,
end

[Jalex Stark]

adding sub_mul and mul_sub to the simp list doesn't do it for me, I think you need to put them down in a smart order

[Jalex Stark]

oh i think one of my simp lemmas is backward

[Mario Carneiro]

I didn't actually look up the names

variables {α : Type*} [comm_ring α]
lemma p (a₁ b₁ a₂ b₂ : α) : a₁ * b₁ - a₂ * b₂ = a₁ * (b₁ - b₂) + (a₁ - a₂) * b₂ :=
begin
simp only [add_mul, mul_add, sub_eq_add_neg, neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm],
abel,
end

[Mario Carneiro]

Oh mul_assoc should also be in the list

[Heather Macbeth]

Thanks!

[Jalex Stark]

@Heather Macbeth , you could stick this in your project somewhere and modify it as needed

import tactic

meta def noncomm_ring := `[simp only [add_mul, mul_add, sub_eq_add_neg, neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm, mul_assoc]; abel]

variables {α : Type*} [comm_ring α]
lemma p (a₁ b₁ a₂ b₂ : α) : a₁ * b₁ - a₂ * b₂ = a₁ * (b₁ - b₂) + (a₁ - a₂) * b₂ :=
begin
noncomm_ring,
end