Skip to content

Commit 7fa39cd

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
fix(formal/agda): make the intrinsic-typing formalization check under --safe --without-K
The Agda formalization never typechecked. Fixes: - Ctx's `_,_` clashed with Data.Product `_,_` (AmbiguousParseForApplication at the context-extension sites) -> renamed to `_,,_`. - Two `Data.Integer` imports listed names in both `using` and `renaming` (RepeatedNamesInImportDirective) and re-imported `_+_`, clashing with Data.Nat -> kept only the renamings. - `_≟ᵗ_` (decidable type equality) was UNSOUND: it omitted the TRecord case and used a single `_ ≟ᵗ _ = no (λ ())` catch-all, which --safe rejects ([ShouldBeEmpty]) since `TRecord fs ≡ TRecord gs` is inhabited by refl. Rewritten as a mutual decision with `_≟ᶠ_` over the field list; every same-head case is handled and the distinct-head pairs are enumerated. - `_<ᵛ_` parsed as `a ≤ᵇ (b ∧ …)` (fixity) and used `_≡ᵛ_` at an ambiguous type index -> parenthesised and indexed at TInt. - Added `{-# OPTIONS --safe --without-K #-}`. `agda Phronesis.agda` now exits 0 under --safe --without-K (no postulates, no holes, termination + positivity checked), so the intrinsic-typing "type safety is automatic" and "eval is total" claims now genuinely hold. SPDX header unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 174ecfd commit 7fa39cd

1 file changed

Lines changed: 122 additions & 25 deletions

File tree

‎academic/formal-verification/agda/Phronesis.agda‎

Lines changed: 122 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
-- Phronesis Formalization in Agda
33
-- Intrinsically typed representation with dependent types
44

5+
{-# OPTIONS --safe --without-K #-}
6+
57
module Phronesis where
68

79
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_)
@@ -35,20 +37,115 @@ data PhrType : Set where
3537
-- 2. Type Equality Decidability
3638
-- ═══════════════════════════════════════════════════════════════════════════
3739

38-
-- Decidable equality for types (needed for type checking)
39-
_≟ᵗ_ : (τ₁ τ₂ : PhrType) → Dec (τ₁ ≡ τ₂)
40-
TInt ≟ᵗ TInt = yes refl
41-
TBool ≟ᵗ TBool = yes refl
42-
TString ≟ᵗ TString = yes refl
43-
TNull ≟ᵗ TNull = yes refl
44-
TFloat ≟ᵗ TFloat = yes refl
45-
TIP ≟ᵗ TIP = yes refl
46-
TDateTime ≟ᵗ TDateTime = yes refl
47-
TList τ₁ ≟ᵗ TList τ₂ with τ₁ ≟ᵗ τ₂
48-
... | yes refl = yes refl
49-
... | no ¬p = no (λ { refl → ¬p refl })
50-
-- ... other cases omitted for brevity
51-
_ ≟ᵗ _ = no (λ ())
40+
-- Decidable equality for types (needed for type checking).
41+
--
42+
-- TRecord nests through List (String × PhrType), so the field list is decided
43+
-- mutually (_≟ᶠ_). EVERY same-head case — including TRecord — is handled
44+
-- explicitly *above* the final catch-all, so the catch-all covers only
45+
-- distinct-head pairs and `no (λ ())` is sound. (The previous version omitted
46+
-- the TRecord case, which made the catch-all unsound: `TRecord fs ≡ TRecord gs`
47+
-- is inhabited by `refl`, so `λ ()` did not typecheck under --safe.)
48+
mutual
49+
_≟ᵗ_ : (τ₁ τ₂ : PhrType) → Dec (τ₁ ≡ τ₂)
50+
TInt ≟ᵗ TInt = yes refl
51+
TBool ≟ᵗ TBool = yes refl
52+
TString ≟ᵗ TString = yes refl
53+
TNull ≟ᵗ TNull = yes refl
54+
TFloat ≟ᵗ TFloat = yes refl
55+
TIP ≟ᵗ TIP = yes refl
56+
TDateTime ≟ᵗ TDateTime = yes refl
57+
TList τ₁ ≟ᵗ TList τ₂ with τ₁ ≟ᵗ τ₂
58+
... | yes refl = yes refl
59+
... | no ¬p = no (λ { refl → ¬p refl })
60+
TRecord fs ≟ᵗ TRecord gs with fs ≟ᶠ gs
61+
... | yes refl = yes refl
62+
... | no ¬p = no (λ { refl → ¬p refl })
63+
-- distinct-head pairs (all absurd; enumerated because Agda will not refine a
64+
-- single `_ ≟ᵗ _` catch-all to the distinct-head cases under --safe):
65+
TInt ≟ᵗ TFloat = no (λ ())
66+
TInt ≟ᵗ TString = no (λ ())
67+
TInt ≟ᵗ TBool = no (λ ())
68+
TInt ≟ᵗ TIP = no (λ ())
69+
TInt ≟ᵗ TDateTime = no (λ ())
70+
TInt ≟ᵗ TList _ = no (λ ())
71+
TInt ≟ᵗ TRecord _ = no (λ ())
72+
TInt ≟ᵗ TNull = no (λ ())
73+
TFloat ≟ᵗ TInt = no (λ ())
74+
TFloat ≟ᵗ TString = no (λ ())
75+
TFloat ≟ᵗ TBool = no (λ ())
76+
TFloat ≟ᵗ TIP = no (λ ())
77+
TFloat ≟ᵗ TDateTime = no (λ ())
78+
TFloat ≟ᵗ TList _ = no (λ ())
79+
TFloat ≟ᵗ TRecord _ = no (λ ())
80+
TFloat ≟ᵗ TNull = no (λ ())
81+
TString ≟ᵗ TInt = no (λ ())
82+
TString ≟ᵗ TFloat = no (λ ())
83+
TString ≟ᵗ TBool = no (λ ())
84+
TString ≟ᵗ TIP = no (λ ())
85+
TString ≟ᵗ TDateTime = no (λ ())
86+
TString ≟ᵗ TList _ = no (λ ())
87+
TString ≟ᵗ TRecord _ = no (λ ())
88+
TString ≟ᵗ TNull = no (λ ())
89+
TBool ≟ᵗ TInt = no (λ ())
90+
TBool ≟ᵗ TFloat = no (λ ())
91+
TBool ≟ᵗ TString = no (λ ())
92+
TBool ≟ᵗ TIP = no (λ ())
93+
TBool ≟ᵗ TDateTime = no (λ ())
94+
TBool ≟ᵗ TList _ = no (λ ())
95+
TBool ≟ᵗ TRecord _ = no (λ ())
96+
TBool ≟ᵗ TNull = no (λ ())
97+
TIP ≟ᵗ TInt = no (λ ())
98+
TIP ≟ᵗ TFloat = no (λ ())
99+
TIP ≟ᵗ TString = no (λ ())
100+
TIP ≟ᵗ TBool = no (λ ())
101+
TIP ≟ᵗ TDateTime = no (λ ())
102+
TIP ≟ᵗ TList _ = no (λ ())
103+
TIP ≟ᵗ TRecord _ = no (λ ())
104+
TIP ≟ᵗ TNull = no (λ ())
105+
TDateTime ≟ᵗ TInt = no (λ ())
106+
TDateTime ≟ᵗ TFloat = no (λ ())
107+
TDateTime ≟ᵗ TString = no (λ ())
108+
TDateTime ≟ᵗ TBool = no (λ ())
109+
TDateTime ≟ᵗ TIP = no (λ ())
110+
TDateTime ≟ᵗ TList _ = no (λ ())
111+
TDateTime ≟ᵗ TRecord _ = no (λ ())
112+
TDateTime ≟ᵗ TNull = no (λ ())
113+
TList _ ≟ᵗ TInt = no (λ ())
114+
TList _ ≟ᵗ TFloat = no (λ ())
115+
TList _ ≟ᵗ TString = no (λ ())
116+
TList _ ≟ᵗ TBool = no (λ ())
117+
TList _ ≟ᵗ TIP = no (λ ())
118+
TList _ ≟ᵗ TDateTime = no (λ ())
119+
TList _ ≟ᵗ TRecord _ = no (λ ())
120+
TList _ ≟ᵗ TNull = no (λ ())
121+
TRecord _ ≟ᵗ TInt = no (λ ())
122+
TRecord _ ≟ᵗ TFloat = no (λ ())
123+
TRecord _ ≟ᵗ TString = no (λ ())
124+
TRecord _ ≟ᵗ TBool = no (λ ())
125+
TRecord _ ≟ᵗ TIP = no (λ ())
126+
TRecord _ ≟ᵗ TDateTime = no (λ ())
127+
TRecord _ ≟ᵗ TList _ = no (λ ())
128+
TRecord _ ≟ᵗ TNull = no (λ ())
129+
TNull ≟ᵗ TInt = no (λ ())
130+
TNull ≟ᵗ TFloat = no (λ ())
131+
TNull ≟ᵗ TString = no (λ ())
132+
TNull ≟ᵗ TBool = no (λ ())
133+
TNull ≟ᵗ TIP = no (λ ())
134+
TNull ≟ᵗ TDateTime = no (λ ())
135+
TNull ≟ᵗ TList _ = no (λ ())
136+
TNull ≟ᵗ TRecord _ = no (λ ())
137+
138+
-- Decidable equality for record field lists.
139+
_≟ᶠ_ : (fs gs : List (String × PhrType)) → Dec (fs ≡ gs)
140+
[] ≟ᶠ [] = yes refl
141+
[] ≟ᶠ (_ ∷ _) = no (λ ())
142+
(_ ∷ _) ≟ᶠ [] = no (λ ())
143+
((s₁ , τ₁) ∷ fs) ≟ᶠ ((s₂ , τ₂) ∷ gs)
144+
with Data.String._≟_ s₁ s₂ | τ₁ ≟ᵗ τ₂ | fs ≟ᶠ gs
145+
... | yes refl | yes refl | yes refl = yes refl
146+
... | no ¬p | _ | _ = no (λ { refl → ¬p refl })
147+
... | _ | no ¬p | _ = no (λ { refl → ¬p refl })
148+
... | _ | _ | no ¬p = no (λ { refl → ¬p refl })
52149

53150
-- ═══════════════════════════════════════════════════════════════════════════
54151
-- 3. Semantic Domain (Values indexed by Type)
@@ -72,15 +169,15 @@ _ ≟ᵗ _ = no (λ ())
72169
-- ═══════════════════════════════════════════════════════════════════════════
73170

74171
data Ctx : Set where
75-
∅ : Ctx
76-
_,_ : Ctx → String × PhrType → Ctx
172+
∅ : Ctx
173+
_,,_ : Ctx → String × PhrType → Ctx
77174

78-
infixl 5 _,_
175+
infixl 5 _,,_
79176

80177
-- Variable lookup (de Bruijn style would be cleaner, but using names for clarity)
81178
data _∋_∶_ : Ctx → String → PhrType → Set where
82-
here : ∀ {Γ x τ} → (Γ , (x , τ)) ∋ x ∶ τ
83-
there : ∀ {Γ x y τ τ'} → Γ ∋ x ∶ τ → (Γ , (y , τ')) ∋ x ∶ τ
179+
here : ∀ {Γ x τ} → (Γ ,, (x , τ)) ∋ x ∶ τ
180+
there : ∀ {Γ x y τ τ'} → Γ ∋ x ∶ τ → (Γ ,, (y , τ')) ∋ x ∶ τ
84181

85182
-- ═══════════════════════════════════════════════════════════════════════════
86183
-- 5. Intrinsically Typed Expressions
@@ -130,7 +227,7 @@ infix 5 _==ᵉ_ _<ᵉ_
130227

131228
data Env : Ctx → Set where
132229
ε : Env ∅
133-
_▷_ : ∀ {Γ x τ} → Env Γ → ⟦ τ ⟧ → Env (Γ , (x , τ))
230+
_▷_ : ∀ {Γ x τ} → Env Γ → ⟦ τ ⟧ → Env (Γ ,, (x , τ))
134231

135232
infixl 5 _▷_
136233

@@ -143,12 +240,12 @@ lookupEnv (there x) (ρ ▷ _) = lookupEnv x ρ
143240
-- 7. Denotational Semantics (Evaluation)
144241
-- ═══════════════════════════════════════════════════════════════════════════
145242

146-
open import Data.Integer using (_+_; _-_; _*_; _≤ᵇ_) renaming (_+_ to _+ℤ_; _-_ to _-ℤ_; _*_ to _*ℤ_)
243+
open import Data.Integer using (_≤ᵇ_) renaming (_+_ to _+ℤ_; _-_ to _-ℤ_; _*_ to _*ℤ_)
147244

148245
-- Value equality (for comparison operators)
149246
-- Implemented via decidable equality per type, not postulated.
150247

151-
open import Data.Integer using (_≟_) renaming (_≟_ to _≟ℤ_)
248+
open import Data.Integer using () renaming (_≟_ to _≟ℤ_)
152249
open import Data.String using () renaming (_≟_ to _≟ˢ_)
153250
open import Data.Nat using () renaming (_≟_ to _≟ⁿ_)
154251
open import Data.Bool using () renaming (_≟_ to _≟ᵇ_)
@@ -196,10 +293,10 @@ mutual
196293
eqRecord {[]} tt tt = true
197294
eqRecord {(_ , τ) ∷ fs} (v , vs) (w , ws) = _≡ᵛ_ v w ∧ eqRecord {fs} vs ws
198295

199-
-- Integer less-than via the standard library ordering.
296+
-- Integer less-than via the standard library ordering. The parentheses are
297+
-- load-bearing (`_∧_` binds tighter than `_≤ᵇ_`); `_≡ᵛ_` is indexed at TInt.
200298
_<ᵛ_ : ℤ → ℤ → Bool
201-
a <ᵛ b = a ≤ᵇ b ∧ not (a ≡ᵛ b)
202-
where open import Data.Integer using (_≤ᵇ_)
299+
a <ᵛ b = (a ≤ᵇ b) ∧ not (_≡ᵛ_ {TInt} a b)
203300

204301
-- List membership via value equality.
205302
_∈ᵛ_ : ∀ {τ} → ⟦ τ ⟧ → List ⟦ τ ⟧ → Bool

0 commit comments

Comments
 (0)