feat(data/fin/succ_pred): fin is an archimedean succ/pred order (#1…

…2792)

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/algebra/big_operators/fin.lean

@@ -181,11 +181,7 @@ end
 lemma alternating_sum_eq_finset_sum {G : Type*} [add_comm_group G] :
   ∀ (L : list G), alternating_sum L = ∑ i : fin L.length, (-1 : ℤ) ^ (i : ℕ) • L.nth_le i i.is_lt
 | [] := by { rw [alternating_sum, finset.sum_eq_zero], rintro ⟨i, ⟨⟩⟩ }
-| (g :: []) :=
-begin
-  show g = ∑ i : fin 1, (-1 : ℤ) ^ (i : ℕ) • [g].nth_le i i.2,
-  rw [fin.sum_univ_succ], simp,
-end
+| (g :: []) := by simp
 | (g :: h :: L) :=
 calc g + -h + L.alternating_sum
     = g + -h + ∑ i : fin L.length, (-1 : ℤ) ^ (i : ℕ) • L.nth_le i i.2 :

src/data/fin/basic.lean

@@ -1169,6 +1169,54 @@ protected lemma coe_neg (a : fin n) : ((-a : fin n) : ℕ) = (n - a) % n := rfl
 protected lemma coe_sub (a b : fin n) : ((a - b : fin n) : ℕ) = (a + (n - b)) % n :=
 by cases a; cases b; refl
 
+@[simp] lemma coe_fin_one (a : fin 1) : ↑a = 0 :=
+by rw [subsingleton.elim a 0, fin.coe_zero]
+
+@[simp] lemma coe_neg_one : ↑(-1 : fin (n + 1)) = n :=
+begin
+  cases n,
+  { simp },
+  rw [fin.coe_neg, fin.coe_one, nat.succ_sub_one, nat.mod_eq_of_lt],
+  constructor
+end
+
+lemma coe_sub_one {n} (a : fin (n + 1)) : ↑(a - 1) = if a = 0 then n else a - 1 :=
+begin
+  cases n,
+  { simp },
+  split_ifs,
+  { simp [h] },
+  rw [sub_eq_add_neg, coe_add_eq_ite, coe_neg_one, if_pos, add_comm, add_tsub_add_eq_tsub_left],
+  rw [add_comm ↑a, add_le_add_iff_left, nat.one_le_iff_ne_zero],
+  rwa subtype.ext_iff at h
+end
+
+/-- By sending `x` to `last n - x`, `fin n` is order-equivalent to its `order_dual`. -/
+def _root_.order_iso.fin_equiv : ∀ {n}, order_dual (fin n) ≃o fin n
+| 0 := ⟨⟨elim0, elim0, elim0, elim0⟩, elim0⟩
+| (n+1) := order_iso.symm $
+{ to_fun    := λ x, last n - x,
+  inv_fun   := λ x, last n - x,
+  left_inv  := sub_sub_cancel _,
+  right_inv := sub_sub_cancel _,
+  map_rel_iff' := λ a b,
+  begin
+    rw [order_dual.has_le],
+    simp only [equiv.coe_fn_mk],
+    rw [le_iff_coe_le_coe, fin.coe_sub, fin.coe_sub, coe_last],
+    have : (n - ↑b) % (n + 1) ≤ (n - ↑a) % (n + 1) ↔ a ≤ b,
+    { rw [nat.mod_eq_of_lt, nat.mod_eq_of_lt, tsub_le_tsub_iff_left a.is_le,
+          le_iff_coe_le_coe]; exact tsub_le_self.trans_lt n.lt_succ_self },
+    suffices key : ∀ {x : fin (n + 1)}, (n + (n + 1 - x)) % (n + 1) = (n - x) % (n + 1),
+    { convert this using 2; exact key },
+    intro x,
+    rw [add_comm, tsub_add_eq_add_tsub x.is_lt.le, add_tsub_assoc_of_le x.is_le, nat.add_mod_left]
+  end }
+
+lemma _root_.order_iso.fin_equiv_apply (a) : order_iso.fin_equiv a = last n - a.of_dual := rfl
+lemma _root_.order_iso.fin_equiv_symm_apply (a) :
+  order_iso.fin_equiv.symm a = order_dual.to_dual (last n - a) := rfl
+
 end add_group
 
 section succ_above

src/data/fin/succ_pred.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2022 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Rodriguez
+-/
+import order.succ_pred.basic
+
+/-!
+# Successors and predecessors of `fin n`
+
+In this file, we show that `fin n` is both a `succ_order` and a `pred_order`. Note that they are
+also archimedean, but this is derived from the general instance for well-orderings as opposed
+to a specific `fin` instance.
+
+-/
+
+namespace fin
+
+instance : ∀ {n : ℕ}, succ_order (fin n)
+| 0 := by constructor; exact elim0
+| (n+1) :=
+_root_.succ_order.of_core (λ i, if i < fin.last n then i + 1 else i)
+begin
+  intros a ha b,
+  rw [is_max_iff_eq_top, eq_top_iff, not_le, top_eq_last] at ha,
+  rw [if_pos ha, lt_iff_coe_lt_coe, le_iff_coe_le_coe, coe_add_one_of_lt ha],
+  exact nat.lt_iff_add_one_le
+end
+begin
+  intros a ha,
+  rw [is_max_iff_eq_top, top_eq_last] at ha,
+  rw [if_neg ha.not_lt],
+end
+
+@[simp] lemma succ_eq {n : ℕ} : succ_order.succ = λ a, if a < fin.last n then a + 1 else a := rfl
+@[simp] lemma succ_apply {n : ℕ} (a) :
+  succ_order.succ a = if a < fin.last n then a + 1 else a := rfl
+
+instance : ∀ {n : ℕ}, pred_order (fin n)
+| 0 := by constructor; exact elim0
+| (n+1) :=
+_root_.pred_order.of_core (λ x, if x = 0 then 0 else x - 1)
+begin
+  intros a ha b,
+  rw [is_min_iff_eq_bot, eq_bot_iff, not_le, bot_eq_zero] at ha,
+  rw [if_neg ha.ne', lt_iff_coe_lt_coe, le_iff_coe_le_coe, coe_sub_one,
+      if_neg ha.ne', le_tsub_iff_right, iff.comm],
+  exact nat.lt_iff_add_one_le,
+  exact ha
+end
+begin
+  intros a ha,
+  rw [is_min_iff_eq_bot, bot_eq_zero] at ha,
+  rwa [if_pos ha, eq_comm],
+end
+
+@[simp] lemma pred_eq {n} : pred_order.pred = λ a : fin (n + 1), if a = 0 then 0 else a - 1 := rfl
+@[simp] lemma pred_apply {n : ℕ} (a : fin (n + 1)) :
+  pred_order.pred a = if a = 0 then 0 else a - 1 := rfl
+
+end fin

src/data/fintype/basic.lean

@@ -1727,12 +1727,19 @@ have ∀ x y, r x y → (univ.filter (λ z, r z x)).card < (univ.filter (λ z, r
     exact ⟨λ z hzx, trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩,
 subrelation.wf this (measure_wf _)
 
-lemma preorder.well_founded [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) :=
+lemma preorder.well_founded_lt [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) :=
 well_founded_of_trans_of_irrefl _
 
-@[instance, priority 10] lemma linear_order.is_well_order [fintype α] [linear_order α] :
+lemma preorder.well_founded_gt [fintype α] [preorder α] : well_founded ((>) : α → α → Prop) :=
+well_founded_of_trans_of_irrefl _
+
+@[instance, priority 10] lemma linear_order.is_well_order_lt [fintype α] [linear_order α] :
   is_well_order α (<) :=
-{ wf := preorder.well_founded }
+{ wf := preorder.well_founded_lt }
+
+@[instance, priority 10] lemma linear_order.is_well_order_gt [fintype α] [linear_order α] :
+  is_well_order α (>) :=
+{ wf := preorder.well_founded_gt }
 
 end fintype
 

src/order/rel_classes.lean

@@ -462,3 +462,6 @@ instance order_dual.is_total_le [has_le α] [is_total α (≤)] : is_total (orde
 @is_total.swap α _ _
 
 instance nat.lt.is_well_order : is_well_order ℕ (<) := ⟨nat.lt_wf⟩
+
+instance [linear_order α] [h : is_well_order α (<)] : is_well_order (order_dual α) (>) := h
+instance [linear_order α] [h : is_well_order α (>)] : is_well_order (order_dual α) (<) := h

src/order/succ_pred/basic.lean

@@ -114,6 +114,29 @@ end preorder
 section linear_order
 variables [linear_order α]
 
+/-- A constructor for `succ_order α` for `α` a linear order. -/
+@[simps] def succ_order.of_core (succ : α → α) (hn : ∀ {a}, ¬ is_max a → ∀ b, a < b ↔ succ a ≤ b)
+  (hm : ∀ a, is_max a → succ a = a) : succ_order α :=
+{ succ           := succ,
+  succ_le_of_lt  := λ a b, classical.by_cases (λ h hab, (hm a h).symm ▸ hab.le) (λ h, (hn h b).mp),
+  le_succ        := λ a, classical.by_cases (λ h, (hm a h).symm.le)
+                                            (λ h, le_of_lt $ by simpa using (hn h a).not),
+  le_of_lt_succ  := λ a b hab, classical.by_cases (λ h, hm b h ▸ hab.le)
+                                                  (λ h, by simpa [hab] using (hn h a).not),
+  max_of_succ_le := λ a, not_imp_not.mp $ λ h, by simpa using (hn h a).not }
+
+/-- A constructor for `pred_order α` for `α` a linear order. -/
+@[simps] def pred_order.of_core {α} [linear_order α] (pred : α → α)
+  (hn : ∀ {a}, ¬ is_min a → ∀ b, b ≤ pred a ↔ b < a) (hm : ∀ a, is_min a → pred a = a) :
+  pred_order α :=
+{ pred           := pred,
+  le_pred_of_lt  := λ a b, classical.by_cases (λ h hab, (hm b h).symm ▸ hab.le) (λ h, (hn h a).mpr),
+  pred_le        := λ a, classical.by_cases (λ h, (hm a h).le)
+                                            (λ h, le_of_lt $ by simpa using (hn h a).not),
+  le_of_pred_lt  := λ a b hab, classical.by_cases (λ h, hm a h ▸ hab.le)
+                                                  (λ h, by simpa [hab] using (hn h b).not),
+  min_of_le_pred := λ a, not_imp_not.mp $ λ h, by simpa using (hn h a).not }
+
 /-- A constructor for `succ_order α` usable when `α` is a linear order with no maximal element. -/
 def succ_order.of_succ_le_iff (succ : α → α) (hsucc_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b) :
   succ_order α :=
@@ -939,6 +962,31 @@ lemma pred.rec_linear {p : α → Prop} (hsucc : ∀ a, p a ↔ p (pred a)) (a b
 end pred_order
 end linear_order
 
+section is_well_order
+variables [linear_order α]
+
+@[priority 100]
+instance is_well_order.to_is_pred_archimedean [h : is_well_order α (<)] [pred_order α] :
+  is_pred_archimedean α :=
+⟨λ a, begin
+  refine well_founded.fix h.wf (λ b ih hab, _),
+  replace hab := hab.eq_or_lt,
+  rcases hab with rfl | hab,
+  { exact ⟨0, rfl⟩ },
+  cases le_or_lt b (pred b) with hb hb,
+  { cases (min_of_le_pred hb).not_lt hab },
+  obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt hab),
+  refine ⟨k + 1, _⟩,
+  rw [iterate_add_apply, iterate_one, hk],
+end⟩
+
+@[priority 100]
+instance is_well_order.to_is_succ_archimedean [h : is_well_order α (>)] [succ_order α] :
+  is_succ_archimedean α :=
+by convert @order_dual.is_succ_archimedean (order_dual α) _ _ _
+
+end is_well_order
+
 section order_bot
 variables [preorder α] [order_bot α] [succ_order α] [is_succ_archimedean α]
 

src/set_theory/ordinal/basic.lean

@@ -479,7 +479,7 @@ instance (o : ordinal) : has_well_founded o.out.α := ⟨o.out.r, o.out.wo.wf⟩
 instance (o : ordinal) : linear_order o.out.α :=
 is_well_order.linear_order o.out.r
 
-instance (o : ordinal) : is_well_order o.out.α (<) :=
+instance ordinal.is_well_order_lt (o : ordinal) : is_well_order o.out.α (<) :=
 o.out.wo
 
 namespace ordinal