Infer matrix preservation certificates

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

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

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

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,