Specifications #

inductive ConNF.SpecCondition [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) :

atom: [inst : ConNF.Params] → [inst_1 : ConNF.Level] → [inst_2 : ConNF.BasePositions] → [inst_3 : ConNF.FOAAssumptions] → {β : ConNF.Λ} → ConNF.ExtendedIndex ↑β → Set ConNF.κ → Set ConNF.κ → ConNF.SpecCondition β
flexible: [inst : ConNF.Params] → [inst_1 : ConNF.Level] → [inst_2 : ConNF.BasePositions] → [inst_3 : ConNF.FOAAssumptions] → {β : ConNF.Λ} → ConNF.ExtendedIndex ↑β → Set ConNF.κ → (ConNF.κ → Set ConNF.κ) → ConNF.SpecCondition β
inflexibleCoe: [inst : ConNF.Params] → [inst_1 : ConNF.Level] → [inst_2 : ConNF.BasePositions] → [inst_3 : ConNF.FOAAssumptions] → {β : ConNF.Λ} → (A : ConNF.ExtendedIndex ↑β) → (h : ConNF.InflexibleCoePath A) → ConNF.CodingFunction h.δ → (ConNF.κ → Set ConNF.κ) → ConNF.κ → (ConNF.κ → Set ConNF.κ) → ConNF.SpecCondition β
inflexibleBot: [inst : ConNF.Params] → [inst_1 : ConNF.Level] → [inst_2 : ConNF.BasePositions] → [inst_3 : ConNF.FOAAssumptions] → {β : ConNF.Λ} → (A : ConNF.ExtendedIndex ↑β) → ConNF.InflexibleBotPath A → Set ConNF.κ → (ConNF.κ → Set ConNF.κ) → ConNF.SpecCondition β

Instances For

theorem ConNF.SpecCondition.le_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} :

∀ (a a_1 : ConNF.SpecCondition β), a.LE a_1 ↔ (∃ (A : ConNF.ExtendedIndex ↑β) (s₁ : Set ConNF.κ) (s₂ : Set ConNF.κ) (t₁ : Set ConNF.κ) (t₂ : Set ConNF.κ), s₁ ⊆ s₂ ∧ t₁ ⊆ t₂ ∧ a = ConNF.SpecCondition.atom A s₁ t₁ ∧ a_1 = ConNF.SpecCondition.atom A s₂ t₂) ∨ (∃ (A : ConNF.ExtendedIndex ↑β) (s₁ : Set ConNF.κ) (s₂ : Set ConNF.κ) (t₁ : ConNF.κ → Set ConNF.κ) (t₂ : ConNF.κ → Set ConNF.κ), s₁ ⊆ s₂ ∧ t₁ ≤ t₂ ∧ a = ConNF.SpecCondition.flexible A s₁ t₁ ∧ a_1 = ConNF.SpecCondition.flexible A s₂ t₂) ∨ (∃ (A : ConNF.ExtendedIndex ↑β) (h : ConNF.InflexibleCoePath A) (χ : ConNF.CodingFunction h.δ) (t₁ : ConNF.κ → Set ConNF.κ) (t₂ : ConNF.κ → Set ConNF.κ) (m : ConNF.κ) (u₁ : ConNF.κ → Set ConNF.κ) (u₂ : ConNF.κ → Set ConNF.κ), t₁ ≤ t₂ ∧ u₁ ≤ u₂ ∧ a = ConNF.SpecCondition.inflexibleCoe A h χ t₁ m u₁ ∧ a_1 = ConNF.SpecCondition.inflexibleCoe A h χ t₂ m u₂) ∨ ∃ (A : ConNF.ExtendedIndex ↑β) (h : ConNF.InflexibleBotPath A) (s₁ : Set ConNF.κ) (s₂ : Set ConNF.κ) (t₁ : ConNF.κ → Set ConNF.κ) (t₂ : ConNF.κ → Set ConNF.κ), s₁ ⊆ s₂ ∧ t₁ ≤ t₂ ∧ a = ConNF.SpecCondition.inflexibleBot A h s₁ t₁ ∧ a_1 = ConNF.SpecCondition.inflexibleBot A h s₂ t₂

source

inductive ConNF.SpecCondition.LE [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} :

ConNF.SpecCondition β → ConNF.SpecCondition β → Prop

atom: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {s₁ s₂ t₁ t₂ : Set ConNF.κ}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → (ConNF.SpecCondition.atom A s₁ t₁).LE (ConNF.SpecCondition.atom A s₂ t₂)
flexible: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {s₁ s₂ : Set ConNF.κ} {t₁ t₂ : ConNF.κ → Set ConNF.κ}, s₁ ⊆ s₂ → t₁ ≤ t₂ → (ConNF.SpecCondition.flexible A s₁ t₁).LE (ConNF.SpecCondition.flexible A s₂ t₂)
inflexibleCoe: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {h : ConNF.InflexibleCoePath A} {χ : ConNF.CodingFunction h.δ} {t₁ t₂ : ConNF.κ → Set ConNF.κ} {m : ConNF.κ} {u₁ u₂ : ConNF.κ → Set ConNF.κ}, t₁ ≤ t₂ → u₁ ≤ u₂ → (ConNF.SpecCondition.inflexibleCoe A h χ t₁ m u₁).LE (ConNF.SpecCondition.inflexibleCoe A h χ t₂ m u₂)
inflexibleBot: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {h : ConNF.InflexibleBotPath A} {s₁ s₂ : Set ConNF.κ} {t₁ t₂ : ConNF.κ → Set ConNF.κ}, s₁ ⊆ s₂ → t₁ ≤ t₂ → (ConNF.SpecCondition.inflexibleBot A h s₁ t₁).LE (ConNF.SpecCondition.inflexibleBot A h s₂ t₂)

Instances For

source

instance ConNF.instLESpecCondition [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} :

LE (ConNF.SpecCondition β)

Equations

ConNF.instLESpecCondition = { le := ConNF.SpecCondition.LE }

source

instance ConNF.instPartialOrderSpecCondition [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} :

PartialOrder (ConNF.SpecCondition β)

Equations

ConNF.instPartialOrderSpecCondition = PartialOrder.mk ⋯

source

@[reducible, inline]

abbrev ConNF.Spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) :

Type u

Equations

ConNF.Spec β = ConNF.Enumeration (ConNF.SpecCondition β)

Instances For

source

theorem ConNF.Spec.before_comp_supports [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) (hS : S.Strong) {i : ConNF.κ} (hi : i < S.max) {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} (h : ConNF.InflexibleCoe A N.fst) (hSi : S.f i hi = { path := A, value := Sum.inr N }) :

MulAction.Supports (ConNF.Allowable ↑h.path.δ) (ConNF.Enumeration.carrier ((S.before i hi).comp (h.path.B.cons ⋯))) h.t

source

theorem ConNF.Spec.before_comp_supports' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) (hS : S.Strong) {i : ConNF.κ} (hi : i < S.max) {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} (h : ConNF.InflexibleCoe A N.fst) (hSi : S.f i hi = { path := A, value := Sum.inr N }) :

MulAction.Supports (ConNF.Allowable ↑h.path.δ) (ConNF.Enumeration.carrier ((S.before i hi).comp (h.path.B.cons ⋯))) h.t.set

source

structure ConNF.Spec.Specifies [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (σ : ConNF.Spec β) (S : ConNF.Support ↑β) (hS : S.Strong) :

Prop

A specification σ specifies an ordered support S if each support condition in S is described in a sensible way by σ.

max_eq_max : S.max = σ.max
atom_spec : ∀ (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom), S.f i hi = { path := A, value := Sum.inl a } → σ.f i ⋯ = ConNF.SpecCondition.atom A {j : ConNF.κ | ∃ (hj : j < S.max), S.f j hj = { path := A, value := Sum.inl a }} {j : ConNF.κ | ∃ (hj : j < S.max) (N : ConNF.NearLitter), S.f j hj = { path := A, value := Sum.inr N } ∧ a ∈ N}
flexible_spec : ∀ (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter), ConNF.Flexible A N.fst → S.f i hi = { path := A, value := Sum.inr N } → σ.f i ⋯ = ConNF.SpecCondition.flexible A {j : ConNF.κ | ∃ (hj : j < S.max) (N' : ConNF.NearLitter), S.f j hj = { path := A, value := Sum.inr N' } ∧ N'.fst = N.fst} fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < S.max) (hk : k < S.max) (a : ConNF.Atom) (N' : ConNF.NearLitter), N'.fst = N.fst ∧ a ∈ symmDiff ↑N ↑N' ∧ S.f j hj = { path := A, value := Sum.inr N' } ∧ S.f k hk = { path := A, value := Sum.inl a }}
inflexibleCoe_spec : ∀ (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleCoe A N.fst) (hSi : S.f i hi = { path := A, value := Sum.inr N }), σ.f i ⋯ = ConNF.SpecCondition.inflexibleCoe A h.path (ConNF.CodingFunction.code ((S.before i hi).comp (h.path.B.cons ⋯)) h.t.set ⋯) (fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < S.max) (hk : k < S.max) (a : ConNF.Atom) (N' : ConNF.NearLitter), N'.fst = N.fst ∧ a ∈ symmDiff ↑N ↑N' ∧ S.f j hj = { path := A, value := Sum.inr N' } ∧ S.f k hk = { path := A, value := Sum.inl a }}) h.t.support.max fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < h.t.support.max) (hk : k < S.max), { path := (h.path.B.cons ⋯).comp (h.t.support.f j hj).path, value := (h.t.support.f j hj).value } = S.f k hk}
inflexibleBot_spec : ∀ (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleBot A N.fst), S.f i hi = { path := A, value := Sum.inr N } → σ.f i ⋯ = ConNF.SpecCondition.inflexibleBot A h.path {j : ConNF.κ | ∃ (hj : j < S.max), S.f j hj = { path := h.path.B.cons ⋯, value := Sum.inl h.a }} fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < S.max) (hk : k < S.max) (a : ConNF.Atom) (N' : ConNF.NearLitter), N'.fst = N.fst ∧ a ∈ symmDiff ↑N ↑N' ∧ S.f j hj = { path := A, value := Sum.inr N' } ∧ S.f k hk = { path := A, value := Sum.inl a }}

Instances For

source

theorem ConNF.Spec.Specifies.max_eq_max [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (self : σ.Specifies S hS) :

S.max = σ.max

source

theorem ConNF.Spec.Specifies.atom_spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (self : σ.Specifies S hS) (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) :

S.f i hi = { path := A, value := Sum.inl a } → σ.f i ⋯ = ConNF.SpecCondition.atom A {j : ConNF.κ | ∃ (hj : j < S.max), S.f j hj = { path := A, value := Sum.inl a }} {j : ConNF.κ | ∃ (hj : j < S.max) (N : ConNF.NearLitter), S.f j hj = { path := A, value := Sum.inr N } ∧ a ∈ N}

source

theorem ConNF.Spec.Specifies.flexible_spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (self : σ.Specifies S hS) (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) :

ConNF.Flexible A N.fst → S.f i hi = { path := A, value := Sum.inr N } → σ.f i ⋯ = ConNF.SpecCondition.flexible A {j : ConNF.κ | ∃ (hj : j < S.max) (N' : ConNF.NearLitter), S.f j hj = { path := A, value := Sum.inr N' } ∧ N'.fst = N.fst} fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < S.max) (hk : k < S.max) (a : ConNF.Atom) (N' : ConNF.NearLitter), N'.fst = N.fst ∧ a ∈ symmDiff ↑N ↑N' ∧ S.f j hj = { path := A, value := Sum.inr N' } ∧ S.f k hk = { path := A, value := Sum.inl a }}

source

theorem ConNF.Spec.Specifies.inflexibleCoe_spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (self : σ.Specifies S hS) (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleCoe A N.fst) (hSi : S.f i hi = { path := A, value := Sum.inr N }) :

σ.f i ⋯ = ConNF.SpecCondition.inflexibleCoe A h.path (ConNF.CodingFunction.code ((S.before i hi).comp (h.path.B.cons ⋯)) h.t.set ⋯) (fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < S.max) (hk : k < S.max) (a : ConNF.Atom) (N' : ConNF.NearLitter), N'.fst = N.fst ∧ a ∈ symmDiff ↑N ↑N' ∧ S.f j hj = { path := A, value := Sum.inr N' } ∧ S.f k hk = { path := A, value := Sum.inl a }}) h.t.support.max fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < h.t.support.max) (hk : k < S.max), { path := (h.path.B.cons ⋯).comp (h.t.support.f j hj).path, value := (h.t.support.f j hj).value } = S.f k hk}

source

theorem ConNF.Spec.Specifies.inflexibleBot_spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (self : σ.Specifies S hS) (i : ConNF.κ) (hi : i < S.max) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (h : ConNF.InflexibleBot A N.fst) :

S.f i hi = { path := A, value := Sum.inr N } → σ.f i ⋯ = ConNF.SpecCondition.inflexibleBot A h.path {j : ConNF.κ | ∃ (hj : j < S.max), S.f j hj = { path := h.path.B.cons ⋯, value := Sum.inl h.a }} fun (j : ConNF.κ) => {k : ConNF.κ | ∃ (hj : j < S.max) (hk : k < S.max) (a : ConNF.Atom) (N' : ConNF.NearLitter), N'.fst = N.fst ∧ a ∈ symmDiff ↑N ↑N' ∧ S.f j hj = { path := A, value := Sum.inr N' } ∧ S.f k hk = { path := A, value := Sum.inl a }}

source

theorem ConNF.Spec.Specifies.of_eq_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (h : σ.Specifies S hS) {i : ConNF.κ} {hi : i < σ.max} {A : ConNF.ExtendedIndex ↑β} {s : Set ConNF.κ} {t : Set ConNF.κ} (hi' : σ.f i hi = ConNF.SpecCondition.atom A s t) :

∃ (a : ConNF.Atom), S.f i ⋯ = { path := A, value := Sum.inl a }

source

theorem ConNF.Spec.Specifies.of_eq_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (h : σ.Specifies S hS) {i : ConNF.κ} {hi : i < σ.max} {A : ConNF.ExtendedIndex ↑β} {s : Set ConNF.κ} {t : ConNF.κ → Set ConNF.κ} (hi' : σ.f i hi = ConNF.SpecCondition.flexible A s t) :

∃ (N : ConNF.NearLitter), ConNF.Flexible A N.fst ∧ S.f i ⋯ = { path := A, value := Sum.inr N }

source

theorem ConNF.Spec.Specifies.of_eq_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (h : σ.Specifies S hS) {i : ConNF.κ} {hi : i < σ.max} {A : ConNF.ExtendedIndex ↑β} {P : ConNF.InflexibleCoePath A} {χ : ConNF.CodingFunction P.δ} {s : ConNF.κ → Set ConNF.κ} {m : ConNF.κ} {u : ConNF.κ → Set ConNF.κ} (hi' : σ.f i hi = ConNF.SpecCondition.inflexibleCoe A P χ s m u) :

∃ (N : ConNF.NearLitter) (t : ConNF.Tangle ↑P.δ), N.fst = ConNF.fuzz ⋯ t ∧ S.f i ⋯ = { path := A, value := Sum.inr N }

source

theorem ConNF.Spec.Specifies.of_eq_inflexibleBot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {σ : ConNF.Spec β} {S : ConNF.Support ↑β} {hS : S.Strong} (h : σ.Specifies S hS) {i : ConNF.κ} {hi : i < σ.max} {A : ConNF.ExtendedIndex ↑β} {P : ConNF.InflexibleBotPath A} {s : Set ConNF.κ} {t : ConNF.κ → Set ConNF.κ} (hi' : σ.f i hi = ConNF.SpecCondition.inflexibleBot A P s t) :

∃ (N : ConNF.NearLitter) (a : ConNF.Tangle ⊥), N.fst = ConNF.fuzz ⋯ a ∧ S.f i ⋯ = { path := A, value := Sum.inr N }

Documentation

ConNF.Counting.Spec

Specifications #