Merge pull request #45 from leanprover-community/support-refactor

ConNF/BaseType/Params.lean

@@ -54,9 +54,10 @@ class Params where
   [κ_isWellOrder : IsWellOrder κ (· < ·)]
   κ_ord : Ordinal.type ((· < ·) : κ → κ → Prop) = (#κ).ord
   κ_isRegular : (#κ).IsRegular
+  [κ_succ : SuccOrder κ]
   [κ_addMonoid : AddMonoid κ]
-  [κ_covariant : CovariantClass κ κ (· + ·) (· ≤ ·)]
-  [κ_covariant_swap : CovariantClass κ κ (Function.swap (· + ·)) (· ≤ ·)]
+  κ_typein (i j : κ) : Ordinal.typein (· < ·) (i + j : κ) =
+    Ordinal.typein (· < ·) i + Ordinal.typein (· < ·) j
   Λ_lt_κ : #Λ < #κ
   /--
   A large type used in indexing the litters.
@@ -83,6 +84,41 @@ There exist valid parameters for the model. The smallest such parameters are
 * `μ = ℶ_{ω_1}`.
 -/
 
+theorem noMaxOrder_of_ordinal_type_eq {α : Type u} [Preorder α] [Infinite α] [IsWellOrder α (· < ·)]
+    (h : (Ordinal.type ((· < ·) : α → α → Prop)).IsLimit) : NoMaxOrder α := by
+  refine ⟨fun a => ?_⟩
+  have := (Ordinal.succ_lt_of_isLimit h).mpr (Ordinal.typein_lt_type (· < ·) a)
+  obtain ⟨b, hb⟩ := Ordinal.typein_surj (· < ·) this
+  refine ⟨b, ?_⟩
+  have := Order.lt_succ (Ordinal.typein (fun x y => x < y) a)
+  rw [← hb, Ordinal.typein_lt_typein] at this
+  exact this
+
+noncomputable def succOrderOfIsWellOrder {α : Type u} [Preorder α] [Infinite α]
+    [inst : IsWellOrder α (· < ·)] (h : (Ordinal.type ((· < ·) : α → α → Prop)).IsLimit) :
+    SuccOrder α where
+  succ := inst.toIsWellFounded.wf.succ
+  le_succ a := le_of_lt (WellFounded.lt_succ _ ((noMaxOrder_of_ordinal_type_eq h).exists_gt a))
+  max_of_succ_le ha hb :=
+    (ha.not_lt (WellFounded.lt_succ _ ((noMaxOrder_of_ordinal_type_eq h).exists_gt _))).elim
+  succ_le_of_lt := by
+    intro a b ha
+    by_contra hb
+    obtain hab | hab | hab :=
+      inst.toIsTrichotomous.trichotomous (inst.toIsWellFounded.wf.succ a) b
+    · exact hb hab.le
+    · exact hb hab.le
+    · rw [WellFounded.lt_succ_iff ((noMaxOrder_of_ordinal_type_eq h).exists_gt a)] at hab
+      obtain (hab | hab) := hab
+      exact ha.not_lt hab
+      exact ha.ne hab.symm
+  le_of_lt_succ := by
+    intro a b ha
+    rw [WellFounded.lt_succ_iff ((noMaxOrder_of_ordinal_type_eq h).exists_gt _)] at ha
+    obtain (ha | ha) := ha
+    exact ha.le
+    exact ha.le
+
 theorem typein_add_lt_of_type_eq_ord {α : Type _}
     [Infinite α] [LinearOrder α] [IsWellOrder α (· < ·)]
     (h : Ordinal.type ((· < ·) : α → α → Prop) = (#α).ord) (x y : α) :
@@ -162,33 +198,6 @@ 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 add_covariant_of_type_eq_ord {α : Type _}
-    [Infinite α] [LinearOrder α] [IsWellOrder α (· < ·)]
-    (h : Ordinal.type ((· < ·) : α → α → Prop) = (#α).ord) :
-    CovariantClass α α (add_of_type_eq_ord h).add (· ≤ ·) where
-  elim x y z := by
-    contrapose
-    rw [not_le, not_le]
-    intro h
-    have := (Ordinal.enum_lt_enum _ _).mp h
-    simp only [add_lt_add_iff_left, Ordinal.typein_lt_typein] at this
-    exact this
-
-noncomputable def add_covariant_swap_of_type_eq_ord {α : Type _}
-    [Infinite α] [LinearOrder α] [IsWellOrder α (· < ·)]
-    (h : Ordinal.type ((· < ·) : α → α → Prop) = (#α).ord) :
-    CovariantClass α α (Function.swap (add_of_type_eq_ord h).add) (· ≤ ·) where
-  elim x y z := by
-    contrapose
-    rw [not_le, not_le]
-    intro h
-    have := (Ordinal.enum_lt_enum _ _).mp h
-    obtain (h' | h' | h') := lt_trichotomy z y
-    · exact h'
-    · subst h'
-      simp only [lt_self_iff_false] at this
-    · cases (add_le_add_right ((Ordinal.typein_lt_typein (· < ·)).mpr h').le _).not_lt this
-
 noncomputable example : Params.{0} where
   Λ := ℕ
   Λ_zero_le := zero_le
@@ -200,18 +209,15 @@ noncomputable example : Params.{0} where
   κ_isRegular := by
     simp only [Cardinal.card_ord, Cardinal.mk_ordinal_out]
     exact isRegular_aleph_one
-  κ_addMonoid :=
-    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)
-  κ_covariant :=
+  κ_succ :=
     let _ : Infinite (aleph 1).ord.out.α :=
       by simp only [Cardinal.infinite_iff, mk_ordinal_out, card_ord, aleph0_le_aleph]
-    add_covariant_of_type_eq_ord (by simp)
-  κ_covariant_swap :=
+    succOrderOfIsWellOrder (by rw [Ordinal.type_lt]; exact ord_aleph_isLimit 1)
+  κ_addMonoid :=
     let _ : Infinite (aleph 1).ord.out.α :=
       by simp only [Cardinal.infinite_iff, mk_ordinal_out, card_ord, aleph0_le_aleph]
-    add_covariant_swap_of_type_eq_ord (by simp)
+    addMonoid_of_type_eq_ord (by simp)
+  κ_typein i j := Ordinal.typein_enum _ _
   Λ_lt_κ := by
     rw [mk_denumerable, mk_ordinal_out, card_ord]
     exact aleph0_lt_aleph_one
@@ -228,16 +234,6 @@ noncomputable example : Params.{0} where
     rw [beth_normal.cof_eq (ord_isLimit <| aleph0_le_aleph 1)]
     exact isRegular_aleph_one.2
 
-theorem noMaxOrder_of_ordinal_type_eq {α : Type u} [Preorder α] [Infinite α] [IsWellOrder α (· < ·)]
-    (h : (Ordinal.type ((· < ·) : α → α → Prop)).IsLimit) : NoMaxOrder α := by
-  refine ⟨fun a => ?_⟩
-  have := (Ordinal.succ_lt_of_isLimit h).mpr (Ordinal.typein_lt_type (· < ·) a)
-  obtain ⟨b, hb⟩ := Ordinal.typein_surj (· < ·) this
-  refine ⟨b, ?_⟩
-  have := Order.lt_succ (Ordinal.typein (fun x y => x < y) a)
-  rw [← hb, Ordinal.typein_lt_typein] at this
-  exact this
-
 variable [Params.{u}] {ι α β : Type u}
 
 /-! The types `Λ`, `κ`, `μ` are inhabited and infinite. -/
@@ -260,11 +256,14 @@ instance : NoMaxOrder Λ := noMaxOrder_of_ordinal_type_eq Params.Λ_isLimit
 
 instance : LinearOrder κ := Params.κ_linearOrder
 instance : IsWellOrder κ (· < ·) := Params.κ_isWellOrder
+instance : SuccOrder κ := Params.κ_succ
 instance : AddMonoid κ := Params.κ_addMonoid
-instance : CovariantClass κ κ (· + ·) (· ≤ ·) := Params.κ_covariant
-instance : CovariantClass κ κ (Function.swap (· + ·)) (· ≤ ·) := Params.κ_covariant_swap
 instance : Inhabited κ := ⟨0⟩
 instance : Infinite κ := Cardinal.infinite_iff.mpr Params.κ_isRegular.aleph0_le
+instance : NoMaxOrder κ := by
+  have := Cardinal.ord_isLimit Params.κ_isRegular.aleph0_le
+  rw [← Params.κ_ord] at this
+  exact noMaxOrder_of_ordinal_type_eq this
 
 instance : LinearOrder μ := Params.μ_linearOrder
 instance : IsWellOrder μ (· < ·) := Params.μ_isWellOrder
@@ -275,6 +274,74 @@ instance : NoMaxOrder μ := by
   rw [← Params.μ_ord] at this
   exact noMaxOrder_of_ordinal_type_eq this
 
+def κ_ofNat : ℕ → κ
+  | 0 => 0
+  | n + 1 => Order.succ (κ_ofNat n)
+
+instance (n : ℕ) : OfNat κ n := ⟨κ_ofNat n⟩
+
+instance : CovariantClass κ κ (· + ·) (· ≤ ·) := by
+  constructor
+  intro i j k h
+  rw [← not_lt, ← Ordinal.typein_le_typein (· < ·)] at h ⊢
+  rw [Params.κ_typein, Params.κ_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]
+  exact add_le_add_right h _
+
+@[simp]
+theorem κ_typein_zero : Ordinal.typein ((· < ·) : κ → κ → Prop) 0 = 0 := by
+  have := add_zero (0 : κ)
+  rw [← Ordinal.typein_inj (· < ·), Params.κ_typein] at this
+  conv at this => rhs; rw [← add_zero (Ordinal.typein _ _)]
+  rw [Ordinal.add_left_cancel] at this
+  exact this
+
+theorem κ_le_zero_iff (i : κ) : i ≤ 0 ↔ i = 0 :=
+  by rw [← not_lt, ← Ordinal.typein_le_typein (· < ·), κ_typein_zero, Ordinal.le_zero,
+    ← κ_typein_zero, Ordinal.typein_inj]
+
+@[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]
+
+@[simp]
+theorem κ_succ_typein (i : κ) :
+    Ordinal.typein ((· < ·) : κ → κ → Prop) (Order.succ i) =
+    Ordinal.typein ((· < ·) : κ → κ → Prop) i + 1 := by
+  refine le_antisymm ?_ ?_
+  · have : i < Ordinal.enum (· < ·) (Ordinal.typein ((· < ·) : κ → κ → Prop) i + 1) ?_
+    · conv_lhs => rw [← Ordinal.enum_typein ((· < ·) : κ → κ → Prop) i]
+      rw [Ordinal.enum_lt_enum (r := (· < ·))]
+      · exact lt_add_one _
+      · have := Order.lt_succ i
+        rw [← Ordinal.typein_lt_typein ((· < ·) : κ → κ → Prop)] at this
+        exact (Order.succ_le_of_lt this).trans_lt (Ordinal.typein_lt_type _ _)
+    have := Order.succ_le_of_lt this
+    conv at this => lhs; rw [← Ordinal.enum_typein ((· < ·) : κ → κ → Prop) (Order.succ i)]
+    rw [← not_lt, Ordinal.enum_le_enum] at this
+    exact this
+  · simp only [Ordinal.add_one_eq_succ, Order.succ_le_iff, Ordinal.typein_lt_typein,
+      Order.lt_succ_iff_not_isMax, gt_iff_lt, not_isMax, not_false_eq_true]
+
+theorem κ_zero_lt_one : (0 : κ) < 1 := by
+  rw [← Ordinal.typein_lt_typein ((· < ·) : κ → κ → Prop)]
+  exact lt_of_lt_of_eq (lt_add_one _) (κ_succ_typein 0).symm
+
+@[simp]
+theorem κ_lt_one_iff (i : κ) : i < 1 ↔ i = 0 := by
+  constructor
+  · rw [← κ_le_zero_iff]
+    exact SuccOrder.le_of_lt_succ
+  · rintro rfl
+    exact κ_zero_lt_one
+
 /-- Either the base type or a proper type index (an element of `Λ`).
 The base type is written `⊥`. -/
 @[reducible]

ConNF/FOA/Basic/Constrains.lean

@@ -405,9 +405,9 @@ theorem small_constrains {β : Λ} (c : SupportCondition β) : Small {d | d ≺
     · obtain ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, B, t, rfl, rfl⟩ := h
       refine lt_of_le_of_lt ?_ (designatedSupport t).small
       suffices
-        #{a : SupportCondition β |
-            ∃ c : designatedSupport t, a = ⟨(B.cons hδ).comp c.val.path, c.val.value⟩} ≤
-          #(designatedSupport t) by
+        #{a : SupportCondition β | ∃ c : (designatedSupport t : Set (SupportCondition δ)),
+            a = ⟨(B.cons hδ).comp c.val.path, c.val.value⟩} ≤
+          #(designatedSupport t : Set (SupportCondition δ)) by
         refine le_trans (Cardinal.mk_subtype_le_of_subset ?_) this
         rintro x ⟨_, _, _, _, _, _, _, _, _, _, _, c, hc, rfl, h⟩
         rw [SupportCondition.mk.injEq] at h

ConNF/FOA/Basic/Reduction.lean

@@ -184,29 +184,8 @@ theorem reduction_supports (S : Set (SupportCondition β)) (c : SupportCondition
 theorem reduction_designatedSupport_supports [TangleData β] (t : Tangle β) :
     Supports (Allowable β) (reduction (designatedSupport t : Set (SupportCondition β))) t := by
   intro ρ h
-  refine (designatedSupport t).supports ρ ?_
+  refine designatedSupport_supports t ρ ?_
   intros c hc'
   exact reduction_supports (designatedSupport t) c hc' (Allowable.toStructPerm ρ) h
 
-/-- A support for a tangle containing only reduced support conditions. -/
-noncomputable def reducedSupport [TangleData β] (t : Tangle β) : Support β (Allowable β) t
-    where
-  carrier := reduction (designatedSupport t : Set (SupportCondition β))
-  small := reduction_small (designatedSupport t).small
-  supports := reduction_designatedSupport_supports t
-
-theorem mem_reducedSupport_iff [TangleData β] (t : Tangle β) (c : SupportCondition β) :
-    c ∈ reducedSupport t ↔ c ∈ reduction (designatedSupport t : Set (SupportCondition β)) :=
-  Iff.rfl
-
-theorem lt_of_mem_reducedSupport
-    {β γ δ ε : Λ} [LeLevel β] [LeLevel γ] [LtLevel δ] [LtLevel ε]
-    (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < γ) (hδε : (δ : TypeIndex) ≠ ε)
-    (B : Path (β : TypeIndex) γ) (t : Tangle δ)
-    (c : SupportCondition δ) (h : c ∈ reducedSupport t) :
-    (⟨(B.cons hδ).comp c.path, c.value⟩ : SupportCondition β) <
-      ⟨(B.cons hε).cons (bot_lt_coe _), inr (fuzz hδε t).toNearLitter⟩ := by
-  obtain ⟨⟨d, hd, hcd⟩, _⟩ := h
-  exact Relation.TransGen.tail' (le_comp hcd _) (Constrains.fuzz hδ hε hδε B t d hd)
-
 end ConNF

ConNF/FOA/Properties/Injective.lean

@@ -218,7 +218,7 @@ theorem Biexact.smul_eq_smul {β : Λ} [LeLevel β] {π π' : Allowable β} {c :
     refine h₁.trans (h₂.trans ?_).symm
     refine' congr_arg _ _
     rw [← inv_smul_eq_iff, smul_smul]
-    refine' (designatedSupport t).supports _ _
+    refine' designatedSupport_supports t _ _
     intro c hc
     rw [mul_smul, inv_smul_eq_iff]
     simp only [Allowable.toStructPerm_smul, Allowable.toStructPerm_comp, Tree.comp_comp]
@@ -423,7 +423,7 @@ theorem supports {β : Λ} [LeLevel β] {π π' : Allowable β} {t : Tangle β}
       Allowable.toStructPerm π' A • N) :
     π • t = π' • t := by
   rw [← inv_smul_eq_iff, smul_smul]
-  refine' (designatedSupport t).supports _ _
+  refine' designatedSupport_supports t _ _
   intro c hc
   rw [mul_smul, inv_smul_eq_iff]
   simp only [Allowable.smul_supportCondition_eq_smul_iff]
@@ -802,7 +802,7 @@ theorem ihAction_smul_tangle' (hπf : π.Free) (c d : SupportCondition β) (A :
         (ihsAction_comp_mapFlexible hπf _ _ _) • hL₂.t := by
   obtain ⟨⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩, t, rfl⟩ := hL₂
   rw [← inv_smul_eq_iff, smul_smul]
-  refine' (designatedSupport t).supports _ _
+  refine' designatedSupport_supports t _ _
   intro e he
   rw [mul_smul, inv_smul_eq_iff]
   simp only [ne_eq, Allowable.smul_supportCondition_eq_smul_iff]

ConNF/Fuzz/Hypotheses.lean

@@ -41,10 +41,11 @@ class TangleData (α : TypeIndex) where
   [allowableGroup : Group Allowable]
   allowableToStructPerm : Allowable →* StructPerm α
   [allowableAction : MulAction Allowable Tangle]
-  designatedSupport :
+  designatedSupport : Tangle → Support α
+  designatedSupport_supports (t : Tangle) :
     haveI : MulAction Allowable (SupportCondition α) :=
       MulAction.compHom _ allowableToStructPerm
-    (t : Tangle) → Support α Allowable t
+    MulAction.Supports Allowable (designatedSupport t : Set (SupportCondition α)) t
 
 export TangleData (Tangle Allowable)
 
@@ -87,9 +88,13 @@ end Allowable
 
 /-- For each tangle, we provide a small support for it. This is known as the designated support of
 the tangle. -/
-def designatedSupport {α : TypeIndex} [TangleData α] (t : Tangle α) : Support α (Allowable α) t :=
+def designatedSupport {α : TypeIndex} [TangleData α] (t : Tangle α) : Support α :=
   TangleData.designatedSupport t
 
+theorem designatedSupport_supports {α : TypeIndex} [TangleData α] (t : Tangle α) :
+    MulAction.Supports (Allowable α) (designatedSupport t : Set (SupportCondition α)) t :=
+  TangleData.designatedSupport_supports t
+
 class PositionedTangles (α : TypeIndex) [TangleData α] where
   /-- A position function, giving each tangle a unique position `ν : μ`.
   The existence of this injection proves that there are at most `μ` tangles at level `α`.
@@ -140,14 +145,11 @@ instance Bot.tangleData : TangleData ⊥
   Allowable := NearLitterPerm
   allowableToStructPerm := Tree.toBotIso.toMonoidHom
   allowableAction := inferInstance
-  designatedSupport a :=
-    { carrier := {⟨Quiver.Path.nil, Sum.inl a⟩}
-      supports := fun π => by
-        intro h
-        simp only [mem_singleton_iff, NearLitterPerm.smul_supportCondition_eq_iff, forall_eq,
-          Sum.smul_inl, Sum.inl.injEq] at h
-        exact h
-      small := small_singleton _ }
+  designatedSupport a := ⟨1, fun _ _ => ⟨Quiver.Path.nil, Sum.inl a⟩⟩
+  designatedSupport_supports a π h := by
+    simp only [Support.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
+      NearLitterPerm.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inl, Sum.inl.injEq] at h
+    exact h
 
 /-- A position function for atoms, which is chosen arbitrarily. -/
 noncomputable instance instPositionAtom : Position Atom μ :=