Infer local Favard certificates

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)) :

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

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) =>

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