Coercion.applyComputable is the second of Core/TypedTLAPlus/Coercion.lean's two structural recursions over TypedTLAPlus.Coercion, discharging against ComputableTLAPlus.Expression instead of TypedTLAPlus.Expression. Needed because a receive's channel/reference coercion is stored unapplied and survives past Typed2Computable's type change: Guarded2Network is the first pass with a concrete ComputableTLAPlus.Expression (the built Head(inbox)/Tail(inbox) expression) to discharge it against, so it can't reuse Coercion.apply (fixed at TypedTLAPlus.Expr).

Mirrors Coercion.apply case-for-case, except choose's domain here is a required Expression α rather than Option (Expression α) — see Core/ComputableTLAPlus/Syntax.lean's module doc.

@[reducible, inline]

abbrev TypedTLAPlus.CExpr : Type

Checked TLA⁺ expressions at ComputableTLAPlus's output type — what Coercion.applyComputable transforms.

Equations

• TypedTLAPlus.CExpr = ComputableTLAPlus.Expression ComputableTLAPlus.Typ

@[irreducible]

def TypedTLAPlus.Coercion.applyComputable (c : Coercion) (e : CExpr) : CExpr

Applies a coercion to an already-built ComputableTLAPlus.Expression — see the module doc above for why this can't reuse Coercion.apply. Registers every synthesized node at the coerced expression's own span, for the reason spelled out on Coercion.apply.

Equations

• One or more equations did not get rendered due to their size.
• TypedTLAPlus.Coercion.id.applyComputable e = e
• (c₁.comp c₂).applyComputable e = c₂.applyComputable (c₁.applyComputable e)

Coercion.applyComputable and free variables

freeVars_applyComputable_subset — a coercion adds no free variable — lives here rather than next to the semantics: it needs Coercion.applyComputable's induction principle, generated only in this module. The small mem_freeVars_* unfoldings it uses are re-exported for the semantics to reuse.

TODO(locally-nameless): re-derive freeVars_applyComputable_subset against the de Bruijn applyComputable/liftBound; parked with the semantics port.

@[simp]

theorem ComputableTLAPlus.freeVars_var_free {n : String} {τ : Typ} : (Expression.var τ (TypedTLAPlus.Origin.free n)).freeVars = {n}

@[simp]

theorem ComputableTLAPlus.freeVars_var_bound {i : ℕ} {τ : Typ} : (Expression.var τ (TypedTLAPlus.Origin.bound i)).freeVars = ∅

@[simp]

theorem ComputableTLAPlus.freeVars_var_intrinsic {n : String} {τ : Typ} : (Expression.var τ (TypedTLAPlus.Origin.intrinsic n)).freeVars = ∅

@[simp]

theorem ComputableTLAPlus.freeVars_var_module {m n : String} {τ : Typ} : (Expression.var τ (TypedTLAPlus.Origin.module m n)).freeVars = ∅

@[simp]

theorem ComputableTLAPlus.freeVars_nat {s : String} : (Expression.nat s).freeVars = ∅

@[simp]

theorem ComputableTLAPlus.freeVars_str {s : String} : (Expression.str s).freeVars = ∅

theorem ComputableTLAPlus.mem_freeVars_fn {z y : String} {a co : Typ} {dom body : Expression Typ} : z ∈ (Expression.fn y a co dom body).freeVars ↔ z ∈ dom.freeVars ∨ z ∈ body.freeVars

theorem ComputableTLAPlus.mem_freeVars_map' {z y : String} {a co : Typ} {dom body : Expression Typ} : z ∈ (body.map' y a co dom).freeVars ↔ z ∈ dom.freeVars ∨ z ∈ body.freeVars

theorem ComputableTLAPlus.mem_freeVars_choose {z y : String} {a : Typ} {dom body : Expression Typ} : z ∈ (Expression.choose y a dom body).freeVars ↔ z ∈ dom.freeVars ∨ z ∈ body.freeVars

theorem ComputableTLAPlus.mem_freeVars_fnCall {z : String} {f e' : Expression Typ} {a : Typ} : z ∈ (f.fnCall a e').freeVars ↔ z ∈ f.freeVars ∨ z ∈ e'.freeVars

theorem ComputableTLAPlus.freeVars_fnCall_nat {e : Expression Typ} {τ : Typ} {s : String} : (e.fnCall τ (Expression.nat s)).freeVars = e.freeVars

A .fnCall at a .nat index reads only its head.

theorem ComputableTLAPlus.freeVars_recordAccess {e : Expression Typ} {n : String} : (e.recordAccess n).freeVars = e.freeVars

Field access reads only its subject.

theorem ComputableTLAPlus.freeVars_applyComputable_subset {z : String} {c : TypedTLAPlus.Coercion} {e : Expression Typ} (hz : z ∈ Expression.freeVars (c.applyComputable e)) : z ∈ e.freeVars

A coercion adds no free variable: every binder applyComputable introduces refers to itself by a .bound index, liftBound never touches a .free name, and every splice of e sits under an operator (Len/DOMAIN/.fnCall/.recordAccess) that carries e's free variables through unchanged. ExprSemantics.evalCoerce needs this to shrink a Coercion.FreshFor hypothesis onto a sub-expression (.comp, .function).

theorem ComputableTLAPlus.freeVars_applyComputable_subset' {c : TypedTLAPlus.Coercion} {e : Expression Typ} : Expression.freeVars (c.applyComputable e) ⊆ e.freeVars

The ⊆ reading of freeVars_applyComputable_subset.

Coercion.applyComputable and openVar

applyComputable commutes with an openVar traversal: every binder it introduces refers to itself by .bound, every splice of e under a binder carries a liftBound 1 that openVar at the raised depth cancels (Expression.openVar_liftBound_one_comm), and every other node passes the traversal through. ExprSemantics.evalCoerce's .set/.function cases need this: the built .fn/ .map' body opens with the binder's hint, and the opened term must read as applyComputable of the opened argument so the coercion recursion applies.

theorem ComputableTLAPlus.openVar_applyComputable_aux (c : TypedTLAPlus.Coercion) (x : String) (e : Expression Typ) (k : ℕ) : Expression.mapVars (Expression.openVarLam x) k (c.applyComputable e) = c.applyComputable (Expression.mapVars (Expression.openVarLam x) k e)

mapVars (openVarLam x) k pushes through applyComputable: the depth-generalised statement, proved by recursion on the coercion. openVar_applyComputable is the k = 0 reading.

theorem ComputableTLAPlus.openVar_applyComputable (c : TypedTLAPlus.Coercion) (x : String) (e : Expression Typ) : Expression.openVar x (c.applyComputable e) = c.applyComputable (Expression.openVar x e)

Applying a coercion and then opening the enclosing binder is opening it inside the argument first: openVar slides through applyComputable.

theorem ComputableTLAPlus.Expression.LC.applyComputable {c : TypedTLAPlus.Coercion} {e : Expression Typ} (he : e.LC) : LC (c.applyComputable e)

A coercion preserves local closedness. applyComputable introduces binders but every splice of e under one carries a liftBound 1, so opening the enclosing binder slides through (openVar_applyComputable) and lands on e, which a locally-closed e is fixed by — so the whole term is fixed by openVar, hence locally closed (Expression.LC.of_openVar_eq).