Strong.smul

Signed-off-by: zeramorphic <[email protected]>

ConNF/Counting/CodingFunction.lean

@@ -1,4 +1,4 @@
-import ConNF.FOA.Basic.Hypotheses
+import ConNF.Counting.StrongSupport
 
 /-!
 # Coding functions
@@ -161,6 +161,15 @@ theorem code_smul (S : Support β) (t : Tangle β) (ρ : Allowable β)
   rw [this]
   simp only [code_decode, Part.get_some, inv_smul_smul]
 
+def Strong (χ : CodingFunction β) : Prop :=
+  ∀ S ∈ χ.decode.Dom, S.Strong
+
+theorem strong_of_strong_mem (χ : CodingFunction β) (S : Support β)
+    (hS : S.Strong) (hSχ : S ∈ χ.decode.Dom) : χ.Strong := by
+  intro T hTχ
+  obtain ⟨ρ, rfl⟩ := (χ.dom_iff S T hSχ).mp hTχ
+  exact hS.smul ρ
+
 end CodingFunction
 
 end ConNF

ConNF/Counting/Spec.lean

@@ -16,153 +16,11 @@ namespace ConNF
 
 variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ}
 
-inductive SpecComponent (β : Λ) : Type u
-  | atom (A : ExtendedIndex β) (others : Set κ) (nearLitters : Set κ) :
-      SpecComponent β
-  | flexible (A : ExtendedIndex β) (others : Set κ) :
-      SpecComponent β
-  | inflexibleCoe (A : ExtendedIndex β) (h : InflexibleCoePath A)
-      (χ : CodingFunction h.δ) (r : κ → κ) :
-      SpecComponent β
-  | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (atoms : Set κ) :
-      SpecComponent β
-
-inductive Spec : Λ → Type u
-  | mk {β : Λ} (cond : Enumeration (SpecComponent β))
-      (lower : ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → Spec γ)
-      (r : ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → κ → κ) : Spec β
-
-def Spec.cond : Spec β → Enumeration (SpecComponent β)
-  | mk cond _ _ => cond
-
-def Spec.lower : Spec β → ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → Spec γ
-  | mk _ lower _ => lower
-
-def Spec.r : Spec β → ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → κ → κ
-  | mk _ _ r => r
-
-inductive SpecifiesC (σ : Spec β) (S : Support β)
-    (lS : ∀ {γ : Λ}, (hγ : (γ : TypeIndex) < β) → (A : Path (β : TypeIndex) γ) → Support γ) :
-    SpecComponent β → Address β → Prop
-  | atom (A : ExtendedIndex β) (a : Atom) :
-    SpecifiesC σ S lS
-      (SpecComponent.atom A
-        {i | ∃ hi : i < S.max, S.f i hi = ⟨A, inl a⟩}
-        {i | ∃ N : NearLitter, a ∈ N ∧ ∃ hi : i < S.max, S.f i hi = ⟨A, inr N⟩})
-      ⟨A, inl a⟩
+inductive SpecCondition (β : Λ)
+  | atom (A : ExtendedIndex β) (i : κ)
   | flexible (A : ExtendedIndex β)
-    (N : NearLitter) (h : Flexible A N.1) :
-    SpecifiesC σ S lS
-      (SpecComponent.flexible A
-        {i | ∃ hi : i < S.max, ∃ N', S.f i hi = ⟨A, inr N'⟩ ∧ N'.1 = N.1})
-      ⟨A, inr N⟩
-  | inflexibleCoe (A : ExtendedIndex β)
-    (N : NearLitter) (h : InflexibleCoe A N.1) (r : κ → κ)
-    (hr : ∀ i < h.t.support.max, r i < (lS (h.path.δ_lt_β) (h.path.B.cons h.path.hδ)).max)
-    (hS : ∀ (i : κ) (hit : i < h.t.support.max),
-      h.t.support.f i hit = (lS (h.path.δ_lt_β) (h.path.B.cons h.path.hδ)).f (r i) (hr i hit)) :
-    SpecifiesC σ S lS
-      (SpecComponent.inflexibleCoe A h.path
-        (CodingFunction.code h.t.support h.t (support_supports _)) r)
-      ⟨A, inr N⟩
-  | inflexibleBot (A : ExtendedIndex β)
-    (N : NearLitter) (h : InflexibleBot A N.1) :
-    SpecifiesC σ S lS
-      (SpecComponent.inflexibleBot A h.path
-        {i | ∃ hi : i < S.max, S.f i hi = ⟨h.path.B.cons (bot_lt_coe _), inl h.a⟩})
-      ⟨A, inr N⟩
-
-/-- TODO: We really should make this definition much earlier. -/
-def Address.comp {β γ : TypeIndex} (A : Quiver.Path β γ) (c : Address γ) : Address β :=
-  ⟨A.comp c.1, c.2⟩
-
-inductive Spec.Specifies : ∀ {β : Λ}, Spec β → Support β → Prop
-  | mk {β : Λ} (σ : Spec β) (S : Support β)
-    (max_eq_max : σ.cond.max = S.max)
-    (lS : ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → Support γ)
-    (hlS₁ : ∀ {γ : Λ} (hγ : (γ : TypeIndex) < β) (A : Path (β : TypeIndex) γ),
-      ∀ i < (lS hγ A).max, σ.r hγ A i < S.max)
-    (hlS₂ : ∀ {γ : Λ} (hγ : (γ : TypeIndex) < β) (A : Path (β : TypeIndex) γ)
-      (i : κ) (hi : i < (lS hγ A).max),
-      ((lS hγ A).f i hi).comp A = S.f (σ.r hγ A i) (hlS₁ hγ A i hi))
-    (hlS₃ : ∀ {γ : Λ} (hγ : (γ : TypeIndex) < β) (A : Path (β : TypeIndex) γ),
-      (σ.lower hγ A).Specifies (lS hγ A))
-    (cond : ∀ (i : κ) (hiσ : i < σ.cond.max) (hiS : i < S.max),
-      SpecifiesC σ S lS (σ.cond.f i hiσ) (S.f i hiS)) :
-    σ.Specifies S
-
-variable {σ : Spec β} {S : Support β}
-  {lS : ∀ {γ : Λ}, (hγ : (γ : TypeIndex) < β) → (A : Path (β : TypeIndex) γ) → Support γ}
-
-theorem specifiesC_atom_right_iff (σc : SpecComponent β) (A : ExtendedIndex β) (a : Atom) :
-    SpecifiesC σ S lS σc ⟨A, inl a⟩ ↔
-      σc = SpecComponent.atom A
-        {i | ∃ hi : i < S.max, S.f i hi = ⟨A, inl a⟩}
-        {i | ∃ N : NearLitter, a ∈ N ∧ ∃ hi : i < S.max, S.f i hi = ⟨A, inr N⟩} := by
-  constructor
-  · rintro ⟨⟩
-    rfl
-  · rintro rfl
-    exact SpecifiesC.atom A a
-
-theorem specifiesC_flexible_right_iff (σc : SpecComponent β)
-    (A : ExtendedIndex β) (N : NearLitter) (hN : Flexible A N.1) :
-    SpecifiesC σ S lS σc ⟨A, inr N⟩ ↔
-      σc = SpecComponent.flexible A
-        {i | ∃ hi : i < S.max, ∃ N', S.f i hi = ⟨A, inr N'⟩ ∧ N'.1 = N.1} := by
-  constructor
-  · intro h
-    cases h
-    case flexible => rfl
-    case inflexibleCoe r h hr hS =>
-      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at hN
-      exact hN.2.elim h
-    case inflexibleBot h =>
-      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at hN
-      exact hN.1.elim h
-  · rintro rfl
-    exact SpecifiesC.flexible A N hN
-
-theorem specifiesC_inflexibleCoe_right_iff (σc : SpecComponent β)
-    (A : ExtendedIndex β) (N : NearLitter) (hN : InflexibleCoe A N.1) :
-    SpecifiesC σ S lS σc ⟨A, inr N⟩ ↔
-      ∃ (r : κ → κ)
-      (hr : ∀ i < hN.t.support.max, r i < (lS (hN.path.δ_lt_β) (hN.path.B.cons hN.path.hδ)).max),
-      (∀ (i : κ) (hit : i < hN.t.support.max), hN.t.support.f i hit =
-        (lS (hN.path.δ_lt_β) (hN.path.B.cons hN.path.hδ)).f (r i) (hr i hit)) ∧
-      σc = SpecComponent.inflexibleCoe A hN.path
-        (CodingFunction.code hN.t.support hN.t (support_supports _)) r := by
-  constructor
-  · intro h
-    cases h
-    case flexible h' =>
-      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at h'
-      exact h'.2.elim hN
-    case inflexibleCoe r h hr hS =>
-      cases Subsingleton.elim hN h
-      exact ⟨r, hr, hS, rfl⟩
-    case inflexibleBot h =>
-      cases inflexibleBot_inflexibleCoe h hN
-  · rintro ⟨r, hr, hS, rfl⟩
-    exact SpecifiesC.inflexibleCoe A N hN r hr hS
-
-theorem specifiesC_inflexibleBot_right_iff (σc : SpecComponent β)
-    (A : ExtendedIndex β) (N : NearLitter) (hN : InflexibleBot A N.1) :
-    SpecifiesC σ S lS σc ⟨A, inr N⟩ ↔
-      σc = SpecComponent.inflexibleBot A hN.path
-        {i | ∃ hi : i < S.max, S.f i hi = ⟨hN.path.B.cons (bot_lt_coe _), inl hN.a⟩} := by
-  constructor
-  · intro h
-    cases h
-    case flexible h' =>
-      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at h'
-      exact h'.1.elim hN
-    case inflexibleCoe _ h _ _ =>
-      cases inflexibleBot_inflexibleCoe hN h
-    case inflexibleBot h =>
-      cases Subsingleton.elim hN h
-      rfl
-  · rintro ⟨r, hr, hS, rfl⟩
-    exact SpecifiesC.inflexibleBot A N hN
+  | inflexibleCoe (A : ExtendedIndex β) (h : InflexibleCoePath A)
+      (χ : CodingFunction h.δ) (hχ : χ.Strong)
+  | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (i : κ)
 
 end ConNF

ConNF/Counting/SpecSMul.lean

@@ -13,144 +13,4 @@ namespace ConNF
 variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [i : LeLevel β] {σ : Spec β} {S : Support β}
     {lS : ∀ {γ : Λ}, (hγ : (γ : TypeIndex) < β) → (A : Path (β : TypeIndex) γ) → Support γ}
 
-theorem specifiesCondition_atom_smul
-    {σc : SpecComponent β} {A : ExtendedIndex β} {a : Atom}
-    (h : SpecifiesC σ S lS σc ⟨A, inl a⟩) (ρ : Allowable β) :
-    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A)
-      σc ⟨A, inl (Allowable.toStructPerm ρ A • a)⟩ := by
-  rw [specifiesC_atom_right_iff] at h
-  rw [specifiesC_atom_right_iff, h, SpecComponent.atom.injEq]
-  simp only [Allowable.smul_support_f, Allowable.smul_support_max, true_and]
-  constructor
-  · ext i
-    constructor
-    · rintro ⟨hi₁, hi₂⟩
-      refine ⟨hi₁, ?_⟩
-      rw [hi₂]
-      rfl
-    · rintro ⟨hi₁, hi₂⟩
-      refine ⟨hi₁, ?_⟩
-      rw [smul_eq_iff_eq_inv_smul] at hi₂
-      rw [hi₂]
-      simp only [Allowable.smul_address, map_inv, Tree.inv_apply, smul_inl, inv_smul_smul]
-  · ext i
-    constructor
-    · rintro ⟨N, ha, hi₁, hi₂⟩
-      refine ⟨Allowable.toStructPerm ρ A • N, ?_, hi₁, ?_⟩
-      · rw [← SetLike.mem_coe, NearLitterPerm.smul_nearLitter_coe, smul_mem_smul_set_iff]
-        exact ha
-      · rw [hi₂]
-        rfl
-    · rintro ⟨N, ha, hi₁, hi₂⟩
-      refine ⟨(Allowable.toStructPerm ρ A)⁻¹ • N, ha, hi₁, ?_⟩
-      rw [smul_eq_iff_eq_inv_smul] at hi₂
-      rw [hi₂]
-      simp only [Allowable.smul_address, map_inv, Tree.inv_apply, smul_inr]
-
-theorem specifiesCondition_flexible_smul {S : Support β}
-    {σc : SpecComponent β} {A : ExtendedIndex β} {N : NearLitter} (hN : Flexible A N.1)
-    (h : SpecifiesC σ S lS σc ⟨A, inr N⟩) (ρ : Allowable β) :
-    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc
-      ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
-  rw [specifiesC_flexible_right_iff _ _ _ hN] at h
-  rw [specifiesC_flexible_right_iff _ _ _ (by exact hN.smul ρ), h]
-  refine congr_arg _ ?_
-  ext i
-  constructor
-  · rintro ⟨hi, N', hS, hN'⟩
-    refine ⟨hi, Allowable.toStructPerm ρ A • N', ?_, ?_⟩
-    · rw [Allowable.smul_support_f, hS]
-      rfl
-    · rw [NearLitterPerm.smul_nearLitter_fst, hN']
-      rfl
-  · rintro ⟨hi, N', hS, hN'⟩
-    refine ⟨hi, (Allowable.toStructPerm ρ A)⁻¹ • N', ?_, ?_⟩
-    · rw [Allowable.smul_support_f, smul_eq_iff_eq_inv_smul] at hS
-      rw [hS, Allowable.smul_address]
-      simp only [map_inv, Tree.inv_apply, smul_inr]
-    · rw [NearLitterPerm.smul_nearLitter_fst, hN',
-        NearLitterPerm.smul_nearLitter_fst, inv_smul_smul]
-
-theorem specifiesCondition_inflexibleCoe_smul {S : Support β}
-    {σc : SpecComponent β} {A : ExtendedIndex β} {N : NearLitter} (hN : InflexibleCoe A N.1)
-    (h : SpecifiesC σ S lS σc ⟨A, inr N⟩) (ρ : Allowable β) :
-    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc
-      ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
-  rw [specifiesC_inflexibleCoe_right_iff _ _ _ hN] at h
-  rw [specifiesC_inflexibleCoe_right_iff _ _ _ (by exact hN.smul ρ)]
-  obtain ⟨r, hr, hS, rfl⟩ := h
-  refine ⟨r, ?_, ?_, ?_⟩
-  · intro i hi
-    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t,
-      smul_support, Allowable.smul_support_max] at hi
-    exact hr i hi
-  · intro i hi
-    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t,
-      smul_support, Allowable.smul_support_max, Enumeration.smul_f] at hi ⊢
-    rw [← hS i hi]
-    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path,
-      Allowable.toStructPerm_smul, Allowable.toStructPerm_comp, Enumeration.smul_f]
-  · refine congr_arg₂ _ ?_ rfl
-    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t,
-      smul_support]
-    exact (CodingFunction.code_smul _ _ _ _ _).symm
-
-theorem specifiesCondition_inflexibleBot_smul {S : Support β}
-    {σc : SpecComponent β} {A : ExtendedIndex β} {N : NearLitter} (hN : InflexibleBot A N.1)
-    (h : SpecifiesC σ S lS σc ⟨A, inr N⟩) (ρ : Allowable β) :
-    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc
-      ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
-  rw [specifiesC_inflexibleBot_right_iff _ _ _ hN] at h
-  rw [specifiesC_inflexibleBot_right_iff _ _ _ (by exact hN.smul ρ),
-    h, SpecComponent.inflexibleBot.injEq]
-  refine ⟨rfl, HEq.rfl, ?_⟩
-  ext i
-  constructor
-  · rintro ⟨hi₁, hi₂⟩
-    refine ⟨hi₁, ?_⟩
-    rw [Allowable.smul_support_f, hi₂]
-    simp only [Allowable.smul_address, smul_inl, NearLitterPerm.smul_nearLitter_fst,
-      inflexibleBot_smul_path, inflexibleBot_smul_a, ofBot_smul, Allowable.toStructPerm_apply]
-  · rintro ⟨hi₁, hi₂⟩
-    refine ⟨hi₁, ?_⟩
-    rw [Allowable.smul_support_f, smul_eq_iff_eq_inv_smul] at hi₂
-    rw [hi₂]
-    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleBot_smul_path, inflexibleBot_smul_a,
-      ofBot_smul, Allowable.toStructPerm_apply, Allowable.smul_address, map_inv,
-      Tree.inv_apply, smul_inl, inv_smul_smul]
-
-theorem SpecifiesC.smul {σc : SpecComponent β} {c : Address β}
-    (h : SpecifiesC σ S lS σc c) (ρ : Allowable β) :
-    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc (ρ • c) := by
-  obtain ⟨B, a | N⟩ := c
-  · exact specifiesCondition_atom_smul h ρ
-  · obtain (h' | ⟨⟨h'⟩⟩ | ⟨⟨h'⟩⟩) := flexible_cases' B N.1
-    · exact specifiesCondition_flexible_smul h' h ρ
-    · exact specifiesCondition_inflexibleBot_smul h' h ρ
-    · exact specifiesCondition_inflexibleCoe_smul h' h ρ
-
-theorem Spec.Specifies.smul {σ : Spec β} {S : Support β} (h : σ.Specifies S) (ρ : Allowable β) :
-    σ.Specifies (ρ • S) := by
-  have : WellFoundedLT Λ := inferInstance
-  revert i σ S
-  have := this.induction
-    (C := fun β => ∀ (i : LeLevel ↑β) {σ : Spec β} {S : Support ↑β},
-      Specifies σ S → ∀ (ρ : Allowable ↑β), Specifies σ (ρ • S))
-  refine this β ?_
-  intro β ih i σ S h ρ
-  obtain ⟨_, _, max_eq_max, lS, hlS₁, hlS₂, hlS₃, cond⟩ := h
-  refine ⟨_, _, max_eq_max, fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A,
-      hlS₁, ?_, ?_, ?_⟩
-  · intro γ hγ A i hi
-    simp only [Enumeration.smul_f, Allowable.smul_support_f]
-    rw [← hlS₂ hγ A i hi]
-    rfl
-  · intro γ hγ A
-    have : LeLevel γ := ⟨hγ.le.trans i.elim⟩
-    have := ih γ (coe_lt_coe.mp hγ) _ (hlS₃ hγ A) (Allowable.comp A ρ)
-    rw [Allowable.toStructPerm_smul, Allowable.toStructPerm_comp] at this
-    exact this
-  · intro i hiσ hiS
-    exact (cond i hiσ hiS).smul ρ
-
 end ConNF