From ac2dabdedf318d7ec9b41163c314f44fab501787 Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Wed, 14 Aug 2024 09:34:47 +0800 Subject: [PATCH] =?UTF-8?q?chore:=20use=20`=E2=89=A0`=20in=20`Fin.ne=5Fof?= =?UTF-8?q?=5Fval=5Fne`=20(#5011)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Instead of a `Not (Eq …)` term use the proper `≠` in `Fin.ne_of_val_ne`, to make it symmetric with `Fin.val_ne_of_ne`, and move the former to the same place as the latter. This answers a query of @eric-wieser at https://github.com/leanprover-community/mathlib4/pull/15762#discussion_r1714990412 --- src/Init/Data/Fin/Basic.lean | 3 +++ src/Init/Prelude.lean | 5 +---- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index 39896ddb75..cab7b21a77 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -149,6 +149,9 @@ instance : Inhabited (Fin (no_index (n+1))) where @[simp] theorem zero_eta : (⟨0, Nat.zero_lt_succ _⟩ : Fin (n + 1)) = 0 := rfl +theorem ne_of_val_ne {i j : Fin n} (h : val i ≠ val j) : i ≠ j := + fun h' => absurd (val_eq_of_eq h') h + theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j := fun h' => absurd (eq_of_val_eq h') h diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 54fbcd3d5d..d1d4f1627f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1845,14 +1845,11 @@ theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j theorem Fin.val_eq_of_eq {n} {i j : Fin n} (h : Eq i j) : Eq i.val j.val := h ▸ rfl -theorem Fin.ne_of_val_ne {n} {i j : Fin n} (h : Not (Eq i.val j.val)) : Not (Eq i j) := - fun h' => absurd (val_eq_of_eq h') h - instance (n : Nat) : DecidableEq (Fin n) := fun i j => match decEq i.val j.val with | isTrue h => isTrue (Fin.eq_of_val_eq h) - | isFalse h => isFalse (Fin.ne_of_val_ne h) + | isFalse h => isFalse (fun h' => absurd (Fin.val_eq_of_eq h') h) instance {n} : LT (Fin n) where lt a b := LT.lt a.val b.val