refactor: remove h_mono from PolyTimeComputable.comp#396
refactor: remove h_mono from PolyTimeComputable.comp#396JohnEdwardJennings wants to merge 1 commit intoleanprover:mainfrom
Conversation
JohnEdwardJennings
requested review from
chenson2018 and
fmontesi
as code owners
|
@BoltonBailey Could you have a first look at this since it was your TODO comment? |
|
Yep, this resolves the issue. I will leave some review comments but otherwise this seems like a good solution. |
| outputsFunInTime a := | ||
| RelatesWithinSteps.of_le (hf.outputsFunInTime a) (le_monotonizeBound _ _) | ||
|
|
||
| set_option linter.unusedSectionVars false in |
There was a problem hiding this comment.
It seems the issue here is better solved by removing the redundant variable [Inhabited Symbol] [Fintype Symbol] above than by silencing the linter.
There was a problem hiding this comment.
(I guess my fault for not catching this, in my defense it is hard to know what variables are present, the VSCode extension/LSP should do a better job of showing this)
|
|
||
| -- TODO remove `h_mono` assumption | ||
| -- by developing function to convert PolyTimeComputable into one with monotone time bound | ||
| private lemma Polynomial.eval_mono_nat {p : Polynomial ℕ} {a b : ℕ} (h : a ≤ b) : |
There was a problem hiding this comment.
I don't know if this lemma should be private. Rather, I think I would hide it away in a file in /Data.
It is a bit surprising that there is not a more general version in mathlib somewhere that says that p.eval is monotone if all the coefficients are nonnegative / if the semiring we are working over has a typeclass that says every element is nonnegative, but I am not sure what CSLib's stance on generality is.
| /-- | ||
| Convert a `PolyTimeComputable` to one with a monotone time bound. | ||
| -/ | ||
| private noncomputable def PolyTimeComputable.withMonotoneBound {f : List Symbol → List Symbol} |
There was a problem hiding this comment.
I also don't think this has to be private.
| /-- | ||
| Monotonize a function `f : ℕ → ℕ` by taking the supremum over all values up to `n`. | ||
| -/ | ||
| def monotonizeBound (f : ℕ → ℕ) (n : ℕ) : ℕ := |
There was a problem hiding this comment.
I might put this definition and lemmas in a file in /Data, as it seems generally useful.
3 participants
This PR adds proofs autoformalised by @Aristotle-Harmonic.
Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun
Fixes #378
Summary of changes:
Resolved the TODO on lines 487-488 of
Cslib/Computability/Machines/SingleTapeTuring/Basic.leanwhich asked to remove theh_mono : Monotone hg.time_boundassumption fromPolyTimeComputable.compby developing a function to convert aPolyTimeComputableinto one with a monotone time bound.Changes made:
Added
monotonizeBound— a function that monotonizesf : ℕ → ℕby taking(Finset.range (n+1)).sup' ... f, i.e. the maximum offover{0, ..., n}.Added supporting lemmas:
monotonizeBound_mono: the monotonized bound is monotonele_monotonizeBound: the original function is bounded by the monotonized versionmonotonizeBound_le_of_le: iffis bounded by a monotoneg, the monotonizedfis also bounded bygAdded
TimeComputable.withMonotoneBound— converts aTimeComputableto one with a monotone time bound usingmonotonizeBound.Added
PolyTimeComputable.withMonotoneBound— converts aPolyTimeComputableto one with a monotone time bound, preserving the polynomial bound (using the fact thatPolynomial.eval_monogives monotonicity of polynomial evaluation overℕ).Removed
h_monofromPolyTimeComputable.comp— the composition now internally monotonizeshg's time bound before passing it toTimeComputable.comp, eliminating the need for the caller to supply a monotonicity proof.