diff --git a/REPL/ExtractData.lean b/REPL/ExtractData.lean new file mode 100644 index 00000000..9d1c729a --- /dev/null +++ b/REPL/ExtractData.lean @@ -0,0 +1,477 @@ +import Lean +import Lake + + +open Lean Elab System + +set_option maxHeartbeats 2000000 -- 10x the default maxHeartbeats. + + +instance : ToJson Substring where + toJson s := toJson s.toString + +instance : ToJson String.Pos where + toJson n := toJson n.1 + +deriving instance ToJson for SourceInfo +deriving instance ToJson for Syntax.Preresolved +deriving instance ToJson for Syntax +deriving instance ToJson for Position + + +-- namespace LeanDojo + + +/-- +The trace of a tactic. +-/ +structure TacticTrace where + stateBefore: String + stateAfter: String + pos: String.Pos -- Start position of the tactic. + endPos: String.Pos -- End position of the tactic. +deriving ToJson + +-- 定义配置结构 +structure ExtractionConfig where + extractTactics : Bool + extractPremises : Bool + +/-- +The trace of a premise. +-/ +structure PremiseTrace where + fullName: String -- Fully-qualified name of the premise. + defPos: Option Position -- Where the premise is defined. + defEndPos: Option Position + modName: String -- In which module the premise is defined. + defPath: String -- The path of the file where the premise is defined. + pos: Option Position -- Where the premise is used. + endPos: Option Position +deriving ToJson + + +/-- +The trace of a Lean file. +-/ +structure Trace where + commandASTs : Array Syntax -- The ASTs of the commands in the file. + tactics: Array TacticTrace -- All tactics in the file. + premises: Array PremiseTrace -- All premises in the file. +deriving ToJson + + +abbrev TraceM := StateT Trace MetaM + + +namespace Pp + + +private def addLine (s : String) : String := + if s.isEmpty then s else s ++ "\n" + + +-- Similar to `Meta.ppGoal` but uses String instead of Format to make sure local declarations are separated by "\n". +private def ppGoal (mvarId : MVarId) : MetaM String := do + match (← getMCtx).findDecl? mvarId with + | none => return "unknown goal" + | some mvarDecl => + let indent := 2 + let lctx := mvarDecl.lctx + let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } + Meta.withLCtx lctx mvarDecl.localInstances do + -- The followint two `let rec`s are being used to control the generated code size. + -- Then should be remove after we rewrite the compiler in Lean + let rec pushPending (ids : List Name) (type? : Option Expr) (s : String) : MetaM String := do + if ids.isEmpty then + return s + else + let s := addLine s + match type? with + | none => return s + | some type => + let typeFmt ← Meta.ppExpr type + return (s ++ (Format.joinSep ids.reverse (format " ") ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group).pretty + let rec ppVars (varNames : List Name) (prevType? : Option Expr) (s : String) (localDecl : LocalDecl) : MetaM (List Name × Option Expr × String) := do + match localDecl with + | .cdecl _ _ varName type _ _ => + let varName := varName.simpMacroScopes + let type ← instantiateMVars type + if prevType? == none || prevType? == some type then + return (varName :: varNames, some type, s) + else do + let s ← pushPending varNames prevType? s + return ([varName], some type, s) + | .ldecl _ _ varName type val _ _ => do + let varName := varName.simpMacroScopes + let s ← pushPending varNames prevType? s + let s := addLine s + let type ← instantiateMVars type + let typeFmt ← Meta.ppExpr type + let mut fmtElem := format varName ++ " : " ++ typeFmt + let val ← instantiateMVars val + let valFmt ← Meta.ppExpr val + fmtElem := fmtElem ++ " :=" ++ Format.nest indent (Format.line ++ valFmt) + let s := s ++ fmtElem.group.pretty + return ([], none, s) + let (varNames, type?, s) ← lctx.foldlM (init := ([], none, "")) fun (varNames, prevType?, s) (localDecl : LocalDecl) => + if localDecl.isAuxDecl || localDecl.isImplementationDetail then + -- Ignore auxiliary declarations and implementation details. + return (varNames, prevType?, s) + else + ppVars varNames prevType? s localDecl + let s ← pushPending varNames type? s + let goalTypeFmt ← Meta.ppExpr (← instantiateMVars mvarDecl.type) + let goalFmt := Meta.getGoalPrefix mvarDecl ++ Format.nest indent goalTypeFmt + let s := s ++ "\n" ++ goalFmt.pretty + match mvarDecl.userName with + | Name.anonymous => return s + | name => return "case " ++ name.eraseMacroScopes.toString ++ "\n" ++ s + + +def ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO String := + if goals.isEmpty then + return "no goals" + else + let fmt := ctx.runMetaM {} (return Std.Format.prefixJoin "\n\n" (← goals.mapM (ppGoal ·))) + return (← fmt).pretty.trim + + +end Pp + + +namespace Path + +/-- +Return the path of `path` relative to `parent`. +-/ +def relativeTo (path parent : FilePath) : Option FilePath := + let rec componentsRelativeTo (pathComps parentComps : List String) : Option FilePath := + match pathComps, parentComps with + | _, [] => mkFilePath pathComps + | [], _ => none + | (h₁ :: t₁), (h₂ :: t₂) => + if h₁ == h₂ then + componentsRelativeTo t₁ t₂ + else + none + + componentsRelativeTo path.components parent.components + + +/-- +Return if the path `path` is relative to `parent`. +-/ +def isRelativeTo (path parent : FilePath) : Bool := + match relativeTo path parent with + | some _ => true + | none => false + + +/-- +Convert the path `path` to an absolute path. +-/ +def toAbsolute (path : FilePath) : IO FilePath := do + if path.isAbsolute then + pure path + else + let cwd ← IO.currentDir + pure $ cwd / path + + +private def trim (path : FilePath) : FilePath := + assert! path.isRelative + mkFilePath $ path.components.filter (· != ".") + + +def packagesDir : FilePath := + if Lake.defaultPackagesDir == "packages" then + ".lake" / Lake.defaultPackagesDir + else + Lake.defaultPackagesDir + + +def buildDir : FilePath := + if Lake.defaultPackagesDir.fileName == "packages" then -- Lean >= v4.3.0-rc2 + ".lake/build" + else -- Lean < v4.3.0-rc2 + "build" + + +def libDir : FilePath := buildDir / "lib" + + +/-- +Convert the path of a *.lean file to its corresponding file (e.g., *.olean) in the "build" directory. +-/ +def toBuildDir (subDir : FilePath) (path : FilePath) (ext : String) : Option FilePath := + let path' := (trim path).withExtension ext + match relativeTo path' $ packagesDir / "lean4/src" with + | some p => + match relativeTo p "lean/lake" with + | some p' => packagesDir / "lean4/lib/lean" / p' + | none => packagesDir / "lean4/lib" / p + | none => match relativeTo path' packagesDir with + | some p => + match p.components with + | [] => none + | hd :: tl => packagesDir / hd / buildDir / subDir / (mkFilePath tl) + | none => buildDir / subDir / path' + + +/-- +The reverse of `toBuildDir`. +-/ +-- proofwidgets/build/lib/ProofWidgets/Compat.lean +-- proofwidgets/.lake/build/lib +def toSrcDir! (path : FilePath) (ext : String) : FilePath := + let path' := (trim path).withExtension ext + match relativeTo path' $ packagesDir / "lean4/lib" with + | some p => -- E.g., `.lake/packages/lean4/lib/lean/Init/Prelude.olean` -> `.lake/packages/lean4/src/lean/Init/Prelude.lean` + packagesDir / "lean4/src" / p + | none => + match relativeTo path' packagesDir with + | some p => -- E.g., `.lake/packages/aesop/.lake/build/lib/Aesop.olean`-> `.lake/packages/aesop/Aesop.lean` + let pkgName := p.components.head! + let sep := "build/lib/" + packagesDir / pkgName / (p.toString.splitOn sep |>.tail!.head!) + | none => + -- E.g., `.lake/build/lib/Mathlib/LinearAlgebra/Basic.olean` -> `Mathlib/LinearAlgebra/Basic.lean` + relativeTo path' libDir |>.get! + + +/-- +Create all parent directories of `p` if they don't exist. +-/ +def makeParentDirs (p : FilePath) : IO Unit := do + let some parent := p.parent | throw $ IO.userError s!"Unable to get the parent of {p}" + IO.FS.createDirAll parent + + +/-- +Return the *.lean file corresponding to a module name. +-/ +def findLean (mod : Name) : IO FilePath := do + let modStr := mod.toString + if modStr.startsWith "«lake-packages»." then + return FilePath.mk (modStr.replace "«lake-packages»" "lake-packages" |>.replace "." "/") |>.withExtension "lean" + if modStr.startsWith "«.lake»." then + return FilePath.mk (modStr.replace "«.lake»" ".lake" |>.replace "." "/") |>.withExtension "lean" + let olean ← findOLean mod + -- Remove a "build/lib/" substring from the path. + let lean := olean.toString.replace ".lake/build/lib/" "" + |>.replace "build/lib/" "" |>.replace "lib/lean/Lake/" "lib/lean/lake/Lake/" |>.replace "lib/lean/Init" "src/lean/Init" + let mut path := FilePath.mk lean |>.withExtension "lean" + let leanLib ← getLibDir (← getBuildDir) + -- let projectRoot := (leanLib.parent >>= (·.parent) >>= (·.parent) >>= (·.parent) >>= (·.parent) >>= (·.parent) >>= (·.parent)).get! + if let some p := relativeTo path leanLib then + path := packagesDir / "lean4/src/lean" / p + if !(← path.pathExists) then + -- IO.println s!"WARNING: Path does not exist: {path}" + -- IO.println s!"OLean file: {olean.toString}" + -- IO.println s!"path: {path}" + -- Instead of using assert!, return an error or handle it appropriately + throw <| IO.userError s!"Path does not exist: {path}" + return path + +end Path + + +namespace Traversal + + +/-- +Extract tactic information from `TacticInfo` in `InfoTree`. +-/ +private def visitTacticInfo (ctx : ContextInfo) (ti : TacticInfo) (parent : InfoTree) (config : ExtractionConfig) : TraceM Unit := do + if not config.extractTactics then + return () + match ti.stx.getKind with + | ``Lean.Parser.Term.byTactic => + match ti.stx with + | .node _ _ #[.atom _ "by", .node _ ``Lean.Parser.Tactic.tacticSeq _] => pure () + | _ => assert! false + + | ``Lean.Parser.Tactic.tacticSeq => + match ti.stx with + | .node _ _ #[.node _ ``Lean.Parser.Tactic.tacticSeq1Indented _] => pure () + | .node _ _ #[.node _ ``Lean.Parser.Tactic.tacticSeqBracketed _] => pure () + | _ => assert! false + + | _ => pure () + + match parent with + | .node (Info.ofTacticInfo i) _ => + match i.stx.getKind with + | ``Lean.Parser.Tactic.tacticSeq1Indented | ``Lean.Parser.Tactic.tacticSeqBracketed | ``Lean.Parser.Tactic.rewriteSeq => + let ctxBefore := { ctx with mctx := ti.mctxBefore } + let ctxAfter := { ctx with mctx := ti.mctxAfter } + let stateBefore ← Pp.ppGoals ctxBefore ti.goalsBefore + let stateAfter ← Pp.ppGoals ctxAfter ti.goalsAfter + if stateBefore == "no goals" || stateBefore == stateAfter then + pure () + else + let some posBefore := ti.stx.getPos? true | pure () + let some posAfter := ti.stx.getTailPos? true | pure () + match ti.stx with + | .node _ _ _ => + modify fun trace => { + trace with tactics := trace.tactics.push { + stateBefore := stateBefore, + stateAfter := stateAfter, + pos := posBefore, + endPos := posAfter, + } + } + | _ => pure () + | _ => pure () + | _ => pure () + + +/-- +Extract premise information from `TermInfo` in `InfoTree`. +-/ +private def visitTermInfo (ti : TermInfo) (env : Environment) (config : ExtractionConfig) : TraceM Unit := do + if not config.extractPremises then + return () + let some fullName := ti.expr.constName? | return () + let fileMap ← getFileMap + + let posBefore := match ti.toElabInfo.stx.getPos? with + | some posInfo => fileMap.toPosition posInfo + | none => none + + let posAfter := match ti.toElabInfo.stx.getTailPos? with + | some posInfo => fileMap.toPosition posInfo + | none => none + + let decRanges ← withEnv env $ findDeclarationRanges? fullName + let defPos := decRanges >>= fun (decR : DeclarationRanges) => decR.selectionRange.pos + let defEndPos := decRanges >>= fun (decR : DeclarationRanges) => decR.selectionRange.endPos + + let modName := + if let some modIdx := env.const2ModIdx.find? fullName then + env.header.moduleNames[modIdx.toNat]! + else + env.header.mainModule + + -- -- 添加调试输出 + -- IO.println s!"modName: {modName}" + + let mut defPath := "" + try + defPath := toString $ ← Path.findLean modName + if defPath.startsWith "./" then + defPath := defPath.drop 2 + if defPath.startsWith "/lake/" then + defPath := ".lake/" ++ (defPath.drop 6) + catch _ => + defPath := toString modName + + if defPos != posBefore ∧ defEndPos != posAfter then -- Don't include defintions as premises. + modify fun trace => { + trace with premises := trace.premises.push { + fullName := toString fullName, + defPos := defPos, + defEndPos := defEndPos, + defPath := defPath, + modName := toString modName, + pos := posBefore, + endPos := posAfter, + } + } + +-- 修改 visitInfo 函数 +private def visitInfo (ctx : ContextInfo) (i : Info) (parent : InfoTree) (env : Environment) (config : ExtractionConfig) : TraceM Unit := do + match i with + | .ofTacticInfo ti => visitTacticInfo ctx ti parent config + | .ofTermInfo ti => visitTermInfo ti env config + | _ => pure () + +-- 假设 ContextInfo 是一个记录类型，我们需要为其实现 ToString 实例 +-- instance : ToString ContextInfo where +-- toString ctx := s!"ContextInfo(mctx: {ctx.mctx}, lctx: {ctx.lctx}, declName: {ctx.declName})" + +-- 修改 traverseTree 函数 +private partial def traverseTree (ctx: ContextInfo) (tree : InfoTree) +(parent : InfoTree) (env : Environment) (config : ExtractionConfig) : TraceM Unit := do + match tree with + | .context ctx' t => + match ctx'.mergeIntoOuter? ctx with + | some ctx' => + traverseTree ctx' t tree env config + | none => panic! "fail to synthesis contextInfo when traversing infoTree" + | .node i children => + visitInfo ctx i parent env config + for x in children do + traverseTree ctx x tree env config + | _ => pure () + + +-- 修改 traverseTopLevelTree 函数 +private def traverseTopLevelTree (tree : InfoTree) (env : Environment) (config : ExtractionConfig) : TraceM Unit := do + match tree with + | .context ctx t => + match ctx.mergeIntoOuter? none with + | some ctx => traverseTree ctx t tree env config + | none => panic! "fail to synthesis contextInfo for top-level infoTree" + | _ => pure () + + +-- 修改 traverseForest 函数 +def traverseForest (trees : Array InfoTree) (env : Environment) (config : ExtractionConfig) : TraceM Trace := do + for t in trees do + traverseTopLevelTree t env config + get + + +end Traversal + + +open Traversal + + +def getImports (header: Syntax) : IO String := do + -- Similar to `lean --deps` in Lean 3. + let mut s := "" + + for dep in headerToImports header do + let oleanPath ← findOLean dep.module + if oleanPath.isRelative then + let leanPath := Path.toSrcDir! oleanPath "lean" + assert! ← leanPath.pathExists + s := s ++ "\n" ++ leanPath.toString + else if ¬(oleanPath.toString.endsWith "/lib/lean/Init.olean") then + let mut p := (Path.packagesDir / "lean4").toString ++ FilePath.pathSeparator.toString + let mut found := false + for c in (oleanPath.withExtension "lean").components do + if c == "lib" then + found := true + p := p ++ "src" + continue + if found then + p := p ++ FilePath.pathSeparator.toString ++ c + p := p.replace "/lean4/src/lean/Lake" "/lean4/src/lean/lake/Lake" + assert! ← FilePath.mk p |>.pathExists + s := s ++ "\n" ++ p + + return s.trim + +-- 修改 extractAST 函数 +def extractAST (code : String) (config : ExtractionConfig) : IO Json := do + let inputCtx := Parser.mkInputContext code "" + let (header, parserState, messages) ← Parser.parseHeader inputCtx + let (env, messages) ← processHeader header {} messages inputCtx + if messages.hasErrors then + for msg in messages.toList do + if msg.severity == .error then + println! "ERROR: {← msg.toString}" + throw $ IO.userError "Errors during import; aborting" + let commandState := { Command.mkState env messages {} with infoState.enabled := true } + let s ← IO.processCommands inputCtx parserState commandState + let env' := s.commandState.env + let commands := s.commands.pop -- Remove EOI command. + let trees := s.commandState.infoState.trees.toArray + let traceM := (traverseForest trees env' config).run' ⟨#[header] ++ commands, #[], #[]⟩ + let (trace, _) ← traceM.run'.toIO {fileName := "", fileMap := FileMap.ofString code} {env := env} + return toJson trace -- 返回AST的JSON表示 diff --git a/REPL/Main.lean b/REPL/Main.lean index b00b6833..95b12833 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -11,6 +11,7 @@ import REPL.Lean.Environment import REPL.Lean.InfoTree import REPL.Lean.InfoTree.ToJson import REPL.Snapshots +import REPL.ExtractData /-! # A REPL for Lean. @@ -249,9 +250,10 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap return { proofState := id goals := (← proofState.ppGoals).map fun s => s!"{s}" - messages - sorries - traces + messages := messages + sorries := sorries + traces := traces + ast := none proofStatus := (← getProofStatus proofState) } /-- Pickle a `CommandSnapshot`, generating a JSON response. -/ @@ -260,13 +262,27 @@ def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Err | none => return .inr ⟨"Unknown environment."⟩ | some env => discard <| env.pickle n.pickleTo - return .inl { env := n.env } + return .inl { + env := n.env + messages := [] + sorries := [] + tactics := [] + infotree := none + ast := none -- Set to none, since the pickle operation does not involve AST extraction + } /-- Unpickle a `CommandSnapshot`, generating a JSON response. -/ def unpickleCommandSnapshot (n : UnpickleEnvironment) : M IO CommandResponse := do let (env, _) ← CommandSnapshot.unpickle n.unpickleEnvFrom let env ← recordCommandSnapshot env - return { env } + return { + env := env + messages := [] + sorries := [] + tactics := [] + infotree := none + ast := none -- Set to none, since the pickle operation does not involve AST extraction + } /-- Pickle a `ProofSnapshot`, generating a JSON response. -/ -- This generates a new identifier, which perhaps is not what we want? @@ -333,17 +349,26 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do pure none else pure <| some <| Json.arr (← jsonTrees.toArray.mapM fun t => t.toJson none) + let opts : ExtractionConfig := { + extractTactics := s.tactics.getD true, + extractPremises := s.premises.getD true, + -- extractCommandASTs := s.commandAST.getD false + } + let ast ← match s.ast with + | some true => extractAST s.cmd opts + | _ => pure (toJson ([] : List Json)) return .inl { env, messages, sorries, tactics - infotree } + infotree, + ast } -- Return AST information def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do try let cmd ← IO.FS.readFile s.path - runCommand { s with env := none, cmd } + runCommand { s with env := none, cmd, tactics := true, premises := true, commandAST := true, infotree := none } catch e => pure <| .inr ⟨e.toString⟩ diff --git a/test/aime_1983_p9.code.in b/test/aime_1983_p9.code.in new file mode 100644 index 00000000..a17ef59a --- /dev/null +++ b/test/aime_1983_p9.code.in @@ -0,0 +1,34 @@ +import Mathlib +import Aesop + +set_option maxHeartbeats 0 + +open BigOperators Real Nat Topology Rat + + +/-- Show that $ + rac{9x^2\sin^2 x + 4}{x\sin x} \geq 12$ for $0 < x < \pi$.-/ +theorem aime_1983_p9 (x : ℝ) (h₀ : 0 < x ∧ x < Real.pi) : + 12 ≤ (9 * (x ^ 2 * Real.sin x ^ 2) + 4) / (x * Real.sin x) := by + /- + To find the minimum value of $ + rac{9x^2\sin^2 x + 4}{x\sin x}$ for $0 < x < \pi$, we need to show that it is at least 12. We start by noting that the expression can be rewritten using the division property of inequalities. We then use the fact that \$sin x$ and $x$ are positive in the given range to establish the necessary inequalities. Finally, we apply these results to conclude that the minimum value is indeed 12. + -/ + -- We start by ensuring that the product x * sin x is positive in the given range. + have h₁ : 0 < x * Real.sin x := by + apply mul_pos + -- x is positive in the range (0, π). + exact h₀.1 + -- sin x is positive in the range (0, π). + exact Real.sin_pos_of_pos_of_lt_pi h₀.1 h₀.2 + -- Using the division property of inequalities, we rewrite the expression. + rw [le_div_iff h₁] + /- tactic state: + x : ℝ + h₀ : 0 < x ∧ x < π + h₁ : 0 < x * x.sin + ⊢ 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4 + -/ + -- This is equivalent to showing that 9x^2 sin^2 x - 12x sin x + 4 ≥ 0, and the left hand side can be rewritten as a perfect square (3x sin x - 2)^2. + -- We use the fact that (3x sin x - 2)^2 is non-negative to establish this. + nlinarith [sq_nonneg (3 * x * Real.sin x - 2)] diff --git a/test/aime_1983_p9.expected.out b/test/aime_1983_p9.expected.out new file mode 100644 index 00000000..848f590b --- /dev/null +++ b/test/aime_1983_p9.expected.out @@ -0,0 +1,1504 @@ +{"env": 0, + "ast": + {"tactics": + [{"stateBefore": + "x : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 12 ≤ (9 * (x ^ 2 * x.sin ^ 2) + 4) / (x * x.sin)", + "stateAfter": + "x : ℝ\nh₀ : 0 < x ∧ x < π\nh₁ : 0 < x * x.sin\n⊢ 12 ≤ (9 * (x ^ 2 * x.sin ^ 2) + 4) / (x * x.sin)", + "pos": 829, + "endPos": 1043}, + {"stateBefore": "x : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 0 < x * x.sin", + "stateAfter": + "case ha\nx : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 0 < x\n\ncase hb\nx : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 0 < x.sin", + "pos": 870, + "endPos": 883}, + {"stateBefore": + "case ha\nx : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 0 < x\n\ncase hb\nx : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 0 < x.sin", + "stateAfter": "case hb\nx : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 0 < x.sin", + "pos": 931, + "endPos": 943}, + {"stateBefore": "case hb\nx : ℝ\nh₀ : 0 < x ∧ x < π\n⊢ 0 < x.sin", + "stateAfter": "no goals", + "pos": 995, + "endPos": 1043}, + {"stateBefore": + "x : ℝ\nh₀ : 0 < x ∧ x < π\nh₁ : 0 < x * x.sin\n⊢ 12 ≤ (9 * (x ^ 2 * x.sin ^ 2) + 4) / (x * x.sin)", + "stateAfter": + "x : ℝ\nh₀ : 0 < x ∧ x < π\nh₁ : 0 < x * x.sin\n⊢ 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4", + "pos": 1123, + "endPos": 1143}, + {"stateBefore": + "x : ℝ\nh₀ : 0 < x ∧ x < π\nh₁ : 0 < x * x.sin\n⊢ 12 ≤ (9 * (x ^ 2 * x.sin ^ 2) + 4) / (x * x.sin)", + "stateAfter": + "x : ℝ\nh₀ : 0 < x ∧ x < π\nh₁ : 0 < x * x.sin\n⊢ 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4", + "pos": 1127, + "endPos": 1142}, + {"stateBefore": + "x : ℝ\nh₀ : 0 < x ∧ x < π\nh₁ : 0 < x * x.sin\n⊢ 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4", + "stateAfter": "no goals", + "pos": 1524, + "endPos": 1570}], + "premises": + [{"pos": {"line": 11, "column": 26}, + "modName": "Mathlib.Data.Real.Basic", + "fullName": "Real", + "endPos": {"line": 11, "column": 27}, + "defPos": {"line": 32, "column": 10}, + "defPath": "./Mathlib/Data/Real/Basic.lean", + "defEndPos": {"line": 32, "column": 14}}, + {"pos": {"line": 11, "column": 26}, + "modName": "Mathlib.Data.Real.Basic", + "fullName": "Real", + "endPos": {"line": 11, "column": 27}, + "defPos": {"line": 32, "column": 10}, + "defPath": "./Mathlib/Data/Real/Basic.lean", + "defEndPos": {"line": 32, "column": 14}}, + {"pos": {"line": 11, "column": 26}, + "modName": "Mathlib.Data.Real.Basic", + "fullName": "Real", + "endPos": {"line": 11, "column": 27}, + "defPos": {"line": 32, "column": 10}, + "defPath": "./Mathlib/Data/Real/Basic.lean", + "defEndPos": {"line": 32, "column": 14}}, + {"pos": {"line": 11, "column": 35}, + "modName": "Init.Prelude", + "fullName": "And", + "endPos": {"line": 11, "column": 54}, + "defPos": {"line": 516, "column": 10}, + "defPath": + "/cis_prover/elan/toolchains/leanprover--lean4---v4.9.0-rc1/src/lean/Init/Prelude.lean", + "defEndPos": {"line": 516, "column": 13}}, + {"pos": {"line": 11, "column": 47}, + "modName": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", + "fullName": "Real.pi", + "endPos": {"line": 11, "column": 54}, + "defPos": {"line": 134, "column": 28}, + "defPath": "./Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean", + "defEndPos": {"line": 134, "column": 30}}, + {"pos": {"line": 11, "column": 47}, + "modName": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", + "fullName": "Real.pi", + "endPos": {"line": 11, "column": 54}, + "defPos": {"line": 134, "column": 28}, + "defPath": "./Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean", + "defEndPos": {"line": 134, "column": 30}}, + {"pos": {"line": 12, "column": 21}, + "modName": "Mathlib.Data.Complex.Exponential", + "fullName": "Real.sin", + "endPos": {"line": 12, "column": 29}, + "defPos": {"line": 119, "column": 11}, + "defPath": "./Mathlib/Data/Complex/Exponential.lean", + "defEndPos": {"line": 119, "column": 14}}, + {"pos": {"line": 12, "column": 49}, + "modName": "Mathlib.Data.Complex.Exponential", + "fullName": "Real.sin", + "endPos": {"line": 12, "column": 57}, + "defPos": {"line": 119, "column": 11}, + "defPath": "./Mathlib/Data/Complex/Exponential.lean", + "defEndPos": {"line": 119, "column": 14}}, + {"pos": {"line": 17, "column": 20}, + "modName": "Mathlib.Data.Complex.Exponential", + "fullName": "Real.sin", + "endPos": {"line": 17, "column": 28}, + "defPos": {"line": 119, "column": 11}, + "defPath": "./Mathlib/Data/Complex/Exponential.lean", + "defEndPos": {"line": 119, "column": 14}}, + {"pos": {"line": 18, "column": 10}, + "modName": "Mathlib.Algebra.Order.GroupWithZero.Unbundled", + "fullName": "mul_pos", + "endPos": {"line": 18, "column": 17}, + "defPos": {"line": 406, "column": 6}, + "defPath": "./Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean", + "defEndPos": {"line": 406, "column": 13}}, + {"pos": {"line": 20, "column": 13}, + "modName": "Init.Prelude", + "fullName": "And.left", + "endPos": {"line": 20, "column": 14}, + "defPos": {"line": 521, "column": 2}, + "defPath": + "/cis_prover/elan/toolchains/leanprover--lean4---v4.9.0-rc1/src/lean/Init/Prelude.lean", + "defEndPos": {"line": 521, "column": 6}}, + {"pos": {"line": 22, "column": 10}, + "modName": "Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic", + "fullName": "Real.sin_pos_of_pos_of_lt_pi", + "endPos": {"line": 22, "column": 38}, + "defPos": {"line": 461, "column": 8}, + "defPath": "./Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean", + "defEndPos": {"line": 461, "column": 31}}, + {"pos": {"line": 22, "column": 42}, + "modName": "Init.Prelude", + "fullName": "And.left", + "endPos": {"line": 22, "column": 43}, + "defPos": {"line": 521, "column": 2}, + "defPath": + "/cis_prover/elan/toolchains/leanprover--lean4---v4.9.0-rc1/src/lean/Init/Prelude.lean", + "defEndPos": {"line": 521, "column": 6}}, + {"pos": {"line": 22, "column": 47}, + "modName": "Init.Prelude", + "fullName": "And.right", + "endPos": {"line": 22, "column": 48}, + "defPos": {"line": 524, "column": 2}, + "defPath": + "/cis_prover/elan/toolchains/leanprover--lean4---v4.9.0-rc1/src/lean/Init/Prelude.lean", + "defEndPos": {"line": 524, "column": 7}}, + {"pos": {"line": 24, "column": 6}, + "modName": "Mathlib.Algebra.Order.Field.Basic", + "fullName": "le_div_iff", + "endPos": {"line": 24, "column": 16}, + "defPos": {"line": 49, "column": 8}, + "defPath": "./Mathlib/Algebra/Order/Field/Basic.lean", + "defEndPos": {"line": 49, "column": 18}}, + {"pos": {"line": 33, "column": 13}, + "modName": "Mathlib.Algebra.Order.Ring.Defs", + "fullName": "sq_nonneg", + "endPos": {"line": 33, "column": 22}, + "defPos": {"line": 1209, "column": 6}, + "defPath": "./Mathlib/Algebra/Order/Ring/Defs.lean", + "defEndPos": {"line": 1209, "column": 15}}, + {"pos": {"line": 33, "column": 32}, + "modName": "Mathlib.Data.Complex.Exponential", + "fullName": "Real.sin", + "endPos": {"line": 33, "column": 40}, + "defPos": {"line": 119, "column": 11}, + "defPath": "./Mathlib/Data/Complex/Exponential.lean", + "defEndPos": {"line": 119, "column": 14}}], + "commandASTs": + [{"node": + {"kind": "Lean.Parser.Module.header", + "info": "none", + "args": + [{"node": {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Module.import", + "info": "none", + "args": + [{"atom": + {"val": "import", + "info": + {"original": + {"trailing": " ", "pos": 1, "leading": "", "endPos": 7}}}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"ident": + {"val": "Mathlib", + "rawVal": "Mathlib", + "preresolved": [], + "info": + {"original": + {"trailing": "\n", "pos": 8, "leading": "", "endPos": 15}}}}, + {"node": {"kind": "null", "info": "none", "args": []}}]}}, + {"node": + {"kind": "Lean.Parser.Module.import", + "info": "none", + "args": + [{"atom": + {"val": "import", + "info": + {"original": + {"trailing": " ", "pos": 16, "leading": "", "endPos": 22}}}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"ident": + {"val": "Aesop", + "rawVal": "Aesop", + "preresolved": [], + "info": + {"original": + {"trailing": "\n\n", "pos": 23, "leading": "", "endPos": 28}}}}, + {"node": {"kind": "null", "info": "none", "args": []}}]}}]}}]}}, + {"node": + {"kind": "Lean.Parser.Command.set_option", + "info": "none", + "args": + [{"atom": + {"val": "set_option", + "info": + {"original": + {"trailing": " ", "pos": 30, "leading": "", "endPos": 40}}}}, + {"ident": + {"val": "maxHeartbeats", + "rawVal": "maxHeartbeats", + "preresolved": [], + "info": + {"original": + {"trailing": " ", "pos": 41, "leading": "", "endPos": 54}}}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "0", + "info": + {"original": + {"trailing": "\n\n", + "pos": 55, + "leading": "", + "endPos": 56}}}}]}}]}}, + {"node": + {"kind": "Lean.Parser.Command.open", + "info": "none", + "args": + [{"atom": + {"val": "open", + "info": + {"original": + {"trailing": " ", "pos": 58, "leading": "", "endPos": 62}}}}, + {"node": + {"kind": "Lean.Parser.Command.openSimple", + "info": "none", + "args": + [{"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "BigOperators", + "rawVal": "BigOperators", + "preresolved": [], + "info": + {"original": + {"trailing": " ", "pos": 63, "leading": "", "endPos": 75}}}}, + {"ident": + {"val": "Real", + "rawVal": "Real", + "preresolved": [], + "info": + {"original": + {"trailing": " ", "pos": 76, "leading": "", "endPos": 80}}}}, + {"ident": + {"val": "Nat", + "rawVal": "Nat", + "preresolved": [], + "info": + {"original": + {"trailing": " ", "pos": 81, "leading": "", "endPos": 84}}}}, + {"ident": + {"val": "Topology", + "rawVal": "Topology", + "preresolved": [], + "info": + {"original": + {"trailing": " ", "pos": 85, "leading": "", "endPos": 93}}}}, + {"ident": + {"val": "Rat", + "rawVal": "Rat", + "preresolved": [], + "info": + {"original": + {"trailing": "\n\n\n", + "pos": 94, + "leading": "", + "endPos": 97}}}}]}}]}}]}}, + {"node": + {"kind": "Lean.Parser.Command.declaration", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Command.declModifiers", + "info": "none", + "args": + [{"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Command.docComment", + "info": "none", + "args": + [{"atom": + {"val": "/--", + "info": + {"original": + {"trailing": " ", + "pos": 100, + "leading": "", + "endPos": 103}}}}, + {"atom": + {"val": + "Show that $\u000crac{9x^2\\sin^2 x + 4}{x\\sin x} \\geq 12$ for $0 < x < \\pi$.-/", + "info": + {"original": + {"trailing": "\n", + "pos": 104, + "leading": "", + "endPos": 176}}}}]}}]}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"node": {"kind": "null", "info": "none", "args": []}}]}}, + {"node": + {"kind": "Lean.Parser.Command.theorem", + "info": "none", + "args": + [{"atom": + {"val": "theorem", + "info": + {"original": + {"trailing": " ", "pos": 177, "leading": "", "endPos": 184}}}}, + {"node": + {"kind": "Lean.Parser.Command.declId", + "info": "none", + "args": + [{"ident": + {"val": "aime_1983_p9", + "rawVal": "aime_1983_p9", + "preresolved": [], + "info": + {"original": + {"trailing": " ", "pos": 185, "leading": "", "endPos": 197}}}}, + {"node": {"kind": "null", "info": "none", "args": []}}]}}, + {"node": + {"kind": "Lean.Parser.Command.declSig", + "info": "none", + "args": + [{"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.explicitBinder", + "info": "none", + "args": + [{"atom": + {"val": "(", + "info": + {"original": + {"trailing": "", + "pos": 198, + "leading": "", + "endPos": 199}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 199, + "leading": "", + "endPos": 200}}}}]}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"atom": + {"val": ":", + "info": + {"original": + {"trailing": " ", + "pos": 201, + "leading": "", + "endPos": 202}}}}, + {"node": + {"kind": "termℝ", + "info": "none", + "args": + [{"atom": + {"val": "ℝ", + "info": + {"original": + {"trailing": "", + "pos": 203, + "leading": "", + "endPos": 206}}}}]}}]}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"atom": + {"val": ")", + "info": + {"original": + {"trailing": " ", + "pos": 206, + "leading": "", + "endPos": 207}}}}]}}, + {"node": + {"kind": "Lean.Parser.Term.explicitBinder", + "info": "none", + "args": + [{"atom": + {"val": "(", + "info": + {"original": + {"trailing": "", + "pos": 208, + "leading": "", + "endPos": 209}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "h₀", + "rawVal": "h₀", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 209, + "leading": "", + "endPos": 213}}}}]}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"atom": + {"val": ":", + "info": + {"original": + {"trailing": " ", + "pos": 214, + "leading": "", + "endPos": 215}}}}, + {"node": + {"kind": "«term_∧_»", + "info": "none", + "args": + [{"node": + {"kind": "«term_<_»", + "info": "none", + "args": + [{"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "0", + "info": + {"original": + {"trailing": " ", + "pos": 216, + "leading": "", + "endPos": 217}}}}]}}, + {"atom": + {"val": "<", + "info": + {"original": + {"trailing": " ", + "pos": 218, + "leading": "", + "endPos": 219}}}}, + {"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 220, + "leading": "", + "endPos": 221}}}}]}}, + {"atom": + {"val": "∧", + "info": + {"original": + {"trailing": " ", + "pos": 222, + "leading": "", + "endPos": 225}}}}, + {"node": + {"kind": "«term_<_»", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 226, + "leading": "", + "endPos": 227}}}}, + {"atom": + {"val": "<", + "info": + {"original": + {"trailing": " ", + "pos": 228, + "leading": "", + "endPos": 229}}}}, + {"ident": + {"val": "Real.pi", + "rawVal": "Real.pi", + "preresolved": [], + "info": + {"original": + {"trailing": "", + "pos": 230, + "leading": "", + "endPos": 237}}}}]}}]}}]}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"atom": + {"val": ")", + "info": + {"original": + {"trailing": " ", + "pos": 237, + "leading": "", + "endPos": 238}}}}]}}]}}, + {"node": + {"kind": "Lean.Parser.Term.typeSpec", + "info": "none", + "args": + [{"atom": + {"val": ":", + "info": + {"original": + {"trailing": "\n ", + "pos": 239, + "leading": "", + "endPos": 240}}}}, + {"node": + {"kind": "«term_≤_»", + "info": "none", + "args": + [{"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "12", + "info": + {"original": + {"trailing": " ", + "pos": 243, + "leading": "", + "endPos": 245}}}}]}}, + {"atom": + {"val": "≤", + "info": + {"original": + {"trailing": " ", + "pos": 246, + "leading": "", + "endPos": 249}}}}, + {"node": + {"kind": "«term_/_»", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.paren", + "info": "none", + "args": + [{"atom": + {"val": "(", + "info": + {"original": + {"trailing": "", + "pos": 250, + "leading": "", + "endPos": 251}}}}, + {"node": + {"kind": "«term_+_»", + "info": "none", + "args": + [{"node": + {"kind": "«term_*_»", + "info": "none", + "args": + [{"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "9", + "info": + {"original": + {"trailing": " ", + "pos": 251, + "leading": "", + "endPos": 252}}}}]}}, + {"atom": + {"val": "*", + "info": + {"original": + {"trailing": " ", + "pos": 253, + "leading": "", + "endPos": 254}}}}, + {"node": + {"kind": "Lean.Parser.Term.paren", + "info": "none", + "args": + [{"atom": + {"val": "(", + "info": + {"original": + {"trailing": "", + "pos": 255, + "leading": "", + "endPos": 256}}}}, + {"node": + {"kind": "«term_*_»", + "info": "none", + "args": + [{"node": + {"kind": "«term_^_»", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 256, + "leading": "", + "endPos": 257}}}}, + {"atom": + {"val": "^", + "info": + {"original": + {"trailing": " ", + "pos": 258, + "leading": "", + "endPos": 259}}}}, + {"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "2", + "info": + {"original": + {"trailing": " ", + "pos": 260, + "leading": "", + "endPos": 261}}}}]}}]}}, + {"atom": + {"val": "*", + "info": + {"original": + {"trailing": " ", + "pos": 262, + "leading": "", + "endPos": 263}}}}, + {"node": + {"kind": "«term_^_»", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.app", + "info": "none", + "args": + [{"ident": + {"val": "Real.sin", + "rawVal": "Real.sin", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 264, + "leading": "", + "endPos": 272}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 273, + "leading": "", + "endPos": 274}}}}]}}]}}, + {"atom": + {"val": "^", + "info": + {"original": + {"trailing": " ", + "pos": 275, + "leading": "", + "endPos": 276}}}}, + {"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "2", + "info": + {"original": + {"trailing": "", + "pos": 277, + "leading": "", + "endPos": 278}}}}]}}]}}]}}, + {"atom": + {"val": ")", + "info": + {"original": + {"trailing": " ", + "pos": 278, + "leading": "", + "endPos": 279}}}}]}}]}}, + {"atom": + {"val": "+", + "info": + {"original": + {"trailing": " ", + "pos": 280, + "leading": "", + "endPos": 281}}}}, + {"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "4", + "info": + {"original": + {"trailing": "", + "pos": 282, + "leading": "", + "endPos": 283}}}}]}}]}}, + {"atom": + {"val": ")", + "info": + {"original": + {"trailing": " ", + "pos": 283, + "leading": "", + "endPos": 284}}}}]}}, + {"atom": + {"val": "/", + "info": + {"original": + {"trailing": " ", + "pos": 285, + "leading": "", + "endPos": 286}}}}, + {"node": + {"kind": "Lean.Parser.Term.paren", + "info": "none", + "args": + [{"atom": + {"val": "(", + "info": + {"original": + {"trailing": "", + "pos": 287, + "leading": "", + "endPos": 288}}}}, + {"node": + {"kind": "«term_*_»", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 288, + "leading": "", + "endPos": 289}}}}, + {"atom": + {"val": "*", + "info": + {"original": + {"trailing": " ", + "pos": 290, + "leading": "", + "endPos": 291}}}}, + {"node": + {"kind": "Lean.Parser.Term.app", + "info": "none", + "args": + [{"ident": + {"val": "Real.sin", + "rawVal": "Real.sin", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 292, + "leading": "", + "endPos": 300}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": "", + "pos": 301, + "leading": "", + "endPos": 302}}}}]}}]}}]}}, + {"atom": + {"val": ")", + "info": + {"original": + {"trailing": " ", + "pos": 302, + "leading": "", + "endPos": 303}}}}]}}]}}]}}]}}]}}, + {"node": + {"kind": "Lean.Parser.Command.declValSimple", + "info": "none", + "args": + [{"atom": + {"val": ":=", + "info": + {"original": + {"trailing": " ", "pos": 304, "leading": "", "endPos": 306}}}}, + {"node": + {"kind": "Lean.Parser.Term.byTactic", + "info": "none", + "args": + [{"atom": + {"val": "by", + "info": + {"original": + {"trailing": + "\n /-\n To find the minimum value of $\u000crac{9x^2\\sin^2 x + 4}{x\\sin x}$ for $0 < x < \\pi$, we need to show that it is at least 12. We start by noting that the expression can be rewritten using the division property of inequalities. We then use the fact that \\$sin x$ and $x$ are positive in the given range to establish the necessary inequalities. Finally, we apply these results to conclude that the minimum value is indeed 12.\n -/\n -- We start by ensuring that the product x * sin x is positive in the given range.\n ", + "pos": 307, + "leading": "", + "endPos": 309}}}}, + {"node": + {"kind": "Lean.Parser.Tactic.tacticSeq", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Tactic.tacticSeq1Indented", + "info": "none", + "args": + [{"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Tactic.tacticHave_", + "info": "none", + "args": + [{"atom": + {"val": "have", + "info": + {"original": + {"trailing": " ", + "pos": 829, + "leading": "", + "endPos": 833}}}}, + {"node": + {"kind": "Lean.Parser.Term.haveDecl", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.haveIdDecl", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.haveId", + "info": "none", + "args": + [{"ident": + {"val": "h₁", + "rawVal": "h₁", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 834, + "leading": "", + "endPos": 838}}}}]}}, + {"node": + {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.typeSpec", + "info": "none", + "args": + [{"atom": + {"val": ":", + "info": + {"original": + {"trailing": " ", + "pos": 839, + "leading": "", + "endPos": 840}}}}, + {"node": + {"kind": "«term_<_»", + "info": "none", + "args": + [{"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "0", + "info": + {"original": + {"trailing": " ", + "pos": 841, + "leading": "", + "endPos": 842}}}}]}}, + {"atom": + {"val": "<", + "info": + {"original": + {"trailing": " ", + "pos": 843, + "leading": "", + "endPos": 844}}}}, + {"node": + {"kind": "«term_*_»", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 845, + "leading": "", + "endPos": 846}}}}, + {"atom": + {"val": "*", + "info": + {"original": + {"trailing": " ", + "pos": 847, + "leading": "", + "endPos": 848}}}}, + {"node": + {"kind": "Lean.Parser.Term.app", + "info": "none", + "args": + [{"ident": + {"val": "Real.sin", + "rawVal": "Real.sin", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 849, + "leading": "", + "endPos": 857}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 858, + "leading": "", + "endPos": + 859}}}}]}}]}}]}}]}}]}}]}}, + {"atom": + {"val": ":=", + "info": + {"original": + {"trailing": " ", + "pos": 860, + "leading": "", + "endPos": 862}}}}, + {"node": + {"kind": "Lean.Parser.Term.byTactic", + "info": "none", + "args": + [{"atom": + {"val": "by", + "info": + {"original": + {"trailing": "\n ", + "pos": 863, + "leading": "", + "endPos": 865}}}}, + {"node": + {"kind": "Lean.Parser.Tactic.tacticSeq", + "info": "none", + "args": + [{"node": + {"kind": + "Lean.Parser.Tactic.tacticSeq1Indented", + "info": "none", + "args": + [{"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": + "Lean.Parser.Tactic.apply", + "info": "none", + "args": + [{"atom": + {"val": "apply", + "info": + {"original": + {"trailing": " ", + "pos": 870, + "leading": "", + "endPos": 875}}}}, + {"ident": + {"val": "mul_pos", + "rawVal": "mul_pos", + "preresolved": [], + "info": + {"original": + {"trailing": + "\n -- x is positive in the range (0, π).\n ", + "pos": 876, + "leading": "", + "endPos": 883}}}}]}}, + {"node": + {"kind": "null", + "info": "none", + "args": []}}, + {"node": + {"kind": + "Lean.Parser.Tactic.exact", + "info": "none", + "args": + [{"atom": + {"val": "exact", + "info": + {"original": + {"trailing": " ", + "pos": 931, + "leading": "", + "endPos": 936}}}}, + {"node": + {"kind": + "Lean.Parser.Term.proj", + "info": "none", + "args": + [{"ident": + {"val": "h₀", + "rawVal": "h₀", + "preresolved": [], + "info": + {"original": + {"trailing": "", + "pos": 937, + "leading": "", + "endPos": 941}}}}, + {"atom": + {"val": ".", + "info": + {"original": + {"trailing": "", + "pos": 941, + "leading": "", + "endPos": 942}}}}, + {"node": + {"kind": "fieldIdx", + "info": "none", + "args": + [{"atom": + {"val": "1", + "info": + {"original": + {"trailing": + "\n -- sin x is positive in the range (0, π).\n ", + "pos": 942, + "leading": "", + "endPos": + 943}}}}]}}]}}]}}, + {"node": + {"kind": "null", + "info": "none", + "args": []}}, + {"node": + {"kind": + "Lean.Parser.Tactic.exact", + "info": "none", + "args": + [{"atom": + {"val": "exact", + "info": + {"original": + {"trailing": " ", + "pos": 995, + "leading": "", + "endPos": 1000}}}}, + {"node": + {"kind": + "Lean.Parser.Term.app", + "info": "none", + "args": + [{"ident": + {"val": + "Real.sin_pos_of_pos_of_lt_pi", + "rawVal": + "Real.sin_pos_of_pos_of_lt_pi", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 1001, + "leading": "", + "endPos": 1029}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": + "Lean.Parser.Term.proj", + "info": "none", + "args": + [{"ident": + {"val": "h₀", + "rawVal": "h₀", + "preresolved": [], + "info": + {"original": + {"trailing": "", + "pos": 1030, + "leading": "", + "endPos": 1034}}}}, + {"atom": + {"val": ".", + "info": + {"original": + {"trailing": "", + "pos": 1034, + "leading": "", + "endPos": 1035}}}}, + {"node": + {"kind": "fieldIdx", + "info": "none", + "args": + [{"atom": + {"val": "1", + "info": + {"original": + {"trailing": " ", + "pos": 1035, + "leading": "", + "endPos": + 1036}}}}]}}]}}, + {"node": + {"kind": + "Lean.Parser.Term.proj", + "info": "none", + "args": + [{"ident": + {"val": "h₀", + "rawVal": "h₀", + "preresolved": [], + "info": + {"original": + {"trailing": "", + "pos": 1037, + "leading": "", + "endPos": 1041}}}}, + {"atom": + {"val": ".", + "info": + {"original": + {"trailing": "", + "pos": 1041, + "leading": "", + "endPos": 1042}}}}, + {"node": + {"kind": "fieldIdx", + "info": "none", + "args": + [{"atom": + {"val": "2", + "info": + {"original": + {"trailing": + "\n -- Using the division property of inequalities, we rewrite the expression.\n ", + "pos": 1042, + "leading": "", + "endPos": + 1043}}}}]}}]}}]}}]}}]}}]}}]}}]}}]}}]}}]}}]}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "Lean.Parser.Tactic.rwSeq", + "info": "none", + "args": + [{"atom": + {"val": "rw", + "info": + {"original": + {"trailing": " ", + "pos": 1123, + "leading": "", + "endPos": 1125}}}}, + {"node": + {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "Lean.Parser.Tactic.rwRuleSeq", + "info": "none", + "args": + [{"atom": + {"val": "[", + "info": + {"original": + {"trailing": "", + "pos": 1126, + "leading": "", + "endPos": 1127}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Tactic.rwRule", + "info": "none", + "args": + [{"node": + {"kind": "null", + "info": "none", + "args": []}}, + {"node": + {"kind": "Lean.Parser.Term.app", + "info": "none", + "args": + [{"ident": + {"val": "le_div_iff", + "rawVal": "le_div_iff", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 1127, + "leading": "", + "endPos": 1137}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "h₁", + "rawVal": "h₁", + "preresolved": [], + "info": + {"original": + {"trailing": "", + "pos": 1138, + "leading": "", + "endPos": 1142}}}}]}}]}}]}}]}}, + {"atom": + {"val": "]", + "info": + {"original": + {"trailing": + "\n /- tactic state:\n x : ℝ\n h₀ : 0 < x ∧ x < π\n h₁ : 0 < x * x.sin\n ⊢ 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4\n -/\n -- This is equivalent to showing that 9x^2 sin^2 x - 12x sin x + 4 ≥ 0, and the left hand side can be rewritten as a perfect square (3x sin x - 2)^2.\n -- We use the fact that (3x sin x - 2)^2 is non-negative to establish this.\n ", + "pos": 1142, + "leading": "", + "endPos": 1143}}}}]}}, + {"node": + {"kind": "null", "info": "none", "args": []}}]}}, + {"node": {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "nlinarith", + "info": "none", + "args": + [{"atom": + {"val": "nlinarith", + "info": + {"original": + {"trailing": " ", + "pos": 1524, + "leading": "", + "endPos": 1533}}}}, + {"node": + {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "linarithArgsRest", + "info": "none", + "args": + [{"node": + {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "null", "info": "none", "args": []}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"atom": + {"val": "[", + "info": + {"original": + {"trailing": "", + "pos": 1534, + "leading": "", + "endPos": 1535}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.app", + "info": "none", + "args": + [{"ident": + {"val": "sq_nonneg", + "rawVal": "sq_nonneg", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 1535, + "leading": "", + "endPos": 1544}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"node": + {"kind": "Lean.Parser.Term.paren", + "info": "none", + "args": + [{"atom": + {"val": "(", + "info": + {"original": + {"trailing": "", + "pos": 1545, + "leading": "", + "endPos": 1546}}}}, + {"node": + {"kind": "«term_-_»", + "info": "none", + "args": + [{"node": + {"kind": "«term_*_»", + "info": "none", + "args": + [{"node": + {"kind": "«term_*_»", + "info": "none", + "args": + [{"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "3", + "info": + {"original": + {"trailing": " ", + "pos": 1546, + "leading": "", + "endPos": + 1547}}}}]}}, + {"atom": + {"val": "*", + "info": + {"original": + {"trailing": " ", + "pos": 1548, + "leading": "", + "endPos": 1549}}}}, + {"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 1550, + "leading": "", + "endPos": 1551}}}}]}}, + {"atom": + {"val": "*", + "info": + {"original": + {"trailing": " ", + "pos": 1552, + "leading": "", + "endPos": 1553}}}}, + {"node": + {"kind": + "Lean.Parser.Term.app", + "info": "none", + "args": + [{"ident": + {"val": "Real.sin", + "rawVal": "Real.sin", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 1554, + "leading": "", + "endPos": 1562}}}}, + {"node": + {"kind": "null", + "info": "none", + "args": + [{"ident": + {"val": "x", + "rawVal": "x", + "preresolved": [], + "info": + {"original": + {"trailing": " ", + "pos": 1563, + "leading": "", + "endPos": + 1564}}}}]}}]}}]}}, + {"atom": + {"val": "-", + "info": + {"original": + {"trailing": " ", + "pos": 1565, + "leading": "", + "endPos": 1566}}}}, + {"node": + {"kind": "num", + "info": "none", + "args": + [{"atom": + {"val": "2", + "info": + {"original": + {"trailing": "", + "pos": 1567, + "leading": "", + "endPos": 1568}}}}]}}]}}, + {"atom": + {"val": ")", + "info": + {"original": + {"trailing": "", + "pos": 1568, + "leading": "", + "endPos": 1569}}}}]}}]}}]}}]}}, + {"atom": + {"val": "]", + "info": + {"original": + {"trailing": "\n", + "pos": 1569, + "leading": "", + "endPos": 1570}}}}]}}]}}]}}]}}]}}]}}]}}, + {"node": + {"kind": "Lean.Parser.Termination.suffix", + "info": "none", + "args": + [{"node": {"kind": "null", "info": "none", "args": []}}, + {"node": {"kind": "null", "info": "none", "args": []}}]}}, + {"node": {"kind": "null", "info": "none", "args": []}}]}}]}}]}}]}} + diff --git a/test/aime_1983_p9.in b/test/aime_1983_p9.in new file mode 100644 index 00000000..02fd34a9 --- /dev/null +++ b/test/aime_1983_p9.in @@ -0,0 +1,2 @@ +{"cmd": "\nimport Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n\n/-- Show that $\frac{9x^2\\sin^2 x + 4}{x\\sin x} \\geq 12$ for $0 < x < \\pi$.-/\ntheorem aime_1983_p9 (x : ℝ) (h₀ : 0 < x ∧ x < Real.pi) :\n 12 ≤ (9 * (x ^ 2 * Real.sin x ^ 2) + 4) / (x * Real.sin x) := by\n /-\n To find the minimum value of $\frac{9x^2\\sin^2 x + 4}{x\\sin x}$ for $0 < x < \\pi$, we need to show that it is at least 12. We start by noting that the expression can be rewritten using the division property of inequalities. We then use the fact that \\$sin x$ and $x$ are positive in the given range to establish the necessary inequalities. Finally, we apply these results to conclude that the minimum value is indeed 12.\n -/\n -- We start by ensuring that the product x * sin x is positive in the given range.\n have h₁ : 0 < x * Real.sin x := by\n apply mul_pos\n -- x is positive in the range (0, π).\n exact h₀.1\n -- sin x is positive in the range (0, π).\n exact Real.sin_pos_of_pos_of_lt_pi h₀.1 h₀.2\n -- Using the division property of inequalities, we rewrite the expression.\n rw [le_div_iff h₁]\n /- tactic state:\n x : ℝ\n h₀ : 0 < x ∧ x < π\n h₁ : 0 < x * x.sin\n ⊢ 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4\n -/\n -- This is equivalent to showing that 9x^2 sin^2 x - 12x sin x + 4 ≥ 0, and the left hand side can be rewritten as a perfect square (3x sin x - 2)^2.\n -- We use the fact that (3x sin x - 2)^2 is non-negative to establish this.\n nlinarith [sq_nonneg (3 * x * Real.sin x - 2)]\n", "allTactics": false, "ast": true, "tactics": true, "premises": true} +