Presenting vocabularies as data

Ways of exhibiting a FirstOrder.Language.FinVocab, the finite presentation of a relational vocabulary that FirstOrder.Language.FinStruct encodes structures over.

A presentation is exactly a numbering of the symbols, i.e. an equivalence

Fin numSyms ≃ ((n : ℕ) × L.Relations n)

(FirstOrder.Language.FinVocab.symEquiv and FirstOrder.Language.FinVocab.ofEquivSigma are mutually inverse constructions), so a presentation can be built from any such numbering: from a duplicate-free list of all the symbols (FirstOrder.Language.FinVocab.ofList, the way every vocabulary of the catalog is presented), or by combining two presentations (FirstOrder.Language.FinVocab.sum).

The sum is what makes the whole development go through: the vocabularies of the second-order machinery are sums of an instance's vocabulary with a quantifier block's, and everything about them is encoded by the same means as an ordinary instance.

def FirstOrder.Language.FinVocab.symEquiv {L : Language} (V : L.FinVocab) : Fin V.numSyms ≃ (n : ℕ) × L.Relations n

A presentation is a numbering of the symbols.

Equations

• V.symEquiv = { toFun := V.symOf, invFun := fun (p : (n : ℕ) × L.Relations n) => V.index p.snd, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FirstOrder.Language.FinVocab.symEquiv_apply {L : Language} (V : L.FinVocab) (a✝ : Fin V.numSyms) : V.symEquiv a✝ = V.symOf a✝

@[simp]

theorem FirstOrder.Language.FinVocab.symEquiv_symm_apply {L : Language} (V : L.FinVocab) (p : (n : ℕ) × L.Relations n) : V.symEquiv.symm p = V.index p.snd

def FirstOrder.Language.FinVocab.ofEquivSigma {L : Language} (k : ℕ) (e : Fin k ≃ (n : ℕ) × L.Relations n) : L.FinVocab

A numbering of the symbols is a presentation, the converse of FirstOrder.Language.FinVocab.symEquiv.

Equations

• FirstOrder.Language.FinVocab.ofEquivSigma k e = { numSyms := k, symOf := ⇑e, index := fun {n : ℕ} (R : L.Relations n) => e.symm ⟨n, R⟩, symOf_index := ⋯, index_symOf := ⋯ }

@[simp]

theorem FirstOrder.Language.FinVocab.numSyms_ofEquivSigma {L : Language} (k : ℕ) (e : Fin k ≃ (n : ℕ) × L.Relations n) : (ofEquivSigma k e).numSyms = k

@[simp]

theorem FirstOrder.Language.FinVocab.symOf_ofEquivSigma {L : Language} (k : ℕ) (e : Fin k ≃ (n : ℕ) × L.Relations n) (i : Fin k) : (ofEquivSigma k e).symOf i = e i

def FirstOrder.Language.FinVocab.ofList {L : Language} [DecidableEq ((n : ℕ) × L.Relations n)] (l : List ((n : ℕ) × L.Relations n)) (nd : l.Nodup) (h : ∀ (p : (n : ℕ) × L.Relations n), p ∈ l) : L.FinVocab

A vocabulary presented by a list of all its symbols, without repetitions: the way the vocabularies of the catalog, which are finite enumerations, are presented.

Equations

• FirstOrder.Language.FinVocab.ofList l nd h = FirstOrder.Language.FinVocab.ofEquivSigma l.length (List.Nodup.getEquivOfForallMemList l nd h)

def FirstOrder.Language.FinVocab.sum {L L' : Language} (V : L.FinVocab) (W : L'.FinVocab) : (L.sum L').FinVocab

Presentations combine along Language.sum: a symbol of the sum vocabulary is a symbol of one side or of the other. This is what lets the vocabularies of the second-order machinery – an instance's vocabulary summed with a quantifier block's – be encoded like any other.

Equations

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

@[simp]

theorem FirstOrder.Language.FinVocab.numSyms_sum {L L' : Language} (V : L.FinVocab) (W : L'.FinVocab) : (V.sum W).numSyms = V.numSyms + W.numSyms

theorem FirstOrder.Language.FinVocab.index_sum_inl {L L' : Language} (V : L.FinVocab) (W : L'.FinVocab) {n : ℕ} (r : L.Relations n) : (V.sum W).index (Sum.inl r) = Fin.castAdd W.numSyms (V.index r)

The numbering of a sum vocabulary: the symbols of the left summand keep their numbers, those of the right summand are shifted past them. This is the only fact about FirstOrder.Language.FinVocab.sum anything downstream uses – it is what fixes the layout of the table of an encoded structure.

theorem FirstOrder.Language.FinVocab.index_sum_inr {L L' : Language} (V : L.FinVocab) (W : L'.FinVocab) {n : ℕ} (r : L'.Relations n) : (V.sum W).index (Sum.inr r) = Fin.natAdd V.numSyms (W.index r)

@[simp]

theorem FirstOrder.Language.FinVocab.val_index_sum_inl {L L' : Language} (V : L.FinVocab) (W : L'.FinVocab) {n : ℕ} (r : L.Relations n) : ↑((V.sum W).index (Sum.inl r)) = ↑(V.index r)

@[simp]

theorem FirstOrder.Language.FinVocab.val_index_sum_inr {L L' : Language} (V : L.FinVocab) (W : L'.FinVocab) {n : ℕ} (r : L'.Relations n) : ↑((V.sum W).index (Sum.inr r)) = V.numSyms + ↑(W.index r)