|
35 | 35 | - preservation: stepping preserves types |
36 | 36 | - type_safety: multi-step evaluation preserves types (by induction + preservation) |
37 | 37 | - consent_monotonicity / consent_preservation: consent system properties |
| 38 | +
|
| 39 | + ### Arrays (parity with Coq's WokeLang.v): |
| 40 | + `tArray` / `tArrayVal` type array expressions and array literal values |
| 41 | + (the mirror of Coq's `T_Array` / `T_Lit_Array`); `Step` gains `sArrayStep` |
| 42 | + (left-most-element congruence), `sArrayVal` (normalise a fully-evaluated |
| 43 | + array to a `.vArray` literal value), and `sArrayErr` (panic propagation). |
| 44 | + `progress` and `preservation` cover all three. The `∀ e ∈ es` premise shape |
| 45 | + yields a per-element induction hypothesis directly, so — unlike the Coq |
| 46 | + development — no well-founded recursion on an expression-size measure is |
| 47 | + needed: `array_split` does the pure-list decomposition and the IH answers |
| 48 | + value-or-steps per element. |
38 | 49 | -/ |
39 | 50 |
|
40 | 51 | namespace WokeLang |
@@ -221,6 +232,18 @@ inductive HasType : TypeEnv → Expr → WokeType → Prop where |
221 | 232 | HasType Γ (.unwrap e) tOk |
222 | 233 | | tError : ∀ Γ msg t, |
223 | 234 | HasType Γ (.error msg) t |
| 235 | + -- Arrays (mirror of Coq's `T_Array` / `T_Lit_Array` in WokeLang.v). |
| 236 | + -- `tArray` types an array *expression* elementwise; `tArrayVal` types a |
| 237 | + -- fully-evaluated array *literal value*. Both premises use the `∀ e ∈ es` |
| 238 | + -- shape, which (unlike Coq's `Forall`) yields a per-element induction |
| 239 | + -- hypothesis directly from `induction`, so the `progress`/`preservation` |
| 240 | + -- array cases need no well-founded recursion on an `expr_size` measure. |
| 241 | + | tArray : ∀ Γ es t, |
| 242 | + (∀ e, e ∈ es → HasType Γ e t) → |
| 243 | + HasType Γ (.array es) (.array t) |
| 244 | + | tArrayVal : ∀ Γ vs t, |
| 245 | + (∀ v, v ∈ vs → HasType Γ (.lit v) t) → |
| 246 | + HasType Γ (.lit (.vArray vs)) (.array t) |
224 | 247 |
|
225 | 248 | -- ========================================================================= |
226 | 249 | -- 4. Operational Semantics |
@@ -332,6 +355,20 @@ inductive Step : Expr → Env → Expr → Env → Prop where |
332 | 355 | Step (.oops (.error msg)) ρ (.error msg) ρ |
333 | 356 | | sUnwrapErr : ∀ msg ρ, |
334 | 357 | Step (.unwrap (.error msg)) ρ (.error msg) ρ |
| 358 | + -- Array evaluation (mirror of Coq's `S_Array_step` / `S_Array_val`, plus |
| 359 | + -- panic propagation). `sArrayStep` reduces the left-most non-value element; |
| 360 | + -- `sArrayVal` normalises a fully-evaluated array to an array literal value; |
| 361 | + -- `sArrayErr` propagates a panic out of an array, as the binop rules do. |
| 362 | + -- A fully-evaluated array is *not* an `IsValue` (it always steps via |
| 363 | + -- `sArrayVal`); the `IsValue` is the resulting `.lit (.vArray vs)`. |
| 364 | + | sArrayStep : ∀ (vs : List Value) (e e' : Expr) (es : List Expr) (ρ ρ' : Env), |
| 365 | + Step e ρ e' ρ' → |
| 366 | + Step (.array (vs.map Expr.lit ++ e :: es)) ρ |
| 367 | + (.array (vs.map Expr.lit ++ e' :: es)) ρ' |
| 368 | + | sArrayVal : ∀ (vs : List Value) (ρ : Env), |
| 369 | + Step (.array (vs.map Expr.lit)) ρ (.lit (.vArray vs)) ρ |
| 370 | + | sArrayErr : ∀ (vs : List Value) (msg : String) (es : List Expr) (ρ : Env), |
| 371 | + Step (.array (vs.map Expr.lit ++ .error msg :: es)) ρ (.error msg) ρ |
335 | 372 |
|
336 | 373 | /-- Multi-step reduction (reflexive transitive closure) -/ |
337 | 374 | inductive MultiStep : Expr → Env → Expr → Env → Prop where |
@@ -386,6 +423,40 @@ theorem canonical_forms_result : ∀ v tOk tErr, |
386 | 423 | | tOkayVal _ _ h₁ => left; exact ⟨_, rfl⟩ |
387 | 424 | | tOopsVal _ _ => right; exact ⟨_, rfl⟩ |
388 | 425 |
|
| 426 | +/-- `isLitB e` is `true` exactly when `e` is a literal-value expression. |
| 427 | + Used by `array_split` to locate the left-most non-literal array element. -/ |
| 428 | +def isLitB : Expr → Bool |
| 429 | + | .lit _ => true |
| 430 | + | _ => false |
| 431 | + |
| 432 | +theorem isLitB_true {e : Expr} : isLitB e = true → ∃ v, e = .lit v := by |
| 433 | + cases e <;> simp [isLitB] |
| 434 | + |
| 435 | +theorem isLitB_false {e : Expr} : isLitB e = false → ∀ v, e ≠ .lit v := by |
| 436 | + cases e <;> simp [isLitB] |
| 437 | + |
| 438 | +/-- A list of expressions is either all literal values, or splits as a prefix |
| 439 | + of literal values, a left-most non-literal element, and a remainder. This |
| 440 | + is the Lean analogue of Coq's `array_elements_progress` decomposition; |
| 441 | + here it is pure list reasoning, with the "is it a value or does it step?" |
| 442 | + question deferred to the per-element IH in the `tArray` progress case. -/ |
| 443 | +theorem array_split (es : List Expr) : |
| 444 | + (∃ vs : List Value, es = vs.map Expr.lit) ∨ |
| 445 | + (∃ (vs : List Value) (e : Expr) (rest : List Expr), |
| 446 | + es = vs.map Expr.lit ++ e :: rest ∧ ∀ v, e ≠ .lit v) := by |
| 447 | + induction es with |
| 448 | + | nil => left; exact ⟨[], rfl⟩ |
| 449 | + | cons hd tl ih => |
| 450 | + cases hb : isLitB hd with |
| 451 | + | true => |
| 452 | + obtain ⟨v, rfl⟩ := isLitB_true hb |
| 453 | + cases ih with |
| 454 | + | inl h => obtain ⟨vs, rfl⟩ := h; left; exact ⟨v :: vs, rfl⟩ |
| 455 | + | inr h => obtain ⟨vs, e, rest, rfl, hne⟩ := h |
| 456 | + right; exact ⟨v :: vs, e, rest, rfl, hne⟩ |
| 457 | + | false => |
| 458 | + right; exact ⟨[], hd, tl, rfl, isLitB_false hb⟩ |
| 459 | + |
389 | 460 | /-- Progress theorem: a well-typed closed expression is either a value or can step. |
390 | 461 | unwrap of an error value steps to an error expression via sUnwrapError, |
391 | 462 | modelling WokeLang's panic semantics for unwrapping failures. -/ |
@@ -838,6 +909,32 @@ theorem progress : ∀ e t, |
838 | 909 | | tError msg _ => |
839 | 910 | -- Error expressions are terminal values (panics). |
840 | 911 | left; exact .error msg |
| 912 | + | tArray es t hall ih => |
| 913 | + -- An array expression is never a value: it either normalises (all |
| 914 | + -- elements are literals ⇒ sArrayVal), propagates a panic (left-most |
| 915 | + -- non-literal is an error ⇒ sArrayErr), or steps its left-most |
| 916 | + -- non-literal element (⇒ sArrayStep). The per-element progress IH `ih` |
| 917 | + -- discharges the last two via `array_split`. |
| 918 | + right |
| 919 | + cases array_split es with |
| 920 | + | inl hsplit => |
| 921 | + obtain ⟨vs, rfl⟩ := hsplit |
| 922 | + exact ⟨.lit (.vArray vs), emptyEnv, .sArrayVal vs emptyEnv⟩ |
| 923 | + | inr hsplit => |
| 924 | + obtain ⟨vs, e, rest, rfl, hne⟩ := hsplit |
| 925 | + have hin : e ∈ vs.map Expr.lit ++ e :: rest := by simp |
| 926 | + cases ih e hin with |
| 927 | + | inl hv => |
| 928 | + cases hv with |
| 929 | + | lit v => exact absurd rfl (hne v) |
| 930 | + | error msg => exact ⟨.error msg, emptyEnv, .sArrayErr vs msg rest emptyEnv⟩ |
| 931 | + | inr hstp => |
| 932 | + obtain ⟨e', ρ', hs⟩ := hstp |
| 933 | + exact ⟨.array (vs.map Expr.lit ++ e' :: rest), ρ', |
| 934 | + .sArrayStep vs e e' rest emptyEnv ρ' hs⟩ |
| 935 | + | tArrayVal vs t hall ih => |
| 936 | + -- A fully-evaluated array literal `.lit (.vArray vs)` is a value. |
| 937 | + left; constructor |
841 | 938 |
|
842 | 939 | /-- Preservation theorem: if a well-typed expression steps, the result is well-typed. |
843 | 940 | Proof by induction on the Step derivation with inversion on the typing derivation. |
@@ -1036,6 +1133,26 @@ theorem preservation : ∀ e e' t ρ ρ', |
1036 | 1133 | | sUnwrapErr msg _ => |
1037 | 1134 | cases ht with |
1038 | 1135 | | tUnwrap _ tOk tErr h₁ => exact .tError _ msg _ |
| 1136 | + | sArrayStep vs e e' rest ρ ρ' hs ih => |
| 1137 | + -- Congruence: the stepped element keeps its type (by the IH); every other |
| 1138 | + -- element keeps the witness it had from the original `tArray` derivation. |
| 1139 | + cases ht with |
| 1140 | + | tArray _ t' hall => |
| 1141 | + refine .tArray _ _ t' (fun x hx => ?_) |
| 1142 | + rcases List.mem_append.1 hx with hpre | hcons |
| 1143 | + · exact hall x (List.mem_append.2 (Or.inl hpre)) |
| 1144 | + · rcases List.mem_cons.1 hcons with rfl | htail |
| 1145 | + · exact ih t' (hall e (List.mem_append.2 (Or.inr List.mem_cons_self))) |
| 1146 | + · exact hall x (List.mem_append.2 (Or.inr (List.mem_cons_of_mem _ htail))) |
| 1147 | + | sArrayVal vs ρ => |
| 1148 | + -- Normalisation: `.array (vs.map lit) : array t'` becomes the literal value |
| 1149 | + -- `.lit (.vArray vs) : array t'`, re-typed via `tArrayVal`. |
| 1150 | + cases ht with |
| 1151 | + | tArray _ t' hall => |
| 1152 | + exact .tArrayVal _ vs t' (fun v hv => hall (Expr.lit v) (List.mem_map.2 ⟨v, hv, rfl⟩)) |
| 1153 | + | sArrayErr vs msg rest ρ => |
| 1154 | + -- Panic propagation: the result `.error msg` is well-typed at any type. |
| 1155 | + exact .tError _ msg _ |
1039 | 1156 |
|
1040 | 1157 | /-- Type safety theorem -/ |
1041 | 1158 | theorem type_safety : ∀ e t v ρ, |
|
0 commit comments