ch:identity-types: ch:identity-types

Problem and invariant. Construct the J-premise checking required by the seminar. Maintain the invariant that identity elimination is accepted only when every locally checked premise represented by the finite model holds.

Representation. Use a finite Expr syntax with endpoint variables X and Y, path variable P, reflexivity, identity, and one motive node. scoped checks the generic context [X,Y,P]; substituteReflexivity performs the actual simultaneous substitution Y := X and P := Refl X. The branch is accepted only when structural comparison matches that substituted motive.

First complete version. Check endpoint scope, then path scope, then the reflexive branch after both endpoint substitutions. After each stage, add one positive case and one nearby malformed case before extending the syntax.

Observable result. The accepted corpus prints four named PASS lines and then All 4 Chapter 77 corpus cases passed. A rejected input is represented by a false decision; the main oracle negates that result when rejection is expected.

A failing version. Skip the reflexive-branch substitution check. This mutation still typechecks, but changes at least one named oracle, so the inline test harness exits nonzero.

Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact five-line run transcript, and an empty audit. Restore the accepted source after replaying the mutation and repeat all four commands.

Mathematical boundary. The program decides the finite representation and cases just described. It does not prove the chapter’s general theorem; that proof remains the local argument or exact import in the main text.