diff options
author | Son HO | 2023-07-31 16:15:58 +0200 |
---|---|---|
committer | GitHub | 2023-07-31 16:15:58 +0200 |
commit | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (patch) | |
tree | 92d6021eb549f7cc25501856edd58859786b7e90 /backends/lean/Base/Utils.lean | |
parent | 53adf30fe440eb8b6f58ba89f4a4c0acc7877498 (diff) | |
parent | 9b3a58e423333fc9a4a5a264c3beb0a3d951e86b (diff) |
Merge pull request #31 from AeneasVerif/son_lean_backend
Improve the Lean backend
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Utils.lean | 640 |
1 files changed, 640 insertions, 0 deletions
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean new file mode 100644 index 00000000..1f8f1455 --- /dev/null +++ b/backends/lean/Base/Utils.lean @@ -0,0 +1,640 @@ +import Lean +import Mathlib.Tactic.Core +import Mathlib.Tactic.LeftRight +import Base.UtilsBase + +/- +Mathlib tactics: +- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases +- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs +- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num +- should we use linarith or omega? +- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint +- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical +-/ + +/- +TODO: +- we want an easier to use cases: + - keeps in the goal an equation of the shape: `t = case` + - if called on Prop terms, uses Classical.em + Actually, the cases from mathlib seems already quite powerful + (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases) + For instance: cases h : e + Also: **casesm** +- better split tactic +- we need conversions to operate on the head of applications. + Actually, something like this works: + ``` + conv at Hl => + apply congr_fun + simp [fix_fuel_P] + ``` + Maybe we need a rpt ... ; focus? +- simplifier/rewriter have a strange behavior sometimes +-/ + + +namespace List + + -- TODO: I could not find this function?? + @[simp] def flatten {a : Type u} : List (List a) → List a + | [] => [] + | x :: ls => x ++ flatten ls + +end List + +-- TODO: move? +@[simp] +theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all + +namespace Lean + +namespace LocalContext + + open Lean Lean.Elab Command Term Lean.Meta + + -- Small utility: return the list of declarations in the context, from + -- the last to the first. + def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := + lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) [] + + -- Return the list of declarations in the context, but filter the + -- declarations which are considered as implementation details + def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do + let ls ← lctx.getAllDecls + pure (ls.filter (fun d => not d.isImplementationDetail)) + +end LocalContext + +end Lean + +namespace Utils + +open Lean Elab Term Meta Tactic + +-- Useful helper to explore definitions and figure out the variant +-- of their sub-expressions. +def explore_term (incr : String) (e : Expr) : MetaM Unit := + match e with + | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return () + | .fvar _ => do logInfo m!"{incr}fvar: {e}"; return () + | .mvar _ => do logInfo m!"{incr}mvar: {e}"; return () + | .sort _ => do logInfo m!"{incr}sort: {e}"; return () + | .const _ _ => do logInfo m!"{incr}const: {e}"; return () + | .app fn arg => do + logInfo m!"{incr}app: {e}" + explore_term (incr ++ " ") fn + explore_term (incr ++ " ") arg + | .lam _bName bTy body _binfo => do + logInfo m!"{incr}lam: {e}" + explore_term (incr ++ " ") bTy + explore_term (incr ++ " ") body + | .forallE _bName bTy body _bInfo => do + logInfo m!"{incr}forallE: {e}" + explore_term (incr ++ " ") bTy + explore_term (incr ++ " ") body + | .letE _dName ty val body _nonDep => do + logInfo m!"{incr}letE: {e}" + explore_term (incr ++ " ") ty + explore_term (incr ++ " ") val + explore_term (incr ++ " ") body + | .lit _ => do logInfo m!"{incr}lit: {e}"; return () + | .mdata _ e => do + logInfo m!"{incr}mdata: {e}" + explore_term (incr ++ " ") e + | .proj _ _ struct => do + logInfo m!"{incr}proj: {e}" + explore_term (incr ++ " ") struct + +def explore_decl (n : Name) : TermElabM Unit := do + logInfo m!"Name: {n}" + let env ← getEnv + let decl := env.constants.find! n + match decl with + | .defnInfo val => + logInfo m!"About to explore defn: {decl.name}" + logInfo m!"# Type:" + explore_term "" val.type + logInfo m!"# Value:" + explore_term "" val.value + | .axiomInfo _ => throwError m!"axiom: {n}" + | .thmInfo _ => throwError m!"thm: {n}" + | .opaqueInfo _ => throwError m!"opaque: {n}" + | .quotInfo _ => throwError m!"quot: {n}" + | .inductInfo _ => throwError m!"induct: {n}" + | .ctorInfo _ => throwError m!"ctor: {n}" + | .recInfo _ => throwError m!"rec: {n}" + +syntax (name := printDecl) "print_decl " ident : command + +open Lean.Elab.Command + +@[command_elab printDecl] def elabPrintDecl : CommandElab := fun stx => do + liftTermElabM do + let id := stx[1] + addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none + let cs ← resolveGlobalConstWithInfos id + explore_decl cs[0]! + +private def test1 : Nat := 0 +private def test2 (x : Nat) : Nat := x +print_decl test1 +print_decl test2 + +def printDecls (decls : List LocalDecl) : MetaM Unit := do + let decls ← decls.foldrM (λ decl msg => do + pure (m!"\n{decl.toExpr} : {← inferType decl.toExpr}" ++ msg)) m!"" + logInfo m!"# Ctx decls:{decls}" + +-- Small utility: print all the declarations in the context (including the "implementation details") +elab "print_all_ctx_decls" : tactic => do + let ctx ← Lean.MonadLCtx.getLCtx + let decls ← ctx.getAllDecls + printDecls decls + +-- Small utility: print all declarations in the context +elab "print_ctx_decls" : tactic => do + let ctx ← Lean.MonadLCtx.getLCtx + let decls ← ctx.getDecls + printDecls decls + +-- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`) +-- The continuation takes as parameters: +-- - the current depth of the expression (useful for printing/debugging) +-- - the expression to explore +partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr := do + let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do + let localInstances ← getLocalInstances + let mut lctx ← getLCtx + for x in xs do + let xFVarId := x.fvarId! + let localDecl ← xFVarId.getDecl + let type ← mapVisit k localDecl.type + let localDecl := localDecl.setType type + let localDecl ← match localDecl.value? with + | some value => let value ← mapVisit k value; pure <| localDecl.setValue value + | none => pure localDecl + lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl + withLCtx lctx localInstances k2 + -- TODO: use a cache? (Lean.checkCache) + let rec visit (i : Nat) (e : Expr) : MetaM Expr := do + -- Explore + let e ← k i e + match e with + | .bvar _ + | .fvar _ + | .mvar _ + | .sort _ + | .lit _ + | .const _ _ => pure e + | .app .. => do e.withApp fun f args => return mkAppN f (← args.mapM (visit (i + 1))) + | .lam .. => + lambdaLetTelescope e fun xs b => + mapVisitBinders xs do mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false) + | .forallE .. => do + forallTelescope e fun xs b => mapVisitBinders xs do mkForallFVars xs (← visit (i + 1) b) + | .letE .. => do + lambdaLetTelescope e fun xs b => mapVisitBinders xs do + mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false) + | .mdata _ b => return e.updateMData! (← visit (i + 1) b) + | .proj _ _ b => return e.updateProj! (← visit (i + 1) b) + visit 0 e + +-- Generate a fresh user name for an anonymous proposition to introduce in the +-- assumptions +def mkFreshAnonPropUserName := mkFreshUserName `_ + +section Methods + variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m] + variable {a : Type} + + /- Like `lambdaTelescopeN` but only destructs a fixed number of lambdas -/ + def lambdaTelescopeN (e : Expr) (n : Nat) (k : Array Expr → Expr → m a) : m a := + lambdaTelescope e fun xs body => do + if xs.size < n then throwError "lambdaTelescopeN: not enough lambdas" + let xs := xs.extract 0 n + let ys := xs.extract n xs.size + let body ← liftMetaM (mkLambdaFVars ys body) + k xs body + + /- Like `lambdaTelescope`, but only destructs one lambda + TODO: is there an equivalent of this function somewhere in the + standard library? -/ + def lambdaOne (e : Expr) (k : Expr → Expr → m a) : m a := + lambdaTelescopeN e 1 λ xs b => k (xs.get! 0) b + + def isExists (e : Expr) : Bool := e.getAppFn.isConstOf ``Exists ∧ e.getAppNumArgs = 2 + + -- Remark: Lean doesn't find the inhabited and nonempty instances if we don' + -- put them explicitely in the signature + partial def existsTelescopeProcess [Inhabited (m a)] [Nonempty (m a)] + (fvars : Array Expr) (e : Expr) (k : Array Expr → Expr → m a) : m a := do + -- Attempt to deconstruct an existential + if isExists e then do + let p := e.appArg! + lambdaOne p fun x ne => + existsTelescopeProcess (fvars.push x) ne k + else + -- No existential: call the continuation + k fvars e + + def existsTelescope [Inhabited (m a)] [Nonempty (m a)] (e : Expr) (k : Array Expr → Expr → m a) : m a := do + existsTelescopeProcess #[] e k + +end Methods + +-- TODO: this should take a continuation +def addDeclTac (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : TacticM Expr := + -- I don't think we need that + withMainContext do + -- Insert the new declaration + let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type + withDecl fun nval => do + -- For debugging + let lctx ← Lean.MonadLCtx.getLCtx + let fid := nval.fvarId! + let decl := lctx.get! fid + trace[Arith] " new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" + -- + -- Tranform the main goal `?m0` to `let x = nval in ?m1` + let mvarId ← getMainGoal + let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType) + let newVal ← mkLetFVars #[nval] newMVar + -- There are two cases: + -- - asLet is true: newVal is `let $name := $val in $newMVar` + -- - asLet is false: ewVal is `λ $name => $newMVar` + -- We need to apply it to `val` + let newVal := if asLet then newVal else mkAppN newVal #[val] + -- Assign the main goal and update the current goal + mvarId.assign newVal + let goals ← getUnsolvedGoals + setGoals (newMVar.mvarId! :: goals) + -- Return the new value - note: we are in the *new* context, created + -- after the declaration was added, so it will persist + pure nval + +def addDeclTacSyntax (name : Name) (val : Syntax) (asLet : Bool) : TacticM Unit := + -- I don't think we need that + withMainContext do + -- + let val ← Term.elabTerm val .none + let type ← inferType val + -- In some situations, the type will be left as a metavariable (for instance, + -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will + -- not choose): we force the instantiation of the meta-variable + synthesizeSyntheticMVarsUsingDefault + -- + let _ ← addDeclTac name val type asLet + +elab "custom_let " n:ident " := " v:term : tactic => do + addDeclTacSyntax n.getId v (asLet := true) + +elab "custom_have " n:ident " := " v:term : tactic => + addDeclTacSyntax n.getId v (asLet := false) + +example : Nat := by + custom_let x := 4 + custom_have y := 4 + apply y + +example (x : Bool) : Nat := by + cases x <;> custom_let x := 3 <;> apply x + +-- Repeatedly apply a tactic +partial def repeatTac (tac : TacticM Unit) : TacticM Unit := do + try + tac + allGoals (focus (repeatTac tac)) + -- TODO: does this restore the state? + catch _ => pure () + +def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do + match tacl with + | [] => pure () + | tac :: tacl => + -- Should use try ... catch or Lean.observing? + -- Generally speaking we should use Lean.observing? to restore the state, + -- but with tactics the try ... catch variant seems to work + try do + tac + -- Check that there are no remaining goals + let gl ← Tactic.getUnsolvedGoals + if ¬ gl.isEmpty then throwError "tactic failed" + catch _ => firstTac tacl +/- let res ← Lean.observing? do + tac + -- Check that there are no remaining goals + let gl ← Tactic.getUnsolvedGoals + if ¬ gl.isEmpty then throwError "tactic failed" + match res with + | some _ => pure () + | none => firstTac tacl -/ + +-- Taken from Lean.Elab.evalAssumption +def assumptionTac : TacticM Unit := + liftMetaTactic fun mvarId => do mvarId.assumption; pure [] + +def isConj (e : Expr) : MetaM Bool := + e.consumeMData.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2) + +-- Return the first conjunct if the expression is a conjunction, or the +-- expression itself otherwise. Also return the second conjunct if it is a +-- conjunction. +def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do + e.consumeMData.withApp fun f args => + if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1)) + else pure (e, none) + +-- Split the goal if it is a conjunction +def splitConjTarget : TacticM Unit := do + withMainContext do + let g ← getMainTarget + trace[Utils] "splitConjTarget: goal: {g}" + -- The tactic was initially implemened with `_root_.Lean.MVarId.apply` + -- but it tended to mess the goal by unfolding terms, even when it failed + let (l, r) ← optSplitConj g + match r with + | none => do throwError "The goal is not a conjunction" + | some r => do + let lmvar ← mkFreshExprSyntheticOpaqueMVar l + let rmvar ← mkFreshExprSyntheticOpaqueMVar r + let and_intro ← mkAppM ``And.intro #[lmvar, rmvar] + let g ← getMainGoal + g.assign and_intro + let goals ← getUnsolvedGoals + setGoals (lmvar.mvarId! :: rmvar.mvarId! :: goals) + +-- Destruct an equaliy and return the two sides +def destEq (e : Expr) : MetaM (Expr × Expr) := do + e.withApp fun f args => + if f.isConstOf ``Eq ∧ args.size = 3 then pure (args.get! 1, args.get! 2) + else throwError "Not an equality: {e}" + +-- Return the set of FVarIds in the expression +partial def getFVarIds (e : Expr) (hs : HashSet FVarId := HashSet.empty) : MetaM (HashSet FVarId) := do + e.withApp fun body args => do + let hs := if body.isFVar then hs.insert body.fvarId! else hs + args.foldlM (fun hs arg => getFVarIds arg hs) hs + +-- Tactic to split on a disjunction. +-- The expression `h` should be an fvar. +-- TODO: there must be simpler. Use use _root_.Lean.MVarId.cases for instance +def splitDisjTac (h : Expr) (kleft kright : TacticM Unit) : TacticM Unit := do + trace[Arith] "assumption on which to split: {h}" + -- Retrieve the main goal + withMainContext do + let goalType ← getMainTarget + let hDecl := (← getLCtx).get! h.fvarId! + let hName := hDecl.userName + -- Case disjunction + let hTy ← inferType h + hTy.withApp fun f xs => do + trace[Arith] "as app: {f} {xs}" + -- Sanity check + if ¬ (f.isConstOf ``Or ∧ xs.size = 2) then throwError "Invalid argument to splitDisjTac" + let a := xs.get! 0 + let b := xs.get! 1 + -- Introduce the new goals + -- Returns: + -- - the match branch + -- - a fresh new mvar id + let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do + -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse + -- the name of the assumption we split. + withLocalDeclD hName hTy fun var => do + -- The new goal + let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName) + -- Clear the assumption that we split + let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!] + -- The branch expression + let branch ← mkLambdaFVars #[var] (mkMVar mgoal) + pure (branch, mgoal) + let (inl, mleft) ← mkGoal a "left" + let (inr, mright) ← mkGoal b "right" + trace[Arith] "left: {inl}: {mleft}" + trace[Arith] "right: {inr}: {mright}" + -- Create the match expression + withLocalDeclD (← mkFreshAnonPropUserName) hTy fun hVar => do + let motive ← mkLambdaFVars #[hVar] goalType + let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr] + let mgoal ← getMainGoal + trace[Arith] "goals: {← getUnsolvedGoals}" + trace[Arith] "main goal: {mgoal}" + mgoal.assign casesExpr + let goals ← getUnsolvedGoals + -- Focus on the left + setGoals [mleft] + withMainContext kleft + let leftGoals ← getUnsolvedGoals + -- Focus on the right + setGoals [mright] + withMainContext kright + let rightGoals ← getUnsolvedGoals + -- Put all the goals back + setGoals (leftGoals ++ rightGoals ++ goals) + trace[Arith] "new goals: {← getUnsolvedGoals}" + +elab "split_disj " n:ident : tactic => do + withMainContext do + let decl ← Lean.Meta.getLocalDeclFromUserName n.getId + let fvar := mkFVar decl.fvarId + splitDisjTac fvar (fun _ => pure ()) (fun _ => pure ()) + +example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by + split_disj h0 + . left; assumption + . right; assumption + + +-- Tactic to split on an exists. +-- `h` must be an FVar +def splitExistsTac (h : Expr) (optId : Option Name) (k : Expr → Expr → TacticM α) : TacticM α := do + withMainContext do + let goal ← getMainGoal + let hTy ← inferType h + if isExists hTy then do + -- Try to use the user-provided names + let altVarNames ← do + let hDecl ← h.fvarId!.getDecl + let id ← do + match optId with + | none => mkFreshUserName `x + | some id => pure id + pure #[{ varNames := [id, hDecl.userName] }] + let newGoals ← goal.cases h.fvarId! altVarNames + -- There should be exactly one goal + match newGoals.toList with + | [ newGoal ] => + -- Set the new goal + let goals ← getUnsolvedGoals + setGoals (newGoal.mvarId :: goals) + -- There should be exactly two fields + let fields := newGoal.fields + withMainContext do + k (fields.get! 0) (fields.get! 1) + | _ => + throwError "Unreachable" + else + throwError "Not a conjunction" + +-- TODO: move +def listTryPopHead (ls : List α) : Option α × List α := + match ls with + | [] => (none, ls) + | hd :: tl => (some hd, tl) + +/- Destruct all the existentials appearing in `h`, and introduce them as variables + in the context. + + If `ids` is not empty, we use it to name the introduced variables. We + transmit the stripped expression and the remaining ids to the continuation. + -/ +partial def splitAllExistsTac [Inhabited α] (h : Expr) (ids : List (Option Name)) (k : Expr → List (Option Name) → TacticM α) : TacticM α := do + try + let (optId, ids) := + match ids with + | [] => (none, []) + | x :: ids => (x, ids) + splitExistsTac h optId (fun _ body => splitAllExistsTac body ids k) + catch _ => k h ids + +-- Tactic to split on a conjunction. +def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr → TacticM α) : TacticM α := do + withMainContext do + let goal ← getMainGoal + let hTy ← inferType h + if ← isConj hTy then do + -- Try to use the user-provided names + let altVarNames ← + match optIds with + | none => do + let id0 ← mkFreshAnonPropUserName + let id1 ← mkFreshAnonPropUserName + pure #[{ varNames := [id0, id1] }] + | some (id0, id1) => do + pure #[{ varNames := [id0, id1] }] + let newGoals ← goal.cases h.fvarId! altVarNames + -- There should be exactly one goal + match newGoals.toList with + | [ newGoal ] => + -- Set the new goal + let goals ← getUnsolvedGoals + setGoals (newGoal.mvarId :: goals) + -- There should be exactly two fields + let fields := newGoal.fields + withMainContext do + k (fields.get! 0) (fields.get! 1) + | _ => + throwError "Unreachable" + else + throwError "Not a conjunction" + +-- Tactic to fully split a conjunction +partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (l : List Expr) (h : Expr) (k : List Expr → TacticM α) : TacticM α := do + try + let ids ← do + if keepCurrentName then do + let cur := (← h.fvarId!.getDecl).userName + let nid ← mkFreshAnonPropUserName + pure (some (cur, nid)) + else + pure none + splitConjTac h ids (λ h1 h2 => + splitFullConjTacAux keepCurrentName l h1 (λ l1 => + splitFullConjTacAux keepCurrentName l1 h2 (λ l2 => + k l2))) + catch _ => + k (h :: l) + +-- Tactic to fully split a conjunction +-- `keepCurrentName`: if `true`, then the first conjunct has the name of the original assumption +def splitFullConjTac [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (h : Expr) (k : List Expr → TacticM α) : TacticM α := do + splitFullConjTacAux keepCurrentName [] h (λ l => k l.reverse) + +syntax optAtArgs := ("at" ident)? +def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := do + withMainContext do + let args := (args.raw.getArgs.get! 0).getArgs + if args.size > 0 then do + let n := (args.get! 1).getId + let decl ← Lean.Meta.getLocalDeclFromUserName n + let fvar := mkFVar decl.fvarId + pure (some fvar) + else + pure none + +elab "split_conj" args:optAtArgs : tactic => do + withMainContext do + match ← elabOptAtArgs args with + | some fvar => do + trace[Utils] "split at {fvar}" + splitConjTac fvar none (fun _ _ => pure ()) + | none => do + trace[Utils] "split goal" + splitConjTarget + +elab "split_conjs" args:optAtArgs : tactic => do + withMainContext do + match ← elabOptAtArgs args with + | some fvar => + trace[Utils] "split at {fvar}" + splitFullConjTac false fvar (fun _ => pure ()) + | none => + trace[Utils] "split goal" + repeatTac splitConjTarget + +elab "split_existsl" " at " n:ident : tactic => do + withMainContext do + let decl ← Lean.Meta.getLocalDeclFromUserName n.getId + let fvar := mkFVar decl.fvarId + splitAllExistsTac fvar [] (fun _ _ => pure ()) + +example (h : a ∧ b) : a := by + split_existsl at h + split_conj at h + assumption + +example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by + split_existsl at h + rename_i x y z + exists x + y + z + +/- Call the simp tactic. + The initialization of the context is adapted from Tactic.elabSimpArgs. + Something very annoying is that there is no function which allows to + initialize a simp context without doing an elaboration - as a consequence + we write our own here. -/ +def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) + (loc : Tactic.Location) : + Tactic.TacticM Unit := do + -- Initialize with the builtin simp theorems + let simpThms ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) + -- Add the equational theorem for the declarations to unfold + let simpThms ← + declsToUnfold.foldlM (fun thms decl => thms.addDeclToUnfold decl) simpThms + -- Add the hypotheses and the rewriting theorems + let simpThms ← + hypsToUse.foldlM (fun thms fvarId => + -- post: TODO: don't know what that is + -- inv: invert the equality + thms.add (.fvar fvarId) #[] (mkFVar fvarId) (post := false) (inv := false) + -- thms.eraseCore (.fvar fvar) + ) simpThms + -- Add the rewriting theorems to use + let simpThms ← + thms.foldlM (fun thms thmName => do + let info ← getConstInfo thmName + if (← isProp info.type) then + -- post: TODO: don't know what that is + -- inv: invert the equality + thms.addConst thmName (post := false) (inv := false) + else + throwError "Not a proposition: {thmName}" + ) simpThms + let congrTheorems ← getSimpCongrTheorems + let ctx : Simp.Context := { simpTheorems := #[simpThms], congrTheorems } + -- Apply the simplifier + let _ ← Tactic.simpLocation ctx (discharge? := .none) loc + +end Utils |