From 1ddbd610ab575fcd24a7be7dd5d87ec837efa7af Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:51:11 -0500 Subject: [PATCH 1/2] Move proof modules and spec names under SemVer --- Proofs.lean | 1 - Proofs/Chars.lean | 66 ------------ README.md | 34 +++---- SPEC.md | 50 ++++----- SemVer/Proofs.lean | 1 + SemVer/Proofs/Chars.lean | 66 ++++++++++++ {Proofs => SemVer/Proofs}/Format.lean | 50 ++++----- {Proofs => SemVer/Proofs}/Grammar.lean | 42 ++++---- {Proofs => SemVer/Proofs}/Ident.lean | 46 ++++----- {Proofs => SemVer/Proofs}/Lists.lean | 0 {Proofs => SemVer/Proofs}/Main.lean | 68 ++++++------- {Proofs => SemVer/Proofs}/Numeric.lean | 26 ++--- {Proofs => SemVer/Proofs}/Order.lean | 30 +++--- Spec.lean => SemVer/Spec.lean | 54 +++++----- {Spec => SemVer/Spec}/Defs.lean | 136 ++++++++++++------------- SemVer/Types.lean | 4 +- bar.toml | 2 +- comparator.json | 31 ++++-- lakefile.toml | 8 +- 19 files changed, 366 insertions(+), 349 deletions(-) delete mode 100644 Proofs.lean delete mode 100644 Proofs/Chars.lean create mode 100644 SemVer/Proofs.lean create mode 100644 SemVer/Proofs/Chars.lean rename {Proofs => SemVer/Proofs}/Format.lean (74%) rename {Proofs => SemVer/Proofs}/Grammar.lean (69%) rename {Proofs => SemVer/Proofs}/Ident.lean (67%) rename {Proofs => SemVer/Proofs}/Lists.lean (100%) rename {Proofs => SemVer/Proofs}/Main.lean (64%) rename {Proofs => SemVer/Proofs}/Numeric.lean (85%) rename {Proofs => SemVer/Proofs}/Order.lean (88%) rename Spec.lean => SemVer/Spec.lean (72%) rename {Spec => SemVer/Spec}/Defs.lean (60%) diff --git a/Proofs.lean b/Proofs.lean deleted file mode 100644 index 6a6e36c..0000000 --- a/Proofs.lean +++ /dev/null @@ -1 +0,0 @@ -import Proofs.Main diff --git a/Proofs/Chars.lean b/Proofs/Chars.lean deleted file mode 100644 index bbf6623..0000000 --- a/Proofs/Chars.lean +++ /dev/null @@ -1,66 +0,0 @@ -/- - Character classes: the code's `isDigit` and `isIdentChar` against the - specification's `Spec.Digit` and `Spec.IdentChar`, and the digit - characters against their values. --/ - -import SemVer -import Spec.Defs - -open SemVer - -namespace SemVer.Proofs - -theorem le_iff_toNat {a b : Char} : a ≤ b ↔ a.toNat ≤ b.toNat := by - rw [Char.le_def, UInt32.le_iff_toNat_le]; rfl - -theorem digit_iff (c : Char) : Spec.Digit c ↔ 48 ≤ c.toNat ∧ c.toNat ≤ 57 := by - simp only [Spec.Digit, le_iff_toNat]; rfl - -theorem positiveDigit_iff (c : Char) : Spec.PositiveDigit c ↔ 49 ≤ c.toNat ∧ c.toNat ≤ 57 := by - simp only [Spec.PositiveDigit, le_iff_toNat]; rfl - -theorem letter_iff (c : Char) : - Spec.Letter c ↔ (65 ≤ c.toNat ∧ c.toNat ≤ 90) ∨ (97 ≤ c.toNat ∧ c.toNat ≤ 122) := by - simp only [Spec.Letter, le_iff_toNat]; rfl - -theorem eq_hyphen_iff (c : Char) : c = '-' ↔ c.toNat = 45 := by - rw [← Char.toNat_inj]; rfl - -theorem isDigit_iff (c : Char) : isDigit c = true ↔ Spec.Digit c := by - simp [isDigit, Spec.Digit] - -theorem isIdentChar_iff (c : Char) : isIdentChar c = true ↔ Spec.IdentChar c := by - simp only [isIdentChar, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, - isDigit_iff, Spec.IdentChar, Spec.NonDigit, Spec.Letter, or_assoc] - -theorem nonDigit_iff (c : Char) : Spec.NonDigit c ↔ Spec.IdentChar c ∧ ¬ Spec.Digit c := by - simp only [Spec.IdentChar, Spec.NonDigit, letter_iff, digit_iff, eq_hyphen_iff] - omega - -theorem positiveDigit_iff_digit (c : Char) : - Spec.PositiveDigit c ↔ Spec.Digit c ∧ c ≠ '0' := by - rw [positiveDigit_iff, digit_iff, Ne, ← Char.toNat_inj] - show _ ↔ _ ∧ ¬ c.toNat = 48 - omega - -theorem digit_identChar {c : Char} (h : Spec.Digit c) : Spec.IdentChar c := Or.inl h - -/-- A digit character is the character for its value. -/ -theorem digitChar_toNat {c : Char} (h : Spec.Digit c) : Nat.digitChar (c.toNat - 48) = c := by - rw [digit_iff] at h - rw [← Char.toNat_inj, Nat.toNat_digitChar_of_lt_ten (by omega)] - omega - -theorem digit_digitChar {n : Nat} (h : n < 10) : Spec.Digit (Nat.digitChar n) := by - rw [digit_iff, Nat.toNat_digitChar_of_lt_ten h]; omega - -/-- Characters the separators of the format use are not identifier - characters. -/ -theorem not_identChar_dot : ¬ Spec.IdentChar '.' := by decide -theorem not_identChar_plus : ¬ Spec.IdentChar '+' := by decide -theorem not_digit_hyphen : ¬ Spec.Digit '-' := by decide -theorem not_digit_dot : ¬ Spec.Digit '.' := by decide -theorem not_digit_plus : ¬ Spec.Digit '+' := by decide - -end SemVer.Proofs diff --git a/README.md b/README.md index 1cd58bc..af540d3 100644 --- a/README.md +++ b/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. diff --git a/SPEC.md b/SPEC.md index e1447c1..3bc5952 100644 --- a/SPEC.md +++ b/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 `` rule of the Backus–Naur form grammar on semv ::= "." "." ``` -`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 `` 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 `` 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 diff --git a/SemVer/Proofs.lean b/SemVer/Proofs.lean new file mode 100644 index 0000000..783f13a --- /dev/null +++ b/SemVer/Proofs.lean @@ -0,0 +1 @@ +import SemVer.Proofs.Main diff --git a/SemVer/Proofs/Chars.lean b/SemVer/Proofs/Chars.lean new file mode 100644 index 0000000..f26dee1 --- /dev/null +++ b/SemVer/Proofs/Chars.lean @@ -0,0 +1,66 @@ +/- + Character classes: the code's `isDigit` and `isIdentChar` against the + specification's `SemVer.Spec.Digit` and `SemVer.Spec.IdentChar`, and the digit + characters against their values. +-/ + +import SemVer +import SemVer.Spec.Defs + +open SemVer + +namespace SemVer.Proofs + +theorem le_iff_toNat {a b : Char} : a ≤ b ↔ a.toNat ≤ b.toNat := by + rw [Char.le_def, UInt32.le_iff_toNat_le]; rfl + +theorem digit_iff (c : Char) : SemVer.Spec.Digit c ↔ 48 ≤ c.toNat ∧ c.toNat ≤ 57 := by + simp only [SemVer.Spec.Digit, le_iff_toNat]; rfl + +theorem positiveDigit_iff (c : Char) : SemVer.Spec.PositiveDigit c ↔ 49 ≤ c.toNat ∧ c.toNat ≤ 57 := by + simp only [SemVer.Spec.PositiveDigit, le_iff_toNat]; rfl + +theorem letter_iff (c : Char) : + SemVer.Spec.Letter c ↔ (65 ≤ c.toNat ∧ c.toNat ≤ 90) ∨ (97 ≤ c.toNat ∧ c.toNat ≤ 122) := by + simp only [SemVer.Spec.Letter, le_iff_toNat]; rfl + +theorem eq_hyphen_iff (c : Char) : c = '-' ↔ c.toNat = 45 := by + rw [← Char.toNat_inj]; rfl + +theorem isDigit_iff (c : Char) : isDigit c = true ↔ SemVer.Spec.Digit c := by + simp [isDigit, SemVer.Spec.Digit] + +theorem isIdentChar_iff (c : Char) : isIdentChar c = true ↔ SemVer.Spec.IdentChar c := by + simp only [isIdentChar, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, + isDigit_iff, SemVer.Spec.IdentChar, SemVer.Spec.NonDigit, SemVer.Spec.Letter, or_assoc] + +theorem nonDigit_iff (c : Char) : SemVer.Spec.NonDigit c ↔ SemVer.Spec.IdentChar c ∧ ¬ SemVer.Spec.Digit c := by + simp only [SemVer.Spec.IdentChar, SemVer.Spec.NonDigit, letter_iff, digit_iff, eq_hyphen_iff] + omega + +theorem positiveDigit_iff_digit (c : Char) : + SemVer.Spec.PositiveDigit c ↔ SemVer.Spec.Digit c ∧ c ≠ '0' := by + rw [positiveDigit_iff, digit_iff, Ne, ← Char.toNat_inj] + show _ ↔ _ ∧ ¬ c.toNat = 48 + omega + +theorem digit_identChar {c : Char} (h : SemVer.Spec.Digit c) : SemVer.Spec.IdentChar c := Or.inl h + +/-- A digit character is the character for its value. -/ +theorem digitChar_toNat {c : Char} (h : SemVer.Spec.Digit c) : Nat.digitChar (c.toNat - 48) = c := by + rw [digit_iff] at h + rw [← Char.toNat_inj, Nat.toNat_digitChar_of_lt_ten (by omega)] + omega + +theorem digit_digitChar {n : Nat} (h : n < 10) : SemVer.Spec.Digit (Nat.digitChar n) := by + rw [digit_iff, Nat.toNat_digitChar_of_lt_ten h]; omega + +/-- Characters the separators of the format use are not identifier + characters. -/ +theorem not_identChar_dot : ¬ SemVer.Spec.IdentChar '.' := by decide +theorem not_identChar_plus : ¬ SemVer.Spec.IdentChar '+' := by decide +theorem not_digit_hyphen : ¬ SemVer.Spec.Digit '-' := by decide +theorem not_digit_dot : ¬ SemVer.Spec.Digit '.' := by decide +theorem not_digit_plus : ¬ SemVer.Spec.Digit '+' := by decide + +end SemVer.Proofs diff --git a/Proofs/Format.lean b/SemVer/Proofs/Format.lean similarity index 74% rename from Proofs/Format.lean rename to SemVer/Proofs/Format.lean index fff5292..f5e9f41 100644 --- a/Proofs/Format.lean +++ b/SemVer/Proofs/Format.lean @@ -1,10 +1,10 @@ /- - Printing and parsing: `Version.print` writes `Spec.render`, and + Printing and parsing: `Version.print` writes `SemVer.Spec.render`, and `parseChars` accepts a list of characters exactly when it is how a well formed version is written. -/ -import Proofs.Ident +import SemVer.Proofs.Ident open SemVer @@ -15,46 +15,46 @@ namespace SemVer.Proofs theorem toList_toString (n : Nat) : (toString n).toList = Nat.toDigits 10 n := by rw [Nat.toString_eq_repr, Nat.toList_repr] -theorem identPrint_toList (i : Ident) : i.print.toList = Spec.identChars i := by - cases i <;> simp [Ident.print, Spec.identChars, Spec.decimal] +theorem identPrint_toList (i : Ident) : i.print.toList = SemVer.Spec.identChars i := by + cases i <;> simp [Ident.print, SemVer.Spec.identChars, SemVer.Spec.decimal] -theorem print_toList (v : Version) : v.print.toList = Spec.render v := by - simp [Version.print, Spec.render, Spec.core, String.toList_append, Spec.decimal] +theorem print_toList (v : Version) : v.print.toList = SemVer.Spec.render v := by + simp [Version.print, SemVer.Spec.render, SemVer.Spec.core, String.toList_append, SemVer.Spec.decimal] split <;> split <;> simp [List.map_map, Function.comp_def, identPrint_toList] /-! ## The parts of a rendered version -/ /-- The pre-release identifiers as written, if there are any. -/ def prePart (pre : List Ident) : Option (List Char) := - if pre = [] then none else some (['.'].intercalate (pre.map Spec.identChars)) + if pre = [] then none else some (['.'].intercalate (pre.map SemVer.Spec.identChars)) /-- The build identifiers as written, if there are any. -/ def buildPart (build : List String) : Option (List Char) := if build = [] then none else some (['.'].intercalate (build.map String.toList)) -theorem core_eq (a b c : List Char) : Spec.core a b c = ['.'].intercalate [a, b, c] := by - simp [Spec.core, List.intercalate_cons_cons] +theorem core_eq (a b c : List Char) : SemVer.Spec.core a b c = ['.'].intercalate [a, b, c] := by + simp [SemVer.Spec.core, List.intercalate_cons_cons] theorem render_eq (v : Version) : - Spec.render v = - (Spec.core (Spec.decimal v.major) (Spec.decimal v.minor) (Spec.decimal v.patch) ++ + SemVer.Spec.render v = + (SemVer.Spec.core (SemVer.Spec.decimal v.major) (SemVer.Spec.decimal v.minor) (SemVer.Spec.decimal v.patch) ++ after '-' (prePart v.pre)) ++ after '+' (buildPart v.build) := by - simp only [Spec.render, prePart, buildPart] + simp only [SemVer.Spec.render, prePart, buildPart] split <;> split <;> simp [after] -theorem dot_not_mem_decimal (n : Nat) : '.' ∉ Spec.decimal n := not_mem_toDigits not_digit_dot n -theorem plus_not_mem_decimal (n : Nat) : '+' ∉ Spec.decimal n := +theorem dot_not_mem_decimal (n : Nat) : '.' ∉ SemVer.Spec.decimal n := not_mem_toDigits not_digit_dot n +theorem plus_not_mem_decimal (n : Nat) : '+' ∉ SemVer.Spec.decimal n := not_mem_toDigits not_digit_plus n -theorem hyphen_not_mem_decimal (n : Nat) : '-' ∉ Spec.decimal n := +theorem hyphen_not_mem_decimal (n : Nat) : '-' ∉ SemVer.Spec.decimal n := not_mem_toDigits not_digit_hyphen n theorem not_mem_core {c : Char} (hc : c ≠ '.') (a b d : Nat) - (h : ∀ n, c ∉ Spec.decimal n) : - c ∉ Spec.core (Spec.decimal a) (Spec.decimal b) (Spec.decimal d) := by - simp only [Spec.core, List.mem_append, List.mem_singleton, not_or] + (h : ∀ n, c ∉ SemVer.Spec.decimal n) : + c ∉ SemVer.Spec.core (SemVer.Spec.decimal a) (SemVer.Spec.decimal b) (SemVer.Spec.decimal d) := by + simp only [SemVer.Spec.core, List.mem_append, List.mem_singleton, not_or] exact ⟨⟨⟨⟨h a, hc⟩, h b⟩, hc⟩, h d⟩ -theorem plus_not_mem_after_pre {pre : List Ident} (h : ∀ i ∈ pre, Spec.ValidIdent i) : +theorem plus_not_mem_after_pre {pre : List Ident} (h : ∀ i ∈ pre, SemVer.Spec.ValidIdent i) : '+' ∉ after '-' (prePart pre) := by unfold prePart split @@ -70,17 +70,17 @@ theorem plus_not_mem_after_pre {pre : List Ident} (h : ∀ i ∈ pre, Spec.Valid theorem parsePre_iff {p : List Char} {xs : List Ident} : parseEach parsePreIdent (p.splitOn '.') = some xs ↔ - xs ≠ [] ∧ (∀ x ∈ xs, Spec.ValidIdent x) ∧ p = ['.'].intercalate (xs.map Spec.identChars) := + xs ≠ [] ∧ (∀ x ∈ xs, SemVer.Spec.ValidIdent x) ∧ p = ['.'].intercalate (xs.map SemVer.Spec.identChars) := parseDotted_iff (fun _ _ => parsePreIdent_eq_some) (fun _ h => dot_not_mem_identChars h) theorem parseBuild_iff {p : List Char} {xs : List String} : parseEach parseBuildIdent (p.splitOn '.') = some xs ↔ - xs ≠ [] ∧ (∀ x ∈ xs, Spec.BuildIdent x.toList) ∧ + xs ≠ [] ∧ (∀ x ∈ xs, SemVer.Spec.BuildIdent x.toList) ∧ p = ['.'].intercalate (xs.map String.toList) := parseDotted_iff (fun _ _ => parseBuildIdent_eq_some) (fun _ h => dot_not_mem_build h) theorem parsePrePart_iff {r : Option (List Char)} {xs : List Ident} : - parseDotted parsePreIdent r = some xs ↔ (∀ x ∈ xs, Spec.ValidIdent x) ∧ r = prePart xs := by + parseDotted parsePreIdent r = some xs ↔ (∀ x ∈ xs, SemVer.Spec.ValidIdent x) ∧ r = prePart xs := by cases r with | none => simp only [parseDotted, Option.some.injEq, prePart] @@ -103,7 +103,7 @@ theorem parsePrePart_iff {r : Option (List Char)} {xs : List Ident} : exact ⟨hne, hv, h⟩ theorem parseBuildPart_iff {r : Option (List Char)} {xs : List String} : - parseDotted parseBuildIdent r = some xs ↔ (∀ x ∈ xs, Spec.BuildIdent x.toList) ∧ r = buildPart xs := by + parseDotted parseBuildIdent r = some xs ↔ (∀ x ∈ xs, SemVer.Spec.BuildIdent x.toList) ∧ r = buildPart xs := by cases r with | none => simp only [parseDotted, Option.some.injEq, buildPart] @@ -141,7 +141,7 @@ theorem parseChars_eq (cs : List Char) : rfl theorem parseChars_eq_some {cs : List Char} {v : Version} : - parseChars cs = some v ↔ Spec.Valid v ∧ cs = Spec.render v := by + parseChars cs = some v ↔ SemVer.Spec.Valid v ∧ cs = SemVer.Spec.render v := by rw [parseChars_eq] generalize hb : breakAt '+' cs = rb obtain ⟨main, bp⟩ := rb @@ -180,7 +180,7 @@ theorem parseChars_eq_some {cs : List Char} {v : Version} : rw [core_eq, List.splitOn_intercalate] · rw [(parsePrePart_iff (xs := v.pre)).mpr ⟨hvp, rfl⟩, (parseBuildPart_iff (xs := v.build)).mpr ⟨hvb, rfl⟩] - simp only [Spec.decimal, parseNumeric_toDigits, Option.bind_eq_bind, Option.bind_some, + simp only [SemVer.Spec.decimal, parseNumeric_toDigits, Option.bind_eq_bind, Option.bind_some, Option.pure_def] · simp only [List.mem_cons, List.not_mem_nil, or_false, forall_eq_or_imp, forall_eq] exact ⟨dot_not_mem_decimal _, dot_not_mem_decimal _, dot_not_mem_decimal _⟩ diff --git a/Proofs/Grammar.lean b/SemVer/Proofs/Grammar.lean similarity index 69% rename from Proofs/Grammar.lean rename to SemVer/Proofs/Grammar.lean index 6c4e195..e314ea6 100644 --- a/Proofs/Grammar.lean +++ b/SemVer/Proofs/Grammar.lean @@ -3,19 +3,19 @@ it is how some well formed version is written. -/ -import Proofs.Format +import SemVer.Proofs.Format open SemVer namespace SemVer.Proofs theorem preReleaseIdent_iff {q : List Char} : - Spec.PreReleaseIdent q ↔ ∃ i, Spec.ValidIdent i ∧ q = Spec.identChars i := by + SemVer.Spec.PreReleaseIdent q ↔ ∃ i, SemVer.Spec.ValidIdent i ∧ q = SemVer.Spec.identChars i := by constructor · rintro (h | h) · refine ⟨.alnum (String.ofList q), ?_, ?_⟩ - · simpa [Spec.ValidIdent, String.toList_ofList] using h - · simp [Spec.identChars, String.toList_ofList] + · simpa [SemVer.Spec.ValidIdent, String.toList_ofList] using h + · simp [SemVer.Spec.identChars, String.toList_ofList] · obtain ⟨n, rfl⟩ := numericIdent_iff.mp h exact ⟨.num n, trivial, rfl⟩ · rintro ⟨i, hi, rfl⟩ @@ -24,7 +24,7 @@ theorem preReleaseIdent_iff {q : List Char} : | alnum s => exact Or.inl hi theorem buildIdent_iff_exists {q : List Char} : - Spec.BuildIdent q ↔ ∃ s : String, Spec.BuildIdent s.toList ∧ q = s.toList := by + SemVer.Spec.BuildIdent q ↔ ∃ s : String, SemVer.Spec.BuildIdent s.toList ∧ q = s.toList := by constructor · intro h exact ⟨String.ofList q, by rwa [String.toList_ofList], by rw [String.toList_ofList]⟩ @@ -33,7 +33,7 @@ theorem buildIdent_iff_exists {q : List Char} : theorem dotSeparated_iff {α : Type} {P : List Char → Prop} {V : α → Prop} {g : α → List Char} (hP : ∀ q, P q ↔ ∃ x, V x ∧ q = g x) {p : List Char} : - Spec.DotSeparated P p ↔ + SemVer.Spec.DotSeparated P p ↔ ∃ xs : List α, xs ≠ [] ∧ (∀ x ∈ xs, V x) ∧ p = ['.'].intercalate (xs.map g) := by constructor · rintro ⟨parts, hne, hparts, rfl⟩ @@ -47,46 +47,46 @@ theorem dotSeparated_iff {α : Type} {P : List Char → Prop} {V : α → Prop} exact (hP _).mpr ⟨x, hxs x hx, rfl⟩ theorem dotSeparated_pre_iff {p : List Char} : - Spec.DotSeparated Spec.PreReleaseIdent p ↔ - ∃ xs : List Ident, xs ≠ [] ∧ (∀ x ∈ xs, Spec.ValidIdent x) ∧ - p = ['.'].intercalate (xs.map Spec.identChars) := + SemVer.Spec.DotSeparated SemVer.Spec.PreReleaseIdent p ↔ + ∃ xs : List Ident, xs ≠ [] ∧ (∀ x ∈ xs, SemVer.Spec.ValidIdent x) ∧ + p = ['.'].intercalate (xs.map SemVer.Spec.identChars) := dotSeparated_iff (fun _ => preReleaseIdent_iff) theorem dotSeparated_build_iff {p : List Char} : - Spec.DotSeparated Spec.BuildIdent p ↔ - ∃ xs : List String, xs ≠ [] ∧ (∀ x ∈ xs, Spec.BuildIdent x.toList) ∧ + SemVer.Spec.DotSeparated SemVer.Spec.BuildIdent p ↔ + ∃ xs : List String, xs ≠ [] ∧ (∀ x ∈ xs, SemVer.Spec.BuildIdent x.toList) ∧ p = ['.'].intercalate (xs.map String.toList) := dotSeparated_iff (fun _ => buildIdent_iff_exists) theorem validSemVer_iff {cs : List Char} : - Spec.ValidSemVer cs ↔ ∃ v, Spec.Valid v ∧ cs = Spec.render v := by + SemVer.Spec.ValidSemVer cs ↔ ∃ v, SemVer.Spec.Valid v ∧ cs = SemVer.Spec.render v := by constructor · rintro ⟨ma, mi, pa, hma, hmi, hpa, h⟩ obtain ⟨a, rfl⟩ := numericIdent_iff.mp hma obtain ⟨b, rfl⟩ := numericIdent_iff.mp hmi obtain ⟨c, rfl⟩ := numericIdent_iff.mp hpa rcases h with rfl | ⟨pre, hpre, rfl⟩ | ⟨build, hbuild, rfl⟩ | ⟨pre, build, hpre, hbuild, rfl⟩ - · exact ⟨⟨a, b, c, [], []⟩, ⟨by simp, by simp⟩, by simp [Spec.render, Spec.decimal]⟩ + · exact ⟨⟨a, b, c, [], []⟩, ⟨by simp, by simp⟩, by simp [SemVer.Spec.render, SemVer.Spec.decimal]⟩ · obtain ⟨xs, hne, hxs, rfl⟩ := dotSeparated_pre_iff.mp hpre - exact ⟨⟨a, b, c, xs, []⟩, ⟨hxs, by simp⟩, by simp [Spec.render, Spec.decimal, hne]⟩ + exact ⟨⟨a, b, c, xs, []⟩, ⟨hxs, by simp⟩, by simp [SemVer.Spec.render, SemVer.Spec.decimal, hne]⟩ · obtain ⟨ys, hne, hys, rfl⟩ := dotSeparated_build_iff.mp hbuild - exact ⟨⟨a, b, c, [], ys⟩, ⟨by simp, hys⟩, by simp [Spec.render, Spec.decimal, hne]⟩ + exact ⟨⟨a, b, c, [], ys⟩, ⟨by simp, hys⟩, by simp [SemVer.Spec.render, SemVer.Spec.decimal, hne]⟩ · obtain ⟨xs, hne, hxs, rfl⟩ := dotSeparated_pre_iff.mp hpre obtain ⟨ys, hne', hys, rfl⟩ := dotSeparated_build_iff.mp hbuild - exact ⟨⟨a, b, c, xs, ys⟩, ⟨hxs, hys⟩, by simp [Spec.render, Spec.decimal, hne, hne']⟩ + exact ⟨⟨a, b, c, xs, ys⟩, ⟨hxs, hys⟩, by simp [SemVer.Spec.render, SemVer.Spec.decimal, hne, hne']⟩ · rintro ⟨⟨a, b, c, pre, build⟩, ⟨hvp, hvb⟩, rfl⟩ - refine ⟨Spec.decimal a, Spec.decimal b, Spec.decimal c, numericIdent_toDigits a, + refine ⟨SemVer.Spec.decimal a, SemVer.Spec.decimal b, SemVer.Spec.decimal c, numericIdent_toDigits a, numericIdent_toDigits b, numericIdent_toDigits c, ?_⟩ by_cases hp : pre = [] <;> by_cases hb : build = [] · subst hp hb - exact Or.inl (by simp [Spec.render]) + exact Or.inl (by simp [SemVer.Spec.render]) · subst hp exact Or.inr (Or.inr (Or.inl ⟨_, dotSeparated_build_iff.mpr ⟨build, hb, hvb, rfl⟩, - by simp [Spec.render, hb]⟩)) + by simp [SemVer.Spec.render, hb]⟩)) · subst hb exact Or.inr (Or.inl ⟨_, dotSeparated_pre_iff.mpr ⟨pre, hp, hvp, rfl⟩, - by simp [Spec.render, hp]⟩) + by simp [SemVer.Spec.render, hp]⟩) · exact Or.inr (Or.inr (Or.inr ⟨_, _, dotSeparated_pre_iff.mpr ⟨pre, hp, hvp, rfl⟩, - dotSeparated_build_iff.mpr ⟨build, hb, hvb, rfl⟩, by simp [Spec.render, hp, hb]⟩)) + dotSeparated_build_iff.mpr ⟨build, hb, hvb, rfl⟩, by simp [SemVer.Spec.render, hp, hb]⟩)) end SemVer.Proofs diff --git a/Proofs/Ident.lean b/SemVer/Proofs/Ident.lean similarity index 67% rename from Proofs/Ident.lean rename to SemVer/Proofs/Ident.lean index 5a2fabd..f15cf7a 100644 --- a/Proofs/Ident.lean +++ b/SemVer/Proofs/Ident.lean @@ -3,21 +3,21 @@ grammar's `` and ``. -/ -import Proofs.Numeric -import Proofs.Lists +import SemVer.Proofs.Numeric +import SemVer.Proofs.Lists open SemVer namespace SemVer.Proofs theorem all_isIdentChar_iff {cs : List Char} : - cs.all isIdentChar = true ↔ ∀ d ∈ cs, Spec.IdentChar d := by + cs.all isIdentChar = true ↔ ∀ d ∈ cs, SemVer.Spec.IdentChar d := by simp [List.all_eq_true, isIdentChar_iff] /-- ``: identifier characters, not all of them digits. -/ theorem alnumIdent_iff {cs : List Char} : - Spec.AlnumIdent cs ↔ (∀ d ∈ cs, Spec.IdentChar d) ∧ ¬ ∀ d ∈ cs, Spec.Digit d := by + SemVer.Spec.AlnumIdent cs ↔ (∀ d ∈ cs, SemVer.Spec.IdentChar d) ∧ ¬ ∀ d ∈ cs, SemVer.Spec.Digit d := by constructor · rintro ⟨xs, c, ys, rfl, hc, hxs, hys⟩ have hc' := (nonDigit_iff c).mp hc @@ -38,7 +38,7 @@ theorem alnumIdent_iff {cs : List Char} : /-- ``: one or more identifier characters. -/ theorem buildIdent_iff {cs : List Char} : - Spec.BuildIdent cs ↔ cs ≠ [] ∧ ∀ d ∈ cs, Spec.IdentChar d := by + SemVer.Spec.BuildIdent cs ↔ cs ≠ [] ∧ ∀ d ∈ cs, SemVer.Spec.IdentChar d := by constructor · rintro (h | ⟨hne, hd⟩) · refine ⟨?_, (alnumIdent_iff.mp h).1⟩ @@ -46,30 +46,30 @@ theorem buildIdent_iff {cs : List Char} : simp · exact ⟨hne, fun d h => digit_identChar (hd d h)⟩ · rintro ⟨hne, hi⟩ - by_cases hd : ∀ d ∈ cs, Spec.Digit d + by_cases hd : ∀ d ∈ cs, SemVer.Spec.Digit d · exact Or.inr ⟨hne, hd⟩ · exact Or.inl (alnumIdent_iff.mpr ⟨hi, hd⟩) -theorem identChar_of_validIdent {i : Ident} (h : Spec.ValidIdent i) : - ∀ d ∈ Spec.identChars i, Spec.IdentChar d := by +theorem identChar_of_validIdent {i : Ident} (h : SemVer.Spec.ValidIdent i) : + ∀ d ∈ SemVer.Spec.identChars i, SemVer.Spec.IdentChar d := by cases i with | num n => exact fun d hd => digit_identChar (digit_of_mem_toDigits hd) | alnum s => exact (alnumIdent_iff.mp h).1 theorem parsePreIdent_eq_some {cs : List Char} {i : Ident} : - parsePreIdent cs = some i ↔ Spec.ValidIdent i ∧ cs = Spec.identChars i := by + parsePreIdent cs = some i ↔ SemVer.Spec.ValidIdent i ∧ cs = SemVer.Spec.identChars i := by unfold parsePreIdent split · rename_i hd rw [all_isDigit_iff] at hd cases i with | num n => - simp only [Option.map_eq_some_iff, Ident.num.injEq, exists_eq_right, Spec.ValidIdent, - true_and, Spec.identChars, Spec.decimal] + simp only [Option.map_eq_some_iff, Ident.num.injEq, exists_eq_right, SemVer.Spec.ValidIdent, + true_and, SemVer.Spec.identChars, SemVer.Spec.decimal] exact parseNumeric_eq_some | alnum s => simp only [Option.map_eq_some_iff, reduceCtorEq, and_false, exists_false, false_iff, - not_and, Spec.ValidIdent, Spec.identChars] + not_and, SemVer.Spec.ValidIdent, SemVer.Spec.identChars] rintro h rfl exact (alnumIdent_iff.mp h).2 hd · rename_i hd @@ -79,12 +79,12 @@ theorem parsePreIdent_eq_some {cs : List Char} {i : Ident} : rw [all_isIdentChar_iff] at hi cases i with | num n => - simp only [Option.some.injEq, reduceCtorEq, Spec.ValidIdent, Spec.identChars, - Spec.decimal, true_and, false_iff] + simp only [Option.some.injEq, reduceCtorEq, SemVer.Spec.ValidIdent, SemVer.Spec.identChars, + SemVer.Spec.decimal, true_and, false_iff] rintro rfl exact hd (fun d h => digit_of_mem_toDigits h) | alnum s => - simp only [Option.some.injEq, Ident.alnum.injEq, Spec.ValidIdent, Spec.identChars] + simp only [Option.some.injEq, Ident.alnum.injEq, SemVer.Spec.ValidIdent, SemVer.Spec.identChars] constructor · rintro rfl rw [String.toList_ofList] @@ -98,7 +98,7 @@ theorem parsePreIdent_eq_some {cs : List Char} {i : Ident} : exact hi (identChar_of_validIdent hv) theorem parseBuildIdent_eq_some {cs : List Char} {s : String} : - parseBuildIdent cs = some s ↔ Spec.BuildIdent s.toList ∧ cs = s.toList := by + parseBuildIdent cs = some s ↔ SemVer.Spec.BuildIdent s.toList ∧ cs = s.toList := by unfold parseBuildIdent split · rename_i h @@ -121,23 +121,23 @@ theorem parseBuildIdent_eq_some {cs : List Char} {s : String} : /-! ## Separators inside identifiers -/ -theorem not_mem_of_identChar {c : Char} (hc : ¬ Spec.IdentChar c) {cs : List Char} - (h : ∀ d ∈ cs, Spec.IdentChar d) : c ∉ cs := +theorem not_mem_of_identChar {c : Char} (hc : ¬ SemVer.Spec.IdentChar c) {cs : List Char} + (h : ∀ d ∈ cs, SemVer.Spec.IdentChar d) : c ∉ cs := fun hm => hc (h c hm) -theorem dot_not_mem_identChars {i : Ident} (h : Spec.ValidIdent i) : '.' ∉ Spec.identChars i := +theorem dot_not_mem_identChars {i : Ident} (h : SemVer.Spec.ValidIdent i) : '.' ∉ SemVer.Spec.identChars i := not_mem_of_identChar not_identChar_dot (identChar_of_validIdent h) -theorem plus_not_mem_identChars {i : Ident} (h : Spec.ValidIdent i) : '+' ∉ Spec.identChars i := +theorem plus_not_mem_identChars {i : Ident} (h : SemVer.Spec.ValidIdent i) : '+' ∉ SemVer.Spec.identChars i := not_mem_of_identChar not_identChar_plus (identChar_of_validIdent h) -theorem dot_not_mem_build {s : String} (h : Spec.BuildIdent s.toList) : '.' ∉ s.toList := +theorem dot_not_mem_build {s : String} (h : SemVer.Spec.BuildIdent s.toList) : '.' ∉ s.toList := not_mem_of_identChar not_identChar_dot (buildIdent_iff.mp h).2 -theorem plus_not_mem_build {s : String} (h : Spec.BuildIdent s.toList) : '+' ∉ s.toList := +theorem plus_not_mem_build {s : String} (h : SemVer.Spec.BuildIdent s.toList) : '+' ∉ s.toList := not_mem_of_identChar not_identChar_plus (buildIdent_iff.mp h).2 -theorem not_mem_toDigits {c : Char} (hc : ¬ Spec.Digit c) (n : Nat) : c ∉ Nat.toDigits 10 n := +theorem not_mem_toDigits {c : Char} (hc : ¬ SemVer.Spec.Digit c) (n : Nat) : c ∉ Nat.toDigits 10 n := fun hm => hc (digit_of_mem_toDigits hm) end SemVer.Proofs diff --git a/Proofs/Lists.lean b/SemVer/Proofs/Lists.lean similarity index 100% rename from Proofs/Lists.lean rename to SemVer/Proofs/Lists.lean diff --git a/Proofs/Main.lean b/SemVer/Proofs/Main.lean similarity index 64% rename from Proofs/Main.lean rename to SemVer/Proofs/Main.lean index b3534de..0c9eea4 100644 --- a/Proofs/Main.lean +++ b/SemVer/Proofs/Main.lean @@ -1,70 +1,70 @@ /- - The statements of `Spec.lean`, under the same names, from the lemmas - in the other files of `Proofs/`. The test vectors are checked by + The statements of `SemVer/Spec.lean`, under the same names, from the lemmas + in the other files of `SemVer/Proofs/`. The test vectors are checked by evaluation in the kernel. -/ import SemVer -import Spec.Defs -import Proofs.Grammar -import Proofs.Order +import SemVer.Spec.Defs +import SemVer.Proofs.Grammar +import SemVer.Proofs.Order open SemVer open SemVer.Proofs /-! ## Printing -/ -theorem Spec.print_eq (v : Version) : v.print.toList = Spec.render v := +theorem SemVer.Spec.print_eq (v : Version) : v.print.toList = SemVer.Spec.render v := print_toList v /-! ## Parsing -/ -theorem Spec.parse_iff (s : String) (v : Version) : - parse s = some v ↔ Spec.Valid v ∧ s.toList = Spec.render v := +theorem SemVer.Spec.parse_iff (s : String) (v : Version) : + parse s = some v ↔ SemVer.Spec.Valid v ∧ s.toList = SemVer.Spec.render v := parseChars_eq_some -theorem Spec.parse_isSome_iff (s : String) : - (parse s).isSome ↔ Spec.ValidSemVer s.toList := by +theorem SemVer.Spec.parse_isSome_iff (s : String) : + (parse s).isSome ↔ SemVer.Spec.ValidSemVer s.toList := by rw [validSemVer_iff, Option.isSome_iff_exists] - exact exists_congr fun v => Spec.parse_iff s v + exact exists_congr fun v => SemVer.Spec.parse_iff s v -theorem Spec.parse_valid (s : String) (v : Version) (h : parse s = some v) : - Spec.Valid v := - ((Spec.parse_iff s v).mp h).1 +theorem SemVer.Spec.parse_valid (s : String) (v : Version) (h : parse s = some v) : + SemVer.Spec.Valid v := + ((SemVer.Spec.parse_iff s v).mp h).1 -theorem Spec.parse_print (v : Version) (h : Spec.Valid v) : parse v.print = some v := - (Spec.parse_iff _ _).mpr ⟨h, Spec.print_eq v⟩ +theorem SemVer.Spec.parse_print (v : Version) (h : SemVer.Spec.Valid v) : parse v.print = some v := + (SemVer.Spec.parse_iff _ _).mpr ⟨h, SemVer.Spec.print_eq v⟩ -theorem Spec.print_parse (s : String) (v : Version) (h : parse s = some v) : +theorem SemVer.Spec.print_parse (s : String) (v : Version) (h : parse s = some v) : v.print = s := by - obtain ⟨-, hs⟩ := (Spec.parse_iff s v).mp h + obtain ⟨-, hs⟩ := (SemVer.Spec.parse_iff s v).mp h apply String.toList_injective - rw [Spec.print_eq, hs] + rw [SemVer.Spec.print_eq, hs] /-! ## Precedence -/ -theorem Spec.compare_eq (a b : Version) : a.compare b = Spec.precedence a b := +theorem SemVer.Spec.compare_eq (a b : Version) : a.compare b = SemVer.Spec.precedence a b := versionCompare_eq a b -theorem Spec.compare_build (a b : Version) (x y : List String) : +theorem SemVer.Spec.compare_build (a b : Version) (x y : List String) : ({ a with build := x } : Version).compare { b with build := y } = a.compare b := rfl -theorem Spec.compare_eq_eq_iff (a b : Version) : +theorem SemVer.Spec.compare_eq_eq_iff (a b : Version) : a.compare b = .eq ↔ a.major = b.major ∧ a.minor = b.minor ∧ a.patch = b.patch ∧ a.pre = b.pre := by rw [compare_key, lawful_key.eq_iff] simp [key] -theorem Spec.compare_swap (a b : Version) : (a.compare b).swap = b.compare a := by +theorem SemVer.Spec.compare_swap (a b : Version) : (a.compare b).swap = b.compare a := by rw [compare_key, compare_key, lawful_key.swap] -theorem Spec.compare_trans (a b c : Version) (hab : a.compare b ≠ .gt) +theorem SemVer.Spec.compare_trans (a b c : Version) (hab : a.compare b ≠ .gt) (hbc : b.compare c ≠ .gt) : a.compare c ≠ .gt := by rw [compare_key] at hab hbc ⊢ exact lawful_key.le_trans hab hbc -theorem Spec.compare_lt_trans (a b c : Version) (hab : a.compare b = .lt) +theorem SemVer.Spec.compare_lt_trans (a b c : Version) (hab : a.compare b = .lt) (hbc : b.compare c = .lt) : a.compare c = .lt := by rw [compare_key] at hab hbc ⊢ exact lawful_key.lt_trans _ _ _ hab hbc @@ -73,7 +73,7 @@ theorem Spec.compare_lt_trans (a b c : Version) (hab : a.compare b = .lt) /-- The examples of sections 9 and 10, with the parts they are read as. -/ -theorem Spec.semver_examples : +theorem SemVer.Spec.semver_examples : parse "1.0.0-alpha" = some ⟨1, 0, 0, [.alnum "alpha"], []⟩ ∧ parse "1.0.0-alpha.1" = some ⟨1, 0, 0, [.alnum "alpha", .num 1], []⟩ ∧ parse "1.0.0-0.3.7" = some ⟨1, 0, 0, [.num 0, .num 3, .num 7], []⟩ ∧ @@ -90,21 +90,21 @@ theorem Spec.semver_examples : version in it has lower precedence than every later one. And two versions that differ only in build metadata have the same precedence (section 10). -/ -theorem Spec.precedence_examples : +theorem SemVer.Spec.precedence_examples : ["1.0.0", "2.0.0", "2.1.0", "2.1.1"].Pairwise - (fun s t => Spec.compareStrings s t = some .lt) ∧ - ["1.0.0-alpha", "1.0.0"].Pairwise (fun s t => Spec.compareStrings s t = some .lt) ∧ + (fun s t => SemVer.Spec.compareStrings s t = some .lt) ∧ + ["1.0.0-alpha", "1.0.0"].Pairwise (fun s t => SemVer.Spec.compareStrings s t = some .lt) ∧ ["1.0.0-alpha", "1.0.0-alpha.1", "1.0.0-alpha.beta", "1.0.0-beta", "1.0.0-beta.2", "1.0.0-beta.11", "1.0.0-rc.1", "1.0.0"].Pairwise - (fun s t => Spec.compareStrings s t = some .lt) ∧ - Spec.compareStrings "1.0.0-alpha+001" "1.0.0-alpha" = some .eq ∧ - Spec.compareStrings "1.0.0+20130313144700" "1.0.0+21AF26D3----117B344092BD" = some .eq := by + (fun s t => SemVer.Spec.compareStrings s t = some .lt) ∧ + SemVer.Spec.compareStrings "1.0.0-alpha+001" "1.0.0-alpha" = some .eq ∧ + SemVer.Spec.compareStrings "1.0.0+20130313144700" "1.0.0+21AF26D3----117B344092BD" = some .eq := by decide /-- Strings outside the grammar: leading zeros in numbers, missing or extra parts, empty identifiers, characters outside ASCII letters, digits and hyphens, and anything before or after the version. -/ -theorem Spec.reject_vectors : +theorem SemVer.Spec.reject_vectors : parse "01.0.0" = none ∧ parse "1.02.0" = none ∧ parse "1.0.00" = none ∧ @@ -135,7 +135,7 @@ theorem Spec.reject_vectors : pre-release identifier may have leading zeros when it is not all digits, a build identifier may have them always, and a hyphen may start an identifier. -/ -theorem Spec.accept_vectors : +theorem SemVer.Spec.accept_vectors : parse "1.0.0-0a" = some ⟨1, 0, 0, [.alnum "0a"], []⟩ ∧ parse "1.0.0-0" = some ⟨1, 0, 0, [.num 0], []⟩ ∧ parse "1.0.0+001" = some ⟨1, 0, 0, [], ["001"]⟩ ∧ diff --git a/Proofs/Numeric.lean b/SemVer/Proofs/Numeric.lean similarity index 85% rename from Proofs/Numeric.lean rename to SemVer/Proofs/Numeric.lean index 8104e89..b378474 100644 --- a/Proofs/Numeric.lean +++ b/SemVer/Proofs/Numeric.lean @@ -1,16 +1,16 @@ /- - Numbers: `Nat.toDigits 10`, which `Spec.decimal` uses, writes exactly + Numbers: `Nat.toDigits 10`, which `SemVer.Spec.decimal` uses, writes exactly the numeric identifiers of the grammar, and `parseNumeric` reads them back. -/ -import Proofs.Chars +import SemVer.Proofs.Chars open SemVer namespace SemVer.Proofs -theorem digit_of_mem_toDigits {n : Nat} {c : Char} (h : c ∈ Nat.toDigits 10 n) : Spec.Digit c := by +theorem digit_of_mem_toDigits {n : Nat} {c : Char} (h : c ∈ Nat.toDigits 10 n) : SemVer.Spec.Digit c := by have := Nat.isDigit_of_mem_toDigits (by decide) (by decide) h rw [Char.isDigit_iff_toNat] at this exact (digit_iff c).mpr this @@ -27,7 +27,7 @@ theorem toDigits_head {n : Nat} (hn : 0 < n) : exact ⟨c, rest ++ _, by rw [h]; rfl, hc⟩ theorem numericIdent_cons {c : Char} {cs : List Char} : - Spec.NumericIdent (c :: cs) ↔ (∀ d ∈ c :: cs, Spec.Digit d) ∧ (c ≠ '0' ∨ cs = []) := by + SemVer.Spec.NumericIdent (c :: cs) ↔ (∀ d ∈ c :: cs, SemVer.Spec.Digit d) ∧ (c ≠ '0' ∨ cs = []) := by constructor · rintro (h | ⟨c', rest, h, hc, hr⟩) · simp only [List.cons.injEq] at h @@ -45,17 +45,17 @@ theorem numericIdent_cons {c : Char} {cs : List Char} : · exact Or.inr ⟨c, [], rfl, (positiveDigit_iff_digit c).mpr ⟨hd c (by simp), hc⟩, by simp⟩ -theorem numericIdent_toDigits (n : Nat) : Spec.NumericIdent (Nat.toDigits 10 n) := by +theorem numericIdent_toDigits (n : Nat) : SemVer.Spec.NumericIdent (Nat.toDigits 10 n) := by rcases Nat.eq_zero_or_pos n with rfl | hn · exact Or.inl rfl · obtain ⟨c, rest, h, hc⟩ := toDigits_head hn rw [h, numericIdent_cons] exact ⟨fun d hd => digit_of_mem_toDigits (h ▸ hd), Or.inl hc⟩ -theorem numericIdent_ne_nil {cs : List Char} (h : Spec.NumericIdent cs) : cs ≠ [] := by +theorem numericIdent_ne_nil {cs : List Char} (h : SemVer.Spec.NumericIdent cs) : cs ≠ [] := by rcases h with rfl | ⟨c, rest, rfl, _, _⟩ <;> simp -theorem numericIdent_digits {cs : List Char} (h : Spec.NumericIdent cs) : ∀ d ∈ cs, Spec.Digit d := by +theorem numericIdent_digits {cs : List Char} (h : SemVer.Spec.NumericIdent cs) : ∀ d ∈ cs, SemVer.Spec.Digit d := by rcases h with rfl | ⟨c, rest, rfl, hc, hr⟩ · decide · exact List.forall_mem_cons.mpr ⟨⟨by @@ -78,8 +78,8 @@ theorem ofDigitChars_ge (cs : List Char) (init : Nat) : init ≤ Nat.ofDigitChar /-- Digits with a first digit other than `0` are how their value is written. -/ -theorem toDigits_ofDigitChars_cons {c : Char} {rest : List Char} (hc : Spec.PositiveDigit c) - (hr : ∀ d ∈ rest, Spec.Digit d) : +theorem toDigits_ofDigitChars_cons {c : Char} {rest : List Char} (hc : SemVer.Spec.PositiveDigit c) + (hr : ∀ d ∈ rest, SemVer.Spec.Digit d) : Nat.toDigits 10 (Nat.ofDigitChars 10 (c :: rest) 0) = c :: rest := by have hc' := (positiveDigit_iff c).mp hc induction rest using snoc_induction with @@ -102,17 +102,17 @@ theorem toDigits_ofDigitChars_cons {c : Char} {rest : List Char} (hc : Spec.Posi show _ ++ [Nat.digitChar (x.toNat - 48)] = _ rw [digitChar_toNat hx] -theorem toDigits_ofDigitChars {cs : List Char} (h : Spec.NumericIdent cs) : +theorem toDigits_ofDigitChars {cs : List Char} (h : SemVer.Spec.NumericIdent cs) : Nat.toDigits 10 (Nat.ofDigitChars 10 cs 0) = cs := by rcases h with rfl | ⟨c, rest, rfl, hc, hr⟩ · decide · exact toDigits_ofDigitChars_cons hc hr theorem numericIdent_iff {cs : List Char} : - Spec.NumericIdent cs ↔ ∃ n, cs = Nat.toDigits 10 n := + SemVer.Spec.NumericIdent cs ↔ ∃ n, cs = Nat.toDigits 10 n := ⟨fun h => ⟨_, (toDigits_ofDigitChars h).symm⟩, fun ⟨n, h⟩ => h ▸ numericIdent_toDigits n⟩ -theorem all_isDigit_iff {cs : List Char} : cs.all isDigit = true ↔ ∀ d ∈ cs, Spec.Digit d := by +theorem all_isDigit_iff {cs : List Char} : cs.all isDigit = true ↔ ∀ d ∈ cs, SemVer.Spec.Digit d := by simp [List.all_eq_true, isDigit_iff] theorem parseNumeric_eq_some {cs : List Char} {n : Nat} : @@ -121,7 +121,7 @@ theorem parseNumeric_eq_some {cs : List Char} {n : Nat} : | nil => simp [parseNumeric, (Nat.toDigits_ne_nil).symm] | cons c cs => have key : ((c :: cs).all isDigit && (c != '0' || cs.isEmpty)) = true ↔ - Spec.NumericIdent (c :: cs) := by + SemVer.Spec.NumericIdent (c :: cs) := by rw [numericIdent_cons, Bool.and_eq_true, all_isDigit_iff, Bool.or_eq_true, bne_iff_ne, List.isEmpty_iff] rw [parseNumeric] diff --git a/Proofs/Order.lean b/SemVer/Proofs/Order.lean similarity index 88% rename from Proofs/Order.lean rename to SemVer/Proofs/Order.lean index 7b38a1b..addcb0c 100644 --- a/Proofs/Order.lean +++ b/SemVer/Proofs/Order.lean @@ -1,11 +1,11 @@ /- - Precedence: `Version.compare` against `Spec.precedence`, and the laws + Precedence: `Version.compare` against `SemVer.Spec.precedence`, and the laws that make it an order: swapping the sides swaps the answer, it is transitive, and `.eq` means the same numbers and pre-release identifiers. -/ -import Proofs.Chars +import SemVer.Proofs.Chars open SemVer @@ -13,51 +13,51 @@ namespace SemVer.Proofs /-! ## Against the specification -/ -theorem compare_nat (a b : Nat) : compare a b = Spec.numOrder a b := by - unfold Spec.numOrder +theorem compare_nat (a b : Nat) : compare a b = SemVer.Spec.numOrder a b := by + unfold SemVer.Spec.numOrder split · exact Nat.compare_eq_lt.mpr ‹_› · split · exact Nat.compare_eq_gt.mpr ‹_› · exact Nat.compare_eq_eq.mpr (by omega) -theorem compareAscii_eq : ∀ a b : List Char, compareAscii a b = Spec.asciiOrder a b +theorem compareAscii_eq : ∀ a b : List Char, compareAscii a b = SemVer.Spec.asciiOrder a b | [], [] => rfl | [], _ :: _ => rfl | _ :: _, [] => rfl | x :: xs, y :: ys => by - simp only [compareAscii, Spec.asciiOrder, compare_nat, Spec.numOrder, compareAscii_eq xs ys] + simp only [compareAscii, SemVer.Spec.asciiOrder, compare_nat, SemVer.Spec.numOrder, compareAscii_eq xs ys] split · rfl · split · rfl · rfl -theorem identCompare_eq (a b : Ident) : a.compare b = Spec.identOrder a b := by - cases a <;> cases b <;> simp [Ident.compare, Spec.identOrder, compare_nat, compareAscii_eq] +theorem identCompare_eq (a b : Ident) : a.compare b = SemVer.Spec.identOrder a b := by + cases a <;> cases b <;> simp [Ident.compare, SemVer.Spec.identOrder, compare_nat, compareAscii_eq] -theorem compareIdents_eq : ∀ a b : List Ident, compareIdents a b = Spec.preOrder a b +theorem compareIdents_eq : ∀ a b : List Ident, compareIdents a b = SemVer.Spec.preOrder a b | [], [] => rfl | [], _ :: _ => rfl | _ :: _, [] => rfl | x :: xs, y :: ys => by - simp only [compareIdents, Spec.preOrder, identCompare_eq, compareIdents_eq xs ys] - cases Spec.identOrder x y <;> rfl + simp only [compareIdents, SemVer.Spec.preOrder, identCompare_eq, compareIdents_eq xs ys] + cases SemVer.Spec.identOrder x y <;> rfl theorem then_numOrder (a b : Nat) (r : Ordering) : - (compare a b).then r = if a ≠ b then Spec.numOrder a b else r := by + (compare a b).then r = if a ≠ b then SemVer.Spec.numOrder a b else r := by split · rename_i h have : compare a b ≠ .eq := fun e => h (Nat.compare_eq_eq.mp e) rw [compare_nat] at this ⊢ revert this - cases Spec.numOrder a b <;> simp + cases SemVer.Spec.numOrder a b <;> simp · rename_i h rw [Nat.compare_eq_eq.mpr (Classical.not_not.mp h)] rfl -theorem versionCompare_eq (a b : Version) : a.compare b = Spec.precedence a b := by - simp only [Version.compare, Spec.precedence, then_numOrder] +theorem versionCompare_eq (a b : Version) : a.compare b = SemVer.Spec.precedence a b := by + simp only [Version.compare, SemVer.Spec.precedence, then_numOrder] split · rfl · split diff --git a/Spec.lean b/SemVer/Spec.lean similarity index 72% rename from Spec.lean rename to SemVer/Spec.lean index 4bea671..b68c501 100644 --- a/Spec.lean +++ b/SemVer/Spec.lean @@ -2,7 +2,7 @@ The specification as Lean statements: the challenge file. A reviewer who did not write this file approves it, and `bar.toml` - records the hash it had then. The proofs live in `Proofs.lean`, under + records the hash it had then. The proofs live in `SemVer/Proofs.lean`, under the same names; `lake comparator` checks that each one proves exactly the statement written here. The `sorry`s below are expected in this file only. @@ -13,16 +13,16 @@ -/ import SemVer -import Spec.Defs +import SemVer.Spec.Defs open SemVer /-! ## Printing -/ -/-- `print` writes a version as `Spec.render` sets out: the numbers in +/-- `print` writes a version as `SemVer.Spec.render` sets out: the numbers in decimal, then the pre-release and build parts, each left out when empty. -/ -theorem Spec.print_eq (v : Version) : v.print.toList = Spec.render v := sorry +theorem SemVer.Spec.print_eq (v : Version) : v.print.toList = SemVer.Spec.render v := sorry /-! ## Parsing -/ @@ -30,58 +30,58 @@ theorem Spec.print_eq (v : Version) : v.print.toList = Spec.render v := sorry is how `v` is written. So it returns the parts as written, accepts no other spelling of them, and rejects every string that is not how some well formed version is written. -/ -theorem Spec.parse_iff (s : String) (v : Version) : - parse s = some v ↔ Spec.Valid v ∧ s.toList = Spec.render v := sorry +theorem SemVer.Spec.parse_iff (s : String) (v : Version) : + parse s = some v ↔ SemVer.Spec.Valid v ∧ s.toList = SemVer.Spec.render v := sorry /-- `parse` accepts exactly the strings of the grammar on semver.org. -/ -theorem Spec.parse_isSome_iff (s : String) : - (parse s).isSome ↔ Spec.ValidSemVer s.toList := sorry +theorem SemVer.Spec.parse_isSome_iff (s : String) : + (parse s).isSome ↔ SemVer.Spec.ValidSemVer s.toList := sorry /-- What `parse` returns is well formed. -/ -theorem Spec.parse_valid (s : String) (v : Version) (h : parse s = some v) : - Spec.Valid v := sorry +theorem SemVer.Spec.parse_valid (s : String) (v : Version) (h : parse s = some v) : + SemVer.Spec.Valid v := sorry /-- Round trip: printing a well formed version and parsing the result gives it back. -/ -theorem Spec.parse_print (v : Version) (h : Spec.Valid v) : parse v.print = some v := sorry +theorem SemVer.Spec.parse_print (v : Version) (h : SemVer.Spec.Valid v) : parse v.print = some v := sorry /-- Round trip: parsing a string and printing the result gives the string back. -/ -theorem Spec.print_parse (s : String) (v : Version) (h : parse s = some v) : +theorem SemVer.Spec.print_parse (s : String) (v : Version) (h : parse s = some v) : v.print = s := sorry /-! ## Precedence -/ /-- `compare` gives the precedence of section 11. -/ -theorem Spec.compare_eq (a b : Version) : a.compare b = Spec.precedence a b := sorry +theorem SemVer.Spec.compare_eq (a b : Version) : a.compare b = SemVer.Spec.precedence a b := sorry /-- Build identifiers play no part in precedence (11.1): changing them on either side changes nothing. -/ -theorem Spec.compare_build (a b : Version) (x y : List String) : +theorem SemVer.Spec.compare_build (a b : Version) (x y : List String) : ({ a with build := x } : Version).compare { b with build := y } = a.compare b := sorry /-- Two versions have the same precedence exactly when they differ in build identifiers at most. -/ -theorem Spec.compare_eq_eq_iff (a b : Version) : +theorem SemVer.Spec.compare_eq_eq_iff (a b : Version) : a.compare b = .eq ↔ a.major = b.major ∧ a.minor = b.minor ∧ a.patch = b.patch ∧ a.pre = b.pre := sorry /-- Swapping the two sides swaps the answer. -/ -theorem Spec.compare_swap (a b : Version) : (a.compare b).swap = b.compare a := sorry +theorem SemVer.Spec.compare_swap (a b : Version) : (a.compare b).swap = b.compare a := sorry /-- Precedence is transitive, so sorting by it is consistent. -/ -theorem Spec.compare_trans (a b c : Version) (hab : a.compare b ≠ .gt) +theorem SemVer.Spec.compare_trans (a b c : Version) (hab : a.compare b ≠ .gt) (hbc : b.compare c ≠ .gt) : a.compare c ≠ .gt := sorry /-- Strict precedence is transitive too. -/ -theorem Spec.compare_lt_trans (a b c : Version) (hab : a.compare b = .lt) +theorem SemVer.Spec.compare_lt_trans (a b c : Version) (hab : a.compare b = .lt) (hbc : b.compare c = .lt) : a.compare c = .lt := sorry /-! ## Test vectors -/ /-- The examples of sections 9 and 10, with the parts they are read as. -/ -theorem Spec.semver_examples : +theorem SemVer.Spec.semver_examples : parse "1.0.0-alpha" = some ⟨1, 0, 0, [.alnum "alpha"], []⟩ ∧ parse "1.0.0-alpha.1" = some ⟨1, 0, 0, [.alnum "alpha", .num 1], []⟩ ∧ parse "1.0.0-0.3.7" = some ⟨1, 0, 0, [.num 0, .num 3, .num 7], []⟩ ∧ @@ -98,21 +98,21 @@ theorem Spec.semver_examples : version in it has lower precedence than every later one. And two versions that differ only in build metadata have the same precedence (section 10). -/ -theorem Spec.precedence_examples : +theorem SemVer.Spec.precedence_examples : ["1.0.0", "2.0.0", "2.1.0", "2.1.1"].Pairwise - (fun s t => Spec.compareStrings s t = some .lt) ∧ - ["1.0.0-alpha", "1.0.0"].Pairwise (fun s t => Spec.compareStrings s t = some .lt) ∧ + (fun s t => SemVer.Spec.compareStrings s t = some .lt) ∧ + ["1.0.0-alpha", "1.0.0"].Pairwise (fun s t => SemVer.Spec.compareStrings s t = some .lt) ∧ ["1.0.0-alpha", "1.0.0-alpha.1", "1.0.0-alpha.beta", "1.0.0-beta", "1.0.0-beta.2", "1.0.0-beta.11", "1.0.0-rc.1", "1.0.0"].Pairwise - (fun s t => Spec.compareStrings s t = some .lt) ∧ - Spec.compareStrings "1.0.0-alpha+001" "1.0.0-alpha" = some .eq ∧ - Spec.compareStrings "1.0.0+20130313144700" "1.0.0+21AF26D3----117B344092BD" = some .eq := + (fun s t => SemVer.Spec.compareStrings s t = some .lt) ∧ + SemVer.Spec.compareStrings "1.0.0-alpha+001" "1.0.0-alpha" = some .eq ∧ + SemVer.Spec.compareStrings "1.0.0+20130313144700" "1.0.0+21AF26D3----117B344092BD" = some .eq := sorry /-- Strings outside the grammar: leading zeros in numbers, missing or extra parts, empty identifiers, characters outside ASCII letters, digits and hyphens, and anything before or after the version. -/ -theorem Spec.reject_vectors : +theorem SemVer.Spec.reject_vectors : parse "01.0.0" = none ∧ parse "1.02.0" = none ∧ parse "1.0.00" = none ∧ @@ -143,7 +143,7 @@ theorem Spec.reject_vectors : pre-release identifier may have leading zeros when it is not all digits, a build identifier may have them always, and a hyphen may start an identifier. -/ -theorem Spec.accept_vectors : +theorem SemVer.Spec.accept_vectors : parse "1.0.0-0a" = some ⟨1, 0, 0, [.alnum "0a"], []⟩ ∧ parse "1.0.0-0" = some ⟨1, 0, 0, [.num 0], []⟩ ∧ parse "1.0.0+001" = some ⟨1, 0, 0, [], ["001"]⟩ ∧ diff --git a/Spec/Defs.lean b/SemVer/Spec/Defs.lean similarity index 60% rename from Spec/Defs.lean rename to SemVer/Spec/Defs.lean index e2056e2..8ff7f30 100644 --- a/Spec/Defs.lean +++ b/SemVer/Spec/Defs.lean @@ -2,7 +2,7 @@ The definitions the specification uses, written from Semantic Versioning 2.0.0 (https://semver.org/spec/v2.0.0.html) independently of the code in `SemVer/`. Part of the approved specification, with - `Spec.lean` and `SemVer/Types.lean`. + `SemVer/Spec.lean` and `SemVer/Types.lean`. Both the challenge file and the proofs import this file, so each statement means the same thing on both sides. The `example`s check @@ -28,28 +28,28 @@ From the Backus–Naur form grammar on semver.org: -/ /-- ``. -/ -abbrev Spec.Digit (c : Char) : Prop := '0' ≤ c ∧ c ≤ '9' +abbrev SemVer.Spec.Digit (c : Char) : Prop := '0' ≤ c ∧ c ≤ '9' /-- ``. -/ -abbrev Spec.PositiveDigit (c : Char) : Prop := '1' ≤ c ∧ c ≤ '9' +abbrev SemVer.Spec.PositiveDigit (c : Char) : Prop := '1' ≤ c ∧ c ≤ '9' /-- ``: ASCII letters only. -/ -abbrev Spec.Letter (c : Char) : Prop := ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') +abbrev SemVer.Spec.Letter (c : Char) : Prop := ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') /-- ``. -/ -abbrev Spec.NonDigit (c : Char) : Prop := Spec.Letter c ∨ c = '-' +abbrev SemVer.Spec.NonDigit (c : Char) : Prop := SemVer.Spec.Letter c ∨ c = '-' /-- ``. -/ -abbrev Spec.IdentChar (c : Char) : Prop := Spec.Digit c ∨ Spec.NonDigit c +abbrev SemVer.Spec.IdentChar (c : Char) : Prop := SemVer.Spec.Digit c ∨ SemVer.Spec.NonDigit c -example : "0123456789".toList.all (fun c => decide (Spec.Digit c)) := by decide -example : "123456789".toList.all (fun c => decide (Spec.PositiveDigit c)) := by decide -example : ¬ Spec.PositiveDigit '0' := by decide +example : "0123456789".toList.all (fun c => decide (SemVer.Spec.Digit c)) := by decide +example : "123456789".toList.all (fun c => decide (SemVer.Spec.PositiveDigit c)) := by decide +example : ¬ SemVer.Spec.PositiveDigit '0' := by decide example : ("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz-".toList.all fun c => - decide (Spec.NonDigit c)) := by decide + decide (SemVer.Spec.NonDigit c)) := by decide -- The neighbours of each range, and characters people mistake for -- them, are not identifier characters. -example : ("/:@[`{.+_ \n٣０éα".toList.all fun c => !decide (Spec.IdentChar c)) := by decide +example : ("/:@[`{.+_ \n٣０éα".toList.all fun c => !decide (SemVer.Spec.IdentChar c)) := by decide /-! ## The grammar @@ -84,92 +84,92 @@ Each rule below is one of these, over lists of characters. -/ /-- ``: one or more digits. -/ -def Spec.Digits (cs : List Char) : Prop := cs ≠ [] ∧ ∀ c ∈ cs, Spec.Digit c +def SemVer.Spec.Digits (cs : List Char) : Prop := cs ≠ [] ∧ ∀ c ∈ cs, SemVer.Spec.Digit c /-- ``: `0`, or a positive digit followed by any number of digits. So no leading zero. -/ -def Spec.NumericIdent (cs : List Char) : Prop := - cs = ['0'] ∨ ∃ c rest, cs = c :: rest ∧ Spec.PositiveDigit c ∧ ∀ d ∈ rest, Spec.Digit d +def SemVer.Spec.NumericIdent (cs : List Char) : Prop := + cs = ['0'] ∨ ∃ c rest, cs = c :: rest ∧ SemVer.Spec.PositiveDigit c ∧ ∀ d ∈ rest, SemVer.Spec.Digit d /-- ``: the four forms of the rule together are a non-digit with any identifier characters, possibly none, before and after it. -/ -def Spec.AlnumIdent (cs : List Char) : Prop := - ∃ xs c ys, cs = xs ++ c :: ys ∧ Spec.NonDigit c ∧ - (∀ d ∈ xs, Spec.IdentChar d) ∧ ∀ d ∈ ys, Spec.IdentChar d +def SemVer.Spec.AlnumIdent (cs : List Char) : Prop := + ∃ xs c ys, cs = xs ++ c :: ys ∧ SemVer.Spec.NonDigit c ∧ + (∀ d ∈ xs, SemVer.Spec.IdentChar d) ∧ ∀ d ∈ ys, SemVer.Spec.IdentChar d /-- ``. -/ -def Spec.PreReleaseIdent (cs : List Char) : Prop := - Spec.AlnumIdent cs ∨ Spec.NumericIdent cs +def SemVer.Spec.PreReleaseIdent (cs : List Char) : Prop := + SemVer.Spec.AlnumIdent cs ∨ SemVer.Spec.NumericIdent cs /-- ``. -/ -def Spec.BuildIdent (cs : List Char) : Prop := - Spec.AlnumIdent cs ∨ Spec.Digits cs +def SemVer.Spec.BuildIdent (cs : List Char) : Prop := + SemVer.Spec.AlnumIdent cs ∨ SemVer.Spec.Digits cs /-- ``: one or more parts, each of them meeting `P`, with `.` between each two. -/ -def Spec.DotSeparated (P : List Char → Prop) (cs : List Char) : Prop := +def SemVer.Spec.DotSeparated (P : List Char → Prop) (cs : List Char) : Prop := ∃ parts, parts ≠ [] ∧ (∀ p ∈ parts, P p) ∧ cs = ['.'].intercalate parts /-- ``, from its three parts. -/ -def Spec.core (major minor patch : List Char) : List Char := +def SemVer.Spec.core (major minor patch : List Char) : List Char := major ++ ['.'] ++ minor ++ ['.'] ++ patch /-- ``: the four forms of the rule. -/ -def Spec.ValidSemVer (cs : List Char) : Prop := +def SemVer.Spec.ValidSemVer (cs : List Char) : Prop := ∃ major minor patch, - Spec.NumericIdent major ∧ Spec.NumericIdent minor ∧ Spec.NumericIdent patch ∧ - (cs = Spec.core major minor patch ∨ - (∃ pre, Spec.DotSeparated Spec.PreReleaseIdent pre ∧ - cs = Spec.core major minor patch ++ ['-'] ++ pre) ∨ - (∃ build, Spec.DotSeparated Spec.BuildIdent build ∧ - cs = Spec.core major minor patch ++ ['+'] ++ build) ∨ - (∃ pre build, Spec.DotSeparated Spec.PreReleaseIdent pre ∧ - Spec.DotSeparated Spec.BuildIdent build ∧ - cs = Spec.core major minor patch ++ ['-'] ++ pre ++ ['+'] ++ build)) + SemVer.Spec.NumericIdent major ∧ SemVer.Spec.NumericIdent minor ∧ SemVer.Spec.NumericIdent patch ∧ + (cs = SemVer.Spec.core major minor patch ∨ + (∃ pre, SemVer.Spec.DotSeparated SemVer.Spec.PreReleaseIdent pre ∧ + cs = SemVer.Spec.core major minor patch ++ ['-'] ++ pre) ∨ + (∃ build, SemVer.Spec.DotSeparated SemVer.Spec.BuildIdent build ∧ + cs = SemVer.Spec.core major minor patch ++ ['+'] ++ build) ∨ + (∃ pre build, SemVer.Spec.DotSeparated SemVer.Spec.PreReleaseIdent pre ∧ + SemVer.Spec.DotSeparated SemVer.Spec.BuildIdent build ∧ + cs = SemVer.Spec.core major minor patch ++ ['-'] ++ pre ++ ['+'] ++ build)) /-! ## Values -/ /-- A natural number in decimal, as Lean's `Nat.repr` writes it: no leading zero, and `0` for zero. -/ -def Spec.decimal (n : Nat) : List Char := Nat.toDigits 10 n +def SemVer.Spec.decimal (n : Nat) : List Char := Nat.toDigits 10 n -example : Spec.decimal 0 = ['0'] := by decide -example : Spec.decimal 7 = ['7'] := by decide -example : Spec.decimal 1985 = "1985".toList := by decide +example : SemVer.Spec.decimal 0 = ['0'] := by decide +example : SemVer.Spec.decimal 7 = ['7'] := by decide +example : SemVer.Spec.decimal 1985 = "1985".toList := by decide /-- A pre-release identifier as written. -/ -def Spec.identChars : Ident → List Char - | .num n => Spec.decimal n +def SemVer.Spec.identChars : Ident → List Char + | .num n => SemVer.Spec.decimal n | .alnum s => s.toList /-- The string a version stands for: the three numbers, the pre-release identifiers after `-` and the build identifiers after `+`, each list joined by `.` and left out with its sign when it is empty. -/ -def Spec.render (v : Version) : List Char := - Spec.core (Spec.decimal v.major) (Spec.decimal v.minor) (Spec.decimal v.patch) ++ - (if v.pre = [] then [] else ['-'] ++ ['.'].intercalate (v.pre.map Spec.identChars)) ++ +def SemVer.Spec.render (v : Version) : List Char := + SemVer.Spec.core (SemVer.Spec.decimal v.major) (SemVer.Spec.decimal v.minor) (SemVer.Spec.decimal v.patch) ++ + (if v.pre = [] then [] else ['-'] ++ ['.'].intercalate (v.pre.map SemVer.Spec.identChars)) ++ (if v.build = [] then [] else ['+'] ++ ['.'].intercalate (v.build.map String.toList)) -example : Spec.render ⟨1, 0, 0, [.alnum "alpha", .num 1], []⟩ = "1.0.0-alpha.1".toList := by +example : SemVer.Spec.render ⟨1, 0, 0, [.alnum "alpha", .num 1], []⟩ = "1.0.0-alpha.1".toList := by decide -example : Spec.render ⟨1, 0, 0, [.alnum "beta"], ["exp", "sha", "5114f85"]⟩ = +example : SemVer.Spec.render ⟨1, 0, 0, [.alnum "beta"], ["exp", "sha", "5114f85"]⟩ = "1.0.0-beta+exp.sha.5114f85".toList := by decide -example : Spec.render ⟨1, 0, 0, [], ["20130313144700"]⟩ = "1.0.0+20130313144700".toList := by +example : SemVer.Spec.render ⟨1, 0, 0, [], ["20130313144700"]⟩ = "1.0.0+20130313144700".toList := by decide /-- A pre-release identifier is well formed when, as a number, it is any natural number, and otherwise when it is an alphanumeric identifier. An `alnum` of digits only is not well formed: those digits are a numeric identifier. -/ -def Spec.ValidIdent : Ident → Prop +def SemVer.Spec.ValidIdent : Ident → Prop | .num _ => True - | .alnum s => Spec.AlnumIdent s.toList + | .alnum s => SemVer.Spec.AlnumIdent s.toList /-- A version is well formed when each of its identifiers is. The three numbers may be any natural numbers: SemVer sets no upper limit. -/ -def Spec.Valid (v : Version) : Prop := - (∀ i ∈ v.pre, Spec.ValidIdent i) ∧ ∀ b ∈ v.build, Spec.BuildIdent b.toList +def SemVer.Spec.Valid (v : Version) : Prop := + (∀ i ∈ v.pre, SemVer.Spec.ValidIdent i) ∧ ∀ b ∈ v.build, SemVer.Spec.BuildIdent b.toList /-! ## Precedence: section 11 @@ -197,40 +197,40 @@ def Spec.Valid (v : Version) : Prop := -/ /-- Two numbers, compared numerically (11.2 and 11.4.1). -/ -def Spec.numOrder (a b : Nat) : Ordering := +def SemVer.Spec.numOrder (a b : Nat) : Ordering := if a < b then .lt else if b < a then .gt else .eq /-- ASCII sort order (11.4.2): by the code of the first character that differs; when one string runs out first, it comes first. -/ -def Spec.asciiOrder : List Char → List Char → Ordering +def SemVer.Spec.asciiOrder : List Char → List Char → Ordering | [], [] => .eq | [], _ :: _ => .lt | _ :: _, [] => .gt | a :: as, b :: bs => - if a.toNat < b.toNat then .lt else if b.toNat < a.toNat then .gt else Spec.asciiOrder as bs + if a.toNat < b.toNat then .lt else if b.toNat < a.toNat then .gt else SemVer.Spec.asciiOrder as bs -example : Spec.asciiOrder "alpha".toList "beta".toList = .lt := by decide -example : Spec.asciiOrder "Z".toList "a".toList = .lt := by decide -example : Spec.asciiOrder "-".toList "0a".toList = .lt := by decide -example : Spec.asciiOrder "rc".toList "rc1".toList = .lt := by decide +example : SemVer.Spec.asciiOrder "alpha".toList "beta".toList = .lt := by decide +example : SemVer.Spec.asciiOrder "Z".toList "a".toList = .lt := by decide +example : SemVer.Spec.asciiOrder "-".toList "0a".toList = .lt := by decide +example : SemVer.Spec.asciiOrder "rc".toList "rc1".toList = .lt := by decide /-- Two pre-release identifiers: 11.4.1 to 11.4.3. -/ -def Spec.identOrder : Ident → Ident → Ordering - | .num a, .num b => Spec.numOrder a b - | .alnum a, .alnum b => Spec.asciiOrder a.toList b.toList +def SemVer.Spec.identOrder : Ident → Ident → Ordering + | .num a, .num b => SemVer.Spec.numOrder a b + | .alnum a, .alnum b => SemVer.Spec.asciiOrder a.toList b.toList | .num _, .alnum _ => .lt | .alnum _, .num _ => .gt /-- Two lists of pre-release identifiers, from left to right until a difference is found (11.4); when one list runs out first, all of its identifiers being equal to the other's, it comes first (11.4.4). -/ -def Spec.preOrder : List Ident → List Ident → Ordering +def SemVer.Spec.preOrder : List Ident → List Ident → Ordering | [], [] => .eq | [], _ :: _ => .lt | _ :: _, [] => .gt | a :: as, b :: bs => - match Spec.identOrder a b with - | .eq => Spec.preOrder as bs + match SemVer.Spec.identOrder a b with + | .eq => SemVer.Spec.preOrder as bs | o => o /-- The precedence of `a` against `b`: `.lt` when `a` has lower @@ -238,19 +238,19 @@ def Spec.preOrder : List Ident → List Ident → Ordering without a pre-release part above one with it (11.3), then the pre-release identifiers (11.4). Build identifiers are not read (11.1). -/ -def Spec.precedence (a b : Version) : Ordering := - if a.major ≠ b.major then Spec.numOrder a.major b.major - else if a.minor ≠ b.minor then Spec.numOrder a.minor b.minor - else if a.patch ≠ b.patch then Spec.numOrder a.patch b.patch +def SemVer.Spec.precedence (a b : Version) : Ordering := + if a.major ≠ b.major then SemVer.Spec.numOrder a.major b.major + else if a.minor ≠ b.minor then SemVer.Spec.numOrder a.minor b.minor + else if a.patch ≠ b.patch then SemVer.Spec.numOrder a.patch b.patch else if a.pre = [] ∧ b.pre = [] then .eq else if a.pre = [] then .gt else if b.pre = [] then .lt - else Spec.preOrder a.pre b.pre + else SemVer.Spec.preOrder a.pre b.pre /-! ## Helpers for the test vectors -/ /-- The precedence of two strings, when both parse. -/ -def Spec.compareStrings (s t : String) : Option Ordering := do +def SemVer.Spec.compareStrings (s t : String) : Option Ordering := do let a ← parse s let b ← parse t pure (a.compare b) diff --git a/SemVer/Types.lean b/SemVer/Types.lean index dc370cd..0c2095d 100644 --- a/SemVer/Types.lean +++ b/SemVer/Types.lean @@ -1,10 +1,10 @@ /- What a version is: the values the parser produces and the printer - takes. Part of the approved specification, with `Spec.lean` and + takes. Part of the approved specification, with `SemVer/Spec.lean` and `Spec/Defs.lean`, since every statement is about these types. A value holds each part of a Semantic Versioning 2.0.0 string as - written. Which values are valid is `Spec.Valid`, in `Spec/Defs.lean`. + written. Which values are valid is `SemVer.Spec.Valid`, in `Spec/Defs.lean`. -/ namespace SemVer diff --git a/bar.toml b/bar.toml index 6aeb37f..7e8ba89 100644 --- a/bar.toml +++ b/bar.toml @@ -16,7 +16,7 @@ entry_points = ["Main.lean"] [spec] # SemVer/Types.lean holds the types every statement is about, so it is # part of the specification. -files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "SemVer/Types.lean"] +files = ["SPEC.md", "SemVer/Spec.lean", "SemVer/Spec/Defs.lean", "SemVer/Types.lean"] # The code under proof: the functions the statements are about. code = ["SemVer.parse", "SemVer.Version.print", "SemVer.Version.compare"] diff --git a/comparator.json b/comparator.json index b2c2048..a472830 100644 --- a/comparator.json +++ b/comparator.json @@ -1,12 +1,27 @@ { - "challenge_module": "Spec", - "solution_module": "Proofs", + "challenge_module": "SemVer.Spec", + "solution_module": "SemVer.Proofs", "theorem_names": [ - "Spec.print_eq", "Spec.parse_iff", "Spec.parse_isSome_iff", "Spec.parse_valid", - "Spec.parse_print", "Spec.print_parse", "Spec.compare_eq", "Spec.compare_build", - "Spec.compare_eq_eq_iff", "Spec.compare_swap", "Spec.compare_trans", "Spec.compare_lt_trans", - "Spec.semver_examples", "Spec.precedence_examples", "Spec.reject_vectors", - "Spec.accept_vectors" + "SemVer.Spec.print_eq", + "SemVer.Spec.parse_iff", + "SemVer.Spec.parse_isSome_iff", + "SemVer.Spec.parse_valid", + "SemVer.Spec.parse_print", + "SemVer.Spec.print_parse", + "SemVer.Spec.compare_eq", + "SemVer.Spec.compare_build", + "SemVer.Spec.compare_eq_eq_iff", + "SemVer.Spec.compare_swap", + "SemVer.Spec.compare_trans", + "SemVer.Spec.compare_lt_trans", + "SemVer.Spec.semver_examples", + "SemVer.Spec.precedence_examples", + "SemVer.Spec.reject_vectors", + "SemVer.Spec.accept_vectors" ], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"] + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ] } diff --git a/lakefile.toml b/lakefile.toml index b76f737..6f12e88 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,16 +1,18 @@ name = "semver" version = "0.1.0" license = "Apache-2.0" -defaultTargets = ["SemVer", "Spec", "Proofs", "semver"] +defaultTargets = ["SemVer", "SemVerSpec", "SemVerProofs", "semver"] [[lean_lib]] name = "SemVer" [[lean_lib]] -name = "Spec" +name = "SemVerSpec" +roots = ["SemVer.Spec"] [[lean_lib]] -name = "Proofs" +name = "SemVerProofs" +roots = ["SemVer.Proofs"] [[lean_exe]] name = "semver" From 82a8b31b68db342d920b5dd99bdbb1fc649aa55d Mon Sep 17 00:00:00 2001 From: orda-aska Date: Thu, 29 Oct 2026 20:01:14 +0000 Subject: [PATCH 2/2] Point the remaining Spec/Defs.lean references at SemVer/Spec/Defs.lean Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf --- SemVer/Spec.lean | 2 +- SemVer/Types.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/SemVer/Spec.lean b/SemVer/Spec.lean index b68c501..bc31167 100644 --- a/SemVer/Spec.lean +++ b/SemVer/Spec.lean @@ -8,7 +8,7 @@ file only. The definitions the statements use, written from Semantic Versioning - 2.0.0, are in `Spec/Defs.lean`, and the types in `SemVer/Types.lean`. + 2.0.0, are in `SemVer/Spec/Defs.lean`, and the types in `SemVer/Types.lean`. Both are part of the specification too. -/ diff --git a/SemVer/Types.lean b/SemVer/Types.lean index 0c2095d..2e9cd8b 100644 --- a/SemVer/Types.lean +++ b/SemVer/Types.lean @@ -1,10 +1,10 @@ /- What a version is: the values the parser produces and the printer takes. Part of the approved specification, with `SemVer/Spec.lean` and - `Spec/Defs.lean`, since every statement is about these types. + `SemVer/Spec/Defs.lean`, since every statement is about these types. A value holds each part of a Semantic Versioning 2.0.0 string as - written. Which values are valid is `SemVer.Spec.Valid`, in `Spec/Defs.lean`. + written. Which values are valid is `SemVer.Spec.Valid`, in `SemVer/Spec/Defs.lean`. -/ namespace SemVer