Strengthen supports

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

ConNF/Counting.lean

@@ -1,2 +1,3 @@
 import ConNF.Counting.CodingFunction
 import ConNF.Counting.Spec
+import ConNF.Counting.SpecSame

ConNF/Counting/CodingFunction.lean

@@ -115,7 +115,7 @@ noncomputable def code (S : Support β) (t : Tangle β)
     have := h₂.choose_spec.symm
     conv_rhs at this => rw [h₁.choose_spec]
     rw [← inv_smul_eq_iff, ← inv_smul_eq_iff, smul_smul, smul_smul] at this
-    exact Enumeration.smul_eq_of_smul_eq this hc
+    exact Allowable.smul_eq_of_smul_support_eq this hc
 
 @[simp]
 theorem code_decode (S : Support β) (t : Tangle β)
@@ -128,7 +128,7 @@ theorem code_decode (S : Support β) (t : Tangle β)
   · intros h' _
     refine h _ ?_
     intros c hc
-    exact Enumeration.smul_eq_of_smul_eq h'.choose_spec.symm hc
+    exact Allowable.smul_eq_of_smul_support_eq h'.choose_spec.symm hc
 
 @[simp]
 theorem mem_code_self {S : Support β} {t : Tangle β}

ConNF/Counting/Spec.lean

@@ -53,7 +53,7 @@ theorem SupportCondition.comp_smul_comp [LeLevel β] [LeLevel γ] (c : SupportCo
   · rw [comp_eq_of_not_exists h, comp_eq_of_not_exists (by exact h)]
 
 def Support.pathEnumeration (S : Support β) : Enumeration (ExtendedIndex β) :=
-  S.image SupportCondition.path
+  S.enum.image SupportCondition.path
 
 @[simp]
 theorem Support.pathEnumeration_f (S : Support β) (i : κ) (hi : i < S.pathEnumeration.max) :
@@ -84,7 +84,8 @@ theorem Support.compIndex_spec (E : Enumeration (ExtendedIndex β)) (h : canComp
   (Enumeration.chooseIndex_spec (p := (fun B => ∃ C, A.comp C = B)) h).choose_spec
 
 open scoped Classical in
-noncomputable def Support.comp (A : Quiver.Path β γ) (S : Support β) : Support γ :=
+noncomputable def Support.comp' (A : Quiver.Path β γ) (S : Support β) :
+    Enumeration (SupportCondition γ) :=
   if h : canComp A S.pathEnumeration then
     ⟨S.max, fun i hi => (S.f i hi).comp A
       ⟨compIndex_tail S.pathEnumeration h,
@@ -94,44 +95,65 @@ noncomputable def Support.comp (A : Quiver.Path β γ) (S : Support β) : Suppor
 
 variable {S : Support β}
 
-theorem Support.comp_eq_pos (h : canComp A S.pathEnumeration) :
-    S.comp A = ⟨S.max, fun i hi => (S.f i hi).comp A
+theorem Support.comp'_eq_pos (h : canComp A S.pathEnumeration) :
+    S.comp' A = ⟨S.max, fun i hi => (S.f i hi).comp A
       ⟨compIndex_tail S.pathEnumeration h,
         (S.f (compIndex S.pathEnumeration h) (compIndex_lt _ _)).value⟩⟩ :=
-  by rw [Support.comp, dif_pos h]
+  by rw [Support.comp', dif_pos h]
 
-theorem Support.comp_eq_neg (h : ¬canComp A S.pathEnumeration) :
-    S.comp A = ⟨0, fun _ hi => (κ_not_lt_zero _ hi).elim⟩ :=
-  by rw [Support.comp, dif_neg h]
+theorem Support.comp'_eq_neg (h : ¬canComp A S.pathEnumeration) :
+    S.comp' A = ⟨0, fun _ hi => (κ_not_lt_zero _ hi).elim⟩ :=
+  by rw [Support.comp', dif_neg h]
 
-theorem Allowable.comp_smul_support_comp {β γ : TypeIndex} [LeLevel β] [LeLevel γ]
+theorem Allowable.comp_smul_support_comp' {β γ : TypeIndex} [LeLevel β] [LeLevel γ]
     (S : Support β) (ρ : Allowable β) (A : Path β γ) :
-    Allowable.comp A ρ • S.comp A = (ρ • S).comp A := by
+    Allowable.comp A ρ • S.comp' A = (ρ • S).comp' A := by
   by_cases h : Support.canComp A S.pathEnumeration
-  · rw [Support.comp_eq_pos h, Support.comp_eq_pos]
+  · rw [Support.comp'_eq_pos h, Support.comp'_eq_pos]
     swap
     · exact h
     refine Enumeration.ext _ _ rfl (heq_of_eq ?_)
     ext i hi : 2
-    simp only [Enumeration.smul_f, SupportCondition.comp_smul_comp, Support.pathEnumeration_smul]
+    simp only [Enumeration.smul_f, SupportCondition.comp_smul_comp, smul_support_f,
+      Support.pathEnumeration_smul]
     refine congr_arg _ ?_
     rw [Allowable.smul_supportCondition, Allowable.smul_supportCondition,
       toStructPerm_comp, Tree.comp_apply, SupportCondition.mk.injEq,
       Support.compIndex_spec S.pathEnumeration h, Support.pathEnumeration_f]
     exact ⟨rfl, rfl⟩
   · push_neg at h
-    rw [Support.comp_eq_neg h, Support.comp_eq_neg (by rwa [Support.pathEnumeration_smul])]
+    rw [Support.comp'_eq_neg h, Support.comp'_eq_neg (by rwa [Support.pathEnumeration_smul])]
     refine Enumeration.ext _ _ rfl (heq_of_eq ?_)
     ext i hi : 2
     cases κ_not_lt_zero _ hi
 
+theorem Support.mem_of_mem_symmDiff_comp (A : Quiver.Path β γ) (S : Support β) (B : ExtendedIndex γ)
+    (N₁ N₂ : NearLitter) (a : Atom) :
+    N₁.1 = N₂.1 → a ∈ (N₁ : Set Atom) ∆ N₂ →
+    ⟨B, inr N₁⟩ ∈ S.comp' A → ⟨B, inr N₂⟩ ∈ S.comp' A → ⟨B, inl a⟩ ∈ S.comp' A := by
+  intro hN a hN₁ hN₂
+  by_cases h : Support.canComp A S.pathEnumeration
+  · rw [Support.comp'_eq_pos h] at hN₁ hN₂ ⊢
+    sorry
+  · rw [Support.comp'_eq_neg h] at hN₁ hN₂ ⊢
+    sorry
+
+noncomputable def Support.comp (A : Quiver.Path β γ) (S : Support β) : Support γ :=
+  ⟨S.comp' A, mem_of_mem_symmDiff_comp A S⟩
+
+theorem Allowable.comp_smul_support_comp {β γ : TypeIndex} [LeLevel β] [LeLevel γ]
+    (S : Support β) (ρ : Allowable β) (A : Path β γ) :
+    Allowable.comp A ρ • S.comp A = (ρ • S).comp A := by
+  ext : 1
+  simp only [Support.comp, Allowable.smul_mk_support, Allowable.comp_smul_support_comp']
+
 end comp
 
 variable {β : Λ}
 
 mutual
   inductive SpecCondition : Λ → Type u
-    | atom {β : Λ} (A : ExtendedIndex β) (others : Set κ) (nearLitters: Set κ) :
+    | atom {β : Λ} (A : ExtendedIndex β) (others : Set κ) (nearLitters : Set κ) :
         SpecCondition β
     | flexible {β : Λ} (A : ExtendedIndex β) :
         SpecCondition β
@@ -174,6 +196,8 @@ theorem ext {σ τ : Spec β} (h₁ : σ.max = τ.max)
 
 end Spec
 
+/-
+
 instance : WellFoundedRelation Λ where
   rel := (· < ·)
   wf := IsWellFounded.wf
@@ -355,4 +379,6 @@ theorem smul_spec {β : Λ} [LeLevel β] {S : Support β} {ρ : Allowable β} :
     (ρ • S).spec = S.spec :=
   Spec.ext rfl (fun _ _ _ => specFor_smul)
 
+-/
+
 end ConNF

ConNF/Counting/SpecSame.lean

@@ -0,0 +1,16 @@
+import ConNF.FOA
+import ConNF.Counting.Spec
+
+/-!
+# Supports with the same specification
+-/
+
+open Quiver Set Sum WithBot
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] (S T : Support β)
+
+end ConNF

ConNF/FOA/Basic/Constrains.lean

@@ -403,7 +403,7 @@ theorem small_constrains {β : Λ} (c : SupportCondition β) : Small {d | d ≺
         (B : Path (β : TypeIndex) γ) (t : Tangle δ),
         N = (fuzz hδε t).toNearLitter ∧ A = (B.cons hε).cons (bot_lt_coe _)
     · obtain ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, B, t, rfl, rfl⟩ := h
-      refine lt_of_le_of_lt ?_ (t.support).small
+      refine lt_of_le_of_lt ?_ t.support.small
       suffices
         #{a : SupportCondition β | ∃ c : (t.support : Set (SupportCondition δ)),
             a = ⟨(B.cons hδ).comp c.val.path, c.val.value⟩} ≤

ConNF/FOA/Basic/Hypotheses.lean

@@ -208,8 +208,8 @@ theorem Allowable.comp_bot {β : TypeIndex} [LeLevel β] (A : Quiver.Path β ⊥
 theorem smul_mem_support {β : Λ} [LtLevel β] {c : SupportCondition β} {t : Tangle β}
     (h : c ∈ t.support) (π : Allowable β) : π • c ∈ (π • t).support := by
   rw [smul_support]
-  simp only [Enumeration.mem_iff, Enumeration.smul_f, smul_left_cancel_iff,
-    Enumeration.smul_max] at h ⊢
+  simp only [Support.mem_iff, Allowable.smul_support_f, smul_left_cancel_iff,
+    Allowable.smul_support_max] at h ⊢
   exact h
 
 @[simp]

ConNF/FOA/Basic/Reduction.lean

@@ -186,6 +186,6 @@ theorem reduction_support_supports [TangleData β] (t : Tangle β) :
   intro ρ h
   refine support_supports t ρ ?_
   intros c hc'
-  exact reduction_supports (t.support) c hc' (Allowable.toStructPerm ρ) h
+  exact reduction_supports t.support c hc' (Allowable.toStructPerm ρ) h
 
 end ConNF

ConNF/FOA/Properties/ConstrainedAction.lean

@@ -325,7 +325,7 @@ theorem transGen_constrains_of_mem_support {A : ExtendedIndex β} {L : Litter}
     (hd₂ : ⟨(C.cons hε).cons (bot_lt_coe _),
       inr (fuzz hδε t).toNearLitter⟩ ≤ d)
     (hd : ⟨(h.path.B.cons h.path.hδ).comp d.path, d.value⟩ ≺ ⟨A, inr L.toNearLitter⟩)
-    {B : ExtendedIndex δ} {a : Atom} (hc : ⟨B, inl a⟩ ∈ (t.support).carrier) :
+    {B : ExtendedIndex δ} {a : Atom} (hc : ⟨B, inl a⟩ ∈ t.support) :
     (⟨(h.path.B.cons h.path.hδ).comp ((C.cons hδ).comp B), inl a⟩ : SupportCondition β) <
       ⟨A, inr L.toNearLitter⟩ := by
   refine' Relation.TransGen.tail' _ hd

ConNF/Fuzz/Hypotheses.lean

@@ -67,6 +67,34 @@ instance : MulAction (Allowable α) X :=
 theorem toStructPerm_smul (ρ : Allowable α) (x : X) : ρ • x = Allowable.toStructPerm ρ • x :=
   rfl
 
+@[simp]
+theorem smul_support_max (ρ : Allowable α) (S : Support α) :
+    (ρ • S).max = S.max :=
+  rfl
+
+@[simp]
+theorem smul_support_f (ρ : Allowable α) (S : Support α) (i : κ) (hi : i < S.max) :
+    (ρ • S).f i hi = ρ • S.f i hi :=
+  rfl
+
+@[simp]
+theorem smul_support_coe (ρ : Allowable α) (S : Support α) :
+    (ρ • S : Support α) = ρ • (S : Set (SupportCondition α)) :=
+  Support.smul_coe _ _
+
+@[simp]
+theorem smul_mk_support (ρ : Allowable α) (E : Enumeration (SupportCondition α)) (h) :
+    ρ • Support.mk E h = Support.mk (ρ • E) ((Support.mk E h).mem_of_mem_symmDiff_smul _) :=
+  rfl
+
+theorem smul_mem_smul_support {S : Support α} {c : SupportCondition α}
+    (h : c ∈ S) (ρ : Allowable α) : ρ • c ∈ ρ • S :=
+  Support.smul_mem_smul h _
+
+theorem smul_eq_of_smul_support_eq {S : Support α} {ρ : Allowable α}
+    (hS : ρ • S = S) {c : SupportCondition α} (hc : c ∈ S) : ρ • c = c :=
+  Support.smul_eq_of_smul_eq hS hc
+
 variable {ρ ρ' : Allowable α} {c : SupportCondition α}
 
 theorem smul_supportCondition :
@@ -145,10 +173,11 @@ instance Bot.tangleData : TangleData ⊥
   Allowable := NearLitterPerm
   allowableToStructPerm := Tree.toBotIso.toMonoidHom
   allowableAction := inferInstance
-  support a := ⟨1, fun _ _ => ⟨Quiver.Path.nil, Sum.inl a⟩⟩
+  support a := Support.singleton ⟨Quiver.Path.nil, Sum.inl a⟩
   support_supports a π h := by
-    simp only [Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
-      NearLitterPerm.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inl, Sum.inl.injEq] at h
+    simp only [Support.singleton_enum, Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop,
+      exists_eq_left, NearLitterPerm.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inl,
+      Sum.inl.injEq] at h
     exact h
 
 /-- A position function for atoms, which is chosen arbitrarily. -/

ConNF/NewTangle/NewTangle.lean

@@ -460,13 +460,14 @@ theorem NewAllowable.smul_supportCondition_eq_smul_iff
 This is called a *typed near litter*. -/
 def newTypedNearLitter (N : NearLitter) : NewTangle :=
   ⟨intro (show Set (Tangle ⊥) from N.2.1) <| Code.isEven_bot _,
-    ⟨1, fun _ _ => ⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inr N⟩⟩,
+    Support.singleton ⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inr N⟩,
     by
       intro ρ h
       simp only [smul_intro]
       congr 1
-      simp only [Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
-        NewAllowable.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inr, Sum.inr.injEq] at h
+      simp only [Support.singleton_enum, Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop,
+        exists_eq_left, NewAllowable.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inr,
+        Sum.inr.injEq] at h 
       apply_fun SetLike.coe at h
       refine Eq.trans ?_ h
       rw [NearLitterPerm.smul_nearLitter_coe]