From 2e561e525ec34dc8026dcd717dde26c64b8f6735 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Tue, 4 Aug 2026 10:41:24 +0000 Subject: [PATCH] Infer derived matrix tactic certificates --- RealRooted/Tactic/Examples/Matrix.lean | 22 +++---- RealRooted/Tactic/Matrix.lean | 84 +++++++++++++++++++++++++- 2 files changed, 92 insertions(+), 14 deletions(-) diff --git a/RealRooted/Tactic/Examples/Matrix.lean b/RealRooted/Tactic/Examples/Matrix.lean index 72b72ca7..69e2a986 100644 --- a/RealRooted/Tactic/Examples/Matrix.lean +++ b/RealRooted/Tactic/Examples/Matrix.lean @@ -99,8 +99,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs_len : fs.length = n) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeqNonneg ((matPolyAction G fs).filter (· ≠ 0)) := by - rr_matrix0_filter_ne_zero using - G, hG_rect, hG_nonneg, hG_affine, fs, hfs_len, hfs + rr_matrix0_filter_ne_zero example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -138,7 +137,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeq0Nonneg (matPolyAction G fs) ∧ ∀ f ∈ matPolyAction G fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := by - rr_matrix0_realrooted using G, hG_rect, hG_nonneg, hG_affine, fs, hfs_len, hfs + rr_matrix0_realrooted example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -219,8 +218,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs : IsInterlacingSeq0Nonneg fs) (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : IsInterlacingSeqNonneg ((matPolyAction G fs).filter (· ≠ 0)) := by - rr_matrix0_filter_ne_zero_weak using - G, hG_rect, hG_nonneg, hG_affine, fs, hfs_len, hfs, hfs_real + rr_matrix0_filter_ne_zero_weak example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -402,8 +400,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs : IsInterlacingSeq0Nonneg fs) (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : IsInterlacingSeqNonneg ((matPolyAction G fs).filter (· ≠ 0)) := by - rr_row_threshold_matrix0_filter_ne_zero_weak using - G, hG_rect, hG_threshold, hG_affine, fs, hfs_len, hfs, hfs_real + rr_row_threshold_matrix0_filter_ne_zero_weak example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -442,8 +439,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeq0Nonneg (matPolyAction G fs) ∧ ∀ f ∈ matPolyAction G fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := by - rr_row_threshold_matrix0_realrooted using - G, hG_rect, hG_threshold, hG_affine, fs, hfs_len, hfs + rr_row_threshold_matrix0_realrooted example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -480,8 +476,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs_len : fs.length = n) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeqNonneg ((matPolyAction G fs).filter (· ≠ 0)) := by - rr_row_threshold_matrix0_filter_ne_zero using - G, hG_rect, hG_threshold, hG_affine, fs, hfs_len, hfs + rr_row_threshold_matrix0_filter_ne_zero example {G : List (List ℝ[X])} (hG_threshold : HasRowThresholdLinearStructure G) : @@ -566,6 +561,11 @@ example (hfs_len : ([] : List ℝ[X]).length = 0) IsInterlacingSeq0Nonneg (matPolyAction decoyMatrix []) := by rr_matrix0 +example (hfs_len : ([] : List ℝ[X]).length = 0) + (hfs : IsInterlacingSeqNonneg ([] : List ℝ[X])) : + IsInterlacingSeqNonneg ((matPolyAction decoyMatrix []).filter (· ≠ 0)) := by + rr_matrix0_filter_ne_zero + example (hfs_len : ([] : List ℝ[X]).length = 0) (hfs : IsInterlacingSeqNonneg ([] : List ℝ[X])) : IsInterlacingSeq0Nonneg (matPolyAction baseMatrix []) := by diff --git a/RealRooted/Tactic/Matrix.lean b/RealRooted/Tactic/Matrix.lean index e8593f37..fa155c54 100644 --- a/RealRooted/Tactic/Matrix.lean +++ b/RealRooted/Tactic/Matrix.lean @@ -37,9 +37,9 @@ The tactics apply `matrix_preserves_interlacing_seq`, the user supplies the matrix action, rectangularity, entry nonnegativity, and `2 x 2` Branden conditions. -The bare `rr_matrix0`, `rr_matrix0_weak`, `rr_row_threshold_matrix0`, and -`rr_row_threshold_matrix0_weak` forms infer the matrix and input from the goal. -They use exact local length and input certificates, then the registered matrix +Every `matrix0` form has a bare variant inferring the matrix and input from the +goal; `rr_matrix` and `rr_row_threshold_matrix` require `using`. The bare forms +use exact local length and input certificates, then the registered matrix certificate attributes. The bare `rr_row_threshold_entry_nonneg` form infers its matrix from the target. @@ -143,6 +143,9 @@ syntax (name := rr_matrix0_realrooted_named) "input_interlacing" ":=" term : tactic +syntax (name := rr_matrix0_realrooted_inferred) + "rr_matrix0_realrooted" : tactic + syntax (name := rr_matrix0_filter_ne_zero) "rr_matrix0_filter_ne_zero" " using " term ", " term ", " @@ -164,6 +167,9 @@ syntax (name := rr_matrix0_filter_ne_zero_named) "input_interlacing" ":=" term : tactic +syntax (name := rr_matrix0_filter_ne_zero_inferred) + "rr_matrix0_filter_ne_zero" : tactic + syntax (name := rr_matrix0_filter_ne_zero_weak) "rr_matrix0_filter_ne_zero_weak" " using " term ", " term ", " @@ -187,6 +193,9 @@ syntax (name := rr_matrix0_filter_ne_zero_weak_named) "input_real_rooted" ":=" term : tactic +syntax (name := rr_matrix0_filter_ne_zero_weak_inferred) + "rr_matrix0_filter_ne_zero_weak" : tactic + syntax (name := rr_row_threshold_matrix_named) "rr_row_threshold_matrix" " using " "n_pos" ":=" term "," @@ -283,6 +292,9 @@ syntax (name := rr_row_threshold_matrix0_filter_ne_zero_weak) term : tactic +syntax (name := rr_row_threshold_matrix0_filter_ne_zero_weak_inferred) + "rr_row_threshold_matrix0_filter_ne_zero_weak" : tactic + syntax (name := rr_row_threshold_matrix0_realrooted_named) "rr_row_threshold_matrix0_realrooted" " using " "matrix" ":=" term "," @@ -304,6 +316,9 @@ syntax (name := rr_row_threshold_matrix0_realrooted) term : tactic +syntax (name := rr_row_threshold_matrix0_realrooted_inferred) + "rr_row_threshold_matrix0_realrooted" : tactic + syntax (name := rr_row_threshold_matrix0_filter_ne_zero_named) "rr_row_threshold_matrix0_filter_ne_zero" " using " "matrix" ":=" term "," @@ -325,6 +340,9 @@ syntax (name := rr_row_threshold_matrix0_filter_ne_zero) term : tactic +syntax (name := rr_row_threshold_matrix0_filter_ne_zero_inferred) + "rr_row_threshold_matrix0_filter_ne_zero" : tactic + syntax (name := rr_row_threshold_entry_nonneg_named) "rr_row_threshold_entry_nonneg" " using " "row_threshold" ":=" term : @@ -358,6 +376,35 @@ macro_rules case hG_affine => rr_lookup [rr_matrix_2x2] case hfs => assumption case hfs_real => assumption)) + | `(tactic| rr_matrix0_realrooted) => + `(tactic| + exact (by + apply RealRooted.matrix_preserves_interlacing_seq0_of_2x2_realRooted + case hfs_len => assumption + case hG_rect => rr_lookup [rr_matrix_rect] + case hG_nonneg => rr_lookup [rr_matrix_nonneg] + case hG_affine => rr_lookup [rr_matrix_2x2] + case hfs => assumption)) + | `(tactic| rr_matrix0_filter_ne_zero) => + `(tactic| + exact (by + apply RealRooted.matrix_preserves_interlacing_seq0_filter_ne_zero_of_2x2 + case hfs_len => assumption + case hG_rect => rr_lookup [rr_matrix_rect] + case hG_nonneg => rr_lookup [rr_matrix_nonneg] + case hG_affine => rr_lookup [rr_matrix_2x2] + case hfs => assumption)) + | `(tactic| rr_matrix0_filter_ne_zero_weak) => + `(tactic| + exact (by + apply + RealRooted.matrix_preserves_interlacing_seq0_filter_ne_zero_of_2x2_weak + case hfs_len => assumption + case hG_rect => rr_lookup [rr_matrix_rect] + case hG_nonneg => rr_lookup [rr_matrix_nonneg] + case hG_affine => rr_lookup [rr_matrix_2x2] + case hfs => assumption + case hfs_real => assumption)) | `(tactic| rr_row_threshold_matrix0) => `(tactic| exact (by @@ -377,6 +424,37 @@ macro_rules case hG_affine => rr_lookup [rr_matrix_2x2] case hfs => assumption case hfs_real => assumption)) + | `(tactic| rr_row_threshold_matrix0_realrooted) => + `(tactic| + exact (by + apply + RealRooted.rowThreshold_matrix_preserves_interlacing_seq0_of_2x2_realRooted + case hfs_len => assumption + case hG_rect => rr_lookup [rr_matrix_rect] + case hG_threshold => rr_lookup [rr_matrix_threshold] + case hG_affine => rr_lookup [rr_matrix_2x2] + case hfs => assumption)) + | `(tactic| rr_row_threshold_matrix0_filter_ne_zero) => + `(tactic| + exact (by + apply + RealRooted.rowThreshold_matrix_preserves_interlacing_seq0_filter_ne_zero_of_2x2 + case hfs_len => assumption + case hG_rect => rr_lookup [rr_matrix_rect] + case hG_threshold => rr_lookup [rr_matrix_threshold] + case hG_affine => rr_lookup [rr_matrix_2x2] + case hfs => assumption)) + | `(tactic| rr_row_threshold_matrix0_filter_ne_zero_weak) => + `(tactic| + exact (by + apply + RealRooted.rowThreshold_matrix_preserves_interlacing_seq0_filter_ne_zero_of_2x2_weak + case hfs_len => assumption + case hG_rect => rr_lookup [rr_matrix_rect] + case hG_threshold => rr_lookup [rr_matrix_threshold] + case hG_affine => rr_lookup [rr_matrix_2x2] + case hfs => assumption + case hfs_real => assumption)) | `(tactic| rr_row_threshold_entry_nonneg) => `(tactic| rr_row_threshold_entry_nonneg using