feat(algebra/group/with_one): cleanup algebraic instances (#10194)

This:

* adds a `has_neg (with_zero α)` instance which sends `0` to `0` and otherwise uses the underlying negation (and the same for `has_inv (with_one α)`).
* replaces the `has_div (with_zero α)`,  `has_pow (with_zero α) ℕ`, and `has_pow (with_zero α) ℤ` instances in order to produce better definitional properties than the previous default ones.

src/algebra/group/with_one.lean

@@ -36,6 +36,9 @@ instance : has_one (with_one α) := ⟨none⟩
 @[to_additive]
 instance [has_mul α] : has_mul (with_one α) := ⟨option.lift_or_get (*)⟩
 
+@[to_additive]
+instance [has_inv α] : has_inv (with_one α) := ⟨λ a, option.map has_inv.inv a⟩
+
 @[to_additive]
 instance : inhabited (with_one α) := ⟨1⟩
 
@@ -168,6 +171,9 @@ attribute [irreducible] with_one
 @[simp, norm_cast, to_additive]
 lemma coe_mul [has_mul α] (a b : α) : ((a * b : α) : with_one α) = a * b := rfl
 
+@[simp, norm_cast, to_additive]
+lemma coe_inv [has_inv α] (a : α) : ((a⁻¹ : α) : with_one α) = a⁻¹ := rfl
+
 end with_one
 
 namespace with_zero
@@ -221,26 +227,82 @@ instance [mul_one_class α] : mul_zero_one_class (with_zero α) :=
   ..with_zero.mul_zero_class,
   ..with_zero.has_one }
 
+instance [has_one α] [has_pow α ℕ] : has_pow (with_zero α) ℕ :=
+⟨λ x n, match x, n with
+  | none, 0 := 1
+  | none, n + 1 := 0
+  | some x, n := ↑(x ^ n)
+  end⟩
+
+@[simp, norm_cast] lemma coe_pow [has_one α] [has_pow α ℕ] {a : α} (n : ℕ) :
+  ↑(a ^ n : α) = (↑a ^ n : with_zero α) := rfl
+
 instance [monoid α] : monoid_with_zero (with_zero α) :=
-{ ..with_zero.mul_zero_one_class,
-  ..with_zero.semigroup_with_zero }
+{ npow := λ n x, x ^ n,
+  npow_zero' := λ x, match x with
+    | none   := rfl
+    | some x := congr_arg some $ pow_zero _
+    end,
+  npow_succ' := λ n x, match x with
+    | none   := rfl
+    | some x := congr_arg some $ pow_succ _ _
+    end,
+  .. with_zero.mul_zero_one_class,
+  .. with_zero.semigroup_with_zero }
 
 instance [comm_monoid α] : comm_monoid_with_zero (with_zero α) :=
 { ..with_zero.monoid_with_zero, ..with_zero.comm_semigroup }
 
 /-- Given an inverse operation on `α` there is an inverse operation
   on `with_zero α` sending `0` to `0`-/
-definition inv [has_inv α] (x : with_zero α) : with_zero α :=
-do a ← x, return a⁻¹
-
-instance [has_inv α] : has_inv (with_zero α) := ⟨with_zero.inv⟩
+instance [has_inv α] : has_inv (with_zero α) := ⟨λ a, option.map has_inv.inv a⟩
 
 @[simp, norm_cast] lemma coe_inv [has_inv α] (a : α) :
   ((a⁻¹ : α) : with_zero α) = a⁻¹ := rfl
 
 @[simp] lemma inv_zero [has_inv α] :
   (0 : with_zero α)⁻¹ = 0 := rfl
 
+instance [has_div α] : has_div (with_zero α) :=
+⟨λ o₁ o₂, o₁.bind (λ a, option.map (λ b, a / b) o₂)⟩
+
+@[norm_cast] lemma coe_div [has_div α] (a b : α) : ↑(a / b : α) = (a / b : with_zero α) := rfl
+
+instance [has_one α] [has_pow α ℤ] : has_pow (with_zero α) ℤ :=
+⟨λ x n, match x, n with
+  | none, int.of_nat 0            := 1
+  | none, int.of_nat (nat.succ n) := 0
+  | none, int.neg_succ_of_nat n   := 0
+  | some x, n                     := ↑(x ^ n)
+  end⟩
+
+@[simp, norm_cast] lemma coe_zpow [div_inv_monoid α] {a : α} (n : ℤ) :
+  ↑(a ^ n : α) = (↑a ^ n : with_zero α) := rfl
+
+instance [div_inv_monoid α] : div_inv_monoid (with_zero α) :=
+{ div_eq_mul_inv := λ a b, match a, b with
+    | none,   _      := rfl
+    | some a, none   := rfl
+    | some a, some b := congr_arg some (div_eq_mul_inv _ _)
+    end,
+  zpow := λ n x, x ^ n,
+  zpow_zero' := λ x, match x with
+    | none   := rfl
+    | some x := congr_arg some $ zpow_zero _
+    end,
+  zpow_succ' := λ n x, match x with
+    | none   := rfl
+    | some x := congr_arg some $ div_inv_monoid.zpow_succ' _ _
+    end,
+  zpow_neg' := λ n x, match x with
+    | none   := rfl
+    | some x := congr_arg some $ div_inv_monoid.zpow_neg' _ _
+    end,
+  .. with_zero.has_div,
+  .. with_zero.has_inv,
+  .. with_zero.monoid_with_zero, }
+
+
 section group
 variables [group α]
 
@@ -250,14 +312,11 @@ show ((1⁻¹ : α) : with_zero α) = 1, by simp
 /-- if `G` is a group then `with_zero G` is a group with zero. -/
 instance : group_with_zero (with_zero α) :=
 { inv_zero := inv_zero,
-  mul_inv_cancel := by { intros a ha, lift a to α using ha, norm_cast, apply mul_right_inv },
+  mul_inv_cancel := λ a ha, by { lift a to α using ha, norm_cast, apply mul_right_inv },
   .. with_zero.monoid_with_zero,
-  .. with_zero.has_inv,
+  .. with_zero.div_inv_monoid,
   .. with_zero.nontrivial }
 
-@[norm_cast]
-lemma div_coe (a b : α) : (a : with_zero α) / b = (a * b⁻¹ : α) := rfl
-
 end group
 
 instance [comm_group α] : comm_group_with_zero (with_zero α) :=