From 6659b8cfc0c391646636f3995d01f9e90a9d01b0 Mon Sep 17 00:00:00 2001 From: hyperpolymath Date: Sun, 21 Jun 2026 13:45:14 +0000 Subject: [PATCH] feat(formal): grow P-2 to the STLC with functions + substitution (P2_Stlc.v) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wave-1 increment for P-2: adds what the first-order P2_Progress.v lacked — **functions, binders, and the substitution lemma**. Full progress + preservation for the simply-typed lambda calculus (base type TUnit + ->), call-by-value, named (nat) variables. Funext-free, so axiom-free (Print Assumptions: "Closed under the global context"; no Admitted): contexts are compared only on a term's FREE variables (free_in_context + context_invariance), never by function equality, so the development uses no functional_extensionality. Contents: free_in_context, context_invariance, subst_preserves_typing (the substitution lemma), canonical forms, progress (induction on typing), preservation (induction on the step relation). Discharges the Siblings_Stated P2 statements at the closed-term (empty-context) instantiation, as P2_Progress. Scope: simply-typed only — the QTT/affine quantities (substructural context-splitting discipline) are the remaining increment. Track now 10 files, 16 closure reports, no axioms. justfile/_CoqProject build P2_Stlc; .hypatia-ignore extends the Coq-not-V-lang carve-out; README + PROOF-NEEDS P-2 row updated (P2_Progress = first-order, P2_Stlc = STLC grown). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- .hypatia-ignore | 2 + docs/PROOF-NEEDS.adoc | 7 +- formal/P2_Stlc.v | 206 ++++++++++++++++++++++++++++++++++++++++++ formal/README.adoc | 18 +++- formal/_CoqProject | 1 + formal/justfile | 2 +- 6 files changed, 228 insertions(+), 8 deletions(-) create mode 100644 formal/P2_Stlc.v diff --git a/.hypatia-ignore b/.hypatia-ignore index d9ea1b96..d6607c23 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -61,3 +61,5 @@ cicd_rules/vlang_detected:formal/P2_Progress.v cicd_rules/banned_language_file:formal/P2_Progress.v cicd_rules/vlang_detected:formal/P3_BorrowGraph.v cicd_rules/banned_language_file:formal/P3_BorrowGraph.v +cicd_rules/vlang_detected:formal/P2_Stlc.v +cicd_rules/banned_language_file:formal/P2_Stlc.v diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index 7e5d67f8..564388a5 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -124,9 +124,10 @@ obligations. They are the "we might have missed" half of the brief. give `Step` its constructors and prove `progress`/`preservation`/`affinePreservation`. | XL | `partial` -| #513 must-have 1; solo-core (Idris2) `stated`; **small-step progress + - preservation mechanized** for a first-order nat/bool/`add`/`if` fragment in - `formal/P2_Progress.v` +| #513 must-have 1; solo-core (Idris2) `stated`; **progress + preservation + mechanized** for a first-order fragment (`formal/P2_Progress.v`) AND for the + **STLC with functions + the substitution lemma** (`formal/P2_Stlc.v`, + funext-free). QTT/affine quantities are the remaining increment | P-3 | **Borrow-graph soundness.** A well-typed program never observes a moved/aliased diff --git a/formal/P2_Stlc.v b/formal/P2_Stlc.v new file mode 100644 index 00000000..0e824675 --- /dev/null +++ b/formal/P2_Stlc.v @@ -0,0 +1,206 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) + +(* + P2_Stlc.v + ═════════ + P-2, GROWN (Wave 1). Adds what the first-order P2_Progress.v lacked: + **functions, binders, and the substitution lemma**. Full progress + + preservation for the simply-typed lambda calculus (base type `TUnit` plus + `→`), call-by-value, named (`nat`) variables. + + Crucially **funext-free**: contexts are compared only on a term's *free* + variables (`context_invariance`), never by function equality — so the + development uses NO `functional_extensionality` and `Print Assumptions` stays + "Closed under the global context". No `Admitted`, no axioms. + + Scope: simply-typed (no QTT/affine quantities yet) — the substructural + context-splitting discipline on top of this is the next increment. + + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. +*) + +Require Import PeanoNat. +Require Import ASFormal.Siblings_Stated. + +Definition id := nat. + +Inductive ty := TUnit | TArrow (A B : ty). + +Inductive tm := +| var (x : id) +| app (f a : tm) +| abs (x : id) (A : ty) (b : tm) (* A is the domain type *) +| tunit. + +Inductive value : tm -> Prop := +| v_abs : forall x A b, value (abs x A b) +| v_unit : value tunit. + +(* Substitution. Only ever applied with a closed value (the beta-redex + argument), so capture cannot arise — established by the typing lemmas. *) +Fixpoint subst (x : id) (s t : tm) : tm := + match t with + | var y => if Nat.eqb x y then s else var y + | abs y A b => abs y A (if Nat.eqb x y then b else subst x s b) + | app f a => app (subst x s f) (subst x s a) + | tunit => tunit + end. + +Inductive step : tm -> tm -> Prop := +| ST_AppAbs : forall x A b v, value v -> step (app (abs x A b) v) (subst x v b) +| ST_App1 : forall f f' a, step f f' -> step (app f a) (app f' a) +| ST_App2 : forall f a a', value f -> step a a' -> step (app f a) (app f a'). + +Definition context := id -> option ty. +Definition empty : context := fun _ => None. +Definition extend (G : context) (x : id) (T : ty) : context := + fun y => if Nat.eqb x y then Some T else G y. + +Inductive has_type : context -> tm -> ty -> Prop := +| T_Var : forall G x T, G x = Some T -> has_type G (var x) T +| T_Abs : forall G x A B b, has_type (extend G x A) b B -> has_type G (abs x A b) (TArrow A B) +| T_App : forall G f a A B, has_type G f (TArrow A B) -> has_type G a A -> has_type G (app f a) B +| T_Unit : forall G, has_type G tunit TUnit. + +(* ── free variables, free-in-context ───────────────────────────────────── *) + +Inductive afi : id -> tm -> Prop := +| afi_var : forall x, afi x (var x) +| afi_app1 : forall x f a, afi x f -> afi x (app f a) +| afi_app2 : forall x f a, afi x a -> afi x (app f a) +| afi_abs : forall x y A b, y <> x -> afi x b -> afi x (abs y A b). + +#[local] Hint Constructors afi : core. + +Lemma free_in_context : forall x t S G, + afi x t -> has_type G t S -> exists U, G x = Some U. +Proof. + intros x t S G Hafi; generalize dependent S; generalize dependent G. + induction Hafi; intros G S HT; inversion HT; subst. + - eauto. + - eapply IHHafi; eauto. + - eapply IHHafi; eauto. + - edestruct IHHafi as [U HU]; eauto. + unfold extend in HU. destruct (Nat.eqb y x) eqn:E. + + apply Nat.eqb_eq in E; subst y; exfalso; apply H; reflexivity. + + eauto. +Qed. + +Corollary typable_empty_closed : forall x t S, + afi x t -> has_type empty t S -> False. +Proof. + intros x t S Hafi HT. + destruct (free_in_context x t S empty Hafi HT) as [U HU]; discriminate HU. +Qed. + +(* ── context invariance (the funext-free substitute for map equality) ──── *) + +Lemma context_invariance : forall G G' t S, + has_type G t S -> + (forall x, afi x t -> G x = G' x) -> + has_type G' t S. +Proof. + intros G G' t S HT; generalize dependent G'. + induction HT; intros G' Hf. + - apply T_Var. rewrite <- (Hf x (afi_var x)). assumption. + - apply T_Abs. apply IHHT. intros z Hz. unfold extend. + destruct (Nat.eqb x z) eqn:E; auto. + apply Hf. apply Nat.eqb_neq in E. auto. + - eapply T_App; [apply IHHT1 | apply IHHT2]; intros z Hz; apply Hf; auto. + - apply T_Unit. +Qed. + +(* ── substitution preserves typing ─────────────────────────────────────── *) + +Lemma subst_preserves_typing : forall G x U t v S, + has_type (extend G x U) t S -> + has_type empty v U -> + has_type G (subst x v t) S. +Proof. + intros G x U t v S Ht Hv; generalize dependent S; generalize dependent G. + induction t as [ y | f IHf a IHa | y A b IHb | ]; + intros G S Ht; simpl; inversion Ht; subst. + - (* var y *) + unfold extend in H1. destruct (Nat.eqb x y) eqn:E. + + injection H1 as H1. rewrite <- H1. + apply (context_invariance empty G); [assumption |]. + intros z Hz. exfalso; apply (typable_empty_closed z v U Hz Hv). + + apply T_Var; assumption. + - (* app f a *) + eapply T_App; [apply IHf | apply IHa]; eassumption. + - (* abs y A b *) + destruct (Nat.eqb x y) eqn:E. + + apply Nat.eqb_eq in E; subst y. + apply T_Abs. + apply (context_invariance (extend (extend G x U) x A) (extend G x A)); + [assumption |]. + intros z Hz. unfold extend. destruct (Nat.eqb x z); reflexivity. + + apply T_Abs. apply IHb. + apply (context_invariance (extend (extend G x U) y A) + (extend (extend G y A) x U)); [assumption |]. + intros z Hz. unfold extend. + destruct (Nat.eqb y z) eqn:E1; destruct (Nat.eqb x z) eqn:E2; + try reflexivity. + exfalso. apply Nat.eqb_neq in E. apply E. + apply Nat.eqb_eq in E1; apply Nat.eqb_eq in E2. + rewrite E2, <- E1; reflexivity. + - (* tunit *) apply T_Unit. +Qed. + +(* ── canonical forms ───────────────────────────────────────────────────── *) + +Lemma canon_arrow : forall v A B, + value v -> has_type empty v (TArrow A B) -> exists x b, v = abs x A b. +Proof. + intros v A B Hv HT; destruct Hv. + - inversion HT; subst; eauto. + - inversion HT. +Qed. + +(* ── progress ──────────────────────────────────────────────────────────── *) + +Theorem progress : forall t S, has_type empty t S -> value t \/ exists t', step t t'. +Proof. + intros t S HT; remember empty as G eqn:HG. + induction HT. + - subst G; discriminate H. + - left; apply v_abs. + - right; subst G. + destruct IHHT1 as [Hvf | [f' Hf]]; [reflexivity | |]. + + destruct (canon_arrow _ _ _ Hvf HT1) as [x [b ->]]. + destruct IHHT2 as [Hva | [a' Ha]]; [reflexivity | |]. + * eexists; apply ST_AppAbs; assumption. + * eexists; apply ST_App2; [apply v_abs | eassumption]. + + eexists; apply ST_App1; eassumption. + - left; apply v_unit. +Qed. + +(* ── preservation ──────────────────────────────────────────────────────── *) + +Theorem preservation : forall t t' S, + has_type empty t S -> step t t' -> has_type empty t' S. +Proof. + intros t t' S HT Hstep; generalize dependent S. + induction Hstep; intros S HT; inversion HT; subst. + - (* ST_AppAbs *) + match goal with H : has_type _ (abs _ _ _) _ |- _ => inversion H; subst end. + eapply subst_preserves_typing; eassumption. + - (* ST_App1 *) eapply T_App; [ apply IHHstep; eassumption | eassumption ]. + - (* ST_App2 *) eapply T_App; [ eassumption | apply IHHstep; eassumption ]. +Qed. + +(* ── discharge the stated obligations (closed-term, ctx:=unit) ──────────── *) + +Definition P2_progress_discharged + : P2_progress tm ty unit tt + (fun (_ : unit) (t : tm) (T : ty) => has_type empty t T) value step + := progress. + +Definition P2_preservation_discharged + : P2_preservation tm ty unit + (fun (_ : unit) (t : tm) (T : ty) => has_type empty t T) step + := fun (_ : unit) t t' T HT Hs => preservation t t' T HT Hs. + +Print Assumptions progress. +Print Assumptions preservation. diff --git a/formal/README.adoc b/formal/README.adoc index dbdb5dc7..a31f8a99 100644 --- a/formal/README.adoc +++ b/formal/README.adoc @@ -45,7 +45,12 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires. | **stated** — and now discharged for concrete models below | `P2_Progress.v` -| **P-2** — progress + preservation (nat/bool/`add`/`if`, small-step) +| **P-2** — progress + preservation (nat/bool/`add`/`if`, first-order) +| **mechanized**, axiom-free + +| `P2_Stlc.v` +| **P-2, grown** — STLC with *functions* + the substitution lemma; progress + + preservation (funext-free) | **mechanized**, axiom-free | `P3_BorrowSound.v` @@ -82,9 +87,14 @@ the stated obligation and pin its meaning, not the full language: * **P-2** (`P2_Progress.v`) — a simply-typed first-order calculus (nat/bool/`add`/`if`), small-step, call-by-value, with the standard - canonical-forms / progress / preservation development. Functions, binders, - products/sums and the QTT quantities are the next increments (codegen - preservation *with* `let`/variables is already in `K1Let_…`). + canonical-forms / progress / preservation development. +* **P-2, grown** (`P2_Stlc.v`) — the Wave-1 increment: the **simply-typed + lambda calculus** with functions, binders, and the **substitution lemma** + (the thing the first-order version lacked). Full progress + preservation, + **funext-free** — contexts are compared only on a term's *free* variables + (`context_invariance`), so it uses no `functional_extensionality` and stays + axiom-free. The QTT/affine quantities (substructural context splitting) are + the next increment. * **P-3** (`P3_BorrowSound.v`) — a one-resource borrow calculus; proves the precise validity checker is sound and **rejects the #554 witness** (`[OBorrow; OMove; OUseRef]`), matching `lib/borrow.ml`'s post-#554-fix diff --git a/formal/_CoqProject b/formal/_CoqProject index 703c1e9f..4aee801e 100644 --- a/formal/_CoqProject +++ b/formal/_CoqProject @@ -8,3 +8,4 @@ F4_ErrorFaithful.v P3_BorrowSound.v P3_BorrowGraph.v P2_Progress.v +P2_Stlc.v diff --git a/formal/justfile b/formal/justfile index a0f4456c..be481dd8 100644 --- a/formal/justfile +++ b/formal/justfile @@ -11,7 +11,7 @@ check: all="" for f in K1_CodegenPreservation K1Let_CodegenPreservation Siblings_Stated \ F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \ - P3_BorrowSound P3_BorrowGraph P2_Progress; do + P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc; do echo "== coqc $f.v ==" o="$(coqc -Q . ASFormal "$f.v")" printf '%s\n' "$o"