More theory cleanup

Author: nomeata

src/Init/Internal/Order/Basic.lean

@@ -423,7 +423,7 @@ theorem monotone_dite
 
 end monotone_lemmas
 
-section prod_order
+section pprod_order
 
 open PartialOrder
 
@@ -440,87 +440,96 @@ instance [PartialOrder α] [PartialOrder β] : PartialOrder (α ×' β) where
     dsimp at *
     rw [rel_antisymm ha.1 hb.1, rel_antisymm ha.2 hb.2]
 
-theorem monotone_prod [PartialOrder α] [PartialOrder β] [PartialOrder γ]
+theorem monotone_pprod [PartialOrder α] [PartialOrder β] [PartialOrder γ]
     {f : γ → α} {g : γ → β} (hf : monotone f) (hg : monotone g) :
     monotone (fun x => PProd.mk (f x) (g x)) :=
   fun _ _ h12 => ⟨hf _ _ h12, hg _ _ h12⟩
 
-theorem monotone_fst [PartialOrder α] [PartialOrder β] [PartialOrder γ]
+theorem monotone_pprod_fst [PartialOrder α] [PartialOrder β] [PartialOrder γ]
     {f : γ → α ×' β} (hf : monotone f) : monotone (fun x => (f x).1) :=
   fun _ _ h12 => (hf _ _ h12).1
 
-theorem monotone_snd [PartialOrder α] [PartialOrder β] [PartialOrder γ]
+theorem monotone_pprod_snd [PartialOrder α] [PartialOrder β] [PartialOrder γ]
     {f : γ → α ×' β} (hf : monotone f) : monotone (fun x => (f x).2) :=
   fun _ _ h12 => (hf _ _ h12).2
 
-def chain_fst [CCPO α] [CCPO β] (c : α ×' β → Prop) : α → Prop := (fun a => ∃ b, c ⟨a, b⟩)
-def chain_snd [CCPO α] [CCPO β] (c : α ×' β → Prop) : β → Prop := (fun b => ∃ a, c ⟨a, b⟩)
+def chain_pprod_fst [CCPO α] [CCPO β] (c : α ×' β → Prop) : α → Prop := fun a => ∃ b, c ⟨a, b⟩
+def chain_pprod_snd [CCPO α] [CCPO β] (c : α ×' β → Prop) : β → Prop := fun b => ∃ a, c ⟨a, b⟩
 
-theorem chain.fst [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) :
-    chain (chain_fst c) := by
+theorem chain.pprod_fst [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) :
+    chain (chain_pprod_fst c) := by
   intro a₁ a₂ ⟨b₁, h₁⟩ ⟨b₂, h₂⟩
   cases hchain ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h₁ h₂
   case inl h => left; exact h.1
   case inr h => right; exact h.1
 
-theorem chain.snd [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) :
-    chain (chain_snd c) := by
+theorem chain.pprod_snd [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) :
+    chain (chain_pprod_snd c) := by
   intro b₁ b₂ ⟨a₁, h₁⟩ ⟨a₂, h₂⟩
   cases hchain ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h₁ h₂
   case inl h => left; exact h.2
   case inr h => right; exact h.2
 
 instance [CCPO α] [CCPO β] : CCPO (α ×' β) where
-  csup c := ⟨CCPO.csup (chain_fst c), CCPO.csup (chain_snd c)⟩
+  csup c := ⟨CCPO.csup (chain_pprod_fst c), CCPO.csup (chain_pprod_snd c)⟩
   csup_spec := by
     intro ⟨a, b⟩ c hchain
     dsimp
     constructor
     next =>
       intro ⟨h₁, h₂⟩ ⟨a', b'⟩ cab
-      dsimp at *
-      constructor <;> dsimp
+      constructor <;> dsimp at *
       · apply rel_trans ?_ h₁
-        apply le_csup hchain.fst
+        apply le_csup hchain.pprod_fst
         exact ⟨b', cab⟩
       · apply rel_trans ?_ h₂
-        apply le_csup hchain.snd
+        apply le_csup hchain.pprod_snd
         exact ⟨a', cab⟩
     next =>
       intro h
       constructor <;> dsimp
-      · apply csup_le hchain.fst
+      · apply csup_le hchain.pprod_fst
         intro a' ⟨b', hcab⟩
         apply (h _ hcab).1
-      · apply csup_le hchain.snd
+      · apply csup_le hchain.pprod_snd
         intro b' ⟨a', hcab⟩
         apply (h _ hcab).2
 
-theorem admissible_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α → Prop)
+theorem admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α → Prop)
     (hadm : admissible P) : admissible (fun (x : α ×' β) => P x.1) := by
   intro c hchain h
-  apply hadm _ hchain.fst
+  apply hadm _ hchain.pprod_fst
   intro x ⟨y, hxy⟩
   apply h ⟨x,y⟩ hxy
 
-theorem admissible_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β → Prop)
+theorem admissible_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β → Prop)
     (hadm : admissible P) : admissible (fun (x : α ×' β) => P x.2) := by
   intro c hchain h
-  apply hadm _ hchain.snd
+  apply hadm _ hchain.pprod_snd
   intro y ⟨x, hxy⟩
   apply h ⟨x,y⟩ hxy
 
-end prod_order
+end pprod_order
 
 section flat_order
 
 variable {α : Sort u}
 
 set_option linter.unusedVariables false in
+/--
+`FlatOrder b` wraps the type `α` with the flat partial order generated by `∀ x, b ⊑ x`.
+
+This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
+-/
 def FlatOrder {α : Sort u} (b : α) := α
 
 variable {b : α}
 
+/--
+The flat partial order generated by `∀ x, b ⊑ x`.
+
+This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
+-/
 inductive FlatOrder.rel : (x y : FlatOrder b) → Prop where
   | bot : rel b x
   | refl : rel x x
@@ -590,9 +599,15 @@ end flat_order
 
 section mono_bind
 
+/--
+The class `MonoBind m` indicates that every `m α` has a `PartialOrder`, and that the bind operation
+on `m` is monotone in both arguments with regard to that order.
+
+This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
+-/
 class MonoBind (m : Type u → Type v) [Bind m] [∀ α, PartialOrder (m α)] where
-  bind_mono_left (a₁ a₂ : m α) (f : α → m b) (h : a₁ ⊑ a₂) : a₁ >>= f ⊑ a₂ >>= f
-  bind_mono_right (a : m α) (f₁ f₂ : α → m b) (h : ∀ x, f₁ x ⊑ f₂ x) : a >>= f₁ ⊑ a >>= f₂
+  bind_mono_left {a₁ a₂ : m α} {f : α → m b} (h : a₁ ⊑ a₂) : a₁ >>= f ⊑ a₂ >>= f
+  bind_mono_right {a : m α} {f₁ f₂ : α → m b} (h : ∀ x, f₁ x ⊑ f₂ x) : a >>= f₁ ⊑ a >>= f₂
 
 theorem monotone_bind
     (m : Type u → Type v) [Bind m] [∀ α, PartialOrder (m α)] [MonoBind m]
@@ -604,18 +619,18 @@ theorem monotone_bind
     monotone (fun (x : γ) => f x >>= g x) := by
   intro x₁ x₂ hx₁₂
   apply PartialOrder.rel_trans
-  · apply MonoBind.bind_mono_left _ _ _ (hmono₁ _ _ hx₁₂)
-  · apply MonoBind.bind_mono_right _ _ _ (fun y => monotone_apply y _ hmono₂ _ _ hx₁₂)
+  · apply MonoBind.bind_mono_left (hmono₁ _ _ hx₁₂)
+  · apply MonoBind.bind_mono_right (fun y => monotone_apply y _ hmono₂ _ _ hx₁₂)
 
 instance : PartialOrder (Option α) := inferInstanceAs (PartialOrder (FlatOrder none))
 noncomputable instance : CCPO (Option α) := inferInstanceAs (CCPO (FlatOrder none))
 noncomputable instance : MonoBind Option where
-  bind_mono_left _ _ _ h := by
+  bind_mono_left h := by
     cases h
     · exact FlatOrder.rel.bot
     · exact FlatOrder.rel.refl
-  bind_mono_right a _ _ h := by
-    cases a
+  bind_mono_right h := by
+    cases ‹Option _›
     · exact FlatOrder.rel.refl
     · exact h _
 
@@ -626,10 +641,10 @@ theorem admissible_eq_some (P : Prop) (y : α) :
 instance [Monad m] [inst : ∀ α, PartialOrder (m α)] : PartialOrder (ExceptT ε m α) := inst _
 instance [Monad m] [∀ α, PartialOrder (m α)] [inst : ∀ α, CCPO (m α)] : CCPO (ExceptT ε m α) := inst _
 instance [Monad m] [∀ α, PartialOrder (m α)] [∀ α, CCPO (m α)] [MonoBind m] : MonoBind (ExceptT ε m) where
-  bind_mono_left a₁ a₂ f h₁₂ := by
+  bind_mono_left h₁₂ := by
     apply MonoBind.bind_mono_left (m := m)
     exact h₁₂
-  bind_mono_right a₁ a₂ f h₁₂ := by
+  bind_mono_right h₁₂ := by
     apply MonoBind.bind_mono_right (m := m)
     intro x
     cases x