Skip to content

docs(wager): Stage 8, 3 corrections from the review of #101 #102

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Nov 11, 2026
Merged

docs(wager): Stage 8, 3 corrections from the review of #101 #102

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion verification/proofs/agda/Wager/Poly/Proofs.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@
-- SPDX-License-Identifier: MPL-2.0
-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
--
-- 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
Expand Down
7 changes: 5 additions & 2 deletions verification/proofs/agda/Wager/Poly/Statements.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion verification/proofs/agda/Wager/TOOLCHAIN.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading