From de0d7a8a06b8d24bbe503dc9f6bbe691eb0652ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 5 Dec 2022 16:03:29 +0000 Subject: [PATCH 1/3] refactor(algebra/group/defs): Use `nsmul` in `zsmul_rec` --- src/algebra/group/defs.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean index ae71d164e6ef6..5372083eb9857 100644 --- a/src/algebra/group/defs.lean +++ b/src/algebra/group/defs.lean @@ -593,15 +593,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,7 +680,7 @@ 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 : ℤ → 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) @@ -708,7 +708,7 @@ 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 : ℤ → 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) From bbcaf3fbad7bdee53438833f4291d0fa1c422009 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 21 Dec 2022 22:35:06 +0000 Subject: [PATCH 2/3] 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." From f9f19ebc23891c4c7c737a3ff15657c4ceba4f8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 7 Jan 2023 16:29:11 +0100 Subject: [PATCH 3/3] make it fail --- src/tactic/hopt_param.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/hopt_param.lean b/src/tactic/hopt_param.lean index 7fd560df8b20c..5975567a61722 100644 --- a/src/tactic/hopt_param.lean +++ b/src/tactic/hopt_param.lean @@ -47,5 +47,5 @@ example : foo := 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 +try_hopt_param <|> tactic.fail "A previous structure field was changed from its default value, so `solve_default` cannot solve the proof obligation automatically."