Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2022 Eric Rodriguez. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Rodriguez
! This file was ported from Lean 3 source module data.fin.succ_pred
! leanprover-community/mathlib commit 7c523cb78f4153682c2929e3006c863bfef463d0
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fin.Basic
import Mathlib.Order.SuccPred.Basic
/-!
# Successors and predecessors of `Fin n`
In this file, we show that `Fin n` is both a `SuccOrder` and a `PredOrder`. 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 : ℕ }, SuccOrder ( Fin n )
| 0 => by constructor
le_succ ∀ (a : Fin 0 a ≤ ?succ a
max_of_succ_le
succ_le_of_lt ∀ {a b : Fin 0 a < b ?succ a ≤ b
le_of_lt_succ ∀ {a b : Fin 0 a < ?succ b a ≤ b
succ <;>
le_succ ∀ (a : Fin 0 a ≤ ?succ a
max_of_succ_le
succ_le_of_lt ∀ {a b : Fin 0 a < b ?succ a ≤ b
le_of_lt_succ ∀ {a b : Fin 0 a < ?succ b a ≤ b
succ first | assumption
le_succ ∀ (a : Fin 0 a ≤ ?succ a | intro a succ_le_of_lt ∀ {b : Fin 0 a < b ?succ a ≤ b ; le_of_lt_succ ∀ {b : Fin 0 a < ?succ b a ≤ b
succ_le_of_lt ∀ {a b : Fin 0 a < b ?succ a ≤ b exact elim0 : ∀ {α : Sort ?u.433}, Fin 0 α a
| n + 1 =>
SuccOrder.ofCore ( fun i => if i < Fin.last : (n : ℕ ) → Fin (n + 1 n then i + 1 else i )
( by
intro a ha b a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b
rw [ a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b isMax_iff_eq_top , a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b eq_top_iff , a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b not_le , a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b top_eq_last a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b ] a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b at ha a < b ↔ (fun i => if i < last n i + 1 i ) a ≤ b
dsimp a < b ↔ (if a < last n a + 1 a ) ≤ b
rw [ a < b ↔ (if a < last n a + 1 a ) ≤ b if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.922} {t e : α }, (if c then t else e ) = t ha , a < b ↔ (if a < last n a + 1 a ) ≤ b lt_iff_val_lt_val : ∀ {n : ℕ } {a b : Fin n a < b ↔ ↑a < ↑b , a < b ↔ (if a < last n a + 1 a ) ≤ b le_iff_val_le_val : ∀ {n : ℕ } {a b : Fin n a ≤ b ↔ ↑a ≤ ↑b , a < b ↔ (if a < last n a + 1 a ) ≤ b val_add_one_of_lt ha ]
exact Nat.lt_iff_add_one_le : ∀ {m n : ℕ }, m < n ↔ m + 1 ≤ n )
( by
intro a ha (fun i => if i < last n i + 1 i ) a = a
rw [ (fun i => if i < last n i + 1 i ) a = a isMax_iff_eq_top , (fun i => if i < last n i + 1 i ) a = a (fun i => if i < last n i + 1 i ) a = a top_eq_last (fun i => if i < last n i + 1 i ) a = a ] (fun i => if i < last n i + 1 i ) a = a at ha (fun i => if i < last n i + 1 i ) a = a
dsimp (if a < last n a + 1 a ) = a
rw [ (if a < last n a + 1 a ) = a if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.1173} {t e : α }, (if c then t else e ) = e ha . not_lt ] )
@[ simp ]
theorem succ_eq : ∀ {n : ℕ }, SuccOrder.succ = fun a => if a < last n a + 1 a succ_eq { n : ℕ } : SuccOrder.succ = fun a => if a < Fin.last : (n : ℕ ) → Fin (n + 1 n then a + 1 else a :=
rfl : ∀ {α : Sort ?u.2074} {a : α }, a = a
#align fin.succ_eq Fin.succ_eq : ∀ {n : ℕ }, SuccOrder.succ = fun a => if a < last n a + 1 a
@[ simp ]
theorem succ_apply { n : ℕ } ( a ) : SuccOrder.succ a = if a < Fin.last : (n : ℕ ) → Fin (n + 1 n then a + 1 else a :=
rfl : ∀ {α : Sort ?u.2355} {a : α }, a = a
#align fin.succ_apply Fin.succ_apply
instance : ∀ { n : ℕ }, PredOrder ( Fin n )
| 0 => by constructor
pred_le ∀ (a : Fin 0 ?pred a ≤ a
min_of_le_pred
le_pred_of_lt ∀ {a b : Fin 0 a < b a ≤ ?pred b
le_of_pred_lt ∀ {a b : Fin 0 ?pred a < b a ≤ b
pred <;>
pred_le ∀ (a : Fin 0 ?pred a ≤ a
min_of_le_pred
le_pred_of_lt ∀ {a b : Fin 0 a < b a ≤ ?pred b
le_of_pred_lt ∀ {a b : Fin 0 ?pred a < b a ≤ b
pred first |
le_of_pred_lt ∀ {a b : Fin 0 ?pred a < b a ≤ b assumption |
le_of_pred_lt ∀ {a b : Fin 0 ?pred a < b a ≤ b intro a ; le_pred_of_lt ∀ {b : Fin 0 a < b a ≤ ?pred b exact elim0 : ∀ {α : Sort ?u.2842}, Fin 0 α a
| n + 1 =>
PredOrder.ofCore ( fun x => if x = 0 then 0 else x - 1 )
( by
∀ {a : Fin (n + 1 ¬ IsMin a ∀ (b : Fin (n + 1 b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a intro a ha b b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a
∀ {a : Fin (n + 1 ¬ IsMin a ∀ (b : Fin (n + 1 b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a rw [ b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a isMin_iff_eq_bot , b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a eq_bot_iff , b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a not_le , b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a bot_eq_zero : ∀ (n : ℕ ), ⊥ = 0 b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a ] b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a at ha b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a
∀ {a : Fin (n + 1 ¬ IsMin a ∀ (b : Fin (n + 1 b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a dsimp (b ≤ if a = 0 0 else a - 1 ↔ b < a
∀ {a : Fin (n + 1 ¬ IsMin a ∀ (b : Fin (n + 1 b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a rw [ (b ≤ if a = 0 0 else a - 1 ↔ b < a if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.3354} {t e : α }, (if c then t else e ) = e ha . ne' : ∀ {α : Type ?u.3357} [inst : Preorder α x y : α }, x < y y ≠ x , (b ≤ if a = 0 0 else a - 1 ↔ b < a lt_iff_val_lt_val : ∀ {n : ℕ } {a b : Fin n a < b ↔ ↑a < ↑b , (b ≤ if a = 0 0 else a - 1 ↔ b < a le_iff_val_le_val : ∀ {n : ℕ } {a b : Fin n a ≤ b ↔ ↑a ≤ ↑b , (b ≤ if a = 0 0 else a - 1 ↔ b < a coe_sub_one : ∀ {n : ℕ } (a : Fin (n + 1 ↑(a - 1 = if a = 0 n else ↑a - 1 , (↑b ≤ if a = 0 n else ↑a - 1 ↔ ↑b < ↑a (b ≤ if a = 0 0 else a - 1 ↔ b < a if_neg : ∀ {c : Prop } {h : Decidable c ¬ c ∀ {α : Sort ?u.3462} {t e : α }, (if c then t else e ) = e ha . ne' : ∀ {α : Type ?u.3465} [inst : Preorder α x y : α }, x < y y ≠ x ,
(b ≤ if a = 0 0 else a - 1 ↔ b < a le_tsub_iff_right , (b ≤ if a = 0 0 else a - 1 ↔ b < a Iff.comm : ∀ {a b : Prop }, (a ↔ b ↔ (b ↔ a ]
∀ {a : Fin (n + 1 ¬ IsMin a ∀ (b : Fin (n + 1 b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a exact Nat.lt_iff_add_one_le : ∀ {m n : ℕ }, m < n ↔ m + 1 ≤ n
∀ {a : Fin (n + 1 ¬ IsMin a ∀ (b : Fin (n + 1 b ≤ (fun x => if x = 0 0 else x - 1 ) a ↔ b < a exact ha )
( by
∀ (a : Fin (n + 1 IsMin a (fun x => if x = 0 0 else x - 1 ) a = a intro a ha (fun x => if x = 0 0 else x - 1 ) a = a
∀ (a : Fin (n + 1 IsMin a (fun x => if x = 0 0 else x - 1 ) a = a rw [ (fun x => if x = 0 0 else x - 1 ) a = a isMin_iff_eq_bot , (fun x => if x = 0 0 else x - 1 ) a = a (fun x => if x = 0 0 else x - 1 ) a = a bot_eq_zero : ∀ (n : ℕ ), ⊥ = 0 (fun x => if x = 0 0 else x - 1 ) a = a ] (fun x => if x = 0 0 else x - 1 ) a = a at ha (fun x => if x = 0 0 else x - 1 ) a = a
∀ (a : Fin (n + 1 IsMin a (fun x => if x = 0 0 else x - 1 ) a = a dsimp (if a = 0 0 else a - 1 ) = a
∀ (a : Fin (n + 1 IsMin a (fun x => if x = 0 0 else x - 1 ) a = a rwa [ (if a = 0 0 else a - 1 ) = a if_pos : ∀ {c : Prop } {h : Decidable c c → ∀ {α : Sort ?u.4261} {t e : α }, (if c then t else e ) = t ha , (if a = 0 0 else a - 1 ) = a eq_comm : ∀ {α : Sort ?u.4270} {a b : α }, a = b ↔ b = a ] )
@[ simp ]
theorem pred_eq : ∀ {n : ℕ }, PredOrder.pred = fun a => if a = 0 0 else a - 1 pred_eq { n } : PredOrder.pred = fun a : Fin ( n + 1 ) => if a = 0 then 0 else a - 1 :=
rfl : ∀ {α : Sort ?u.5331} {a : α }, a = a
#align fin.pred_eq Fin.pred_eq : ∀ {n : ℕ }, PredOrder.pred = fun a => if a = 0 0 else a - 1
@[ simp ]
theorem pred_apply { n : ℕ } ( a : Fin ( n + 1 )) : PredOrder.pred a = if a = 0 then 0 else a - 1 :=
rfl : ∀ {α : Sort ?u.5663} {a : α }, a = a
#align fin.pred_apply Fin.pred_apply
end Fin