Equivalence of codes

Several codes will be identified to make one TTT object. A TTT object has extensions for all type indices (except possibly ⊥), so our equivalence classes must too.

One way to do this is to make an equivalence class out of a code and its image under each cloudCode map. Thus we want to partition the big tree given by ↝₀ into trees of height 1 that each contains all descendents of its root (this is a slight lie for empty codes as the one equivalence class they form won't be a tree but rather a complete graph).

This is where code parity kicks in. We recursively pick out the small trees by noticing that codes whose preimages under cloud maps are all in a small tree already (in particular, those that have no preimage under an cloud map) must be the root of their own small tree, and that codes that are an image of some root of a small tree must belong to that same tree. This motivates the following definitions:

• A code is even if all its preimages under cloudCode maps are odd.
• A code is odd if one of its preimages under cloudCode maps are even.

If we replace "even" and "odd" by "winning" and "losing", we precisely get the rules for determining whether a game position is winning or losing.

Note that for nonempty codes there is at most one preimage under cloud maps.

Main declarations

• ConNF.IsEven, ConNF.IsOdd: Code parity.
• ConNF.Code.Equiv: Equivalence of codes.
• ConNF.exists_even_equiv: There is a unique even code in each equivalence class.

Parity of a code

Parity of codes. If we consider codes as states of a game and ↝₀ as the "leads to" relation, then even codes are precisely losing codes and odd codes are precisely winning codes. Parity of a nonempty code corresponds to the parity of its number of iterated preimages under cloudCode. The only even empty code is ⊥, all others are odd.

theorem ConNF.Code.isEven_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : ∀ (a : ConNF.Code), a.IsEven ↔ ∀ (d : ConNF.Code), d ↝₀ a → d.IsOdd

inductive ConNF.Code.IsEven [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : ConNF.Code → Prop

A code is even iff it only leads to odd codes.

• intro: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.TypedObjectsLt] [inst_5 : ConNF.PositionedTanglesLt] (c : ConNF.Code), (∀ (d : ConNF.Code), d ↝₀ c → d.IsOdd) → c.IsEven

theorem ConNF.Code.isOdd_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : ∀ (a : ConNF.Code), a.IsOdd ↔ ∃ (d : ConNF.Code), d ↝₀ a ∧ d.IsEven

inductive ConNF.Code.IsOdd [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : ConNF.Code → Prop

A code is odd iff it leads to some even code.

• intro: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.TypedObjectsLt] [inst_5 : ConNF.PositionedTanglesLt] (c d : ConNF.Code), d ↝₀ c → d.IsEven → c.IsOdd

theorem ConNF.Code.isEven_of_forall_not [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} (h : ∀ (d : ConNF.Code), ¬d ↝₀ c) : c.IsEven

@[simp]

theorem ConNF.Code.isEven_of_eq_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] (c : ConNF.Code) (hc : c.β = ⊥) : c.IsEven

@[simp]

theorem ConNF.Code.isEven_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] (s : Set ConNF.Atom) : (ConNF.Code.mk ⊥ s).IsEven

theorem ConNF.Code.not_isOdd_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] (s : Set ConNF.Atom) : ¬(ConNF.Code.mk ⊥ s).IsOdd

@[simp]

theorem ConNF.Code.IsEmpty.isEven_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} (hc : c.IsEmpty) : c.IsEven ↔ c.β = ⊥

An empty code is even iff its extension is ⊥.

@[simp]

theorem ConNF.Code.IsEmpty.isOdd_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} (hc : c.IsEmpty) : c.IsOdd ↔ c.β ≠ ⊥

@[simp]

theorem ConNF.Code.isEven_empty_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.TypeIndex} [ConNF.LtLevel β] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : (ConNF.Code.mk β ∅).IsEven ↔ β = ⊥

@[simp]

theorem ConNF.Code.isOdd_empty_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.TypeIndex} [ConNF.LtLevel β] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : (ConNF.Code.mk β ∅).IsOdd ↔ β ≠ ⊥

@[simp]

theorem ConNF.Code.not_isOdd [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} : ¬c.IsOdd ↔ c.IsEven

A code is not odd iff it is even.

@[simp]

theorem ConNF.Code.not_isEven [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} : ¬c.IsEven ↔ c.IsOdd

A code is not even iff it is odd.

theorem ConNF.Code.IsEven.not_isOdd [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} : c.IsEven → ¬c.IsOdd

Alias of the reverse direction of ConNF.Code.not_isOdd.

---

A code is not odd iff it is even.

theorem ConNF.Code.IsOdd.not_isEven [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} : c.IsOdd → ¬c.IsEven

Alias of the reverse direction of ConNF.Code.not_isEven.

---

A code is not even iff it is odd.

theorem ConNF.Code.isEven_or_isOdd [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] (c : ConNF.Code) : c.IsEven ∨ c.IsOdd

Any code is even or odd.

theorem ConNF.CloudRel.isOdd [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {d : ConNF.Code} (hc : c.IsEven) (h : c ↝₀ d) : d.IsOdd

theorem ConNF.Code.IsEven.cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} (hc : c.IsEven) (hcγ : c.β ≠ ↑γ) : (ConNF.cloudCode γ c).IsOdd

theorem ConNF.Code.IsOdd.cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} (hc : c.IsOdd) (hc' : c.members.Nonempty) (hcγ : c.β ≠ ↑γ) : (ConNF.cloudCode γ c).IsEven

theorem ConNF.Code.IsEven.cloudCode_ne [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} (hc : c.IsEven) (hd : d.IsEven) (hcγ : c.β ≠ ↑γ) : ConNF.cloudCode γ c ≠ d

theorem ConNF.Code.cloudCode_ne_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {s : Set (ConNF.TSet ⊥)} : ConNF.cloudCode γ c ≠ ConNF.Code.mk ⊥ s

theorem ConNF.Code.cloudCode_ne_singleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.TypeIndex} [ConNF.LtLevel β] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {t : ConNF.TSet β} (hcβ : c.β ≠ β) : ConNF.cloudCode γ c ≠ ConNF.Code.mk β {t}

The cloud map cannot produce a singleton code.

@[simp]

theorem ConNF.Code.isEven_singleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.TypeIndex} [ConNF.LtLevel β] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] (t : ConNF.TSet β) : (ConNF.Code.mk β {t}).IsEven

Singleton codes are even.

Equivalence of codes

theorem ConNF.Code.equiv_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : ∀ (a a_1 : ConNF.Code), a ≡ a_1 ↔ a_1 = a ∨ (a_1.IsEven ∧ ∃ (β : ConNF.Λ) (inst : ConNF.LtLevel ↑β), a_1.β ≠ ↑β ∧ a = ConNF.cloudCode β a_1) ∨ (a.IsEven ∧ ∃ (β : ConNF.Λ) (inst : ConNF.LtLevel ↑β), a.β ≠ ↑β ∧ a_1 = ConNF.cloudCode β a) ∨ ∃ (c : ConNF.Code), c.IsEven ∧ ∃ (β : ConNF.Λ) (inst : ConNF.LtLevel ↑β), c.β ≠ ↑β ∧ ∃ (γ : ConNF.Λ) (inst_1 : ConNF.LtLevel ↑γ), c.β ≠ ↑γ ∧ a = ConNF.cloudCode β c ∧ a_1 = ConNF.cloudCode γ c

inductive ConNF.Code.Equiv [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : ConNF.Code → ConNF.Code → Prop

Codes are said to be equivalent if they belong to the same tree of height 1 with a single even root.

• refl: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.TypedObjectsLt] [inst_5 : ConNF.PositionedTanglesLt] (c : ConNF.Code), c ≡ c
• cloud_left: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.TypedObjectsLt] [inst_5 : ConNF.PositionedTanglesLt] (c : ConNF.Code), c.IsEven → ∀ (β : ConNF.Λ) [inst_6 : ConNF.LtLevel ↑β], c.β ≠ ↑β → ConNF.cloudCode β c ≡ c
• cloud_right: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.TypedObjectsLt] [inst_5 : ConNF.PositionedTanglesLt] (c : ConNF.Code), c.IsEven → ∀ (β : ConNF.Λ) [inst_6 : ConNF.LtLevel ↑β], c.β ≠ ↑β → c ≡ ConNF.cloudCode β c
• cloud_cloud: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.TypedObjectsLt] [inst_5 : ConNF.PositionedTanglesLt] (c : ConNF.Code), c.IsEven → ∀ (β : ConNF.Λ) [inst_6 : ConNF.LtLevel ↑β], c.β ≠ ↑β → ∀ (γ : ConNF.Λ) [inst_7 : ConNF.LtLevel ↑γ], c.β ≠ ↑γ → ConNF.cloudCode β c ≡ ConNF.cloudCode γ c

We declare new notation for code equivalence.

def ConNF.Code.«term_≡_» : Lean.TrailingParserDescr

Equations

• ConNF.Code.«term_≡_» = Lean.ParserDescr.trailingNode `ConNF.Code.term_≡_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 51))

theorem ConNF.Code.Equiv.rfl [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} : c ≡ c

theorem ConNF.Code.Equiv.of_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {d : ConNF.Code} : c = d → c ≡ d

theorem ConNF.Code.Equiv.symm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] : Symmetric fun (x x_1 : ConNF.Code) => x ≡ x_1

theorem ConNF.Code.Equiv.comm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {d : ConNF.Code} : c ≡ d ↔ d ≡ c

theorem ConNF.Code.Equiv.empty_empty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] (β : ConNF.TypeIndex) (γ : ConNF.TypeIndex) [ConNF.LtLevel β] [ConNF.LtLevel γ] : ConNF.Code.mk β ∅ ≡ ConNF.Code.mk γ ∅

All empty codes are equivalent.

theorem ConNF.Code.IsEmpty.equiv [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {d : ConNF.Code} (hc : c.IsEmpty) (hd : d.IsEmpty) : c ≡ d

theorem ConNF.Code.Equiv.trans [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} {e : ConNF.Code} : c ≡ d → d ≡ e → c ≡ e

Code equivalence is transitive.

theorem ConNF.Code.Equiv.equiv_equivalence [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] : Equivalence fun (x x_1 : ConNF.Code) => x ≡ x_1

Code equivalence is an equivalence relation.

theorem ConNF.Code.Equiv.nonempty_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {d : ConNF.Code} : c ≡ d → (c.members.Nonempty ↔ d.members.Nonempty)

If two codes are equal, they are either both empty or both nonempty.

theorem ConNF.Code.Equiv.ext [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {d : ConNF.Code} : c ≡ d → c.β = d.β → c = d

If two codes at the same level are equivalent, they are equal.

@[simp]

theorem ConNF.Code.Equiv.bot_left_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {s : Set (ConNF.TSet ⊥)} : ConNF.Code.mk ⊥ s ≡ c ↔ ConNF.Code.mk ⊥ s = c ∨ ∃ (β : ConNF.Λ) (x : ConNF.LtLevel ↑β), c = ConNF.Code.mk (↑β) (ConNF.cloud ⋯ s)

@[simp]

theorem ConNF.Code.Equiv.bot_right_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {s : Set (ConNF.TSet ⊥)} : c ≡ ConNF.Code.mk ⊥ s ↔ c = ConNF.Code.mk ⊥ s ∨ ∃ (β : ConNF.Λ) (x : ConNF.LtLevel ↑β), c = ConNF.Code.mk (↑β) (ConNF.cloud ⋯ s)

@[simp]

theorem ConNF.Code.Equiv.bot_bot_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {s : Set (ConNF.TSet ⊥)} {t : Set (ConNF.TSet ⊥)} : ConNF.Code.mk ⊥ s ≡ ConNF.Code.mk ⊥ t ↔ s = t

theorem ConNF.Code.IsEven.unique [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} : c.IsEven → d.IsEven → c ≡ d → c = d

theorem ConNF.Code.exists_even_equiv [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] (c : ConNF.Code) : ∃ (d : ConNF.Code), d ≡ c ∧ d.IsEven

There is a unique even code in each equivalence class.

theorem ConNF.Code.IsEven.exists_equiv_extension_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} (heven : c.IsEven) : ∃ (d : ConNF.Code), d ≡ c ∧ d.β = ↑γ

theorem ConNF.Code.exists_equiv_extension_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] (c : ConNF.Code) : ∃ (d : ConNF.Code), d ≡ c ∧ d.β = ↑γ

theorem ConNF.Code.Equiv.unique [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] {c : ConNF.Code} {d : ConNF.Code} : c ≡ d → c.β = d.β → c = d

theorem ConNF.Code.equiv_bot_subsingleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.TypedObjectsLt] [ConNF.PositionedTanglesLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} (d : ConNF.Code) (e : ConNF.Code) (hdc : d ≡ c) (hec : e ≡ c) (hd : d.β = ⊥) (he : e.β = ⊥) : d = e