coq: the Trinity proofs do not compile — CorePhi.v:14 uses a lemma that does not exist #3328

Found by repairing coq-proofs.yml (#3316, #3324, #3326). That workflow had never got past opam install, so coqc has never run on these files in CI. With the two workflow defects fixed, it does — and the first line it reaches fails:

File "./CorePhi.v", line 14, characters 8-24:
Error: The variable Rmult_lt_pos_pos was not found in the current environment.

What is wrong

Rmult_lt_pos_pos is used at proofs/trinity/CorePhi.v:14 and
proofs/trinity/AlphaPhi.v:27, and is defined nowhere in the repository. It
is not in Coq's Reals. The lemma with that statement is:

Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2

CorePhi.v requires only Reals.Reals, so neither Interval nor Coquelicot is in
scope at that point.

A rename is not enough

Lemma phi_pos : 0 < phi.
Proof.
  unfold phi.
  apply Rmult_lt_pos_pos.
  - apply (Rlt_trans 0 2). lra.
  - apply Rle_lt_trans with (sqrt(5) + 0).
  ...

After unfold phi the goal is 0 < (1 + sqrt 5) / 2. apply (Rlt_trans 0 2)
leaves two goals, 0 < 2 and 2 < 1 + sqrt 5; lra closes the first and
cannot close the second without a bound on sqrt 5. So phi_pos needs
rewriting, not a substitution.

Scope

This is proof work, not configuration, and it is deliberately not attempted from
the CI loop — iterating a Coq proof blind through a 4-minute cycle is the wrong
instrument. It needs someone with Coq locally.

CorePhi.v is the first file in the compile order, so nothing downstream has
been checked either. The 13 files compile in dependency order and the run stops
at file 1 — the state of the other 12 is unknown, not passing.

Related

• ci: repair the two workflows whose failure was in the workflow #3324 — OPAMROOT, and adding this workflow to its own pull_request paths
• ci(coq): unpin coq-interval, which required a Coq the image does not have #3326 — the coq-interval pin required a Coq older than the image
• Every workflow red on master, diagnosed: 5 fixable, 4 leave, 1 wrong trigger, 0 to delete #3316 — the never-green triage this came out of

Boundary

proofs/trinity/CorePhi.v
proofs/trinity/AlphaPhi.v