From 937735d7963709228e78dd09f713366fba0315fb Mon Sep 17 00:00:00 2001
From: Per Alexandersson <per.w.alexandersson@gmail.com>
Date: Tue, 4 Aug 2026 08:18:11 +0000
Subject: [PATCH] Infer local Favard certificates

---
 RealRooted/Tactic/Examples/Favard.lean | 17 +++++++++++++++++
 RealRooted/Tactic/Examples/Lookup.lean | 13 +++++++++++++
 RealRooted/Tactic/Favard.lean          | 17 +++++++++++++++++
 RealRooted/Tactic/Lookup.lean          |  5 +++--
 4 files changed, 50 insertions(+), 2 deletions(-)

diff --git a/RealRooted/Tactic/Examples/Favard.lean b/RealRooted/Tactic/Examples/Favard.lean
index 8341ec25..49111d6c 100644
--- a/RealRooted/Tactic/Examples/Favard.lean
+++ b/RealRooted/Tactic/Examples/Favard.lean
@@ -35,6 +35,23 @@ example {P : Nat → ℝ[X]} {α β : Nat → ℝ}
     ∀ n : Nat, Prec (P n) (P (n + 1)) := by
   rr_favard using hrec, hbeta
 
+/-- Exact local inference ignores an unrelated Favard certificate packet. -/
+example {P Q : Nat → ℝ[X]} {α β γ δ : Nat → ℝ}
+    (_hrecDecoy : SatisfiesFavardRecurrence Q γ δ)
+    -- This guards against the positivity proof fixing the wrong coefficient sequence.
+    (_hbetaDecoy : ∀ n : Nat, 0 < δ (n + 1))
+    (hrec : SatisfiesFavardRecurrence P α β)
+    (hbeta : ∀ n : Nat, 0 < β (n + 1)) :
+    ∀ n : Nat, Prec (P n) (P (n + 1)) := by
+  rr_favard
+
+/-- The inferred auto form retains positivity automation. -/
+example {P Q : Nat → ℝ[X]} {γ δ : Nat → ℝ}
+    (_hrecDecoy : SatisfiesFavardRecurrence Q γ δ)
+    (hrec : SatisfiesFavardRecurrence P (fun _ => 0) (fun _ => 1)) :
+    ∀ n : Nat, (P n).Splits := by
+  rr_favard_auto
+
 example {P : Nat → ℝ[X]} {α β : Nat → ℝ}
     (hrec : SatisfiesFavardRecurrence P α β)
     (hbeta : ∀ n : Nat, 0 < β (n + 1)) :
diff --git a/RealRooted/Tactic/Examples/Lookup.lean b/RealRooted/Tactic/Examples/Lookup.lean
index 1f960ba0..56266fd5 100644
--- a/RealRooted/Tactic/Examples/Lookup.lean
+++ b/RealRooted/Tactic/Examples/Lookup.lean
@@ -24,5 +24,18 @@ example : True := by
 example : True := by
   rr_lookup [rr_pos_lc]
 
+local syntax (name := rr_lookup_attr_macro_smoke) "rr_lookup_attr_macro_smoke" : tactic
+
+local macro_rules
+  | `(tactic| rr_lookup_attr_macro_smoke) =>
+      `(tactic| rr_lookup [rr_pos_lc])
+
+example : True := by
+  rr_lookup_attr_macro_smoke
+
+example (h : True) : True := by
+  fail_if_success rr_lookup [rr_missing_attr]
+  exact h
+
 end Tactic
 end RealRooted
diff --git a/RealRooted/Tactic/Favard.lean b/RealRooted/Tactic/Favard.lean
index 779fde95..7316f7c1 100644
--- a/RealRooted/Tactic/Favard.lean
+++ b/RealRooted/Tactic/Favard.lean
@@ -11,13 +11,17 @@ open Polynomial
 The tactic
 
 ```lean
+rr_favard
 rr_favard using hrec, hbeta
+rr_favard_auto
 ```
 
 applies the already-formalized Favard interface to goals that match
 `favardInterlacing`,
 `isRealRooted_of_favard`, or
 `isGeneralizedSturmSeq_reverse_range_map_of_favard`.
+The bare forms infer exact local recurrence and positivity hypotheses. Use an
+explicit `using` form when more than one Favard certificate packet is in scope.
 
 First intended regression examples:
 
@@ -1111,6 +1115,8 @@ macro_rules
               | simp))
 syntax (name := rr_favard) "rr_favard" " using " term ", " term : tactic
 
+syntax (name := rr_favard_inferred) "rr_favard" : tactic
+
 syntax (name := rr_favard_named)
   "rr_favard" " using "
     "recurrence" ":=" term ","
@@ -1122,6 +1128,8 @@ syntax (name := rr_favard_auto_named)
     "recurrence" ":=" term :
   tactic
 
+syntax (name := rr_favard_auto_inferred) "rr_favard_auto" : tactic
+
 syntax (name := rr_favard_const)
   "rr_favard_const" " using " term ", " term ", " term ", " term ", " term ", " term :
   tactic
@@ -2167,6 +2175,15 @@ syntax (name := rr_favard_exact_realrooted_positivity_seq)
   tactic
 
 macro_rules
+  | `(tactic| rr_favard) =>
+      `(tactic|
+        rr_favard using
+          recurrence := (by assumption),
+          beta_pos := (by assumption))
+  | `(tactic| rr_favard_auto) =>
+      `(tactic|
+        rr_favard_auto using
+          recurrence := (by assumption))
   | `(tactic| rr_favard_refine_positivity_seq $h:term) =>
       `(tactic| rr_refine_then $h with rr_positivity_seq)
   | `(tactic| rr_favard_exact_realrooted_positivity_seq $h:term) =>
diff --git a/RealRooted/Tactic/Lookup.lean b/RealRooted/Tactic/Lookup.lean
index d2725398..c64d94ec 100644
--- a/RealRooted/Tactic/Lookup.lean
+++ b/RealRooted/Tactic/Lookup.lean
@@ -93,12 +93,13 @@ elab_rules : tactic
         closeWithTaggedMatches found
   | `(tactic| rr_lookup [ $attrName:ident ]) =>
       withMainContext do
+        let attrName := attrName.getId.eraseMacroScopes
+        let some attr := certificateAttrByName? attrName
+          | throwError "rr_lookup failed: unknown certificate attribute [{attrName}]"
         let target ← getMainTarget
         if let some proof ← findLocalProofByType? target then
           closeMainGoal `rr_lookup proof
           return
-        let some attr := certificateAttrByName? attrName.getId
-          | throwError "rr_lookup failed: unknown certificate attribute [{attrName.getId}]"
         closeWithTaggedMatches (← findTaggedProofsByType attr target)
 
 end Tactic