From 344698f8ad9d0ea7ff2b5ee7fdbe1fae0de54c90 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 16:13:15 +0100 Subject: [PATCH] =?UTF-8?q?docs+test:=20Phase=20D=20slice=204=20Phase=204c?= =?UTF-8?q?=20=E2=80=94=20mechanised=20soundness-gap=20counterexample=20fo?= =?UTF-8?q?r=20TFunEff=20=CE=B2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ships a mechanised proof that preservation_l2 fails for TFunEff substituends inside fresh-region scopes, plus a design-doc addendum prescribing the conditional Phase 4c closure path. ## What this PR ships ### `formal/Counterexample_L2.v` (new) Three Qed lemmas (zero axioms, zero admits) witnessing the soundness gap: - `e_before_typed` — input `EApp outer v2` types via T_App_L2_Eff at `TFunEff TUnit TUnit [] []`. - `e_step` — operational step S_App_Fun reduces to `ERegion r2 v2`. - `e_after_untypable` — no L1 derivation exists for the β-result at the same outer type. Configuration: ``` T1_inner = TFunEff TUnit TUnit [] [] (* R_in_v = [] *) outer = ELam T1_inner (ERegion r2 (EVar 0)) v2 = ELam TUnit EUnit e_before = EApp outer v2 (* well-typed *) e_after = ERegion r2 v2 (* β-result, not well-typed *) ``` Structural mechanism: T_Region_L1's `~ In r (free_regions T)` premise prevents the fresh r from being in `R_in_v ⊆ free_regions(TFunEff)`, so the post-β term's inner TFunEff value cannot re-type at the new threaded R = `r :: R`. ### `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` addendum New §"Phase 4c addendum (2026-05-30) — conditional preservation_l2 for TFunEff β" documents the counterexample and prescribes three resolution paths: 1. **Conditional preservation_l2 (recommended)** — Phase 3b lemma takes the `regions_introduced_by(e) ⊆ R_in_v` precondition; Phase 4c β-case requires it; programs outside form a documented soundness-gap class. Aligns with `Counterexample.v` precedent. 2. **Region-polymorphic TFunEff** — type-system change deferred to a future redesign. 3. **L2 region-transfer combinator** — adds L2 expressiveness in a future PR. ### `formal/_CoqProject` Adds `Counterexample_L2.v` after `TypingL2.v` in the build order. ### `.machine_readable/6a2/STATE.a2ml` `next_action` shifted to Phase 3b implementation (option-(a) precondition codified by this PR's counterexample); `last_action` records the counterexample landing. ## Build + assumption audit - `coqc -R . Ephapax` clean rebuild across all 11 .v files. - `Print Assumptions e_before_typed` / `e_step` / `e_after_untypable` → "Closed under the global context" for all three. **Zero axioms.** ## Owner-directive compliance (CLAUDE.md 2026-05-27) - Does not modify `formal/Semantics.v` or `formal/Counterexample.v` (the legacy soundness-gap artifacts). - Does not patch `formal/Typing.v` (legacy judgment). - Does not close any residual `formal/Semantics_L1.v` admit. - Adds NEW infrastructure (a new file) orthogonal to legacy admits, mirroring the precedent of `Counterexample.v` for the legacy preservation. - No new `Axiom` or `Admitted` markers. ## Why this matters Before Phase 3b implementation (~400 lines per PR #230's analysis), this counterexample mechanically witnesses the structural constraint the lemma must satisfy. The conditional preservation_l2 design is now rigorously justified rather than asserted on paper. Refs: - ephapax#225 — Phase 3b tracking issue (option (a) selected). - ephapax#225 comment 4583148707 — on-paper prototype that motivated this mechanical formalisation. - PR #230 — `regions_introduced_by` scaffold (option (a)'s syntactic helper). - PR #228 — Phase 4a (linear T1, no soundness gap). - PR #233 — Phase 4b (ground-non-linear T1, no soundness gap). - `formal/Counterexample.v` — legacy preservation counterexample (precedent for this file's structure). Co-Authored-By: Claude Opus 4.7 (1M context) --- .machine_readable/6a2/STATE.a2ml | 4 +- formal/Counterexample_L2.v | 202 ++++++++++++++++++++ formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md | 44 +++++ formal/_CoqProject | 1 + 4 files changed, 249 insertions(+), 2 deletions(-) create mode 100644 formal/Counterexample_L2.v diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 24a8b09f..56281bc7 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,8 +6,8 @@ @state(version="2.0"): phase: "implementation" -next_action: "Phase D slice 4 Phase 4b — ground-non-linear T1 path for the `T_App_L2_Eff` β-case (uses Phase 2's `subst_typing_gen_l1_m_ground_nonlinear`). Then Phase 4c (TFunEff non-linear T1, blocked on Phase 3b per issue #225) and Phase 4d (compound, deferred to Phase 5). Phase 4a (this slot's predecessor) shipped `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` in TypingL2.v, closing the β-case for linear T1. Phase 3b is still parked at issue #225 with three candidate solutions; Phase 4a prototyping confirmed the substitution shape used for linear T1 (k=0, raw cons in Gin/Gout, m-poly via `linear_value_retype_l1_m` for the Affine branch). For 3b, the actual subst shape will mirror Phase 4a's but with the value being a TFunEff lambda — the substitution premise will need a TFunEff-typed substituend at the threaded R, with the side condition propagating through. Recommend prototyping Phase 4c next (it forces 3b's design hand). Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." -last_action: "Phase D slice 4 Phase 4a LANDED (2026-05-30, this PR): `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` added to `formal/TypingL2.v`. The L1-level kernel takes inverted T_App_L2_Eff premises (a TFunEff lambda + a value argument typed at linear T1) and produces the post-β L1 typing via `subst_typing_gen_l1_m` at k=0. The L2 wrapper inverts both has_type_l2 hypotheses through L2_lift_l1 (T_App_L2_Eff discriminates: lambda's head is ELam not EApp; argument is a value so cannot be EApp). Two structural reductions inside the kernel: inversion on Hlam forces T_Lam_L1_*_Eff (the only formation rules producing TFunEff), exposing body typing at R_in; `value_R_G_preserving_l1` on Harg collapses R_in→R, G''→G. Then subst at k=0 with raw cons in the `with` clause (ctx_extend was too opaque for unification of remove_at 0 _ = G'') — and for the Affine branch, the linear v2 is re-derived at Linear mode via local helper `linear_value_retype_l1_m` (because subst_typing_gen_l1_m's premise 5 uses the bare `|=L1` notation which is Linear-mode-only). The same PR hotfixes a duplicate `tfuneff_lambda_retype_l1_m` from PR #223 + PR #224 (parallel-session merge collision); kept the chronologically-first definition (Hval, Ht, HR' arg order) and removed the second. Coqc 8.18.0 clean rebuild across all 10 .v files. Zero new admits/axioms (Print Assumptions confirms only the pre-existing `region_liveness_at_split_l1_gen` axiom inherited via `subst_typing_gen_l1_m`). `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Phase 4a is clean infrastructure composable with `preservation_l2_via_l1` toward full `preservation_l2` over has_type_l2." +next_action: "Phase D slice 4 Phase 3b — implement `subst_typing_gen_l1_m_tfuneff` with option (a)'s precondition `(forall r, In r (regions_introduced_by e) -> In r R_in_v)`. Per the parallel session's analysis (PR #230's body), this is ~400 lines mirroring Phase 2 with `shift_typing_gen_l1_m` threading at every binder-descent case (Phase 2's `ground_nonlinear_value_shift_id_l1` shortcut doesn't apply to non-scalar TFunEff lambdas — `shift c 1 (ELam T0 e0) = ELam T0 (shift (S c) 1 e0)`, which changes body's de Bruijn indices). The precondition propagates through compound rules (sub-expressions' `regions_introduced_by` are subsets of the parent's) and discharges directly at the T_Region_L1 case. After Phase 3b: Phase 4c wraps preservation_l2's T_App_L2_Eff β-case CONDITIONALLY — requiring the precondition `regions_introduced_by(ebody) ⊆ R_in_v`. Programs not satisfying it form a documented soundness-gap class per `Counterexample_L2.v` (this slot's predecessor, this PR). Phase 4d (compound non-linear) deferred to Phase 5. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." +last_action: "Phase D slice 4 Phase 4c soundness-gap counterexample LANDED (2026-05-30, this PR): `formal/Counterexample_L2.v` with three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising preservation_l2's failure for TFunEff substituends inside fresh-region scopes. Configuration: outer = ELam (TFunEff TUnit TUnit [] []) (ERegion r2 (EVar 0)); v2 = ELam TUnit EUnit; e_before = EApp outer v2 (types at TFunEff via T_App_L2_Eff); e_after = ERegion r2 v2 (β-result, does NOT type because T_Lam_L1_*_Eff's side condition `forall r, In r [r2] -> In r []` is violated). The structural mechanism: T_Region_L1's `~ In r (free_regions T)` premise prevents fresh r from being in R_in_v ⊆ free_regions(TFunEff), so the post-β term's inner TFunEff value cannot re-type at the new R. Phase 4b (parallel session #233) also LANDED on 2026-05-30. SUBST-LEMMA-GENERALIZATION-DESIGN.md gained a Phase 4c addendum documenting the conditional preservation_l2 path and three resolution options. Counterexample_L2.v added to formal/_CoqProject after TypingL2.v. Coqc 8.18.0 clean rebuild across all 11 .v files. Zero new admits/axioms (`Print Assumptions` confirms all three lemmas Closed under the global context). `Semantics.v`/`Typing.v`/`Counterexample.v` (legacy) untouched. The mechanised counterexample is the L1/L2 analogue of Counterexample.v for the legacy preservation, providing rigorous justification for the conditional Phase 4c statement." updated: 2026-05-30T00:00:00Z @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"): diff --git a/formal/Counterexample_L2.v b/formal/Counterexample_L2.v new file mode 100644 index 00000000..b851c262 --- /dev/null +++ b/formal/Counterexample_L2.v @@ -0,0 +1,202 @@ +(* SPDX-License-Identifier: PMPL-1.0-or-later *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) + +(** * Soundness gap (L2): preservation_l2 fails for TFunEff substituends + inside fresh-region scopes + + The Phase D slice 4 Phase 4c β-case of preservation_l2 fails for + programs that substitute a TFunEff value into a body containing + [ERegion] (fresh-region) introduction. + + This file mechanises the counterexample. It mirrors the structure + of [Counterexample.v] (which exhibits the legacy preservation's + soundness gap) but at the L1/L2 layer with the post-redesign + [has_type_l1] / [has_type_l2] judgments. The artifact justifies + the **conditional** preservation_l2 closure recommended in + [SUBST-LEMMA-GENERALIZATION-DESIGN.md] §"Phase 4c": preservation + holds only for programs satisfying + [regions_introduced_by(ebody) ⊆ R_in_v]; programs outside this + class form a documented soundness-gap subclass. + + ===== Configuration ===== + + T1_inner := TFunEff TUnit TUnit [] [] (* substituee type, R_in_v = [] *) + outer := ELam T1_inner (ERegion r2 (EVar 0)) + (* body introduces fresh r2, returns subst position *) + v2 := ELam TUnit EUnit (* a value of type T1_inner *) + e_before := EApp outer v2 (* well-typed via T_App_L2_Eff at R = [] *) + e_after := ERegion r2 v2 (* β-result: subst 0 v2 (ERegion r2 (EVar 0)) *) + + ===== Three theorems ===== + + - [e_before_typed] — the input types at outer type [T1_inner] + via T_App_L2_Eff with mode Affine. + - [e_step] — operational step S_App_Fun reduces e_before + to e_after. + - [e_after_untypable] — no L1 derivation exists for e_after at + the same outer type. By inversion: the only ERegion-producing + rules at non-TEcho output are T_Region_L1 and T_Region_Active_L1; + T_Region_Active_L1 requires [In r2 []] (fails); T_Region_L1's + body premise requires v2 typed at [r2; nil], which only + [T_Lam_L1_*_Eff] can produce, and both rules' side condition + [forall r, In r [r2] -> In r R_in_v = []] is contradicted by + [In r2 [r2]]. + + ===== Owner-directive compliance ===== + + - Does not modify [Semantics.v] or [Counterexample.v] (the legacy + soundness-gap artifacts). + - Does not patch [Typing.v]. + - Does not close any residual [Semantics_L1.v] admit. + - Adds NEW infrastructure (a new file in [formal/]) orthogonal + to legacy admits, mirroring the precedent of [Counterexample.v] + for the legacy preservation. + - No new [Axiom] or [Admitted] markers. *) + +From Ephapax Require Import Syntax Typing TypingL1 Modality Semantics Semantics_L1 TypingL2. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Import ListNotations. +Open Scope string_scope. + +Section CounterexampleL2. + + Definition r2 : region_name := "r2". + + (** Substituee type — a TFunEff lambda with empty input region env. *) + Definition T1_inner : ty := + TFunEff (TBase TUnit) (TBase TUnit) [] []. + + (** Outer lambda: takes a [T1_inner]-typed argument, returns it + inside a fresh-region scope [ERegion r2]. The bound variable + is referenced at de Bruijn index 0 inside the region scope. *) + Definition outer : expr := + ELam T1_inner (ERegion r2 (EVar 0)). + + (** Argument: a TFunEff lambda of type [T1_inner]. The body + [EUnit] is trivially typed at any R. *) + Definition v2 : expr := + ELam (TBase TUnit) EUnit. + + (** Pre-step term. *) + Definition e_before : expr := EApp outer v2. + + (** Post-β term: [subst 0 v2 (ERegion r2 (EVar 0))] + [= ERegion r2 (subst 0 v2 (EVar 0))] (* ERegion isn't a binder *) + [= ERegion r2 v2] (* EVar 0 substitutes to v2 *) *) + Definition e_after : expr := ERegion r2 v2. + + (** Helper: v2 types at [T1_inner] at any R (it's a closed value + whose formation side condition has R_in_v = [] so [R ⊆ []] + means R = []). For the proof below we only need v2 at R = [] + and at R = [r2] — the latter is what fails. *) + + Lemma v2_typed_at_empty : + has_type_l1 Affine [] [] v2 T1_inner [] []. + Proof. + unfold v2, T1_inner. + eapply T_Lam_L1_Affine_Eff with (u := false). + - intros r Hr; inversion Hr. + - apply T_Unit_L1. + Qed. + + (** Outer lambda is well-typed at [TFunEff T1_inner T1_inner [] []]. *) + + Lemma outer_typed : + has_type_l1 Affine [] [] outer + (TFunEff T1_inner T1_inner [] []) [] []. + Proof. + unfold outer. + eapply T_Lam_L1_Affine_Eff with (u := false). + - intros r Hr; inversion Hr. + - eapply T_Region_L1 with (R_body := [r2]). + + intros Hr; inversion Hr. + + simpl. intros Hr. inversion Hr. + + left; reflexivity. + + eapply T_Var_Unr_L1. + * unfold ctx_lookup; simpl. reflexivity. + * reflexivity. + Qed. + + (** ===== (a) e_before is well-typed via T_App_L2_Eff ===== *) + + Lemma e_before_typed : + has_type_l2 Affine [] [] e_before T1_inner [] []. + Proof. + unfold e_before. + eapply T_App_L2_Eff. + - apply L2_lift_l1. exact outer_typed. + - apply L2_lift_l1. exact v2_typed_at_empty. + Qed. + + (** ===== (b) The β-step from e_before to e_after ===== *) + + Lemma e_step : + forall mu, step (mu, [], e_before) (mu, [], e_after). + Proof. + intros mu. unfold e_before, e_after, outer. + (* [subst 0 v2 (ERegion r2 (EVar 0))] reduces to [ERegion r2 v2] + by the [subst] Fixpoint (ERegion is not a binder so no shift). *) + change (ERegion r2 v2) with (subst 0 v2 (ERegion r2 (EVar 0))). + apply S_App_Fun. unfold v2. apply VLam. + Qed. + + (** ===== (c) e_after does NOT type at the same outer type ===== + + No L1 derivation exists for [[] ; [] |=L1[Affine] e_after : + T1_inner -| ?R_out; ?G_out]. + + Proof by inversion on the assumed derivation. ERegion expressions + are produced by exactly four constructors: + - [T_Region_L1] — output type [T] (matches T1_inner) + - [T_Region_Active_L1] — output type [T] (matches but requires + [In r2 []], false) + - [T_Region_L1_Echo] — output type [TEcho T] (≠ T1_inner) + - [T_Region_Active_L1_Echo] — output type [TEcho T] (≠ T1_inner) + + The two Echo cases discriminate on the output-type equation. + The T_Region_Active_L1 case fails [In r2 []]. + The T_Region_L1 case requires v2 typed at [r2; nil]; v2 = ELam + types only via [T_Lam_L1_*_Eff], both of whose side conditions + [forall r, In r [r2] -> In r R_in_v = []] are contradicted by + [In r2 [r2]]. *) + + Lemma e_after_untypable : + forall R_out G_out, + ~ has_type_l1 Affine [] [] e_after T1_inner R_out G_out. + Proof. + intros R_out G_out Ht. + unfold e_after, v2, T1_inner in Ht. + inversion Ht; subst. + - (* T_Region_L1 case: body v2 typed at [r2;nil]. *) + match goal with + | [ Hbody : has_type_l1 _ (r2 :: _) _ (ELam _ _) _ _ _ |- _ ] => + rename Hbody into Hv2_inner + end. + inversion Hv2_inner; subst. + (* Only T_Lam_L1_Affine_Eff survives — T_Lam_L1_Linear / _Affine + produce TFun (discriminated), and T_Lam_L1_Linear_Eff is mode + Linear (discriminated against Hv2_inner's Affine mode). *) + match goal with + | [ Hside : forall r, In r (r2 :: nil) -> In r nil |- _ ] => + specialize (Hside r2 (or_introl eq_refl)); inversion Hside + end. + - (* T_Region_Active_L1 case: requires In r2 nil, false. *) + match goal with + | [ Hr2_in_R : In r2 nil |- _ ] => inversion Hr2_in_R + end. + Qed. + + (** ===== Soundness-gap witness ===== + + The three lemmas above ([e_before_typed] + [e_step] + + [e_after_untypable]) jointly witness preservation_l2's failure + for the TFunEff-substituee-inside-fresh-region class. No + top-level conjunction theorem is stated because [has_type_l2] + is Type-sorted (it is proof-relevant per L2's design) while + [step] and [~ has_type_l1] are Prop, so a Prop-conjunction over + the three would require either a [prod]-based product or + [inhabited]-wrapping. Keeping them as three separate lemmas + preserves the strongest form of each statement. *) + +End CounterexampleL2. diff --git a/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md b/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md index e064d813..0a9696c1 100644 --- a/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md +++ b/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md @@ -159,6 +159,50 @@ With the substitution machinery in place, the T_App_L2_Eff β-case in `preservat `EPair` / `EInl` / `EInr` / `EEcho` of non-linear components. Sub-component analysis. May require additional retype machinery. Realistically multiple sessions of work. +## Phase 4c addendum (2026-05-30) — conditional preservation_l2 for TFunEff β + +Prototyping Phase 4c on paper (after Phase 4a / 4b landed at PRs #228 / #233) revealed a structural soundness gap that requires a **conditional** preservation_l2 statement for the TFunEff β-case. `formal/Counterexample_L2.v` mechanises the witness. + +### The obstacle (mechanised in `Counterexample_L2.v`) + +For any TFunEff lambda body that introduces a fresh region via `ERegion` AND references the substituted variable inside that region scope, β-reduction does **not** preserve typing: + +``` +T1_inner = TFunEff TUnit TUnit [] [] (* substituee type, R_in_v = [] *) +outer = ELam T1_inner (ERegion r2 (EVar 0)) (* body introduces fresh r2 *) +v2 = ELam TUnit EUnit (* a value of type T1_inner *) +e_before = EApp outer v2 (* well-typed via T_App_L2_Eff at R = [] *) +e_after = ERegion r2 v2 (* β-result: subst 0 v2 (ERegion r2 (EVar 0)) *) +``` + +`e_before` types (Qed: `e_before_typed`); `e_step` reduces it to `e_after` (Qed: `e_step`); `e_after` does not type at the same outer type (Qed: `e_after_untypable`). The mechanism: T_Region_L1's `~ In r (free_regions T)` premise prevents the fresh `r` from being in `R_in_v` (since `R_in_v ⊆ free_regions(TFunEff)`). After β-substitution, the inner expression becomes a TFunEff value that must re-type at `r :: R`, requiring `r ∈ R_in_v` (false). + +### Resolution: Phase 4c ships **conditionally** + +Preservation_l2 for the T_App_L2_Eff β-case holds **only** for programs satisfying: + +``` +regions_introduced_by(ebody) ⊆ R_in_v +``` + +where `regions_introduced_by` is the `Fixpoint` already landed in `Syntax.v` (PR #230), `ebody` is the outer lambda's body, and `R_in_v` is the substituee's TFunEff input region env. + +The Phase 3b substitution lemma (`subst_typing_gen_l1_m_tfuneff`) ships with this precondition; the Phase 4c β-case wrapper propagates it. Programs not satisfying the precondition are a **documented soundness-gap subclass** — they witness the same fundamental "scoped resource cannot escape its scope" limitation that motivated the four-layer redesign in the first place. + +### Three resolution paths (broader than original (a)/(b)/(c) options) + +1. **Conditional preservation_l2 (recommended)**: Phase 3b lemma takes the precondition; Phase 4c β-case requires it; programs outside form a documented soundness-gap class. This is what `Counterexample_L2.v` justifies. Aligns with the legacy `Counterexample.v` precedent (preservation holds modulo a structural constraint that legitimate programs satisfy). +2. **Region-polymorphic TFunEff**: change the type system so `TFunEff T1 T2 R_in R_out` permits implicit region extension at use sites. Major type-system change; defers to a future redesign. +3. **L2 region-transfer combinator**: add an L2 typing rule that explicitly transfers a fresh region into a TFunEff lambda's R_in for the duration of a scope. Adds L2 expressiveness; defers to a future PR. + +### What ships in the Phase 4c PR + +- `formal/Counterexample_L2.v` — three Qed lemmas mechanising the soundness gap. +- This addendum to `SUBST-LEMMA-GENERALIZATION-DESIGN.md`. +- STATE.a2ml refresh to reflect the conditional path. + +Phase 3b implementation (the ~400-line `subst_typing_gen_l1_m_tfuneff` lemma body) and Phase 4c β-case wrapper remain follow-up work — but the design constraint they must satisfy is now mechanically witnessed. + ## What this session ships This design document only. No code changes. STATE.a2ml shifts `next_action` to "Phase 1: implement `ground_nonlinear_retype_l1_m` per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`". diff --git a/formal/_CoqProject b/formal/_CoqProject index 97720952..5ef32368 100644 --- a/formal/_CoqProject +++ b/formal/_CoqProject @@ -13,4 +13,5 @@ Counterexample.v Echo.v Modality.v TypingL2.v +Counterexample_L2.v L4.v