From 251ac752f844dfde539ac2bd3ff112305ad59139 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Sat, 30 Nov 2024 13:31:57 +0000 Subject: [PATCH] Prove raise_strong' Signed-off-by: zeramorphic --- ConNF/Construction/RaiseStrong.lean | 103 ++++++++++++++++------------ ConNF/Counting/Recode.lean | 2 +- ConNF/Counting/Strong.lean | 13 ++++ ConNF/Setup/Path.lean | 5 ++ ConNF/Setup/Support.lean | 42 +++++++----- 5 files changed, 105 insertions(+), 60 deletions(-) diff --git a/ConNF/Construction/RaiseStrong.lean b/ConNF/Construction/RaiseStrong.lean index 0db14c8c35..c53c5f15ee 100644 --- a/ConNF/Construction/RaiseStrong.lean +++ b/ConNF/Construction/RaiseStrong.lean @@ -21,7 +21,7 @@ variable [Params.{u}] {β γ : Λ} {hγ : (γ : TypeIndex) < β} namespace Support -theorem not_mem_strongbotDeriv (S : Support γ) (N : NearLitter) : +theorem not_mem_scoderiv_botDeriv (S : Support γ) (N : NearLitter) : N ∉ (S ↗ hγ ⇘. (Path.nil ↘.))ᴺ := by rintro ⟨i, ⟨A, N'⟩, h₁, h₂⟩ simp only [Prod.mk.injEq] at h₂ @@ -41,11 +41,11 @@ theorem not_mem_strong_botDeriv (S : Support γ) (N : NearLitter) : rintro h rw [strong, close_nearLitters, preStrong_nearLitters, Enumeration.mem_add_iff] at h obtain h | h := h - · exact not_mem_strongbotDeriv S N h + · exact not_mem_scoderiv_botDeriv S N h · rw [mem_constrainsNearLitters_nearLitters] at h obtain ⟨B, N', hN', h⟩ := h cases h using Relation.ReflTransGen.head_induction_on - case refl => exact not_mem_strongbotDeriv S N hN' + case refl => exact not_mem_scoderiv_botDeriv S N hN' case head x hx₁ hx₂ _ => obtain ⟨⟨γ, δ, ε, hδ, hε, hδε, A⟩, t, B, hB, hN, ht⟩ := hx₂ simp only at hB @@ -64,47 +64,64 @@ theorem not_mem_strong_botDeriv (S : Support γ) (N : NearLitter) : case nil => cases hB case sderiv ζ B hζ _ _ => cases hB -theorem raise_preStrong (S : Support γ) (hγ : (γ : TypeIndex) < β) : - ((S ↗ hγ).strong ↗ LtLevel.elim).PreStrong := by - constructor - rintro A N hN ⟨γ, δ, ε, hδ, hε, hδε, A⟩ t rfl ht - dsimp only at hN ⊢ - obtain ⟨i, hi⟩ := hN - rw [← derivBot_nearLitters, ← scoderiv_nearLitters, - Enumeration.derivBot_rel, Enumeration.scoderiv_rel] at hi - obtain ⟨B, hB₁, hB₂⟩ := hi - change A ↘ _ ↘ _ = _ at hB₁ - cases B - case sderiv ζ B hζ' _ => - rw [← Path.coderiv_deriv] at hB₁ - cases Path.sderiv_index_injective hB₁ - rw [Path.sderiv_left_inj] at hB₁ - cases B - case nil => - cases A - case nil => - cases hB₁ - cases not_mem_strong_botDeriv S N ⟨i, hB₂⟩ - case sderiv ζ A hζ _ _ => cases hB₁ - case sderiv ζ B hζ _ _ => - rw [← Path.coderiv_deriv] at hB₁ - cases Path.sderiv_index_injective hB₁ - rw [Path.sderiv_left_inj] at hB₁ - cases hB₁ - simp only [Path.botSderiv_coe_eq] at hB₂ - rw [Path.coderiv_deriv, scoderiv_deriv_eq] - exact (S ↗ hγ).strong_strong.support_le ⟨i, hB₂⟩ ⟨γ, δ, ε, hδ, hε, hδε, B⟩ t rfl ht - -theorem raise_strong (S : Support γ) (hγ : (γ : TypeIndex) < β) : - ((S ↗ hγ).strong ↗ LtLevel.elim).Strong := - ⟨S.raise_preStrong hγ, (S ↗ hγ).strong_strong.scoderiv LtLevel.elim⟩ - theorem raise_preStrong' (S : Support α) (hS : S.Strong) (T : Support γ) (ρ : AllPerm β) - (hγ : (γ : TypeIndex) < β) - (hρ : ρᵁ • (S ↘ LtLevel.elim : Support β) = S ↘ LtLevel.elim) : + (hγ : (γ : TypeIndex) < β) : (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ LtLevel.elim + (T ↗ hγ).strong).interferenceSupport)) ↗ LtLevel.elim).PreStrong := by - sorry + apply hS.toPreStrong.add + constructor + intro A N hN P t hA ht + obtain ⟨A, rfl⟩ := eq_of_nearLitter_mem_scoderiv_botDeriv hN + simp only [scoderiv_botDeriv_eq, add_derivBot, smul_derivBot, + BaseSupport.add_nearLitters, BaseSupport.smul_nearLitters, interferenceSupport_nearLitters, + Enumeration.mem_add_iff, Enumeration.mem_smul, Enumeration.not_mem_empty, or_false] at hN + obtain ⟨δ, ε, ζ, hε, hζ, hεζ, B⟩ := P + dsimp only at * + cases A + case sderiv ζ' A hζ' _ => + rw [← Path.coderiv_deriv] at hA + cases Path.sderiv_index_injective hA + apply Path.sderiv_left_inj.mp at hA + cases A + case nil => + cases hA + cases not_mem_strong_botDeriv T _ hN + case sderiv ι A hι _ _ => + rw [← Path.coderiv_deriv] at hA + cases Path.sderiv_index_injective hA + cases hA + haveI : LtLevel δ := ⟨A.le.trans_lt LtLevel.elim⟩ + haveI : LtLevel ε := ⟨hε.trans LtLevel.elim⟩ + haveI : LtLevel ζ := ⟨hζ.trans LtLevel.elim⟩ + have := (T ↗ hγ).strong_strong.support_le hN ⟨δ, ε, ζ, hε, hζ, hεζ, A⟩ + (ρ⁻¹ ⇘ A ↘ hε • t) rfl ?_ + · simp only [Tangle.smul_support, allPermSderiv_forget, allPermDeriv_forget, + allPermForget_inv, Tree.inv_deriv, Tree.inv_sderiv] at this + have := smul_le_smul this (ρᵁ ⇘ A ↘ hε) + simp only [smul_inv_smul] at this + apply le_trans this + intro B + constructor + · intro a ha + simp only [smul_derivBot, Tree.sderiv_apply, Tree.deriv_apply, Path.deriv_scoderiv, + deriv_derivBot, Enumeration.mem_smul] at ha + rw [deriv_derivBot, ← Path.deriv_scoderiv, Path.coderiv_deriv', scoderiv_botDeriv_eq,] + simp only [Path.deriv_scoderiv, add_derivBot, smul_derivBot, + BaseSupport.add_atoms, BaseSupport.smul_atoms, Enumeration.mem_add_iff, + Enumeration.mem_smul] + exact Or.inl ha + · intro N hN + simp only [smul_derivBot, Tree.sderiv_apply, Tree.deriv_apply, Path.deriv_scoderiv, + deriv_derivBot, Enumeration.mem_smul] at hN + rw [deriv_derivBot, ← Path.deriv_scoderiv, Path.coderiv_deriv', scoderiv_botDeriv_eq,] + simp only [Path.deriv_scoderiv, add_derivBot, smul_derivBot, + BaseSupport.add_nearLitters, BaseSupport.smul_nearLitters, Enumeration.mem_add_iff, + Enumeration.mem_smul] + exact Or.inl hN + · rw [← smul_fuzz hε hζ hεζ, ← ht] + simp only [Path.botSderiv_coe_eq, BasePerm.smul_nearLitter_litter, allPermDeriv_forget, + allPermForget_inv, Tree.inv_deriv, Tree.inv_sderiv, Tree.inv_sderivBot] + rfl theorem raise_closed' (S : Support α) (hS : S.Strong) (T : Support γ) (ρ : AllPerm β) (hγ : (γ : TypeIndex) < β) @@ -158,8 +175,8 @@ theorem raise_strong' (S : Support α) (hS : S.Strong) (T : Support γ) (ρ : Al (hγ : (γ : TypeIndex) < β) (hρ : ρᵁ • (S ↘ LtLevel.elim : Support β) = S ↘ LtLevel.elim) : (S + (ρᵁ • ((T ↗ hγ).strong + - (S ↘ LtLevel.elim + (T ↗ hγ).strong).interferenceSupport)) ↗ LtLevel.elim).Strong := by - sorry + (S ↘ LtLevel.elim + (T ↗ hγ).strong).interferenceSupport)) ↗ LtLevel.elim).Strong := + ⟨raise_preStrong' S hS T ρ hγ, raise_closed' S hS T ρ hγ hρ⟩ theorem convAtoms_injective_of_fixes {S : Support α} (hS : S.Strong) {T : Support γ} {ρ₁ ρ₂ : AllPerm β} {hγ : (γ : TypeIndex) < β} diff --git a/ConNF/Counting/Recode.lean b/ConNF/Counting/Recode.lean index 42b264a9e5..f497789dac 100644 --- a/ConNF/Counting/Recode.lean +++ b/ConNF/Counting/Recode.lean @@ -128,7 +128,7 @@ theorem scoderiv_supports_singleton (S : Support γ) (y : TSet γ) (h : S.Suppor theorem raisedSingleton_supports (S : Support β) (y : TSet γ) : (S + designatedSupport y ↗ hγ).Supports (singleton hγ y) := by have := scoderiv_supports_singleton hγ (designatedSupport y) y (designatedSupport_supports y) - apply this.mono le_add_left + apply this.mono Support.le_add_left rintro ⟨⟩ def raisedSingleton (S : Support β) (y : TSet γ) : CodingFunction β := diff --git a/ConNF/Counting/Strong.lean b/ConNF/Counting/Strong.lean index b63e201805..55a06aebc5 100644 --- a/ConNF/Counting/Strong.lean +++ b/ConNF/Counting/Strong.lean @@ -70,6 +70,19 @@ theorem Closed.smul {S : Support β} (hS : S.Closed) (ρ : AllPerm β) : (ρᵁ theorem Strong.smul {S : Support β} (hS : S.Strong) (ρ : AllPerm β) : (ρᵁ • S).Strong := ⟨hS.toPreStrong.smul ρ, hS.toClosed.smul ρ⟩ +theorem PreStrong.add {S T : Support β} (hS : S.PreStrong) (hT : T.PreStrong) : + (S + T).PreStrong := by + constructor + intro A N hN P t hA ht + simp only [add_derivBot, BaseSupport.add_nearLitters, Enumeration.mem_add_iff] at hN + obtain hN | hN := hN + · intro B + simp only [deriv_derivBot, add_derivBot] + exact (hS.support_le hN P t hA ht B).trans (BaseSupport.le_add_right) + · intro B + simp only [deriv_derivBot, add_derivBot] + exact (hT.support_le hN P t hA ht B).trans (BaseSupport.le_add_left) + omit [Level] [CoherentData] [LeLevel β] in theorem Closed.scoderiv {γ : TypeIndex} {S : Support γ} (hS : S.Closed) (hγ : γ < β) : (S ↗ hγ).Closed := by diff --git a/ConNF/Setup/Path.lean b/ConNF/Setup/Path.lean index 733d471561..e1c18fc21a 100644 --- a/ConNF/Setup/Path.lean +++ b/ConNF/Setup/Path.lean @@ -250,6 +250,11 @@ theorem Path.deriv_scoderiv (A : α ↝ β) (B : γ ↝ δ) (h : γ < β) : rw [deriv_sderiv, ← ih] rfl +@[simp] +theorem Path.botDeriv_scoderiv (A : α ↝ β) (B : γ ↝ ⊥) (h : γ < β) : + A ⇘. (B ↗ h) = A ↘ h ⇘. B := + deriv_scoderiv A B h + theorem Path.coderiv_eq_deriv (A : α ↝ β) (B : β ↝ γ) : B ⇗ A = A ⇘ B := rfl diff --git a/ConNF/Setup/Support.lean b/ConNF/Setup/Support.lean index e0ed4db8a6..ea3060219a 100644 --- a/ConNF/Setup/Support.lean +++ b/ConNF/Setup/Support.lean @@ -475,6 +475,26 @@ theorem BaseSupport.smul_le_smul {S T : BaseSupport} (h : S ≤ T) (π : BasePer · intro N exact h.2 (π⁻¹ • N) +theorem BaseSupport.le_add_right {S T : BaseSupport} : + S ≤ S + T := by + constructor + · intro a ha + simp only [Support.add_derivBot, BaseSupport.add_atoms, Enumeration.mem_add_iff] + exact Or.inl ha + · intro N hN + simp only [Support.add_derivBot, BaseSupport.add_nearLitters, Enumeration.mem_add_iff] + exact Or.inl hN + +theorem BaseSupport.le_add_left {S T : BaseSupport} : + S ≤ T + S := by + constructor + · intro a ha + simp only [add_atoms, Enumeration.mem_add_iff] + exact Or.inr ha + · intro N hN + simp only [add_nearLitters, Enumeration.mem_add_iff] + exact Or.inr hN + def BaseSupport.Subsupport (S T : BaseSupport) : Prop := Sᴬ.rel ≤ Tᴬ.rel ∧ Sᴺ.rel ≤ Tᴺ.rel @@ -510,27 +530,17 @@ theorem Support.smul_le_smul {α : TypeIndex} {S T : Support α} (h : S ≤ T) ( π • S ≤ π • T := λ A ↦ BaseSupport.smul_le_smul (h A) (π A) -theorem le_add_right {α : TypeIndex} {S T : Support α} : +theorem Support.le_add_right {α : TypeIndex} {S T : Support α} : S ≤ S + T := by intro A - constructor - · intro a ha - simp only [Support.add_derivBot, BaseSupport.add_atoms, Enumeration.mem_add_iff] - exact Or.inl ha - · intro N hN - simp only [Support.add_derivBot, BaseSupport.add_nearLitters, Enumeration.mem_add_iff] - exact Or.inl hN + rw [add_derivBot] + exact BaseSupport.le_add_right -theorem le_add_left {α : TypeIndex} {S T : Support α} : +theorem Support.le_add_left {α : TypeIndex} {S T : Support α} : S ≤ T + S := by intro A - constructor - · intro a ha - simp only [Support.add_derivBot, BaseSupport.add_atoms, Enumeration.mem_add_iff] - exact Or.inr ha - · intro N hN - simp only [Support.add_derivBot, BaseSupport.add_nearLitters, Enumeration.mem_add_iff] - exact Or.inr hN + rw [add_derivBot] + exact BaseSupport.le_add_left def Support.Subsupport {α : TypeIndex} (S T : Support α) : Prop := ∀ A, (S ⇘. A).Subsupport (T ⇘. A)