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 -- Attempt to apply a tactic def tryTac (tac : TacticM Unit) : TacticM Unit := do let _ ← tryTactic tac -- 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