From 209a7c929d972bf89ea418b02d62d726021c1139 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Thu, 25 Jan 2024 00:38:22 +0000 Subject: [PATCH] Litter maps in near-litter behaviours Signed-off-by: zeramorphic --- ConNF/FOA/Behaviour/NearLitterBehaviour.lean | 247 ++++++++++++++++++- 1 file changed, 240 insertions(+), 7 deletions(-) diff --git a/ConNF/FOA/Behaviour/NearLitterBehaviour.lean b/ConNF/FOA/Behaviour/NearLitterBehaviour.lean index 34dabdd862..b1ddaf7ada 100644 --- a/ConNF/FOA/Behaviour/NearLitterBehaviour.lean +++ b/ConNF/FOA/Behaviour/NearLitterBehaviour.lean @@ -24,13 +24,17 @@ structure Lawful (ξ : NearLitterBehaviour) : Prop where (ξ.atomMap a).get ha = (ξ.atomMap b).get hb → a = b atom_mem_iff : ∀ ⦃a : Atom⦄ (ha : (ξ.atomMap a).Dom) ⦃N : NearLitter⦄ (hN : (ξ.nearLitterMap N).Dom), - a ∈ N ↔ (ξ.atomMap a).get ha ∈ (ξ.nearLitterMap N).get hN - map_nearLitter_fst : ∀ ⦃N₁ N₂ : NearLitter⦄ - (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom), - N₁.fst = N₂.fst ↔ ((ξ.nearLitterMap N₁).get hN₁).fst = ((ξ.nearLitterMap N₂).get hN₂).fst - mem_of_mem_symmDiff : ∀ ⦃a : Atom⦄ ⦃N₁ N₂ : NearLitter⦄, + (ξ.atomMap a).get ha ∈ (ξ.nearLitterMap N).get hN ↔ a ∈ N + -- map_nearLitter_fst : ∀ ⦃N₁ N₂ : NearLitter⦄ + -- (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom), + -- N₁.fst = N₂.fst ↔ ((ξ.nearLitterMap N₁).get hN₁).fst = ((ξ.nearLitterMap N₂).get hN₂).fst + dom_of_mem_symmDiff : ∀ (a : Atom) ⦃N₁ N₂ : NearLitter⦄, N₁.fst = N₂.fst → (ξ.nearLitterMap N₁).Dom → (ξ.nearLitterMap N₂).Dom → a ∈ (N₁ : Set Atom) ∆ N₂ → (ξ.atomMap a).Dom + ran_of_mem_symmDiff : ∀ (a : Atom) ⦃N₁ N₂ : NearLitter⦄, + N₁.fst = N₂.fst → (hN₁ : (ξ.nearLitterMap N₁).Dom) → (hN₂ : (ξ.nearLitterMap N₂).Dom) → + a ∈ ((ξ.nearLitterMap N₁).get hN₁ : Set Atom) ∆ (ξ.nearLitterMap N₂).get hN₂ → + a ∈ ξ.atomMap.ran instance : PartialOrder NearLitterBehaviour where @@ -52,8 +56,237 @@ def action (ξ : NearLitterBehaviour) : NearLitterAction where atomMap_dom_small := ξ.atomMap_dom_small litterMap_dom_small := Small.preimage (fun _ _ => congr_arg Sigma.fst) (ξ.nearLitterMap_dom_small) -theorem exists_hasLitters (ξ : NearLitterBehaviour) (hξ : ξ.Lawful) : - ∃ ξ' ≥ ξ, ξ'.Lawful ∧ ξ'.HasLitters := sorry +def extraAtoms (ξ : NearLitterBehaviour) : Set Atom := + ⋃ (N ∈ ξ.nearLitterMap.Dom), litterSet N.1 ∆ N + +theorem extraAtoms_small (ξ : NearLitterBehaviour) : Small ξ.extraAtoms := + Small.bUnion ξ.nearLitterMap_dom_small (fun N _ => N.2.2) + +@[mk_iff] +inductive BannedLitter (ξ : NearLitterBehaviour) : Litter → Prop + | atomMap (a : Atom) (h) : BannedLitter ξ ((ξ.atomMap a).get h).1 + | nearLitterMap (N : NearLitter) (h) : BannedLitter ξ ((ξ.nearLitterMap N).get h).1 + | diff (N : NearLitter) (h) (a : Atom) : + a ∈ ((ξ.nearLitterMap N).get h : Set Atom) \ litterSet ((ξ.nearLitterMap N).get h).1 → + BannedLitter ξ a.1 + +theorem bannedLitter_of_mem {ξ : NearLitterBehaviour} (a : Atom) (N : NearLitter) + (hN : (ξ.nearLitterMap N).Dom) (ha : a ∈ (ξ.nearLitterMap N).get hN) : ξ.BannedLitter a.1 := by + by_cases h : a.1 = (Part.get (nearLitterMap ξ N) hN).1 + · rw [h] + exact BannedLitter.nearLitterMap N hN + · exact BannedLitter.diff N hN _ ⟨ha, h⟩ + +theorem bannedLitter_small (ξ : NearLitterBehaviour) : Small {L | ξ.BannedLitter L} := by + simp only [bannedLitter_iff, mem_diff, SetLike.mem_coe, mem_litterSet] + refine Small.union ?_ (Small.union ?_ ?_) + · refine' lt_of_le_of_lt _ ξ.atomMap_dom_small + refine' ⟨⟨fun L => ⟨_, L.prop.choose_spec.choose⟩, fun L₁ L₂ h => _⟩⟩ + simp only [Subtype.mk_eq_mk, Prod.mk.inj_iff] at h + have := L₁.prop.choose_spec.choose_spec + simp_rw [h] at this + exact Subtype.coe_injective (this.trans L₂.prop.choose_spec.choose_spec.symm) + · refine' lt_of_le_of_lt _ ξ.nearLitterMap_dom_small + refine' ⟨⟨fun L => ⟨_, L.prop.choose_spec.choose⟩, fun L₁ L₂ h => _⟩⟩ + simp only [Subtype.mk_eq_mk, Prod.mk.inj_iff] at h + have := L₁.prop.choose_spec.choose_spec + simp_rw [h] at this + exact Subtype.coe_injective (this.trans L₂.prop.choose_spec.choose_spec.symm) + · have : Small + (⋃ (L : NearLitter) (h : (ξ.nearLitterMap L).Dom), + ((ξ.nearLitterMap L).get h : Set Atom) \ litterSet ((ξ.nearLitterMap L).get h).1) + · refine' Small.bUnion _ _ + · refine' lt_of_le_of_lt _ ξ.nearLitterMap_dom_small + refine' ⟨⟨fun N => ⟨_, N.prop⟩, fun N₁ N₂ h => _⟩⟩ + simp only [Subtype.mk_eq_mk, Prod.mk.inj_iff] at h + exact Subtype.coe_inj.mp h + · intro L hL + refine' Small.mono _ ((ξ.nearLitterMap L).get hL).2.prop + exact fun x hx => Or.inr hx + refine' lt_of_le_of_lt _ this + refine' ⟨⟨fun L => ⟨L.prop.choose_spec.choose_spec.choose, _⟩, fun L₁ L₂ h => _⟩⟩ + · simp only [mem_iUnion] + exact ⟨_, _, L.prop.choose_spec.choose_spec.choose_spec.1⟩ + simp only [Subtype.mk_eq_mk, Prod.mk.inj_iff] at h + have := L₁.prop.choose_spec.choose_spec.choose_spec.2 + rw [h] at this + exact Subtype.coe_injective (this.trans L₂.prop.choose_spec.choose_spec.choose_spec.2.symm) + +theorem mk_not_bannedLitter (ξ : NearLitterBehaviour) : #{L | ¬ξ.BannedLitter L} = #μ := by + have := mk_sum_compl {L | ξ.BannedLitter L} + rw [compl_setOf, mk_litter] at this + rw [← this, add_eq_right] + · by_contra h + have h' := add_le_add (le_of_lt ξ.bannedLitter_small) (le_of_not_le h) + rw [this] at h' + refine' not_lt_of_le h' _ + refine' Cardinal.add_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le Params.κ_lt_μ _ + exact lt_of_le_of_lt Params.κ_isRegular.aleph0_le Params.κ_lt_μ + · by_contra h + have h' := add_le_add (le_of_lt ξ.bannedLitter_small) (le_of_not_le h) + rw [this] at h' + refine' not_lt_of_le h' _ + refine' Cardinal.add_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le Params.κ_lt_μ _ + exact lt_trans ξ.bannedLitter_small Params.κ_lt_μ + +theorem not_bannedLitter_nonempty (ξ : NearLitterBehaviour) : Nonempty {L | ¬ξ.BannedLitter L} := by + simp only [← mk_ne_zero_iff, mk_not_bannedLitter, Ne.def, mk_ne_zero, not_false_iff] + +noncomputable def sandboxLitter (ξ : NearLitterBehaviour) : Litter := + ξ.not_bannedLitter_nonempty.some + +theorem sandboxLitter_not_banned (ξ : NearLitterBehaviour) : ¬ξ.BannedLitter ξ.sandboxLitter := + ξ.not_bannedLitter_nonempty.some.prop + +noncomputable irreducible_def extraAtoms_embedding (ξ : NearLitterBehaviour) : + ξ.extraAtoms ↪ litterSet ξ.sandboxLitter := + ((Cardinal.le_def _ _).mp (ξ.extraAtoms_small.le.trans (mk_litterSet _).symm.le)).some + +theorem extraAtoms_embedding_fst {ξ : NearLitterBehaviour} (a : ξ.extraAtoms) : + ¬ξ.BannedLitter (ξ.extraAtoms_embedding a).1.1 := by + rw [(ξ.extraAtoms_embedding a).prop] + exact ξ.sandboxLitter_not_banned + +noncomputable def extraAtomMap (ξ : NearLitterBehaviour) : Atom →. Atom := + fun a => ⟨(ξ.atomMap a).Dom ∨ a ∈ ξ.extraAtoms, + fun h => h.elim' (ξ.atomMap a).get (fun h => ξ.extraAtoms_embedding ⟨a, h⟩)⟩ + +variable {ξ : NearLitterBehaviour} + +theorem extraAtomMap_eq_of_dom (a : Atom) (ha : (ξ.atomMap a).Dom) : + (ξ.extraAtomMap a).get (Or.inl ha) = (ξ.atomMap a).get ha := by + dsimp only [extraAtomMap] + rw [Or.elim'_left] + +theorem extraAtomMap_eq_of_not_dom (a : Atom) (ha₁ : ¬(ξ.atomMap a).Dom) (ha₂ : a ∈ ξ.extraAtoms) : + (ξ.extraAtomMap a).get (Or.inr ha₂) = ξ.extraAtoms_embedding ⟨a, ha₂⟩ := by + dsimp only [extraAtomMap] + rw [Or.elim'_right _ _ _ ha₁] + +theorem atomMap_eq_extraAtomMap (a b : Atom) + (ha : (ξ.atomMap a).Dom) (hb : (ξ.extraAtomMap b).Dom) + (h : (ξ.atomMap a).get ha = (ξ.extraAtomMap b).get hb) : + (ξ.atomMap b).Dom := by + by_contra hb₁ + have hb₂ := hb.elim (fun h => (hb₁ h).elim) id + rw [extraAtomMap_eq_of_not_dom b hb₁ hb₂] at h + have := extraAtoms_embedding_fst ⟨b, hb₂⟩ + rw [← h] at this + exact this (BannedLitter.atomMap a ha) + +/-- Works out where `N.1.toNearLitter` should be sent. -/ +def litterMap' (N : NearLitter) (hN : (ξ.nearLitterMap N).Dom) : Set Atom := + (ξ.nearLitterMap N).get hN ∆ + {b | ∃ a, ∃ (ha : a ∈ litterSet N.1 ∆ N), + b = (ξ.extraAtomMap a).get (Or.inr ⟨_, ⟨N, rfl⟩, _, ⟨hN, rfl⟩, ha⟩)} + +theorem litterMap'_isNearLitter (N : NearLitter) (hN : (ξ.nearLitterMap N).Dom) : + IsNearLitter ((ξ.nearLitterMap N).get hN).fst (litterMap' N hN) := by + refine ((ξ.nearLitterMap N).get hN).snd.prop.trans ?_ + rw [IsNear, litterMap'] + erw [symmDiff_symmDiff_cancel_left] + have : {b | ∃ a, ∃ (ha : a ∈ litterSet N.1 ∆ N), + b = (ξ.extraAtomMap a).get (Or.inr ⟨_, ⟨N, rfl⟩, _, ⟨hN, rfl⟩, ha⟩)} + = ⋃ (a : Atom), ⋃ (ha : a ∈ litterSet N.1 ∆ N), + {(ξ.extraAtomMap a).get (Or.inr ⟨_, ⟨N, rfl⟩, _, ⟨hN, rfl⟩, ha⟩)} := by aesop + rw [this] + exact Small.bUnion N.snd.prop (fun _ _ => small_singleton _) + +def litterMap (N : NearLitter) (hN : (ξ.nearLitterMap N).Dom) : NearLitter := + ⟨((ξ.nearLitterMap N).get hN).1, litterMap' N hN, litterMap'_isNearLitter N hN⟩ + +theorem litterMap'_subset (hξ : ξ.Lawful) (N₁ N₂ : NearLitter) + (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) (h : N₁.fst = N₂.fst) : + ξ.litterMap' N₁ hN₁ ⊆ ξ.litterMap' N₂ hN₂ := by + rintro a (⟨h₁, h₂⟩ | ⟨⟨a, h₁, rfl⟩, h₂⟩) + · simp only [mem_setOf_eq, not_exists] at h₂ + by_cases h₃ : a ∈ (ξ.nearLitterMap N₂).get hN₂ + · refine Or.inl ⟨h₃, ?_⟩ + rintro ⟨a, ha, rfl⟩ + by_cases h₄ : (ξ.atomMap a).Dom + · erw [extraAtomMap_eq_of_dom _ h₄, hξ.atom_mem_iff] at h₁ h₃ + obtain (ha | ha) := ha + · cases ha.2 h₃ + · rw [← h] at ha + cases h₂ a (Or.inr ⟨h₁, ha.2⟩) rfl + · have ha : a ∈ ξ.extraAtoms := ⟨_, ⟨N₂, rfl⟩, _, ⟨hN₂, rfl⟩, ha⟩ + rw [extraAtomMap_eq_of_not_dom _ h₄ ha] at h₁ + exact extraAtoms_embedding_fst ⟨a, ha⟩ (bannedLitter_of_mem _ _ _ h₁) + · refine Or.inr ⟨?_, h₃⟩ + obtain ⟨a, ha, rfl⟩ := hξ.ran_of_mem_symmDiff a h hN₁ hN₂ (Or.inl ⟨h₁, h₃⟩) + refine ⟨a, ?_, ?_⟩ + · erw [hξ.atom_mem_iff] at h₁ h₃ + refine Or.inl ⟨?_, h₃⟩ + rw [← h] + by_contra h₄ + refine h₂ a (Or.inr ⟨h₁, h₄⟩) ?_ + rw [extraAtomMap_eq_of_dom] + · rw [extraAtomMap_eq_of_dom] + · have ha : a ∈ ξ.extraAtoms := ⟨_, ⟨N₁, rfl⟩, _, ⟨hN₁, rfl⟩, h₁⟩ + by_cases h₃ : (ξ.extraAtomMap a).get (Or.inr ha) ∈ (ξ.nearLitterMap N₂).get hN₂ + · refine Or.inl ⟨h₃, ?_⟩ + simp only [mem_setOf_eq, not_exists] + intro b hb hab + by_cases h₄ : (ξ.atomMap a).Dom + · rw [extraAtomMap_eq_of_dom _ h₄] at h₂ h₃ hab + erw [hξ.atom_mem_iff] at h₂ h₃ + have h₅ := atomMap_eq_extraAtomMap a b _ _ hab + rw [extraAtomMap_eq_of_dom _ h₅] at hab + cases hξ.atomMap_injective _ _ hab + obtain (h₁ | h₁) := h₁ + · obtain (hb | hb) := hb + · cases hb.2 h₃ + · rw [h] at h₁ + cases hb.2 h₁.1 + · cases h₂ h₁.1 + · rw [extraAtomMap_eq_of_not_dom _ h₄ ha] at h₃ + exact extraAtoms_embedding_fst ⟨a, ha⟩ (bannedLitter_of_mem _ _ hN₂ h₃) + · refine Or.inr ⟨?_, h₃⟩ + refine ⟨a, ?_, rfl⟩ + by_cases h₄ : (ξ.atomMap a).Dom + · erw [extraAtomMap_eq_of_dom _ h₄, hξ.atom_mem_iff] at h₂ h₃ + obtain (h₁ | h₁) := h₁ + · refine Or.inl ⟨?_, h₃⟩ + rw [h] at h₁ + exact h₁.1 + · cases h₂ h₁.1 + · obtain (h₁ | h₁) := h₁ + · by_cases h₅ : a ∈ N₂ + · cases h₄ (hξ.dom_of_mem_symmDiff a h hN₁ hN₂ (Or.inr ⟨h₅, h₁.2⟩)) + · refine Or.inl ⟨?_, h₅⟩ + rw [← h] + exact h₁.1 + · by_cases h₅ : a ∈ N₂ + · refine Or.inr ⟨h₅, ?_⟩ + rw [← h] + exact h₁.2 + · cases h₄ (hξ.dom_of_mem_symmDiff a h hN₁ hN₂ (Or.inl ⟨h₁.1, h₅⟩)) + +theorem litterMap_eq (hξ : ξ.Lawful) (N₁ N₂ : NearLitter) + (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) (h : N₁.fst = N₂.fst) : + ξ.litterMap N₁ hN₁ = ξ.litterMap N₂ hN₂ := by + refine NearLitter.ext (subset_antisymm ?_ ?_) + · exact litterMap'_subset hξ _ _ _ _ h + · exact litterMap'_subset hξ _ _ _ _ h.symm + +noncomputable def extendedNearLitterMap (ξ : NearLitterBehaviour) : NearLitter →. NearLitter := + fun N => + ⟨(ξ.nearLitterMap N).Dom ∨ (N.IsLitter ∧ ∃ N', (ξ.nearLitterMap N').Dom ∧ N'.1 = N.1), + fun h => h.elim' (ξ.nearLitterMap N).get (fun h => ξ.litterMap h.2.choose h.2.choose_spec.1)⟩ + +noncomputable def withLitters (ξ : NearLitterBehaviour) : NearLitterBehaviour where + atomMap := ξ.extraAtomMap + nearLitterMap := ξ.extendedNearLitterMap + atomMap_dom_small := sorry + nearLitterMap_dom_small := sorry + +theorem withLitters_lawful (ξ : NearLitterBehaviour) (hξ : ξ.Lawful) : + ξ.withLitters.Lawful := + sorry + +theorem withLitters_hasLitters (ξ : NearLitterBehaviour) (hξ : ξ.Lawful) : + ξ.withLitters.HasLitters := + sorry end NearLitterBehaviour