Skip to content

Infer Ma-Wang step certificates #334

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
PerAlexandersson merged 1 commit into from
Aug 4, 2026
Merged

Infer Ma-Wang step certificates #334

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions RealRooted/Tactic/Examples/MaWang.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
35 changes: 35 additions & 0 deletions RealRooted/Tactic/MaWang.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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 ","
Expand All @@ -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 ","
Expand All @@ -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 ","
Expand Down Expand Up @@ -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,
Expand Down
Loading