From dda076256283687b2733343a91017689d949d090 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Tue, 4 Aug 2026 07:14:44 +0000 Subject: [PATCH] Infer Ma-Wang step certificates --- RealRooted/Tactic/Examples/MaWang.lean | 42 ++++++++++++++++++++++++++ RealRooted/Tactic/MaWang.lean | 35 +++++++++++++++++++++ 2 files changed, 77 insertions(+) diff --git a/RealRooted/Tactic/Examples/MaWang.lean b/RealRooted/Tactic/Examples/MaWang.lean index 5e591cba..727b0496 100644 --- a/RealRooted/Tactic/Examples/MaWang.lean +++ b/RealRooted/Tactic/Examples/MaWang.lean @@ -136,6 +136,48 @@ example {f u v : ℝ[X]} source_pos_lc := hf_pos, root_sign := hroot_sign +example {f u v g a b : ℝ[X]} + (_hg : g.Splits) + (_hdegg : 2 ≤ g.natDegree) + (_hdeg_g_lo : g.natDegree ≤ (a * g + b * g.derivative).natDegree) + (_hdeg_g_hi : (a * g + b * g.derivative).natDegree ≤ g.natDegree + 1) + (_hG_pos : HasPosLeadingCoeff (a * g + b * g.derivative)) + (_hg_pos : HasPosLeadingCoeff g) + (_hroot_sign_g : + ∀ r, g.IsRoot r → b.eval r * (g.derivative.eval r) ^ 2 < 0) + (hf : f.Splits) + (hdegf : 2 ≤ f.natDegree) + (hdeg_lo : f.natDegree ≤ (u * f + v * f.derivative).natDegree) + (hdeg_hi : (u * f + v * f.derivative).natDegree ≤ f.natDegree + 1) + (hF_pos : HasPosLeadingCoeff (u * f + v * f.derivative)) + (hf_pos : HasPosLeadingCoeff f) + (hroot_sign : + ∀ r, f.IsRoot r → v.eval r * (f.derivative.eval r) ^ 2 < 0) : + Prec f (u * f + v * f.derivative) := by + rr_ma_wang + +example {f u v : ℝ[X]} + (hf : f.Splits) + (hdegf : 2 ≤ f.natDegree) + (hdeg : (u * f + v * f.derivative).natDegree = f.natDegree) + (hF_pos : HasPosLeadingCoeff (u * f + v * f.derivative)) + (hf_pos : HasPosLeadingCoeff f) + (hroot_sign : + ∀ r, f.IsRoot r → v.eval r * (f.derivative.eval r) ^ 2 < 0) : + Prec f (u * f + v * f.derivative) := by + rr_ma_wang_same + +example {f u v : ℝ[X]} + (hf : f.Splits) + (hdegf : 2 ≤ f.natDegree) + (hdeg : (u * f + v * f.derivative).natDegree = f.natDegree + 1) + (hF_pos : HasPosLeadingCoeff (u * f + v * f.derivative)) + (hf_pos : HasPosLeadingCoeff f) + (hroot_sign : + ∀ r, f.IsRoot r → v.eval r * (f.derivative.eval r) ^ 2 < 0) : + Prec f (u * f + v * f.derivative) := by + rr_ma_wang_succ + example {f g a b : ℝ[X]} (hgf : Interlaces g f) (hg_pos : HasPosLeadingCoeff g) diff --git a/RealRooted/Tactic/MaWang.lean b/RealRooted/Tactic/MaWang.lean index 67e4a1f8..f62b66f2 100644 --- a/RealRooted/Tactic/MaWang.lean +++ b/RealRooted/Tactic/MaWang.lean @@ -1,6 +1,7 @@ import RealRooted.LiuWangRecursion import RealRooted.MaWang import RealRooted.Tactic.Finish +import RealRooted.Tactic.Lookup import RealRooted.Tactic.RootBounds import RealRooted.Tactic.ScalarDen import RealRooted.Tactic.Sign @@ -1793,6 +1794,8 @@ syntax (name := rr_ma_wang) "rr_ma_wang" " using " term ", " term ", " term ", " term ", " term ", " term ", " term : tactic +syntax (name := rr_ma_wang_inferred) "rr_ma_wang" : tactic + syntax (name := rr_ma_wang_named) "rr_ma_wang" " using " "splits" ":=" term "," @@ -1808,6 +1811,8 @@ syntax (name := rr_ma_wang_same) "rr_ma_wang_same" " using " term ", " term ", " term ", " term ", " term ", " term : tactic +syntax (name := rr_ma_wang_same_inferred) "rr_ma_wang_same" : tactic + syntax (name := rr_ma_wang_same_named) "rr_ma_wang_same" " using " "splits" ":=" term "," @@ -1822,6 +1827,8 @@ syntax (name := rr_ma_wang_succ) "rr_ma_wang_succ" " using " term ", " term ", " term ", " term ", " term ", " term : tactic +syntax (name := rr_ma_wang_succ_inferred) "rr_ma_wang_succ" : tactic + syntax (name := rr_ma_wang_succ_named) "rr_ma_wang_succ" " using " "splits" ":=" term "," @@ -3493,6 +3500,34 @@ macro_rules rr_mw_three_variants $hleft:term, $hmiddle:term, $hright:term) => `(tactic| rr_first_exact_then_realrooted_sequence_or_projection $hleft, $hmiddle, $hright) + | `(tactic| rr_ma_wang) => + `(tactic| + rr_ma_wang using + splits := (by rr_lookup), + degree_two := (by rr_lookup [rr_degree]), + degree_lower := (by rr_lookup [rr_degree]), + degree_upper := (by rr_lookup [rr_degree]), + target_pos_lc := (by rr_lookup [rr_pos_lc]), + source_pos_lc := (by rr_lookup [rr_pos_lc]), + root_sign := (by rr_lookup)) + | `(tactic| rr_ma_wang_same) => + `(tactic| + rr_ma_wang_same using + splits := (by rr_lookup), + degree_two := (by rr_lookup [rr_degree]), + degree := (by rr_lookup [rr_degree]), + target_pos_lc := (by rr_lookup [rr_pos_lc]), + source_pos_lc := (by rr_lookup [rr_pos_lc]), + root_sign := (by rr_lookup)) + | `(tactic| rr_ma_wang_succ) => + `(tactic| + rr_ma_wang_succ using + splits := (by rr_lookup), + degree_two := (by rr_lookup [rr_degree]), + degree := (by rr_lookup [rr_degree]), + target_pos_lc := (by rr_lookup [rr_pos_lc]), + source_pos_lc := (by rr_lookup [rr_pos_lc]), + root_sign := (by rr_lookup)) | `(tactic| rr_ma_wang using $hf:term, $hdegf:term, $hdeg_lo:term, $hdeg_hi:term, $hF_pos:term,