Conversation
Id now takes two type codes A and B (both in U_{!,l}) with arguments
t : El A and u : El B, so Id A B t u expresses heterogeneous equality.
Idrefl A t : Id A A t t.
Updated the Id former, its subst rule, all Id-Nat computation rules, and
the id_injectivity list, plus the consumers in Cast.v (cast's Id-over-
universe premises, cast-Nat rules, castrefl) and Computations.v (Id-Nat-00).
Id.vo / Cast.vo / Computations.vo all build.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
Adds the observational-equality computation rules for the heterogeneous Id whose two type arguments have DIFFERENT head constructors (-> Empty), plus the tractable same-head universe (type-equality) rules. Computations.v (term layer, level 0): Id-Nat-Pi / Id-Pi-Nat : Id between Nat and a Pi code = Empty. IdUniv.v (new; universe layer, A=B=u0 rel so t,u are level-0 type codes): Id-U-Nat-Nat : Nat ~ Nat = sUnit Id-U-Nat-Pi / Id-U-Pi-Nat : Nat ~ Pi = Empty (type-level head clash) Id-u0-Pi / Id-Pi-u0 : universe code ~ Pi at level 1 = Empty Base composes cast++id++pi++sigma++nat++base++subst++info (new combination). Still deferred (OOM on the e-graph wf/inference pass, as documented): Id-Pi (funext, Pi~Pi term layer) and Id-U-Pi-Pi (structural Pi~Pi at the universe). Documented in-file; to be attempted next / on a larger machine. Computations.vo and IdUniv.vo both build. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
Records that the funext rule Id-Π is deferred for TWO reasons: (1) the general heterogeneous form needs cast to bridge distinct domains, since Id requires its two type args at a common level/relevance (so inner Id F1 F2 a1 a2 is otherwise ill-formed) — cast needs the deferred Idsym/transp; and (2) even the restricted same-domain form OOMs the e-graph pass (>500s), the transp wall. Notes that the head-clash rules (Id-Nat-Pi/Id-Pi-Nat) are the done, tractable part. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
transp A P t u e s : El(P u) — transport a proof s : El(P t) along a proof e : Id A A t u, for a proof-irrelevant predicate P : El A -> SProp. This was previously deferred as OOMing the structural wf prover at 6.93GB; with the improved e-graph performance it now elaborates via elab_rule and peaks at ~0.57GB. Added transp to id_injectivity. Removed the obsolete deferral note. Downstream Cast.vo / Computations.vo / IdUniv.vo all rebuild clean against the extended ott_id. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
Idsym (Id.v): symmetry of heterogeneous Id — Idsym A B t u e : Id B A u t. Posited term former (coherent by proof irrelevance); the flip needed to state the codomain equalities of the structural rules. Elaborates via elab_rule. Id-Π (Computations.v): homogeneous function extensionality Id (Π F B)(Π F B) f g = Π(a:F). Id B B (f·a)(g·a) [proof-irr Π] Pre-elaborated (id_pi_funext_rule, modeled on Pi.v's `Pi_rel eta`) and added via push_rule; the inner equality is on the rel codomain so no cast is needed. The old note said this OOMed >500s; with the perf improvements the wf-check peaks at ~0.63GB. The fully heterogeneous funext (distinct domains) is documented as still open — it needs the domain equality / cast, i.e. Id-U-ΠΠ. Whole OTT stack (Id/Cast/Computations/IdUniv) rebuilds green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
id_u_pi_pi_rule (IdUniv.v): the structural universe rule
Id_U (Π F1 B1)(Π F2 B2)
= Σ (Id_U F1 F2). Π(a2:F2). Id_U (B1[cast F2 F1 (Idsym ef) a2]) (B2[a2])
fully pre-elaborated (cast-based single-binder form; casts the argument
contravariantly across the domain equality using the now-available cast+Idsym).
The Definition compiles; the push_rule (compute_wf_rule) is left COMMENTED.
Unlike transp/Idsym/funext — which the perf improvements brought well under
budget (<0.8GB, seconds/minutes) — pushing this rule runs the e-graph wf
saturation >25min without terminating at a flat ~0.77GB (a saturation-time
wall, not OOM; it is the deepest term in the development). The authored term is
retained so a faster wf-check (or the structural wfstep prover) can land it by
uncommenting one line. cast-Π is deeper still and stays deferred on the same
basis. Whole OTT stack builds green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
Idcong maps a term b with one extra variable in context (b : El B in ext G (El A), codomain code B may itself depend on the variable) to a proof of congruence: given endpoints t,u : El A and e : Id A A t u, conclude Id (B[t]) (B[u]) (b[t]) (b[u]). The substituted codomains make the target heterogeneous, which is exactly why Id was generalized. Idrefl A t : Id A A t t is the degenerate case (b := hd, B := A weakened, both ignoring the endpoints). Like Idsym/transp, Idcong is a posited term former, coherent by proof irrelevance (it lives in SProp). Landed via elab_rule; wf-check terminates fast at ~1GB (no saturation wall). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
Directed reduction rules for Idcong (congruence), pushing under each
neutral/normal form and landing at a term that matches the corresponding
Id-type reduction. The Nat/base fragment (all self-contained at the Id.v
layer — needs only Idrefl and the Id-Nat-SS reduction already in this file):
- Idcong-var: cong hd e = e
(neutral base case: b := hd, B := wkn A, both instances
collapse to the endpoints, Id (B[t])(B[u])(hd[t])(hd[u]) =
Id A A t u)
- Idcong-zero: cong zero e = Idrefl Nat zero
(nullary constructor; Id Nat Nat zero zero reduces to sUnit)
- Idcong-suc: cong (suc n) e = cong n e
(pushes under suc, transported across Id-Nat-SS)
- Idcong-wkn: cong (wkn C) (wkn c) e = Idrefl C c
(general leaf: a closed subterm ignores the variable, so cong
bottoms out at reflexivity for any type)
All four added via elab_rule (surface form; bare wkn/hd elaborate), peak
~2GB, no saturation wall. The universe-code cases (cong Nat / Pi codes,
needs u0 + Id-U-Pi-Pi) and the Pi term cases (cong lam / app, needs
heterogeneous funext + cast-Pi) remain blocked on the deferred chain.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0119nFrfTeXSscbZjZA3zqQR
The heterogeneous observational identity type, in the form the
normalization proof needs. Kept SEPARATE from Lang/OTT/Id.v, which stays
the exploratory playground (Idrefl/Idsym/transp, and the Cast / IdUniv /
Computations chain that is explicitly out of scope).
Two term rules and thirteen equations, 14 of the 15 wf-checked:
Id G l A B t u : U G irr L0 -- heterogeneous, A,B RELEVANT codes at a
common level. There is no Id between irrelevant codes and none is
wanted; proof irrelevance already equates all their inhabitants.
Idcong A B b t u e -- the only proof former.
No Idrefl: Idcong strictly generalizes it, via a body that ignores the
bound variable, with Id-Nat-00 supplying the trivial proof.
No equations for Idcong AT ALL -- not the substitution commutation, not
the rules pushing it under a constructor. Each equates two inhabitants
of a code at U _ irr _, so ott_proofirr_el proves it; they are derived in
Gluing/Dtt/Eqns.v rather than posited. This is the one place the "a
former with no subst commutation is stuck under an explicit substitution"
lesson of design.md 9a does not apply, because irrelevance supplies the
equation the missing rule would have.
The computation table is complete, so an Id whose arguments are canonical
always reduces and the only normal Id codes are the neutral ones: the Nat
family (00/0S/S0/SS), the Nat-vs-Pi clashes, four Pi-Pi domain-index
clashes, and function extensionality.
Funext is heterogeneous and quantifies over a PAIR of arguments plus a
proof they are equal, which is what lets it be stated without a cast --
Cast's u0 is a code whose El is a universe and breaks the code grammar.
The premise is required for consistency at relevant domains: without it
the rule inhabits Id N N a1 a2 for arbitrary a1,a2, hence Empty. At
irrelevant domains it genuinely is unnecessary, so that is a separate
two-binder rule; that one is verified. The three-binder relevant-domain
rule is authored and typechecks as syntax, but its wf-check is still
open -- see the next commit.
design.md gains section 12, including 12d: Idcong must be an
UNCONDITIONAL neutral. Making it neutral only when its body is neutral
does not close -- at a lam body the reduced type needs a congruence in
two variables at once, which single-binder Idcong cannot express and
which cannot be assembled from two one-variable congruences without a
cast. Unconditional neutrality lets the type-directed eta /
proof-irrelevance machinery do the work instead.
12e records the consequence for the proof: Id's Nat rules dispatch on
element terms, so the rigid model of Layer 0.5 must erase them, and then
Id-Nat-00 and Id-Nat-0S are jointly REFUTABLE. Rigid/RigidOk/Inj are
retired in favour of a two-sided (PER) logical relation.
…periment design.md 14: normalization becomes functional and every irrelevant type reifies to a single token *. * NEW Gluing/Dtt/Values.v -- the Val/ValCode/ValTy/ValEnv/ValNe/NeCode/ ValVar block over *-collapsed values. Named representatives with an eq_term premise become COMPUTED ones (wkTy / instC, section parameters). Drops nfet_ne_empty / nfet_lam_irr / neet_app_irr / neet_idcong and oIdcongTy for one val_irr clause; keeps the five NeCode clauses verbatim. (E1) ValCode_irr_shape and the *-collapse Val_irr_star are proved. * NEW Gluing/Dtt/WkVal.v -- T3. wkV (weakening of code values) is an ordinary Fixpoint and wkV_sound goes through with NfWk.v's eq_pi_rel_wk / eq_pi_irr_wk / Wk_liftC slotting in unreshaped. The NEUTRAL case is carried as a named Context hypothesis: it cannot be a Gallina function (guard checker rejects the code/weakening mutual recursion). * DELETED Rigid.v, RigidOk.v, Inj.v (design.md 12e: two of the rigid model's obligations are refutable once Id is in). VarT_shape -- the only lemma in Inj.v with no dependence on the rigid model -- is rescued into NormalForms.v, with NeET_shape and NeCode_shape alongside it. All three files build; Print Assumptions on every new result is "Closed under the global context". Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
… (a)) WkRel.v. Four mutual judgements -- WkTy / WkTm / WkVar / VarTy -- and Wk_det, all four determinism conjuncts, axiom-free. The stuck-Id and element clauses that WkVal.v could not reach are here: wktm_id weakens an Id's two codes and its two ELEMENT endpoints in one clause, which is all that design.md 14d's "code/element mutual recursion" amounts to once the *-collapse is in. Two things the block forced, neither of them anticipated: * CODES AND ELEMENTS SHARE ONE JUDGEMENT (WkTm). Their head symbols are pairwise disjoint, so nothing is lost and determinism becomes a discrimination argument. Only VARIABLES need a type index, because they are the only subjects that introduce an annotation not already stored in the term. That collapses the naive 13-inductive block to 4. * VarTy IS FORCED. With only a syntactic IsVar side condition, WkTm determinism is FALSE: wkvar_wkn emits exp_subst wkn i A x, whose annotation is a type the relation never pinned. VarTy G i A x pins it, and it is exactly Values.v's ValVar minus the value-hood premises -- i.e. where Values.v's wkTy parameter goes when this is wired up. The circularity (WkTm det needs variable-type uniqueness needs WkTy det needs WkTm det) is closed by strengthening the WkVar conjunct to conclude i = i2 and A = A2, so every use is an IH of a sub-derivation. WkVal.v records that (a) was taken and why (b) was not needed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
Rz.v. Rz G i A v e ("v realizes e"), and
Rz_eqt : Rz G i A v e1 -> Rz G i A v e2 -> eqt (sExp G i A) e1 e2
Qed, with 0 NEW axioms (everything rests on exactly the tracked
IdFunextRelAXIOM.ott_id_funext_rel_wf, via ott_dtt_wf, as any file using
estep/cong_step/wf_by does). Needs neither Nrm nor the weakening layer,
which is why it was worth doing first: had it failed, the erasure would
have been wrong.
Both erasable positions of (E2) are discharged directly:
* emptyrec_star_eqt is design.md 14a VERBATIM -- the two Emptyrecs that
refuted NfET_inj are provably equal, at a relevant type. Emptyrec_cong
+ eq_proof_irr.
* app_rel_star_eqt, the same at an irrelevant domain.
rz_id is in the block on purpose: it is the 14e chain (code -> Id ->
relevant element -> Emptyrec/app_rel -> *), so the reachability of * from
a code is exercised rather than assumed away.
Proof irrelevance is spent in exactly one place, the rz_star case.
Rz is conversion-FREE; RzE is the closure, and RzE_eqt is three lines. A
rz_conv clause inside the inductive would appear on both sides of Rz_eqt
and the leaf-vs-conversion case has no induction hypothesis.
Two facts Eqns.v/Wf.v were missing, because both predate the Id fragment
(neither mentions oIdEq at all): wf_IdEq and IdEq_cong, one wf_by and one
cong_step in the files' own idiom. They belong upstream.
SCOPE: type arguments are held fixed between value and term, which keeps
the relation single-sorted; app_rel is outside the block for that reason
(its conclusion sort mentions its argument) and is covered by the
standalone lemma.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
Both files predated ott_id_cong and mentioned oIdEq nowhere, so every
consumer was rolling its own on demand. Front-loaded, per the plan,
rather than one at a time:
Wf.v wf_IdEq (+ dtt_wf hint)
Eqns.v IdEq_cong, eq_Id_subst,
eq_Id_Nat_00 / _0S / _S0 / _SS
Rz.v wft_c0, wf_IdEq_c (the next0 bridge -- see below)
Wf.vo and Eqns.vo rebuild; Rz.v now consumes them and drops its local
copies. 0 new axioms.
TWO THINGS WORTH KNOWING.
* THE FRAGMENT'S INDEX SPELLINGS ARE NOT UNIFORM, and I found that by
experiment, not by reading the rules -- design.md 9b's mismatch again,
since infer_rule re-extracts each conclusion sort with mk_weight and the
tie-break depends on the rule's own right-hand side:
"Id", "Id subst", "Id-Nat-00" stored at iEl rel L1
"Id-Nat-0S/-S0/-SS" stored at iCode L0 (= sCode)
i.e. the rules whose RHS is a Pi-shaped code got one spelling and those
whose RHS is Empty or an Id got the other. Documented in Eqns.v with a
warning not to "tidy" them into a single form.
* THE next0 BRIDGE CANNOT GO UPSTREAM. wft_c0 (an irrelevant-L0 code at
the iota-L1 spelling is one at the next-L0 spelling) needs both a wf_
lemma and a congruence, and Wf.v and Eqns.v are SIBLINGS over Syntax.v --
neither imports the other. It stays in the first file importing both,
which is Rz.v today, and should move to whatever bridge file replaces
NfTyping.v. Noted in both places.
wf_Idcong and Idcong_cong are deliberately NOT included: the stored
spelling of Idcong's conclusion sort is not the obvious one (NormalForms'
oIdcongTy does not unify) and nothing needs them -- under the *-collapse
an Idcong is a proof, so its value is * and the value layer never inspects
it. Wf.v records why, and to pin it when something first asks.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
Step 2 as scoped. oStar moves Values.v -> WkRel.v (Require Export, so
downstream sees both), flipping the dependency; ValVar's wkTy parameter
becomes a WkTy premise:
valvar_hd : ValEnv G -> ValTy G i A ->
WkTy (ext G i A) G (wkn G i A) i A A' ->
ValVar (ext G i A) i A' (hd G i A)
Determinism (WkRel.Wk_det) is what makes A' THE weakening rather than one
of them, which is the whole of the turn to functional content. Two
bridges added: ValVar_VarTy (a value variable is a variable) and
ValVar_type_unique (its type is determined by its context and itself,
Wk_det's fourth conjunct transported).
instC is now the SOLE remaining parameter, used only as the type index of
valne_app_rel. WkRel.vo / Values.vo / Rz.vo all build, 0 new axioms.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
Correcting a claim this file made one commit ago. The instantiation relation is not a sibling of the weakening relation: WEAKENING NEVER CREATES A REDEX -- it only shifts -- which is why WkRel.v is purely structural and was cheap. INSTANTIATION substitutes a VALUE for a variable, and a value in a neutral's head position turns that neutral into a redex. So instantiation must EVALUATE, and it is a fragment of the normalizer, not a sibling of weakening. Located exactly. Substituting an element into a value CODE is structural at Nat/Empty/Pi_rel/Pi_irr AND at code variables -- a code variable's type is a universe, but the de Bruijn-0 variable of extC G rF lF F has type El _ rF lF F[wkn], so a code variable is never the one substituted and always merely strips. An Id stuck on a neutral CODE stays stuck for the same reason. It breaks in exactly one place: necode_id_nat_l/_r, whose stuck endpoint is an ELEMENT at El _ rel L0 (Nat _) and CAN be the 0-variable (when F is Nat), so substituting zero or suc n fires "Id-Nat-00"/"-0S"/"-SS"; symmetrically an endpoint app_rel whose head is the 0-variable becomes a beta-redex under a lam_rel. This is design.md 14d confirmed from the substitution side, and it says what the Id fragment actually costs: NfWk.v:3139's NfCode_csubst -- "the code grammar is a free algebra closed under substitution STRUCTURALLY" (NormalForms.v:66) -- held only because pre-Id codes contain no elements. Consequence for the block: it needs the SEMANTIC operations too, an application judgement (beta) and an Id judgement (the whole 12b table), not just the substitution ones. Five or six mutual judgements, so the factorization survives; the growth is in clauses. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
The table (design.md 12b) is a dozen clauses and is the part of this
development most likely to contain a transcription error -- and an omitted
case there does not fail to typecheck, it fails much later as a stuck
determinism proof. So the case analysis goes in FIRST, stated over head
symbols and proved once, so that writing the table against it turns an
omission into a missing case:
ValCode_rel_shape the relevant canonical codes are EXACTLY Nat and
Pi_rel (the dual of ValCode_irr_shape)
Val_nat_shape the values at Nat are EXACTLY zero, suc and neutrals
Val_pi_rel_shape at a Pi_rel type the only value is a lam_rel (eta) --
what the funext clause needs to know its endpoints
are lambdas and not neutrals
NeCode_head a neutral code is hd-, exp_subst- or Id-headed
NeCode_not_nat / NeCode_not_pi_rel
Together: the analysis is 3x3 in the codes and, at Nat, 3x3 in the
endpoints. DISJOINTNESS needs no lemma -- the shapes are pairwise
distinct con heads.
One asymmetry worth recording, since it is the eta rule showing up as a
proof obligation: in Val_nat_shape the val_ne case is ABSORBED (a neutral
at Nat is exactly the third alternative), but in Val_pi_rel_shape it must
be REFUTED, because eta leaves no neutral alternative at a Pi_rel type for
it to land in. That is why NeCode_not_pi_rel has to exist.
Axiom-free. Values.vo and Rz.vo build.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
Weakening never creates a redex, so WkRel.v is purely structural.
Instantiation substitutes a VALUE for a variable, and a value in a
neutral's head position turns that neutral into a redex, so this
relation must EVALUATE (design.md 14k). Five mutual judgements:
InstTy / InstTm / InstVar mirroring WkRel.v
AppV the value of an application (beta)
IdV the section-12b Id computation table
The block sits ON TOP of the closed weakening block: no clause of
WkRel.v mentions instantiation, and exactly one clause here mentions
weakening.
DESIGN POINTS, all inherited from WkRel.v and all load-bearing.
* Codes and elements SHARE InstTm. Their head symbols are pairwise
disjoint, which turns determinism into a discrimination argument.
* No type index except at variables -- and here not even there. WkRel's
fourth judgement VarTy was forced because wkvar_wkn EMITS an annotated
exp_subst; no clause here emits a new annotation, so InstVar needs no
type index and the block is FIVE judgements, not six.
* Dispatch is head-directed. InstTm's variable clauses are split
hd/exp_subst, as wktm_var_hd/wktm_var_wkn was; InstVar dispatches on
the SUBSTITUTION first (oId / oSnoc / oCmp), which is what makes
instvar_id's unconstrained subject harmless.
* The *-collapse keeps the irrelevant fragment free: one insttm_star.
EVALUATION HAPPENS IN EXACTLY TWO CLAUSES, insttm_app_rel (through
AppV) and insttm_id (through IdV). Everything else -- Nat, Empty,
Pi_rel, Pi_irr, zero, suc, *, lam_rel, Emptyrec, and code variables --
is structural, confirming 14k from the substitution side.
THE Id TABLE is 16 clauses: two stuck-on-a-neutral-code, six for
Nat/Nat (00 / 0S / S0 / SS / neutral endpoint either side), two for the
head clash Nat-vs-Pi, four for mismatched Pi domain indices, and the
two funext clauses. Transcribed from the compiled rules of
Lang/OTT/IdComp.v and Lang/OTT/IdFunextDefs.v, not from the surface
notation. Three things the transcription turned up:
- The four clash rules already PARTITION. IdComp.v's comment says
they "overlap, which is harmless"; as compiled, -rel-irr/-irr-rel
pin the two relevances to distinct LITERALS while -L0-L1/-L1-L0
share one relevance METAVARIABLE, so relevance-mismatch and
level-mismatch are mutually exclusive. No restructuring needed.
- Id-Nat-Pi / Id-Pi-Nat are stated at l = L0 with the Pi's own lG
pinned to L0. That is forced (Nat is a code at L0 only, and an
Id's two codes share a level), not a restriction.
- The IRRELEVANT funext clause takes oStar, not variables, for the
two bound arguments: they sit at an irrelevant El, where the only
value is *. The choice is also immaterial, since a value over
oExtC G irr lF F cannot mention that context's de Bruijn-0
variable at all.
DETERMINISM (13b's property (D)) is proved by WkRel.v's own argument,
with two additions: WkTm premises carry no induction hypothesis and go
through WkTm_det explicitly, and the clauses separated only by a
neutrality premise are killed by five refutation lemmas
(NeCode_not_nat, NeCode_not_pi_rel, and the three ValNe_not_* proved
here from ValNe_shape). Axiom-free. Totality is NOT attempted: it is
13b's (T) and belongs to the model, and it is where 14k's relocated
lexicographic measure comes back.
Determinism does not witness COMPLETENESS -- a table with a case
missing is still deterministic -- so IdV_code_cases and
IdV_pi_index_cases exhibit the two case analyses the clauses were
written against and show them exhaustive. The third axis, the
endpoints at Nat/Nat, is Values.v's Val_nat_shape verbatim.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJEPP2PBDQPZ5odzB4gXga
ott_dtt is now
ott_id_cong ++ ott_proofirr_el ++ ott_subst_commute ++ ott_pi ++ ott_nat
++ ott_base ++ subst_ott ++ ott_info (89 rules)
and `Print Assumptions ott_dtt_wf` is "Closed under the global context".
THE FRAGMENT IS SPLIT ACROSS FIVE FILES, AND THAT IS A PERFORMANCE FIX.
compute_wf_rule checks each rule against its PREFIX and its cost grows
sharply with that prefix, so each rule is now checked against the smallest
prefix it needs and the pieces are concatenated, with
Core.lang_ext_monotonicity lifting a rule verified against a small prefix
into its position. Measured, same machine:
BEFORE one Derive, rules sequenced > 4 h, killed, unfinished
AFTER IdCore.v Id, Id subst 35 s
IdComp.v Idcong + 10 computations 3.5 min
IdFunextDefs.v the two rule DEFINITIONS 1.3 s
IdFunextIrr.v 2-binder funext } siblings ~12 min
IdFunextRel.v 3-binder funext } common base 2h13m
IdCong.v assembly, three lifts 10 s
Syntax.v 89-rule ott_dtt + wf 12 s
Three effects, each a surprise:
1. A funext rule in a prefix is poison: the SAME 2-binder rule costs
~4 min with no funext ahead of it and >16 min with one. Making the
two funext rules SIBLINGS over a common base recovers it. They are
independent; only the authoring order made them a chain.
2. The split dissolves an elaboration constraint instead of trading
against it. Rules cannot merely be REORDERED for a smaller prefix:
with a funext rule in scope, infer_rule re-elaborates "Id-Nat-00" to
a DIFFERENT rule (the next L0 <-> iota L1 flip of design.md 9b;
measured, the inferred rules compare unequal and inference costs
5.6x more). Siblings over a COMMON base each elaborate as before.
3. Rule DEFINITIONS belong in their own file. IdFunextDefs.v costs
1.3 s and lets anything import a pre-elaborated rule without
triggering its check -- which is what makes probing a slow rule
possible, and what let a stand-in be swapped for a running proof.
ott_dtt_wf is COMPOSITIONAL (prove_by_lang_db over the fragments' own
wf_lang_ext lemmas), never compute_wf_lang: re-checking 89 rules ran
>15 min and growing, against 12 s for the assembly.
Also corrects IdComp.v's claim that the four Pi-Pi clash rules overlap.
They do not: the relevance-mismatch pair pins the two relevances to the
distinct literals rel/irr while the level-mismatch pair shares one
relevance metavariable, so the two families are mutually exclusive and
the four transcribe directly as the partition the value layer's Id table
needs for determinism.
design.md gains 12 (the fragment), 13 (why normalization must become
functional -- four cheaper routes refuted, not merely unproved), and 14
(the *-erasure: proof irrelevance is the eta rule of the irrelevant
types), including 14i, the negative result that generated injectivity
does NOT speed up the wf-check, and 14j, the split above.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Begins adding everything needed for the Id type. Preserves the normalization proof.