Fix a few minor Lean misformalisations #210
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ocfnash
force-pushed
the
fixes_20240904
branch
from
46e120f
to
f469d27
Compare
ocfnash
force-pushed
the
fixes_20240904
branch
from
c10cab3
to
59d9c41
Compare
This was disprovable because the key predicate did not quantify over all groups (and the goal was false even for the trivial group).
The original form was disprovable because of quantifier confusion (e.g., taking `x` and `y` to be non-zero and constant gave a contradiction).
This was disprovable because the argument `ha : SDiff (Finset a)` allowed the user to fill in any function for the set difference function. So for example by providing a dummy set difference function that just always returned the empty set, the goal was false. Presumably this error arose because the original formaliser found that they could not use the existing set difference function out of the box. The right fix is either to put `open Classical` before the proof or to add the typeclass argument `[DecidableEq a]`. In the end I have provided rewrite since the original formalisation is a bit more complicated than it needs to be.
This was disprovable because it did not restrict `x` and `y` to the positive quadrant. The informal statement is quite sloppy in this same sense (presumably because non-integral powers of negative reals are not defined). I have also proposed changing the implementation of "tangent to the curve" since a priori a line could intersect a degree `m` curve in up to `m` points so the naive set-counting definition is arguably too strong.
This was disprovable because the hypothesis `apos : a > 0` means that `0 ≤ a n` for all `n` and there exists some `n` such that `0 < a n`. (So the sequence: 1, 0, 0, 0, 0, ... was admissible and provided a counter example to the statement.)
This was previously "fixed" in c75c0b0 but unfortunately an error remained.
This was disprovable because of a minor Mathlib footgun: namely the limsup of a real-valued function which is not bounded above is zero.
This was disprovable because the zero function was excluded from the solution set. The fix is to replace `a > 0` with `a ≥ 0` in the solution. Other changes are just style. There is incidentally a sharper version of this question which requires establishing which solutions correspond to functions with finite / infinite domain. However this is not actually asked.
ocfnash
force-pushed
the
fixes_20240904
branch
from
59d9c41
to
c109419
Compare
GeorgeTsoukalas
approved these changes
Sep 9, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.