REL1 foundation: schema-based inductive + HIT CTypes (Lean side)
Adds schema-based inductive type encoding to the engine, supporting both
plain inductives (Nat, List, Bool) and HITs (S¹, propositional truncation,
suspensions) via a single CTypeSchema/CtorSpec/CTypeArg structure.
New CType constructor:
- .ind (S : CTypeSchema) (params : List CType)
New CTerm constructors:
- .dimExpr (r : DimExpr)
- .ctor (S, ctorName, params, args)
- .indElim (S, params, motive, branches, target)
New CVal constructors:
- .vctor (S, ctorName, params, evaluatedArgs)
- .vdimExpr (DimExpr)
New CNeu constructor:
- .nIndElim (S, params, motive, branches, neuTarget)
Five-way mutual block in Syntax.lean (CType, CTerm, CTypeArg, CtorSpec,
CTypeSchema) with Repr derivation post-hoc. Tag layout per
docs/INDUCTIVE_TYPES.md §6: old tags preserved (no shifting). Existing
62/62 smoke + property tests pass unchanged through Rust.
Substitution / dim-absent / endpoint handling:
Subst.lean — substDim, substDimExpr, equation lemmas,
substDim_eq_substDimExpr (mutual with .params helpers).
DimLine.lean — CTerm.dimAbsent + CType.dimAbsent (mutual w/ helpers
for list / branches / params). Plus all five
auxiliary mutual blocks: substDim_absent_aux,
substDimExpr_absent_aux, dimAbsent_after_substDim_aux,
substDim_comm_aux — for both CTerm and CType.
Eval.lean: ctor → vctor (eval'd args); indElim β-reduces on canonical
vctor target via vApp chain over branch body, otherwise stuck via
.nIndElim; dimExpr → vdimExpr. Path-ctor boundary firing and
recursive-arg IH wiring marked TODO REL1.1 (β-reduction works for
non-recursive ctors today).
Readback.lean: vctor → .ctor, vdimExpr → .dimExpr, nIndElim → .indElim.
FFITest.lean: cvalSummary / ctermSummary extended with new constructor
arms.
Topolei (sibling repo) has not yet been migrated — see
docs/INDUCTIVE_TYPES.md §9.1 for the per-file impact map.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Maximus Gorog
parent
f9e79b7b0d
commit
f27211f73f
7 changed files with 748 additions and 252 deletions
|
|
@ -75,6 +75,15 @@ mutual
|
|||
| .pair a b => a.dimAbsent i && b.dimAbsent i
|
||||
| .fst t => t.dimAbsent i
|
||||
| .snd t => t.dimAbsent i
|
||||
-- REL1 inductive-type constructors. Schema and ctor/elim *params*
|
||||
-- are static (caller-supplied externally to any binder we'd be
|
||||
-- substituting into) — same approximation as transp/comp's `A`.
|
||||
| .dimExpr s => s.dimAbsent i
|
||||
| .ctor _ _ _ args => CTerm.dimAbsent.list i args
|
||||
| .indElim _ _ motive branches target =>
|
||||
motive.dimAbsent i &&
|
||||
CTerm.dimAbsent.branches i branches &&
|
||||
target.dimAbsent i
|
||||
|
||||
/-- Helper: check that `i` is absent from every clause in a system. -/
|
||||
def CTerm.dimAbsent.clauses (i : DimVar) :
|
||||
|
|
@ -82,18 +91,38 @@ mutual
|
|||
| [] => true
|
||||
| (φ, u) :: rest =>
|
||||
φ.dimAbsent i && u.dimAbsent i && CTerm.dimAbsent.clauses i rest
|
||||
|
||||
/-- Helper: check `i` absent from every CTerm in a list (ctor args). -/
|
||||
def CTerm.dimAbsent.list (i : DimVar) : List CTerm → Bool
|
||||
| [] => true
|
||||
| t :: rest => t.dimAbsent i && CTerm.dimAbsent.list i rest
|
||||
|
||||
/-- Helper: check `i` absent from every branch body of an `indElim`. -/
|
||||
def CTerm.dimAbsent.branches (i : DimVar) :
|
||||
List (String × CTerm) → Bool
|
||||
| [] => true
|
||||
| (_, b) :: rest =>
|
||||
b.dimAbsent i && CTerm.dimAbsent.branches i rest
|
||||
end
|
||||
|
||||
def CType.dimAbsent (i : DimVar) : CType → Bool
|
||||
| .univ => true
|
||||
| .pi A B => A.dimAbsent i && B.dimAbsent i
|
||||
| .path A a t => A.dimAbsent i && a.dimAbsent i && t.dimAbsent i
|
||||
| .sigma A B => A.dimAbsent i && B.dimAbsent i
|
||||
| .glue φ T f fInv sec ret coh A =>
|
||||
φ.dimAbsent i && T.dimAbsent i &&
|
||||
f.dimAbsent i && fInv.dimAbsent i &&
|
||||
sec.dimAbsent i && ret.dimAbsent i && coh.dimAbsent i &&
|
||||
A.dimAbsent i
|
||||
mutual
|
||||
def CType.dimAbsent (i : DimVar) : CType → Bool
|
||||
| .univ => true
|
||||
| .pi A B => A.dimAbsent i && B.dimAbsent i
|
||||
| .path A a t => A.dimAbsent i && a.dimAbsent i && t.dimAbsent i
|
||||
| .sigma A B => A.dimAbsent i && B.dimAbsent i
|
||||
| .glue φ T f fInv sec ret coh A =>
|
||||
φ.dimAbsent i && T.dimAbsent i &&
|
||||
f.dimAbsent i && fInv.dimAbsent i &&
|
||||
sec.dimAbsent i && ret.dimAbsent i && coh.dimAbsent i &&
|
||||
A.dimAbsent i
|
||||
| .ind _ params => CType.dimAbsent.params i params
|
||||
|
||||
/-- Helper: check `i` absent from every CType in a parameter list. -/
|
||||
def CType.dimAbsent.params (i : DimVar) : List CType → Bool
|
||||
| [] => true
|
||||
| A :: rest => A.dimAbsent i && CType.dimAbsent.params i rest
|
||||
end
|
||||
|
||||
-- ── Absence → subst is identity: DimExpr level ───────────────────────────────
|
||||
|
||||
|
|
@ -201,6 +230,21 @@ mutual
|
|||
simp only [CTerm.dimAbsent] at h
|
||||
simp only [CTerm.substDim]
|
||||
rw [CTerm.substDim_absent_aux i r t h]
|
||||
| .dimExpr s, h => by
|
||||
simp only [CTerm.dimAbsent] at h
|
||||
simp only [CTerm.substDim]
|
||||
rw [DimExpr.subst_of_absent i r s h]
|
||||
| .ctor S c params args, h => by
|
||||
simp only [CTerm.dimAbsent] at h
|
||||
simp only [CTerm.substDim]
|
||||
rw [CTerm.substDim.list_of_absent i r args h]
|
||||
| .indElim S params motive branches target, h => by
|
||||
simp only [CTerm.dimAbsent, Bool.and_eq_true] at h
|
||||
simp only [CTerm.substDim]
|
||||
obtain ⟨⟨hm, hbr⟩, htg⟩ := h
|
||||
rw [CTerm.substDim_absent_aux i r motive hm,
|
||||
CTerm.substDim.branches_of_absent i r branches hbr,
|
||||
CTerm.substDim_absent_aux i r target htg]
|
||||
|
||||
/-- Helper: `substDim.clauses` is identity on clause lists whose every
|
||||
`(face, body)` pair has `i` absent. -/
|
||||
|
|
@ -216,6 +260,32 @@ mutual
|
|||
rw [FaceFormula.substDim_of_absent i r φ hφ,
|
||||
CTerm.substDim_absent_aux i r u hu,
|
||||
CTerm.substDim.clauses_of_absent i r rest hrest]
|
||||
|
||||
/-- Helper: `substDim.list` is identity on CTerm lists with `i` absent
|
||||
from every element. -/
|
||||
private def CTerm.substDim.list_of_absent (i : DimVar) (r : DimExpr) :
|
||||
(ts : List CTerm) →
|
||||
CTerm.dimAbsent.list i ts = true →
|
||||
CTerm.substDim.list i r ts = ts
|
||||
| [], _ => rfl
|
||||
| t :: rest, h => by
|
||||
simp only [CTerm.dimAbsent.list, Bool.and_eq_true] at h
|
||||
simp only [CTerm.substDim.list]
|
||||
rw [CTerm.substDim_absent_aux i r t h.1,
|
||||
CTerm.substDim.list_of_absent i r rest h.2]
|
||||
|
||||
/-- Helper: `substDim.branches` is identity on branch lists whose every
|
||||
body has `i` absent. -/
|
||||
private def CTerm.substDim.branches_of_absent (i : DimVar) (r : DimExpr) :
|
||||
(brs : List (String × CTerm)) →
|
||||
CTerm.dimAbsent.branches i brs = true →
|
||||
CTerm.substDim.branches i r brs = brs
|
||||
| [], _ => rfl
|
||||
| (n, b) :: rest, h => by
|
||||
simp only [CTerm.dimAbsent.branches, Bool.and_eq_true] at h
|
||||
simp only [CTerm.substDim.branches]
|
||||
rw [CTerm.substDim_absent_aux i r b h.1,
|
||||
CTerm.substDim.branches_of_absent i r rest h.2]
|
||||
end
|
||||
|
||||
/-- Generalised: `CTerm.substDim i r t = t` whenever `i` is absent from `t`,
|
||||
|
|
@ -230,49 +300,68 @@ theorem CTerm.substDimBool_of_absent (i : DimVar) (b : Bool) (t : CTerm)
|
|||
unfold CTerm.substDimBool
|
||||
exact CTerm.substDim_of_absent i _ t h
|
||||
|
||||
private def CType.substDim_absent_aux (i : DimVar) (b : Bool) :
|
||||
(A : CType) → CType.dimAbsent i A = true → CType.substDim i b A = A
|
||||
| .univ, _ => rfl
|
||||
| .pi A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.pi (CType.substDim i b A) (CType.substDim i b B) = CType.pi A B
|
||||
congr 1
|
||||
· exact CType.substDim_absent_aux i b A h.1
|
||||
· exact CType.substDim_absent_aux i b B h.2
|
||||
| .path A a t, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.path (CType.substDim i b A)
|
||||
(CTerm.substDimBool i b a) (CTerm.substDimBool i b t) =
|
||||
CType.path A a t
|
||||
congr 1
|
||||
· exact CType.substDim_absent_aux i b A h.1.1
|
||||
· exact CTerm.substDimBool_of_absent i b a h.1.2
|
||||
· exact CTerm.substDimBool_of_absent i b t h.2
|
||||
| .sigma A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.sigma (CType.substDim i b A) (CType.substDim i b B) =
|
||||
CType.sigma A B
|
||||
congr 1
|
||||
· exact CType.substDim_absent_aux i b A h.1
|
||||
· exact CType.substDim_absent_aux i b B h.2
|
||||
| .glue φ T f fInv sec ret coh A, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.glue (φ.substDim i (if b then DimExpr.one else DimExpr.zero))
|
||||
(CType.substDim i b T)
|
||||
(CTerm.substDimBool i b f) (CTerm.substDimBool i b fInv)
|
||||
(CTerm.substDimBool i b sec) (CTerm.substDimBool i b ret)
|
||||
(CTerm.substDimBool i b coh)
|
||||
(CType.substDim i b A) =
|
||||
CType.glue φ T f fInv sec ret coh A
|
||||
obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h
|
||||
rw [FaceFormula.substDim_of_absent i _ φ hφ,
|
||||
CType.substDim_absent_aux i b T hT,
|
||||
CTerm.substDimBool_of_absent i b f hf,
|
||||
CTerm.substDimBool_of_absent i b fInv hfInv,
|
||||
CTerm.substDimBool_of_absent i b sec hsec,
|
||||
CTerm.substDimBool_of_absent i b ret hret,
|
||||
CTerm.substDimBool_of_absent i b coh hcoh,
|
||||
CType.substDim_absent_aux i b A hA]
|
||||
mutual
|
||||
private def CType.substDim_absent_aux (i : DimVar) (b : Bool) :
|
||||
(A : CType) → CType.dimAbsent i A = true → CType.substDim i b A = A
|
||||
| .univ, _ => rfl
|
||||
| .pi A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.pi (CType.substDim i b A) (CType.substDim i b B) = CType.pi A B
|
||||
congr 1
|
||||
· exact CType.substDim_absent_aux i b A h.1
|
||||
· exact CType.substDim_absent_aux i b B h.2
|
||||
| .path A a t, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.path (CType.substDim i b A)
|
||||
(CTerm.substDimBool i b a) (CTerm.substDimBool i b t) =
|
||||
CType.path A a t
|
||||
congr 1
|
||||
· exact CType.substDim_absent_aux i b A h.1.1
|
||||
· exact CTerm.substDimBool_of_absent i b a h.1.2
|
||||
· exact CTerm.substDimBool_of_absent i b t h.2
|
||||
| .sigma A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.sigma (CType.substDim i b A) (CType.substDim i b B) =
|
||||
CType.sigma A B
|
||||
congr 1
|
||||
· exact CType.substDim_absent_aux i b A h.1
|
||||
· exact CType.substDim_absent_aux i b B h.2
|
||||
| .glue φ T f fInv sec ret coh A, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.glue (φ.substDim i (if b then DimExpr.one else DimExpr.zero))
|
||||
(CType.substDim i b T)
|
||||
(CTerm.substDimBool i b f) (CTerm.substDimBool i b fInv)
|
||||
(CTerm.substDimBool i b sec) (CTerm.substDimBool i b ret)
|
||||
(CTerm.substDimBool i b coh)
|
||||
(CType.substDim i b A) =
|
||||
CType.glue φ T f fInv sec ret coh A
|
||||
obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h
|
||||
rw [FaceFormula.substDim_of_absent i _ φ hφ,
|
||||
CType.substDim_absent_aux i b T hT,
|
||||
CTerm.substDimBool_of_absent i b f hf,
|
||||
CTerm.substDimBool_of_absent i b fInv hfInv,
|
||||
CTerm.substDimBool_of_absent i b sec hsec,
|
||||
CTerm.substDimBool_of_absent i b ret hret,
|
||||
CTerm.substDimBool_of_absent i b coh hcoh,
|
||||
CType.substDim_absent_aux i b A hA]
|
||||
| .ind S params, h => by
|
||||
simp only [CType.dimAbsent] at h
|
||||
simp only [CType.substDim]
|
||||
rw [CType.substDim.params_of_absent i b params h]
|
||||
|
||||
/-- Helper: `CType.substDim.params i b` is identity on CType lists with
|
||||
`i` absent from every element. -/
|
||||
private def CType.substDim.params_of_absent (i : DimVar) (b : Bool) :
|
||||
(params : List CType) →
|
||||
CType.dimAbsent.params i params = true →
|
||||
CType.substDim.params i b params = params
|
||||
| [], _ => rfl
|
||||
| A :: rest, h => by
|
||||
simp only [CType.dimAbsent.params, Bool.and_eq_true] at h
|
||||
simp only [CType.substDim.params]
|
||||
rw [CType.substDim_absent_aux i b A h.1,
|
||||
CType.substDim.params_of_absent i b rest h.2]
|
||||
end
|
||||
|
||||
theorem CType.substDim_of_absent (i : DimVar) (b : Bool) (A : CType)
|
||||
(h : CType.dimAbsent i A = true) : CType.substDim i b A = A :=
|
||||
|
|
@ -280,47 +369,66 @@ theorem CType.substDim_of_absent (i : DimVar) (b : Bool) (A : CType)
|
|||
|
||||
-- ── CType.substDimExpr absent-subst (general DimExpr version) ─────────────────
|
||||
|
||||
private def CType.substDimExpr_absent_aux (i : DimVar) (r : DimExpr) :
|
||||
(A : CType) → CType.dimAbsent i A = true → CType.substDimExpr i r A = A
|
||||
| .univ, _ => rfl
|
||||
| .pi A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.pi (A.substDimExpr i r) (B.substDimExpr i r) = CType.pi A B
|
||||
congr 1
|
||||
· exact CType.substDimExpr_absent_aux i r A h.1
|
||||
· exact CType.substDimExpr_absent_aux i r B h.2
|
||||
| .path A a t, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r) =
|
||||
CType.path A a t
|
||||
congr 1
|
||||
· exact CType.substDimExpr_absent_aux i r A h.1.1
|
||||
· exact CTerm.substDim_of_absent i r a h.1.2
|
||||
· exact CTerm.substDim_of_absent i r t h.2
|
||||
| .sigma A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.sigma (A.substDimExpr i r) (B.substDimExpr i r) =
|
||||
CType.sigma A B
|
||||
congr 1
|
||||
· exact CType.substDimExpr_absent_aux i r A h.1
|
||||
· exact CType.substDimExpr_absent_aux i r B h.2
|
||||
| .glue φ T f fInv sec ret coh A, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.glue (φ.substDim i r)
|
||||
(T.substDimExpr i r)
|
||||
(f.substDim i r) (fInv.substDim i r)
|
||||
(sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
|
||||
(A.substDimExpr i r) =
|
||||
CType.glue φ T f fInv sec ret coh A
|
||||
obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h
|
||||
rw [FaceFormula.substDim_of_absent i r φ hφ,
|
||||
CType.substDimExpr_absent_aux i r T hT,
|
||||
CTerm.substDim_of_absent i r f hf,
|
||||
CTerm.substDim_of_absent i r fInv hfInv,
|
||||
CTerm.substDim_of_absent i r sec hsec,
|
||||
CTerm.substDim_of_absent i r ret hret,
|
||||
CTerm.substDim_of_absent i r coh hcoh,
|
||||
CType.substDimExpr_absent_aux i r A hA]
|
||||
mutual
|
||||
private def CType.substDimExpr_absent_aux (i : DimVar) (r : DimExpr) :
|
||||
(A : CType) → CType.dimAbsent i A = true → CType.substDimExpr i r A = A
|
||||
| .univ, _ => rfl
|
||||
| .pi A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.pi (A.substDimExpr i r) (B.substDimExpr i r) = CType.pi A B
|
||||
congr 1
|
||||
· exact CType.substDimExpr_absent_aux i r A h.1
|
||||
· exact CType.substDimExpr_absent_aux i r B h.2
|
||||
| .path A a t, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r) =
|
||||
CType.path A a t
|
||||
congr 1
|
||||
· exact CType.substDimExpr_absent_aux i r A h.1.1
|
||||
· exact CTerm.substDim_of_absent i r a h.1.2
|
||||
· exact CTerm.substDim_of_absent i r t h.2
|
||||
| .sigma A B, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.sigma (A.substDimExpr i r) (B.substDimExpr i r) =
|
||||
CType.sigma A B
|
||||
congr 1
|
||||
· exact CType.substDimExpr_absent_aux i r A h.1
|
||||
· exact CType.substDimExpr_absent_aux i r B h.2
|
||||
| .glue φ T f fInv sec ret coh A, h => by
|
||||
simp only [CType.dimAbsent, Bool.and_eq_true] at h
|
||||
show CType.glue (φ.substDim i r)
|
||||
(T.substDimExpr i r)
|
||||
(f.substDim i r) (fInv.substDim i r)
|
||||
(sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
|
||||
(A.substDimExpr i r) =
|
||||
CType.glue φ T f fInv sec ret coh A
|
||||
obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h
|
||||
rw [FaceFormula.substDim_of_absent i r φ hφ,
|
||||
CType.substDimExpr_absent_aux i r T hT,
|
||||
CTerm.substDim_of_absent i r f hf,
|
||||
CTerm.substDim_of_absent i r fInv hfInv,
|
||||
CTerm.substDim_of_absent i r sec hsec,
|
||||
CTerm.substDim_of_absent i r ret hret,
|
||||
CTerm.substDim_of_absent i r coh hcoh,
|
||||
CType.substDimExpr_absent_aux i r A hA]
|
||||
| .ind S params, h => by
|
||||
simp only [CType.dimAbsent] at h
|
||||
simp only [CType.substDimExpr]
|
||||
rw [CType.substDimExpr.params_of_absent i r params h]
|
||||
|
||||
/-- Helper: `CType.substDimExpr.params i r` is identity on CType lists
|
||||
with `i` absent from every element. -/
|
||||
private def CType.substDimExpr.params_of_absent (i : DimVar) (r : DimExpr) :
|
||||
(params : List CType) →
|
||||
CType.dimAbsent.params i params = true →
|
||||
CType.substDimExpr.params i r params = params
|
||||
| [], _ => rfl
|
||||
| A :: rest, h => by
|
||||
simp only [CType.dimAbsent.params, Bool.and_eq_true] at h
|
||||
simp only [CType.substDimExpr.params]
|
||||
rw [CType.substDimExpr_absent_aux i r A h.1,
|
||||
CType.substDimExpr.params_of_absent i r rest h.2]
|
||||
end
|
||||
|
||||
/-- Generalised: when `i` is absent from `A`, substituting `i` by any `DimExpr`
|
||||
leaves `A` unchanged. Equivalently: line reversal (via `i := inv i`) is
|
||||
|
|
@ -447,6 +555,17 @@ mutual
|
|||
| .snd t => by
|
||||
simp only [CTerm.substDim, CTerm.dimAbsent,
|
||||
CTerm.dimAbsent_after_substDim_aux i r hr t]
|
||||
| .dimExpr s => by
|
||||
simp only [CTerm.substDim, CTerm.dimAbsent,
|
||||
DimExpr.dimAbsent_after_subst i r hr s]
|
||||
| .ctor S c params args => by
|
||||
simp only [CTerm.substDim, CTerm.dimAbsent,
|
||||
CTerm.dimAbsent.list_after_substDim i r hr args]
|
||||
| .indElim S params motive branches target => by
|
||||
simp only [CTerm.substDim, CTerm.dimAbsent,
|
||||
CTerm.dimAbsent_after_substDim_aux i r hr motive,
|
||||
CTerm.dimAbsent.branches_after_substDim i r hr branches,
|
||||
CTerm.dimAbsent_after_substDim_aux i r hr target, Bool.and_self]
|
||||
|
||||
/-- Helper: `i` is absent from every clause in the result of substituting
|
||||
`i := r` in a clause list (provided `r` doesn't mention `i`). -/
|
||||
|
|
@ -462,6 +581,30 @@ mutual
|
|||
· exact FaceFormula.dimAbsent_after_substDim i r hr φ
|
||||
· exact CTerm.dimAbsent_after_substDim_aux i r hr u
|
||||
· exact CTerm.dimAbsent.clauses_after_substDim i r hr rest
|
||||
|
||||
/-- Helper: `i` is absent from every CTerm in the result of substituting
|
||||
`i := r` in a CTerm list. -/
|
||||
private def CTerm.dimAbsent.list_after_substDim
|
||||
(i : DimVar) (r : DimExpr) (hr : r.dimAbsent i = true) :
|
||||
(ts : List CTerm) →
|
||||
CTerm.dimAbsent.list i (CTerm.substDim.list i r ts) = true
|
||||
| [] => rfl
|
||||
| t :: rest => by
|
||||
simp only [CTerm.substDim.list, CTerm.dimAbsent.list,
|
||||
CTerm.dimAbsent_after_substDim_aux i r hr t,
|
||||
CTerm.dimAbsent.list_after_substDim i r hr rest, Bool.and_self]
|
||||
|
||||
/-- Helper: `i` is absent from every branch body in the result of
|
||||
substituting `i := r` in a branch list. -/
|
||||
private def CTerm.dimAbsent.branches_after_substDim
|
||||
(i : DimVar) (r : DimExpr) (hr : r.dimAbsent i = true) :
|
||||
(brs : List (String × CTerm)) →
|
||||
CTerm.dimAbsent.branches i (CTerm.substDim.branches i r brs) = true
|
||||
| [] => rfl
|
||||
| (n, b) :: rest => by
|
||||
simp only [CTerm.substDim.branches, CTerm.dimAbsent.branches,
|
||||
CTerm.dimAbsent_after_substDim_aux i r hr b,
|
||||
CTerm.dimAbsent.branches_after_substDim i r hr rest, Bool.and_self]
|
||||
end
|
||||
|
||||
theorem CTerm.dimAbsent_after_substDimBool (i : DimVar) (b : Bool) (t : CTerm) :
|
||||
|
|
@ -470,33 +613,48 @@ theorem CTerm.dimAbsent_after_substDimBool (i : DimVar) (b : Bool) (t : CTerm) :
|
|||
|
||||
-- Step 3: after CType.substDim i b, i is absent from the type.
|
||||
|
||||
private def CType.dimAbsent_after_substDim_aux (i : DimVar) (b : Bool) :
|
||||
(A : CType) → (A.substDim i b).dimAbsent i = true
|
||||
| .univ => rfl
|
||||
| .pi A B => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
CType.dimAbsent_after_substDim_aux i b A,
|
||||
CType.dimAbsent_after_substDim_aux i b B, Bool.and_self]
|
||||
| .path A a t => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
CType.dimAbsent_after_substDim_aux i b A,
|
||||
CTerm.dimAbsent_after_substDimBool i b a,
|
||||
CTerm.dimAbsent_after_substDimBool i b t, Bool.and_self]
|
||||
| .sigma A B => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
CType.dimAbsent_after_substDim_aux i b A,
|
||||
CType.dimAbsent_after_substDim_aux i b B, Bool.and_self]
|
||||
| .glue φ T f fInv sec ret coh A => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
FaceFormula.dimAbsent_after_substDim i _
|
||||
(DimExpr.dimAbsent_endpoint i b) φ,
|
||||
CType.dimAbsent_after_substDim_aux i b T,
|
||||
CTerm.dimAbsent_after_substDimBool i b f,
|
||||
CTerm.dimAbsent_after_substDimBool i b fInv,
|
||||
CTerm.dimAbsent_after_substDimBool i b sec,
|
||||
CTerm.dimAbsent_after_substDimBool i b ret,
|
||||
CTerm.dimAbsent_after_substDimBool i b coh,
|
||||
CType.dimAbsent_after_substDim_aux i b A, Bool.and_self]
|
||||
mutual
|
||||
private def CType.dimAbsent_after_substDim_aux (i : DimVar) (b : Bool) :
|
||||
(A : CType) → (A.substDim i b).dimAbsent i = true
|
||||
| .univ => rfl
|
||||
| .pi A B => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
CType.dimAbsent_after_substDim_aux i b A,
|
||||
CType.dimAbsent_after_substDim_aux i b B, Bool.and_self]
|
||||
| .path A a t => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
CType.dimAbsent_after_substDim_aux i b A,
|
||||
CTerm.dimAbsent_after_substDimBool i b a,
|
||||
CTerm.dimAbsent_after_substDimBool i b t, Bool.and_self]
|
||||
| .sigma A B => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
CType.dimAbsent_after_substDim_aux i b A,
|
||||
CType.dimAbsent_after_substDim_aux i b B, Bool.and_self]
|
||||
| .glue φ T f fInv sec ret coh A => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
FaceFormula.dimAbsent_after_substDim i _
|
||||
(DimExpr.dimAbsent_endpoint i b) φ,
|
||||
CType.dimAbsent_after_substDim_aux i b T,
|
||||
CTerm.dimAbsent_after_substDimBool i b f,
|
||||
CTerm.dimAbsent_after_substDimBool i b fInv,
|
||||
CTerm.dimAbsent_after_substDimBool i b sec,
|
||||
CTerm.dimAbsent_after_substDimBool i b ret,
|
||||
CTerm.dimAbsent_after_substDimBool i b coh,
|
||||
CType.dimAbsent_after_substDim_aux i b A, Bool.and_self]
|
||||
| .ind S params => by
|
||||
simp only [CType.substDim, CType.dimAbsent,
|
||||
CType.dimAbsent.params_after_substDim i b params]
|
||||
|
||||
/-- Helper: `i` absent from every CType in `substDim.params i b ps`. -/
|
||||
private def CType.dimAbsent.params_after_substDim (i : DimVar) (b : Bool) :
|
||||
(params : List CType) →
|
||||
CType.dimAbsent.params i (CType.substDim.params i b params) = true
|
||||
| [] => rfl
|
||||
| A :: rest => by
|
||||
simp only [CType.substDim.params, CType.dimAbsent.params,
|
||||
CType.dimAbsent_after_substDim_aux i b A,
|
||||
CType.dimAbsent.params_after_substDim i b rest, Bool.and_self]
|
||||
end
|
||||
|
||||
theorem CType.dimAbsent_after_substDim (i : DimVar) (b : Bool) (A : CType) :
|
||||
(A.substDim i b).dimAbsent i = true :=
|
||||
|
|
@ -632,6 +790,20 @@ mutual
|
|||
| .snd t => by
|
||||
simp only [CTerm.substDim]
|
||||
exact congrArg CTerm.snd (CTerm.substDim_comm_aux i j r s hij hrj hsi t)
|
||||
| .dimExpr e => by
|
||||
simp only [CTerm.substDim]
|
||||
exact congrArg CTerm.dimExpr
|
||||
(DimExpr.subst_comm i j r s hij hrj hsi e).symm
|
||||
| .ctor S c params args => by
|
||||
simp only [CTerm.substDim]
|
||||
exact congrArg (CTerm.ctor S c params)
|
||||
(CTerm.substDim.list_comm_aux i j r s hij hrj hsi args)
|
||||
| .indElim S params motive branches target => by
|
||||
simp only [CTerm.substDim]
|
||||
congr 1
|
||||
· exact CTerm.substDim_comm_aux i j r s hij hrj hsi motive
|
||||
· exact CTerm.substDim.branches_comm_aux i j r s hij hrj hsi branches
|
||||
· exact CTerm.substDim_comm_aux i j r s hij hrj hsi target
|
||||
|
||||
/-- Helper: `substDim.clauses` commutes on disjoint dim variables. -/
|
||||
private def CTerm.substDim.clauses_comm_aux
|
||||
|
|
@ -648,6 +820,34 @@ mutual
|
|||
(FaceFormula.substDim_comm i j r s hij hrj hsi φ)
|
||||
(CTerm.substDim_comm_aux i j r s hij hrj hsi u)
|
||||
· exact CTerm.substDim.clauses_comm_aux i j r s hij hrj hsi rest
|
||||
|
||||
/-- Helper: `substDim.list` commutes on disjoint dim variables. -/
|
||||
private def CTerm.substDim.list_comm_aux
|
||||
(i j : DimVar) (r s : DimExpr) (hij : i ≠ j)
|
||||
(hrj : r.dimAbsent j = true) (hsi : s.dimAbsent i = true) :
|
||||
(ts : List CTerm) →
|
||||
CTerm.substDim.list j s (CTerm.substDim.list i r ts) =
|
||||
CTerm.substDim.list i r (CTerm.substDim.list j s ts)
|
||||
| [] => rfl
|
||||
| t :: rest => by
|
||||
simp only [CTerm.substDim.list]
|
||||
congr 1
|
||||
· exact CTerm.substDim_comm_aux i j r s hij hrj hsi t
|
||||
· exact CTerm.substDim.list_comm_aux i j r s hij hrj hsi rest
|
||||
|
||||
/-- Helper: `substDim.branches` commutes on disjoint dim variables. -/
|
||||
private def CTerm.substDim.branches_comm_aux
|
||||
(i j : DimVar) (r s : DimExpr) (hij : i ≠ j)
|
||||
(hrj : r.dimAbsent j = true) (hsi : s.dimAbsent i = true) :
|
||||
(brs : List (String × CTerm)) →
|
||||
CTerm.substDim.branches j s (CTerm.substDim.branches i r brs) =
|
||||
CTerm.substDim.branches i r (CTerm.substDim.branches j s brs)
|
||||
| [] => rfl
|
||||
| (n, b) :: rest => by
|
||||
simp only [CTerm.substDim.branches]
|
||||
congr 1
|
||||
· exact Prod.ext rfl (CTerm.substDim_comm_aux i j r s hij hrj hsi b)
|
||||
· exact CTerm.substDim.branches_comm_aux i j r s hij hrj hsi rest
|
||||
end
|
||||
|
||||
theorem CTerm.substDimBool_comm
|
||||
|
|
@ -659,36 +859,55 @@ theorem CTerm.substDimBool_comm
|
|||
|
||||
-- CType commutativity
|
||||
|
||||
private def CType.substDim_comm_aux
|
||||
(i j : DimVar) (b c : Bool) (hij : i ≠ j) :
|
||||
(A : CType) →
|
||||
(A.substDim i b).substDim j c =
|
||||
(A.substDim j c).substDim i b
|
||||
| .univ => rfl
|
||||
| .pi A B => by
|
||||
simp only [CType.substDim]
|
||||
rw [CType.substDim_comm_aux i j b c hij A,
|
||||
CType.substDim_comm_aux i j b c hij B]
|
||||
| .path A a t => by
|
||||
simp only [CType.substDim]
|
||||
rw [CType.substDim_comm_aux i j b c hij A,
|
||||
CTerm.substDimBool_comm i j b c hij a,
|
||||
CTerm.substDimBool_comm i j b c hij t]
|
||||
| .sigma A B => by
|
||||
simp only [CType.substDim]
|
||||
rw [CType.substDim_comm_aux i j b c hij A,
|
||||
CType.substDim_comm_aux i j b c hij B]
|
||||
| .glue φ T f fInv sec ret coh A => by
|
||||
simp only [CType.substDim]
|
||||
rw [FaceFormula.substDim_comm i j _ _ hij
|
||||
(DimExpr.dimAbsent_endpoint j b) (DimExpr.dimAbsent_endpoint i c) φ,
|
||||
CType.substDim_comm_aux i j b c hij T,
|
||||
CTerm.substDimBool_comm i j b c hij f,
|
||||
CTerm.substDimBool_comm i j b c hij fInv,
|
||||
CTerm.substDimBool_comm i j b c hij sec,
|
||||
CTerm.substDimBool_comm i j b c hij ret,
|
||||
CTerm.substDimBool_comm i j b c hij coh,
|
||||
CType.substDim_comm_aux i j b c hij A]
|
||||
mutual
|
||||
private def CType.substDim_comm_aux
|
||||
(i j : DimVar) (b c : Bool) (hij : i ≠ j) :
|
||||
(A : CType) →
|
||||
(A.substDim i b).substDim j c =
|
||||
(A.substDim j c).substDim i b
|
||||
| .univ => rfl
|
||||
| .pi A B => by
|
||||
simp only [CType.substDim]
|
||||
rw [CType.substDim_comm_aux i j b c hij A,
|
||||
CType.substDim_comm_aux i j b c hij B]
|
||||
| .path A a t => by
|
||||
simp only [CType.substDim]
|
||||
rw [CType.substDim_comm_aux i j b c hij A,
|
||||
CTerm.substDimBool_comm i j b c hij a,
|
||||
CTerm.substDimBool_comm i j b c hij t]
|
||||
| .sigma A B => by
|
||||
simp only [CType.substDim]
|
||||
rw [CType.substDim_comm_aux i j b c hij A,
|
||||
CType.substDim_comm_aux i j b c hij B]
|
||||
| .glue φ T f fInv sec ret coh A => by
|
||||
simp only [CType.substDim]
|
||||
rw [FaceFormula.substDim_comm i j _ _ hij
|
||||
(DimExpr.dimAbsent_endpoint j b) (DimExpr.dimAbsent_endpoint i c) φ,
|
||||
CType.substDim_comm_aux i j b c hij T,
|
||||
CTerm.substDimBool_comm i j b c hij f,
|
||||
CTerm.substDimBool_comm i j b c hij fInv,
|
||||
CTerm.substDimBool_comm i j b c hij sec,
|
||||
CTerm.substDimBool_comm i j b c hij ret,
|
||||
CTerm.substDimBool_comm i j b c hij coh,
|
||||
CType.substDim_comm_aux i j b c hij A]
|
||||
| .ind S params => by
|
||||
simp only [CType.substDim]
|
||||
exact congrArg (CType.ind S)
|
||||
(CType.substDim.params_comm_aux i j b c hij params)
|
||||
|
||||
/-- Helper: `CType.substDim.params` commutes on disjoint dim variables. -/
|
||||
private def CType.substDim.params_comm_aux
|
||||
(i j : DimVar) (b c : Bool) (hij : i ≠ j) :
|
||||
(params : List CType) →
|
||||
CType.substDim.params j c (CType.substDim.params i b params) =
|
||||
CType.substDim.params i b (CType.substDim.params j c params)
|
||||
| [] => rfl
|
||||
| A :: rest => by
|
||||
simp only [CType.substDim.params]
|
||||
congr 1
|
||||
· exact CType.substDim_comm_aux i j b c hij A
|
||||
· exact CType.substDim.params_comm_aux i j b c hij rest
|
||||
end
|
||||
|
||||
theorem CType.substDim_comm
|
||||
(i j : DimVar) (b c : Bool) (hij : i ≠ j) (A : CType) :
|
||||
|
|
|
|||
|
|
@ -119,6 +119,38 @@ mutual
|
|||
| .pair a b => .vpair (eval env a) (eval env b)
|
||||
| .fst t => vFst (eval env t)
|
||||
| .snd t => vSnd (eval env t)
|
||||
-- REL1 inductive-type constructors.
|
||||
| .dimExpr r => .vdimExpr r
|
||||
| .ctor S c params args =>
|
||||
-- Produce a canonical constructor value with all args evaluated.
|
||||
-- (Boundary firing for path ctors lands in a follow-up — REL1
|
||||
-- design doc §4: when a `.dim`-typed arg evaluates to .zero/.one
|
||||
-- and matches a clause in `S.ctors[c].boundary`, we should fire
|
||||
-- that clause body instead. TODO REL1.1.)
|
||||
.vctor S c params (args.map (eval env))
|
||||
| .indElim S params motive branches target =>
|
||||
-- β-reduce on a canonical `vctor`; otherwise build a stuck
|
||||
-- `.nIndElim` that preserves env-evaluated motive and branches
|
||||
-- so it can unstick when target later resolves.
|
||||
match eval env target with
|
||||
| .vctor _ c _ argsV =>
|
||||
match List.lookup c branches with
|
||||
| some body =>
|
||||
-- Apply branch body to constructor's args via repeated
|
||||
-- `vApp` — the body is curried: λ a₁ … aₙ. result.
|
||||
-- Recursive-arg hypotheses (the IH passed alongside each
|
||||
-- `.self` arg in the design doc §5) are not yet wired
|
||||
-- here; an `indElim` of a non-recursive ctor is fully
|
||||
-- handled, but recursive ctors land their branch body
|
||||
-- with only the constructor args (no IH) — TODO REL1.1.
|
||||
argsV.foldl (fun f a => vApp f a) (eval env body)
|
||||
| none =>
|
||||
.vneu (.nvar s!"<indElim: no branch for {c}>")
|
||||
| .vneu n =>
|
||||
.vneu (.nIndElim S params (eval env motive)
|
||||
(branches.map (fun (nm, b) => (nm, eval env b))) n)
|
||||
| _ =>
|
||||
.vneu (.nvar "<indElim: target is not canonical>")
|
||||
|
||||
/-- First projection at the value level. β-reduces `vpair`; pushes a
|
||||
stuck neutral into `nfst`. Projecting any other value shape is a
|
||||
|
|
@ -176,6 +208,8 @@ mutual
|
|||
| .vTubeApp _ _, _ => .vneu (.nvar "<vApp: vTubeApp applied as function>")
|
||||
| .vPathTransp _ _ _ _ _ _ _, _ => .vneu (.nvar "<vApp: vPathTransp applied as function>")
|
||||
| .vpair _ _, _ => .vneu (.nvar "<vApp: vpair applied as function>")
|
||||
| .vctor _ _ _ _, _ => .vneu (.nvar "<vApp: vctor applied as function>")
|
||||
| .vdimExpr _, _ => .vneu (.nvar "<vApp: vdimExpr applied as function>")
|
||||
|
||||
/-- Apply a value to a dimension expression. β-reduces `vplam` closures
|
||||
by substituting the dim in the body and re-evaluating; pushes stuck
|
||||
|
|
@ -206,6 +240,8 @@ mutual
|
|||
| .vHCompFun _ _ _ _, _ => .vneu (.nvar "<vPApp: vHCompFun applied as path>")
|
||||
| .vCompFun _ _ _ _ _ _ _, _ => .vneu (.nvar "<vPApp: vCompFun applied as path>")
|
||||
| .vpair _ _, _ => .vneu (.nvar "<vPApp: vpair applied as path>")
|
||||
| .vctor _ _ _ _, _ => .vneu (.nvar "<vPApp: vctor applied as path>")
|
||||
| .vdimExpr _, _ => .vneu (.nvar "<vPApp: vdimExpr applied as path>")
|
||||
|
||||
/-- Homogeneous composition at the value level. The type `A` is
|
||||
*homogeneous* (doesn't vary along `i`); the tube and base are
|
||||
|
|
|
|||
|
|
@ -26,35 +26,41 @@ namespace CubicalTransportFFITest
|
|||
-- ── Summarisers ────────────────────────────────────────────────────────────
|
||||
|
||||
def cvalSummary : CVal → String
|
||||
| .vneu (.nvar s) => s!"vneu nvar {s}"
|
||||
| .vneu (.napp _ _) => "vneu napp"
|
||||
| .vneu (.npapp _ _) => "vneu npapp"
|
||||
| .vneu (.ntransp _ _ _ _) => "vneu ntransp"
|
||||
| .vneu (.nhcomp _ _ _ _) => "vneu nhcomp"
|
||||
| .vneu (.ncomp _ _ _ _ _) => "vneu ncomp"
|
||||
| .vneu (.ncompN _ _ _ _ _) => "vneu ncompN"
|
||||
| .vneu (.nglueIn _ _ _) => "vneu nglueIn"
|
||||
| .vneu (.nunglue _ _ _) => "vneu nunglue"
|
||||
| .vneu (.nfst _) => "vneu nfst"
|
||||
| .vneu (.nsnd _) => "vneu nsnd"
|
||||
| .vlam _ x _ => s!"vlam {x} ..."
|
||||
| .vplam _ i _ => s!"vplam {i.name} ..."
|
||||
| .vpair _ _ => "vpair ..."
|
||||
| .vTranspFun _ _ _ _ _ => "vTranspFun"
|
||||
| .vHCompFun _ _ _ _ => "vHCompFun"
|
||||
| .vCompFun _ _ _ _ _ _ _ => "vCompFun"
|
||||
| .vTubeApp _ _ => "vTubeApp"
|
||||
| .vPathTransp _ _ _ _ _ _ _ => "vPathTransp"
|
||||
| .vneu (.nvar s) => s!"vneu nvar {s}"
|
||||
| .vneu (.napp _ _) => "vneu napp"
|
||||
| .vneu (.npapp _ _) => "vneu npapp"
|
||||
| .vneu (.ntransp _ _ _ _) => "vneu ntransp"
|
||||
| .vneu (.nhcomp _ _ _ _) => "vneu nhcomp"
|
||||
| .vneu (.ncomp _ _ _ _ _) => "vneu ncomp"
|
||||
| .vneu (.ncompN _ _ _ _ _) => "vneu ncompN"
|
||||
| .vneu (.nglueIn _ _ _) => "vneu nglueIn"
|
||||
| .vneu (.nunglue _ _ _) => "vneu nunglue"
|
||||
| .vneu (.nfst _) => "vneu nfst"
|
||||
| .vneu (.nsnd _) => "vneu nsnd"
|
||||
| .vneu (.nIndElim _ _ _ _ _) => "vneu nIndElim"
|
||||
| .vlam _ x _ => s!"vlam {x} ..."
|
||||
| .vplam _ i _ => s!"vplam {i.name} ..."
|
||||
| .vpair _ _ => "vpair ..."
|
||||
| .vTranspFun _ _ _ _ _ => "vTranspFun"
|
||||
| .vHCompFun _ _ _ _ => "vHCompFun"
|
||||
| .vCompFun _ _ _ _ _ _ _ => "vCompFun"
|
||||
| .vTubeApp _ _ => "vTubeApp"
|
||||
| .vPathTransp _ _ _ _ _ _ _ => "vPathTransp"
|
||||
| .vctor _ c _ _ => s!"vctor {c} ..."
|
||||
| .vdimExpr _ => "vdimExpr ..."
|
||||
|
||||
def ctermSummary : CTerm → String
|
||||
| .var x => s!"var {x}"
|
||||
| .lam x _ => s!"lam {x} ..."
|
||||
| .app _ _ => "app ..."
|
||||
| .plam i _ => s!"plam {i.name} ..."
|
||||
| .pair _ _ => "pair ..."
|
||||
| .fst _ => "fst ..."
|
||||
| .snd _ => "snd ..."
|
||||
| _ => "<other CTerm>"
|
||||
| .var x => s!"var {x}"
|
||||
| .lam x _ => s!"lam {x} ..."
|
||||
| .app _ _ => "app ..."
|
||||
| .plam i _ => s!"plam {i.name} ..."
|
||||
| .pair _ _ => "pair ..."
|
||||
| .fst _ => "fst ..."
|
||||
| .snd _ => "snd ..."
|
||||
| .dimExpr _ => "dimExpr ..."
|
||||
| .ctor _ c _ _ => s!"ctor {c} ..."
|
||||
| .indElim _ _ _ _ _ => "indElim ..."
|
||||
| _ => "<other CTerm>"
|
||||
|
||||
-- ── Individual test definitions ────────────────────────────────────────────
|
||||
-- Each returns (description, actual, expected) for runSmokeTests to print.
|
||||
|
|
|
|||
|
|
@ -138,6 +138,10 @@ mutual
|
|||
| _ =>
|
||||
.transp i (.path A a b) φ p
|
||||
| .vpair a b => .pair (readback a) (readback b)
|
||||
-- REL1 inductive-type values.
|
||||
| .vctor S c params args =>
|
||||
.ctor S c params (args.map readback)
|
||||
| .vdimExpr r => .dimExpr r
|
||||
|
||||
/-- Readback a `CNeu` into a `CTerm`. Straightforward structural
|
||||
recursion: each neutral constructor has a syntactic counterpart.
|
||||
|
|
@ -161,6 +165,11 @@ mutual
|
|||
| .nunglue φ f g => .unglue φ (readback f) (readback g)
|
||||
| .nfst n => .fst (readbackNeu n)
|
||||
| .nsnd n => .snd (readbackNeu n)
|
||||
-- REL1 inductive-eliminator stuck form.
|
||||
| .nIndElim S params motive branches target =>
|
||||
.indElim S params (readback motive)
|
||||
(branches.map (fun p => (p.1, readback p.2)))
|
||||
(readbackNeu target)
|
||||
end
|
||||
|
||||
-- ── Convenience wrapper ─────────────────────────────────────────────────────
|
||||
|
|
|
|||
|
|
@ -46,40 +46,64 @@ theorem CTerm.substDimBool_true (i : DimVar) (t : CTerm) :
|
|||
t.substDimBool i true = t.substDim i .one := rfl
|
||||
|
||||
-- ── CType.substDim ────────────────────────────────────────────────────────────
|
||||
-- Substitute dimension variable i with Bool endpoint b throughout a type.
|
||||
-- Path type endpoints are terms, so we delegate to CTerm.substDimBool.
|
||||
--
|
||||
-- `.ind S params` recurses pointwise through the parameter list via an
|
||||
-- explicit mutually-recursive helper (`CType.substDim.params`); this
|
||||
-- is the standard way to thread structural recursion through a
|
||||
-- `List CType` field of a CType constructor.
|
||||
|
||||
/-- Substitute dimension variable i with Bool endpoint b throughout a type.
|
||||
Path type endpoints are terms, so we delegate to CTerm.substDimBool. -/
|
||||
def CType.substDim (i : DimVar) (b : Bool) : CType → CType
|
||||
| .univ => .univ
|
||||
| .pi A B => .pi (A.substDim i b) (B.substDim i b)
|
||||
| .path A a t => .path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b)
|
||||
| .sigma A B => .sigma (A.substDim i b) (B.substDim i b)
|
||||
| .glue φ T f fInv sec ret coh A =>
|
||||
.glue (φ.substDim i (if b then .one else .zero))
|
||||
(T.substDim i b)
|
||||
(f.substDimBool i b) (fInv.substDimBool i b)
|
||||
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
||||
(A.substDim i b)
|
||||
mutual
|
||||
def CType.substDim (i : DimVar) (b : Bool) : CType → CType
|
||||
| .univ => .univ
|
||||
| .pi A B => .pi (A.substDim i b) (B.substDim i b)
|
||||
| .path A a t => .path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b)
|
||||
| .sigma A B => .sigma (A.substDim i b) (B.substDim i b)
|
||||
| .glue φ T f fInv sec ret coh A =>
|
||||
.glue (φ.substDim i (if b then .one else .zero))
|
||||
(T.substDim i b)
|
||||
(f.substDimBool i b) (fInv.substDimBool i b)
|
||||
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
||||
(A.substDim i b)
|
||||
-- REL1: schema-defined inductive. Recurse into params; the schema
|
||||
-- itself is static (its boundary CTerms are the schema's data, not
|
||||
-- caller-substituted dim-bound terms).
|
||||
| .ind S params => .ind S (CType.substDim.params i b params)
|
||||
|
||||
/-- Pointwise `substDim` through a list of CType parameters. -/
|
||||
def CType.substDim.params (i : DimVar) (b : Bool) : List CType → List CType
|
||||
| [] => []
|
||||
| A :: rest => A.substDim i b :: CType.substDim.params i b rest
|
||||
end
|
||||
|
||||
-- ── CType.substDimExpr ────────────────────────────────────────────────────────
|
||||
-- Substitute dimension variable `i` with an arbitrary `DimExpr r` throughout
|
||||
-- a type. Generalises `CType.substDim`, which fixes `r` to a Bool endpoint.
|
||||
--
|
||||
-- Used for *line reversal* in transport: the reversed line is
|
||||
-- `A[i := inv i]`, which cannot be expressed as a Bool-endpoint
|
||||
-- substitution because `inv i` is an open DimExpr.
|
||||
|
||||
/-- Substitute dimension variable `i` with an arbitrary `DimExpr r` throughout
|
||||
a type. Generalises `CType.substDim`, which fixes `r` to a Bool endpoint.
|
||||
mutual
|
||||
def CType.substDimExpr (i : DimVar) (r : DimExpr) : CType → CType
|
||||
| .univ => .univ
|
||||
| .pi A B => .pi (A.substDimExpr i r) (B.substDimExpr i r)
|
||||
| .path A a t => .path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r)
|
||||
| .sigma A B => .sigma (A.substDimExpr i r) (B.substDimExpr i r)
|
||||
| .glue φ T f fInv sec ret coh A =>
|
||||
.glue (φ.substDim i r)
|
||||
(T.substDimExpr i r)
|
||||
(f.substDim i r) (fInv.substDim i r)
|
||||
(sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
|
||||
(A.substDimExpr i r)
|
||||
| .ind S params => .ind S (CType.substDimExpr.params i r params)
|
||||
|
||||
Used for *line reversal* in transport: the reversed line is
|
||||
`A[i := inv i]`, which cannot be expressed as a Bool-endpoint
|
||||
substitution because `inv i` is an open DimExpr. -/
|
||||
def CType.substDimExpr (i : DimVar) (r : DimExpr) : CType → CType
|
||||
| .univ => .univ
|
||||
| .pi A B => .pi (A.substDimExpr i r) (B.substDimExpr i r)
|
||||
| .path A a t => .path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r)
|
||||
| .sigma A B => .sigma (A.substDimExpr i r) (B.substDimExpr i r)
|
||||
| .glue φ T f fInv sec ret coh A =>
|
||||
.glue (φ.substDim i r)
|
||||
(T.substDimExpr i r)
|
||||
(f.substDim i r) (fInv.substDim i r)
|
||||
(sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
|
||||
(A.substDimExpr i r)
|
||||
/-- Pointwise `substDimExpr` through a list of CType parameters. -/
|
||||
def CType.substDimExpr.params (i : DimVar) (r : DimExpr) : List CType → List CType
|
||||
| [] => []
|
||||
| A :: rest => A.substDimExpr i r :: CType.substDimExpr.params i r rest
|
||||
end
|
||||
|
||||
-- ── Reduction lemmas ──────────────────────────────────────────────────────────
|
||||
-- All proved by rfl: substDim is defined by pattern matching, so these
|
||||
|
|
@ -109,6 +133,9 @@ theorem substDim_glue (i : DimVar) (b : Bool) (φ : FaceFormula) (T : CType)
|
|||
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
||||
(A.substDim i b) := rfl
|
||||
|
||||
theorem substDim_ind (i : DimVar) (b : Bool) (S : CTypeSchema) (params : List CType) :
|
||||
(ind S params).substDim i b = .ind S (CType.substDim.params i b params) := rfl
|
||||
|
||||
-- ── substDimExpr reduction lemmas ─────────────────────────────────────────────
|
||||
|
||||
theorem substDimExpr_univ (i : DimVar) (r : DimExpr) :
|
||||
|
|
@ -135,49 +162,76 @@ theorem substDimExpr_glue (i : DimVar) (r : DimExpr) (φ : FaceFormula) (T : CTy
|
|||
(sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
|
||||
(A.substDimExpr i r) := rfl
|
||||
|
||||
/-- The Bool-endpoint `substDim` is exactly `substDimExpr` at the canonical
|
||||
endpoint `DimExpr`. Proof is by pattern-matching `def` (rather than the
|
||||
`induction` tactic) because `CType` is mutually inductive with `CTerm`.
|
||||
`CTerm.substDimBool` is defined as `CTerm.substDim` at the same DimExpr,
|
||||
so the path case closes by unfolding both. -/
|
||||
def substDim_eq_substDimExpr (i : DimVar) (b : Bool) :
|
||||
(A : CType) →
|
||||
A.substDim i b = A.substDimExpr i (if b then DimExpr.one else DimExpr.zero)
|
||||
| .univ => rfl
|
||||
| .pi A B => by
|
||||
show CType.pi (A.substDim i b) (B.substDim i b) =
|
||||
CType.pi (A.substDimExpr i _) (B.substDimExpr i _)
|
||||
rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
|
||||
| .path A a t => by
|
||||
show CType.path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b) =
|
||||
CType.path (A.substDimExpr i _) (a.substDim i _) (t.substDim i _)
|
||||
rw [substDim_eq_substDimExpr i b A,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim]
|
||||
| .sigma A B => by
|
||||
show CType.sigma (A.substDim i b) (B.substDim i b) =
|
||||
CType.sigma (A.substDimExpr i _) (B.substDimExpr i _)
|
||||
rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
|
||||
| .glue φ T f fInv sec ret coh A => by
|
||||
show CType.glue
|
||||
(φ.substDim i (if b then DimExpr.one else DimExpr.zero))
|
||||
(T.substDim i b)
|
||||
(f.substDimBool i b) (fInv.substDimBool i b)
|
||||
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
||||
(A.substDim i b)
|
||||
= CType.glue
|
||||
(φ.substDim i _)
|
||||
(T.substDimExpr i _)
|
||||
(f.substDim i _) (fInv.substDim i _)
|
||||
(sec.substDim i _) (ret.substDim i _) (coh.substDim i _)
|
||||
(A.substDimExpr i _)
|
||||
rw [substDim_eq_substDimExpr i b T,
|
||||
substDim_eq_substDimExpr i b A,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim]
|
||||
theorem substDimExpr_ind (i : DimVar) (r : DimExpr) (S : CTypeSchema) (params : List CType) :
|
||||
(ind S params).substDimExpr i r = .ind S (CType.substDimExpr.params i r params) := rfl
|
||||
|
||||
-- The Bool-endpoint `substDim` is exactly `substDimExpr` at the canonical
|
||||
-- endpoint `DimExpr`. Proof is by pattern-matching `def` (rather than the
|
||||
-- `induction` tactic) because `CType` is mutually inductive with `CTerm`.
|
||||
-- `CTerm.substDimBool` is defined as `CTerm.substDim` at the same DimExpr,
|
||||
-- so the path case closes by unfolding both.
|
||||
--
|
||||
-- `.ind` recurses into params via `substDim_eq_substDimExpr.params`,
|
||||
-- a structurally-recursive helper that establishes pointwise equality
|
||||
-- on the parameter list.
|
||||
|
||||
mutual
|
||||
def substDim_eq_substDimExpr (i : DimVar) (b : Bool) :
|
||||
(A : CType) →
|
||||
A.substDim i b = A.substDimExpr i (if b then DimExpr.one else DimExpr.zero)
|
||||
| .univ => rfl
|
||||
| .pi A B => by
|
||||
show CType.pi (A.substDim i b) (B.substDim i b) =
|
||||
CType.pi (A.substDimExpr i _) (B.substDimExpr i _)
|
||||
rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
|
||||
| .path A a t => by
|
||||
show CType.path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b) =
|
||||
CType.path (A.substDimExpr i _) (a.substDim i _) (t.substDim i _)
|
||||
rw [substDim_eq_substDimExpr i b A,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim]
|
||||
| .sigma A B => by
|
||||
show CType.sigma (A.substDim i b) (B.substDim i b) =
|
||||
CType.sigma (A.substDimExpr i _) (B.substDimExpr i _)
|
||||
rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
|
||||
| .glue φ T f fInv sec ret coh A => by
|
||||
show CType.glue
|
||||
(φ.substDim i (if b then DimExpr.one else DimExpr.zero))
|
||||
(T.substDim i b)
|
||||
(f.substDimBool i b) (fInv.substDimBool i b)
|
||||
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
||||
(A.substDim i b)
|
||||
= CType.glue
|
||||
(φ.substDim i _)
|
||||
(T.substDimExpr i _)
|
||||
(f.substDim i _) (fInv.substDim i _)
|
||||
(sec.substDim i _) (ret.substDim i _) (coh.substDim i _)
|
||||
(A.substDimExpr i _)
|
||||
rw [substDim_eq_substDimExpr i b T,
|
||||
substDim_eq_substDimExpr i b A,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim,
|
||||
CTerm.substDimBool_eq_substDim]
|
||||
| .ind S params => by
|
||||
show CType.ind S (CType.substDim.params i b params)
|
||||
= CType.ind S (CType.substDimExpr.params i _ params)
|
||||
rw [substDim_eq_substDimExpr.params i b params]
|
||||
|
||||
/-- Helper: pointwise equality between `substDim.params` and
|
||||
`substDimExpr.params` at the canonical endpoint DimExpr. -/
|
||||
def substDim_eq_substDimExpr.params (i : DimVar) (b : Bool) :
|
||||
(params : List CType) →
|
||||
CType.substDim.params i b params =
|
||||
CType.substDimExpr.params i (if b then DimExpr.one else DimExpr.zero) params
|
||||
| [] => rfl
|
||||
| A :: rest => by
|
||||
show A.substDim i b :: CType.substDim.params i b rest
|
||||
= A.substDimExpr i _ :: CType.substDimExpr.params i _ rest
|
||||
rw [substDim_eq_substDimExpr i b A,
|
||||
substDim_eq_substDimExpr.params i b rest]
|
||||
end
|
||||
|
||||
-- ── Face connection ───────────────────────────────────────────────────────────
|
||||
-- These lemmas state the relationship between the Bool dimension environment
|
||||
|
|
|
|||
|
|
@ -51,7 +51,19 @@ mutual
|
|||
| glue (φ : FaceFormula) (T : CType)
|
||||
(f fInv sec ret coh : CTerm)
|
||||
(A : CType) : CType -- Glue [φ ↦ (T, e)] A
|
||||
deriving Repr
|
||||
/-- Schema-defined inductive type (REL1, INDUCTIVE_TYPES.md).
|
||||
|
||||
`ind S params` is an instance of the schema `S` at the given
|
||||
type parameters. `params.length = S.numParams` is a typing-side
|
||||
condition (not enforced syntactically — see `HasType.ind` in
|
||||
`Typing.lean`).
|
||||
|
||||
The schema `S` carries the constructor list (point + path
|
||||
ctors) and their boundary partial-element systems. Both plain
|
||||
inductives (`Nat`, `List A`, `Bool`) and HITs (`S¹`, `‖A‖₋₁`,
|
||||
suspensions, pushouts) are encoded uniformly via
|
||||
`CTypeSchema`. -/
|
||||
| ind (S : CTypeSchema) (params : List CType) : CType -- ind S params
|
||||
|
||||
/-- Terms in the cubical calculus. -/
|
||||
inductive CTerm where
|
||||
|
|
@ -94,9 +106,115 @@ mutual
|
|||
| fst (t : CTerm) : CTerm -- t.1
|
||||
/-- Σ elimination (second projection). -/
|
||||
| snd (t : CTerm) : CTerm -- t.2
|
||||
deriving Repr
|
||||
/-- A dimension expression lifted into the term language (REL1).
|
||||
|
||||
Used to fill `.dim`-typed argument positions of schema
|
||||
constructors (path ctors) and to hand a `DimExpr` to any
|
||||
future term-level operation that needs one. `DimExpr` is
|
||||
de Morgan algebra over `DimVar` and 0/1; lifting it lets path
|
||||
constructors take general dim arguments like `.meet i j`,
|
||||
`.inv r`, etc., not just bare `.var`-shaped dim names. -/
|
||||
| dimExpr (r : DimExpr) : CTerm -- ⟦ r ⟧
|
||||
/-- Schema constructor application (REL1, INDUCTIVE_TYPES.md §2.4).
|
||||
|
||||
`ctor S c params args` applies the constructor named `c` of
|
||||
schema `S` at parameters `params`, with `args.length =
|
||||
(S.ctors.find c).args.length`.
|
||||
|
||||
Args are positional and follow `CtorSpec.args` order. `.dim`-
|
||||
typed arg positions carry `CTerm.dimExpr r` (or any other
|
||||
CTerm that evaluates to a dim) — eval consults the
|
||||
constructor's boundary system on these to decide whether to
|
||||
produce the canonical `vctor` or fire a boundary clause. -/
|
||||
| ctor (S : CTypeSchema) (ctorName : String)
|
||||
(params : List CType) (args : List CTerm) : CTerm
|
||||
/-- Inductive eliminator (REL1, INDUCTIVE_TYPES.md §5).
|
||||
|
||||
`indElim S params motive branches target` eliminates a value
|
||||
of type `.ind S params`.
|
||||
|
||||
- `motive` is a CTerm of (function-CType) shape `.pi (.ind S
|
||||
params) .univ` — i.e. `λx : .ind S params. SomeType x`.
|
||||
- `branches` is one entry per ctor in *schema-declaration
|
||||
order*. Entry `(c, body)` says: when target reduces to the
|
||||
ctor `c`, evaluate `body` applied to the ctor's args plus
|
||||
(for each `.self` arg) the recursive elimination result.
|
||||
- `target : .ind S params` is the term being eliminated.
|
||||
|
||||
For path constructors, the branch must respect boundary
|
||||
coherence: at every face in the ctor's boundary system, the
|
||||
branch agrees with the corresponding eliminated body. This
|
||||
is a typing-level side condition (see `HasType.indElim`). -/
|
||||
| indElim (S : CTypeSchema) (params : List CType)
|
||||
(motive : CTerm)
|
||||
(branches : List (String × CTerm))
|
||||
(target : CTerm) : CTerm
|
||||
|
||||
/-- Argument shape for a schema constructor (REL1, §2.1).
|
||||
|
||||
Distinguishes ordinary CType-typed args (which may reference
|
||||
schema parameters via `.param`) from recursive `.self` args
|
||||
(the inductive being defined) and `.dim` args (used by path
|
||||
constructors). Boundary clauses inside `CtorSpec` reference
|
||||
args positionally; `.dim` args are addressed in face formulae
|
||||
via `DimVar.mk "$d_k"` where `k` is the dim-arg index counted
|
||||
among `.dim` arg positions only. -/
|
||||
inductive CTypeArg where
|
||||
/-- A non-recursive arg whose type is a closed CType. May
|
||||
reference schema parameters via embedded `.param i` inside `A`
|
||||
(parameter substitution happens at instantiation time). -/
|
||||
| type (A : CType) : CTypeArg
|
||||
/-- The `i`th schema parameter (zero-indexed against
|
||||
`CTypeSchema.numParams`). -/
|
||||
| param (i : Nat) : CTypeArg
|
||||
/-- Recursive reference to the inductive type being defined. -/
|
||||
| self : CTypeArg
|
||||
/-- A dimension binder, used by path constructors. -/
|
||||
| dim : CTypeArg
|
||||
|
||||
/-- Constructor specification (REL1, §2.2).
|
||||
|
||||
`name` is unique within the schema. `args` is the positional
|
||||
arg list. `boundary` is the partial-element system for path
|
||||
constructors (empty list ≡ point ctor). Each clause `(φ, body)`
|
||||
says: on the face `φ` of the dim args, the constructor reduces
|
||||
to `body`. Coherence obligations on the clauses are enforced
|
||||
at typing time (see `HasType.ctor` in `Typing.lean`).
|
||||
|
||||
Boundary clause bodies are CTerms in a scope where the ctor's
|
||||
args are bound positionally as `.var "$arg_k"`. Face formulae
|
||||
reference dim args as `DimVar.mk "$d_k"`. -/
|
||||
inductive CtorSpec where
|
||||
| mk (name : String) (args : List CTypeArg)
|
||||
(boundary : List (FaceFormula × CTerm)) : CtorSpec
|
||||
|
||||
/-- Schema for an inductive (or higher-inductive) type (REL1, §2.3).
|
||||
|
||||
`name` is the schema's symbolic name (used for diagnostics, not
|
||||
identity — schemas are compared structurally). `numParams` is
|
||||
the count of type parameters; `ctors` is the constructor list
|
||||
in declaration order. Equality is structural (no interning).
|
||||
|
||||
The schema mutually depends on `CType` (via `.type`-typed args
|
||||
and via `params : List CType` in `CType.ind`) and `CTerm` (via
|
||||
boundary clauses), so all five types live in this `mutual`
|
||||
block. -/
|
||||
inductive CTypeSchema where
|
||||
| mk (name : String) (numParams : Nat)
|
||||
(ctors : List CtorSpec) : CTypeSchema
|
||||
end
|
||||
|
||||
-- ── Repr derivations ─────────────────────────────────────────────────────────
|
||||
-- All five mutual inductives get `Repr` instances post-hoc (Lean's
|
||||
-- `deriving Repr` clause inside a mutual block of five doesn't always
|
||||
-- compose; explicit `deriving instance` is the robust form).
|
||||
|
||||
deriving instance Repr for CType
|
||||
deriving instance Repr for CTerm
|
||||
deriving instance Repr for CTypeArg
|
||||
deriving instance Repr for CtorSpec
|
||||
deriving instance Repr for CTypeSchema
|
||||
|
||||
-- ── Dimension substitution ────────────────────────────────────────────────────
|
||||
-- Substitute dimension variable i with DimExpr r throughout a term.
|
||||
--
|
||||
|
|
@ -138,6 +256,18 @@ mutual
|
|||
| .pair a b => .pair (a.substDim i r) (b.substDim i r)
|
||||
| .fst t => .fst (t.substDim i r)
|
||||
| .snd t => .snd (t.substDim i r)
|
||||
-- REL1 inductive-type constructors. Same CType-approximation as
|
||||
-- transp/comp/glue: schemas and `params : List CType` are *not*
|
||||
-- recursed into. The schemas are static and the params are
|
||||
-- supplied externally to any binder we'd be substituting into.
|
||||
| .dimExpr s => .dimExpr (DimExpr.subst i r s)
|
||||
| .ctor S c params args =>
|
||||
.ctor S c params (CTerm.substDim.list i r args)
|
||||
| .indElim S params motive branches target =>
|
||||
.indElim S params
|
||||
(motive.substDim i r)
|
||||
(CTerm.substDim.branches i r branches)
|
||||
(target.substDim i r)
|
||||
|
||||
/-- Helper: apply `CTerm.substDim i r` to each clause body (and
|
||||
`FaceFormula.substDim` to each face) in a system's clause list.
|
||||
|
|
@ -147,6 +277,21 @@ mutual
|
|||
| [] => []
|
||||
| (φ, u) :: rest =>
|
||||
(φ.substDim i r, u.substDim i r) :: CTerm.substDim.clauses i r rest
|
||||
|
||||
/-- Helper: apply `CTerm.substDim i r` to each element of a CTerm
|
||||
list (ctor argument lists). Mutually recursive for termination. -/
|
||||
def CTerm.substDim.list (i : DimVar) (r : DimExpr) :
|
||||
List CTerm → List CTerm
|
||||
| [] => []
|
||||
| t :: rest => t.substDim i r :: CTerm.substDim.list i r rest
|
||||
|
||||
/-- Helper: apply `CTerm.substDim i r` to the body of each branch in
|
||||
an `indElim`. Branch *names* are not affected; only bodies. -/
|
||||
def CTerm.substDim.branches (i : DimVar) (r : DimExpr) :
|
||||
List (String × CTerm) → List (String × CTerm)
|
||||
| [] => []
|
||||
| (n, b) :: rest =>
|
||||
(n, b.substDim i r) :: CTerm.substDim.branches i r rest
|
||||
end
|
||||
|
||||
-- ── One-step reduction ────────────────────────────────────────────────────────
|
||||
|
|
|
|||
|
|
@ -114,6 +114,26 @@ mutual
|
|||
`vpair` they reduce component-wise, on a `vneu` they produce a
|
||||
stuck `.nfst`/`.nsnd` neutral. -/
|
||||
| vpair : CVal → CVal → CVal
|
||||
/-- Schema constructor application — fully-evaluated, canonical
|
||||
constructor of an inductive (or higher-inductive) type (REL1).
|
||||
|
||||
`vctor S c params args` carries:
|
||||
- `S : CTypeSchema` — the schema this constructor belongs to.
|
||||
- `c : String` — the constructor's name.
|
||||
- `params : List CType` — the type parameters at which the
|
||||
inductive was instantiated.
|
||||
- `args : List CVal` — already-evaluated argument values.
|
||||
|
||||
For path constructors, when a `.dim`-typed arg lands on a face
|
||||
in the constructor's boundary system, eval fires the boundary
|
||||
clause and never produces a `vctor` — so a `vctor` represents
|
||||
a value that is *not* on a boundary face. -/
|
||||
| vctor : CTypeSchema → String → List CType → List CVal → CVal
|
||||
/-- Lifted dimension-expression value (REL1). Produced by
|
||||
`eval env (.dimExpr r)`; consumed by path-constructor face
|
||||
dispatch and by `vPApp` when its left operand is a `vplam`
|
||||
whose argument is a `.dimExpr`. -/
|
||||
| vdimExpr : DimExpr → CVal
|
||||
|
||||
/-- Neutral (stuck) terms. Each constructor corresponds to a
|
||||
λ-calculus or cubical elimination whose principal argument is itself
|
||||
|
|
@ -160,6 +180,13 @@ mutual
|
|||
| nfst : CNeu → CNeu
|
||||
/-- A stuck second projection. Produced by `vSnd` on a neutral. -/
|
||||
| nsnd : CNeu → CNeu
|
||||
/-- A stuck inductive eliminator (REL1). Produced by `eval`'s
|
||||
`.indElim` arm when the target evaluates to a neutral (or a
|
||||
non-`vctor` value). Preserves the schema, parameters, motive,
|
||||
evaluated branches, and the underlying neutral target so that
|
||||
later substitution / unstucking can fire the matching branch. -/
|
||||
| nIndElim : CTypeSchema → List CType → CVal →
|
||||
List (String × CVal) → CNeu → CNeu
|
||||
end
|
||||
|
||||
-- Inhabited instances — needed so `partial def` evaluators can be elaborated
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue