diff --git a/ConNF.lean b/ConNF.lean index 064bfd7f20..6c4184c2a7 100644 --- a/ConNF.lean +++ b/ConNF.lean @@ -6,6 +6,7 @@ import ConNF.Aux.Rel import ConNF.Aux.Set import ConNF.Aux.Transfer import ConNF.Aux.WellOrder +import ConNF.Counting.BaseCoding import ConNF.Counting.CodingFunction import ConNF.Counting.Recode import ConNF.Counting.SmulSpec diff --git a/ConNF/Aux/Rel.lean b/ConNF/Aux/Rel.lean index 0311064602..7c6ea237cf 100644 --- a/ConNF/Aux/Rel.lean +++ b/ConNF/Aux/Rel.lean @@ -80,6 +80,7 @@ theorem codomEqDom_iff' (r : Rel α α) : theorem OneOne.inv {r : Rel α β} (h : r.OneOne) : r.inv.OneOne := ⟨⟨h.coinjective⟩, ⟨h.injective⟩⟩ +@[simp] theorem inv_apply {r : Rel α β} {x : α} {y : β} : r.inv y x ↔ r x y := Iff.rfl diff --git a/ConNF/Counting/BaseCoding.lean b/ConNF/Counting/BaseCoding.lean new file mode 100644 index 0000000000..46a8ced552 --- /dev/null +++ b/ConNF/Counting/BaseCoding.lean @@ -0,0 +1,105 @@ +import ConNF.Counting.SpecSame + +/-! +# Coding the base type + +In this file, we prove a consequence of freedom of action for `⊥`: a base support can support at +most `2 ^ #κ`-many different sets of atoms under the action of base permutations. + +## Main declarations + +* `ConNF.foo`: Something new. +-/ + +noncomputable section +universe u + +open Cardinal Ordinal + +namespace ConNF + +variable [Params.{u}] + +def addAtom' (S : BaseSupport) (a : Atom) : BaseSupport where + atoms := Sᴬ + .singleton a + nearLitters := Sᴺ + +theorem addAtom'_atoms (S : BaseSupport) (a : Atom) : + (addAtom' S a)ᴬ = Sᴬ + .singleton a := + rfl + +theorem addAtom'_nearLitters (S : BaseSupport) (a : Atom) : + (addAtom' S a)ᴺ = Sᴺ := + rfl + +theorem addAtom'_closed (S : BaseSupport) (a : Atom) (hS : S.Closed) : + (addAtom' S a).Closed := by + constructor + intro N₁ N₂ hN₁ hN₂ b hb + rw [addAtom'_atoms, Enumeration.mem_add_iff] + exact Or.inl (hS.interference_subset hN₁ hN₂ b hb) + +def Support.ofBase (S : BaseSupport) : Support ⊥ where + atoms := + Sᴬ.invImage Prod.snd (λ _ _ ↦ Prod.ext ((Path.eq_nil _).trans (Path.eq_nil _).symm)) + nearLitters := + Sᴺ.invImage Prod.snd (λ _ _ ↦ Prod.ext ((Path.eq_nil _).trans (Path.eq_nil _).symm)) + +@[simp] +theorem Support.ofBase_derivBot (S : BaseSupport) (A : ⊥ ↝ ⊥) : + Support.ofBase S ⇘. A = S := + rfl + +variable [Level] [CoherentData] + +theorem bot_preStrong (S : Support ⊥) : S.PreStrong := by + constructor + intro A N _ P + have := le_antisymm P.A.le bot_le + have := P.hδ.trans_eq this + cases not_lt_bot this + +def addAtom (S : BaseSupport) (a : Atom) : Support ⊥ := + .ofBase (addAtom' S a) + +omit [Level] [CoherentData] in +theorem addAtom_derivBot (S : BaseSupport) (a : Atom) (A : ⊥ ↝ ⊥) : + addAtom S a ⇘. A = addAtom' S a := + rfl + +theorem addAtom_strong (S : BaseSupport) (a : Atom) (hS : S.Closed) : (addAtom S a).Strong := by + constructor + · exact bot_preStrong _ + · constructor + intro A + rw [addAtom_derivBot] + exact addAtom'_closed S a hS + +theorem addAtom_spec_eq_spec {S : BaseSupport} (hS : S.Closed) {a₁ a₂ : Atom} + (ha₁ : a₁ ∉ Sᴬ) (ha₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) : + (addAtom S a₁).spec = (addAtom S a₂).spec := by + rw [Support.spec_eq_spec_iff] + constructor + · intro; rfl + · intro; rfl + all_goals sorry + +theorem exists_swap {S : BaseSupport} (h : S.Closed) {a₁ a₂ : Atom} + (ha₁ : a₁ ∉ Sᴬ) (ha₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) : + ∃ π : BasePerm, π • S = S ∧ π • a₁ = a₂ := by + obtain ⟨ρ, hρ⟩ := Support.exists_conv (addAtom_spec_eq_spec h ha₁ ha₂ ha) + (addAtom_strong S a₁ h) (addAtom_strong S a₂ h) + have hρa := congr_arg (λ S ↦ (S ⇘. .nil)ᴬ) hρ + have hρN := congr_arg (λ S ↦ (S ⇘. .nil)ᴺ) hρ + simp only [Support.smul_derivBot, BaseSupport.smul_atoms, BaseSupport.smul_nearLitters, + addAtom_derivBot, addAtom'_atoms, addAtom'_nearLitters, Enumeration.smul_add] at hρa hρN + rw [Enumeration.add_inj_iff_of_bound_eq_bound (by rfl)] at hρa + simp only [Enumeration.smul_singleton, Enumeration.singleton_injective.eq_iff] at hρa + obtain ⟨hρa, rfl⟩ := hρa + refine ⟨ρᵁ .nil, ?_, rfl⟩ + rw [BaseSupport.smul_eq_iff] + constructor + · exact Enumeration.eq_of_smul_eq hρa + · exact Enumeration.eq_of_smul_eq hρN + +end ConNF diff --git a/ConNF/Counting/SpecSame.lean b/ConNF/Counting/SpecSame.lean index 137bb2d5cc..8bbebdecbf 100644 --- a/ConNF/Counting/SpecSame.lean +++ b/ConNF/Counting/SpecSame.lean @@ -105,7 +105,7 @@ theorem interference_subset_convAtoms_dom (hST : S.spec = T.spec) (hS : S.Strong intro a ha obtain ⟨N₃, i, hiS, hiT⟩ := hN₁ obtain ⟨N₄, j, hjS, hjT⟩ := hN₂ - obtain ⟨k, hkS⟩ := hS.interference_subset ⟨i, hiS⟩ ⟨j, hjS⟩ a ha + obtain ⟨k, hkS⟩ := (hS.closed _).interference_subset ⟨i, hiS⟩ ⟨j, hjS⟩ a ha rw [spec_eq_spec_iff] at hST obtain ⟨a', hkT⟩ := hST.atoms_dom_of_dom hkS exact ⟨a', k, hkS, hkT⟩ @@ -117,7 +117,7 @@ theorem interference_subset_convAtoms_codom (hST : S.spec = T.spec) (hT : T.Stro intro a ha obtain ⟨N₃, i, hiS, hiT⟩ := hN₁ obtain ⟨N₄, j, hjS, hjT⟩ := hN₂ - obtain ⟨k, hkT⟩ := hT.interference_subset ⟨i, hiT⟩ ⟨j, hjT⟩ a ha + obtain ⟨k, hkT⟩ := (hT.closed _).interference_subset ⟨i, hiT⟩ ⟨j, hjT⟩ a ha rw [spec_eq_spec_iff] at hST obtain ⟨a', hkS⟩ := (sameSpec_comm hST).atoms_dom_of_dom hkT exact ⟨a', k, hkS, hkT⟩ diff --git a/ConNF/Counting/Strong.lean b/ConNF/Counting/Strong.lean index 0122b77f65..e6fe82db0d 100644 --- a/ConNF/Counting/Strong.lean +++ b/ConNF/Counting/Strong.lean @@ -21,6 +21,10 @@ namespace ConNF variable [Params.{u}] {β : TypeIndex} +structure BaseSupport.Closed (S : BaseSupport) : Prop where + interference_subset {N₁ N₂ : NearLitter} : + N₁ ∈ Sᴺ → N₂ ∈ Sᴺ → ∀ a ∈ interference N₁ N₂, a ∈ Sᴬ + namespace Support variable [Level] [CoherentData] [LeLevel β] @@ -31,9 +35,10 @@ structure PreStrong (S : Support β) : Prop where (hA : A = P.A ↘ P.hε ↘.) (ht : Nᴸ = fuzz P.hδε t) : t.support ≤ S ⇘ (P.A ↘ P.hδ) -structure Strong (S : Support β) extends S.PreStrong : Prop where - interference_subset {A : β ↝ ⊥} {N₁ N₂ : NearLitter} : - N₁ ∈ (S ⇘. A)ᴺ → N₂ ∈ (S ⇘. A)ᴺ → ∀ a ∈ interference N₁ N₂, a ∈ (S ⇘. A)ᴬ +structure Closed (S : Support β) : Prop where + closed : ∀ A, (S ⇘. A).Closed + +structure Strong (S : Support β) extends S.PreStrong, S.Closed : Prop theorem PreStrong.smul {S : Support β} (hS : S.PreStrong) (ρ : AllPerm β) : (ρᵁ • S).PreStrong := by constructor @@ -51,15 +56,19 @@ theorem PreStrong.smul {S : Support β} (hS : S.PreStrong) (ρ : AllPerm β) : ( BasePerm.smul_nearLitter_litter, ← Tree.inv_apply, hA, ht] rfl -theorem Strong.smul {S : Support β} (hS : S.Strong) (ρ : AllPerm β) : (ρᵁ • S).Strong := by +theorem Closed.smul {S : Support β} (hS : S.Closed) (ρ : AllPerm β) : (ρᵁ • S).Closed := by + constructor + intro A constructor - · exact hS.toPreStrong.smul ρ - · intro A N₁ N₂ h₁ h₂ - simp only [smul_derivBot, BaseSupport.smul_nearLitters, BaseSupport.smul_atoms, - Enumeration.mem_smul] at h₁ h₂ ⊢ - intro a ha - apply hS.interference_subset h₁ h₂ - rwa [← BasePerm.smul_interference, Set.smul_mem_smul_set_iff] + intro N₁ N₂ h₁ h₂ + simp only [smul_derivBot, BaseSupport.smul_nearLitters, BaseSupport.smul_atoms, + Enumeration.mem_smul] at h₁ h₂ ⊢ + intro a ha + apply (hS.closed A).interference_subset h₁ h₂ + rwa [← BasePerm.smul_interference, Set.smul_mem_smul_set_iff] + +theorem Strong.smul {S : Support β} (hS : S.Strong) (ρ : AllPerm β) : (ρᵁ • S).Strong := + ⟨hS.toPreStrong.smul ρ, hS.toClosed.smul ρ⟩ def Constrains : Rel (β ↝ ⊥ × NearLitter) (β ↝ ⊥ × NearLitter) := λ x y ↦ ∃ (P : InflexiblePath β) (t : Tangle P.δ) (B : P.δ ↝ ⊥), @@ -238,39 +247,53 @@ theorem interferenceSupport_nearLitters (S : Support β) (A : β ↝ ⊥) : (S.interferenceSupport ⇘. A)ᴺ = .empty := rfl +def close (S : Support β) : Support β := + S + S.interferenceSupport + +theorem le_close (S : Support β) : + S ≤ S.close := + le_add_right + +theorem close_atoms (S : Support β) (A : β ↝ ⊥) : + (S.close ⇘. A)ᴬ = (S ⇘. A)ᴬ + (S.interferenceSupport ⇘. A)ᴬ := + rfl + +theorem close_nearLitters (S : Support β) (A : β ↝ ⊥) : + (S.close ⇘. A)ᴺ = (S ⇘. A)ᴺ := by + rw [close, add_derivBot, BaseSupport.add_nearLitters, interferenceSupport_nearLitters, + Enumeration.add_empty] + +theorem close_closed (S : Support β) : + S.close.Closed := by + constructor + intro A + constructor + intro N₁ N₂ hN₁ hN₂ a ha + rw [close_nearLitters] at hN₁ hN₂ + rw [close_atoms, Enumeration.mem_add_iff, mem_interferenceSupport_atoms] + exact Or.inr ⟨N₁, hN₁, N₂, hN₂, ha⟩ + def strong (S : Support β) : Support β := - S.preStrong + S.preStrong.interferenceSupport + S.preStrong.close theorem preStrong_le_strong (S : Support β) : S.preStrong ≤ S.strong := - le_add_right + S.preStrong.le_close theorem le_strong (S : Support β) : S ≤ S.strong := S.le_preStrong.trans S.preStrong_le_strong -theorem strong_atoms (S : Support β) (A : β ↝ ⊥) : - (S.strong ⇘. A)ᴬ = (S.preStrong ⇘. A)ᴬ + (S.preStrong.interferenceSupport ⇘. A)ᴬ := - rfl - -theorem strong_nearLitters (S : Support β) (A : β ↝ ⊥) : - (S.strong ⇘. A)ᴺ = (S.preStrong ⇘. A)ᴺ := by - rw [strong, add_derivBot, BaseSupport.add_nearLitters, interferenceSupport_nearLitters, - Enumeration.add_empty] - theorem strong_strong (S : Support β) : S.strong.Strong := by constructor · constructor intro A N hN P t hA ht - rw [strong_nearLitters] at hN + rw [strong, close_nearLitters] at hN apply (S.preStrong_preStrong.support_le hN P t hA ht).trans intro B exact S.preStrong_le_strong (P.A ↘ P.hδ ⇘ B) - · intro A N₁ N₂ hN₁ hN₂ a ha - rw [strong_nearLitters] at hN₁ hN₂ - rw [strong_atoms, Enumeration.mem_add_iff, mem_interferenceSupport_atoms] - exact Or.inr ⟨N₁, hN₁, N₂, hN₂, ha⟩ + · exact close_closed _ end Support end ConNF diff --git a/ConNF/Setup/Enumeration.lean b/ConNF/Setup/Enumeration.lean index cdcd888e66..c354da66de 100644 --- a/ConNF/Setup/Enumeration.lean +++ b/ConNF/Setup/Enumeration.lean @@ -294,7 +294,7 @@ theorem mem_smul_iff {G X : Type _} [Group G] [MulAction G X] (x : X) (g : G) (E x ∈ g • E ↔ g⁻¹ • x ∈ E := Iff.rfl -theorem eq_of_smul_eq {G X : Type _} [Group G] [MulAction G X] {g₁ g₂ : G} {E : Enumeration X} +theorem eq_of_smul_eq_smul {G X : Type _} [Group G] [MulAction G X] {g₁ g₂ : G} {E : Enumeration X} (h : g₁ • E = g₂ • E) (x : X) (hx : x ∈ E) : g₁ • x = g₂ • x := by obtain ⟨i, hi⟩ := hx have : (g₁ • E).rel i (g₁ • x) := by rwa [smul_rel, inv_smul_smul] @@ -302,6 +302,21 @@ theorem eq_of_smul_eq {G X : Type _} [Group G] [MulAction G X] {g₁ g₂ : G} { have := E.rel_coinjective.coinjective hi this exact (eq_inv_smul_iff.mp this).symm +theorem eq_of_smul_eq {G X : Type _} [Group G] [MulAction G X] {g : G} {E : Enumeration X} + (h : g • E = E) (x : X) (hx : x ∈ E) : g • x = x := by + have := eq_of_smul_eq_smul (g₁ := g) (g₂ := 1) ?_ x hx + · rwa [one_smul] at this + · rwa [one_smul] + +@[simp] +theorem smul_singleton {G X : Type _} [Group G] [MulAction G X] {g : G} {x : X} : + g • singleton x = singleton (g • x) := by + apply Enumeration.ext + · rfl + · ext i y + rw [smul_rel] + simp only [singleton, and_congr_right_iff, inv_smul_eq_iff] + /-! ## Concatenation of enumerations -/ @@ -367,6 +382,61 @@ theorem add_empty (E : Enumeration X) : · rw [add_bound, empty, add_zero] · simp only [empty, rel_add_iff, and_false, exists_const, or_false] +theorem add_inj_of_bound_eq_bound {E F G H : Enumeration X} (h : E.bound = F.bound) + (h' : E + G = F + H) : E = F ∧ G = H := by + have := congr_arg (·.rel) h' + conv at this => dsimp only; rw [funext_iff]; intro; rw [funext_iff]; intro; rw [eq_iff_iff] + constructor + · apply Enumeration.ext h + ext i x + constructor + · intro hx + obtain (hx' | ⟨j, rfl, _⟩) := (this i x).mp (Or.inl hx) + · exact hx' + · have := E.lt_bound _ ⟨x, hx⟩ + rw [h, add_lt_iff_neg_left] at this + cases (κ_zero_le j).not_lt this + · intro hx + obtain (hx' | ⟨j, rfl, _⟩) := (this i x).mpr (Or.inl hx) + · exact hx' + · have := F.lt_bound _ ⟨x, hx⟩ + rw [h, add_lt_iff_neg_left] at this + cases (κ_zero_le j).not_lt this + · apply Enumeration.ext + · have := congr_arg (·.bound) h' + simp only [add_bound, h, add_right_inj] at this + exact this + ext i x + constructor + · intro hx + obtain (hx' | ⟨j, hj₁, hj₂⟩) := (this (E.bound + i) x).mp (Or.inr ⟨i, rfl, hx⟩) + · have := F.lt_bound _ ⟨x, hx'⟩ + rw [h, add_lt_iff_neg_left] at this + cases (κ_zero_le i).not_lt this + · simp only [h, Rel.inv_apply, Function.graph_def, add_right_inj] at hj₁ + rw [← hj₁] + exact hj₂ + · intro hx + obtain (hx' | ⟨j, hj₁, hj₂⟩) := (this (F.bound + i) x).mpr (Or.inr ⟨i, rfl, hx⟩) + · have := E.lt_bound _ ⟨x, hx'⟩ + rw [h, add_lt_iff_neg_left] at this + cases (κ_zero_le i).not_lt this + · simp only [h, Rel.inv_apply, Function.graph_def, add_right_inj] at hj₁ + rw [← hj₁] + exact hj₂ + +theorem add_inj_iff_of_bound_eq_bound {E F G H : Enumeration X} (h : E.bound = F.bound) : + E + G = F + H ↔ E = F ∧ G = H := by + constructor + · exact add_inj_of_bound_eq_bound h + · rintro ⟨rfl, rfl⟩ + rfl + +@[simp] +theorem smul_add {G X : Type _} [Group G] [MulAction G X] (g : G) (E F : Enumeration X) : + g • (E + F) = g • E + g • F := + rfl + -- TODO: Some stuff about the partial order on enumerations and concatenation of enumerations. end Enumeration diff --git a/ConNF/Setup/ModelData.lean b/ConNF/Setup/ModelData.lean index ce4bcaa5ad..431e4b04f8 100644 --- a/ConNF/Setup/ModelData.lean +++ b/ConNF/Setup/ModelData.lean @@ -175,13 +175,13 @@ theorem Tangle.smul_atom_eq_of_mem_support {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} {t : Tangle α} (h : ρ₁ • t = ρ₂ • t) {a : Atom} {A : α ↝ ⊥} (ha : a ∈ (t.support ⇘. A)ᴬ) : ρ₁ᵁ A • a = ρ₂ᵁ A • a := - Enumeration.eq_of_smul_eq (congr_arg (λ t ↦ (t.support ⇘. A)ᴬ) h) a ha + Enumeration.eq_of_smul_eq_smul (congr_arg (λ t ↦ (t.support ⇘. A)ᴬ) h) a ha theorem Tangle.smul_nearLitter_eq_of_mem_support {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} {t : Tangle α} (h : ρ₁ • t = ρ₂ • t) {N : NearLitter} {A : α ↝ ⊥} (hN : N ∈ (t.support ⇘. A)ᴺ) : ρ₁ᵁ A • N = ρ₂ᵁ A • N := - Enumeration.eq_of_smul_eq (congr_arg (λ t ↦ (t.support ⇘. A)ᴺ) h) N hN + Enumeration.eq_of_smul_eq_smul (congr_arg (λ t ↦ (t.support ⇘. A)ᴺ) h) N hN /-! ## Criteria for supports diff --git a/ConNF/Setup/Support.lean b/ConNF/Setup/Support.lean index 98a9d215a5..c8d8e4ffa3 100644 --- a/ConNF/Setup/Support.lean +++ b/ConNF/Setup/Support.lean @@ -130,6 +130,12 @@ theorem smul_eq_smul_iff (π₁ π₂ : BasePerm) (S : BaseSupport) : rw [smul_inv_smul, smul_eq_iff_eq_inv_smul] at this rwa [← this] +theorem smul_eq_iff (π : BasePerm) (S : BaseSupport) : + π • S = S ↔ (∀ a ∈ Sᴬ, π • a = a) ∧ (∀ N ∈ Sᴺ, π • N = N) := by + have := smul_eq_smul_iff π 1 S + simp only [one_smul] at this + exact this + noncomputable instance : Add BaseSupport where add S T := ⟨Sᴬ + Tᴬ, Sᴺ + Tᴺ⟩