Merge pull request #28 from zksecurity/feat/specialize-auto-tactic

Add specialize_auto tactic

Clean/Tables/Fibonacci.lean

@@ -8,6 +8,7 @@ import Mathlib.NumberTheory.LucasLehmer
 import Clean.Gadgets.Addition8
 import Clean.Gadgets.Equality
 import Clean.Table
+import Clean.Utils.Tactics
 
 section FibonacciTable
 open Expression
@@ -104,7 +105,7 @@ def fibonacciTable : Table 3 M p := {
     · simp
       simp at ih2
       intro lookup_next lookup_curr lookup_rest
-      specialize ih2 lookup_curr lookup_rest
+      specialize_auto ih2
       simp [fullTableConstraintSet.foldl, fib8, TraceOfLength.eval]
       simp [forallList, fullConstraintSet, fullConstraintSet.foldl]
 
@@ -172,7 +173,7 @@ def fibonacciTable : Table 3 M p := {
           := by
           have add_relation := Addition8.equiv 3 M (A curr) (B curr) (B next) (carry curr) trace
           simp [ByteLookup.lookup, TraceOfLength.eval, Addition8.spec] at add_relation
-          specialize add_relation lookup_first lookup_curr lookup_next
+          specialize_auto add_relation
 
           -- and now we reason about fib
           have add_input := And.intro c1 c2
@@ -198,7 +199,7 @@ def fibonacciTable : Table 3 M p := {
 
         have add_relation := Addition8.equiv 3 M (A curr) (B curr) (B next) (carry curr) trace
         simp [ByteLookup.lookup, TraceOfLength.eval, Addition8.spec] at add_relation
-        specialize add_relation lookup_first lookup_curr lookup_next
+        specialize_auto add_relation
 
         nth_rewrite 1 [fib_curr0] at add_relation
         nth_rewrite 1 [fib_curr1] at add_relation

Clean/Utils/Tactics.lean

@@ -0,0 +1,59 @@
+import Lean.Elab.Tactic
+import Lean.Elab.Exception
+
+open Lean.Elab.Tactic
+open Lean.Meta
+
+
+partial def get_max_matching_hyp (e : Lean.Expr) : Lean.Elab.Tactic.TacticM (List Lean.Expr) := do
+  -- it suffices to reduce to whnf to look at the outer structure
+  let e ← whnf e
+  match e with
+  | (.forallE _ typ body _) => do
+    -- dependent function type, search the context for a matching hypothesis
+    let ctx ← Lean.MonadLCtx.getLCtx
+    let option_matching_expr ← ctx.findDeclM? fun decl: Lean.LocalDecl => do
+      let declExpr := decl.toExpr
+      let declType ← Lean.Meta.inferType declExpr
+      if ← Lean.Meta.isExprDefEq declType typ
+        then return Option.some declExpr
+        else return Option.none
+
+    -- if we found one, keep it and recurse on the body
+    match option_matching_expr with
+    | some res => do
+      let other_hyps ← get_max_matching_hyp body
+      return [res] ++ other_hyps
+    | none => do return []
+  | _ => return []
+
+
+partial def specializeAuto (e_term : Lean.Term): Lean.Elab.Tactic.TacticM Unit := do
+  let (e, mvarIds') ← elabTermWithHoles e_term none `specialize_auto (allowNaturalHoles := true)
+
+  -- e must be a free variable in the local context
+  if e.isFVar then
+    let localDecl ← e.fvarId!.getDecl
+    let declType ← Lean.Meta.inferType localDecl.toExpr
+
+    -- get the maximum number of matching hypotheses
+    let matching ← get_max_matching_hyp declType
+
+    -- construct an application expr `t e1 e2 ... en` where `t` is the term we want to specialize
+    let h' := Lean.mkAppN e matching.toArray
+
+    -- replace the term with the specialized term
+    let goal ← getMainGoal
+    let mvarId ← goal.assert (← e.fvarId!.getDecl).userName (← inferType h').headBeta h'
+    let (_, mvarId) ← mvarId.intro1P
+    let mvarId ← mvarId.tryClear e.fvarId!
+    replaceMainGoal (mvarIds' ++ [mvarId])
+  else
+    throwError "'specialize_auto' requires a term that appears in the local context"
+
+/--
+  Takes in input a term `t` which must be present in the context. If `t` is of the form
+  `h1 -> h2 -> ... -> hn -> t'`, it searches in the context for `h1`, `h2`, ..., `hn` and
+  specializess it with them.
+-/
+elab "specialize_auto" e:term : tactic => withMainContext do specializeAuto e