Prove the tree holds a sorted set - #9
Merged
Merged
Conversation
added 2 commits
September 23, 2026 21:33
(sort xs) and (sort (distinct xs)) on integer lists are now modelled as a fold that inserts each element into the sorted list so far, checked against sort by model-check. Building the tree is the same kind of fold, so holds-a-sorted-set follows from lemmas in tree-proof: insert keeps a bst? invariant, and listing the tree after an insert is that list insert. The prover needed a few things for it: - a proof namespace may define helper defns, and its lemmas may be about clojure.core alone - a lemma hypothesis variable its conclusion doesn't bind is taken from the facts, as ACL2 does - a :vary hint lets the induction hypothesis hold at any value of an accumulator; the trace records it and the checker rebuilds it - fn parameters get canonical names, so alpha-equivalent fns are one term - float-free? covers values that only pick parts of float-free inputs, and equality drops a shared float-free prefix - a recursive definition unfolds past an and of calls once its tag is decided - a hypothesis or lemma that rewrites a term to itself is skipped before its hypothesis is read, which looped on () -> () - filter and every? walk a concatenation
The prover's logic is untyped, as ACL2's is, so a type is a hypothesis. Lemma rules, varying induction hypotheses and accumulator rules now record their variables' types, and each term a variable takes must be shown to have its type: a typed variable, an integer term for Int and Nat, or the type's recognizer rewriting to true. Recognizers are built from the spec's data the way the type's cases take values apart. A set, map or fn has none and takes only a variable of its own type. A signature is only a claim, so each signed fn's contract is proved from its code before any law, as ACL2s defunc does, and a proved contract says a call is of its return type. Nat and Int return contracts aren't proved yet.
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
1 participant
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.
The tree spec's holds-a-sorted-set law is now proved, not just tested (writ-tpr).
On integer lists, (sort xs) and (sort (distinct xs)) are modelled as a fold that inserts each element into the sorted list so far. model-check runs the model against sort itself. Building the tree is the same kind of fold, so the law follows from lemmas in test/writ/spec_demo/tree_proof.clj: insert keeps a bst? invariant, and listing the tree after an insert is that list insert.
Prover changes it needed:
andof calls once its tag is decidedLemmas are now used only at terms of their types. That gap predates this PR: lemma variables were matched against any term. The logic is untyped, as ACL2's is, so a type is treated as a hypothesis. Each term a variable takes must be a variable of that type, an integer term (for Int and Nat), or satisfy the type's recognizer, which is built from the spec's data. Signatures aren't trusted. Each signed fn's contract is proved from its code before the laws, as ACL2s defunc does. Sets, maps and fns have no recognizer and accept only a variable of their own type. Contracts for Nat and Int return types aren't proved yet; they would feed int-term? and change existing normal forms.
writ tests: 370 pass. Examples: 28 pass. Proving the contracts takes the examples run from about 16.5 to 26 minutes.