Codes of parameter values relative to a cut

The right side of an apply inside a recursive term cannot be decorrelated: the decorrelation would read the recursive relation twice. What replaces it is a table of the right side at every type of the parameter row, computed outside the recursion and joined to the recursive relation. The type of a parameter u is read relative to a finite set C of values, the cut: each component either is a value of C (or the null), or lies strictly between two consecutive non-null values of C – or below the least – and then only its rank among the components of u in the same gap is recorded. That is the component's code.

This file is the value-level part: the codes (Sym.Code), the code of a component (Sym.code), and the facts the symbolic evaluation rests on – two components have the same code exactly when they are equal (Sym.code_eq_code_iff), and the order of the codes, which reads the bound and the rank and never the value, is the order of the values wherever the concrete side is in the cut (Sym.Code.lt_iff).

def Sym.IsFresh {T : Type} [ValueType T] (C : Finset T) (a : T) : Prop

A fresh value: non-null and outside the cut.

Equations

• Sym.IsFresh C a = (a ∉ C ∧ ValueType.isNull a = false)

@[instance_reducible]

instance Sym.instDecidableIsFresh {T : Type} [ValueType T] (C : Finset T) (a : T) : Decidable (IsFresh C a)

Equations

• Sym.instDecidableIsFresh C a = id inferInstance

def Sym.below {T : Type} [ValueType T] (C : Finset T) (a : T) : Finset T

The non-null values of the cut strictly below a.

Equations

• Sym.below C a = {t ∈ C | ValueType.isNull t = false ∧ t < a}

def Sym.lo {T : Type} [ValueType T] (C : Finset T) (a : T) : WithBot T

The gap's lower bound: the greatest non-null value of the cut below a, ⊥ if there is none.

Equations

• Sym.lo C a = (Sym.below C a).max

def Sym.rank {T : Type} [ValueType T] (C : Finset T) {k : ℕ} (u : Fin k → T) (a : T) : ℕ

The rank of a among the components of u: how many distinct fresh components share its gap and are below it.

Equations

• Sym.rank C u a = {b ∈ Finset.image u Finset.univ | Sym.IsFresh C b ∧ Sym.lo C b = Sym.lo C a ∧ b < a}.card

Codes

inductive Sym.Code (T : Type) : Type

A code: a value standing for itself, or a gap of the cut (its lower bound, ⊥ below the least non-null value) with a rank in it.

• conc {T : Type} (a : T) : Code T
• fresh {T : Type} (l : WithBot T) (r : ℕ) : Code T

@[instance_reducible]

instance Sym.instDecidableEqCode {T✝ : Type} [DecidableEq T✝] : DecidableEq (Code T✝)

Equations

• Sym.instDecidableEqCode = Sym.instDecidableEqCode.decEq

def Sym.instDecidableEqCode.decEq {T✝ : Type} [DecidableEq T✝] (x✝ x✝¹ : Code T✝) : Decidable (x✝ = x✝¹)

Equations

• Sym.instDecidableEqCode.decEq (Sym.Code.conc a) (Sym.Code.conc b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Sym.instDecidableEqCode.decEq (Sym.Code.conc a) (Sym.Code.fresh l r) = isFalse ⋯
• Sym.instDecidableEqCode.decEq (Sym.Code.fresh l r) (Sym.Code.conc a) = isFalse ⋯
• Sym.instDecidableEqCode.decEq (Sym.Code.fresh a a_1) (Sym.Code.fresh b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Sym.code {T : Type} [ValueType T] (C : Finset T) {k : ℕ} (u : Fin k → T) (i : Fin k) : Code T

The code of a component of the parameter row.

Equations

• Sym.code C u i = if Sym.IsFresh C (u i) then Sym.Code.fresh (Sym.lo C (u i)) (Sym.rank C u (u i)) else Sym.Code.conc (u i)

theorem Sym.code_eq_code_iff {T : Type} [ValueType T] {C : Finset T} {k : ℕ} {u : Fin k → T} {i j : Fin k} : code C u i = code C u j ↔ u i = u j

Two components have the same code exactly when they are equal.

The order of codes

def Sym.Code.lt {T : Type} [ValueType T] : Code T → Code T → Prop

The order of codes: concrete values by their order; a concrete value below a gap when it is at most its bound; a gap below a concrete value when its bound is; two gaps by their bounds, then their ranks.

Equations

• (Sym.Code.conc a).lt (Sym.Code.conc b) = (a < b)
• (Sym.Code.conc a).lt (Sym.Code.fresh l r) = (↑a ≤ l)
• (Sym.Code.fresh l r).lt (Sym.Code.conc a) = (l < ↑a)
• (Sym.Code.fresh a a_1).lt (Sym.Code.fresh b b_1) = (a < b ∨ a = b ∧ a_1 < b_1)

def Sym.Valid {T : Type} [ValueType T] (C : Finset T) {k : ℕ} (u : Fin k → T) (x : Code T) : Prop

A code standing for a value of u, or for a value of the cut: what a cell holds wherever the symbolic evaluation is faithful. The null is set aside – a comparison with it is unknown, whatever the code.

Equations

• Sym.Valid C u x = ((∃ (i : Fin k), Sym.IsFresh C (u i) ∧ x = Sym.code C u i) ∨ ∃ a ∈ C, ValueType.isNull a = false ∧ x = Sym.Code.conc a)

noncomputable def Sym.dec {T : Type} [ValueType T] (C : Finset T) {k : ℕ} (u : Fin k → T) : Code T → T

The value a code stands for under the parameter row u: a fresh code reads the component it is the code of.

Equations

• Sym.dec C u (Sym.Code.conc a) = a
• Sym.dec C u (Sym.Code.fresh l r) = if h : ∃ (i : Fin k), Sym.IsFresh C (u i) ∧ Sym.lo C (u i) = l ∧ Sym.rank C u (u i) = r then u h.choose else 0

theorem Sym.Code.lt_iff {T : Type} [ValueType T] {C : Finset T} {k : ℕ} {u : Fin k → T} {x y : Code T} (hx : Valid C u x) (hy : Valid C u y) : x.lt y ↔ dec C u x < dec C u y

The order of valid codes is the order of the values they stand for.

Home · Documentation · Publications · Contributors · Source · Cite