From 5534fdd8d1e41b56faae82551a903d66ca824438 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 11 Nov 2026 01:12:25 +0000 Subject: [PATCH] docs(wager): Stage 8, 3 corrections from review - Poly/Statements.agda: the comment of T8-Closed said that T0 to T6 apply to each closed instance. That was too strong. The comment now follows DC-8.3. The statement did not change. - Poly/Proofs.agda: the header names each proof of the module. - TOOLCHAIN.adoc: the last row of the gate watch of Stage 8 records the run with 91 files only. scripts/check-proofs.sh agda: PASS, 96 modules. Co-Authored-By: Claude --- verification/proofs/agda/Wager/Poly/Proofs.agda | 4 +++- verification/proofs/agda/Wager/Poly/Statements.agda | 7 +++++-- verification/proofs/agda/Wager/TOOLCHAIN.adoc | 2 +- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/verification/proofs/agda/Wager/Poly/Proofs.agda b/verification/proofs/agda/Wager/Poly/Proofs.agda index 7ffc7ff..1dd17b8 100644 --- a/verification/proofs/agda/Wager/Poly/Proofs.agda +++ b/verification/proofs/agda/Wager/Poly/Proofs.agda @@ -4,7 +4,9 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- --- Stage 8. Proofs of T8-Conv, T8-Inst and T8-Closed. +-- Stage 8. Proofs of T8-Conv, T8-Inst, T8-Closed, T8-Closed-Instance, +-- T8-Instance-Progress and T8-Instance-Preservation. The lemmas `sub-⇑` +-- and `⇑-closed` are also used by `Wager.Poly.CoercionProofs`. open import Wager.L1.Signature open import Wager.Grade.Algebra import Wager.L2.Signature diff --git a/verification/proofs/agda/Wager/Poly/Statements.agda b/verification/proofs/agda/Wager/Poly/Statements.agda index 4a63f38..1e07b94 100644 --- a/verification/proofs/agda/Wager/Poly/Statements.agda +++ b/verification/proofs/agda/Wager/Poly/Statements.agda @@ -34,8 +34,11 @@ T8-Inst = ∀ {Δ Δ' n} (σ : TySub Δ' Δ) {γ : Usage n} {Γ : Cxᵖ Δ n} γ ▸ (λ i → sub σ (Γ i)) ⊢ᵖ inst σ t ∶ sub σ A -- T8-Closed. A typed term with no type variable is a typed term of the --- target calculus of stages 1 to 5. So T0 to T6 apply to each closed --- instance of an open term. +-- target calculus of stages 1 to 5. A theorem about each typed target +-- term, such as T0, thus applies to each closed instance of an open +-- term, under its own hypotheses. T3, T5 and T6 are about the +-- translation of a source program, and T2 and T4 are about types +-- (DESIGN-CHOICES.adoc, DC-8.3). The statement below did not change. T8-Closed : Type T8-Closed = ∀ {n} {γ : Usage n} {Γ : Cxᵖ [] n} {t : Tmᵖ [] n} {A : Ty [] ★} → γ ▸ Γ ⊢ᵖ t ∶ A → γ ▸ Γ ⊢ ⌊ t ⌋ ∶ A diff --git a/verification/proofs/agda/Wager/TOOLCHAIN.adoc b/verification/proofs/agda/Wager/TOOLCHAIN.adoc index 3846cb5..ac85487 100644 --- a/verification/proofs/agda/Wager/TOOLCHAIN.adoc +++ b/verification/proofs/agda/Wager/TOOLCHAIN.adoc @@ -483,7 +483,7 @@ Each row is one change, alone. After each change the 2 commands `agda --safe Wag | All changes removed | None -| PASS. The gate passed with 91 files before the watch. After the watch it ran with the 5 files of the side item: PASS, 96 files. +| PASS, 91 files. This run was before the watch. The run after the watch had the 5 files of the side item also: see the last row of the next table. |=== The second and the third test show that the proof of `T8-Closed` depends on the map `⌊_⌋` and on the text of a rule.