Skip to content

Commit

Permalink
fix ordering of used theorem in fun_trans
Browse files Browse the repository at this point in the history
  • Loading branch information
lecopivo committed Oct 3, 2024
1 parent 11a6bd1 commit 145ab7f
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion SciLean/Tactic/FunTrans/Theorems.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import Batteries.Data.RBMap.Alter

import SciLean.Tactic.FunTrans.Decl
import Mathlib.Tactic.FunProp.Theorems
import SciLean.Lean.Array

/-!
## `fun_trans` enviroment extensions storing thorems for `fun_trans`
Expand Down Expand Up @@ -226,6 +227,13 @@ initialize functionTheoremsExt : FunctionTheoremsExt ←
}


def FunctionTheorem.ord (t s : FunctionTheorem) : Ordering :=

let tl := #[t.appliedArgs, t.mainArgs.size, t.transAppliedArgs]
let sl := #[s.appliedArgs, s.mainArgs.size, s.transAppliedArgs]

tl.lexOrd sl

/-- -/
def getTheoremsForFunction (funName : Name) (funTransName : Name) (nargs : Option Nat) (mainArgs : Option (Array ℕ)) :
CoreM (Array FunctionTheorem) := do
Expand All @@ -238,7 +246,7 @@ def getTheoremsForFunction (funName : Name) (funTransName : Name) (nargs : Optio
(nargs.map (fun n => (thm.transAppliedArgs ≤ n : Bool))).getD true
&&
(mainArgs.map (fun args => FunProp.isOrderedSubsetOf args thm.mainArgs)).getD true)
|>.qsort (fun t t' => t'.transAppliedArgs < t.transAppliedArgs)
|>.qsort (fun t t' => t.ord t' == .lt)

return thms

Expand Down

0 comments on commit 145ab7f

Please sign in to comment.