lean-eval Aristotle (Harmonic) submission for bvp_comparison

Challenge.lean

import Mathlib

theorem bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 ⊆ J)
    (u v : ℝ → ℝ)
    (hu : ∀ x ∈ J, HasDerivAt u (deriv u x) x)
    (hu' : ∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) x)
    (hv : ∀ x ∈ J, HasDerivAt v (deriv v x) x)
    (hv' : ∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) x)
    (hineq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x ≤ -deriv (deriv v) x)
    (hu0 : u 0 ≤ v 0) (hu1 : u 1 ≤ v 1) :
    ∀ x ∈ Set.Icc (0 : ℝ) 1, u x ≤ v x := by
  sorry

config.json

{
  "challenge_module": "Challenge",
  "solution_module": "Solution",
  "theorem_names": [
    "bvp_comparison"
  ],
  "permitted_axioms": [
    "propext",
    "Quot.sound",
    "Classical.choice"
  ],
  "enable_nanoda": false
}

Helpers.lean

namespace Submission.Helpers

end Submission.Helpers

lakefile.toml

name = "bvp_comparison"
testDriver = "workspace_test"
defaultTargets = ["Challenge", "Solution", "Submission"]

[leanOptions]
autoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "5450b53e5ddc"

[[lean_lib]]
name = "Challenge"

[[lean_lib]]
name = "Solution"

[[lean_lib]]
name = "Submission"

[[lean_exe]]
name = "workspace_test"
root = "WorkspaceTest"

lean-toolchain

leanprover/lean4:v4.30.0-rc2

Solution.lean

import Mathlib
import Submission

theorem bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 ⊆ J)
    (u v : ℝ → ℝ)
    (hu : ∀ x ∈ J, HasDerivAt u (deriv u x) x)
    (hu' : ∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) x)
    (hv : ∀ x ∈ J, HasDerivAt v (deriv v x) x)
    (hv' : ∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) x)
    (hineq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x ≤ -deriv (deriv v) x)
    (hu0 : u 0 ≤ v 0) (hu1 : u 1 ≤ v 1) :
    ∀ x ∈ Set.Icc (0 : ℝ) 1, u x ≤ v x := by
  exact Submission.bvp_comparison J hJ_open hJ_sub u v hu hu' hv hv' hineq hu0 hu1

Submission.lean

import Mathlib

namespace Submission

theorem bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 ⊆ J)
    (u v : ℝ → ℝ)
    (hu : ∀ x ∈ J, HasDerivAt u (deriv u x) x)
    (hu' : ∀ x ∈ J, HasDerivAt (deriv u) (deriv (deriv u) x) x)
    (hv : ∀ x ∈ J, HasDerivAt v (deriv v x) x)
    (hv' : ∀ x ∈ J, HasDerivAt (deriv v) (deriv (deriv v) x) x)
    (hineq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x ≤ -deriv (deriv v) x)
    (hu0 : u 0 ≤ v 0) (hu1 : u 1 ≤ v 1) :
    ∀ x ∈ Set.Icc (0 : ℝ) 1, u x ≤ v x := by
  -- Define $w(x) = u(x) - v(x)$.
  set w : ℝ → ℝ := fun x => u x - v x;
  -- By definition of $w$, we know that $w''(x) \geq 0$ for all $x \in (0,1)$.
  have hw''_nonneg : ∀ x ∈ Set.Ioo 0 1, deriv^[2] w x ≥ 0 := by
    simp +zetaDelta at *;
    intro x hx₁ hx₂; rw [ show deriv ( deriv fun x => u x - v x ) x = deriv ( fun x => deriv u x - deriv v x ) x from Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_of_mem ( Ioo_mem_nhds hx₁ hx₂ ) fun y hy => deriv_sub ( hu y <| hJ_sub <| Set.Ioo_subset_Icc_self hy ) ( hv y <| hJ_sub <| Set.Ioo_subset_Icc_self hy ) ] ;
    norm_num [ hu' x ( hJ_sub <| Set.mem_Icc.mpr ⟨ hx₁.le, hx₂.le ⟩ ), hv' x ( hJ_sub <| Set.mem_Icc.mpr ⟨ hx₁.le, hx₂.le ⟩ ) ] ; linarith [ hineq x hx₁ hx₂ ];
  -- Since $w''(x) \geq 0$ for all $x \in (0,1)$, $w$ is convex on $[0,1]$.
  have hw_convex : ConvexOn ℝ (Set.Icc 0 1) w := by
    apply_rules [ convexOn_of_deriv2_nonneg, convex_Icc ];
    · exact ContinuousOn.sub ( continuousOn_of_forall_continuousAt fun x hx => HasDerivAt.continuousAt ( hu x ( hJ_sub hx ) ) ) ( continuousOn_of_forall_continuousAt fun x hx => HasDerivAt.continuousAt ( hv x ( hJ_sub hx ) ) );
    · exact fun x hx => DifferentiableAt.differentiableWithinAt ( by exact DifferentiableAt.sub ( hu x ( hJ_sub <| interior_subset hx ) |> HasDerivAt.differentiableAt ) ( hv x ( hJ_sub <| interior_subset hx ) |> HasDerivAt.differentiableAt ) );
    · norm_num +zetaDelta at *;
      refine' DifferentiableOn.congr _ _;
      exacts [ fun x => deriv u x - deriv v x, fun x hx => DifferentiableAt.differentiableWithinAt ( by exact DifferentiableAt.sub ( hu' x ( hJ_sub <| Set.Ioo_subset_Icc_self hx ) ) ( hv' x ( hJ_sub <| Set.Ioo_subset_Icc_self hx ) ) ), fun x hx => deriv_sub ( hu x ( hJ_sub <| Set.Ioo_subset_Icc_self hx ) ) ( hv x ( hJ_sub <| Set.Ioo_subset_Icc_self hx ) ) ];
    · aesop;
  intro x hx;
  have := hw_convex.2 ( show 0 ∈ Set.Icc 0 1 by norm_num ) ( show 1 ∈ Set.Icc 0 1 by norm_num );
  simp +zetaDelta at *;
  nlinarith [ this ( show 0 ≤ 1 - x by linarith ) ( show 0 ≤ x by linarith ) ( by linarith ) ]

end Submission

WorkspaceTest.lean

import Lean

open Lean

def comparatorExists (comparatorBin : String) : IO Bool := do
  if comparatorBin.contains '/' then
    return (← System.FilePath.pathExists comparatorBin)
  try
    let child ← IO.Process.spawn {
      cmd := "sh"
      args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin]
    }
    let exitCode ← child.wait
    return exitCode == 0
  catch _ =>
    return false

def main : IO UInt32 := do
  let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
  if !(← comparatorExists comparatorBin) then
    IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
    IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
    IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
    pure 1
  else
    try
      let child ← IO.Process.spawn {
        cmd := "lake"
        args := #["env", comparatorBin, "config.json"]
      }
      let exitCode ← child.wait
      pure exitCode
    catch err =>
      IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
      IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
      IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
      IO.eprintln s!"Original error: {err}"
      pure 1