proofs(agda): reach literal zero axioms (discharge funext + Conflicts postulates)#274
Merged
Merged
Conversation
echidna's own Agda corpus had exactly two `postulate`s; both removed: - SoundnessPreservation.agda: `Conflicts` was a module-level postulate used only in `compose-sound`'s (discarded) hypothesis. Now an explicit parameter of that theorem -- strictly more general, no axiom declared. - Basic.agda (CurryUncurryLaws): dropped the `funext` postulate; the curry/uncurry inverse laws are now stated pointwise and proved by `refl` (the axiom-free plain-Agda formulation). The full function-equality form would need funext (or Cubical Agda + the cubical lib); pointwise needs neither. With this, every echidna-owned proof (Agda + Idris2 ABI + Coq/Lean/Isabelle/ Mizar dogfood) is literally axiom-free: no postulate / sorry / admit / believe_me in the tree. Type-check is confirmed by the gated dogfood Agda CI. 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.
Discharges the only two
postulates in echidna's own proof corpus, so the tree is now literally axiom-free.Changes
SoundnessPreservation.agda—Conflictswas a module-levelpostulateused only incompose-sound's hypothesis (which the proof discards). Made it an explicit parameter ofcompose-sound— strictly more general (works for any conflict predicate), no axiom declared, no burden on the other lemmas.Basic.agda(CurryUncurryLaws) — dropped thefunextpostulate. The curry/uncurry inverse laws are now stated pointwise and proved byrefl(the axiom-free plain-Agda formulation). The fullcurry (uncurry f) ≡ fform would need funext — a standard axiom, or Cubical Agda + the cubical library; pointwise needs neither, so no new CI dep.Why this form (not Cubical)
Cubical Agda would preserve the fully-extensional statement but requires adding the cubical library to the Agda CI (an addition we're avoiding) and couldn't be verified in the authoring sandbox. The pointwise statement is the honest axiom-free truth and is
refl-trivial.Verification
grepconfirms zeropostulatedeclarations acrossproofs/,meta-checker/,verification/proofs/,src/abi/,src/idris/; no danglingfunext/Conflictsrefs.just proofs-agdatype-checks both files), since I can't run Agda locally.Net: every echidna-owned proof (Agda + Idris2 ABI + Coq/Lean/Isabelle/Mizar dogfood) is now axiom-free — no postulate / sorry / admit / believe_me anywhere. Draft until the Agda job goes green.
https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
Generated by Claude Code