refactor(algebra/group/defs): Use nsmul in zsmul_rec

src/algebra/group/defs.lean

@@ -3,8 +3,9 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
-import tactic.basic
 import logic.function.basic
+import tactic.basic
+import tactic.hopt_param
 
 /-!
 # Typeclasses for (semi)groups and monoids
@@ -593,15 +594,15 @@ end cancel_monoid
 
 /-- The fundamental power operation in a group. `zpow_rec n a = a*a*...*a` n times, for integer `n`.
 Use instead `a ^ n`,  which has better definitional behavior. -/
-def zpow_rec {M : Type*} [has_one M] [has_mul M] [has_inv M] : ℤ → M → M
-| (int.of_nat n) a := npow_rec n a
-| -[1+ n]    a := (npow_rec n.succ a) ⁻¹
+def zpow_rec [has_one G] [has_mul G] [has_inv G] (npow : ℕ → G → G := npow_rec) : ℤ → G → G
+| (int.of_nat n) a := npow n a
+| -[1+ n]        a := (npow n.succ a)⁻¹
 
 /-- The fundamental scalar multiplication in an additive group. `zsmul_rec n a = a+a+...+a` n
 times, for integer `n`. Use instead `n • a`, which has better definitional behavior. -/
-def zsmul_rec {M : Type*} [has_zero M] [has_add M] [has_neg M]: ℤ → M → M
-| (int.of_nat n) a := nsmul_rec n a
-| -[1+ n]    a := - (nsmul_rec n.succ a)
+def zsmul_rec [has_zero G] [has_add G] [has_neg G] (nsmul : ℕ → G → G := nsmul_rec) : ℤ → G → G
+| (int.of_nat n) a := nsmul n a
+| -[1+ n]        a := -nsmul n.succ a
 
 attribute [to_additive] zpow_rec
 
@@ -680,10 +681,10 @@ explanations on this.
 class div_inv_monoid (G : Type u) extends monoid G, has_inv G, has_div G :=
 (div := λ a b, a * b⁻¹)
 (div_eq_mul_inv : ∀ a b : G, a / b = a * b⁻¹ . try_refl_tac)
-(zpow : ℤ → G → G := zpow_rec)
-(zpow_zero' : ∀ (a : G), zpow 0 a = 1 . try_refl_tac)
-(zpow_succ' :
-  ∀ (n : ℕ) (a : G), zpow (int.of_nat n.succ) a = a * zpow (int.of_nat n) a . try_refl_tac)
+(zpow : ℤ → G → G := zpow_rec npow)
+(zpow_zero' : hopt_param (∀ a : G, zpow 0 a = 1) npow_zero' . solve_default)
+(zpow_succ' : hopt_param (∀ (n : ℕ) (a : G), zpow (int.of_nat n.succ) a = a * zpow (int.of_nat n) a)
+  npow_succ' . solve_default)
 (zpow_neg' :
   ∀ (n : ℕ) (a : G), zpow (-[1+ n]) a = (zpow n.succ a)⁻¹ . try_refl_tac)
 
@@ -708,10 +709,11 @@ explanations on this.
 class sub_neg_monoid (G : Type u) extends add_monoid G, has_neg G, has_sub G :=
 (sub := λ a b, a + -b)
 (sub_eq_add_neg : ∀ a b : G, a - b = a + -b . try_refl_tac)
-(zsmul : ℤ → G → G := zsmul_rec)
-(zsmul_zero' : ∀ (a : G), zsmul 0 a = 0 . try_refl_tac)
-(zsmul_succ' :
-  ∀ (n : ℕ) (a : G), zsmul (int.of_nat n.succ) a = a + zsmul (int.of_nat n) a . try_refl_tac)
+(zsmul : ℤ → G → G := zsmul_rec nsmul)
+(zsmul_zero' : hopt_param (∀ (a : G), zsmul 0 a = 0) nsmul_zero' . solve_default)
+(zsmul_succ' : hopt_param
+  (∀ (n : ℕ) (a : G), zsmul (int.of_nat n.succ) a = a + zsmul (int.of_nat n) a) nsmul_succ'
+  . solve_default)
 (zsmul_neg' :
   ∀ (n : ℕ) (a : G), zsmul (-[1+ n]) a = - (zsmul n.succ a) . try_refl_tac)
 

src/tactic/hopt_param.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2022 Yaël Dillies, Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Eric Wieser
+-/
+
+/-!
+# Heterogeneous optional parameter
+
+This file provides a heterogeneous version of `opt_param` for use in structure defaults.
+
+The associated tactic `solve_default` allows solving proof obligations involving default field
+values in terms of previous structure fields.
+
+The syntax is to make the type of the defaulted field
+`hopt_param the_type the_default . solve_default` where `the_type` is the type you actually want for
+the field, and `the_default` is the default value (often, proof) for it.
+
+The point is that `the_default` does **not** have to be of type `the_type` at the time the structure
+is declared, but only when constructing an instance of the structure.
+-/
+
+/-- Gadget for optional parameter support. -/
+@[reducible] def hopt_param {α β : Sort*} (a : α) (b : β) : α := a
+
+/-- Return `b` if the goal is `hopt_param a b`. -/
+meta def try_hopt_param : command :=
+do
+  `(hopt_param %%a %%b) ← tactic.target,
+  tactic.exact b
+
+/-- Return `b` if the goal is `hopt_param a b`.
+
+This can be used in structure declarations to alleviate proof obligations which can be derived from
+other fields which themselves have a default value.
+```
+structure foo :=
+(bar : ℕ)
+(bar_eq : bar = 37)
+(baz : ℕ := bar)
+(baz_eq : hopt_param (baz = 37) bar_eq . solve_default)
+
+/-- `baz_eq` is automatically proved using `bar_eq` because `baz` wasn't changed from its default
+value `bar. -/
+example : foo :=
+{ bar := if 2 = 2 then 37 else 0,
+  bar_eq := if_pos rfl }
+``` -/
+meta def solve_default : command :=
+try_hopt_param <|> tactic.fail "A previous structure field was changed from its default value, so
+  `solve_default` cannot solve the proof obligation automatically."