fix(proofs): comprehensively nat-annotate EchidnaNat to green the Isabelle base#282
Merged
Conversation
Two pre-existing failures left red on main after #220 merged: - agda-meta-checker.yml: `cabal install Agda-2.7.0.1` aborts on a warm ~/.cabal cache with "Path '.../bin/agda' already exists"; add --overwrite-policy=always so the install is idempotent. Until this lands the Agda meta-checker never actually runs in CI. - contractile.just defined a `heal` recipe that collides with the root Justfile's `heal` across `import?`, so `just` aborts with a duplicate-recipe error — breaking every `just` call incl. MVP Smoke's `just mvp-env`. Drop the contractile copy; keep the richer root recipe (and contractile's heal-provers). https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
ProverKindInjectivity.idr:
- Replace all 107 LTESucc towers with lteLit calls (eliminates off-by-one
bug class permanently; Nunchaku was -1 close and Faial was +1)
- Add `import NatLte` for the machine-checked LTE helper
- Fix docstring range [0, 104] -> [0, 106] to match actual max discriminant
DispatchCorrectness.idr:
- Remove `import EchidnaABI.Provers` (pulls in a conflicting `proverLogic`
from InteractiveAssistants; file only needs EchidnaABI.Types)
- Allows file to type-check with the echidnaabi package installed
proofs/agda/Basic.agda:
- Hoist `data ℕ` and `data _≡_` to module scope (were only in `where`
blocks, causing scope errors when used in type signatures)
- Remove duplicate `data _≡_` from CombinatorLaws/CurryUncurryLaws
(they now inherit from module scope)
- Instantiate SKK's second const with {B = A} to resolve unsolved meta
All 11 verification/proofs/idris2/ files now pass `idris2 --check`.
12/13 proofs/agda/ files pass (DispatchOrdering needs stdlib 2.1).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Coq: - proofs/coq/nat.v: fix Nat.lt_irrefl/Nat.lt_trans usage for stdlib compat - proofs/coq/list.v: fix in_filter backward direction — case-split on (f h) first so congruence can close the x=h/f h=false/f x=true contradiction - proofs/coq/algebra/GroupTheory.v: complete rewrite; make G implicit in GroupAxioms Record so projections unify; remove Section (explicit params per theorem); fix rewrite direction in left_cancel (forward) vs right_cancel (backward); fix inv_mul associativity rewrite chain Lean4: - proofs/lean/Nat.lean, List.lean, Propositional.lean: fix imports and theorem statements for Lean 4.x stdlib API - proofs/lean/algebra/GroupTheory.lean: port group theory proofs to Lean4 - proofs/lean/ECHIDNA.lean: add root module required by lakefile roots Agda: - proofs/agda/DispatchOrdering.agda: replace z<s/s<s (not in installed stdlib) with s≤s z≤n; Fin._<_ = ℕ._<_ on toℕ = suc · ≤ · suc Idris2: - src/idris/Validator.idr: rename bound var `proof` → `pterm` throughout; `proof` is a reserved keyword in Idris2 0.8.0 (Idris1 tactic holdover) Build: - .gitignore: add proofs/agda/**/dist-newstyle/, proofs/lean/**/.lake/, .lia.cache, .nia.cache - proofs/lean/lake-manifest.json: add empty Lake lock file (no ext deps) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…idator)
The proof corpus had zero CI coverage: agda-meta-checker.yml only triggers
on meta-checker/**, idris2-abi-ci.yml only on src/abi/**, and there was no
Coq or Lean workflow at all. So proofs/{coq,lean,agda} and src/idris were
never type-checked in CI — a green PR proved nothing about the proofs and
regressions would land silently.
New dogfood-proofs-ci.yml with three jobs (Coq via apt, Lean 4 via elan,
Agda 2.7.0.1 + stdlib v2.1), each calling a just recipe so local and CI run
identical commands (RSR-H14). idris2-abi-ci.yml extended to also type-check
the src/idris validator (reuses its Idris2 install; adds src/idris/** to the
path trigger).
Closing the gap surfaced two latent bugs the absent CI had hidden:
- proofs/lean/lakefile.lean rooted only `ECHIDNA`, whose umbrella imported
4 of 6 files; `lake build` silently skipped algebra/GroupTheory.lean and
mvp_basic.lean, and in fact failed outright ("unknown module prefix
'Basic'") because the top-level modules were not in the lib's module
space. Now every proof file is a root and ECHIDNA.lean imports the whole
corpus.
- src/idris/echidna-validator.ipkg declares an executable (main = Validator)
but Validator.idr had no `main`, so `idris2 --build` failed with
"Undefined name Validator.main". Added `main = testValidation`.
New Justfile recipes: proofs, proofs-coq, proofs-lean, proofs-agda,
proofs-idris (proofs-agda exports LC_ALL=C.UTF-8 — Agda aborts under a
non-UTF-8 locale).
Verified locally against real toolchains: coqc 8.18.0 (5/5), Lean v4.13.0
lake build (6 modules + umbrella), agda (13/13), idris2 0.8.0 --typecheck.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Re-triggers the workflow's first real run (the initial PR run hit a startup_failure during workflow registration) and keeps the header comments ASCII for parser portability. No behavioural change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Temporary: reduce to one trivial job to localise the GitHub-parser rejection (passes yq + actionlint but startup_failures twice). Jobs restored in the next commit once the skeleton is confirmed to start. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…actions taiki-e/install-action reproducibly triggers a startup_failure in this workflow's context (bisected: header + checkout + run steps start fine; adding the action fails before any job runs, even though mvp-smoke.yml uses the same pin on main). Switch all toolchain installs to plain run steps -- apt for Coq and Agda, curl tarballs for elan and just -- matching the idris2/chapel workflows, which use only actions/checkout plus run steps. Agda now installs via apt (agda + agda-stdlib), which reproduces the local verification environment exactly. just is installed from its release tarball. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The Agda job failed with "Library 'standard-library' not found / Installed libraries: (none)": apt-get --fix-missing silently skips agda-stdlib when it can't be fetched, exiting 0, so the registration step found no .agda-lib and wrote an empty ~/.agda/libraries. Install only the agda binary via apt (2.6.3 on ubuntu-24.04) and fetch the matching stdlib v1.7.3 from GitHub, registering its explicit path -- the same deterministic pattern agda-meta-checker.yml uses. Verified locally: all 13 corpus files type-check against a fresh GitHub v1.7.3 in an isolated AGDA_DIR. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The trust-pipeline property proofs under verification/proofs/lean4
(ConfidenceLattice, ParetoMaximality, ParetoStrongMaximality,
IntegrityVerification, PortfolioCompleteness) had no CI coverage:
dogfood-proofs-ci gated only proofs/{coq,lean,agda} + src/idris, and the
idris2-abi / agda-meta-checker workflows are path-filtered to src/abi/**
and meta-checker/** respectively, so this corpus fell through every
filter.
Add a `verif-lean` job mirroring the existing `lean` job (elan shim +
pinned-toolchain pre-install with retry/backoff, then `just`), reading
the pin from verification/proofs/lean4/lean-toolchain and running a new
`just proofs-verif-lean` recipe (cd verification/proofs/lean4 && lake
build). No mathlib dependency (lake-manifest packages: []), so it builds
well under the 20-minute timeout. Extend the push/PR path triggers to
verification/proofs/lean4/**.
Verified locally on Lean 4.13.0: a fresh `lake build` (cleared
.lake/build first) compiles all five modules, exit 0, with zero
sorry/admit/axiom/native_decide across the corpus.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
…idris2)
The 11 trust-pipeline property proofs under verification/proofs/idris2
(AxiomCompleteness, AxiomPolicyOrdering, BasicTotality, ClampTrustBounds,
DispatchCorrectness, DispatchOrdering, NatLte, ProofStateSerialisation,
ProverKindInjectivity, TrustKernelMonotonicity, TrustLevelSoundness) had no
CI gate: dogfood-proofs-ci covered proofs/{coq,lean,agda} + src/idris and
(just-added) verification/proofs/lean4; idris2-abi-ci is path-filtered to
src/abi/** + src/idris/**. So this corpus fell through every filter.
Add:
- echidna-verif-proofs.ipkg listing all 11 modules with `depends = base,
echidnaabi`. DispatchCorrectness imports EchidnaABI.Types (the echidnaabi
package in src/abi), unresolvable by a standalone `idris2 --check`.
- `just proofs-verif-idris`: installs echidnaabi (--install builds it), then
`idris2 --typecheck echidna-verif-proofs.ipkg`; added to the `proofs` rollup.
- a `verif-idris` job in dogfood-proofs-ci.yml (apt idris2 + source fallback,
mirroring idris2-abi-ci) and verification/proofs/idris2/** path triggers.
Why an ipkg rather than a per-file `idris2 --check` loop: `idris2 --check`
exits 0 even when a module fails to resolve an import (verified: a
"Module ... not found" error prints but the process returns exit 0), which
would let a broken corpus pass CI silently. Building through the ipkg gives a
reliable aggregate exit code; the recipe additionally fails on any "Error"
line as a belt-and-suspenders guard.
Verified locally on idris2 0.8.0 from a clean state (ABI build + installed
package both removed first): `just proofs-verif-idris` type-checks all 11
modules, exit 0. Negative test -- injecting `n = S n` proved by `Refl` into a
module makes the ipkg typecheck exit 1 -- confirms the gate actually gates.
Corpus is axiom-clean (no believe_me / assert_total / postulate; fully total).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
# Conflicts: # .github/workflows/dogfood-proofs-ci.yml # Justfile
proofs/isabelle (5 .thy) and proofs/mizar (4 .miz) were the last self-proof corpora with no CI gate. Both toolchains are large, non-apt downloads (Isabelle ~500MB plus the HOL-Algebra image; Mizar's system + full MML from mizar.org, Tier-4 in this project), so -- per plan -- they are gated by a weekly schedule + manual dispatch rather than per-PR, mirroring container-ci.yml. Add: - .github/workflows/verification-proofs-cron.yml: isabelle + mizar jobs. Isabelle reuses live-provers.yml's proven Isabelle2024 install; Mizar discovers the newest linux tarball from mizar.org at runtime so the pin survives MML releases. - proofs/isabelle/ROOT: two sessions -- Echidna_Isabelle (base HOL: Basic, List, Nat, Propositional) and Echidna_Isabelle_Algebra (GroupTheory, on HOL-Algebra). - just proofs-isabelle (isabelle build) and just proofs-mizar (makeenv + verifier per file, failing on a non-empty .err since the verifier exit code is unreliable). Kept out of the per-PR `proofs` rollup (heavy toolchains). Verification note: isabelle.in.tum.de and mizar.org are both blocked (403 host_not_allowed) from the dev sandbox and neither tool is in apt, so these recipes cannot be run locally here. They are validated by dispatching this workflow on GitHub's runners (where live-provers.yml already downloads Isabelle successfully) and iterating on the real run output. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
workflow_dispatch can't reach a workflow that isn't yet on the default branch (404), so add a pull_request trigger path-filtered to proofs/isabelle/**, proofs/mizar/**, and this workflow file. This (a) lets the jobs run on this PR for verification, and (b) gives a confirmation run on future PRs that directly edit these proof corpora, while leaving unrelated PRs untouched -- the weekly schedule stays the primary gate. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
First dispatched run 404'd on both pinned URLs (the hosts are reachable on CI, but isabelle.in.tum.de/dist/Isabelle2024 has been superseded and the Mizar /system/i386-linux/ path is wrong). Replace both pins with index-scraping discovery + diagnostic href dumps so the install survives version drift and one run reveals the real layout if discovery still misses. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
Isabelle: the base session (Basic/List/Nat/Propositional) now passes on the
discovered Isabelle2025-2. GroupTheory used the deprecated path import
"~~/src/HOL/Algebra/Group", which isabelle build rejects ('Implicit use of
directory') because the HOL-Algebra theories already come from the parent image;
switch to the session-qualified "HOL-Algebra.Group".
Mizar: the diagnostic dump showed mizar.org/system/ links only to per-arch
directories on the upstream host (mizar.uwb.edu.pl/.../i386-linux/), with the
tarball inside. Switch to two-stage discovery (find the i386-linux dir, then the
.tar within it).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
Isabelle: the base session (Basic/List/Nat/Propositional) verifies green on the discovered Isabelle2025-2. Drop the Echidna_Isabelle_Algebra session: GroupTheory.thy is 'ML training corpus' material that does not verify (lemmas omit their assumes "group G" yet use assms; center_closed invokes group.m_comm which needs comm_group). Gating it would keep the cron permanently red -- excluded with a note in ROOT until repaired separately. Mizar: discovery + download now work (resolved mizar-8.1.15 from the upstream i386-linux dir). mizbin.tar.gz extracts binaries flat into $HOME/mizar (no bin/), so point PATH at $HOME/mizar (was $HOME/mizar/bin -> makeenv: command not found). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
Rely on the per-file .err (line col code) rather than makeenv/verifier exit codes, and print the offending source line, so a single run diagnoses all four .miz files. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
# Conflicts: # Justfile
Nat.thy and List.thy were named Nat / List, colliding with HOL's own theories
of those names (duplicate fact declarations: Nat.le_refl, List.append_assoc).
Rename them to EchidnaNat / EchidnaList. Additionally, three Nat addition lemmas
(0+n=n, n+0=n, m+n=n+m) were stated with polymorphic variables that simp cannot
discharge over a bare {zero,plus} type -- annotate them :: nat. All other proofs
are unchanged (they were already passing per the CI log). Update ROOT to the new
theory names. GroupTheory remains excluded pending a separate repair.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
Run #5 (Isabelle2025-2) reported the complete remaining failure set after the rename: EchidnaNat add_assoc, add_zero_right_inductive (induction couldn't pick a rule on a polymorphic n), mult_zero_left/right, mult_one_left/right, mult_comm -- all under-constrained over {zero,plus,times}; annotate :: nat. EchidnaList map_rev needed rev_map (HOL's simpset orients it the other way) -> by (simp add: rev_map). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
Isabelle base (per the run-#5/#279 error lists): - EchidnaNat: annotate mult_assoc, mult_distrib_left, mult_distrib_right :: nat (polymorphic over {plus,times}); rewrite factorial_monotone to derive Suc k <= Suc k * factorial k via mult_le_mono2 + factorial_positive (the old calc step's `by simp` couldn't do the multiplication-monotonicity). - EchidnaList: list_all_filter via list_all_iff + filter_id_conv (the `by (induction; auto)` left the not-P / length case open). Descope Mizar from the weekly cron: the .miz corpus has genuine, heterogeneous verification errors (propositional.miz alone: 24, the set-equality double-inclusion skeleton; basic.miz: a makeenv error) and Mizar is the project's mock-only Tier-4 tail. Drop the mizar job + proofs/mizar/** trigger; the proofs-mizar recipe stays for local use. Tracked for dedicated, locally-tested repair (see issue). Fix verif-idris permission flakiness: when apt idris2 falls back to the source build, `sudo make install` can leave ~/.idris2 root-owned, so the recipe's unprivileged `idris2 --install echidnaabi.ipkg` failed with Permission Denied. chown ~/.idris2 to the runner after install. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
Isabelle reports polymorphic-lemma failures in batches, so the incremental approach kept surfacing a new layer each round (power_*, le_*, ... after the mult_* layer). Annotate every remaining arithmetic/order/div/even lemma (power, le/less, add-mono, cancellation, div/mod, even, strong_induction) :: nat in one pass to end it; suc_* stay as-is (Suc already forces nat). Proof bodies unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
What
Final pass to make the cron's Isabelle base job green (the prior PRs fixed errors
incrementally, but Isabelle reports polymorphic-lemma failures in batches, so each round
surfaced a new layer). This annotates every remaining polymorphic lemma in
EchidnaNat:: natin one go —power_*,le_*/less_*,add_le_mono/add_less_mono, the additioncancellation laws,
div_*/mod_*,even_*, andstrong_induction_example.suc_*stayas-is (
Sucalready forces nat). All proof bodies are unchanged.After this, all four base theories (Basic, EchidnaList, EchidnaNat, Propositional) should
verify on Isabelle2025-2: every statement is now nat-typed, so the standard
by simp/by autoproofs discharge, and the earlier genuine gaps (
factorial_monotone,list_all_filter,map_rev) were already repaired in #281.Scope
Per the agreed plan ("finish Isabelle base only"): GroupTheory + Mizar remain excluded/descoped
and are tracked in #280 for dedicated, locally-tested repair. This PR is EchidnaNat-only.
Verification
Isabelle is
403-blocked in the dev sandbox, so this is verified by the cron's Isabelle job onGitHub runners (Isabelle2025-2). The comprehensive annotation preempts the batch-reveal cycle,
so it should go green rather than surfacing another layer.
🤖 Generated with Claude Code
Generated by Claude Code