From 2f1c9643dda7e79ae16fe07927e603c8b88eb563 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Sun, 24 Nov 2024 18:17:32 +0000 Subject: [PATCH] Prove tSet_ext in matin induction Signed-off-by: zeramorphic --- ConNF/Construction/MainInduction.lean | 53 ++++++++++++++++++++++++++- ConNF/Construction/NewModelData.lean | 25 +++++++++++++ 2 files changed, 77 insertions(+), 1 deletion(-) diff --git a/ConNF/Construction/MainInduction.lean b/ConNF/Construction/MainInduction.lean index 8103a8a2ed..26a9f21e00 100644 --- a/ConNF/Construction/MainInduction.lean +++ b/ConNF/Construction/MainInduction.lean @@ -82,6 +82,8 @@ structure Hypothesis {α : Λ} (M : Motive α) (N : (β : Λ) → (β : TypeInde ∃ ρ : M.data.AllPerm, (∀ (β : Λ) (hβ : (β : TypeIndex) < α), allPermSderiv hβ ρ = ρs hβ) ∧ allPermBotSderiv ρ = π + tSet_ext (β : Λ) (hβ : (β : TypeIndex) < α) (x y : M.data.TSet) : + (∀ z : (N β hβ).data.TSet, z ∈[hβ] x ↔ z ∈[hβ] y) → x = y def castTSet {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β} (h₁ : α = β) (h₂ : HEq D₁ D₂) : @@ -95,6 +97,9 @@ def castTangle {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β} (h₁ : α = β) (h₂ : HEq D₁ D₂) : (letI := D₁; Tangle α) ≃ (letI := D₂; Tangle β) := by cases h₁; rw [eq_of_heq h₂] +theorem castTSet_forget {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : HEq D₁ D₂) (ρ : D₁.TSet) : + D₂.tSetForget (castTSet rfl h₂ ρ) = D₁.tSetForget ρ := by cases h₂; rfl + theorem castAllPerm_forget {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : HEq D₁ D₂) (ρ : D₁.AllPerm) : D₂.allPermForget (castAllPerm rfl h₂ ρ) = D₁.allPermForget ρ := by cases h₂; rfl @@ -217,6 +222,16 @@ def castTangleLeEq {β : Λ} (hβ : (β : TypeIndex) = α) : TangleLe M β hβ.le ≃ (letI := newModelData' M; Tangle α) := castTangle hβ (by cases hβ; exact heq_of_eq <| leData_data_eq M) +theorem castTSetLeLt_forget {β : Λ} (hβ : (β : TypeIndex) < α) (x : TSetLe M β hβ.le) : + (M β hβ).data.tSetForget (castTSetLeLt M hβ x) = + letI : Level := ⟨α⟩; letI : LeLevel β := ⟨hβ.le⟩; ((leData M).data β).tSetForget x := + castTSet_forget _ _ + +theorem castTSetLeEq_forget (x : TSetLe M α le_rfl) : + (newModelData' M).tSetForget (castTSetLeEq M rfl x) = + letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩; ((leData M).data α).tSetForget x := + castTSet_forget _ _ + theorem castAllPermLeLt_forget {β : Λ} (hβ : (β : TypeIndex) < α) (ρ : AllPermLe M β hβ.le) : (M β hβ).data.allPermForget (castAllPermLeLt M hβ ρ) = letI : Level := ⟨α⟩; letI : LeLevel β := ⟨hβ.le⟩; ((leData M).data β).allPermForget ρ := @@ -487,6 +502,41 @@ theorem preCoherentData_allPerm_of_smulFuzz rw [← castAllPermLeLt_forget M LtLevel.elim] at this exact this +theorem preCoherent_tSet_ext + (H : (β : Λ) → (h : (β : TypeIndex) < α) → Hypothesis (M β h) λ γ h' ↦ M γ (h'.trans h)) + {β γ : Λ} + [iβ : letI : Level := ⟨α⟩; LeLevel β] [iγ : letI : Level := ⟨α⟩; LeLevel γ] + (hγ : (γ : TypeIndex) < β) (x y : letI : Level := ⟨α⟩; TSetLe M β LeLevel.elim) + (hxy : letI : Level := ⟨α⟩; ∀ (z : TSetLe M γ LeLevel.elim), z ∈[hγ] x ↔ z ∈[hγ] y) : + x = y := by + letI : Level := ⟨α⟩ + by_cases h : (β : TypeIndex) = α + · cases coe_injective h + apply (castTSetLeEq M rfl).injective + letI : LtLevel γ := ⟨hγ⟩ + letI := ltData M + apply newModelData_ext γ + intro z + simp only [← TSet.forget_mem_forget] at hxy ⊢ + convert hxy ((castTSetLeLt M hγ).symm z) using 2 + · have := castTSetLeLt_forget M hγ ((castTSetLeLt M hγ).symm z) + rwa [Equiv.apply_symm_apply] at this + · exact castTSetLeEq_forget M x + · have := castTSetLeLt_forget M hγ ((castTSetLeLt M hγ).symm z) + rwa [Equiv.apply_symm_apply] at this + · exact castTSetLeEq_forget M y + · apply (castTSetLeLt M (LeLevel.elim.lt_of_ne h)).injective + apply (H β _).tSet_ext γ hγ + intro z + simp only [← TSet.forget_mem_forget] at hxy ⊢ + convert hxy ((castTSetLeLt M (hγ.trans_le LeLevel.elim)).symm z) using 2 + · have := castTSetLeLt_forget M (hγ.trans_le LeLevel.elim) ((castTSetLeLt M _).symm z) + rwa [Equiv.apply_symm_apply] at this + · exact castTSetLeLt_forget M _ x + · have := castTSetLeLt_forget M (hγ.trans_le LeLevel.elim) ((castTSetLeLt M _).symm z) + rwa [Equiv.apply_symm_apply] at this + · exact castTSetLeLt_forget M _ y + def coherentData : letI : Level := ⟨α⟩; CoherentData := letI : Level := ⟨α⟩ @@ -498,7 +548,7 @@ def coherentData : smul_fuzz := preCoherentData_smul_fuzz M H allPerm_of_basePerm := λ π ↦ ⟨π, rfl⟩ allPerm_of_smulFuzz := preCoherentData_allPerm_of_smulFuzz M H - tSet_ext := sorry + tSet_ext := preCoherent_tSet_ext M H typedMem_singleton_iff := sorry } @@ -536,6 +586,7 @@ def constructHypothesis (α : Λ) (M : (β : Λ) → (β : TypeIndex) < α → M pos_nearLitter_lt_pos := sorry smul_fuzz := sorry smul_fuzz_bot := sorry + allPerm_of_smul_fuzz := sorry } instance : IsTrans Λ λ β γ ↦ (β : TypeIndex) < (γ : TypeIndex) := diff --git a/ConNF/Construction/NewModelData.lean b/ConNF/Construction/NewModelData.lean index 0b063d0999..2a68b4d38f 100644 --- a/ConNF/Construction/NewModelData.lean +++ b/ConNF/Construction/NewModelData.lean @@ -403,6 +403,31 @@ def newSingleton {γ : Λ} [LtLevel γ] (x : TSet γ) : NewSet := local instance : ModelData α := newModelData +theorem not_mem_none {β : TypeIndex} [LtLevel β] (z : TSet β) : + ¬z ∈[LtLevel.elim] (show TSet α from none) := by + unfold TypedMem.typedMem instTypedMemTSet + change zᵁ ∉ _ + erw [Equiv.apply_symm_apply] + exact id + +theorem newModelData_ext (β : Λ) [LtLevel β] (x y : TSet α) + (h : ∀ z : TSet β, z ∈[LtLevel.elim] x ↔ z ∈[LtLevel.elim] y) : + x = y := by + obtain (_ | x) := x <;> obtain (_ | y) := y + · rfl + · obtain ⟨z, hz⟩ := Code.members_nonempty y.hc β + rw [NewSet.mem_members] at hz + cases not_mem_none z ((h z).mpr hz) + · obtain ⟨z, hz⟩ := Code.members_nonempty x.hc β + rw [NewSet.mem_members] at hz + cases not_mem_none z ((h z).mp hz) + · apply congr_arg some + apply NewSet.ext + apply Code.ext x.hc y.hc β + ext z + rw [NewSet.mem_members, NewSet.mem_members] + exact h z + def newPositionDeny (t : Tangle α) : Set μ := pos '' {N | t.set = some (newTyped N)} ∪ pos '' (t.supportᴬ.image Prod.snd : Set Atom) ∪