Skip to content

Automate direct finite-symbol stability tactic #333

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

Automate direct finite-symbol stability tactic #333

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
16 changes: 16 additions & 0 deletions RealRooted/Tactic/Examples/FiniteSymbol.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,5 +29,21 @@ example {sigma tau : Type*} [Fintype sigma]
symbol_stable := hSymbol,
input_stable := hf

example {sigma tau : Type*} [Fintype sigma]
(T : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1) →ₗ[ℂ]
MvPolynomial tau ℂ)
(S : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1) →ₗ[ℂ]
MvPolynomial tau ℂ)
(_hSymbolS : MvUpperHalfPlaneStable
(MvPolynomial.algebraicSymbol (fun _ : sigma => 1) S))
(hSymbol : MvUpperHalfPlaneStable
(MvPolynomial.algebraicSymbol (fun _ : sigma => 1) T))
(g : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1))
(_hg : MvUpperHalfPlaneStable g.1)
(f : MvPolynomial.degreeOfLE sigma ℂ (fun _ => 1))
(hf : MvUpperHalfPlaneStable f.1) :
MvUpperHalfPlaneStableOrZero (T f) := by
rr_finite_symbol_stable_or_zero_auto

end Tactic
end RealRooted
12 changes: 10 additions & 2 deletions RealRooted/Tactic/FiniteSymbol.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ import RealRooted.BorceaBranden.FiniteSymbolPreserver
/-!
# Finite-symbol stable-or-zero tactic frontend

Thin certificate-driven wrappers around the proved multiaffine finite-symbol
stability theorem.
Thin explicit and automatic wrappers around the proved multiaffine
finite-symbol stability theorem.
-/

namespace RealRooted
Expand All @@ -24,6 +24,9 @@ syntax (name := rr_finite_symbol_stable_or_zero_inferred)
"input_stable" ":=" term :
tactic

syntax (name := rr_finite_symbol_stable_or_zero_auto)
"rr_finite_symbol_stable_or_zero_auto" : tactic

macro_rules
| `(tactic|
rr_finite_symbol_stable_or_zero using
Expand All @@ -41,6 +44,11 @@ macro_rules
`(tactic|
exact RealRooted.BorceaBranden.finiteSymbol_preserves_stability
_ $hSymbol _ $hf)
| `(tactic| rr_finite_symbol_stable_or_zero_auto) =>
`(tactic|
rr_finite_symbol_stable_or_zero using
symbol_stable := (by assumption),
input_stable := (by assumption))

end Tactic
end RealRooted
Loading