From 1301df7fe4230213adf2a819b0850424752324df Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Tue, 19 Nov 2024 20:49:01 +0000 Subject: [PATCH] Progress on coherent data Signed-off-by: zeramorphic --- ConNF/Construction/MainInduction.lean | 144 ++++++++++++++++++++++++-- ConNF/Construction/NewModelData.lean | 75 ++++++++++++-- ConNF/Counting/Conclusions.lean | 4 + ConNF/Setup/CoherentData.lean | 7 +- ConNF/Setup/ModelData.lean | 13 ++- 5 files changed, 221 insertions(+), 22 deletions(-) diff --git a/ConNF/Construction/MainInduction.lean b/ConNF/Construction/MainInduction.lean index 4e8944db2c..be37b18730 100644 --- a/ConNF/Construction/MainInduction.lean +++ b/ConNF/Construction/MainInduction.lean @@ -1,5 +1,6 @@ -import ConNF.Construction.NewModelData import ConNF.Basic.InductiveConstruction +import ConNF.Construction.NewModelData +import ConNF.Counting.Conclusions /-! # New file @@ -26,10 +27,13 @@ structure Motive (α : Λ) where typed : TypedNearLitters α structure Hypothesis (α : Λ) (M : Motive α) (N : (β : Λ) → β < α → Motive β) where + allPermSderiv {β : Λ} (h : β < α) : M.data.AllPerm → (N β h).data.AllPerm + allPermBotSderiv : M.data.AllPerm → botModelData.AllPerm + singleton {β : Λ} (h : β < α) : (N β h).data.TSet → M.data.TSet theorem card_tangle_bot_le [ModelData ⊥] : #(Tangle ⊥) ≤ #μ := by apply card_tangle_le_of_card_tSet - apply (mk_le_of_injective (tSetForget_injective' (α := ⊥))).trans + apply (mk_le_of_injective (ModelData.tSetForget_injective' (α := ⊥))).trans apply (mk_le_of_injective StrSet.botEquiv.injective).trans rw [card_atom] @@ -43,8 +47,7 @@ theorem pos_tangle_bot [ModelData ⊥] (t : Tangle ⊥) : pos (StrSet.botEquiv t.setᵁ) < pos t := funOfDeny_gt_deny _ _ _ _ _ rfl -def ltData - (α : Λ) (M : (β : Λ) → β < α → Motive β) : +def ltData (α : Λ) (M : (β : Λ) → β < α → Motive β) : letI : Level := ⟨α⟩; LtData := letI : Level := ⟨α⟩ letI data : (β : TypeIndex) → [LtLevel β] → ModelData β := @@ -57,15 +60,142 @@ def ltData λ β hβ ↦ (M β (WithBot.coe_lt_coe.mp hβ.elim)).typed LtData.mk (data := data) (positions := positions) (typedNearLitters := typedNearLitters) +def newModelData' (α : Λ) (M : (β : Λ) → β < α → Motive β) : + letI : Level := ⟨α⟩; ModelData α := + letI : Level := ⟨α⟩ + letI : LtData := ltData α M + newModelData + +def castData (α : Λ) (M : (β : Λ) → β < α → Motive β) + (β : TypeIndex) [letI : Level := ⟨α⟩; LeLevel β] : ModelData β := + if h : β = α then + cast (by simp_rw [h]) (newModelData' α M) + else + letI : Level := ⟨α⟩ + haveI : LtLevel β := ⟨LeLevel.elim.lt_of_ne h⟩ + (ltData α M).data β + +theorem castData_eq_of_eq (α : Λ) (M : (β : Λ) → β < α → Motive β) : + letI : Level := ⟨α⟩ + letI : LeLevel α := ⟨le_rfl⟩ + castData α M α = newModelData' α M := by + letI : Level := ⟨α⟩ + rw [castData, dif_pos rfl] + rfl + +theorem castData_eq_of_lt (α : Λ) (M : (β : Λ) → β < α → Motive β) + (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] : + letI : Level := ⟨α⟩ + castData α M β = (ltData α M).data β := by + letI : Level := ⟨α⟩ + rw [castData, dif_neg] + rintro rfl + exact LtLevel.elim.ne rfl + +def liftCastDataLt (α : Λ) (M : (β : Λ) → β < α → Motive β) + {D : (β : TypeIndex) → ModelData β → Type _} + (f : letI : Level := ⟨α⟩; (β : TypeIndex) → [LtLevel β] → D β ((ltData α M).data β)) + (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] : D β (castData α M β) := + cast (by rw [castData_eq_of_lt]) (f β) + +def liftCastDataLe (α : Λ) (M : (β : Λ) → β < α → Motive β) + {D : (β : TypeIndex) → ModelData β → Type _} (β : TypeIndex) + (fβ : letI : Level := ⟨α⟩; [LtLevel β] → D β ((ltData α M).data β)) + (fα : D α (newModelData' α M)) + [letI : Level := ⟨α⟩; LeLevel β] : D β (castData α M β) := + if h : β = α then + cast (by cases h; rw [castData_eq_of_eq]) fα + else + letI : Level := ⟨α⟩ + haveI : LtLevel β := ⟨LeLevel.elim.lt_of_ne h⟩ + cast (by rw [castData_eq_of_lt]) (fβ) + +def leData (α : Λ) (M : (β : Λ) → β < α → Motive β) : + letI : Level := ⟨α⟩; LeData := + letI : Level := ⟨α⟩ + letI data : (β : TypeIndex) → [LeLevel β] → ModelData β := castData α M + letI positions : (β : TypeIndex) → [LtLevel β] → Position (Tangle β) := + liftCastDataLt α M + (D := λ β (x : ModelData β) ↦ Position (@Tangle _ β x)) (ltData α M).positions + LeData.mk (data := data) (positions := positions) + +def preCoherentData (α : Λ) (M : (β : Λ) → β < α → Motive β) + (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) : + letI : Level := ⟨α⟩; PreCoherentData := + letI : Level := ⟨α⟩ + letI := leData α M + { + allPermSderiv := λ {β γ} _ _ hγ ρ ↦ + -- Case split on `γ = α`. + liftCastDataLe α M (D := λ γ Mγ ↦ γ < β → Mγ.AllPerm) γ + -- Case split on `β = α`. + (λ hγ ↦ liftCastDataLe α M + (D := λ _β Mβ ↦ Mβ.AllPerm → ((ltData α M).data γ).AllPerm) β + ( -- Case split on `β = ⊥`. + β.recBotCoe (C := λ β ↦ [LtLevel β] → γ < β → + ((ltData α M).data β).AllPerm → ((ltData α M).data γ).AllPerm) + (λ h ↦ (not_lt_bot h).elim) + (λ β _ ↦ -- Case split on `γ = ⊥`. + γ.recBotCoe (C := λ γ ↦ [LtLevel γ] → γ < β → + ((ltData α M).data β).AllPerm → ((ltData α M).data γ).AllPerm) + (λ _ ↦ (H β (WithBot.coe_lt_coe.mp LtLevel.elim)).allPermBotSderiv) + (λ _γ _ hγ ↦ (H β (WithBot.coe_lt_coe.mp LtLevel.elim)).allPermSderiv + (WithBot.coe_lt_coe.mp hγ))) + hγ) + (λ ρ ↦ letI : LtData := ltData α M; ρ.sderiv γ) + ρ) + (λ h' ↦ (LeLevel.elim.not_lt h').elim) hγ + singleton := λ {β γ} _ _ hγ x ↦ + -- Case split on `γ = α`. + liftCastDataLe α M (D := λ γ Mγ ↦ γ < β → Mγ.TSet → TSet β) γ + (λ _hγ ↦ + -- Case split on `β = α`. + liftCastDataLe α M + (D := λ _β Mβ ↦ ((ltData α M).data γ).TSet → Mβ.TSet) β + ((H β (WithBot.coe_lt_coe.mp LtLevel.elim)).singleton (WithBot.coe_lt_coe.mp hγ)) + (λ x ↦ letI : LtData := ltData α M; some (newSingleton x))) + (λ h' ↦ (LeLevel.elim.not_lt h').elim) hγ x + } + +def coherentData + (α : Λ) (M : (β : Λ) → β < α → Motive β) + (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) : + letI : Level := ⟨α⟩; CoherentData := + letI : Level := ⟨α⟩ + letI := preCoherentData α M H + ⟨sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry⟩ + +theorem construct_tangle_le_μ' (α : Λ) (M : (β : Λ) → β < α → Motive β) + (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) : + letI : Level := ⟨α⟩ + letI : LeLevel α := ⟨le_rfl⟩ + letI := coherentData α M H + #(Tangle α) ≤ #μ := + letI : Level := ⟨α⟩ + letI : LeLevel α := ⟨le_rfl⟩ + letI := coherentData α M H + card_tangle_le α + +theorem construct_tangle_le_μ (α : Λ) (M : (β : Λ) → β < α → Motive β) + (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) : + letI := newModelData' α M + #(Tangle α) ≤ #μ := + sorry + def constructMotive (α : Λ) (M : (β : Λ) → β < α → Motive β) - (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) fun γ h' ↦ M γ (h'.trans h)) : + (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) : Motive α := letI : Level := ⟨α⟩ letI : LtData := ltData α M - ⟨newModelData, sorry, sorry⟩ + letI := newModelData + { + data := newModelData, + pos := newPosition (construct_tangle_le_μ α M H), + typed := newTypedNearLitters (construct_tangle_le_μ α M H) + } def constructHypothesis (α : Λ) (M : (β : Λ) → β < α → Motive β) - (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) fun γ h' ↦ M γ (h'.trans h)) : + (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) : Hypothesis α (constructMotive α M H) M := sorry diff --git a/ConNF/Construction/NewModelData.lean b/ConNF/Construction/NewModelData.lean index 9037f173d4..c0c767d229 100644 --- a/ConNF/Construction/NewModelData.lean +++ b/ConNF/Construction/NewModelData.lean @@ -264,6 +264,30 @@ def newPreModelData : PreModelData α where tSetForget x := x.elim (StrSet.coeEquiv.symm λ _ _ ↦ ∅) (·ᵁ) allPermForget := (·ᵁ) +@[simp] +theorem newPreModelData.tSetForget_none : + newPreModelData.tSetForget none = (StrSet.coeEquiv.symm λ _ _ ↦ ∅) := + rfl + +@[simp] +theorem newPreModelData.tSetForget_some (x : NewSet) : + newPreModelData.tSetForget (some x) = xᵁ := + rfl + +@[simp] +theorem newPreModelData.tSetForget_none' : + (show @TSet _ α newPreModelData from none)ᵁ = (StrSet.coeEquiv.symm λ _ _ ↦ ∅) := + rfl + +@[simp] +theorem newPreModelData.tSetForget_some' (x : NewSet) : + (show @TSet _ α newPreModelData from some x)ᵁ = xᵁ := + rfl + +theorem StrSet.smul_none (π : StrPerm α) : + π • (StrSet.coeEquiv.symm λ _ _ ↦ ∅ : StrSet α) = StrSet.coeEquiv.symm λ _ _ ↦ ∅ := by + sorry + theorem NewPerm.forget_injective (ρ₁ ρ₂ : NewPerm) (h : ρ₁ᵁ = ρ₂ᵁ) : ρ₁ = ρ₂ := by ext β hβ : 3 apply allPermForget_injective @@ -299,18 +323,38 @@ theorem NewSet.exists_support (x : letI := newPreModelData; TSet α) : letI := newPreModelData ∃ S : Support α, S.Supports x := by letI := newPreModelData - obtain ⟨S, hS⟩ := x.hS - refine ⟨S, ?_, λ h ↦ (WithBot.bot_ne_coe.symm h).elim⟩ - intro ρ hρ - apply NewSet.ext - exact hS ρ hρ + obtain (_ | x) := x + · use ⟨.empty, .empty⟩ + constructor + · intros + rfl + · rintro ⟨⟩ + · obtain ⟨S, hS⟩ := x.hS + refine ⟨S, ?_, λ h ↦ (WithBot.bot_ne_coe.symm h).elim⟩ + intro ρ hρ + apply congr_arg some + apply NewSet.ext + exact hS ρ hρ + +theorem NewSet.coe_ne_empty (x : NewSet) : xᵁ ≠ (StrSet.coeEquiv.symm λ _ _ ↦ ∅) := by + sorry def newModelData : ModelData α where - tSetForget_injective' := NewSet.forget_injective + tSetForget_injective' := by + rintro (_ | x) (_ | y) h + · rfl + · cases NewSet.coe_ne_empty y h.symm + · cases NewSet.coe_ne_empty x h + · rw [NewSet.forget_injective x y h] + tSetForget_surjective_of_bot' := by rintro ⟨⟩ allPermForget_injective' := NewPerm.forget_injective allPermForget_one := NewPerm.forget_one allPermForget_mul := NewPerm.forget_mul - smul_forget := NewPerm.smul_forget + smul_forget := by + rintro ρ (_ | x) + · rw [newPreModelData.tSetForget_none', StrSet.smul_none] + rfl + · exact NewPerm.smul_forget ρ x exists_support := NewSet.exists_support __ := newPreModelData @@ -342,9 +386,14 @@ def NearLitter.code (N : NearLitter) : Code := have : #Nᴬ ≠ 0 := sorry rw [Cardinal.mk_ne_zero_iff_nonempty] at this obtain ⟨a, ha⟩ := this - ⟩ + obtain ⟨x, hx⟩ := tSetForget_surjective (StrSet.botEquiv.symm a) + use x + rwa [Set.mem_setOf_eq, hx, Equiv.apply_symm_apply]⟩ def newTyped (N : NearLitter) : NewSet := + N.code.toSet sorry + +def newSingleton {γ : Λ} [LtLevel γ] (x : TSet γ) : NewSet := sorry local instance : ModelData α := newModelData @@ -360,4 +409,14 @@ theorem card_newPositionDeny (t : Tangle α) : def newPosition (h : #(Tangle α) ≤ #μ) : Position (Tangle α) where pos := ⟨funOfDeny h newPositionDeny card_newPositionDeny, funOfDeny_injective _ _ _⟩ +def newTypedNearLitters (h : #(Tangle α) ≤ #μ) : + letI := newPosition h; TypedNearLitters α := + letI := newPosition h + { + typed := some ∘ newTyped + typed_injective := sorry + pos_le_pos_of_typed := sorry + smul_typed := sorry + } + end ConNF diff --git a/ConNF/Counting/Conclusions.lean b/ConNF/Counting/Conclusions.lean index 482017832e..f271727ac9 100644 --- a/ConNF/Counting/Conclusions.lean +++ b/ConNF/Counting/Conclusions.lean @@ -78,4 +78,8 @@ theorem card_tSet_le (β : TypeIndex) [LeLevel β] : apply mul_le_of_le μ_isStrongLimit.aleph0_le (card_codingFunction β).le rw [card_support] +theorem card_tangle_le (β : TypeIndex) [LeLevel β] : + #(Tangle β) ≤ #μ := + card_tangle_le_of_card_tSet (card_tSet_le β) + end ConNF diff --git a/ConNF/Setup/CoherentData.lean b/ConNF/Setup/CoherentData.lean index c25775fb20..c78c53563d 100644 --- a/ConNF/Setup/CoherentData.lean +++ b/ConNF/Setup/CoherentData.lean @@ -39,7 +39,7 @@ instance [LeData] : (β : TypeIndex) → [LtLevel β] → Position (Tangle β) : class PreCoherentData extends LeData where allPermSderiv {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : AllPerm β → AllPerm γ - singleton {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : TSet γ → TSet β + singleton {β γ : Λ} [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) : TSet γ → TSet β export PreCoherentData (singleton) @@ -92,8 +92,9 @@ class CoherentData extends PreCoherentData where (ρs hε)ᵁ ↘. • fuzz hδε t = fuzz hδε (ρs hδ • t)) : ∃ ρ : AllPerm γ, ∀ δ : TypeIndex, [LtLevel δ] → ∀ hδ : δ < γ, ρ ↘ hδ = ρs hδ tSet_ext {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : (γ : TypeIndex) < β) (x y : TSet β) - (h : ∀ z : TSet γ, z ∈[hγ] x ↔ z ∈[hγ] y) : x = y - typedMem_singleton_iff {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (hγ : γ < β) (x y : TSet γ) : + (h : ∀ z : TSet γ, z ∈[hγ] x ↔ z ∈[hγ] y) : x = y + typedMem_singleton_iff {β γ : Λ} [LeLevel β] [LeLevel γ] + (hγ : (γ : TypeIndex) < β) (x y : TSet γ) : y ∈[hγ] singleton hγ x ↔ y = x export CoherentData (allPermSderiv_forget pos_atom_lt_pos pos_nearLitter_lt_pos smul_fuzz diff --git a/ConNF/Setup/ModelData.lean b/ConNF/Setup/ModelData.lean index 55da9ca6c8..11cd8bb042 100644 --- a/ConNF/Setup/ModelData.lean +++ b/ConNF/Setup/ModelData.lean @@ -61,24 +61,28 @@ theorem Support.Supports.mono {X : Type _} {α : TypeIndex} [PreModelData α] class ModelData (α : TypeIndex) extends PreModelData α where tSetForget_injective' : Function.Injective tSetForget + tSetForget_surjective_of_bot' : α = ⊥ → Function.Surjective tSetForget allPermForget_injective' : Function.Injective allPermForget allPermForget_one : (1 : AllPerm)ᵁ = 1 allPermForget_mul (ρ₁ ρ₂ : AllPerm) : (ρ₁ * ρ₂)ᵁ = ρ₁ᵁ * ρ₂ᵁ smul_forget (ρ : AllPerm) (x : TSet) : (ρ • x)ᵁ = ρᵁ • xᵁ exists_support (x : TSet) : ∃ S : Support α, S.Supports x -export ModelData (tSetForget_injective' allPermForget_injective' allPermForget_one allPermForget_mul - smul_forget exists_support) +export ModelData (allPermForget_one allPermForget_mul smul_forget exists_support) attribute [simp] allPermForget_one allPermForget_mul smul_forget theorem tSetForget_injective {α : TypeIndex} [ModelData α] {x₁ x₂ : TSet α} (h : x₁ᵁ = x₂ᵁ) : x₁ = x₂ := - tSetForget_injective' h + ModelData.tSetForget_injective' h + +theorem tSetForget_surjective [ModelData ⊥] (x : StrSet ⊥) : + ∃ y : TSet ⊥, yᵁ = x := + ModelData.tSetForget_surjective_of_bot' rfl x theorem allPermForget_injective {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α} (h : ρ₁ᵁ = ρ₂ᵁ) : ρ₁ = ρ₂ := - allPermForget_injective' h + ModelData.allPermForget_injective' h @[simp] theorem allPermForget_inv {α : TypeIndex} [ModelData α] (ρ : AllPerm α) : ρ⁻¹ᵁ = ρᵁ⁻¹ := by @@ -243,6 +247,7 @@ def botPreModelData : PreModelData ⊥ where def botModelData : ModelData ⊥ where tSetForget_injective' := Equiv.injective _ + tSetForget_surjective_of_bot' _ := Equiv.surjective _ allPermForget_injective' _ _ h := congr_fun h Path.nil allPermForget_one := rfl allPermForget_mul _ _ := rfl