Payloads by name, and the tape they present

DescriptiveComplexity.Draw.Table gives a state, a symbol and a transition each a payload Fin c → A, and DescriptiveComplexity.Draw.pad makes that payload the element's only spelling. Nothing so far says what the coordinates are, and a program that had to count them would be unreadable. This file names them:

the payload is a function of a finite slot type, and a slot that carries a bit holds one of the two designated elements.

DescriptiveComplexity.Draw.slotPl is the naming – a payload is f ∘ e.symm for the canonical enumeration e of the slots, so two payloads are equal exactly when the functions are – and DescriptiveComplexity.Draw.bitVal is the bit, read back by DescriptiveComplexity.Draw.bitVal_iff from the two designated elements being distinct. Between them, the distinctness obligations a transition table owes (DescriptiveComplexity.Draw.Table.Sep) become statements about named fields.

Which slots there are is not decided here. DescriptiveComplexity.Problems.Wide.DrawRules splits them into the control slots a state uses and the track slots a symbol uses, and builds the tape a register pass runs over on top of the two.

Bits

noncomputable def DescriptiveComplexity.Draw.bitVal {A : Type} (zero one : A) (P : Prop) : A

The element a bit is written as: the designated one when it is set, the designated zero when it is clear.

Equations

• DescriptiveComplexity.Draw.bitVal zero one P = if P then one else zero

@[simp]

theorem DescriptiveComplexity.Draw.bitVal_pos {A : Type} {zero one : A} {P : Prop} (hP : P) : bitVal zero one P = one

@[simp]

theorem DescriptiveComplexity.Draw.bitVal_neg {A : Type} {zero one : A} {P : Prop} (hP : ¬P) : bitVal zero one P = zero

theorem DescriptiveComplexity.Draw.bitVal_iff {A : Type} {zero one : A} {P : Prop} (hne : zero ≠ one) : bitVal zero one P = one ↔ P

A bit reads back, the two designated elements being distinct.

theorem DescriptiveComplexity.Draw.bitVal_congr {A : Type} {zero one : A} {P Q : Prop} (h : P ↔ Q) : bitVal zero one P = bitVal zero one Q

Bits that agree are the same element.

Payloads by name

noncomputable def DescriptiveComplexity.Draw.slotPl {A S : Type} [Fintype S] (f : S → A) : Fin (Fintype.card S) → A

A payload, named: the value of each slot, read through the canonical enumeration of the slot type. A program writes slotPl fun s => … and never mentions a coordinate number.

Equations

• DescriptiveComplexity.Draw.slotPl f i = f ((Fintype.equivFin S).symm i)

@[simp]

theorem DescriptiveComplexity.Draw.slotPl_apply {A S : Type} [Fintype S] (f : S → A) (s : S) : slotPl f ((Fintype.equivFin S) s) = f s

theorem DescriptiveComplexity.Draw.slotPl_injective {A S : Type} [Fintype S] : Function.Injective slotPl

A payload is determined by its slots, so a distinctness obligation about elements is one about the fields a program named.

theorem DescriptiveComplexity.Draw.slotPl_congr {A S : Type} [Fintype S] {f g : S → A} (h : ∀ (s : S), f s = g s) : slotPl f = slotPl g

Payloads agreeing slot by slot are equal.

noncomputable def DescriptiveComplexity.Draw.unslot {A S : Type} [Fintype S] (w : Fin (Fintype.card S) → A) : S → A

Reading a payload by name: the value a coordinate holds, addressed by its slot. This is what a rule's guard and its written symbol are written with – the rule's data arrives as a tuple and every field of it is unslot.

Equations

• DescriptiveComplexity.Draw.unslot w s = w ((Fintype.equivFin S) s)

@[simp]

theorem DescriptiveComplexity.Draw.unslot_slotPl {A S : Type} [Fintype S] (f : S → A) : unslot (slotPl f) = f

@[simp]

theorem DescriptiveComplexity.Draw.slotPl_unslot {A S : Type} [Fintype S] (w : Fin (Fintype.card S) → A) : slotPl (unslot w) = w