inductive ISAR.IotaTerm : Type

Barker's Iota dialect terms.

• iota : IotaTerm
• app : IotaTerm → IotaTerm → IotaTerm

@[implicit_reducible]

instance ISAR.instDecidableEqIotaTerm : DecidableEq IotaTerm

Equations

• ISAR.instDecidableEqIotaTerm = ISAR.instDecidableEqIotaTerm.decEq

def ISAR.instDecidableEqIotaTerm.decEq (x✝ x✝¹ : IotaTerm) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ISAR.instDecidableEqIotaTerm.decEq ISAR.IotaTerm.iota ISAR.IotaTerm.iota = isTrue ⋯
• ISAR.instDecidableEqIotaTerm.decEq ISAR.IotaTerm.iota (a.app a_1) = isFalse ⋯
• ISAR.instDecidableEqIotaTerm.decEq (a.app a_1) ISAR.IotaTerm.iota = isFalse ⋯

def ISAR.instReprIotaTerm.repr : IotaTerm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• ISAR.instReprIotaTerm.repr ISAR.IotaTerm.iota prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.IotaTerm.iota")).group prec✝

@[implicit_reducible]

instance ISAR.instReprIotaTerm : Repr IotaTerm

Equations

• ISAR.instReprIotaTerm = { reprPrec := ISAR.instReprIotaTerm.repr }

def ISAR.iota_sub_val : ITerm

The universal combinator ι = λx. x S K in the ISAR substrate.

Equations

• ISAR.iota_sub_val = ISAR.ITerm.sₛ · (ISAR.ITerm.sₛ · ISAR.ITerm.norm · (ISAR.ITerm.konst · ISAR.ITerm.sₛ)) · (ISAR.ITerm.konst · ISAR.ITerm.konst)

theorem ISAR.iota_sub_is_ISK : ISKTerm iota_sub_val

def ISAR.iota_sub : ISKSubtype

The universal iota combinator as an ISKSubtype.

Equations

• ISAR.iota_sub = ⟨ISAR.iota_sub_val, ISAR.iota_sub_is_ISK⟩

def ISAR.iota_encode : IotaTerm → ISKSubtype

Encode an IotaTerm into the ISAR substrate ISKSubtype.

Equations

• ISAR.iota_encode ISAR.IotaTerm.iota = ISAR.iota_sub
• ISAR.iota_encode (a.app a_1) = ISAR.app_raw (ISAR.iota_encode a) (ISAR.iota_encode a_1)

def ISAR.iota_decode_raw_val : ITerm → IotaTerm

Constructive decoder over the ITerm structure.

Equations

• ISAR.iota_decode_raw_val (ISAR.ITerm.sₛ · (ISAR.ITerm.sₛ · ISAR.ITerm.norm · (ISAR.ITerm.konst · ISAR.ITerm.sₛ)) · (ISAR.ITerm.konst · ISAR.ITerm.konst)) = ISAR.IotaTerm.iota
• ISAR.iota_decode_raw_val (f · x_1) = (ISAR.iota_decode_raw_val f).app (ISAR.iota_decode_raw_val x_1)
• ISAR.iota_decode_raw_val x✝ = ISAR.IotaTerm.iota

def ISAR.iota_decode_raw (t : ISKSubtype) : IotaTerm

Decode an ISKSubtype back to IotaTerm.

Equations

• ISAR.iota_decode_raw t = ISAR.iota_decode_raw_val ↑t

theorem ISAR.iota_decode_raw_val_app (t1 t2 : IotaTerm) : iota_decode_raw_val (↑(iota_encode t1) · ↑(iota_encode t2)) = (iota_decode_raw_val ↑(iota_encode t1)).app (iota_decode_raw_val ↑(iota_encode t2))

Lemma showing that iota_decode_raw_val distributes over encoded applications.

theorem ISAR.iota_decode_raw_iota_encode (t : IotaTerm) : iota_decode_raw (iota_encode t) = t

Proof that iota_decode_raw after iota_encode is the identity on IotaTerm.

def ISAR.iota_obs_eq (t1 t2 : IotaTerm) : Prop

Observational equivalence on iota terms via substrate OperEq of encodings. Unlike TRS, iota_encode ∘ iota_decode_raw is not id on all ISKSubtype (ι is a proper sublanguage), so a syntactic decode InvariantLayer → IotaTerm cannot be lifted without a false “NF stays in ι-image” claim.

Equations

• ISAR.iota_obs_eq t1 t2 = ISAR.OperEq (ISAR.iota_encode t1) (ISAR.iota_encode t2)

theorem ISAR.iota_obs_equiv : Equivalence iota_obs_eq

def ISAR.Iota_Dialect : Dialect

Iota_Dialect observations are substrate classes (not raw IotaTerm). This keeps the dialect axiom-free and computable: decoding is the identity on InvariantLayer, and preserves is definitional. Syntactic round-trip lives in iota_decode_raw_iota_encode.

Equations

• One or more equations did not get rendered due to their size.

def ISAR.iota_decode_term (t : ISKSubtype) : IotaTerm

Convenience: syntactic decode of a concrete substrate term (not a quotient section).

Equations

• ISAR.iota_decode_term t = ISAR.iota_decode_raw t

theorem ISAR.iota_decode_term_encode (x : IotaTerm) : iota_decode_term (iota_encode x) = x