From e0668683fdb17be5fe415ce63747b7e06b247ece Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 03:15:14 +0000 Subject: [PATCH] applied: Rocq and Lean re-proofs of APP-1 to APP-4 (WO 4.2, 3 of 3) The third of three pull requests for WO 4.2 (owner rulings 2026-11-12). Each leg restates the Agda definitions of verification/proofs/agda/Applied/ clause for clause and re-proves every theorem, the laws of the integer instance included. - verification/proofs/coq/Cohort.v: Rocq 8.18.0; the gate finds all 82 theorems closed under the global context. The standard library's PeanoNat and Lia prove the natural-number arithmetic; `Unset Lia Cache` keeps lia from writing a file. - verification/proofs/lean4/Cohort.lean: Lean 4.29.0, core only; the gate finds no axiom in any of the 95 theorems. No simp, omega or ac_rfl, which bring propext in; overlapping patterns are listed case by case for the same reason, and natLt and monus recurse on their second argument as Agda's do. - PROOF-STATUS records the legs and how the statements were compared; PROOF-NEEDS, EXPLAINME (15 proven of 17 legs), README, ROADMAP and the applied documents follow; the deed lists the two new files. No receipt records APP-1 to APP-4 yet, so no grade is derived for them. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- EXPLAINME.adoc | 22 +- README.adoc | 6 +- .../finance/cohort-economics/README.adoc | 4 +- .../finance/cohort-economics/modes.adoc | 2 +- .../methods/types-and-assurance.adoc | 2 +- docs/status/PROOF-NEEDS.adoc | 24 +- docs/status/PROOF-STATUS.adoc | 71 +- docs/status/ROADMAP.adoc | 13 +- mathesis_chora.deed | 1 + verification/proofs/coq/Cohort.v | 861 ++++++++++++++++ verification/proofs/coq/MANIFEST | 1 + verification/proofs/lean4/Cohort.lean | 945 ++++++++++++++++++ verification/proofs/lean4/MANIFEST | 1 + 13 files changed, 1919 insertions(+), 34 deletions(-) create mode 100644 verification/proofs/coq/Cohort.v create mode 100644 verification/proofs/lean4/Cohort.lean diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index d1023be..d3efbf4 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -135,7 +135,7 @@ Methods that apply mathematics to decisions, starting with accounting and finance. A shared input schema keeps missing apart from zero. A cohort model in Agda has three number modes and three synthetic worked examples, each checked by Agda. Its four general properties are proved -in Agda; the Rocq and Lean re-proofs are next. +in Agda and re-proved in Rocq and Lean. ____ How this is implemented:: @@ -152,7 +152,7 @@ fails it. Caveat:: Its four general properties (APP-1 to APP-4) are proved in Agda for the -model as it runs; the Rocq and Lean re-proofs are open. The examples are synthetic and say nothing about any +model as it runs, and re-proved in Rocq and Lean. The examples are synthetic and say nothing about any organisation. The management-accounting design has no model yet. == Privacy by count @@ -289,14 +289,20 @@ cash identity, the funding gap, status never upgrades), Agda leg |The model only. APP-2 and APP-3 rest on the laws that `IntLaws.agda` proves for the integer instance -|APP-1 to APP-4, Rocq and Lean legs -|open -|- -|- -|Not yet re-proved (WO 4.2, third pull request) +|APP-1 to APP-4, Rocq leg (re-proved) +|proven +|Rocq 8.18.0, `coqc`; `Print Assumptions` closed +|`verification/proofs/coq/Cohort.v` +|The model only, as in Agda + +|APP-1 to APP-4, Lean leg (re-proved) +|proven +|Lean 4.29.0, `lean`; no axiom +|`verification/proofs/lean4/Cohort.lean` +|The model only, as in Agda |=== -Proofs, counted by leg: 7 proven of 17; 1 argued, 9 open (the token-lattice +Proofs, counted by leg: 15 proven of 17; 1 argued, 1 open (the token-lattice theorems count as one; APP-1 to APP-4 count one for each prover). The registry derives `PWG-1` for THY-1 from the receipt. The checker versions are those that CI asserts in the Guix shell (CI run 43057783538). diff --git a/README.adoc b/README.adoc index 477687d..27b1647 100644 --- a/README.adoc +++ b/README.adoc @@ -36,15 +36,15 @@ describes what is proved, where, and how strongly. with accounting and finance. A shared input schema keeps missing apart from zero. A cohort model in Agda has three number modes and three synthetic worked examples, each checked by Agda. Its four general properties are proved - in Agda; the Rocq and Lean re-proofs are next. + in Agda and re-proved in Rocq and Lean. * *Privacy by count.* The frame names public repositories only. The number of private repositories in the listing is kept as one number. [NOTE] .Planned ==== -The token-lattice theorems of the theory shelf, the Rocq and Lean re-proofs -of the cohort model (APP-1 to APP-4), a published atlas, receipts in more home +The token-lattice theorems of the theory shelf, receipts for the cohort model +proofs (APP-1 to APP-4), a published atlas, receipts in more home repositories, and a scheduled census. See link:docs/status/ROADMAP.adoc[the roadmap]. ==== diff --git a/applied-systems/finance/cohort-economics/README.adoc b/applied-systems/finance/cohort-economics/README.adoc index ef4015b..85e7fde 100644 --- a/applied-systems/finance/cohort-economics/README.adoc +++ b/applied-systems/finance/cohort-economics/README.adoc @@ -41,6 +41,6 @@ link:../../methods/input-schema.adoc[input schema], and its expected outputs. `just applied-build` writes link:generated/examples.adoc[the worked examples] and one Agda module for each example. Agda accepts that module only if the model computes every expected output, missing ones included. The general -properties of the model, APP-1 to APP-4, are proved in Agda (Rocq and Lean -re-proofs open); see +properties of the model, APP-1 to APP-4, are proved in Agda and re-proved in +Rocq and Lean; see `docs/status/PROOF-NEEDS.adoc`. diff --git a/applied-systems/finance/cohort-economics/modes.adoc b/applied-systems/finance/cohort-economics/modes.adoc index abcd5ef..5c64460 100644 --- a/applied-systems/finance/cohort-economics/modes.adoc +++ b/applied-systems/finance/cohort-economics/modes.adoc @@ -66,4 +66,4 @@ costs and floors in each mode, so you can compare the results. different rates. * The model checks each worked example exactly. The general properties (obligations APP-1 to APP-4 in `docs/status/PROOF-NEEDS.adoc`) are proved - in Agda for every mode; the Rocq and Lean re-proofs are open. + in Agda for every mode, and re-proved in Rocq and Lean. diff --git a/applied-systems/methods/types-and-assurance.adoc b/applied-systems/methods/types-and-assurance.adoc index 3a550c0..42c489f 100644 --- a/applied-systems/methods/types-and-assurance.adoc +++ b/applied-systems/methods/types-and-assurance.adoc @@ -31,5 +31,5 @@ The cohort model (`verification/proofs/agda/Applied/Cohort.agda`) is the first test of these ideas. Each value carries its evidence status, a missing value stays missing, and every worked example is checked by Agda. Its general properties (obligations APP-1 to APP-4 in `docs/status/PROOF-NEEDS.adoc`) are -proved in Agda; the Rocq and Lean re-proofs are open. A check of a model on an example is not a proof of the model, and neither +proved in Agda and re-proved in Rocq and Lean. A check of a model on an example is not a proof of the model, and neither establishes the truth of real inputs. diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index eef7efc..edf291a 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -42,31 +42,31 @@ missing input is missing, in every period after it too, and never zero. A verdict is "no" on a known breach and otherwise missing when any value it depends on is missing; it is never "yes" then |Agda, re-checked in Rocq and Lean -|Agda leg proved; Rocq and Lean legs open (WO 4.2) -|`verification/proofs/agda/Applied/Missing.agda` +|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean` |APP-2 |Cash identity: the closing cash of the last period equals the opening cash plus, summed over the periods, receipts minus payments; when a value is missing, both sides are missing |Agda, re-checked in Rocq and Lean -|Agda leg proved; Rocq and Lean legs open (WO 4.2) -|`verification/proofs/agda/Applied/Cash.agda` (`cash-identity`) +|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|`verification/proofs/agda/Applied/Cash.agda` (`cash-identity`); Rocq and Lean: `cash_identity` |APP-3 |The funding gap is sound and least: adding the gap to the opening cash keeps every closing balance at or above its floor, and no smaller non-negative amount does |Agda, re-checked in Rocq and Lean -|Agda leg proved; Rocq and Lean legs open (WO 4.2) -|`verification/proofs/agda/Applied/Cash.agda` (`gap-sound`, `gap-least`) +|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|`verification/proofs/agda/Applied/Cash.agda` (`gap-sound`, `gap-least`); Rocq and Lean: `gap_sound`, `gap_least` |APP-4 |Status never upgrades: the evidence status of an output is never stronger than the weakest status of the inputs that it depends on |Agda, re-checked in Rocq and Lean -|Agda leg proved; Rocq and Lean legs open (WO 4.2) -|`verification/proofs/agda/Applied/Missing.agda` +|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean` |=== APP-1 to APP-4 are about the cohort model of the applied shelf (re-anchoring @@ -79,8 +79,12 @@ The Agda leg holds for the model as it runs. APP-1 and APP-4 hold for any number structure: one statement carries both (`Covers`, in `Applied/Status.agda`). APP-2 and APP-3 hold for any ordered abelian group (`Laws`, in `Applied/Cash.agda`), and `Applied/IntLaws.agda` proves that -the integer instance of the worked examples is one. Every module is in the -gated Agda manifest, with no postulate in its import cone. +the integer instance of the worked examples is one. The Rocq and Lean legs +(`verification/proofs/coq/Cohort.v`, `verification/proofs/lean4/Cohort.lean`) +restate the same definitions and re-prove every theorem, the integer laws +included. Every module is gated: no postulate in an Agda import cone, every +Rocq theorem closed under the global context, and no axiom in any Lean +theorem. No receipt records these legs yet, so no grade is derived. No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed declares neither capability. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 77b702d..411ff8e 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -24,15 +24,14 @@ reader of PROOF-POLICY §8.5.1. |Not yet stated in a prover |APP-1 to APP-4, the cohort model of the applied shelf (WO 4.2) -|Agda leg proved; Rocq and Lean legs open +|Proved in Agda, Rocq and Lean |- -|`verification/proofs/agda/Applied/Missing.agda`, `Cash.agda` and -`IntLaws.agda`, gated in CI. No receipt yet: a grade needs all three legs +|The record below. No receipt yet, so no grade is derived |=== -*Overall*: 1 of 6 obligations discharged; 5 open (the token-lattice theorems -count as one). APP-1 to APP-4 have their Agda leg; each stays open until its -Rocq and Lean legs land. These are counts, not a +*Overall*: 5 of 6 obligations are proved in all three provers; THY-1 alone has +a receipt and a derived grade. The token-lattice theorems (counted as one) are +open. These are counts, not a percentage: PROOF-POLICY §8 grades are derived from receipts and are never flattened. The template example proofs were removed in WO 4.1. @@ -211,6 +210,62 @@ dependency units unify features separately, and the theorem applies to each unit's graph. |=== +== Applied obligations + +=== APP-1 to APP-4: the cohort model of the applied shelf + +[cols="1,3"] +|=== +|Statements +|`docs/status/PROOF-NEEDS.adoc`, rows APP-1 to APP-4. + +|Agda (source of truth) +|`verification/proofs/agda/Applied/`: `Cohort` (the model), `Status` and +`Missing` (APP-1, APP-4), `Cash` (APP-2, APP-3, for any ordered abelian +group), `IntNumber` and `IntLaws` (the integer instance and its laws). +`--safe --without-K --cubical-compatible`; no postulate in any import cone. + +|Rocq leg +|`PROVEN`, route `re-proved`. `verification/proofs/coq/Cohort.v`, Rocq +8.18.0. The gate's `Print Assumptions` finds all 82 theorems closed under +the global context. The standard library's `PeanoNat` and `Lia` prove the +natural-number arithmetic; `Unset Lia Cache` keeps `lia` from writing a +file. + +|Lean leg +|`PROVEN`, route `re-proved`. `verification/proofs/lean4/Cohort.lean`, +Lean 4.29.0, core only. The gate's audit finds no axiom in any of the 95 +theorems. No `simp`, `omega` or `ac_rfl`: each brings `propext` in. + +|Statement correspondence (§2.2) +|Compared by reading, item by item. Each target restates every Agda +definition with the same constructors, fields and clauses, and states every +Agda theorem with the same hypotheses and conclusions (Agda `cash-identity` +is `cash_identity`, and so on). The differences are encoding only: + +* Agda's `_<_` and `_-_` on Nat are `natLt` and `monus`, with the same + clauses, recursive on the second argument as Agda's are, so that the + same terms reduce. +* Lean compiles overlapping patterns with `propext`, so `meet`, + `zipWith`, `kand` and `denominator` list their cases without overlap; + `zipWith` and `kand` split their first argument first, as Agda's do. + Each is the same function. +* Agda's `n div suc m` is `Nat.div` (Rocq) or `/` (Lean): each rounds + down and gives 0 for a zero divisor. +* `T b` is `b = true`. The proof-relevant records `Covers`, `Bounded` + and `Yes` are existential propositions, so every result is a theorem + that the axiom audit inspects. `All` and `Any` stay functions on lists. +* The integers are Agda's (`pos`, `negsuc` and the same operations), not + the standard `Z` or `Int`: Lean's `Int` lemmas use `propext`. + +Residual assumptions: none in any leg. + +|Machine receipt (§8.5.1) +|None yet. The receipt `verification/receipts/theory_praxis.deed` records +THY-1 only. Adding APP-1 to APP-4 needs receipts from a CI run on the merged +commit, so no grade is derived for them yet. +|=== + == Verification commands [source,bash] @@ -233,6 +288,10 @@ bash tests/proofs/gate_controls_test.sh agda |THY-1 receipts earned again at Agda 2.7.0.1 and Lean 4.29.0 in the pinned Guix shell; the receipt derives `PWG-1`. +|2026-11-12 +|APP-1 to APP-4 proved in Agda (with the laws of the integer instance), then +re-proved in Rocq and Lean (re-anchoring plan WO 4.2). No receipt yet. + |2026-11-11 |The template obligations ABI-1 to ABI-5, TP-1 and TP-2 leave the lists: they never applied to Mathesis (re-anchoring plan WO 3.4, owner ruling diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 785a03a..f2dfaff 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -191,7 +191,14 @@ One pull request that changes census rows is open at a time (atlas README, for the model as it runs. ** The two local helpers of `cohortAt` became top-level functions, so that the proofs can name them. The worked examples are unchanged. -** Next: the Rocq and Lean re-proofs (third pull request). +** Merged (pull request 83). +* WO 4.2, third pull request: the Rocq and Lean re-proofs of APP-1 to APP-4, + with the integer laws: `verification/proofs/coq/Cohort.v` (82 theorems, + `Print Assumptions` closed) and `verification/proofs/lean4/Cohort.lean` + (95 theorems, no axiom). Each restates the Agda definitions clause for + clause; `docs/status/PROOF-STATUS.adoc` records the comparison. WO 4.2 is + then done. Next: receipts for APP-1 to APP-4, from a CI run on the merged + commit, then WO 4.3 (needs a ruling). * Open item for the owner (ruling 2026-11-12): none of the JSON Lines data files declares a licence; JSON has no comment syntax. The owner will write one `REUSE.toml` rule at the root that covers all of them (doctrine 6: a @@ -237,8 +244,8 @@ anchors `c81cb84` |The three shelves: the theory admission rule and the token-lattice theorems, the applied shelf tied to the evidence spine, the published atlas (needs a ruling) -|In progress: WO 4.1, the theory ledger and WO 4.2 (1 of 3) merged; the -Agda proofs of WO 4.2 in review +|In progress: WO 4.1, the theory ledger and WO 4.2 (2 of 3) merged; the +Rocq and Lean re-proofs of WO 4.2 in review |5 |Scale: receipts in the home repositories, the bridge lock pilot, a diff --git a/mathesis_chora.deed b/mathesis_chora.deed index a0bf5ac..b456514 100644 --- a/mathesis_chora.deed +++ b/mathesis_chora.deed @@ -1021,6 +1021,7 @@ "verification/proofs/agda/FeatureReachability.agda" "verification/proofs/coq/FeatureReachability.v" "verification/proofs/lean4/FeatureReachability.lean" + "verification/proofs/coq/Cohort.v" "verification/proofs/lean4/Cohort.lean" "EXPLAINME.adoc" "docs/theory/admissions.jsonl" "docs/theory/ledger.jsonl" "docs/theory/generated/" "scripts/applied/" "tests/applied/" "verification/proofs/agda/Applied/") diff --git a/verification/proofs/coq/Cohort.v b/verification/proofs/coq/Cohort.v new file mode 100644 index 0000000..24a94b9 --- /dev/null +++ b/verification/proofs/coq/Cohort.v @@ -0,0 +1,861 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) + +(** APP-1 to APP-4, Rocq leg (re-proved by hand), and the integer laws. + + Source of truth: verification/proofs/agda/Applied/ (Cohort, Status, + Missing, Cash, IntNumber, IntLaws). This file restates the same + definitions, clause for clause, and proves the same theorems again; it + is not a translation. docs/status/PROOF-STATUS.adoc records how the + statements were compared. + + Correspondence choices, all mirrored from the Agda source: + - Agda's [_<_] and [_-_] on Nat are [natLt] and [monus] here, with the + same clauses, recursive on the second argument as in Agda. + - Agda's [T b] is [b = true]. Agda's proof-relevant records [Covers] and + [Bounded] are existential propositions here. + - Agda's [All] and [Any] (functions on lists) are [Forall'] and [Exists']. + - The integers are Agda's: [Z'] with [pos] and [negsuc], and the same + operations, not the standard library's [Z]. + - [lia] (standard library) proves the natural-number arithmetic; it adds + no axiom, as the gate's [Print Assumptions] audit checks. *) + +From Coq Require Import PeanoNat Lia. + +(* Keep lia from writing a cache file beside the sources. *) +Unset Lia Cache. + +(** * Natural numbers, as Agda.Builtin.Nat defines them *) + +Fixpoint natLt (n m : nat) {struct m} : bool := + match m with + | 0 => false + | S m' => match n with 0 => true | S n' => natLt n' m' end + end. + +Fixpoint monus (n m : nat) {struct m} : nat := + match m with + | 0 => n + | S m' => match n with 0 => 0 | S n' => monus n' m' end + end. + +(** * Evidence status *) + +Inductive Status : Type := + | illustrative | estimate | reported | verified | definitional. + +Definition meet (s t : Status) : Status := + match s, t with + | illustrative, _ => illustrative + | _, illustrative => illustrative + | estimate, _ => estimate + | _, estimate => estimate + | reported, _ => reported + | _, reported => reported + | verified, _ => verified + | _, verified => verified + | definitional, definitional => definitional + end. + +Definition rank (s : Status) : nat := + match s with + | illustrative => 0 | estimate => 1 | reported => 2 | verified => 3 | definitional => 4 + end. + +Fixpoint leB (m n : nat) : bool := + match m, n with + | 0, _ => true + | S _, 0 => false + | S m', S n' => leB m' n' + end. + +(** [stLe s t]: status s is no stronger than status t. *) +Definition stLe (s t : Status) : Prop := leB (rank s) (rank t) = true. + +Lemma leB_trans : forall a b c, leB a b = true -> leB b c = true -> leB a c = true. +Proof. + intro a; induction a as [|a IH]; intros [|b] [|c] p q; simpl in *; try reflexivity; try discriminate. + exact (IH b c p q). +Qed. + +Lemma stLe_refl : forall s, stLe s s. +Proof. intros []; reflexivity. Qed. + +Lemma stLe_trans : forall s t u, stLe s t -> stLe t u -> stLe s u. +Proof. intros s t u. apply leB_trans. Qed. + +Lemma meet_le_left : forall s t, stLe (meet s t) s. +Proof. intros [] []; reflexivity. Qed. + +Lemma meet_le_right : forall s t, stLe (meet s t) t. +Proof. intros [] []; reflexivity. Qed. + +Lemma meet_assoc : forall s t u, meet (meet s t) u = meet s (meet t u). +Proof. intros [] [] []; reflexivity. Qed. + +Lemma meet_definitional : forall s, meet s definitional = s. +Proof. intros []; reflexivity. Qed. + +(** * Values that may be missing *) + +Inductive Val (A : Type) : Type := + | missing : Val A + | given : Status -> A -> Val A. +Arguments missing {A}. +Arguments given {A}. + +Definition vpure {A : Type} (a : A) : Val A := given definitional a. + +Definition vmap {A B : Type} (f : A -> B) (x : Val A) : Val B := + match x with missing => missing | given s a => given s (f a) end. + +Definition zipWith {A B C : Type} (f : A -> B -> C) (x : Val A) (y : Val B) : Val C := + match x, y with + | given s a, given t b => given (meet s t) (f a b) + | _, _ => missing + end. + +(** Kleene conjunction: a known [false] decides the result. *) +Definition kand (x y : Val bool) : Val bool := + match x, y with + | given s false, _ => given s false + | given s true, given t b => given (meet s t) b + | given _ true, missing => missing + | missing, given t false => given t false + | missing, _ => missing + end. + +Fixpoint at' {A : Type} (n : nat) (l : list (Val A)) {struct l} : Val A := + match l with + | nil => missing + | cons x xs => match n with 0 => x | S n' => at' n' xs end + end. + +(** * Cohorts and rates *) + +Inductive Rate : Type := + | perMille : nat -> Rate + | fraction : nat -> nat -> Rate. + +Inductive Cohort : Type := + | observed : nat -> list (Val nat) -> Cohort + | modelled : nat -> Val nat -> Val Rate -> Val Rate -> Cohort. + +Definition denominator (r : Val Rate) : nat := + match r with given _ (fraction _ d) => d | _ => 1 end. + +Fixpoint scaleOf (periods : nat) (cs : list Cohort) : nat := + match cs with + | nil => 1 + | cons (observed _ _) cs' => scaleOf periods cs' + | cons (modelled _ _ c r) cs' => denominator c * Nat.pow (denominator r) periods * scaleOf periods cs' + end. + +Definition applyRate (scale x : nat) (r : Rate) : nat := + match r with + | perMille m => Nat.div (Nat.div x scale * m) 1000 * scale + | fraction n d => Nat.div (x * n) d + end. + +Definition joined (scale : nat) (contacts : Val nat) (conversion : Val Rate) : Val nat := + zipWith (applyRate scale) (vmap (fun n => n * scale) contacts) conversion. + +Fixpoint renewed (scale : nat) (start : Val nat) (retention : Val Rate) (k : nat) : Val nat := + match k with + | 0 => start + | S k' => zipWith (applyRate scale) (renewed scale start retention k') retention + end. + +Definition cohortAt (scale t : nat) (c : Cohort) : Val nat := + match c with + | observed start counts => + if natLt t start then vpure 0 else vmap (fun n => n * scale) (at' (monus t start) counts) + | modelled start contacts conversion retention => + if natLt t start then vpure 0 + else renewed scale (joined scale contacts conversion) retention (monus t start) + end. + +Fixpoint sumAt (scale t : nat) (cs : list Cohort) : Val nat := + match cs with + | nil => vpure 0 + | cons c cs' => zipWith Nat.add (cohortAt scale t c) (sumAt scale t cs') + end. + +(** * The model *) + +Record Number : Type := mkNumber { + R : Type; + zero : R; + add : R -> R -> R; + sub : R -> R -> R; + mul : R -> R -> R; + le : R -> R -> bool; + fromNat : nat -> R +}. + +Definition Covers {A : Type} (u : Status) (v : Val A) : Prop := + exists s a, v = given s a /\ stLe u s. + +Fixpoint Forall' {A : Type} (P : A -> Prop) (l : list A) : Prop := + match l with nil => True | cons x xs => P x /\ Forall' P xs end. + +Fixpoint Exists' {A : Type} (P : A -> Prop) (l : list A) : Prop := + match l with nil => False | cons x xs => P x \/ Exists' P xs end. + +Lemma forall_map : forall {A : Type} (P Q : A -> Prop), (forall x, P x -> Q x) -> + forall xs, Forall' P xs -> Forall' Q xs. +Proof. + intros A P Q f. induction xs as [|x xs IH]; simpl; [auto|]. + intros [p ps]. split; [apply f, p | apply IH, ps]. +Qed. + +Lemma covers_weaken : forall {A : Type} (u w : Status) (v : Val A), + stLe u w -> Covers w v -> Covers u v. +Proof. + intros A u w v le [s [a [e le']]]. exists s, a. split; [exact e | exact (stLe_trans u w s le le')]. +Qed. + +Lemma zipWith_given : forall {A B C : Type} (f : A -> B -> C) x y u c, + zipWith f x y = given u c -> Covers u x /\ Covers u y. +Proof. + intros A B C f [|s a] [|t b] u c e; simpl in e; try discriminate. + injection e as <- <-. split. + - exists s, a. split; [reflexivity | apply meet_le_left]. + - exists t, b. split; [reflexivity | apply meet_le_right]. +Qed. + +Lemma zipWith_needs : forall {A B C : Type} (f : A -> B -> C) x y u, + Covers u (zipWith f x y) -> Covers u x /\ Covers u y. +Proof. + intros A B C f x y u [s [c [e le]]]. + destruct (zipWith_given f x y s c e) as [cx cy]. + split; [exact (covers_weaken u s x le cx) | exact (covers_weaken u s y le cy)]. +Qed. + +Lemma map_needs : forall {A B : Type} (f : A -> B) x u, Covers u (vmap f x) -> Covers u x. +Proof. + intros A B f [|s a] u [s' [c [e le]]]; simpl in e; [discriminate|]. + injection e as <- _. exists s, a. split; [reflexivity | exact le]. +Qed. + +Lemma missing_uncovered : forall {A : Type} (u : Status), ~ Covers u (@missing A). +Proof. intros A u [s [a [e _]]]. discriminate. Qed. + +Lemma joined_needs : forall u scale contacts conversion, + Covers u (joined scale contacts conversion) -> Covers u contacts /\ Covers u conversion. +Proof. + intros u scale contacts conversion c. unfold joined in c. + destruct (zipWith_needs _ _ _ u c) as [cl cc]. split; [exact (map_needs _ _ u cl) | exact cc]. +Qed. + +Lemma renewed_joined : forall u scale start retention k, + Covers u (renewed scale start retention k) -> Covers u start. +Proof. + intros u scale start retention. induction k as [|k IH]; simpl; intro c; [exact c|]. + apply IH. exact (proj1 (zipWith_needs _ _ _ u c)). +Qed. + +Lemma renewed_retention : forall u scale start retention k, + Covers u (renewed scale start retention (S k)) -> Covers u retention. +Proof. intros u scale start retention k c. exact (proj2 (zipWith_needs _ _ _ u c)). Qed. + +Lemma modelled_needs : forall u scale t start contacts conversion retention, + natLt t start = false -> + Covers u (cohortAt scale t (modelled start contacts conversion retention)) -> + Covers u contacts /\ Covers u conversion. +Proof. + intros u scale t start contacts conversion retention h c. simpl in c. rewrite h in c. + exact (joined_needs _ _ _ _ (renewed_joined _ _ _ _ _ c)). +Qed. + +Lemma modelled_renewal_needs : forall u scale t start contacts conversion retention k, + natLt t start = false -> monus t start = S k -> + Covers u (cohortAt scale t (modelled start contacts conversion retention)) -> Covers u retention. +Proof. + intros u scale t start contacts conversion retention k h gap c. simpl in c. rewrite h, gap in c. + exact (renewed_retention _ _ _ _ _ c). +Qed. + +Lemma observed_needs : forall u scale t start counts, + natLt t start = false -> Covers u (cohortAt scale t (observed start counts)) -> + Covers u (at' (monus t start) counts). +Proof. + intros u scale t start counts h c. simpl in c. rewrite h in c. exact (map_needs _ _ u c). +Qed. + +Lemma sum_needs : forall u scale t cs, + Covers u (sumAt scale t cs) -> Forall' (fun c => Covers u (cohortAt scale t c)) cs. +Proof. + intros u scale t. induction cs as [|c cs IH]; simpl; intro h; [exact I|]. + destruct (zipWith_needs _ _ _ u h) as [hc hr]. split; [exact hc | exact (IH hr)]. +Qed. + +(** A "yes" needs both sides to be a known "yes". *) +Definition Yes (u : Status) (v : Val bool) : Prop := exists s, v = given s true /\ stLe u s. + +Lemma kand_yes : forall x y u, kand x y = given u true -> Yes u x /\ Yes u y. +Proof. + intros [|s [|]] [|t [|]] u e; simpl in e; try discriminate. + - injection e as <-. split; [exists s | exists t]; split; try reflexivity; + [apply meet_le_left | apply meet_le_right]. +Qed. + +Lemma kand_false_left : forall x y s, x = given s false -> kand x y = given s false. +Proof. intros x y s ->. reflexivity. Qed. + +Lemma kand_false_right : forall x y t, y = given t false -> exists u, kand x y = given u false. +Proof. + intros [|s [|]] y t ->; simpl. + - exists t. reflexivity. + - exists (meet s t). reflexivity. + - exists s. reflexivity. +Qed. + +Section Model. + +Variable N : Number. + +Definition nmax (a b : R N) : R N := if le N a b then b else a. + +Record Inputs : Type := mkInputs { + periods : nat; + opening : Val (R N); + price : Val (R N); + unitCost : Val (R N); + minutes : Val (R N); + fixed : list (Val (R N)); + floor : list (Val (R N)); + capacity : list (Val (R N)); + cohorts : list Cohort +}. + +Record Row : Type := mkRow { + members : Val (R N); + receipts : Val (R N); + payments : Val (R N); + closing : Val (R N); + shortfall : Val (R N); + hours : Val (R N); + cashOk : Val bool; + capacityOk : Val bool +}. + +Definition scale (i : Inputs) : nat := scaleOf (periods i) (cohorts i). + +Definition scaled (i : Inputs) : Val (R N) -> Val (R N) := + vmap (fun x => mul N x (fromNat N (scale i))). + +Definition rowAt (i : Inputs) (t : nat) (previous : Val (R N)) : Row := + let m := vmap (fromNat N) (sumAt (scale i) t (cohorts i)) in + let rec_ := zipWith (mul N) (price i) m in + let pay := zipWith (add N) (scaled i (at' (monus t 1) (fixed i))) (zipWith (mul N) (unitCost i) m) in + let clo := zipWith (sub N) (zipWith (add N) previous rec_) pay in + let hrs := zipWith (mul N) (minutes i) m in + let flo := scaled i (at' (monus t 1) (floor i)) in + mkRow m rec_ pay clo (zipWith (sub N) flo clo) hrs (zipWith (le N) flo clo) + (zipWith (le N) hrs (scaled i (at' (monus t 1) (capacity i)))). + +Fixpoint rowsFrom (i : Inputs) (t n : nat) (previous : Val (R N)) : list Row := + match n with + | 0 => nil + | S n' => cons (rowAt i t previous) (rowsFrom i (S t) n' (closing (rowAt i t previous))) + end. + +Definition allRows (i : Inputs) : list Row := rowsFrom i 1 (periods i) (scaled i (opening i)). + +Fixpoint verdict (f : Row -> Val bool) (rs : list Row) : Val bool := + match rs with nil => vpure true | cons r rs' => kand (f r) (verdict f rs') end. + +Fixpoint worst (rs : list Row) : Val (R N) := + match rs with nil => vpure (zero N) | cons r rs' => zipWith nmax (shortfall r) (worst rs') end. + +(** * APP-1 and APP-4: what a given output needs *) + +Section Needs. + +Variable i : Inputs. + +Lemma members_needs : forall u t previous, + Covers u (members (rowAt i t previous)) -> Covers u (sumAt (scale i) t (cohorts i)). +Proof. intros u t previous c. exact (map_needs _ _ u c). Qed. + +Lemma receipts_needs : forall u t previous, + Covers u (receipts (rowAt i t previous)) -> Covers u (price i) /\ Covers u (sumAt (scale i) t (cohorts i)). +Proof. + intros u t previous c. destruct (zipWith_needs _ _ _ u c) as [cp cm]. + split; [exact cp | exact (map_needs _ _ u cm)]. +Qed. + +Lemma payments_needs : forall u t previous, + Covers u (payments (rowAt i t previous)) -> + Covers u (at' (monus t 1) (fixed i)) /\ Covers u (unitCost i) /\ Covers u (sumAt (scale i) t (cohorts i)). +Proof. + intros u t previous c. destruct (zipWith_needs _ _ _ u c) as [cf cv]. + destruct (zipWith_needs _ _ _ u cv) as [cu cm]. + split; [exact (map_needs _ _ u cf) | split; [exact cu | exact (map_needs _ _ u cm)]]. +Qed. + +Lemma closing_needs : forall u t previous, + Covers u (closing (rowAt i t previous)) -> + Covers u previous /\ Covers u (price i) /\ Covers u (at' (monus t 1) (fixed i)) /\ + Covers u (unitCost i) /\ Covers u (sumAt (scale i) t (cohorts i)). +Proof. + intros u t previous c. destruct (zipWith_needs _ _ _ u c) as [cpr cpay]. + destruct (zipWith_needs _ _ _ u cpr) as [cprev crec]. + destruct (payments_needs u t previous cpay) as [cf [cu cm]]. + repeat split; try assumption. exact (proj1 (zipWith_needs _ _ _ u crec)). +Qed. + +Lemma shortfall_needs : forall u t previous, + Covers u (shortfall (rowAt i t previous)) -> + Covers u (at' (monus t 1) (floor i)) /\ Covers u (closing (rowAt i t previous)). +Proof. + intros u t previous c. destruct (zipWith_needs _ _ _ u c) as [cfl cc]. + split; [exact (map_needs _ _ u cfl) | exact cc]. +Qed. + +Lemma cashOk_needs : forall u t previous, + Covers u (cashOk (rowAt i t previous)) -> + Covers u (at' (monus t 1) (floor i)) /\ Covers u (closing (rowAt i t previous)). +Proof. + intros u t previous c. destruct (zipWith_needs _ _ _ u c) as [cfl cc]. + split; [exact (map_needs _ _ u cfl) | exact cc]. +Qed. + +Lemma hours_needs : forall u t previous, + Covers u (hours (rowAt i t previous)) -> Covers u (minutes i) /\ Covers u (sumAt (scale i) t (cohorts i)). +Proof. + intros u t previous c. destruct (zipWith_needs _ _ _ u c) as [cmin cm]. + split; [exact cmin | exact (map_needs _ _ u cm)]. +Qed. + +Lemma capacityOk_needs : forall u t previous, + Covers u (capacityOk (rowAt i t previous)) -> + Covers u (minutes i) /\ Covers u (sumAt (scale i) t (cohorts i)) /\ Covers u (at' (monus t 1) (capacity i)). +Proof. + intros u t previous c. destruct (zipWith_needs _ _ _ u c) as [ch ccap]. + destruct (hours_needs u t previous ch) as [cmin cm]. + split; [exact cmin | split; [exact cm | exact (map_needs _ _ u ccap)]]. +Qed. + +Lemma opening_needs : forall u, Covers u (scaled i (opening i)) -> Covers u (opening i). +Proof. intros u c. exact (map_needs _ _ u c). Qed. + +Lemma closings_missing : forall n t, Forall' (fun r => closing r = missing) (rowsFrom i t n missing). +Proof. + induction n as [|n IH]; intro t; simpl; [exact I|]. split; [reflexivity | apply IH]. +Qed. + +Lemma missing_persists : forall t n previous, closing (rowAt i t previous) = missing -> + Forall' (fun r => closing r = missing) (rowsFrom i (S t) n (closing (rowAt i t previous))). +Proof. intros t n previous h. rewrite h. apply closings_missing. Qed. + +Lemma verdict_yes : forall (f : Row -> Val bool) rs u, + verdict f rs = given u true -> Forall' (fun r => Yes u (f r)) rs. +Proof. + intro f. induction rs as [|r rs IH]; simpl; intros u e; [exact I|]. + destruct (kand_yes _ _ _ e) as [yr [s [e' le]]]. split; [exact yr|]. + apply (forall_map (fun r => Yes s (f r))). + - intros x [s' [ex le']]. exists s'. split; [exact ex | exact (stLe_trans u s s' le le')]. + - exact (IH s e'). +Qed. + +Lemma breach_decides : forall (f : Row -> Val bool) rs, + Exists' (fun r => exists s, f r = given s false) rs -> exists u, verdict f rs = given u false. +Proof. + intro f. induction rs as [|r rs IH]; simpl; intro h; [destruct h|]. + destruct h as [[s e] | p]. + - exists s. exact (kand_false_left _ _ _ e). + - destruct (IH p) as [t e]. exact (kand_false_right _ _ _ e). +Qed. + +Lemma gap_needs : forall u rs, Covers u (worst rs) -> Forall' (fun r => Covers u (shortfall r)) rs. +Proof. + intro u. induction rs as [|r rs IH]; simpl; intro c; [exact I|]. + destruct (zipWith_needs _ _ _ u c) as [cs rest]. split; [exact cs | exact (IH rest)]. +Qed. + +End Needs. + +(** * APP-2 and APP-3: ordered abelian groups *) + +Record Laws : Type := mkLaws { + neg : R N -> R N; + add_assoc : forall a b c, add N (add N a b) c = add N a (add N b c); + add_comm : forall a b, add N a b = add N b a; + add_zero : forall a, add N a (zero N) = a; + add_neg : forall a, add N a (neg a) = zero N; + sub_def : forall a b, sub N a b = add N a (neg b); + le_refl : forall a, le N a a = true; + le_trans : forall a b c, le N a b = true -> le N b c = true -> le N a c = true; + le_total : forall a b, le N a b = false -> le N b a = true; + le_add : forall a b c, le N a b = true -> le N (add N a c) (add N b c) = true +}. + +Section Cash. + +Variable L : Laws. + +Lemma step_law : forall a r q x, + add N (sub N (add N a r) q) x = add N a (add N (sub N r q) x). +Proof. + intros a r q x. rewrite !(sub_def L), (add_assoc L a r (neg L q)), (add_assoc L a (add N r (neg L q)) x). + reflexivity. +Qed. + +Lemma shift_law : forall a g r q, + sub N (add N (add N a g) r) q = add N (sub N (add N a r) q) g. +Proof. + intros a g r q. rewrite !(sub_def L), (add_assoc L a g r), (add_comm L g r), <- (add_assoc L a r g), + (add_assoc L (add N a r) g (neg L q)), (add_comm L g (neg L q)), <- (add_assoc L (add N a r) (neg L q) g). + reflexivity. +Qed. + +Lemma cancel_right : forall f c, add N (sub N f c) c = f. +Proof. + intros f c. rewrite (sub_def L), (add_assoc L), (add_comm L (neg L c) c), (add_neg L), (add_zero L). + reflexivity. +Qed. + +Lemma cancel_left : forall c g, add N (add N c g) (neg L c) = g. +Proof. + intros c g. rewrite (add_comm L c g), (add_assoc L), (add_neg L), (add_zero L). reflexivity. +Qed. + +Lemma below_shift : forall f c g, le N (sub N f c) g = true -> le N f (add N c g) = true. +Proof. + intros f c g h. pose proof (le_add L _ _ c h) as k. + rewrite cancel_right, (add_comm L g c) in k. exact k. +Qed. + +Lemma shift_below : forall f c g, le N f (add N c g) = true -> le N (sub N f c) g = true. +Proof. + intros f c g h. pose proof (le_add L _ _ (neg L c) h) as k. + rewrite cancel_left, <- (sub_def L) in k. exact k. +Qed. + +Lemma meet4 : forall s t v w, meet (meet (meet s t) v) w = meet s (meet (meet t v) w). +Proof. intros [] [] [] []; reflexivity. Qed. + +Lemma step_val : forall p r q n : Val (R N), + zipWith (add N) (zipWith (sub N) (zipWith (add N) p r) q) n = + zipWith (add N) p (zipWith (add N) (zipWith (sub N) r q) n). +Proof. + intros [|s a] [|t b] [|v c] [|w d]; simpl; try reflexivity. + rewrite meet4, step_law. reflexivity. +Qed. + +Lemma base_val : forall p : Val (R N), p = zipWith (add N) p (vpure (zero N)). +Proof. + intros [|s a]; simpl; [reflexivity|]. rewrite meet_definitional, (add_zero L). reflexivity. +Qed. + +Lemma shift_val : forall (p r q : Val (R N)) g, + zipWith (sub N) (zipWith (add N) (vmap (fun x => add N x g) p) r) q = + vmap (fun x => add N x g) (zipWith (sub N) (zipWith (add N) p r) q). +Proof. + intros [|s a] [|t b] [|v c] g; simpl; try reflexivity. rewrite shift_law. reflexivity. +Qed. + +Lemma floor_met : forall (F C : Val (R N)) g s d, + zipWith (sub N) F C = given s d -> le N d g = true -> + exists s', zipWith (le N) F (vmap (fun x => add N x g) C) = given s' true. +Proof. + intros [|sf f] [|sc c] g s d e h; simpl in e; try discriminate. + injection e as <- <-. exists (meet sf sc). simpl. rewrite (below_shift f c g h). reflexivity. +Qed. + +Lemma floor_needs : forall (F C : Val (R N)) g s s' d, + zipWith (sub N) F C = given s d -> + zipWith (le N) F (vmap (fun x => add N x g) C) = given s' true -> le N d g = true. +Proof. + intros [|sf f] [|sc c] g s s' d e ok; simpl in e, ok; try discriminate. + injection e as <- <-. injection ok as _ h. exact (shift_below f c g h). +Qed. + +Lemma max_left : forall a b, le N a (nmax a b) = true. +Proof. + intros a b. unfold nmax. destruct (le N a b) eqn:h; [exact h | exact (le_refl L a)]. +Qed. + +Lemma max_right : forall a b, le N b (nmax a b) = true. +Proof. + intros a b. unfold nmax. destruct (le N a b) eqn:h; [exact (le_refl L b) | exact (le_total L a b h)]. +Qed. + +Lemma max_least : forall a b c, le N a c = true -> le N b c = true -> le N (nmax a b) c = true. +Proof. intros a b c ha hb. unfold nmax. destruct (le N a b); assumption. Qed. + +Variable i : Inputs. + +Fixpoint lastClosing (p : Val (R N)) (rs : list Row) : Val (R N) := + match rs with nil => p | cons r rs' => lastClosing (closing r) rs' end. + +Fixpoint netSum (rs : list Row) : Val (R N) := + match rs with + | nil => vpure (zero N) + | cons r rs' => zipWith (add N) (zipWith (sub N) (receipts r) (payments r)) (netSum rs') + end. + +(** APP-2: the closing cash of the last period is the opening cash plus, + summed over the periods, receipts minus payments. Both sides are missing + together, with the same status when given. *) +Lemma cash_identity : forall n t p, + lastClosing p (rowsFrom i t n p) = zipWith (add N) p (netSum (rowsFrom i t n p)). +Proof. + induction n as [|n IH]; intros t p; simpl; [apply base_val|]. + rewrite IH. apply step_val. +Qed. + +(** Adding g to the previous balance adds g to the closing balance. *) +Lemma shifted_closing : forall t p g, + closing (rowAt i t (vmap (fun x => add N x g) p)) = vmap (fun x => add N x g) (closing (rowAt i t p)). +Proof. intros t p g. apply shift_val. Qed. + +Definition Bounded (g : R N) (v : Val (R N)) : Prop := exists s d, v = given s d /\ le N d g = true. + +Definition Met (r : Row) : Prop := exists s, cashOk r = given s true. + +Lemma worst_bounds : forall rs u g, worst rs = given u g -> Forall' (fun r => Bounded g (shortfall r)) rs. +Proof. + induction rs as [|r rs IH]; simpl; intros u g e; [exact I|]. + destruct (zipWith_given _ _ _ _ _ e) as [[s [d [eqd _]]] [w [m [eqm _]]]]. + rewrite eqd, eqm in e. simpl in e. injection e as _ hg. + split. + - exists s, d. split; [exact eqd|]. rewrite <- hg. apply max_left. + - apply (forall_map (fun r => Bounded m (shortfall r))). + + intros x [s' [d' [e2 t2]]]. exists s', d'. split; [exact e2|]. + apply (le_trans L d' m g t2). rewrite <- hg. apply max_right. + + exact (IH w m eqm). +Qed. + +(** APP-3, sound: when every shortfall is at most g, adding g to the previous + balance meets the floor in every period. *) +Lemma meets_floor : forall n t p g, + Forall' (fun r => Bounded g (shortfall r)) (rowsFrom i t n p) -> + Forall' Met (rowsFrom i t n (vmap (fun x => add N x g) p)). +Proof. + induction n as [|n IH]; intros t p g h; cbn [rowsFrom Forall'] in h |- *; [exact I|]. + destruct h as [[s [d [eq hle]]] rest]. split. + - unfold Met. change (cashOk (rowAt i t (vmap (fun x => add N x g) p))) with + (zipWith (le N) (scaled i (at' (monus t 1) (floor i))) (closing (rowAt i t (vmap (fun x => add N x g) p)))). + rewrite shifted_closing. exact (floor_met _ _ g s d eq hle). + - rewrite shifted_closing. exact (IH (S t) (closing (rowAt i t p)) g rest). +Qed. + +Lemma gap_sound : forall n t p u g, worst (rowsFrom i t n p) = given u g -> + Forall' Met (rowsFrom i t n (vmap (fun x => add N x g) p)). +Proof. intros n t p u g e. exact (meets_floor n t p g (worst_bounds _ u g e)). Qed. + +(** APP-3, least: no smaller non-negative addition meets every floor. *) +Lemma gap_least : forall n t p u g g', worst (rowsFrom i t n p) = given u g -> le N (zero N) g' = true -> + Forall' Met (rowsFrom i t n (vmap (fun x => add N x g') p)) -> le N g g' = true. +Proof. + induction n as [|n IH]; intros t p u g g' e z h; cbn [rowsFrom worst Forall'] in e, h |- * . + - injection e as _ hg. rewrite <- hg. exact z. + - destruct (zipWith_given _ _ _ _ _ e) as [[s [d [eqd _]]] [w [m [eqm _]]]]. + rewrite eqd, eqm in e. simpl in e. injection e as _ hg. + destruct h as [[s' ok] rest]. + change (cashOk (rowAt i t (vmap (fun x => add N x g') p))) with + (zipWith (le N) (scaled i (at' (monus t 1) (floor i))) (closing (rowAt i t (vmap (fun x => add N x g') p)))) in ok. + rewrite shifted_closing in ok, rest. + pose proof (floor_needs _ _ g' _ _ _ eqd ok) as head. + pose proof (IH (S t) (closing (rowAt i t p)) w m g' eqm z rest) as tail. + rewrite <- hg. exact (max_least d m g' head tail). +Qed. + +End Cash. + +End Model. + +(** * The integer instance satisfies the laws *) + +Inductive Z' : Type := + | pos : nat -> Z' + | negsuc : nat -> Z'. + +Definition ominus (m n : nat) : Z' := + if natLt m n then negsuc (monus (monus n m) 1) else pos (monus m n). + +Definition zneg (z : Z') : Z' := + match z with pos 0 => pos 0 | pos (S n) => negsuc n | negsuc n => pos (S n) end. + +Definition zadd (i j : Z') : Z' := + match i, j with + | pos m, pos n => pos (m + n) + | pos m, negsuc n => ominus m (S n) + | negsuc m, pos n => ominus n (S m) + | negsuc m, negsuc n => negsuc (S (m + n)) + end. + +Definition zsub (a b : Z') : Z' := zadd a (zneg b). + +Definition zmul (i j : Z') : Z' := + match i, j with + | pos m, pos n => pos (m * n) + | pos m, negsuc n => zneg (pos (m * S n)) + | negsuc m, pos n => zneg (pos (S m * n)) + | negsuc m, negsuc n => pos (S m * S n) + end. + +Definition zle (i j : Z') : bool := + match i, j with + | pos m, pos n => natLt m (S n) + | pos _, negsuc _ => false + | negsuc _, pos _ => true + | negsuc m, negsuc n => natLt n (S m) + end. + +Definition intNumber : Number := mkNumber Z' (pos 0) zadd zsub zmul zle pos. + +(** m <= n, as the integer order uses it. *) +Definition leq (m n : nat) : bool := natLt m (S n). + +Lemma leq_refl : forall n, leq n n = true. +Proof. induction n as [|n IH]; [reflexivity | exact IH]. Qed. + +Lemma leq_trans : forall a b c, leq a b = true -> leq b c = true -> leq a c = true. +Proof. + intro a; induction a as [|a IH]; intros b c p q; [reflexivity|]. + destruct b as [|b]; [simpl in p; destruct a; discriminate p|]. + destruct c as [|c]; [simpl in q; destruct b; discriminate q|]. + exact (IH b c p q). +Qed. + +Lemma leq_total : forall a b, leq a b = false -> leq b a = true. +Proof. + intro a; induction a as [|a IH]; intros b h; [discriminate h|]. + destruct b as [|b]; [reflexivity|]. + exact (IH b h). +Qed. + +Lemma leq_cancel : forall k x y, leq (k + x) (k + y) = leq x y. +Proof. induction k as [|k IH]; intros x y; [reflexivity | exact (IH x y)]. Qed. + +Lemma ominus_cancel : forall k a b, ominus (k + a) (k + b) = ominus a b. +Proof. induction k as [|k IH]; intros a b; [reflexivity | exact (IH a b)]. Qed. + +Lemma ominus_diff : forall a b c d, a + d = c + b -> ominus a b = ominus c d. +Proof. + intros a b c d h. + rewrite <- (ominus_cancel d a b), <- (ominus_cancel b c d). + replace (d + a) with (b + c) by lia. replace (d + b) with (b + d) by lia. reflexivity. +Qed. + +Lemma ominus_self : forall n, ominus n n = pos 0. +Proof. induction n as [|n IH]; [reflexivity | exact IH]. Qed. + +Definition P (z : Z') : nat := match z with pos m => m | negsuc _ => 0 end. +Definition Q (z : Z') : nat := match z with pos _ => 0 | negsuc n => S n end. + +Lemma asDiff : forall z, z = ominus (P z) (Q z). +Proof. intros [m|n]; reflexivity. Qed. + +Lemma ominus_parts : forall a b, P (ominus a b) + b = a + Q (ominus a b). +Proof. + induction a as [|m IH]; intros [|n]; try reflexivity. + change (P (ominus m n) + S n = S m + Q (ominus m n)). + pose proof (IH n). lia. +Qed. + +Lemma add_parts : forall i j, zadd i j = ominus (P i + P j) (Q i + Q j). +Proof. + intros [m|m] [n|n]; simpl. + - reflexivity. + - rewrite Nat.add_0_r. reflexivity. + - rewrite Nat.add_0_r. reflexivity. + - change (negsuc (S (m + n)) = negsuc (m + S n)). f_equal. lia. +Qed. + +Lemma ominus_add : forall a b c d, zadd (ominus a b) (ominus c d) = ominus (a + c) (b + d). +Proof. + intros a b c d. rewrite add_parts. apply ominus_diff. + pose proof (ominus_parts a b). pose proof (ominus_parts c d). lia. +Qed. + +Lemma ord : forall i j, zle i j = leq (P i + Q j) (P j + Q i). +Proof. + intros [m|m] [n|n]; simpl. + - rewrite !Nat.add_0_r. reflexivity. + - rewrite Nat.add_comm. reflexivity. + - reflexivity. + - reflexivity. +Qed. + +Lemma ord_ominus : forall a b c d, zle (ominus a b) (ominus c d) = leq (a + d) (c + b). +Proof. + intros a b c d. rewrite ord, <- (leq_cancel (b + d)). + pose proof (ominus_parts a b). pose proof (ominus_parts c d). + replace (b + d + (P (ominus a b) + Q (ominus c d))) + with (Q (ominus a b) + Q (ominus c d) + (a + d)) by lia. + replace (b + d + (P (ominus c d) + Q (ominus a b))) + with (Q (ominus a b) + Q (ominus c d) + (c + b)) by lia. + apply leq_cancel. +Qed. + +Lemma zadd_comm : forall i j, zadd i j = zadd j i. +Proof. + intros i j. rewrite (add_parts i j), (add_parts j i). + replace (P i + P j) with (P j + P i) by lia. replace (Q i + Q j) with (Q j + Q i) by lia. reflexivity. +Qed. + +Lemma zadd_assoc : forall i j k, zadd (zadd i j) k = zadd i (zadd j k). +Proof. + intros i j k. + rewrite (add_parts i j), (asDiff k), ominus_add, (add_parts j (ominus (P k) (Q k))), <- (asDiff k). + rewrite (asDiff i), ominus_add, <- (asDiff i). + replace (P i + P j + P k) with (P i + (P j + P k)) by lia. + replace (Q i + Q j + Q k) with (Q i + (Q j + Q k)) by lia. reflexivity. +Qed. + +Lemma zadd_zero : forall i, zadd i (pos 0) = i. +Proof. intros [m|m]; simpl; [rewrite Nat.add_0_r|]; reflexivity. Qed. + +Lemma zadd_neg : forall i, zadd i (zneg i) = pos 0. +Proof. intros [[|n]|m]; simpl; [reflexivity | apply ominus_self | apply ominus_self]. Qed. + +Lemma zle_add_same : forall i j k, zle (zadd i k) (zadd j k) = zle i j. +Proof. + intros i j k. rewrite (add_parts i k), (add_parts j k), ord_ominus, (ord i j). + replace (P i + P k + (Q j + Q k)) with (P k + Q k + (P i + Q j)) by lia. + replace (P j + P k + (Q i + Q k)) with (P k + Q k + (P j + Q i)) by lia. + apply leq_cancel. +Qed. + +Lemma zle_refl : forall i, zle i i = true. +Proof. intros [m|m]; apply leq_refl. Qed. + +Lemma zle_trans : forall i j k, zle i j = true -> zle j k = true -> zle i k = true. +Proof. + intros [m|m] [n|n] [k|k] p q; simpl in *; try discriminate; try reflexivity. + - exact (leq_trans m n k p q). + - exact (leq_trans k n m q p). +Qed. + +Lemma zle_total : forall i j, zle i j = false -> zle j i = true. +Proof. + intros [m|m] [n|n] h; simpl in *; try reflexivity; try discriminate. + - exact (leq_total m n h). + - exact (leq_total n m h). +Qed. + +Definition intLaws : Laws intNumber := + mkLaws intNumber zneg zadd_assoc zadd_comm zadd_zero zadd_neg (fun _ _ => eq_refl) + zle_refl zle_trans zle_total (fun i j k h => eq_trans (zle_add_same i j k) h). + +(** APP-2 and APP-3 for the model as it runs on the worked examples. *) + +Lemma cash_identity_int : forall (i : Inputs intNumber) n t p, + lastClosing intNumber p (rowsFrom intNumber i t n p) = + zipWith zadd p (netSum intNumber (rowsFrom intNumber i t n p)). +Proof. intros i n t p. exact (cash_identity intNumber intLaws i n t p). Qed. + +Lemma gap_sound_int : forall (i : Inputs intNumber) n t p u g, + worst intNumber (rowsFrom intNumber i t n p) = given u g -> + Forall' (Met intNumber) (rowsFrom intNumber i t n (vmap (fun x => zadd x g) p)). +Proof. intros i n t p u g e. exact (gap_sound intNumber intLaws i n t p u g e). Qed. + +Lemma gap_least_int : forall (i : Inputs intNumber) n t p u g g', + worst intNumber (rowsFrom intNumber i t n p) = given u g -> zle (pos 0) g' = true -> + Forall' (Met intNumber) (rowsFrom intNumber i t n (vmap (fun x => zadd x g') p)) -> zle g g' = true. +Proof. intros i n t p u g g' e z m. exact (gap_least intNumber intLaws i n t p u g g' e z m). Qed. diff --git a/verification/proofs/coq/MANIFEST b/verification/proofs/coq/MANIFEST index f9e003f..91e3048 100644 --- a/verification/proofs/coq/MANIFEST +++ b/verification/proofs/coq/MANIFEST @@ -2,3 +2,4 @@ # Format: ||gated|quarantine| # Ground-truthed 2026-07-17 with coqc. verification/proofs/coq|FeatureReachability.v|gated| THY-1 Rocq leg, re-proved; prelude only; Print Assumptions: closed +verification/proofs/coq|Cohort.v|gated| APP-1 to APP-4 Rocq leg, re-proved, with the integer laws; stdlib Lia only; Print Assumptions: closed diff --git a/verification/proofs/lean4/Cohort.lean b/verification/proofs/lean4/Cohort.lean new file mode 100644 index 0000000..a0212fd --- /dev/null +++ b/verification/proofs/lean4/Cohort.lean @@ -0,0 +1,945 @@ +/- +SPDX-License-Identifier: MPL-2.0 +Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +APP-1 to APP-4, Lean leg (re-proved by hand), and the integer laws. + +Source of truth: verification/proofs/agda/Applied/ (Cohort, Status, +Missing, Cash, IntNumber, IntLaws). This file restates the same definitions, +clause for clause, and proves the same theorems again; it is not a +translation. docs/status/PROOF-STATUS.adoc records how the statements were +compared. + +Correspondence choices, all mirrored from the Agda source: +- Agda's `_<_` and `_-_` on Nat (Agda.Builtin.Nat) are `natLt` and `monus` + here, with the same clauses; Agda's `if_then_else_` on Bool is `cond`. +- Clauses that overlap in Agda (`meet`, `zipWith`, `kand`, `denominator`) + are listed here case by case: Lean compiles overlapping patterns with + `propext`. Each function is the same, case for case. +- Agda's `n div suc m` is Lean's `n / (m + 1)` (both round down; both give + 0 for a zero divisor). +- Agda's `T b` is `b = true`. Agda's proof-relevant records `Covers` and + `Bounded` are existential propositions here, so that every result is a + theorem that the axiom audit inspects. +- Agda's `All` and `Any` (functions on lists) are `Forall` and `Exists'`. +- The integers are Agda's: `Z` with `pos` and `negsuc`, and the same + operations, not Lean's `Int`, whose core lemmas use `propext`. + +Only Lean core is used: no `import`, no Mathlib, no `simp`, no `omega`. +-/ + +namespace Applied + +/-! ## Natural numbers, as Agda.Builtin.Nat defines them -/ + +/-- Agda.Builtin.Nat `_<_`. It splits on the second argument first, as + Agda's does, so `natLt m 0` reduces to `false` for any m. -/ +def natLt (n m : Nat) : Bool := + match m, n with + | 0, _ => false + | _ + 1, 0 => true + | m + 1, n + 1 => natLt n m +termination_by structural m + +/-- Agda.Builtin.Nat `_-_` (truncated subtraction), split as `natLt` is. -/ +def monus (n m : Nat) : Nat := + match m, n with + | 0, n => n + | _ + 1, 0 => 0 + | m + 1, n + 1 => monus n m +termination_by structural m + +def ndiv (n : Nat) : Nat → Nat + | 0 => 0 + | m + 1 => n / (m + 1) + +def pow (b : Nat) : Nat → Nat + | 0 => 1 + | e + 1 => b * pow b e + +/-! ## Evidence status -/ + +inductive Status + | illustrative | estimate | reported | verified | definitional + +open Status + +def meet : Status → Status → Status + | illustrative, illustrative => illustrative + | illustrative, estimate => illustrative + | illustrative, reported => illustrative + | illustrative, verified => illustrative + | illustrative, definitional => illustrative + | estimate, illustrative => illustrative + | estimate, estimate => estimate + | estimate, reported => estimate + | estimate, verified => estimate + | estimate, definitional => estimate + | reported, illustrative => illustrative + | reported, estimate => estimate + | reported, reported => reported + | reported, verified => reported + | reported, definitional => reported + | verified, illustrative => illustrative + | verified, estimate => estimate + | verified, reported => reported + | verified, verified => verified + | verified, definitional => verified + | definitional, illustrative => illustrative + | definitional, estimate => estimate + | definitional, reported => reported + | definitional, verified => verified + | definitional, definitional => definitional + + +def rank : Status → Nat + | illustrative => 0 + | estimate => 1 + | reported => 2 + | verified => 3 + | definitional => 4 + +def leB : Nat → Nat → Bool + | 0, _ => true + | _ + 1, 0 => false + | m + 1, n + 1 => leB m n + +/-- `stLe s t`: status s is no stronger than status t. -/ +def stLe (s t : Status) : Prop := leB (rank s) (rank t) = true + +theorem leB_refl : ∀ n, leB n n = true + | 0 => rfl + | n + 1 => leB_refl n + +theorem leB_trans : ∀ a b c, leB a b = true → leB b c = true → leB a c = true + | 0, _, _, _, _ => rfl + | _ + 1, 0, _, h, _ => nomatch h + | _ + 1, _ + 1, 0, _, h => nomatch h + | a + 1, b + 1, c + 1, p, q => leB_trans a b c p q + +theorem stLe_refl (s : Status) : stLe s s := leB_refl (rank s) + +theorem stLe_trans (s t u : Status) : stLe s t → stLe t u → stLe s u := + leB_trans (rank s) (rank t) (rank u) + +theorem meet_le_left (s t : Status) : stLe (meet s t) s := by + cases s <;> cases t <;> rfl + +theorem meet_le_right (s t : Status) : stLe (meet s t) t := by + cases s <;> cases t <;> rfl + +theorem meet_assoc (s t u : Status) : meet (meet s t) u = meet s (meet t u) := by + cases s <;> cases t <;> cases u <;> rfl + +theorem meet_definitional (s : Status) : meet s definitional = s := by + cases s <;> rfl + +/-! ## Values that may be missing -/ + +inductive Val (α : Type) + | missing : Val α + | given : Status → α → Val α + +open Val + +def Val.pure {α : Type} (a : α) : Val α := given definitional a + +def Val.map {α β : Type} (f : α → β) : Val α → Val β + | missing => missing + | given s a => given s (f a) + +def zipWith {α β γ : Type} (f : α → β → γ) (x : Val α) (y : Val β) : Val γ := + match x with + | missing => missing + | given s a => + match y with + | missing => missing + | given t b => given (meet s t) (f a b) + +/-- Kleene conjunction: a known `false` decides the result. -/ +def kand (x y : Val Bool) : Val Bool := + match x with + | given s false => given s false + | given s true => + match y with + | given t b => given (meet s t) b + | missing => missing + | missing => + match y with + | given t false => given t false + | given _ true => missing + | missing => missing + +def at' {α : Type} : Nat → List (Val α) → Val α + | _, [] => missing + | 0, x :: _ => x + | n + 1, _ :: xs => at' n xs + +/-! ## Cohorts and rates -/ + +inductive Rate + | perMille : Nat → Rate + | fraction : Nat → Nat → Rate + +inductive Cohort + | observed : Nat → List (Val Nat) → Cohort + | modelled : Nat → Val Nat → Val Rate → Val Rate → Cohort + +open Rate Cohort + +def denominator : Val Rate → Nat + | given _ (fraction _ d) => d + | given _ (perMille _) => 1 + | missing => 1 + +def scaleOf (periods : Nat) : List Cohort → Nat + | [] => 1 + | observed _ _ :: cs => scaleOf periods cs + | modelled _ _ c r :: cs => denominator c * pow (denominator r) periods * scaleOf periods cs + +def applyRate (scale x : Nat) : Rate → Nat + | perMille m => ndiv (ndiv x scale * m) 1000 * scale + | fraction n d => ndiv (x * n) d + +def joined (scale : Nat) (contacts : Val Nat) (conversion : Val Rate) : Val Nat := + zipWith (applyRate scale) (Val.map (fun n => n * scale) contacts) conversion + +def renewed (scale : Nat) (start : Val Nat) (retention : Val Rate) : Nat → Val Nat + | 0 => start + | k + 1 => zipWith (applyRate scale) (renewed scale start retention k) retention + +def cohortAt (scale t : Nat) : Cohort → Val Nat + | observed start counts => + cond (natLt t start) (Val.pure 0) (Val.map (fun n => n * scale) (at' (monus t start) counts)) + | modelled start contacts conversion retention => + cond (natLt t start) (Val.pure 0) (renewed scale (joined scale contacts conversion) retention (monus t start)) + +def sumAt (scale t : Nat) : List Cohort → Val Nat + | [] => Val.pure 0 + | c :: cs => zipWith (· + ·) (cohortAt scale t c) (sumAt scale t cs) + +/-! ## The model -/ + +structure Number where + R : Type + zero : R + add : R → R → R + sub : R → R → R + mul : R → R → R + le : R → R → Bool + fromNat : Nat → R + +section Model + +variable (N : Number) + +def nmax (a b : N.R) : N.R := cond (N.le a b) b a + +structure Inputs where + periods : Nat + opening : Val N.R + price : Val N.R + unitCost : Val N.R + minutes : Val N.R + fixed : List (Val N.R) + floor : List (Val N.R) + capacity : List (Val N.R) + cohorts : List Cohort + +structure Row where + members : Val N.R + receipts : Val N.R + payments : Val N.R + closing : Val N.R + shortfall : Val N.R + hours : Val N.R + cashOk : Val Bool + capacityOk : Val Bool + +variable {N} + +def scale (i : Inputs N) : Nat := scaleOf i.periods i.cohorts + +def scaled (i : Inputs N) : Val N.R → Val N.R := + Val.map (fun x => N.mul x (N.fromNat (scale i))) + +def rowAt (i : Inputs N) (t : Nat) (previous : Val N.R) : Row N := + let m := Val.map N.fromNat (sumAt (scale i) t i.cohorts) + let rec_ := zipWith N.mul i.price m + let pay := zipWith N.add (scaled i (at' (monus t 1) i.fixed)) (zipWith N.mul i.unitCost m) + let clo := zipWith N.sub (zipWith N.add previous rec_) pay + let hrs := zipWith N.mul i.minutes m + let flo := scaled i (at' (monus t 1) i.floor) + { members := m + receipts := rec_ + payments := pay + closing := clo + shortfall := zipWith N.sub flo clo + hours := hrs + cashOk := zipWith N.le flo clo + capacityOk := zipWith N.le hrs (scaled i (at' (monus t 1) i.capacity)) } + +def rowsFrom (i : Inputs N) : Nat → Nat → Val N.R → List (Row N) + | _, 0, _ => [] + | t, n + 1, previous => rowAt i t previous :: rowsFrom i (t + 1) n (rowAt i t previous).closing + +def allRows (i : Inputs N) : List (Row N) := rowsFrom i 1 i.periods (scaled i i.opening) + +def verdict (f : Row N → Val Bool) : List (Row N) → Val Bool + | [] => Val.pure true + | r :: rs => kand (f r) (verdict f rs) + +def worst : List (Row N) → Val N.R + | [] => Val.pure N.zero + | r :: rs => zipWith (nmax N) r.shortfall (worst rs) + +end Model + +/-! ## APP-1 and APP-4: what a given output needs -/ + +/-- `Covers u v`: v is given, with a status at least u. -/ +def Covers {α : Type} (u : Status) (v : Val α) : Prop := + ∃ s a, v = given s a ∧ stLe u s + +def Forall {α : Type} (P : α → Prop) : List α → Prop + | [] => True + | x :: xs => P x ∧ Forall P xs + +def Exists' {α : Type} (P : α → Prop) : List α → Prop + | [] => False + | x :: xs => P x ∨ Exists' P xs + +theorem forall_map {α : Type} {P Q : α → Prop} (f : ∀ x, P x → Q x) : + ∀ xs, Forall P xs → Forall Q xs + | [], _ => True.intro + | x :: xs, ⟨p, ps⟩ => ⟨f x p, forall_map f xs ps⟩ + +theorem covers_weaken {α : Type} {u w : Status} {v : Val α} (le : stLe u w) : + Covers w v → Covers u v + | ⟨s, a, e, le'⟩ => ⟨s, a, e, stLe_trans u w s le le'⟩ + +theorem zipWith_given {α β γ : Type} {f : α → β → γ} : + ∀ {x : Val α} {y : Val β} {u : Status} {c : γ}, + zipWith f x y = given u c → Covers u x ∧ Covers u y + | given s a, given t b, _, _, e => by + cases e + exact ⟨⟨s, a, rfl, meet_le_left s t⟩, ⟨t, b, rfl, meet_le_right s t⟩⟩ + | given _ _, missing, _, _, e => nomatch e + | missing, _, _, _, e => nomatch e + +theorem zipWith_needs {α β γ : Type} {f : α → β → γ} {x : Val α} {y : Val β} {u : Status} + (c : Covers u (zipWith f x y)) : Covers u x ∧ Covers u y := + match c with + | ⟨_, _, e, le⟩ => + match zipWith_given e with + | ⟨cx, cy⟩ => ⟨covers_weaken le cx, covers_weaken le cy⟩ + +theorem map_needs {α β : Type} {f : α → β} : + ∀ {x : Val α} {u : Status}, Covers u (Val.map f x) → Covers u x + | given s a, _, ⟨_, _, e, le⟩ => by + cases e + exact ⟨s, a, rfl, le⟩ + | missing, _, ⟨_, _, e, _⟩ => nomatch e + +theorem missing_uncovered {α : Type} {u : Status} : ¬ Covers u (missing : Val α) + | ⟨_, _, e, _⟩ => nomatch e + +theorem cond_false {α : Type} {b : Bool} {x y : α} (h : b = false) : cond b x y = y := by + cases h; rfl + +theorem joined_needs {u : Status} {scale : Nat} {contacts : Val Nat} {conversion : Val Rate} + (c : Covers u (joined scale contacts conversion)) : Covers u contacts ∧ Covers u conversion := + match zipWith_needs c with + | ⟨cl, cc⟩ => ⟨map_needs cl, cc⟩ + +theorem renewed_joined {u : Status} {scale : Nat} {start : Val Nat} {retention : Val Rate} : + ∀ k, Covers u (renewed scale start retention k) → Covers u start + | 0, c => c + | k + 1, c => renewed_joined k (zipWith_needs c).1 + +theorem renewed_retention {u : Status} {scale : Nat} {start : Val Nat} {retention : Val Rate} + (k : Nat) (c : Covers u (renewed scale start retention (k + 1))) : Covers u retention := + (zipWith_needs c).2 + +theorem modelled_needs {u : Status} {scale t start : Nat} {contacts : Val Nat} + {conversion retention : Val Rate} (h : natLt t start = false) + (c : Covers u (cohortAt scale t (modelled start contacts conversion retention))) : + Covers u contacts ∧ Covers u conversion := by + have e : cohortAt scale t (modelled start contacts conversion retention) = + renewed scale (joined scale contacts conversion) retention (monus t start) := + cond_false h + rw [e] at c + exact joined_needs (renewed_joined _ c) + +theorem modelled_renewal_needs {u : Status} {scale t start : Nat} {contacts : Val Nat} + {conversion retention : Val Rate} (k : Nat) (h : natLt t start = false) + (gap : monus t start = k + 1) + (c : Covers u (cohortAt scale t (modelled start contacts conversion retention))) : + Covers u retention := by + have e : cohortAt scale t (modelled start contacts conversion retention) = + renewed scale (joined scale contacts conversion) retention (monus t start) := + cond_false h + rw [e, gap] at c + exact renewed_retention k c + +theorem observed_needs {u : Status} {scale t start : Nat} {counts : List (Val Nat)} + (h : natLt t start = false) (c : Covers u (cohortAt scale t (observed start counts))) : + Covers u (at' (monus t start) counts) := by + have e : cohortAt scale t (observed start counts) = + Val.map (fun n => n * scale) (at' (monus t start) counts) := + cond_false h + rw [e] at c + exact map_needs c + +theorem sum_needs {u : Status} {scale t : Nat} : + ∀ cs, Covers u (sumAt scale t cs) → Forall (fun c => Covers u (cohortAt scale t c)) cs + | [], _ => True.intro + | _ :: cs, c => ⟨(zipWith_needs c).1, sum_needs cs (zipWith_needs c).2⟩ + +section Needs + +variable {N : Number} (i : Inputs N) + +theorem members_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).members) : Covers u (sumAt (scale i) t i.cohorts) := + map_needs c + +theorem receipts_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).receipts) : + Covers u i.price ∧ Covers u (sumAt (scale i) t i.cohorts) := + match zipWith_needs c with + | ⟨cp, cm⟩ => ⟨cp, map_needs cm⟩ + +theorem payments_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).payments) : + Covers u (at' (monus t 1) i.fixed) ∧ Covers u i.unitCost ∧ Covers u (sumAt (scale i) t i.cohorts) := + match zipWith_needs c with + | ⟨cf, cv⟩ => + match zipWith_needs cv with + | ⟨cu, cm⟩ => ⟨map_needs cf, cu, map_needs cm⟩ + +theorem closing_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).closing) : + Covers u previous ∧ Covers u i.price ∧ Covers u (at' (monus t 1) i.fixed) ∧ + Covers u i.unitCost ∧ Covers u (sumAt (scale i) t i.cohorts) := + match zipWith_needs c with + | ⟨cpr, cpay⟩ => + match zipWith_needs cpr, payments_needs i t previous cpay with + | ⟨cprev, crec⟩, ⟨cf, cu, cm⟩ => ⟨cprev, (zipWith_needs crec).1, cf, cu, cm⟩ + +theorem shortfall_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).shortfall) : + Covers u (at' (monus t 1) i.floor) ∧ Covers u (rowAt i t previous).closing := + match zipWith_needs c with + | ⟨cfl, cc⟩ => ⟨map_needs cfl, cc⟩ + +theorem cashOk_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).cashOk) : + Covers u (at' (monus t 1) i.floor) ∧ Covers u (rowAt i t previous).closing := + match zipWith_needs c with + | ⟨cfl, cc⟩ => ⟨map_needs cfl, cc⟩ + +theorem hours_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).hours) : + Covers u i.minutes ∧ Covers u (sumAt (scale i) t i.cohorts) := + match zipWith_needs c with + | ⟨cmin, cm⟩ => ⟨cmin, map_needs cm⟩ + +theorem capacityOk_needs {u : Status} (t : Nat) (previous : Val N.R) + (c : Covers u (rowAt i t previous).capacityOk) : + Covers u i.minutes ∧ Covers u (sumAt (scale i) t i.cohorts) ∧ Covers u (at' (monus t 1) i.capacity) := + match zipWith_needs c with + | ⟨ch, ccap⟩ => + match hours_needs i t previous ch with + | ⟨cmin, cm⟩ => ⟨cmin, cm, map_needs ccap⟩ + +theorem opening_needs {u : Status} (c : Covers u (scaled i i.opening)) : Covers u i.opening := + map_needs c + +theorem closings_missing : ∀ t n, Forall (fun r : Row N => r.closing = missing) (rowsFrom i t n missing) + | _, 0 => True.intro + | t, n + 1 => ⟨rfl, closings_missing (t + 1) n⟩ + +theorem missing_persists (t n : Nat) (previous : Val N.R) (h : (rowAt i t previous).closing = missing) : + Forall (fun r : Row N => r.closing = missing) (rowsFrom i (t + 1) n (rowAt i t previous).closing) := by + rw [h] + exact closings_missing i (t + 1) n + +/-- A "yes" needs both sides to be a known "yes". -/ +def Yes (u : Status) (v : Val Bool) : Prop := ∃ s, v = given s true ∧ stLe u s + +theorem kand_yes : ∀ {x y : Val Bool} {u : Status}, kand x y = given u true → Yes u x ∧ Yes u y + | given s true, given t b, _, e => by + cases e + exact ⟨⟨s, rfl, meet_le_left s t⟩, ⟨t, rfl, meet_le_right s t⟩⟩ + | given _ true, missing, _, e => nomatch e + | given _ false, _, _, e => nomatch e + | missing, given _ false, _, e => nomatch e + | missing, given _ true, _, e => nomatch e + | missing, missing, _, e => nomatch e + +theorem verdict_yes {u : Status} (f : Row N → Val Bool) : + ∀ rs, verdict f rs = given u true → Forall (fun r => Yes u (f r)) rs + | [], _ => True.intro + | _ :: rs, e => + match kand_yes e with + | ⟨yr, ⟨s, e', le⟩⟩ => + ⟨yr, forall_map (fun _ ⟨s', ex, le'⟩ => ⟨s', ex, stLe_trans u s s' le le'⟩) rs (verdict_yes f rs e')⟩ + +theorem kand_false_left : ∀ {x y : Val Bool} {s : Status}, x = given s false → kand x y = given s false + | _, _, _, rfl => rfl + +theorem kand_false_right : ∀ {x y : Val Bool} {t : Status}, y = given t false → + ∃ u, kand x y = given u false + | given s false, _, _, rfl => ⟨s, rfl⟩ + | given s true, _, t, rfl => ⟨meet s t, rfl⟩ + | missing, _, t, rfl => ⟨t, rfl⟩ + +theorem breach_decides (f : Row N → Val Bool) : + ∀ rs, Exists' (fun r => ∃ s, f r = given s false) rs → ∃ u, verdict f rs = given u false + | [], h => nomatch h + | _ :: _, Or.inl ⟨s, e⟩ => ⟨s, kand_false_left e⟩ + | _ :: rs, Or.inr p => + match breach_decides f rs p with + | ⟨_, e⟩ => kand_false_right e + +theorem gap_needs {u : Status} : ∀ rs : List (Row N), Covers u (worst rs) → + Forall (fun r => Covers u r.shortfall) rs + | [], _ => True.intro + | _ :: rs, c => ⟨(zipWith_needs c).1, gap_needs rs (zipWith_needs c).2⟩ + +end Needs + + +/-! ## APP-2 and APP-3: ordered abelian groups -/ + +structure Laws (N : Number) where + neg : N.R → N.R + add_assoc : ∀ a b c, N.add (N.add a b) c = N.add a (N.add b c) + add_comm : ∀ a b, N.add a b = N.add b a + add_zero : ∀ a, N.add a N.zero = a + add_neg : ∀ a, N.add a (neg a) = N.zero + sub_def : ∀ a b, N.sub a b = N.add a (neg b) + le_refl : ∀ a, N.le a a = true + le_trans : ∀ a b c, N.le a b = true → N.le b c = true → N.le a c = true + le_total : ∀ a b, N.le a b = false → N.le b a = true + le_add : ∀ a b c, N.le a b = true → N.le (N.add a c) (N.add b c) = true + +section Cash + +variable {N : Number} (L : Laws N) +include L + +theorem step_law (a r q x : N.R) : + N.add (N.sub (N.add a r) q) x = N.add a (N.add (N.sub r q) x) := by + rw [L.sub_def, L.sub_def, L.add_assoc a r (L.neg q), L.add_assoc a (N.add r (L.neg q)) x] + +theorem shift_law (a g r q : N.R) : + N.sub (N.add (N.add a g) r) q = N.add (N.sub (N.add a r) q) g := by + rw [L.sub_def, L.sub_def, L.add_assoc a g r, L.add_comm g r, ← L.add_assoc a r g, + L.add_assoc (N.add a r) g (L.neg q), L.add_comm g (L.neg q), ← L.add_assoc (N.add a r) (L.neg q) g] + +theorem cancel_right (f c : N.R) : N.add (N.sub f c) c = f := by + rw [L.sub_def, L.add_assoc, L.add_comm (L.neg c) c, L.add_neg, L.add_zero] + +theorem cancel_left (c g : N.R) : N.add (N.add c g) (L.neg c) = g := by + rw [L.add_comm c g, L.add_assoc, L.add_neg, L.add_zero] + +/-- f − c ≤ g gives f ≤ c + g. -/ +theorem below_shift (f c g : N.R) (h : N.le (N.sub f c) g = true) : N.le f (N.add c g) = true := by + have k := L.le_add _ _ c h + rw [cancel_right L, L.add_comm g c] at k + exact k + +/-- f ≤ c + g gives f − c ≤ g. -/ +theorem shift_below (f c g : N.R) (h : N.le f (N.add c g) = true) : N.le (N.sub f c) g = true := by + have k := L.le_add _ _ (L.neg c) h + rw [cancel_left L, ← L.sub_def] at k + exact k + +omit L in +theorem meet4 (s t v w : Status) : meet (meet (meet s t) v) w = meet s (meet (meet t v) w) := by + rw [meet_assoc (meet s t) v w, meet_assoc s t (meet v w), meet_assoc t v w] + +theorem step_val : ∀ p r q n : Val N.R, + zipWith N.add (zipWith N.sub (zipWith N.add p r) q) n = + zipWith N.add p (zipWith N.add (zipWith N.sub r q) n) + | given s a, given t b, given v c, given w d => by + show given (meet (meet (meet s t) v) w) (N.add (N.sub (N.add a b) c) d) = + given (meet s (meet (meet t v) w)) (N.add a (N.add (N.sub b c) d)) + rw [meet4, step_law L] + | missing, _, _, _ => rfl + | given _ _, missing, _, _ => rfl + | given _ _, given _ _, missing, _ => rfl + | given _ _, given _ _, given _ _, missing => rfl + +theorem base_val : ∀ p : Val N.R, p = zipWith N.add p (Val.pure N.zero) + | missing => rfl + | given s a => by + show given s a = given (meet s definitional) (N.add a N.zero) + rw [meet_definitional, L.add_zero] + +theorem shift_val : ∀ (p r q : Val N.R) (g : N.R), + zipWith N.sub (zipWith N.add (Val.map (fun x => N.add x g) p) r) q = + Val.map (fun x => N.add x g) (zipWith N.sub (zipWith N.add p r) q) + | given s a, given t b, given v c, g => by + show given (meet (meet s t) v) (N.sub (N.add (N.add a g) b) c) = + given (meet (meet s t) v) (N.add (N.sub (N.add a b) c) g) + rw [shift_law L] + | missing, _, _, _ => rfl + | given _ _, missing, _, _ => rfl + | given _ _, given _ _, missing, _ => rfl + +theorem floor_met : ∀ (F C : Val N.R) (g : N.R) {s : Status} {d : N.R}, + zipWith N.sub F C = given s d → N.le d g = true → + ∃ s', zipWith N.le F (Val.map (fun x => N.add x g) C) = given s' true + | given sf f, given sc c, g, _, _, e, h => by + cases e + exact ⟨meet sf sc, congrArg (given (meet sf sc)) (below_shift L f c g h)⟩ + | given _ _, missing, _, _, _, e, _ => nomatch e + | missing, _, _, _, _, e, _ => nomatch e + +theorem floor_needs : ∀ (F C : Val N.R) (g : N.R) {s s' : Status} {d : N.R}, + zipWith N.sub F C = given s d → + zipWith N.le F (Val.map (fun x => N.add x g) C) = given s' true → N.le d g = true + | given sf f, given sc c, g, _, _, _, e, ok => by + cases e + injection ok with _ h + exact shift_below L f c g h + | given _ _, missing, _, _, _, _, e, _ => nomatch e + | missing, _, _, _, _, _, e, _ => nomatch e + +theorem max_left (a b : N.R) : N.le a (nmax N a b) = true := by + show N.le a (cond (N.le a b) b a) = true + cases h : N.le a b + · exact L.le_refl a + · exact h + +theorem max_right (a b : N.R) : N.le b (nmax N a b) = true := by + show N.le b (cond (N.le a b) b a) = true + cases h : N.le a b + · exact L.le_total a b h + · exact L.le_refl b + +omit L in +theorem max_least (a b c : N.R) (ha : N.le a c = true) (hb : N.le b c = true) : + N.le (nmax N a b) c = true := by + show N.le (cond (N.le a b) b a) c = true + cases N.le a b + · exact ha + · exact hb + +variable (i : Inputs N) + +omit L in +def lastClosing : Val N.R → List (Row N) → Val N.R + | p, [] => p + | _, r :: rs => lastClosing r.closing rs + +omit L in +def netSum : List (Row N) → Val N.R + | [] => Val.pure N.zero + | r :: rs => zipWith N.add (zipWith N.sub r.receipts r.payments) (netSum rs) + +/-- APP-2: the closing cash of the last period is the opening cash plus, + summed over the periods, receipts minus payments. Both sides are + missing together, with the same status when given. -/ +theorem cash_identity : ∀ (t n : Nat) (p : Val N.R), + lastClosing p (rowsFrom i t n p) = zipWith N.add p (netSum (rowsFrom i t n p)) + | _, 0, p => base_val L p + | t, n + 1, p => + (cash_identity (t + 1) n (rowAt i t p).closing).trans + (step_val L p (rowAt i t p).receipts (rowAt i t p).payments + (netSum (rowsFrom i (t + 1) n (rowAt i t p).closing))) + +/-- Adding g to the previous balance adds g to the closing balance. -/ +theorem shifted_closing (t : Nat) (p : Val N.R) (g : N.R) : + (rowAt i t (Val.map (fun x => N.add x g) p)).closing = + Val.map (fun x => N.add x g) (rowAt i t p).closing := + shift_val L p (rowAt i t p).receipts (rowAt i t p).payments g + +omit L in +/-- A shortfall bounded by g. -/ +def Bounded (g : N.R) (v : Val N.R) : Prop := ∃ s d, v = given s d ∧ N.le d g = true + +omit L in +/-- The floor holds in a row. -/ +def Met (r : Row N) : Prop := ∃ s, r.cashOk = given s true + +theorem worst_bounds : ∀ (rs : List (Row N)) {u : Status} {g : N.R}, + worst rs = given u g → Forall (fun r => Bounded g r.shortfall) rs + | [], _, _, _ => True.intro + | r :: rs, _, g, e => + match zipWith_given e with + | ⟨⟨s, d, eqd, _⟩, ⟨w, m, eqm, _⟩⟩ => by + have e' : zipWith (nmax N) r.shortfall (worst rs) = given _ g := e + rw [eqd, eqm] at e' + injection e' with _ hg + refine ⟨⟨s, d, eqd, ?_⟩, forall_map (fun _ ⟨s', d', e2, t2⟩ => ⟨s', d', e2, ?_⟩) rs (worst_bounds rs eqm)⟩ + · rw [← hg]; exact max_left L d m + · exact L.le_trans d' m g t2 (by rw [← hg]; exact max_right L d m) + +/-- APP-3, sound: when every shortfall is at most g, adding g to the + previous balance meets the floor in every period. -/ +theorem meets_floor : ∀ (t n : Nat) (p : Val N.R) (g : N.R), + Forall (fun r => Bounded g r.shortfall) (rowsFrom i t n p) → + Forall Met (rowsFrom i t n (Val.map (fun x => N.add x g) p)) + | _, 0, _, _, _ => True.intro + | t, n + 1, p, g, ⟨⟨_, _, eq, le⟩, rest⟩ => by + have hc := shifted_closing L i t p g + refine ⟨?_, ?_⟩ + · show ∃ s', zipWith N.le (scaled i (at' (monus t 1) i.floor)) + (rowAt i t (Val.map (fun x => N.add x g) p)).closing = given s' true + rw [hc] + exact floor_met L (scaled i (at' (monus t 1) i.floor)) (rowAt i t p).closing g eq le + · show Forall Met (rowsFrom i (t + 1) n (rowAt i t (Val.map (fun x => N.add x g) p)).closing) + rw [hc] + exact meets_floor (t + 1) n (rowAt i t p).closing g rest + +theorem gap_sound (t n : Nat) (p : Val N.R) {u : Status} {g : N.R} + (e : worst (rowsFrom i t n p) = given u g) : + Forall Met (rowsFrom i t n (Val.map (fun x => N.add x g) p)) := + meets_floor L i t n p g (worst_bounds L _ e) + +/-- APP-3, least: no smaller non-negative addition meets every floor. -/ +theorem gap_least : ∀ (t n : Nat) (p : Val N.R) {u : Status} {g : N.R} (g' : N.R), + worst (rowsFrom i t n p) = given u g → N.le N.zero g' = true → + Forall Met (rowsFrom i t n (Val.map (fun x => N.add x g') p)) → N.le g g' = true + | _, 0, _, _, _, _, e, z, _ => by + injection e with _ hg + rw [← hg]; exact z + | t, n + 1, p, _, g, g', e, z, ⟨⟨s', ok⟩, rest⟩ => + match zipWith_given e with + | ⟨⟨_, d, eqd, _⟩, ⟨_, m, eqm, _⟩⟩ => by + have e' : zipWith (nmax N) (rowAt i t p).shortfall + (worst (rowsFrom i (t + 1) n (rowAt i t p).closing)) = given _ g := e + rw [eqd, eqm] at e' + injection e' with _ hg + have ok' : zipWith N.le (scaled i (at' (monus t 1) i.floor)) + (Val.map (fun x => N.add x g') (rowAt i t p).closing) = given s' true := by + rw [← shifted_closing L i t p g']; exact ok + have head := floor_needs L (scaled i (at' (monus t 1) i.floor)) (rowAt i t p).closing g' eqd ok' + have rest' : Forall Met (rowsFrom i (t + 1) n (Val.map (fun x => N.add x g') (rowAt i t p).closing)) := by + rw [← shifted_closing L i t p g']; exact rest + have tail := gap_least (t + 1) n (rowAt i t p).closing g' eqm z rest' + rw [← hg] + exact max_least d m g' head tail + +end Cash + + +/-! ## The integer instance satisfies the laws -/ + +inductive Z + | pos : Nat → Z + | negsuc : Nat → Z + +open Z + +def ominus (m n : Nat) : Z := cond (natLt m n) (negsuc (monus (monus n m) 1)) (pos (monus m n)) + +def zneg : Z → Z + | pos 0 => pos 0 + | pos (n + 1) => negsuc n + | negsuc n => pos (n + 1) + +def zadd : Z → Z → Z + | pos m, pos n => pos (m + n) + | pos m, negsuc n => ominus m (n + 1) + | negsuc m, pos n => ominus n (m + 1) + | negsuc m, negsuc n => negsuc (m + n + 1) + +def zsub (a b : Z) : Z := zadd a (zneg b) + +def zmul : Z → Z → Z + | pos m, pos n => pos (m * n) + | pos m, negsuc n => zneg (pos (m * (n + 1))) + | negsuc m, pos n => zneg (pos ((m + 1) * n)) + | negsuc m, negsuc n => pos ((m + 1) * (n + 1)) + +def zle : Z → Z → Bool + | pos m, pos n => natLt m (n + 1) + | pos _, negsuc _ => false + | negsuc _, pos _ => true + | negsuc m, negsuc n => natLt n (m + 1) + +def intNumber : Number := + { R := Z, zero := pos 0, add := zadd, sub := zsub, mul := zmul, le := zle, fromNat := pos } + +/-- m ≤ n, as the integer order uses it. -/ +def leq (m n : Nat) : Bool := natLt m (n + 1) + +theorem leq_refl : ∀ n, leq n n = true + | 0 => rfl + | n + 1 => leq_refl n + +theorem leq_trans : ∀ a b c, leq a b = true → leq b c = true → leq a c = true + | 0, _, _, _, _ => rfl + | _ + 1, 0, _, h, _ => nomatch h + | _ + 1, _ + 1, 0, _, h => nomatch h + | a + 1, b + 1, c + 1, p, q => leq_trans a b c p q + +theorem leq_total : ∀ a b, leq a b = false → leq b a = true + | 0, _, h => nomatch h + | _ + 1, 0, _ => rfl + | a + 1, b + 1, h => leq_total a b h + +theorem leq_cancel_right : ∀ k x y, leq (x + k) (y + k) = leq x y + | 0, _, _ => rfl + | k + 1, x, y => leq_cancel_right k x y + +theorem leq_cancel (k x y : Nat) : leq (k + x) (k + y) = leq x y := by + rw [Nat.add_comm k x, Nat.add_comm k y] + exact leq_cancel_right k x y + +/-- (w + x) + (y + z) = (w + y) + (x + z) -/ +theorem swap (w x y z : Nat) : (w + x) + (y + z) = (w + y) + (x + z) := by + rw [Nat.add_assoc w x (y + z), Nat.add_left_comm x y z, ← Nat.add_assoc w y (x + z)] + +theorem ominus_cancel_right : ∀ k a b, ominus (a + k) (b + k) = ominus a b + | 0, _, _ => rfl + | k + 1, a, b => ominus_cancel_right k a b + +theorem ominus_diff (a b c d : Nat) (h : a + d = c + b) : ominus a b = ominus c d := by + rw [← ominus_cancel_right d a b, h, Nat.add_comm b d, ominus_cancel_right b c d] + +theorem ominus_self : ∀ n, ominus n n = pos 0 + | 0 => rfl + | n + 1 => ominus_self n + +def P : Z → Nat + | pos m => m + | negsuc _ => 0 + +def Q : Z → Nat + | pos _ => 0 + | negsuc n => n + 1 + +theorem asDiff : ∀ i, i = ominus (P i) (Q i) + | pos _ => rfl + | negsuc _ => rfl + +theorem ominus_parts : ∀ a b, P (ominus a b) + b = a + Q (ominus a b) + | 0, 0 => rfl + | _ + 1, 0 => rfl + | 0, _ + 1 => rfl + | m + 1, n + 1 => by + show P (ominus m n) + n + 1 = m + 1 + Q (ominus m n) + rw [ominus_parts m n, Nat.add_right_comm m 1 (Q (ominus m n))] + +theorem add_parts : ∀ i j, zadd i j = ominus (P i + P j) (Q i + Q j) + | pos _, pos _ => rfl + | pos m, negsuc n => by + show ominus m (n + 1) = ominus m (0 + (n + 1)) + rw [Nat.zero_add] + | negsuc m, pos n => by + show ominus n (m + 1) = ominus (0 + n) (m + 1) + rw [Nat.zero_add] + | negsuc m, negsuc n => by + show negsuc (m + n + 1) = negsuc (m + 1 + n) + rw [Nat.add_right_comm m 1 n] + +theorem ominus_add (a b c d : Nat) : zadd (ominus a b) (ominus c d) = ominus (a + c) (b + d) := by + rw [add_parts] + apply ominus_diff + rw [swap, ominus_parts a b, ominus_parts c d, swap a (Q (ominus a b)) c (Q (ominus c d))] + +theorem ord : ∀ i j, zle i j = leq (P i + Q j) (P j + Q i) + | pos _, pos _ => rfl + | pos _, negsuc _ => rfl + | negsuc _, pos _ => rfl + | negsuc m, negsuc n => by + show natLt n (m + 1) = leq (0 + (n + 1)) (0 + (m + 1)) + rw [Nat.zero_add, Nat.zero_add] + rfl + +theorem ord_ominus (a b c d : Nat) : zle (ominus a b) (ominus c d) = leq (a + d) (c + b) := by + rw [ord, ← leq_cancel (b + d)] + have left : b + d + (P (ominus a b) + Q (ominus c d)) = + Q (ominus a b) + Q (ominus c d) + (a + d) := by + rw [Nat.add_comm (b + d), swap (P (ominus a b)) (Q (ominus c d)) b d, ominus_parts a b, + Nat.add_comm a (Q (ominus a b)), swap (Q (ominus a b)) a (Q (ominus c d)) d] + have right : b + d + (P (ominus c d) + Q (ominus a b)) = + Q (ominus a b) + Q (ominus c d) + (c + b) := by + rw [Nat.add_comm (b + d), swap (P (ominus c d)) (Q (ominus a b)) b d, + Nat.add_comm (Q (ominus a b)) d, swap (P (ominus c d)) b d (Q (ominus a b)), ominus_parts c d, + swap c (Q (ominus c d)) b (Q (ominus a b)), Nat.add_comm (c + b), + Nat.add_comm (Q (ominus c d)) (Q (ominus a b))] + rw [left, right, leq_cancel] + +theorem zadd_comm (i j : Z) : zadd i j = zadd j i := by + rw [add_parts i j, add_parts j i, Nat.add_comm (P i), Nat.add_comm (Q i)] + +theorem zadd_assoc (i j k : Z) : zadd (zadd i j) k = zadd i (zadd j k) := + calc zadd (zadd i j) k + = zadd (ominus (P i + P j) (Q i + Q j)) (ominus (P k) (Q k)) := by + rw [add_parts i j, ← asDiff k] + _ = ominus (P i + P j + P k) (Q i + Q j + Q k) := ominus_add _ _ _ _ + _ = ominus (P i + (P j + P k)) (Q i + (Q j + Q k)) := by + rw [Nat.add_assoc (P i), Nat.add_assoc (Q i)] + _ = zadd (ominus (P i) (Q i)) (ominus (P j + P k) (Q j + Q k)) := (ominus_add _ _ _ _).symm + _ = zadd i (zadd j k) := by rw [← asDiff i, ← add_parts j k] + +theorem zadd_zero : ∀ i, zadd i (pos 0) = i + | pos _ => rfl + | negsuc _ => rfl + +theorem zadd_neg : ∀ i, zadd i (zneg i) = pos 0 + | pos 0 => rfl + | pos (n + 1) => ominus_self n + | negsuc m => ominus_self m + +theorem zle_add_same (i j k : Z) : zle (zadd i k) (zadd j k) = zle i j := by + rw [add_parts i k, add_parts j k, ord_ominus, ord i j] + have r : ∀ a k b l, a + k + (b + l) = k + l + (a + b) := fun a k b l => by + rw [swap, Nat.add_comm] + rw [r (P i) (P k) (Q j) (Q k), r (P j) (P k) (Q i) (Q k), leq_cancel] + +theorem zle_refl : ∀ i, zle i i = true + | pos m => leq_refl m + | negsuc m => leq_refl m + +theorem zle_trans : ∀ i j k, zle i j = true → zle j k = true → zle i k = true + | pos m, pos n, pos k, p, q => leq_trans m n k p q + | pos _, pos _, negsuc _, _, q => nomatch q + | pos _, negsuc _, _, p, _ => nomatch p + | negsuc _, pos _, pos _, _, _ => rfl + | negsuc _, negsuc _, pos _, _, _ => rfl + | negsuc _, pos _, negsuc _, _, q => nomatch q + | negsuc m, negsuc n, negsuc k, p, q => leq_trans k n m q p + +theorem zle_total : ∀ i j, zle i j = false → zle j i = true + | pos m, pos n, h => leq_total m n h + | pos _, negsuc _, _ => rfl + | negsuc _, pos _, h => nomatch h + | negsuc m, negsuc n, h => leq_total n m h + +def intLaws : Laws intNumber := + { neg := zneg + add_assoc := zadd_assoc + add_comm := zadd_comm + add_zero := zadd_zero + add_neg := zadd_neg + sub_def := fun _ _ => rfl + le_refl := zle_refl + le_trans := zle_trans + le_total := zle_total + le_add := fun i j k h => (zle_add_same i j k).trans h } + +/-! APP-2 and APP-3 for the model as it runs on the worked examples. -/ + +theorem cash_identity_int (i : Inputs intNumber) (t n : Nat) (p : Val Z) : + lastClosing p (rowsFrom i t n p) = zipWith zadd p (netSum (rowsFrom i t n p)) := + cash_identity intLaws i t n p + +theorem gap_sound_int (i : Inputs intNumber) (t n : Nat) (p : Val Z) {u : Status} {g : Z} + (e : worst (rowsFrom i t n p) = given u g) : + Forall Met (rowsFrom i t n (Val.map (fun x => zadd x g) p)) := + gap_sound intLaws i t n p e + +theorem gap_least_int (i : Inputs intNumber) (t n : Nat) (p : Val Z) {u : Status} {g : Z} (g' : Z) + (e : worst (rowsFrom i t n p) = given u g) (z : zle (pos 0) g' = true) + (m : Forall Met (rowsFrom i t n (Val.map (fun x => zadd x g') p))) : zle g g' = true := + gap_least intLaws i t n p g' e z m + +end Applied diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST index aa66f7a..cc5da5e 100644 --- a/verification/proofs/lean4/MANIFEST +++ b/verification/proofs/lean4/MANIFEST @@ -2,3 +2,4 @@ # Format: ||gated|quarantine| # Ground-truthed 2026-07-17 with Lean leanprover/lean4:v4.15.0 (via elan). verification/proofs/lean4|FeatureReachability.lean|gated| THY-1 Lean leg, re-proved; core only; #print axioms: none +verification/proofs/lean4|Cohort.lean|gated| APP-1 to APP-4 Lean leg, re-proved, with the integer laws; core only; no axiom