From 62b21052d94604510ef4a1c206ab42a082229e2b Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Tue, 4 Aug 2026 09:21:38 +0000 Subject: [PATCH] Infer matrix preservation certificates --- RealRooted/Tactic/Examples/Lookup.lean | 44 +++++++++++ RealRooted/Tactic/Examples/Matrix.lean | 103 +++++++++++++++++++++++-- RealRooted/Tactic/Lookup.lean | 31 ++++++-- RealRooted/Tactic/Matrix.lean | 66 ++++++++++++++++ 4 files changed, 229 insertions(+), 15 deletions(-) diff --git a/RealRooted/Tactic/Examples/Lookup.lean b/RealRooted/Tactic/Examples/Lookup.lean index 56266fd5..a088034e 100644 --- a/RealRooted/Tactic/Examples/Lookup.lean +++ b/RealRooted/Tactic/Examples/Lookup.lean @@ -24,6 +24,50 @@ example : True := by example : True := by rr_lookup [rr_pos_lc] +def RRLookupSmokeRel {α : Type} (x : α) : Prop := x = x + +@[rr_matrix_rect] theorem rr_lookup_forall_smoke (m : ℕ) : + ∀ n : ℕ, RRLookupSmokeRel (n + m) := by + intro n + rfl + +example : ∀ n : ℕ, RRLookupSmokeRel (n + 3) := by + rr_lookup [rr_matrix_rect] + +@[rr_base_prec] theorem rr_lookup_full_forall_smoke : + ∀ n : ℕ, RRLookupSmokeRel n := by + intro n + rfl + +example : ∀ n : ℕ, RRLookupSmokeRel n := by + rr_lookup [rr_base_prec] + +@[rr_degree] theorem rr_lookup_determined_smoke : 37 = 37 := by + rfl + +@[rr_degree] theorem rr_lookup_partial_decoy_smoke (h : False) : 37 = 37 := by + contradiction + +example : 37 = 37 := by + rr_lookup [rr_degree] + +class RRLookupSmokeClass (α : Type) : Prop where + witness : True + +class RRLookupMissingClass (α : Type) : Prop where + witness : True + +instance : RRLookupSmokeClass ℕ := ⟨trivial⟩ + +@[rr_nonneg] theorem rr_lookup_missing_typeclass_decoy {α : Type} + [RRLookupMissingClass α] (x : α) : RRLookupSmokeRel x := rfl + +@[rr_nonneg] theorem rr_lookup_typeclass_smoke {α : Type} [RRLookupSmokeClass α] + (x : α) : RRLookupSmokeRel x := rfl + +example : RRLookupSmokeRel (37 : ℕ) := by + rr_lookup [rr_nonneg] + local syntax (name := rr_lookup_attr_macro_smoke) "rr_lookup_attr_macro_smoke" : tactic local macro_rules diff --git a/RealRooted/Tactic/Examples/Matrix.lean b/RealRooted/Tactic/Examples/Matrix.lean index 1ef6966c..72b72ca7 100644 --- a/RealRooted/Tactic/Examples/Matrix.lean +++ b/RealRooted/Tactic/Examples/Matrix.lean @@ -62,7 +62,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs_len : fs.length = n) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeq0Nonneg (matPolyAction G fs) := by - rr_matrix0 using G, hG_rect, hG_nonneg, hG_affine, fs, hfs_len, hfs + rr_matrix0 example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -178,8 +178,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : IsInterlacingSeq0Nonneg (matPolyAction G fs) ∧ ∀ f ∈ matPolyAction G fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := by - rr_matrix0_weak using - G, hG_rect, hG_nonneg, hG_affine, fs, hfs_len, hfs, hfs_real + rr_matrix0_weak example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -321,8 +320,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs_len : fs.length = n) (hfs : IsInterlacingSeqNonneg fs) : IsInterlacingSeq0Nonneg (matPolyAction G fs) := by - rr_row_threshold_matrix0 using - G, hG_rect, hG_threshold, hG_affine, fs, hfs_len, hfs + rr_row_threshold_matrix0 example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -364,8 +362,7 @@ example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hfs_real : ∀ f ∈ fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : IsInterlacingSeq0Nonneg (matPolyAction G fs) ∧ ∀ f ∈ matPolyAction G fs, f ≠ 0 → (f ≠ 0 ∧ f.Splits) := by - rr_row_threshold_matrix0_weak using - G, hG_rect, hG_threshold, hG_affine, fs, hfs_len, hfs, hfs_real + rr_row_threshold_matrix0_weak example {n : ℕ} (G : List (List ℝ[X])) (fs : List ℝ[X]) (hG_rect : ∀ row ∈ G, row.length = n) @@ -494,7 +491,97 @@ example {G : List (List ℝ[X])} example {G : List (List ℝ[X])} (hG_threshold : HasRowThresholdLinearStructure G) : ∀ row ∈ G, ∀ p ∈ row, HasNonnegCoeffs p := by - rr_row_threshold_entry_nonneg using hG_threshold + rr_row_threshold_entry_nonneg + +namespace MatrixInferenceSmoke + +def baseMatrix : List (List ℝ[X]) := [] + +def decoyMatrix : List (List ℝ[X]) := [[]] + +theorem baseMatrix_rect : ∀ row ∈ baseMatrix, row.length = 0 := by + simp [baseMatrix] + +theorem decoyMatrix_rect : ∀ row ∈ decoyMatrix, row.length = 0 := by + simp [decoyMatrix] + +theorem baseMatrix_wrongWidth_rect (h : False) : + ∀ row ∈ baseMatrix, row.length = 1 := by + contradiction + +theorem baseMatrix_nonneg : + ∀ row ∈ baseMatrix, ∀ p ∈ row, HasNonnegCoeffs p := by + simp [baseMatrix] + +theorem decoyMatrix_nonneg : + ∀ row ∈ decoyMatrix, ∀ p ∈ row, HasNonnegCoeffs p := by + simp [decoyMatrix] + +def ZeroWidthTwoByTwo (G : List (List ℝ[X])) : Prop := + ∀ (i₁ i₂ : Fin G.length) (j₁ j₂ : Fin 0), + i₁ ≤ i₂ → j₁ ≤ j₂ → + Has2x2InterlacingProperty0 + ((G.get i₁).get ⟨j₁, by exact Fin.elim0 j₁⟩) + ((G.get i₁).get ⟨j₂, by exact Fin.elim0 j₂⟩) + ((G.get i₂).get ⟨j₁, by exact Fin.elim0 j₁⟩) + ((G.get i₂).get ⟨j₂, by exact Fin.elim0 j₂⟩) + +theorem zeroWidth_twoByTwo (G : List (List ℝ[X])) : + ZeroWidthTwoByTwo G := by + unfold ZeroWidthTwoByTwo + intro _ _ j₁ + exact Fin.elim0 j₁ + +theorem baseMatrix_twoByTwo : ZeroWidthTwoByTwo baseMatrix := + zeroWidth_twoByTwo baseMatrix + +theorem decoyMatrix_twoByTwo : ZeroWidthTwoByTwo decoyMatrix := + zeroWidth_twoByTwo decoyMatrix + +theorem baseMatrix_threshold : HasRowThresholdLinearStructure baseMatrix := by + simp [HasRowThresholdLinearStructure, baseMatrix] + +theorem decoyMatrix_threshold : + HasRowThresholdLinearStructure decoyMatrix := by + refine ⟨fun _ => 0, ?_, ?_⟩ + · intro i + fin_cases i + simp [HasRowThreshold, decoyMatrix] + · intro i j _ + simp + +attribute [rr_matrix_rect] + baseMatrix_wrongWidth_rect baseMatrix_rect decoyMatrix_rect +attribute [rr_matrix_nonneg] baseMatrix_nonneg decoyMatrix_nonneg +attribute [rr_matrix_2x2] baseMatrix_twoByTwo decoyMatrix_twoByTwo +attribute [rr_matrix_threshold] baseMatrix_threshold decoyMatrix_threshold + +example (hfs_len : ([] : List ℝ[X]).length = 0) + (hfs : IsInterlacingSeqNonneg ([] : List ℝ[X])) : + IsInterlacingSeq0Nonneg (matPolyAction baseMatrix []) := by + rr_matrix0 + +example (hfs_len : ([] : List ℝ[X]).length = 0) + (hfs : IsInterlacingSeqNonneg ([] : List ℝ[X])) : + IsInterlacingSeq0Nonneg (matPolyAction decoyMatrix []) := by + rr_matrix0 + +example (hfs_len : ([] : List ℝ[X]).length = 0) + (hfs : IsInterlacingSeqNonneg ([] : List ℝ[X])) : + IsInterlacingSeq0Nonneg (matPolyAction baseMatrix []) := by + rr_row_threshold_matrix0 + +example (hfs_len : ([] : List ℝ[X]).length = 0) + (hfs : IsInterlacingSeq0Nonneg ([] : List ℝ[X])) + (hfs_real : ∀ f ∈ ([] : List ℝ[X]), f ≠ 0 → (f ≠ 0 ∧ f.Splits)) : + IsInterlacingSeq0Nonneg (matPolyAction baseMatrix []) ∧ + ∀ f ∈ matPolyAction baseMatrix [], f ≠ 0 → (f ≠ 0 ∧ f.Splits) := by + rr_matrix0_weak + +example : ∀ row ∈ baseMatrix, ∀ p ∈ row, HasNonnegCoeffs p := by + rr_row_threshold_entry_nonneg + +end MatrixInferenceSmoke end Tactic end RealRooted diff --git a/RealRooted/Tactic/Lookup.lean b/RealRooted/Tactic/Lookup.lean index c64d94ec..f522e5e3 100644 --- a/RealRooted/Tactic/Lookup.lean +++ b/RealRooted/Tactic/Lookup.lean @@ -38,15 +38,32 @@ def findLocalProofByType? (target : Expr) : TacticM (Option Expr) := return some (mkFVar ldecl.fvarId) return none +private def instantiateCertificateProof? (proof : Expr) : TacticM (Option Expr) := do + let proof ← instantiateMVars proof + return if proof.hasMVar then none else some proof + +private partial def mkProofFromPrefixFor? (proof proofType target : Expr) + (args : Array Expr) (binderInfos : Array BinderInfo) : + TacticM (Option Expr) := do + if ← isDefEq proofType target then + synthAppInstances `rr_lookup (← getMainGoal) args binderInfos + (synthAssignedInstances := false) (allowSynthFailures := true) + if let some proof ← instantiateCertificateProof? (mkAppN proof args) then + return some proof + let (newArgs, newBinderInfos, conclusion) ← + forallMetaBoundedTelescope proofType 1 + if newArgs.isEmpty then + return none + mkProofFromPrefixFor? proof conclusion target (args ++ newArgs) + (binderInfos ++ newBinderInfos) + def mkProofFromDeclFor? (decl : Name) (target : Expr) : TacticM (Option Expr) := withMainContext do - withNewMCtxDepth do - let proof ← mkConstWithFreshMVarLevels decl - let (args, _, conclusion) ← forallMetaTelescopeReducing (← inferType proof) - if ← isDefEq conclusion target then - return some (← instantiateMVars (mkAppN proof args)) - else - return none + withoutModifyingState do + withNewMCtxDepth do + let proof ← mkConstWithFreshMVarLevels decl + let proofType ← inferType proof + mkProofFromPrefixFor? proof proofType target #[] #[] def findTaggedProofsByType (attr : Lean.TagAttribute) (target : Expr) : TacticM (Array (Name × Expr)) := do diff --git a/RealRooted/Tactic/Matrix.lean b/RealRooted/Tactic/Matrix.lean index ebddc558..e8593f37 100644 --- a/RealRooted/Tactic/Matrix.lean +++ b/RealRooted/Tactic/Matrix.lean @@ -1,6 +1,7 @@ import RealRooted.MatrixInterlacing import RealRooted.RowThreshold import RealRooted.StaircaseSum +import RealRooted.Tactic.Lookup import RealRooted.Tactic.SideGoals /-! @@ -15,10 +16,13 @@ rr_matrix0_weak rr_matrix0_realrooted rr_matrix0_filter_ne_zero rr_matrix0_filter_ne_zero_weak +rr_row_threshold_matrix +rr_row_threshold_matrix0 rr_row_threshold_matrix0_weak rr_row_threshold_matrix0_realrooted rr_row_threshold_matrix0_filter_ne_zero rr_row_threshold_matrix0_filter_ne_zero_weak +rr_row_threshold_entry_nonneg ``` Primary target: @@ -33,6 +37,12 @@ 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 +certificate attributes. The bare `rr_row_threshold_entry_nonneg` form infers +its matrix from the target. + Family J warning: do not attack raw scalar long-lag recurrences. First derive a refined vector or production-matrix recurrence. @@ -85,6 +95,8 @@ syntax (name := rr_matrix0_named) "input_interlacing" ":=" term : tactic +syntax (name := rr_matrix0_inferred) "rr_matrix0" : tactic + syntax (name := rr_matrix0_weak) "rr_matrix0_weak" " using " term ", " term ", " @@ -108,6 +120,8 @@ syntax (name := rr_matrix0_weak_named) "input_real_rooted" ":=" term : tactic +syntax (name := rr_matrix0_weak_inferred) "rr_matrix0_weak" : tactic + syntax (name := rr_matrix0_realrooted) "rr_matrix0_realrooted" " using " term ", " term ", " @@ -217,6 +231,9 @@ syntax (name := rr_row_threshold_matrix0) term : tactic +syntax (name := rr_row_threshold_matrix0_inferred) + "rr_row_threshold_matrix0" : tactic + syntax (name := rr_row_threshold_matrix0_weak_named) "rr_row_threshold_matrix0_weak" " using " "matrix" ":=" term "," @@ -240,6 +257,9 @@ syntax (name := rr_row_threshold_matrix0_weak) term : tactic +syntax (name := rr_row_threshold_matrix0_weak_inferred) + "rr_row_threshold_matrix0_weak" : tactic + syntax (name := rr_row_threshold_matrix0_filter_ne_zero_weak_named) "rr_row_threshold_matrix0_filter_ne_zero_weak" " using " "matrix" ":=" term "," @@ -314,7 +334,53 @@ syntax (name := rr_row_threshold_entry_nonneg) "rr_row_threshold_entry_nonneg" " using " term : tactic +syntax (name := rr_row_threshold_entry_nonneg_inferred) + "rr_row_threshold_entry_nonneg" : tactic + +-- The local length proof fixes the hidden width before frozen attribute lookup. macro_rules + | `(tactic| rr_matrix0) => + `(tactic| + exact (by + apply RealRooted.matrix_preserves_interlacing_seq0_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_weak) => + `(tactic| + exact (by + apply RealRooted.matrix_preserves_interlacing_seq0_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 + apply RealRooted.rowThreshold_matrix_preserves_interlacing_seq0_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_weak) => + `(tactic| + exact (by + apply RealRooted.rowThreshold_matrix_preserves_interlacing_seq0_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 + row_threshold := (by rr_lookup [rr_matrix_threshold])) | `(tactic| rr_matrix using $hn:term, $G:term, $hG_rect:term, $hG_nonneg:term, $hG_affine:term,