From 92d80d2c5bd6be1eb869c4a2491dac586e8dc214 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Fri, 15 Dec 2023 12:14:39 +0000 Subject: [PATCH] Addition of supports Signed-off-by: zeramorphic --- ConNF/BaseType/Params.lean | 46 ++++++++++++++++--- ConNF/Structural/Support.lean | 85 ++++++++++++++++++++++++++++++----- 2 files changed, 114 insertions(+), 17 deletions(-) diff --git a/ConNF/BaseType/Params.lean b/ConNF/BaseType/Params.lean index bc1d0a18b2..6017f1009c 100644 --- a/ConNF/BaseType/Params.lean +++ b/ConNF/BaseType/Params.lean @@ -56,8 +56,11 @@ class Params where κ_isRegular : (#κ).IsRegular [κ_succ : SuccOrder κ] [κ_addMonoid : AddMonoid κ] - κ_typein (i j : κ) : Ordinal.typein (· < ·) (i + j : κ) = + [κ_sub : Sub κ] + κ_add_typein (i j : κ) : Ordinal.typein (· < ·) (i + j : κ) = Ordinal.typein (· < ·) i + Ordinal.typein (· < ·) j + κ_sub_typein (i j : κ) : Ordinal.typein (· < ·) (i - j : κ) = + Ordinal.typein (· < ·) i - Ordinal.typein (· < ·) j Λ_lt_κ : #Λ < #κ /-- A large type used in indexing the litters. @@ -198,6 +201,12 @@ noncomputable def addMonoid_of_type_eq_ord {α : Type _} simp only [Ordinal.typein_enum, Ordinal.enum_inj, add_assoc] __ := addZeroClass_of_type_eq_ord h +noncomputable def sub_of_isWellOrder {α : Type _} + [LinearOrder α] [IsWellOrder α (· < ·)] : Sub α where + sub x y := Ordinal.enum (· < ·) + (Ordinal.typein (· < ·) x - Ordinal.typein (· < ·) y) + ((Ordinal.sub_le_self _ _).trans_lt (Ordinal.typein_lt_type _ _)) + noncomputable example : Params.{0} where Λ := ℕ Λ_zero_le := zero_le @@ -217,7 +226,9 @@ noncomputable example : Params.{0} where let _ : Infinite (aleph 1).ord.out.α := by simp only [Cardinal.infinite_iff, mk_ordinal_out, card_ord, aleph0_le_aleph] addMonoid_of_type_eq_ord (by simp) - κ_typein i j := Ordinal.typein_enum _ _ + κ_sub := sub_of_isWellOrder + κ_add_typein i j := Ordinal.typein_enum _ _ + κ_sub_typein i j := Ordinal.typein_enum _ _ Λ_lt_κ := by rw [mk_denumerable, mk_ordinal_out, card_ord] exact aleph0_lt_aleph_one @@ -258,6 +269,7 @@ instance : LinearOrder κ := Params.κ_linearOrder instance : IsWellOrder κ (· < ·) := Params.κ_isWellOrder instance : SuccOrder κ := Params.κ_succ instance : AddMonoid κ := Params.κ_addMonoid +instance : Sub κ := Params.κ_sub instance : Inhabited κ := ⟨0⟩ instance : Infinite κ := Cardinal.infinite_iff.mpr Params.κ_isRegular.aleph0_le instance : NoMaxOrder κ := by @@ -284,20 +296,27 @@ instance : CovariantClass κ κ (· + ·) (· ≤ ·) := by constructor intro i j k h rw [← not_lt, ← Ordinal.typein_le_typein (· < ·)] at h ⊢ - rw [Params.κ_typein, Params.κ_typein] + rw [Params.κ_add_typein, Params.κ_add_typein] exact add_le_add_left h _ instance : CovariantClass κ κ (Function.swap (· + ·)) (· ≤ ·) := by constructor intro i j k h rw [← not_lt, ← Ordinal.typein_le_typein (· < ·)] at h ⊢ - rw [Params.κ_typein, Params.κ_typein] + rw [Params.κ_add_typein, Params.κ_add_typein] exact add_le_add_right h _ +instance : ContravariantClass κ κ (· + ·) (· ≤ ·) := by + constructor + intro i j k h + rw [← not_lt, ← Ordinal.typein_le_typein (· < ·)] at h ⊢ + rw [Params.κ_add_typein, Params.κ_add_typein, add_le_add_iff_left] at h + exact h + @[simp] theorem κ_typein_zero : Ordinal.typein ((· < ·) : κ → κ → Prop) 0 = 0 := by have := add_zero (0 : κ) - rw [← Ordinal.typein_inj (· < ·), Params.κ_typein] at this + rw [← Ordinal.typein_inj (· < ·), Params.κ_add_typein] at this conv at this => rhs; rw [← add_zero (Ordinal.typein _ _)] rw [Ordinal.add_left_cancel] at this exact this @@ -309,7 +328,7 @@ theorem κ_le_zero_iff (i : κ) : i ≤ 0 ↔ i = 0 := @[simp] theorem κ_add_eq_zero_iff (i j : κ) : i + j = 0 ↔ i = 0 ∧ j = 0 := by rw [← Ordinal.typein_inj (α := κ) (· < ·), ← Ordinal.typein_inj (α := κ) (· < ·), - ← Ordinal.typein_inj (α := κ) (· < ·), Params.κ_typein, κ_typein_zero, Ordinal.add_eq_zero_iff] + ← Ordinal.typein_inj (α := κ) (· < ·), Params.κ_add_typein, κ_typein_zero, Ordinal.add_eq_zero_iff] @[simp] theorem κ_succ_typein (i : κ) : @@ -342,6 +361,21 @@ theorem κ_lt_one_iff (i : κ) : i < 1 ↔ i = 0 := by · rintro rfl exact κ_zero_lt_one +theorem κ_le_self_add (i j : κ) : i ≤ i + j := by + rw [← not_lt, ← Ordinal.typein_le_typein (· < ·), Params.κ_add_typein] + exact Ordinal.le_add_right _ _ + +theorem κ_add_sub_cancel (i j : κ) : i + j - i = j := by + rw [← Ordinal.typein_inj (· < ·), Params.κ_sub_typein, Params.κ_add_typein] + exact Ordinal.add_sub_cancel _ _ + +theorem κ_sub_lt {i j k : κ} (h₁ : i < j + k) (h₂ : j ≤ i) : i - j < k := by + rw [← Ordinal.typein_lt_typein (· < ·)] at h₁ ⊢ + rw [← not_lt, ← Ordinal.typein_le_typein (· < ·)] at h₂ + rw [Params.κ_add_typein, ← Ordinal.sub_lt_of_le h₂] at h₁ + rw [Params.κ_sub_typein] + exact h₁ + /-- Either the base type or a proper type index (an element of `Λ`). The base type is written `⊥`. -/ @[reducible] diff --git a/ConNF/Structural/Support.lean b/ConNF/Structural/Support.lean index 48b2e5487a..3a70dcb903 100644 --- a/ConNF/Structural/Support.lean +++ b/ConNF/Structural/Support.lean @@ -229,17 +229,26 @@ theorem pow_le_of_isStrongLimit {κ μ : Cardinal.{u}} (h₁ : IsStrongLimit μ) have := Cardinal.infinite_iff.mpr h₁.isLimit.aleph0_le exact pow_le_of_isStrongLimit' h₁ h₂ -/-- There are at most `μ` supports. -/ -theorem mk_support_le : #(Support α) ≤ #μ := by - rw [Cardinal.mk_congr supportEquiv] - simp only [mk_sigma, mk_pi, mk_supportCondition, prod_const, lift_id] - refine le_trans (sum_le_sum _ (fun _ => #μ) ?_) ?_ - · intro i - refine pow_le_of_isStrongLimit Params.μ_isStrongLimit ?_ - refine lt_of_lt_of_le ?_ Params.κ_le_μ_ord_cof - exact card_typein_lt (· < ·) i Params.κ_ord.symm - · simp only [sum_const, lift_id, mul_mk_eq_max, ge_iff_le, max_le_iff, le_refl, and_true] - exact Params.κ_lt_μ.le +/-- There are exactly `μ` supports. -/ +@[simp] +theorem mk_support : #(Support α) = #μ := by + refine le_antisymm ?_ ?_ + · rw [Cardinal.mk_congr supportEquiv] + simp only [mk_sigma, mk_pi, mk_supportCondition, prod_const, lift_id] + refine le_trans (sum_le_sum _ (fun _ => #μ) ?_) ?_ + · intro i + refine pow_le_of_isStrongLimit Params.μ_isStrongLimit ?_ + refine lt_of_lt_of_le ?_ Params.κ_le_μ_ord_cof + exact card_typein_lt (· < ·) i Params.κ_ord.symm + · simp only [sum_const, lift_id, mul_mk_eq_max, ge_iff_le, max_le_iff, le_refl, and_true] + exact Params.κ_lt_μ.le + · rw [← mk_atom] + refine ⟨⟨fun a => ⟨1, fun _ _ => ⟨default, Sum.inl a⟩⟩, ?_⟩⟩ + intro a₁ a₂ h + simp only [Support.mk.injEq, heq_eq_eq, true_and] at h + have := congr_fun₂ h 0 κ_zero_lt_one + simp only [SupportCondition.mk.injEq, Sum.inl.injEq, true_and] at this + exact this instance {G : Type _} [SMul G (SupportCondition α)] : SMul G (Support α) where smul g S := ⟨S.max, fun i hi => g • S.f i hi⟩ @@ -286,4 +295,58 @@ instance {G : Type _} [Monoid G] [MulAction G (SupportCondition α)] : MulAction intro j hj simp only [smul_f, mul_smul] +/-- Note: In the paper, the sum of supports requires an additional step of closing over atoms in +certain intersections of near-litters. We'll try to get away without adding this for as long as +possible. -/ +instance : Add (Support α) where + add S T := ⟨S.max + T.max, fun i hi => + if hi' : i < S.max then + S.f i hi' + else + T.f (i - S.max) (κ_sub_lt hi (not_lt.mp hi'))⟩ + +theorem Support.add_f_eq {S T : Support α} {i : κ} (hi : i < (S + T).max) : + (S + T).f i hi = + if hi' : i < S.max then + S.f i hi' + else + T.f (i - S.max) (κ_sub_lt hi (not_lt.mp hi')) := + rfl + +@[simp] +theorem Support.add_max {S T : Support α} : (S + T).max = S.max + T.max := + rfl + +theorem Support.add_f_left {S T : Support α} {i : κ} (h : i < S.max) : + (S + T).f i (h.trans_le (κ_le_self_add _ _)) = S.f i h := + by rw [add_f_eq, dif_pos h] + +theorem Support.add_f_right {S T : Support α} {i : κ} (h₁ : i < (S + T).max) (h₂ : S.max ≤ i) : + (S + T).f i h₁ = T.f (i - S.max) (κ_sub_lt h₁ h₂) := + by rw [add_f_eq, dif_neg (not_lt.mpr h₂)] + +theorem Support.add_f_right_add {S T : Support α} {i : κ} (h : i < T.max) : + (S + T).f (S.max + i) (add_lt_add_left h S.max) = T.f i h := by + rw [add_f_right] + simp only [κ_add_sub_cancel] + exact κ_le_self_add _ _ + +theorem Support.add_coe (S T : Support α) : + (S + T : Set (SupportCondition α)) = (S : Set _) ∪ T := by + ext c + simp only [mem_carrier_iff, Set.mem_union] + constructor + · rintro ⟨i, hi, rfl⟩ + by_cases hi' : i < S.max + · refine Or.inl ⟨i, hi', ?_⟩ + rw [add_f_left] + · refine Or.inr ⟨i - S.max, κ_sub_lt hi (not_lt.mp hi'), ?_⟩ + rw [add_f_right] + exact not_lt.mp hi' + · rintro (⟨i, hi, rfl⟩ | ⟨i, hi, rfl⟩) + · refine ⟨i, hi.trans_le (κ_le_self_add _ _), ?_⟩ + rw [add_f_left] + · refine ⟨S.max + i, add_lt_add_left hi S.max, ?_⟩ + rw [add_f_right_add] + end ConNF