From 380f7fb98aad78c3dbe93121cc114d4d7de70e25 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 28 May 2022 03:16:02 -0400 Subject: [PATCH 1/7] feat(tactic/ring): recursive ring_nf --- src/tactic/ring.lean | 38 +++++++++++++++++++++++++------------- test/ring.lean | 13 +++++++++++++ 2 files changed, 38 insertions(+), 13 deletions(-) diff --git a/src/tactic/ring.lean b/src/tactic/ring.lean index 82a18559f2a72..e1365615f119b 100644 --- a/src/tactic/ring.lean +++ b/src/tactic/ring.lean @@ -431,6 +431,17 @@ do c ← get_cache, return (xadd' c (const α1 1) (e, i) (`(1), 1) (const α0 0), c.cs_app ``horner_atom [e]) +/-- Evaluate `a` where `a` is an atom. -/ +meta def eval_norm_atom (norm_atom : expr → tactic (expr × expr)) + (e : expr) : ring_m (horner_expr × expr) := +do o ← lift $ try_core (guard (e.get_app_args.length > 0) >> norm_atom e), + match o with + | none := eval_atom e + | some (e', p) := do + (e₂, p₂) ← eval_atom e', + prod.mk e₂ <$> lift (mk_eq_trans p p₂) + end + lemma subst_into_pow {α} [monoid α] (l r tl tr t) (prl : (l : α) = tl) (prr : (r : ℕ) = tr) (prt : tl ^ tr = t) : l ^ r = t := by rw [prl, prr, prt] @@ -445,7 +456,7 @@ by rw [div_eq_mul_inv, h] /-- Evaluate a ring expression `e` recursively to normal form, together with a proof of equality. -/ -meta def eval : expr → ring_m (horner_expr × expr) +meta def eval (norm_atom : expr → tactic (expr × expr)) : expr → ring_m (horner_expr × expr) | `(%%e₁ + %%e₂) := do (e₁', p₁) ← eval e₁, (e₂', p₂) ← eval e₂, @@ -460,7 +471,7 @@ meta def eval : expr → ring_m (horner_expr × expr) (e', p) ← eval e, p' ← ic_lift $ λ ic, ic.mk_app ``unfold_sub [e₁, e₂, e', p], return (e', p')) - (eval_atom e) + (eval_norm_atom norm_atom e) | `(- %%e) := do (e₁, p₁) ← eval e, (e₂, p₂) ← eval_neg e₁, @@ -475,7 +486,7 @@ meta def eval : expr → ring_m (horner_expr × expr) | e@`(has_inv.inv %%_) := (do (e', p) ← lift $ norm_num.derive e <|> refl_conv e, n ← lift $ e'.to_rat, - return (const e' n, p)) <|> eval_atom e + return (const e' n, p)) <|> eval_norm_atom norm_atom e | e@`(@has_div.div _ %%inst %%e₁ %%e₂) := mcond (succeeds (do inst' ← ic_lift $ λ ic, ic.mk_app ``div_inv_monoid.to_has_div [], @@ -486,7 +497,7 @@ meta def eval : expr → ring_m (horner_expr × expr) (e', p) ← eval e, p' ← ic_lift $ λ ic, ic.mk_app ``unfold_div [e₁, e₂, e', p], return (e', p')) - (eval_atom e) + (eval_norm_atom norm_atom e) | e@`(@has_pow.pow _ _ %%P %%e₁ %%e₂) := do (e₂', p₂) ← lift $ norm_num.derive e₂ <|> refl_conv e₂, match e₂'.to_nat, P with @@ -495,18 +506,18 @@ meta def eval : expr → ring_m (horner_expr × expr) (e', p') ← eval_pow e₁' (e₂, k), p ← ic_lift $ λ ic, ic.mk_app ``subst_into_pow [e₁, e₂, e₁', e₂', e', p₁, p₂, p'], return (e', p) - | _, _ := eval_atom e + | _, _ := eval_norm_atom norm_atom e end | e := match e.to_nat with | some n := (const e (rat.of_int n)).refl_conv - | none := eval_atom e + | none := eval_norm_atom norm_atom e end /-- Evaluate a ring expression `e` recursively to normal form, together with a proof of equality. -/ meta def eval' (red : transparency) (atoms : ref (buffer expr)) - (e : expr) : tactic (expr × expr) := -ring_m.run' red atoms e $ do (e', p) ← eval e, return (e', p) + (norm_atom : expr → tactic (expr × expr)) (e : expr) : tactic (expr × expr) := +ring_m.run' red atoms e $ do (e', p) ← eval norm_atom e, return (e', p) theorem horner_def' {α} [comm_semiring α] (a x n b) : @horner α _ a x n b = x ^ n * a + b := by simp [horner, mul_comm] @@ -542,8 +553,8 @@ instance : inhabited normalize_mode := ⟨normalize_mode.horner⟩ /-- A `ring`-based normalization simplifier that rewrites ring expressions into the specified mode. See `normalize`. This version takes a list of atoms to persist across multiple calls. -/ meta def normalize' (atoms : ref (buffer expr)) - (red : transparency) (mode := normalize_mode.horner) (e : expr) : tactic (expr × expr) := -do + (red : transparency) (mode := normalize_mode.horner) : expr → opt_param _ ff → tactic (expr × expr) +| e inner := do pow_lemma ← simp_lemmas.mk.add_simp ``pow_one, let lemmas := match mode with | normalize_mode.SOP := @@ -564,9 +575,10 @@ do (λ e, do a ← read_ref atoms, (a, e', pr) ← ext_simplify_core a {} - simp_lemmas.mk (λ _, failed) (λ a _ _ _ e, do + simp_lemmas.mk (λ _, failed) (λ a _ _ p e, do + guard (inner → p.is_some), write_ref atoms a, - (new_e, pr) ← eval' red atoms e, + (new_e, pr) ← eval' red atoms (λ e, normalize' e tt) e, (new_e, pr) ← match mode with | normalize_mode.raw := λ _, pure (new_e, pr) | normalize_mode.horner := trans_conv (λ _, pure (new_e, pr)) @@ -613,7 +625,7 @@ meta def ring1 (red : parse (tk "!")?) : tactic unit := let transp := if red.is_some then semireducible else reducible in do `(%%e₁ = %%e₂) ← target >>= instantiate_mvars, ((e₁', p₁), (e₂', p₂)) ← ring_m.run transp e₁ $ - prod.mk <$> eval e₁ <*> eval e₂, + prod.mk <$> eval (λ _, failed) e₁ <*> eval (λ _, failed) e₂, is_def_eq e₁' e₂', p ← mk_eq_symm p₂ >>= mk_eq_trans p₁, tactic.exact p diff --git a/test/ring.lean b/test/ring.lean index 04cef1e5ad9fa..9650c284b8ccc 100644 --- a/test/ring.lean +++ b/test/ring.lean @@ -36,6 +36,19 @@ begin ring end +example {A : ℤ} (f : ℤ → ℤ) : f 0 = f (A - A) := by ring_nf +example {A : ℤ} (f : ℤ → ℤ) : f 0 = f (A + -A) := by ring_nf + +example {a b c : ℝ} (h : 0 < a ^ 4 + b ^ 4 + c ^ 4) : + a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) + + b ^ 4 / (b ^ 4 + c ^ 4 + a ^ 4) + + c ^ 4 / (c ^ 4 + a ^ 4 + b ^ 4) + = 1 := +begin + ring_nf at ⊢ h, + field_simp [h.ne'], +end + example (a b c d x y : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) : a + b / x - c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x - c) / x) := begin From 5816f75ba2f79ff4273e7c61b1d6d330edf08baa Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 28 May 2022 03:28:40 -0400 Subject: [PATCH 2/7] fix --- .../continued_fractions/computation/approximations.lean | 3 +-- src/tactic/ring.lean | 3 ++- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/algebra/continued_fractions/computation/approximations.lean b/src/algebra/continued_fractions/computation/approximations.lean index 3dda5bacdabcc..15194e3e7af1f 100644 --- a/src/algebra/continued_fractions/computation/approximations.lean +++ b/src/algebra/continued_fractions/computation/approximations.lean @@ -515,8 +515,7 @@ begin simp only [stream_nth_fr_ne_zero, conts_eq.symm, pred_conts_eq.symm] at tmp, rw tmp, simp only [denom'], - ring_nf, - ac_refl }, + ring_nf }, rwa this }, -- derive some tedious inequalities that we need to rewrite our goal have nextConts_b_ineq : (fib (n + 2) : K) ≤ (pred_conts.b + gp.b * conts.b), by diff --git a/src/tactic/ring.lean b/src/tactic/ring.lean index e1365615f119b..31a6c114cef26 100644 --- a/src/tactic/ring.lean +++ b/src/tactic/ring.lean @@ -553,7 +553,8 @@ instance : inhabited normalize_mode := ⟨normalize_mode.horner⟩ /-- A `ring`-based normalization simplifier that rewrites ring expressions into the specified mode. See `normalize`. This version takes a list of atoms to persist across multiple calls. -/ meta def normalize' (atoms : ref (buffer expr)) - (red : transparency) (mode := normalize_mode.horner) : expr → opt_param _ ff → tactic (expr × expr) + (red : transparency) (mode := normalize_mode.horner) : + expr → opt_param _ ff → tactic (expr × expr) | e inner := do pow_lemma ← simp_lemmas.mk.add_simp ``pow_one, let lemmas := match mode with From 57ad0b2eecda3c333fa353ea1ddc5c72d2e5d162 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 28 May 2022 04:11:07 -0400 Subject: [PATCH 3/7] fix --- src/ring_theory/trace.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean index a00ca29fbb241..b6c478a7d5406 100644 --- a/src/ring_theory/trace.lean +++ b/src/ring_theory/trace.lean @@ -396,7 +396,7 @@ begin trace_form_apply, algebra.smul_mul_assoc], rw [mul_comm (b x), ← smul_def], ring_nf, - simp, + simp [mul_comm], end lemma trace_matrix_of_matrix_mul_vec [fintype κ] (b : κ → B) (P : matrix κ κ A) : From 1aba786748c2ef6325bcfb4125fa88946cd9ce8b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 14 Jun 2022 22:04:56 -0400 Subject: [PATCH 4/7] add docs, option --- src/tactic/ring.lean | 35 +++++++++++++++++++++++++---------- test/ring.lean | 6 ++++++ 2 files changed, 31 insertions(+), 10 deletions(-) diff --git a/src/tactic/ring.lean b/src/tactic/ring.lean index 31a6c114cef26..afe876f08e380 100644 --- a/src/tactic/ring.lean +++ b/src/tactic/ring.lean @@ -551,9 +551,20 @@ inductive normalize_mode | raw | SOP | horner instance : inhabited normalize_mode := ⟨normalize_mode.horner⟩ /-- A `ring`-based normalization simplifier that rewrites ring expressions into the specified mode. - See `normalize`. This version takes a list of atoms to persist across multiple calls. -/ +See `normalize`. This version takes a list of atoms to persist across multiple calls. + +* `atoms`: a mutable reference containing the atom set from the previous call +* `red`: the reducibility setting to use when comparing atoms for defeq +* `mode`: the normalization style (see `normalize_mode`) +* `recursive`: if true, atoms will be reduced recursively using `normalize'` +* `e`: the expression to normalize +* `inner`: This should be set to `ff`. It is used internally to disable normalization + at the top level when called from `eval` in order to prevent an infinite loop + `eval' -> eval_atom -> normalize' -> eval'` when called on something that can't + be simplified like `x`. +-/ meta def normalize' (atoms : ref (buffer expr)) - (red : transparency) (mode := normalize_mode.horner) : + (red : transparency) (mode := normalize_mode.horner) (recursive := tt) : expr → opt_param _ ff → tactic (expr × expr) | e inner := do pow_lemma ← simp_lemmas.mk.add_simp ``pow_one, @@ -575,11 +586,12 @@ meta def normalize' (atoms : ref (buffer expr)) pure (e', pr)) (λ e, do a ← read_ref atoms, + let norm_rec := if recursive then λ e, normalize' e tt else λ _, failed, (a, e', pr) ← ext_simplify_core a {} simp_lemmas.mk (λ _, failed) (λ a _ _ p e, do guard (inner → p.is_some), write_ref atoms a, - (new_e, pr) ← eval' red atoms (λ e, normalize' e tt) e, + (new_e, pr) ← eval' red atoms norm_rec e, (new_e, pr) ← match mode with | normalize_mode.raw := λ _, pure (new_e, pr) | normalize_mode.horner := trans_conv (λ _, pure (new_e, pr)) @@ -607,9 +619,11 @@ meta def normalize' (atoms : ref (buffer expr)) This results in terms like `(3 * x ^ 2 * y + 1) * x + y`. * `SOP` means sum of products form, expanding everything to monomials. This results in terms like `3 * x ^ 3 * y + x + y`. -/ -meta def normalize (red : transparency) (mode := normalize_mode.horner) (e : expr) : +meta def normalize (red : transparency) (mode := normalize_mode.horner) (recursive := tt) (e : expr) : tactic (expr × expr) := -using_new_ref mk_buffer $ λ atoms, normalize' atoms red mode e +using_new_ref mk_buffer $ λ atoms, normalize' atoms red mode recursive e + +structure ring_nf_cfg := (recursive := tt) end ring @@ -649,12 +663,12 @@ which rewrites all ring expressions into a normal form. When writing a normal fo `ring_nf SOP` will use sum-of-products form instead of horner form. `ring_nf!` will use a more aggressive reducibility setting to identify atoms. -/ -meta def ring_nf (red : parse (tk "!")?) (SOP : parse ring.mode) (loc : parse location) : - tactic unit := +meta def ring_nf (red : parse (tk "!")?) (SOP : parse ring.mode) (loc : parse location) + (cfg : ring_nf_cfg := {}) : tactic unit := do ns ← loc.get_locals, let transp := if red.is_some then semireducible else reducible, tt ← using_new_ref mk_buffer $ λ atoms, - tactic.replace_at (normalize' atoms transp SOP) ns loc.include_goal + tactic.replace_at (normalize' atoms transp SOP cfg.recursive) ns loc.include_goal | fail "ring_nf failed to simplify", when loc.include_goal $ try tactic.reflexivity @@ -695,9 +709,10 @@ local postfix `?`:9001 := optional /-- Normalises expressions in commutative (semi-)rings inside of a `conv` block using the tactic `ring`. -/ -meta def ring_nf (red : parse (lean.parser.tk "!")?) (SOP : parse ring.mode) : conv unit := +meta def ring_nf (red : parse (lean.parser.tk "!")?) (SOP : parse ring.mode) + (cfg : ring.ring_nf_cfg := {}) : conv unit := let transp := if red.is_some then semireducible else reducible in -replace_lhs (normalize transp SOP) +replace_lhs (normalize transp SOP cfg.recursive) <|> fail "ring_nf failed to simplify" /-- diff --git a/test/ring.lean b/test/ring.lean index 9650c284b8ccc..82c99e1c65feb 100644 --- a/test/ring.lean +++ b/test/ring.lean @@ -89,3 +89,9 @@ by transitivity; [exact h, ring] -- `ring_nf` should descend into the subexpressions `x * -a` and `-a * x`: example {a x : ℚ} : x * -a = - a * x := by ring_nf + +example (f : ℤ → ℤ) (a b : ℤ) : f (2 * a + b) + b = b + f (b + a + a) := +begin + success_if_fail {{ ring_nf {recursive := ff} }}, + ring_nf +end From c7e578511a4dce52d3f55b20bf12999ebfede6de Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 14 Jun 2022 22:50:18 -0400 Subject: [PATCH 5/7] fix --- src/tactic/ring.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/ring.lean b/src/tactic/ring.lean index afe876f08e380..ffe09506e67b1 100644 --- a/src/tactic/ring.lean +++ b/src/tactic/ring.lean @@ -619,8 +619,8 @@ meta def normalize' (atoms : ref (buffer expr)) This results in terms like `(3 * x ^ 2 * y + 1) * x + y`. * `SOP` means sum of products form, expanding everything to monomials. This results in terms like `3 * x ^ 3 * y + x + y`. -/ -meta def normalize (red : transparency) (mode := normalize_mode.horner) (recursive := tt) (e : expr) : - tactic (expr × expr) := +meta def normalize (red : transparency) (mode := normalize_mode.horner) + (recursive := tt) (e : expr) : tactic (expr × expr) := using_new_ref mk_buffer $ λ atoms, normalize' atoms red mode recursive e structure ring_nf_cfg := (recursive := tt) From 3e802d968b387b1431c4a41e054cd347f23a5019 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 15 Jun 2022 02:24:02 -0400 Subject: [PATCH 6/7] fix --- src/tactic/ring.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/ring.lean b/src/tactic/ring.lean index ffe09506e67b1..fb38496e02fcc 100644 --- a/src/tactic/ring.lean +++ b/src/tactic/ring.lean @@ -623,7 +623,7 @@ meta def normalize (red : transparency) (mode := normalize_mode.horner) (recursive := tt) (e : expr) : tactic (expr × expr) := using_new_ref mk_buffer $ λ atoms, normalize' atoms red mode recursive e -structure ring_nf_cfg := (recursive := tt) +@[derive inhabited] structure ring_nf_cfg := (recursive := tt) end ring From 35254bcd8d173dd95d3bee1a7dca7be1c9eeb640 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 15 Jun 2022 06:36:06 -0400 Subject: [PATCH 7/7] fix --- src/tactic/ring.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/tactic/ring.lean b/src/tactic/ring.lean index fb38496e02fcc..8aff0fdd568ab 100644 --- a/src/tactic/ring.lean +++ b/src/tactic/ring.lean @@ -623,6 +623,10 @@ meta def normalize (red : transparency) (mode := normalize_mode.horner) (recursive := tt) (e : expr) : tactic (expr × expr) := using_new_ref mk_buffer $ λ atoms, normalize' atoms red mode recursive e +/-- Configuration for `ring_nf`. + + * `recursive`: if true, atoms inside ring expressions will be reduced recursively +-/ @[derive inhabited] structure ring_nf_cfg := (recursive := tt) end ring