Addition of supports

Signed-off-by: zeramorphic <[email protected]>

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]

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