From bbcaf3fbad7bdee53438833f4291d0fa1c422009 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 21 Dec 2022 22:35:06 +0000
Subject: [PATCH] introduce hopt_param

---
 src/algebra/group/defs.lean | 16 +++++++-----
 src/tactic/hopt_param.lean  | 51 +++++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 7 deletions(-)
 create mode 100644 src/tactic/hopt_param.lean

diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean
index 5372083eb9857..f0f2ec3c39f57 100644
--- a/src/algebra/group/defs.lean
+++ b/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
@@ -681,9 +682,9 @@ 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 npow)
-(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_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)
 
@@ -709,9 +710,10 @@ 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 nsmul)
-(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_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)
 
diff --git a/src/tactic/hopt_param.lean b/src/tactic/hopt_param.lean
new file mode 100644
index 0000000000000..7fd560df8b20c
--- /dev/null
+++ b/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.trace "A previous structure field was changed from its default value, so
+  `solve_default` cannot solve the proof obligation automatically."