multiplicative annoyance

Stream: maths

[Kevin Buzzard]

import group_theory.subgroup

example (R : Type*) [comm_ring R] (P : R → Prop) (T : set R)
  (HP1 : ∀ t : R, t ∈ T → P t) (HP2 : P 0) (HP3 : ∀ r : R, P r → P (-r))
  (HP4 : ∀ r s : R, P r → P s → P (r + s))
 (u : R) (hu : u ∈ add_group.closure T) : P u :=
begin
  induction hu with a ha a ha ih a b ha hb iha ihb,
  { exact HP1 a ha},
  { -- goal P 1
    exact HP2},
  { -- goal P a⁻¹
    exact HP3 a ih,
  },
  { -- goal P (a * b)
    exact HP4 a b iha ihb,
  }
end

All the goals are multiplicative.

[Kevin Buzzard]

In real life I have much more complex goals, and I just failed to use mul_one to deal with v * 1 and then I realised that it might be any of mul_zero, add_one or add_zero

[Kevin Buzzard]

turned out it was mul_zero

[Mario Carneiro]

does add_group.closure have a defined recursor?

[Mario Carneiro]

in_closure.rec_on

[Kenny Lau]

this is all XXX's fault of not allowing variable operation