max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use ≠ in Fin.ne_of_val_ne (#5011)

Browse source 
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
This commit is contained in:
Jeremy Tan Jie Rui 2024-08-14 09:34:47 +08:00 • committed by GitHub
parent 7283e2c14e
commit ac2dabdedf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Data/Fin/Basic.lean
View file

@ -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

5
src/Init/Prelude.lean
View file

@ -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