Missing side conditions #2
Description
There are some known issues in the source Lean files.
They have been correctly translated to Rocq, but not provable in their current form.
Summary
| File | Issue Type |
|---|---|
| amc12a_2019_p12.v | Missing positivity |
| aime_1994_p3.v | Quantifier scope |
| imo_1968_p5_1.v | Missing well-formedness |
| imo_2019_p1.v | Quantifier scope |
| imo_1982_p1.v | Nat subtraction semantics |
| amc12a_2020_p15.v | Wrong formalization |
| amc12a_2020_p25.v | Missing constraints |
| mathd_numbertheory_618.v | Missing edge case |
Detailed Fixes
1. amc12a_2019_p12.v - Missing Positivity Hypotheses
Issue: Uses ln x, ln y without requiring x > 0, y > 0.
Informal statement: "Positive real numbers x ≠ 1 and y ≠ 1..."
Current:
Theorem amc12a_2019_p12:
forall (x y : R),
(x <> 1) /\ (y <> 1) ->
(ln x / ln 2 = ln 16 / ln y) ->
(x * y = 64) ->
(ln (x / y) / ln 2)^2 = 20.Proposed:
Theorem amc12a_2019_p12:
forall (x y : R),
0 < x -> 0 < y ->
x <> 1 -> y <> 1 ->
(ln x / ln 2 = ln 16 / ln y) ->
(x * y = 64) ->
(ln (x / y) / ln 2)^2 = 20.Justification: Matches informal statement and ensures ln is well-defined.
2. aime_1994_p3.v - Quantifier Scope Error
Issue: Functional equation only holds for one arbitrary x, not all x.
Informal statement: "for each real number x, f(x)+f(x-1) = x²"
Current:
Theorem aime_1994_p3:
forall (x : Z) (f : Z -> Z),
(f x + f (x - 1) = x * x) -> (f 19 = 94) -> (f 94 mod 1000 = 561).Proposed:
Theorem aime_1994_p3:
forall (f : Z -> Z),
(forall x : Z, f x + f (x - 1) = x * x) ->
(f 19 = 94) ->
(f 94 mod 1000 = 561).Justification: The functional equation must hold for ALL x, not just one.
3. imo_1968_p5_1.v - Missing Well-formedness Constraint
Issue: sqrt(f(x) - f(x)²) requires 0 ≤ f(x) ≤ 1 for the argument to be non-negative.
Informal statement: Implicitly assumes f maps to [0,1]. The proof notes "f(x+a) ≥ 1/2".
Current:
Theorem imo_1968_p5_1 :
forall (a : R) (f : R -> R),
0 < a ->
(forall x, f (x + a) = 1 / 2 + sqrt (f x - (f x)^2)) ->
exists b : R, b > 0 /\ forall x, f (x + b) = f x.Proposed:
Theorem imo_1968_p5_1 :
forall (a : R) (f : R -> R),
0 < a ->
(forall x, 0 <= f x <= 1) ->
(forall x, f (x + a) = 1 / 2 + sqrt (f x - (f x)^2)) ->
exists b : R, b > 0 /\ forall x, f (x + b) = f x.Justification: Ensures sqrt argument is non-negative.
4. imo_2019_p1.v - Malformed Conclusion (Quantifier Scope)
Issue: The conclusion has wrong quantifier nesting.
Informal statement: Solutions are (1) f(z) = 0 for all z, or (2) f(z) = 2z + c for some constant c.
Current:
Theorem imo_2019_p1 (f : Z -> Z) :
(forall a b, f (2 * a) + (2 * f b) = f (f (a + b))) <->
(forall z, f z = 0 \/ exists c, forall z, f z = 2 * z + c).Problem: forall z, f z = 0 \/ exists c, forall z, ... is wrong. The outer forall z shouldn't be there.
Proposed:
Theorem imo_2019_p1 (f : Z -> Z) :
(forall a b, f (2 * a) + (2 * f b) = f (f (a + b))) <->
((forall z, f z = 0) \/ (exists c, forall z, f z = 2 * z + c)).Justification: Correctly captures "either f is zero everywhere, or f(z) = 2z+c for some c".
5. imo_1982_p1.v - Natural Number Subtraction Semantics
Issue: f(m+n) - f(m) - f(n) uses nat subtraction which truncates to 0 if negative.
Informal statement: "f(m+n) - f(m) - f(n) = 0 or 1" (assumes result is non-negative)
Current:
Theorem imo_1982_p1:
forall (f : nat -> nat),
(forall m n, 0 < m -> 0 < n -> (f (m + n) - f m - f n = 0 \/ f (m + n) - f m - f n = 1)) ->
f 2 = 0 ->
0 < f 3 ->
f 9999 = 3333 ->
f 1982 = 660.Proposed:
Theorem imo_1982_p1:
forall (f : nat -> nat),
(forall m n, 0 < m -> 0 < n ->
f m + f n <= f (m + n) /\ f (m + n) <= f m + f n + 1) ->
f 2 = 0 ->
0 < f 3 ->
f 9999 = 3333 ->
f 1982 = 660.Justification: Avoids nat subtraction semantics; captures "f(m+n) - f(m) - f(n) ∈ {0,1}" correctly.
6. amc12a_2020_p15.v - Wrong Formalization (Bound vs Maximum)
Issue: States upper bound, but problem asks for the greatest distance (exact maximum).
Informal statement: "What is the greatest distance between a point of A and a point of B?"
Current:
Theorem amc12a_2020_p15 :
forall (a b : C),
(a^3 - 8 = 0)%C ->
(b^3 - 8 * b^2 - 8 * b + 64 = 0)%C ->
Cmod (a - b) <= 2 * sqrt 21.Proposed:
Theorem amc12a_2020_p15 :
(* The maximum distance is exactly 2*sqrt(21) *)
(exists (a b : C),
(a^3 - 8 = 0)%C /\
(b^3 - 8 * b^2 - 8 * b + 64 = 0)%C /\
Cmod (a - b) = 2 * sqrt 21) /\
(* And this is an upper bound *)
(forall (a b : C),
(a^3 - 8 = 0)%C ->
(b^3 - 8 * b^2 - 8 * b + 64 = 0)%C ->
Cmod (a - b) <= 2 * sqrt 21).Justification: Captures that 2√21 is achieved (not just an upper bound).
7. amc12a_2020_p25.v - Missing Constraints
Issue: Rpower x 2 requires x > 0; also p, q should be positive.
Current:
Theorem amc12a_2020_p25 :
forall (p q : nat), Nat.gcd p q = 1%nat ->
forall (S : list R),
(forall x : R, In x S <->
(IZR (Int_part x) * (x - IZR (Int_part x)) = INR p / INR q * Rpower x 2))
-> NoDup S
-> fold_left Rplus S 0 = 420
-> (p + q = 929)%nat.Proposed:
Theorem amc12a_2020_p25 :
forall (p q : nat),
0 < p -> 0 < q ->
Nat.gcd p q = 1%nat ->
forall (S : list R),
(forall x : R, In x S <->
(0 < x /\ IZR (Int_part x) * (x - IZR (Int_part x)) = INR p / INR q * x^2))
-> NoDup S
-> fold_left Rplus S 0 = 420
-> (p + q = 929)%nat.Justification:
- Added
0 < pand0 < qto ensure fraction is well-defined - Changed
Rpower x 2tox^2(works for all reals) - Added
0 < xconstraint to match floor function behavior expected in problem
8. mathd_numbertheory_618.v - Missing Edge Case in Conclusion
Issue: Theorem is FALSE for n = 0. p(0) = p(1) = 41, so gcd(p(0), p(1)) = 41 > 1, but conclusion requires 41 <= 0.
Mathematical fact: For Euler's polynomial p(n) = n² - n + 41, gcd(p(n), p(n+1)) > 1 iff n = 0 or n >= 41.
Current:
Theorem mathd_numbertheory_618:
forall n : nat,
forall p : nat -> nat,
(forall x, p x = x*x - x + 41) ->
1 < Nat.gcd (p n) (p (S n)) ->
41 <= n.Proposed:
Theorem mathd_numbertheory_618:
forall n : nat,
forall p : nat -> nat,
(forall x, p x = x*x - x + 41) ->
1 < Nat.gcd (p n) (p (S n)) ->
n = 0 \/ 41 <= n.Justification: n = 0 is a valid case where gcd(p(n), p(n+1)) > 1 since p(0) = p(1) = 41.