Move proof modules under SemVer

README.md

@@ -4,7 +4,7 @@ This library reads and writes Semantic Versioning 2.0.0 strings in Lean, and giv
 
 - The parser accepts exactly the strings of the grammar on semver.org, and nothing else.
 - It returns each part as written, and printing what it returns gives the string back.
-- `compare` follows the precedence rules of section 11, as `Spec/Defs.lean` states them.
+- `compare` follows the precedence rules of section 11, as `SemVer/Spec/Defs.lean` states them.
 - That order is consistent: swapping the sides swaps the answer, it is transitive, and two versions tie exactly when they differ in build metadata at most.
 
 So `01.0.0`, `1.0.0-01`, `v1.0.0`, `1.0` and `1.0.0 ` are rejected, `1.0.0-0a` and `1.0.0+001` are accepted, and numbers have no upper limit.
@@ -25,21 +25,21 @@ From Lean:
 
 ## What is proved
 
-The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, and the proofs in `Proofs/`.
+The statements are in `SemVer/Spec.lean`, the definitions they use in `SemVer/Spec/Defs.lean`, and the proofs in `SemVer/Proofs/`.
 
 | Claim | Theorem |
 |-------|---------|
-| `print` writes the three numbers in decimal, then the pre-release and build identifiers, each part left out when it is empty. | `Spec.print_eq` |
-| `parse` returns a version exactly when the version is well formed and the string is how it is written. So it returns the parts as written, and there is one way to write each version. | `Spec.parse_iff` |
-| `parse` accepts exactly the strings of the grammar on semver.org, as `Spec/Defs.lean` writes it out. It rejects leading zeros in numbers and in numeric pre-release identifiers, empty identifiers, characters other than ASCII letters, digits and hyphens, and anything before or after the version. | `Spec.parse_isSome_iff` |
-| What `parse` returns is well formed. | `Spec.parse_valid` |
-| Printing a well formed version and parsing the result gives it back. | `Spec.parse_print` |
-| Parsing a string and printing the result gives the string back. | `Spec.print_parse` |
-| `compare` follows section 11: major, minor and patch as numbers, then a version with a pre-release part below one without, then the pre-release identifiers from the left, numbers as numbers and below other identifiers, other identifiers in ASCII order, and a shorter list first when it runs out. | `Spec.compare_eq` |
-| Build metadata plays no part: changing it on either side changes no answer. | `Spec.compare_build` |
-| Two versions have the same precedence exactly when they differ in build metadata at most. | `Spec.compare_eq_eq_iff` |
-| Swapping the two versions swaps the answer, and precedence is transitive. So sorting by it is consistent. | `Spec.compare_swap`, `Spec.compare_trans`, `Spec.compare_lt_trans` |
-| The examples of sections 9 to 11, both ways; a selection of strings outside the grammar; and strings inside it that loose parsers get wrong. | `Spec.semver_examples`, `Spec.precedence_examples`, `Spec.reject_vectors`, `Spec.accept_vectors` |
+| `print` writes the three numbers in decimal, then the pre-release and build identifiers, each part left out when it is empty. | `SemVer.Spec.print_eq` |
+| `parse` returns a version exactly when the version is well formed and the string is how it is written. So it returns the parts as written, and there is one way to write each version. | `SemVer.Spec.parse_iff` |
+| `parse` accepts exactly the strings of the grammar on semver.org, as `SemVer/Spec/Defs.lean` writes it out. It rejects leading zeros in numbers and in numeric pre-release identifiers, empty identifiers, characters other than ASCII letters, digits and hyphens, and anything before or after the version. | `SemVer.Spec.parse_isSome_iff` |
+| What `parse` returns is well formed. | `SemVer.Spec.parse_valid` |
+| Printing a well formed version and parsing the result gives it back. | `SemVer.Spec.parse_print` |
+| Parsing a string and printing the result gives the string back. | `SemVer.Spec.print_parse` |
+| `compare` follows section 11: major, minor and patch as numbers, then a version with a pre-release part below one without, then the pre-release identifiers from the left, numbers as numbers and below other identifiers, other identifiers in ASCII order, and a shorter list first when it runs out. | `SemVer.Spec.compare_eq` |
+| Build metadata plays no part: changing it on either side changes no answer. | `SemVer.Spec.compare_build` |
+| Two versions have the same precedence exactly when they differ in build metadata at most. | `SemVer.Spec.compare_eq_eq_iff` |
+| Swapping the two versions swaps the answer, and precedence is transitive. So sorting by it is consistent. | `SemVer.Spec.compare_swap`, `SemVer.Spec.compare_trans`, `SemVer.Spec.compare_lt_trans` |
+| The examples of sections 9 to 11, both ways; a selection of strings outside the grammar; and strings inside it that loose parsers get wrong. | `SemVer.Spec.semver_examples`, `SemVer.Spec.precedence_examples`, `SemVer.Spec.reject_vectors`, `SemVer.Spec.accept_vectors` |
 
 The command-line tool in `Main.lean` answers `parse` and `compare` requests with these functions directly.
 
@@ -74,7 +74,7 @@ python3 tests/run_tests.py
 python3 tests/plant_bugs.py
 ```
 
-`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean.
+`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `SemVer/Proofs/` proves exactly the statement in `SemVer/Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean.
 
 The test script compares the tool with python-semver. It runs every string of up to eight characters over `0`, `1`, `.`, `-`, `+` and `a`, the examples of the specification, and random and mutated versions from a recorded seed, then compares pairs of versions. It then rewrites `tests/TEST-RESULTS.md`. When Python lacks python-semver 3.1.0, it installs it into `.lake/oracle-venv`, checked against the hashes in `tests/oracle-requirements.txt`.
 
@@ -84,9 +84,9 @@ The test script compares the tool with python-semver. It runs every string of up
 
 - `SemVer/Types.lean`: the `Version` and `Ident` types.
 - `SemVer/Basic.lean`: the code under proof.
-- `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file.
-- `Spec/Defs.lean`: the definitions the statements use, written from the grammar and section 11, with checks against the specification's examples.
-- `Proofs.lean` and `Proofs/`: the proofs, under the same names.
+- `SemVer/Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file.
+- `SemVer/Spec/Defs.lean`: the definitions the statements use, written from the grammar and section 11, with checks against the specification's examples.
+- `SemVer/Proofs.lean` and `SemVer/Proofs/`: the proofs, under the same names.
 - `Main.lean`: the command-line tool the tests drive.
 - `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else.
 - `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows.

SPEC.md

@@ -1,6 +1,6 @@
 # Specification: semver
 
-This library reads and writes version strings in the form Semantic Versioning 2.0.0 sets out (https://semver.org/spec/v2.0.0.html), such as `1.0.0-beta.11+exp.sha.5114f85`. It also gives the precedence of two versions, as section 11 of that specification defines it. A reviewer who did not write this specification approves it. The approval also covers `Spec.lean`, `Spec/Defs.lean`, `SemVer/Types.lean`, and the other files `bar.toml` lists.
+This library reads and writes version strings in the form Semantic Versioning 2.0.0 sets out (https://semver.org/spec/v2.0.0.html), such as `1.0.0-beta.11+exp.sha.5114f85`. It also gives the precedence of two versions, as section 11 of that specification defines it. A reviewer who did not write this specification approves it. The approval also covers `SemVer/Spec.lean`, `SemVer/Spec/Defs.lean`, `SemVer/Types.lean`, and the other files `bar.toml` lists.
 
 ## The format
 
@@ -14,7 +14,7 @@ The scope is the `<valid semver>` rule of the Backus–Naur form grammar on semv
 <version core> ::= <major> "." <minor> "." <patch>
 ```
 
-`Spec/Defs.lean` writes out each rule of the grammar. In plain words:
+`SemVer/Spec/Defs.lean` writes out each rule of the grammar. In plain words:
 
 - The major, minor and patch numbers are numeric identifiers: `0`, or ASCII digits that do not start with `0` (section 2). There is no upper limit on their size.
 - The pre-release part follows a `-`. It is one or more identifiers joined by `.`. Each is a numeric identifier, which has no leading zero, or an alphanumeric identifier. An alphanumeric identifier is ASCII letters, digits and hyphens, with at least one letter or hyphen. So `0a` and `--` are identifiers, and `01` is not (section 9).
@@ -29,7 +29,7 @@ The scope is the `<valid semver>` rule of the Backus–Naur form grammar on semv
 
 ## The value
 
-`parse` returns a `Version`: the three numbers, the list of pre-release identifiers, and the list of build identifiers. Each pre-release identifier is a number (`num`) when it is all digits, and its text (`alnum`) otherwise. Each build identifier is its text. A list is empty when its part is absent. `Spec.Valid` says which values are well formed: every `alnum` identifier is an alphanumeric identifier, and every build identifier is one or more identifier characters.
+`parse` returns a `Version`: the three numbers, the list of pre-release identifiers, and the list of build identifiers. Each pre-release identifier is a number (`num`) when it is all digits, and its text (`alnum`) otherwise. Each build identifier is its text. A list is empty when its part is absent. `SemVer.Spec.Valid` says which values are well formed: every `alnum` identifier is an alphanumeric identifier, and every build identifier is one or more identifier characters.
 
 `Version.print` writes a version: the three numbers in decimal, then `-` and the pre-release identifiers, then `+` and the build identifiers. Each list is joined by `.` and left out, with its sign, when it is empty.
 
@@ -46,7 +46,7 @@ The scope is the `<valid semver>` rule of the Backus–Naur form grammar on semv
    3. A number comes before any other identifier.
    4. When one list runs out first, all its identifiers being equal to the other's, it comes first.
 
-So two versions have the same precedence exactly when they differ in build identifiers at most. `Spec.precedence` in `Spec/Defs.lean` states these rules as written.
+So two versions have the same precedence exactly when they differ in build identifiers at most. `SemVer.Spec.precedence` in `SemVer/Spec/Defs.lean` states these rules as written.
 
 ## Errors
 
@@ -63,33 +63,33 @@ Every answer comes from `parse`, `Version.print` and `Version.compare`.
 
 ## What must always hold
 
-Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`. They are written from the specification and checked against its examples.
+Each property is a theorem in `SemVer/Spec.lean`, under the name given. The definitions the statements use are in `SemVer/Spec/Defs.lean`. They are written from the specification and checked against its examples.
 
 | Property | Theorem |
 |----------|---------|
-| `print` writes a version as `Spec.render` sets out. | `Spec.print_eq` |
-| `parse` returns `v` exactly when `v` is well formed and the string is how `v` is written. | `Spec.parse_iff` |
-| `parse` accepts exactly the strings of the grammar on semver.org. | `Spec.parse_isSome_iff` |
-| What `parse` returns is well formed. | `Spec.parse_valid` |
-| Printing then parsing gives a well formed version back. | `Spec.parse_print` |
-| Parsing then printing gives the string back. | `Spec.print_parse` |
-| `compare` gives the precedence of section 11, as `Spec.precedence` states it. | `Spec.compare_eq` |
-| Changing the build identifiers of either version changes no answer of `compare`. | `Spec.compare_build` |
-| `compare` gives `.eq` exactly when the numbers and the pre-release identifiers are the same. | `Spec.compare_eq_eq_iff` |
-| Swapping the two versions swaps the answer. | `Spec.compare_swap` |
-| Precedence is transitive, both "at most" and "lower". | `Spec.compare_trans`, `Spec.compare_lt_trans` |
-| The examples of sections 9 and 10 parse to the parts the specification reads them as. | `Spec.semver_examples` |
-| The example lists of section 11 are in rising order, every version below every later one. Two versions that differ only in build metadata have the same precedence. | `Spec.precedence_examples` |
-| Leading zeros, missing and extra parts, empty identifiers, characters outside the grammar, and text around the version are rejected. | `Spec.reject_vectors` |
-| Leading zeros in alphanumeric and build identifiers, an identifier of hyphens, and numbers past 64 bits are accepted. | `Spec.accept_vectors` |
+| `print` writes a version as `SemVer.Spec.render` sets out. | `SemVer.Spec.print_eq` |
+| `parse` returns `v` exactly when `v` is well formed and the string is how `v` is written. | `SemVer.Spec.parse_iff` |
+| `parse` accepts exactly the strings of the grammar on semver.org. | `SemVer.Spec.parse_isSome_iff` |
+| What `parse` returns is well formed. | `SemVer.Spec.parse_valid` |
+| Printing then parsing gives a well formed version back. | `SemVer.Spec.parse_print` |
+| Parsing then printing gives the string back. | `SemVer.Spec.print_parse` |
+| `compare` gives the precedence of section 11, as `SemVer.Spec.precedence` states it. | `SemVer.Spec.compare_eq` |
+| Changing the build identifiers of either version changes no answer of `compare`. | `SemVer.Spec.compare_build` |
+| `compare` gives `.eq` exactly when the numbers and the pre-release identifiers are the same. | `SemVer.Spec.compare_eq_eq_iff` |
+| Swapping the two versions swaps the answer. | `SemVer.Spec.compare_swap` |
+| Precedence is transitive, both "at most" and "lower". | `SemVer.Spec.compare_trans`, `SemVer.Spec.compare_lt_trans` |
+| The examples of sections 9 and 10 parse to the parts the specification reads them as. | `SemVer.Spec.semver_examples` |
+| The example lists of section 11 are in rising order, every version below every later one. Two versions that differ only in build metadata have the same precedence. | `SemVer.Spec.precedence_examples` |
+| Leading zeros, missing and extra parts, empty identifiers, characters outside the grammar, and text around the version are rejected. | `SemVer.Spec.reject_vectors` |
+| Leading zeros in alphanumeric and build identifiers, an identifier of hyphens, and numbers past 64 bits are accepted. | `SemVer.Spec.accept_vectors` |
 
 Together, these fix every output.
 
-- `parse` is fixed for every string by `Spec.parse_iff`.
-- `print` is fixed for every version by `Spec.print_eq`.
-- `compare` is fixed for every pair of versions by `Spec.compare_eq`.
-- A parser that accepted nothing would meet `Spec.parse_valid`, but it would fail `Spec.parse_iff`, `Spec.parse_isSome_iff` and `Spec.parse_print`.
-- A parser that accepted too much would fail `Spec.parse_iff` and `Spec.parse_isSome_iff`.
+- `parse` is fixed for every string by `SemVer.Spec.parse_iff`.
+- `print` is fixed for every version by `SemVer.Spec.print_eq`.
+- `compare` is fixed for every pair of versions by `SemVer.Spec.compare_eq`.
+- A parser that accepted nothing would meet `SemVer.Spec.parse_valid`, but it would fail `SemVer.Spec.parse_iff`, `SemVer.Spec.parse_isSome_iff` and `SemVer.Spec.parse_print`.
+- A parser that accepted too much would fail `SemVer.Spec.parse_iff` and `SemVer.Spec.parse_isSome_iff`.
 
 ## Oracle
 

SemVer/Proofs.lean

@@ -0,0 +1 @@
+import SemVer.Proofs.Main