Putname 1980 A5 issues

[LasseBlaauwbroek]

Again a problem from the paper:

https://github.com/trishullab/PutnamBench/blob/6ddcaacfafbdcc16cf72740f78c7f3709328492b/coq/src/putnam_1980_a5.v#L2-L10

• The integrals are parameterized on a nat but should be on a real.
• The theorem states that the largest parameter for which the integrals are zero is bounded. It should instead be bounding the number of parameters where the integral is zero.
• Is the successor function in p really needed? Not sure, but this might be a off-by-one error.

[eric-wieser]

Is #166 a problem for Coq too? Or does := mean something different?

[LasseBlaauwbroek]

It shouldn't be a correctness issue. In Coq, (H := t) means the same as let H := t in .... I creates a local definition that becomes part of the proof state.

That being said, I'm not a fan of extensive usage of this pattern. In some cases, it might be okay. But these local definitions tend to massively pollute the proof state and are easily unfolded (making things even worse). Moreover, one often has to prove some lemmas about these local definitions. As a human, I would strongly prefer to do so as separate lemmas. I tried to prove some of the formalized statements, and this was not a fun experience, in part due to these local definitions.

[eric-wieser]

Interesting; in lean, theorem foo (H : T := t) : G means the same as theorem foo (H : T) : G, except that foo is a shorthand for foo t (that is, the semantics are the same as default arguments in Python).

[GeorgeTsoukalas]

Yeah, this formalization is inaccurate. Thanks for pointing it out. What do you think about the following one, which uses mathcomp?

From mathcomp Require Import all_algebra all_ssreflect.
From mathcomp Require Import reals trigo lebesgue_integral lebesgue_measure measure.
From mathcomp Require Import classical_sets cardinality.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Variable R : realType.
Definition mu := [the measure _ _ of @lebesgue_measure R].
Theorem putnam_1980_a5
    (P : {poly R})
    (Pnonconst : gtn (size P) (1%nat))
    : finite_set [set x : R | \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun x => P.[x] * (sin x)) t = 0 /\ \int[mu]_(t in [set t : R | 0 <= t <= x]) (fun x => P.[x] * (cos x)) t = 0].
Proof. Admitted.

[LasseBlaauwbroek]

I'm not knowledgeable enough in mathcomp-analysis to judge this. All I can say is that it doesn't look obviously wrong. But you should really ask the authors of mathcomp-analysis.