The constrains relation

Addresses can be said to constrain each other in a number of ways. This is detailed below. The Constrains relation is well-founded.

Main declarations

• ConNF.Constrains: The constrains relation.
• ConNF.constrains_wf: The constrains relation is well-founded.
• ConNF.small_constrains: Only a small amount of things are constrained by a particular address.

theorem ConNF.constrains_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : ∀ (a a_1 : ConNF.Address ↑β), a ≺ a_1 ↔ (∃ (A : ConNF.ExtendedIndex ↑β) (a_2 : ConNF.Atom), a = { path := A, value := Sum.inr a_2.1.toNearLitter } ∧ a_1 = { path := A, value := Sum.inl a_2 }) ∨ (∃ (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter), ¬N.IsLitter ∧ a = { path := A, value := Sum.inr N.fst.toNearLitter } ∧ a_1 = { path := A, value := Sum.inr N }) ∨ (∃ (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter), ∃ a_2 ∈ symmDiff (ConNF.litterSet N.fst) ↑N, a = { path := A, value := Sum.inl a_2 } ∧ a_1 = { path := A, value := Sum.inr N }) ∨ (∃ (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (h : ConNF.InflexibleCoe A L), ∃ c ∈ h.t.support, a = { path := (h.path.B.cons ⋯).comp c.path, value := c.value } ∧ a_1 = { path := A, value := Sum.inr L.toNearLitter }) ∨ ∃ (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (h : ConNF.InflexibleBot A L), a = { path := h.path.B.cons ⋯, value := Sum.inl h.a } ∧ a_1 = { path := A, value := Sum.inr L.toNearLitter }

inductive ConNF.Constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : ConNF.Address ↑β → ConNF.Address ↑β → Prop

Addresses can be said to constrain each other in a number of ways.

1. (L, A) ≺ (a, A) when a ∈ L and L is a litter. We can say that an atom is constrained by the litter it belongs to.
2. (N°, A) ≺ (N, A) when N is a near-litter not equal to its corresponding litter N°.
3. (a, A) ≺ (N, A) for all a ∈ N ∆ N°.
4. (x, A ⬝ (γ ⟶ δ) ⬝ B) ≺ (f_{γ,δ}(t), A ⬝ (γ ⟶ ε) ⬝ (ε ⟶ ⊥)) for all paths A : β ⟶ γ and δ, ε < γ with δ ≠ ε, t a γ-tangle, where (x, B) lies in the δ-support in t.

This choice of relation makes some parts of the freedom of action theorem easier to prove.

• atom: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom), { path := A, value := Sum.inr a.1.toNearLitter } ≺ { path := A, value := Sum.inl a }
• nearLitter: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter), ¬N.IsLitter → { path := A, value := Sum.inr N.fst.toNearLitter } ≺ { path := A, value := Sum.inr N }
• symmDiff: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter), ∀ a ∈ symmDiff (ConNF.litterSet N.fst) ↑N, { path := A, value := Sum.inl a } ≺ { path := A, value := Sum.inr N }
• fuzz: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (h : ConNF.InflexibleCoe A L), ∀ c ∈ h.t.support, { path := (h.path.B.cons ⋯).comp c.path, value := c.value } ≺ { path := A, value := Sum.inr L.toNearLitter }
• fuzzBot: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (h : ConNF.InflexibleBot A L), { path := h.path.B.cons ⋯, value := Sum.inl h.a } ≺ { path := A, value := Sum.inr L.toNearLitter }

We declare new notation for the "constrains" relation on addresses.

def ConNF.«term_≺_» : Lean.TrailingParserDescr

Addresses can be said to constrain each other in a number of ways.

1. (L, A) ≺ (a, A) when a ∈ L and L is a litter. We can say that an atom is constrained by the litter it belongs to.
2. (N°, A) ≺ (N, A) when N is a near-litter not equal to its corresponding litter N°.
3. (a, A) ≺ (N, A) for all a ∈ N ∆ N°.
4. (x, A ⬝ (γ ⟶ δ) ⬝ B) ≺ (f_{γ,δ}(t), A ⬝ (γ ⟶ ε) ⬝ (ε ⟶ ⊥)) for all paths A : β ⟶ γ and δ, ε < γ with δ ≠ ε, t a γ-tangle, where (x, B) lies in the δ-support in t.

This choice of relation makes some parts of the freedom of action theorem easier to prove.

Equations

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

theorem ConNF.not_constrains_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (hL : ConNF.Flexible A L) : ¬c ≺ { path := A, value := Sum.inr L.toNearLitter }

def ConNF.Address.pos [ConNF.Params] [ConNF.BasePositions] {β : ConNF.Λ} (c : ConNF.Address ↑β) : ConNF.μ

Equations

• c.pos = Sum.elim (⇑ConNF.pos) (⇑ConNF.pos) c.value

@[simp]

theorem ConNF.Address.pos_atom [ConNF.Params] [ConNF.BasePositions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) : { path := A, value := Sum.inl a }.pos = ConNF.pos a

@[simp]

theorem ConNF.Address.pos_nearLitter [ConNF.Params] [ConNF.BasePositions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) : { path := A, value := Sum.inr N }.pos = ConNF.pos N

theorem ConNF.Constrains.hasPosition_lt [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (h : c ≺ d) : c.pos < d.pos

If c constrains d, then the position of c is less than the position of d.

theorem ConNF.constrains_subrelation [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) : Subrelation (fun (x x_1 : ConNF.Address ↑β) => x ≺ x_1) (InvImage (fun (x x_1 : ConNF.μ) => x < x_1) ConNF.Address.pos)

theorem ConNF.constrains_wf [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) : WellFounded fun (x x_1 : ConNF.Address ↑β) => x ≺ x_1

The ≺ relation is well-founded.

We establish some useful lemmas that show what addresses can possibly constrain what other addresses.

@[simp]

theorem ConNF.constrains_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} : c ≺ { path := A, value := Sum.inl a } ↔ c = { path := A, value := Sum.inr a.1.toNearLitter }

theorem ConNF.constrains_nearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} (hN : ¬N.IsLitter) : c ≺ { path := A, value := Sum.inr N } ↔ c = { path := A, value := Sum.inr N.fst.toNearLitter } ∨ ∃ a ∈ symmDiff (ConNF.litterSet N.fst) ↑N.snd, c = { path := A, value := Sum.inl a }

theorem ConNF.constrains_comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {c : ConNF.Address ↑γ} {d : ConNF.Address ↑γ} (h : c ≺ d) (B : Quiver.Path ↑β ↑γ) : { path := B.comp c.path, value := c.value } ≺ { path := B.comp d.path, value := d.value }

The constrains relation is stable under composition of paths. The converse is false.

We establish a strict partial order < on addresses given by the transitive closure of the constrains relation. This is well-founded.

instance ConNF.instPartialOrderAddressSomeΛ [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : PartialOrder (ConNF.Address ↑β)

Equations

• ConNF.instPartialOrderAddressSomeΛ = PartialOrder.mk ⋯

instance ConNF.instWellFoundedLTAddressSomeΛ [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : WellFoundedLT (ConNF.Address ↑β)

Equations

• ⋯ = ⋯

instance ConNF.instWellFoundedRelationAddressSomeΛ [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : WellFoundedRelation (ConNF.Address ↑β)

Equations

• ConNF.instWellFoundedRelationAddressSomeΛ = { rel := fun (x x_1 : ConNF.Address ↑β) => x < x_1, wf := ⋯ }

theorem ConNF.Address.le_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} : c ≤ d ↔ Relation.ReflTransGen (fun (x x_1 : ConNF.Address ↑β) => x ≺ x_1) c d

theorem ConNF.Address.lt_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} : c < d ↔ Relation.TransGen (fun (x x_1 : ConNF.Address ↑β) => x ≺ x_1) c d

theorem ConNF.not_transConstrains_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (hL : ConNF.Flexible A L) : ¬c < { path := A, value := Sum.inr L.toNearLitter }

theorem ConNF.InflexibleBot.constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleBot A L) : { path := h.path.B.cons ⋯, value := Sum.inl h.a } < { path := A, value := Sum.inr L.toNearLitter }

theorem ConNF.le_comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {c : ConNF.Address ↑γ} {d : ConNF.Address ↑γ} (h : c ≤ d) (B : Quiver.Path ↑β ↑γ) : { path := B.comp c.path, value := c.value } ≤ { path := B.comp d.path, value := d.value }

theorem ConNF.lt_comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {c : ConNF.Address ↑γ} {d : ConNF.Address ↑γ} (h : c < d) (B : Quiver.Path ↑β ↑γ) : { path := B.comp c.path, value := c.value } < { path := B.comp d.path, value := d.value }

theorem ConNF.le_nearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {N : ConNF.NearLitter} {B : ConNF.ExtendedIndex ↑β} {c : ConNF.Address ↑β} (h : { path := B, value := Sum.inr N } ≤ c) : { path := B, value := Sum.inr N.fst.toNearLitter } ≤ c

theorem ConNF.lt_nearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {N : ConNF.NearLitter} {B : ConNF.ExtendedIndex ↑β} {c : ConNF.Address ↑β} (h : c < { path := B, value := Sum.inr N.fst.toNearLitter }) : c < { path := B, value := Sum.inr N }

theorem ConNF.lt_nearLitter' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {N : ConNF.NearLitter} {B : ConNF.ExtendedIndex ↑β} {c : ConNF.Address ↑β} (h : { path := B, value := Sum.inr N } < c) : { path := B, value := Sum.inr N.fst.toNearLitter } < c

theorem ConNF.small_constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) : ConNF.Small {d : ConNF.Address ↑β | d ≺ c}

There is a small amount of addresses that constrain a given address.

def ConNF.reflTransClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : Set (ConNF.Address ↑β)) : Set (ConNF.Address ↑β)

The reflexive transitive closure of a set of addresses.

Equations

• ConNF.reflTransClosure S = {c : ConNF.Address ↑β | ∃ d ∈ S, c ≤ d}

def ConNF.transClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : Set (ConNF.Address ↑β)) : Set (ConNF.Address ↑β)

The transitive closure of a set of addresses.

Equations

• ConNF.transClosure S = {c : ConNF.Address ↑β | ∃ d ∈ S, c < d}

def ConNF.nthClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : Set (ConNF.Address ↑β)) : ℕ → Set (ConNF.Address ↑β)

Gadget that helps us prove that the reflTransClosure of a small set is small.

Equations

• ConNF.nthClosure S 0 = S
• ConNF.nthClosure S n.succ = {c : ConNF.Address ↑β | ∃ d ∈ ConNF.nthClosure S n, c ≺ d}

theorem ConNF.small_nthClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : Set (ConNF.Address ↑β)} {n : ℕ} (h : ConNF.Small S) : ConNF.Small (ConNF.nthClosure S n)

The nthClosure of a small set is small.

theorem ConNF.mem_nthClosure_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : Set (ConNF.Address ↑β)} {n : ℕ} {c : ConNF.Address ↑β} : c ∈ ConNF.nthClosure S n ↔ ∃ (l : List (ConNF.Address ↑β)), List.Chain (fun (x x_1 : ConNF.Address ↑β) => x ≺ x_1) c l ∧ l.length = n ∧ (c :: l).getLast ⋯ ∈ S

theorem ConNF.reflTransClosure_eq_iUnion_nthClosure [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : Set (ConNF.Address ↑β)} : ConNF.reflTransClosure S = ⋃ (n : ℕ), ConNF.nthClosure S n

The reflTransClosure of a set is the ℕ-indexed union of the nth closures.

theorem ConNF.reflTransClosure_small [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : Set (ConNF.Address ↑β)} (h : ConNF.Small S) : ConNF.Small (ConNF.reflTransClosure S)

The reflTransClosure of a small set is small.

theorem ConNF.transClosure_small [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {S : Set (ConNF.Address ↑β)} (h : ConNF.Small S) : ConNF.Small (ConNF.transClosure S)

The transClosure of a small set is small.