Base coding

Signed-off-by: Sky Wilshaw <[email protected]>

ConNF/Counting/BaseCoding.lean

@@ -32,6 +32,18 @@ theorem addAtom'_nearLitters (S : BaseSupport) (a : Atom) :
     (addAtom' S a)ᴺ = Sᴺ :=
   rfl
 
+theorem addAtom'_atoms_rel (S : BaseSupport) (a : Atom) (i : κ) (b : Atom) :
+    (addAtom' S a)ᴬ.rel i b ↔ Sᴬ.rel i b ∨ (b = a ∧ i = Sᴬ.bound) := by
+  constructor
+  · rintro (hb | ⟨_, rfl, rfl, rfl⟩)
+    · exact Or.inl hb
+    · refine Or.inr ⟨rfl, ?_⟩
+      simp only [add_zero]
+  · rintro (hb | ⟨rfl, rfl⟩)
+    · exact Or.inl hb
+    · refine Or.inr ⟨0, ?_, rfl, rfl⟩
+      simp only [Rel.inv_apply, Function.graph_def, add_zero]
+
 theorem addAtom'_closed (S : BaseSupport) (a : Atom) (hS : S.Closed) :
     (addAtom' S a).Closed := by
   constructor
@@ -50,14 +62,17 @@ theorem Support.ofBase_derivBot (S : BaseSupport) (A : ⊥ ↝ ⊥) :
     Support.ofBase S ⇘. A = S :=
   rfl
 
+theorem InflexiblePath.elim_bot (P : InflexiblePath ⊥) : False := by
+  have := le_antisymm P.A.le bot_le
+  have := P.hδ.trans_eq this
+  exact not_lt_bot this
+
 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
+  intro _ _ _ P
+  cases P.elim_bot
 
 def addAtom (S : BaseSupport) (a : Atom) : Support ⊥ :=
   .ofBase (addAtom' S a)
@@ -75,19 +90,88 @@ theorem addAtom_strong (S : BaseSupport) (a : Atom) (hS : S.Closed) : (addAtom S
     rw [addAtom_derivBot]
     exact addAtom'_closed S a hS
 
-theorem addAtom_spec_eq_spec {S : BaseSupport} (hS : S.Closed) {a₁ a₂ : Atom}
+omit [Level] [CoherentData] in
+@[simp]
+theorem addAtom_convAtoms (S : BaseSupport) (a₁ a₂ : Atom) (A : ⊥ ↝ ⊥) :
+    convAtoms (addAtom S a₁) (addAtom S a₂) A =
+      (λ a₃ a₄ ↦ (a₃ = a₄ ∧ a₃ ∈ Sᴬ) ∨ (a₃ = a₁ ∧ a₄ = a₂)) := by
+  ext a₃ a₄
+  simp only [convAtoms, Rel.comp, addAtom_derivBot, Rel.inv_apply, addAtom'_atoms_rel]
+  constructor
+  · rintro ⟨i, hi₃ | hi₃, hi₄ | hi₄⟩
+    · exact Or.inl ⟨Sᴬ.rel_coinjective.coinjective hi₃ hi₄, i, hi₃⟩
+    · cases (Sᴬ.lt_bound i ⟨a₃, hi₃⟩).ne hi₄.2
+    · cases (Sᴬ.lt_bound i ⟨a₄, hi₄⟩).ne hi₃.2
+    · exact Or.inr ⟨hi₃.1, hi₄.1⟩
+  · rintro (⟨rfl, i, ha⟩ | ⟨rfl, rfl⟩)
+    · exact ⟨i, Or.inl ha, Or.inl ha⟩
+    · exact ⟨Sᴬ.bound, Or.inr ⟨rfl, rfl⟩, Or.inr ⟨rfl, rfl⟩⟩
+
+omit [Level] [CoherentData] in
+@[simp]
+theorem addAtom_convNearLitters (S : BaseSupport) (a₁ a₂ : Atom) (A : ⊥ ↝ ⊥) :
+    convNearLitters (addAtom S a₁) (addAtom S a₂) A = (λ N₁ N₂ ↦ N₁ = N₂ ∧ N₁ ∈ Sᴺ) := by
+  ext N₁ N₂
+  constructor
+  · rintro ⟨i, hi₁, hi₂⟩
+    exact ⟨Sᴺ.rel_coinjective.coinjective hi₁ hi₂, i, hi₁⟩
+  · rintro ⟨rfl, i, hi⟩
+    exact ⟨i, hi, hi⟩
+
+theorem addAtom_sameSpecLe {S : BaseSupport} {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]
+    SameSpecLE (addAtom S a₁) (addAtom S a₂) := by
   constructor
   · intro; rfl
   · intro; rfl
-  all_goals sorry
+  · intro A
+    simp only [addAtom_derivBot, Rel.dom, addAtom'_atoms_rel]
+    rintro i ⟨a, hi | ⟨rfl, rfl⟩⟩
+    · exact ⟨a, Or.inl hi⟩
+    · exact ⟨a₂, Or.inr ⟨rfl, rfl⟩⟩
+  · intro; rfl
+  · intro A
+    constructor
+    intro b₁ b₂ c hb₁ hb₂
+    rw [addAtom_convAtoms] at hb₁ hb₂
+    obtain (hb₁ | hb₁) := hb₁ <;> obtain (hb₂ | hb₂) := hb₂
+    · exact hb₁.1.trans hb₂.1.symm
+    · cases ha₂ (hb₁.1.trans hb₂.2 ▸ hb₁.2)
+    · cases ha₂ (hb₂.1.trans hb₁.2 ▸ hb₂.2)
+    · exact hb₁.1.trans hb₂.1.symm
+  · rintro A i j ⟨N, hi, a, haN, hj⟩
+    refine ⟨N, hi, ?_⟩
+    obtain (ha | ⟨j, rfl, rfl, rfl⟩) := hj
+    · exact ⟨a, haN, Or.inl ha⟩
+    · refine ⟨a₂, ?_, Or.inr ⟨_, rfl, rfl, rfl⟩⟩
+      dsimp only
+      rw [← ha]
+      · exact haN
+      · exact ⟨i, hi⟩
+  · intro _ _ _ _ P
+    cases P.elim_bot
+  · intro A N₁ N₂ N₃ N₄ h₁ h₂ _ _ _ _ h
+    rw [addAtom_convNearLitters] at h₁ h₂
+    cases h₁.1
+    cases h₂.1
+    exact h
+  · intro _ _ _ P
+    cases P.elim_bot
+  · intro _ _ _ P
+    cases P.elim_bot
+
+theorem addAtom_spec_eq_spec {S : BaseSupport} {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]
+  apply sameSpec_antisymm
+  · exact addAtom_sameSpecLe ha₁ ha₂ ha
+  · exact addAtom_sameSpecLe ha₂ ha₁ (λ N hN ↦ (ha N hN).symm)
 
 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)
+  obtain ⟨ρ, hρ⟩ := Support.exists_conv (addAtom_spec_eq_spec 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ρ