feat: improvements to grind annotations for Fin (#11299)
This PR add many `@[grind]` annotations for `Fin`, and updates the tests.
This commit is contained in:
Kim Morrison
GitHub
parent
26b435fa4d
commit
90389a8d90
8 changed files with 706 additions and 441 deletions
|
|
@ -1056,7 +1056,7 @@ theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} :
|
|||
@[simp, grind =] theorem toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
|
||||
(setWidth' p x).toFin = x.toFin.castLE (Nat.pow_le_pow_right (by omega) (by omega)) := by
|
||||
ext
|
||||
rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.coe_castLE, val_toFin,
|
||||
rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.val_castLE, val_toFin,
|
||||
Nat.mod_eq_of_lt (by apply BitVec.toNat_lt_twoPow_of_le p)]
|
||||
|
||||
theorem toNat_setWidth_of_le {w w' : Nat} {b : BitVec w} (h : w ≤ w') : (b.setWidth w').toNat = b.toNat := by
|
||||
|
|
|
|||
|
|
@ -246,6 +246,11 @@ instance neg (n : Nat) : Neg (Fin n) :=
|
|||
|
||||
theorem neg_def (a : Fin n) : -a = ⟨(n - a) % n, Nat.mod_lt _ a.pos⟩ := rfl
|
||||
|
||||
-- Later we give another version called `Fin.val_neg` that splits on `a = 0`.
|
||||
protected theorem val_neg' (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
|
||||
rfl
|
||||
|
||||
@[deprecated Fin.val_neg' (since := "2025-11-21")]
|
||||
protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
|
||||
rfl
|
||||
|
||||
|
|
|
|||
|
|
@ -16,17 +16,25 @@ open Std
|
|||
|
||||
namespace Fin
|
||||
|
||||
@[simp] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
|
||||
@[simp, grind =] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
|
||||
|
||||
@[deprecated ofNat_zero (since := "2025-05-28")] abbrev ofNat'_zero := @ofNat_zero
|
||||
|
||||
theorem mod_def (a m : Fin n) : a % m = Fin.mk (a.val % m.val) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
|
||||
rfl
|
||||
|
||||
theorem val_mod (a m : Fin n) : (a % m).val = a.val % m.val := rfl
|
||||
|
||||
theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ a.pos) := rfl
|
||||
|
||||
theorem val_mul (a b : Fin n) : (a * b).val = (a.val * b.val) % n := rfl
|
||||
|
||||
theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b.val) + a.val) % n) (Nat.mod_lt _ a.pos) := rfl
|
||||
|
||||
@[grind =]
|
||||
theorem val_sub (a b : Fin n) : (a - b).val = ((n - b.val) + a.val) % n := rfl
|
||||
|
||||
@[grind →]
|
||||
theorem pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.pos
|
||||
|
||||
@[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
|
||||
|
|
@ -38,7 +46,8 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
|
|||
|
||||
@[simp] protected theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := rfl
|
||||
|
||||
@[ext] protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
|
||||
@[ext, grind ext]
|
||||
protected theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
|
||||
|
||||
theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
|
||||
|
||||
|
|
@ -69,7 +78,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
|
|||
|
||||
@[deprecated val_ofNat (since := "2025-05-28")] abbrev val_ofNat' := @val_ofNat
|
||||
|
||||
@[simp] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
|
||||
@[simp, grind =] theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by
|
||||
ext
|
||||
simp
|
||||
congr
|
||||
|
|
@ -89,7 +98,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
|
|||
@[simp] theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val :=
|
||||
rfl
|
||||
|
||||
@[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
|
||||
@[simp, grind =] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
|
||||
rfl
|
||||
|
||||
@[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
|
||||
|
|
@ -259,7 +268,9 @@ instance : LawfulOrderLT (Fin n) where
|
|||
lt_iff := by
|
||||
simp [← Fin.not_le, Decidable.imp_iff_not_or, Std.Total.total]
|
||||
|
||||
@[simp, grind =] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
|
||||
@[simp] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
|
||||
|
||||
grind_pattern val_rev => i.rev
|
||||
|
||||
@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
|
||||
rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
|
||||
|
|
@ -284,6 +295,8 @@ theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
|
|||
|
||||
@[simp] theorem val_last (n : Nat) : (last n).1 = n := rfl
|
||||
|
||||
grind_pattern val_last => last n
|
||||
|
||||
@[simp] theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by
|
||||
ext
|
||||
simp
|
||||
|
|
@ -393,6 +406,8 @@ theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt zero_lt_one
|
|||
|
||||
@[simp] theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := rfl
|
||||
|
||||
grind_pattern val_succ => j.succ
|
||||
|
||||
@[simp] theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by
|
||||
simp [Fin.lt_def]
|
||||
|
||||
|
|
@ -453,12 +468,18 @@ theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
|
|||
theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
|
||||
Fin.ne_of_gt (one_lt_succ_succ a)
|
||||
|
||||
@[simp] theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
|
||||
@[simp, grind =] theorem val_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
|
||||
|
||||
@[deprecated val_castLT (since := "2025-11-21")]
|
||||
theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
|
||||
|
||||
@[simp] theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ :=
|
||||
rfl
|
||||
|
||||
@[simp, grind =] theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
|
||||
@[simp, grind =] theorem val_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
|
||||
|
||||
@[deprecated val_castLE (since := "2025-11-21")]
|
||||
theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
|
||||
|
||||
@[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
|
||||
castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := rfl
|
||||
|
|
@ -470,13 +491,16 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
|
|||
|
||||
@[simp] theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
|
||||
Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
|
||||
Fin.ext (by simp only [coe_castLE])
|
||||
Fin.ext (by simp only [val_castLE])
|
||||
|
||||
@[simp] theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
|
||||
Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) :=
|
||||
funext (castLE_castLE km mn)
|
||||
|
||||
@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
|
||||
@[simp, grind =] theorem val_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
|
||||
|
||||
@[deprecated val_cast (since := "2025-11-21")]
|
||||
theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
|
||||
|
||||
@[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
|
||||
Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
|
||||
|
|
@ -489,7 +513,7 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
|
|||
@[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
|
||||
|
||||
@[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h = last n' :=
|
||||
Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
|
||||
Fin.ext (by rw [val_cast, val_last, val_last, Nat.succ.inj h])
|
||||
|
||||
@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
|
||||
|
||||
|
|
@ -504,7 +528,10 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
|
|||
|
||||
theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
|
||||
|
||||
@[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
|
||||
@[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
|
||||
|
||||
@[deprecated val_castAdd (since := "2025-11-21")]
|
||||
theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
|
||||
|
||||
@[simp] theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := rfl
|
||||
|
||||
|
|
@ -540,7 +567,10 @@ the reverse direction. -/
|
|||
theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
|
||||
(i.cast h).succ = i.succ.cast (by rw [h]) := rfl
|
||||
|
||||
@[simp] theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
|
||||
@[simp, grind =] theorem val_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
|
||||
|
||||
@[deprecated val_castSucc (since := "2025-11-21")]
|
||||
theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
|
||||
|
||||
@[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt_succ_of_lt h⟩ := rfl
|
||||
|
||||
|
|
@ -548,7 +578,7 @@ theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
|
|||
i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := rfl
|
||||
|
||||
theorem castSucc_lt_succ {i : Fin n} : i.castSucc < i.succ :=
|
||||
lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
|
||||
lt_def.2 <| by simp only [val_castSucc, val_succ, Nat.lt_succ_self]
|
||||
|
||||
theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by
|
||||
simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm
|
||||
|
|
@ -602,7 +632,7 @@ theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by
|
|||
|
||||
@[deprecated castSucc_lt_succ (since := "2025-10-29")]
|
||||
theorem lt_succ {a : Fin n} : a.castSucc < a.succ := by
|
||||
rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
|
||||
rw [castSucc, lt_def, val_castAdd, val_succ]; exact Nat.lt_succ_self a.val
|
||||
|
||||
theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n :=
|
||||
⟨fun ⟨j, hj⟩ => hj ▸ Fin.ne_of_lt j.castSucc_lt_last,
|
||||
|
|
@ -610,7 +640,10 @@ theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i)
|
|||
|
||||
theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
|
||||
|
||||
@[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
|
||||
@[simp, grind =] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
|
||||
|
||||
@[deprecated val_addNat (since := "2025-11-21")]
|
||||
theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
|
||||
|
||||
@[simp] theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by
|
||||
ext
|
||||
|
|
@ -638,7 +671,10 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
|
|||
(addNat i m').cast h = addNat i m :=
|
||||
Fin.ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
|
||||
|
||||
@[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
|
||||
@[simp, grind =] theorem val_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
|
||||
|
||||
@[deprecated val_natAdd (since := "2025-11-21")]
|
||||
theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
|
||||
|
||||
@[simp] theorem natAdd_mk (n i : Nat) (hi : i < m) :
|
||||
natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := rfl
|
||||
|
|
@ -695,7 +731,7 @@ theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSu
|
|||
omega
|
||||
|
||||
theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
|
||||
rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
|
||||
rw [val_rev, val_castAdd, val_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
|
||||
|
||||
theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
|
||||
rw [← rev_rev (castAdd ..), rev_castAdd, rev_rev]
|
||||
|
|
@ -717,7 +753,12 @@ theorem castSucc_natAdd (n : Nat) (i : Fin k) :
|
|||
|
||||
/-! ### pred -/
|
||||
|
||||
@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
|
||||
@[simp] theorem val_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
|
||||
|
||||
grind_pattern val_pred => j.pred h
|
||||
|
||||
@[deprecated val_pred (since := "2025-11-21")]
|
||||
theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
|
||||
|
||||
@[simp] theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
|
||||
| ⟨0, _⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
|
||||
|
|
@ -735,7 +776,7 @@ theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin
|
|||
theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
|
||||
Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
|
||||
⟨i, h⟩ := by
|
||||
simp only [Fin.ext_iff, coe_pred, Nat.add_sub_cancel]
|
||||
simp only [Fin.ext_iff, val_pred, Nat.add_sub_cancel]
|
||||
|
||||
@[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
|
||||
Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := pred_mk_succ i _
|
||||
|
|
@ -762,10 +803,13 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
|
|||
|
||||
theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
|
||||
pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
|
||||
rw [Fin.ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
|
||||
rw [Fin.ext_iff, val_pred, val_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
|
||||
exact Nat.add_lt_add_right h 1
|
||||
|
||||
@[simp] theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
|
||||
@[simp, grind =] theorem val_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
|
||||
|
||||
@[deprecated val_subNat (since := "2025-11-21")]
|
||||
theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
|
||||
|
||||
@[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
|
||||
subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := rfl
|
||||
|
|
@ -830,11 +874,11 @@ step. `Fin.succRec` is a version of this induction principle that takes the `Fin
|
|||
(zero : ∀ n, motive (n + 1) 0) (succ : ∀ n i, motive n i → motive (Nat.succ n) i.succ) :
|
||||
motive n i := i.succRec zero succ
|
||||
|
||||
@[simp] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
|
||||
@[simp, grind =] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
|
||||
@Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by
|
||||
cases n <;> rfl
|
||||
|
||||
@[simp] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
|
||||
@[simp, grind =] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
|
||||
@Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
|
||||
cases i; rfl
|
||||
|
||||
|
|
@ -862,11 +906,11 @@ where
|
|||
| 0, hi => by rwa [Fin.mk_zero]
|
||||
| i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
|
||||
|
||||
@[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
@[simp, grind =] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
(hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
|
||||
(induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := rfl
|
||||
|
||||
@[simp] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
@[simp, grind =] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
(succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
|
||||
induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := rfl
|
||||
|
||||
|
|
@ -898,13 +942,13 @@ The corresponding induction principle is `Fin.induction`.
|
|||
(zero : motive 0) (succ : ∀ i : Fin n, motive i.succ) :
|
||||
∀ i : Fin (n + 1), motive i := induction zero fun i _ => succ i
|
||||
|
||||
@[simp] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
@[simp, grind =] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
@Fin.cases n motive zero succ 0 = zero := rfl
|
||||
|
||||
@[simp] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
|
||||
@[simp, grind =] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
|
||||
@Fin.cases n motive zero succ i.succ = succ i := rfl
|
||||
|
||||
@[simp] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
@[simp, grind =] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
{i : Nat} (h : i + 1 < n + 1) :
|
||||
@Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
|
||||
|
||||
|
|
@ -954,7 +998,7 @@ For the induction:
|
|||
| j + 1 => go j (by omega) (by omega) (cast ⟨j, by omega⟩ x)
|
||||
go _ _ (by omega) last
|
||||
|
||||
@[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
@[simp, grind =] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
(reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
|
||||
rw [reverseInduction, reverseInduction.go]; simp
|
||||
|
||||
|
|
@ -971,7 +1015,7 @@ private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1)
|
|||
dsimp only
|
||||
rw [ih _ _ (by omega), eq_comm, reverseInduction.go, dif_neg (by change i.1 + 1 ≠ _; omega)]
|
||||
|
||||
@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
@[simp, grind =] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
(i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
|
||||
succ i (reverseInduction zero succ i.succ) := by
|
||||
rw [reverseInduction, reverseInduction_castSucc_aux _ _ _ i.isLt, reverseInduction]
|
||||
|
|
@ -990,11 +1034,11 @@ The corresponding induction principle is `Fin.reverseInduction`.
|
|||
(cast : ∀ i : Fin n, motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
|
||||
reverseInduction last (fun i _ => cast i) i
|
||||
|
||||
@[simp] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
|
||||
@[simp, grind =] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
|
||||
(Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last :=
|
||||
reverseInduction_last ..
|
||||
|
||||
@[simp] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
|
||||
@[simp, grind =] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
|
||||
(i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i :=
|
||||
reverseInduction_castSucc ..
|
||||
|
||||
|
|
@ -1014,11 +1058,11 @@ as `Fin.natAdd m (j : Fin n)`.
|
|||
if hi : (i : Nat) < m then (castAdd_castLT n i hi) ▸ (left (castLT i hi))
|
||||
else (natAdd_subNat_cast (Nat.le_of_not_lt hi)) ▸ (right _)
|
||||
|
||||
@[simp] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
|
||||
@[simp, grind =] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
|
||||
addCases (motive := motive) left right (Fin.castAdd n i) = left i := by
|
||||
rw [addCases, dif_pos (castAdd_lt _ _)]; rfl
|
||||
|
||||
@[simp]
|
||||
@[simp, grind =]
|
||||
theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
|
||||
addCases (motive := motive) left right (natAdd m i) = right i := by
|
||||
have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)
|
||||
|
|
@ -1051,6 +1095,7 @@ theorem add_ofNat [NeZero n] (x : Fin n) (y : Nat) :
|
|||
|
||||
/-! ### sub -/
|
||||
|
||||
@[deprecated val_sub (since := "2025-11-21")]
|
||||
protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
|
||||
cases a; cases b; rfl
|
||||
|
||||
|
|
@ -1102,6 +1147,7 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
|
|||
|
||||
/-! ### neg -/
|
||||
|
||||
@[grind =]
|
||||
theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
|
||||
(-x).val = if x = 0 then 0 else n - x.val := by
|
||||
change (n - ↑x) % n = _
|
||||
|
|
@ -1117,7 +1163,7 @@ protected theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by
|
|||
apply elim0 x
|
||||
· replace h : NeZero n := ⟨h⟩
|
||||
ext
|
||||
rw [Fin.coe_sub, Fin.val_add, val_neg]
|
||||
rw [Fin.val_sub, Fin.val_add, val_neg]
|
||||
split
|
||||
· simp_all
|
||||
· simp [Nat.add_comm]
|
||||
|
|
@ -1138,9 +1184,6 @@ theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
|
|||
|
||||
@[deprecated mul_ofNat (since := "2025-05-28")] abbrev mul_ofNat' := @mul_ofNat
|
||||
|
||||
theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
|
||||
| ⟨_, _⟩, ⟨_, _⟩ => rfl
|
||||
|
||||
@[deprecated val_mul (since := "2025-10-26")]
|
||||
theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
|
||||
| ⟨_, _⟩, ⟨_, _⟩ => rfl
|
||||
|
|
|
|||
|
|
@ -108,7 +108,7 @@ instance : ToInt (Fin n) (.co 0 n) where
|
|||
toInt_inj x y w := Fin.eq_of_val_eq (Int.ofNat_inj.mp w)
|
||||
toInt_mem := by simp
|
||||
|
||||
@[simp] theorem toInt_fin (x : Fin n) : ToInt.toInt x = (x.val : Int) := rfl
|
||||
@[simp, grind =] theorem toInt_fin (x : Fin n) : ToInt.toInt x = (x.val : Int) := rfl
|
||||
|
||||
instance [NeZero n] : ToInt.Zero (Fin n) (.co 0 n) where
|
||||
toInt_zero := rfl
|
||||
|
|
|
|||
|
|
@ -2264,6 +2264,7 @@ structure Fin (n : Nat) where
|
|||
isLt : LT.lt val n
|
||||
|
||||
attribute [coe] Fin.val
|
||||
grind_pattern Fin.isLt => self.val
|
||||
|
||||
theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
|
||||
| ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
|
||||
|
|
|
|||
|
|
@ -5,409 +5,108 @@ Many of these will remain out of scope, and can be deleted as this is decided.
|
|||
|
||||
open Fin
|
||||
|
||||
example (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := by grind
|
||||
namespace Fin'
|
||||
|
||||
example {n a : Nat} {ha : a < n} [NeZero n] :
|
||||
/-! Challenge problems: -/
|
||||
|
||||
theorem mk_eq_zero {n a : Nat} {ha : a < n} [NeZero n] :
|
||||
(⟨a, ha⟩ : Fin n) = 0 ↔ a = 0 := by grind
|
||||
|
||||
example {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by grind
|
||||
theorem zero_eq_mk {n a : Nat} {ha : a < n} [NeZero n] :
|
||||
0 = (⟨a, ha⟩ : Fin n) ↔ a = 0 := by grind
|
||||
|
||||
example [NeZero n] (x : Fin n) : (Fin.ofNat n x.val) = x := by grind
|
||||
theorem zero_eq_one_iff {n : Nat} [NeZero n] : (0 : Fin n) = 1 ↔ n = 1 := by grind
|
||||
|
||||
example (a : Fin (2 * n + 1)) : a.val + (-a).val = 2 * n + 1 := by grind
|
||||
theorem one_eq_zero_iff {n : Nat} [NeZero n] : (1 : Fin n) = 0 ↔ n = 1 := by grind
|
||||
|
||||
example [NeZero n] {a : Fin n} : 0 < a ↔ a ≠ 0 := by grind
|
||||
theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1 := by grind
|
||||
|
||||
example (i : Fin n) : rev (rev i) = i := by grind
|
||||
theorem last_add_one : ∀ n, last n + 1 = 0 := by grind
|
||||
|
||||
example {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by grind
|
||||
theorem val_add_one {n : Nat} (i : Fin (n + 1)) :
|
||||
((i + 1 : Fin (n + 1)) : Nat) = if i = last _ then (0 : Nat) else i + 1 := by grind
|
||||
|
||||
example {i j : Fin n} : rev i = rev j ↔ i = j := by grind
|
||||
theorem val_two {n : Nat} : (2 : Fin (n + 3)).val = 2 := by grind
|
||||
|
||||
example (n : Nat) : (last n).1 = n := by grind
|
||||
theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) < i + 1 := by grind
|
||||
|
||||
example {n : Nat} : (0 : Fin (n + 1)) = last n ↔ n = 0 := by grind
|
||||
theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := by grind
|
||||
|
||||
example {n : Nat} : Fin.last n = 0 ↔ n = 0 := by grind
|
||||
theorem succ_one_eq_two : Fin.succ (1 : Fin (n + 2)) = 2 := by grind
|
||||
|
||||
example (i : Fin (n + 1)) : i ≤ last n := by grind
|
||||
theorem add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _ := by grind
|
||||
|
||||
example : (0 : Fin (n + 2)) < last (n + 1) := by grind
|
||||
theorem add_one_le_iff {n : Nat} : ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last _ := by grind
|
||||
|
||||
example {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n := by grind
|
||||
theorem lt_add_one_iff {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n := by grind
|
||||
|
||||
example {i : Fin (n + 1)} : i ≠ last n → (i : Nat) < n := by grind
|
||||
theorem castSucc_inj {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b := by grind
|
||||
|
||||
example (n : Nat) : rev (last n) = 0 := by grind
|
||||
theorem castSucc_eq_zero_iff [NeZero n] {a : Fin n} : a.castSucc = 0 ↔ a = 0 := by grind
|
||||
|
||||
example (n : Nat) : rev 0 = last n := by grind
|
||||
theorem castSucc_ne_zero_iff [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0 := by grind
|
||||
|
||||
example {n : Nat} : (2 : Fin (n + 3)).val = 2 := by grind
|
||||
example {n : Nat} : (17 : Fin (n + 18)).val = 17 := by grind
|
||||
theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by grind
|
||||
|
||||
example : (0 : Fin (n + 2)) < 1 := by grind
|
||||
theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n := by grind
|
||||
|
||||
example (j : Fin n) : (j.succ : Nat) = j + 1 := by grind
|
||||
|
||||
example (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by grind
|
||||
|
||||
example {a b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b := by grind
|
||||
|
||||
example {a b : Fin n} : a.succ < b.succ ↔ a < b := by grind
|
||||
|
||||
example {a b : Fin n} : a.succ = b.succ ↔ a = b := by grind
|
||||
|
||||
example {n} : ∀ k : Fin n, Fin.succ k ≠ 0 := by grind
|
||||
|
||||
example {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _ := by grind
|
||||
|
||||
example {n : Nat} : ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last _ := by grind
|
||||
|
||||
example {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n := by grind
|
||||
|
||||
example {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n := by grind
|
||||
|
||||
example (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := by grind
|
||||
|
||||
example (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ := by grind
|
||||
|
||||
example (i n m : Nat) (hn : i < n) (h : n ≤ m) :
|
||||
castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := by grind
|
||||
|
||||
example {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by grind
|
||||
|
||||
example {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
|
||||
castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by grind
|
||||
|
||||
example {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
|
||||
Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i := by grind
|
||||
|
||||
example {k m n} (km : k ≤ m) (mn : m ≤ n) :
|
||||
Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) := by grind
|
||||
|
||||
example (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := by grind
|
||||
|
||||
example {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
|
||||
Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) := by grind
|
||||
|
||||
example {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
|
||||
Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) := by grind
|
||||
|
||||
example [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := by grind
|
||||
|
||||
example {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h = last n' := by grind
|
||||
|
||||
example (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := by grind
|
||||
|
||||
example (n : Nat) (h : n = n) : Fin.cast h = id := by grind
|
||||
|
||||
example {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := by grind
|
||||
|
||||
example (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := by grind
|
||||
|
||||
example : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := by grind
|
||||
|
||||
example {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m := by grind
|
||||
|
||||
example (m : Nat) (i : Nat) (h : i < n) :
|
||||
castAdd m ⟨i, h⟩ = ⟨i, Nat.lt_add_right m h⟩ := by grind
|
||||
|
||||
example (m : Nat) (i : Fin (n + m)) (hi : i.val < n) :
|
||||
castAdd m (castLT i hi) = i := by grind
|
||||
|
||||
example (m : Nat) (i : Fin n) :
|
||||
castLT (castAdd m i) (castAdd_lt m i) = i := by grind
|
||||
|
||||
example {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
|
||||
castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := by grind
|
||||
|
||||
example {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
|
||||
(i.castAdd m).cast h = (i.cast (Nat.add_right_cancel h)).castAdd m := by grind
|
||||
|
||||
example {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
|
||||
(i.castAdd m').cast h = i.castAdd m := by grind
|
||||
|
||||
example {m n p : Nat} (i : Fin m) :
|
||||
(i.castAdd n).castAdd p = (i.castAdd (n + p)).cast (Nat.add_assoc ..).symm := by grind
|
||||
|
||||
example {n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :
|
||||
i.succ.cast h = (i.cast (Nat.succ.inj h)).succ := by grind
|
||||
|
||||
example {n' : Nat} (i : Fin n) (h : n = n') :
|
||||
(i.cast h).succ = i.succ.cast (by rw [h]) := by grind
|
||||
|
||||
example (i : Fin n) : (i.castSucc : Nat) = i := by grind
|
||||
|
||||
example (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt.step h⟩ := by grind
|
||||
|
||||
example {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
|
||||
i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := by grind
|
||||
|
||||
example (i : Fin n) : i.castSucc < i.succ := by grind
|
||||
|
||||
example {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by grind
|
||||
|
||||
example {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
|
||||
i.castSucc < j ↔ i.succ ≤ j := by grind
|
||||
|
||||
example (n : Nat) : (last n).succ = last n.succ := by grind
|
||||
|
||||
example {n : Nat} {i : Fin n.succ} :
|
||||
i.succ = last (n + 1) ↔ i = last n := by grind
|
||||
|
||||
example (i : Fin (n + 1)) (h : (i : Nat) < n) :
|
||||
(castLT i h).castSucc = i := by grind
|
||||
|
||||
example {n : Nat} (a : Fin n) (h : (a : Nat) < n) :
|
||||
castLT a.castSucc h = a := by grind
|
||||
|
||||
example {a b : Fin n} :
|
||||
a.castSucc < b.castSucc ↔ a < b := by grind
|
||||
|
||||
example {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b := by grind
|
||||
|
||||
example (a : Fin n) : a.castSucc < last n := by grind
|
||||
|
||||
example [NeZero n] : castSucc (0 : Fin n) = 0 := by grind
|
||||
|
||||
example {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := by grind
|
||||
|
||||
example [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc := by grind
|
||||
|
||||
example [NeZero n] {a : Fin n} : a.castSucc = 0 ↔ a = 0 := by grind
|
||||
|
||||
example [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0 := by grind
|
||||
|
||||
example {a : Fin n} : a.castSucc + 1 = a.succ := by grind
|
||||
|
||||
example {a : Fin n} : a.castSucc < a.succ := by grind
|
||||
|
||||
example {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n := by grind
|
||||
|
||||
example (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := by grind
|
||||
|
||||
example (n : Nat) (i : Fin n) : addNat i 0 = i := by grind
|
||||
|
||||
example {i : Fin n} : addNat i 1 = i.succ := by grind
|
||||
|
||||
example (m : Nat) (i : Fin n) : m ≤ addNat i m := by grind
|
||||
|
||||
example (n i : Nat) (hi : i < m) :
|
||||
addNat ⟨i, hi⟩ n = ⟨i + n, Nat.add_lt_add_right hi n⟩ := by grind
|
||||
|
||||
example {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
|
||||
(addNat i 0).cast h = i.cast ((Nat.add_zero _).symm.trans h) := by grind
|
||||
|
||||
example {n n' m : Nat} (i : Fin n') (h : n' = n) :
|
||||
addNat (i.cast h) m = (addNat i m).cast (congrArg (. + m) h) := by grind
|
||||
|
||||
example {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
|
||||
(addNat i m).cast h = addNat (i.cast (Nat.add_right_cancel h)) m := by grind
|
||||
|
||||
example {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
|
||||
(addNat i m').cast h = addNat i m := by grind
|
||||
|
||||
example (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := by grind
|
||||
|
||||
example (n i : Nat) (hi : i < m) :
|
||||
natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := by grind
|
||||
|
||||
example (m : Nat) (i : Fin n) : m ≤ natAdd m i := by grind
|
||||
|
||||
example {n : Nat} : natAdd 0 = Fin.cast (Nat.zero_add n).symm := by grind
|
||||
|
||||
example {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
|
||||
natAdd m (i.cast h) = (natAdd m i).cast (congrArg _ h) := by grind
|
||||
|
||||
example {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
|
||||
(natAdd m i).cast h = natAdd m (i.cast (Nat.add_left_cancel h)) := by grind
|
||||
|
||||
example {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
|
||||
(natAdd m' i).cast h = natAdd m i := by grind
|
||||
|
||||
example (p m : Nat) {n : Nat} (i : Fin n) :
|
||||
castAdd p (natAdd m i) = (natAdd m (castAdd p i)).cast (Nat.add_assoc ..).symm := by grind
|
||||
|
||||
example (p m : Nat) {n : Nat} (i : Fin n) :
|
||||
natAdd m (castAdd p i) = (castAdd p (natAdd m i)).cast (Nat.add_assoc ..) := by grind
|
||||
|
||||
example (m n : Nat) {p : Nat} (i : Fin p) :
|
||||
natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) := by grind
|
||||
|
||||
example {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
|
||||
(natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := by grind
|
||||
|
||||
example (n : Nat) {m : Nat} (i : Fin m) :
|
||||
(natAdd n i).cast (Nat.add_comm ..) = addNat i n := by grind
|
||||
|
||||
example {n : Nat} (m : Nat) (i : Fin n) :
|
||||
(addNat i m).cast (Nat.add_comm ..) = natAdd m i := by grind
|
||||
|
||||
example {m n : Nat} : natAdd n (last m) = last (n + m) := by grind
|
||||
|
||||
example (n : Nat) :
|
||||
addNat (last n) m = (last (n + m)).cast (by grind) := by grind
|
||||
|
||||
example (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n := by grind
|
||||
|
||||
example (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := by grind
|
||||
|
||||
example (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by grind
|
||||
|
||||
example (k : Fin n) : rev (castSucc k) = succ (rev k) := by grind
|
||||
|
||||
example (k : Fin n) : rev (succ k) = castSucc (rev k) := by grind
|
||||
|
||||
example (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := by grind
|
||||
|
||||
example : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i := by grind
|
||||
|
||||
example (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by grind
|
||||
|
||||
example {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} :
|
||||
i.pred hi = j ↔ i = j.succ := by grind
|
||||
|
||||
example (i : Nat) (h : i < n + 1) :
|
||||
Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
|
||||
⟨i, h⟩ := by grind
|
||||
|
||||
example (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
|
||||
Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := by grind
|
||||
|
||||
example {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w =
|
||||
⟨i - 1, Nat.sub_lt_right_of_lt_add (Nat.pos_iff_ne_zero.2 (Fin.val_ne_of_ne w)) h⟩ := by grind
|
||||
|
||||
example {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
|
||||
a.pred ha ≤ b.pred hb ↔ a ≤ b := by grind
|
||||
|
||||
example {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
|
||||
a.pred ha < b.pred hb ↔ a < b := by grind
|
||||
|
||||
example :
|
||||
∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b := by grind
|
||||
|
||||
example {n : Nat} :
|
||||
Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := by grind
|
||||
|
||||
example (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
|
||||
theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
|
||||
pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by grind
|
||||
|
||||
example (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := by grind
|
||||
|
||||
example {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
|
||||
subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := by grind
|
||||
|
||||
example (i : Fin n) (h : 0 ≤ (i : Nat)): Fin.subNat 0 i h = i := by grind
|
||||
|
||||
example (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by grind
|
||||
|
||||
example (i : Fin n) :
|
||||
pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := by grind
|
||||
|
||||
example {i : Fin (n + m)} (h : m ≤ i) : addNat (subNat m i h) m = i := by grind
|
||||
|
||||
example (i : Fin n) (m : Nat) (h : m ≤ addNat i m := le_coe_addNat m i) :
|
||||
subNat m (addNat i m) h = i := by grind
|
||||
|
||||
example {i : Fin (n + m)} (h : n ≤ i) :
|
||||
natAdd n (subNat n (i.cast (Nat.add_comm ..)) h) = i := by grind
|
||||
|
||||
/-! ### Recursion and induction principles -/
|
||||
|
||||
example {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
|
||||
@Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by grind
|
||||
|
||||
example {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
|
||||
@Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by grind
|
||||
|
||||
example {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
(hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
|
||||
(induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := by grind
|
||||
|
||||
example {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
(succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
|
||||
induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := by grind
|
||||
|
||||
example {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
@Fin.cases n motive zero succ 0 = zero := by grind
|
||||
|
||||
example {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
|
||||
@Fin.cases n motive zero succ i.succ = succ i := by grind
|
||||
|
||||
example {n} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
{i : Nat} (h : i + 1 < n + 1) :
|
||||
@Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := by grind
|
||||
|
||||
example {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P 0 ∧ ∀ i : Fin n, P i.succ := by grind
|
||||
|
||||
example {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨ ∃ i : Fin n, P i.succ := by grind
|
||||
|
||||
example {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 := by grind
|
||||
|
||||
example {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 := by grind
|
||||
|
||||
example {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 := by grind
|
||||
|
||||
example {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 := by grind
|
||||
|
||||
example {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
(reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by grind
|
||||
|
||||
example {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
(i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
|
||||
succ i (reverseInduction zero succ i.succ) := by grind
|
||||
|
||||
example {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
|
||||
(Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last := by grind
|
||||
|
||||
example {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
|
||||
(i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i := by grind
|
||||
|
||||
example {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
|
||||
addCases (motive := motive) left right (Fin.castAdd n i) = left i := by grind
|
||||
|
||||
example {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
|
||||
addCases (motive := motive) left right (natAdd m i) = right i := by grind
|
||||
|
||||
example [NeZero n] {a : Fin n} : a.val = 0 ↔ a = 0 := by grind
|
||||
|
||||
example [NeZero n] {a : Fin n} : a.val ≠ 0 ↔ a ≠ 0 := by grind
|
||||
|
||||
example [NeZero n] (x : Nat) (y : Fin n) :
|
||||
theorem ofNat_add [NeZero n] (x : Nat) (y : Fin n) :
|
||||
Fin.ofNat n x + y = Fin.ofNat n (x + y.val) := by grind
|
||||
|
||||
example [NeZero n] (x : Fin n) (y : Nat) :
|
||||
theorem add_ofNat [NeZero n] (x : Fin n) (y : Nat) :
|
||||
x + Fin.ofNat n y = Fin.ofNat n (x.val + y) := by grind
|
||||
|
||||
|
||||
example (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by grind
|
||||
|
||||
example [NeZero n] (x : Nat) (y : Fin n) :
|
||||
theorem ofNat_sub [NeZero n] (x : Nat) (y : Fin n) :
|
||||
Fin.ofNat n x - y = Fin.ofNat n ((n - y.val) + x) := by grind
|
||||
|
||||
example [NeZero n] (x : Fin n) (y : Nat) :
|
||||
x - Fin.ofNat n y = Fin.ofNat n ((n - y % n) + x.val) := by grind
|
||||
|
||||
example {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
|
||||
private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
|
||||
x % n = x - n := by grind
|
||||
|
||||
example {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by grind
|
||||
theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by grind
|
||||
|
||||
example {a b : Fin n} : b ≤ a → (a - b).val = a.val - b.val := by grind
|
||||
theorem sub_val_of_le {a b : Fin n} : b ≤ a → (a - b).val = a.val - b.val := by grind
|
||||
|
||||
example {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by grind
|
||||
theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by grind
|
||||
|
||||
/-! ### neg -/
|
||||
theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by grind [Fin.val_add]
|
||||
|
||||
example {n : Nat} [NeZero n] (x : Fin n) :
|
||||
(-x).val = if x = 0 then 0 else n - x.val := by grind
|
||||
|
||||
example {n : Nat} (x y : Fin n) : x - y = x + -y := by grind
|
||||
|
||||
/-! ### mul -/
|
||||
|
||||
example [NeZero n] (x : Nat) (y : Fin n) :
|
||||
theorem ofNat_mul [NeZero n] (x : Nat) (y : Fin n) :
|
||||
Fin.ofNat n x * y = Fin.ofNat n (x * y.val) := by grind
|
||||
|
||||
example [NeZero n] (x : Fin n) (y : Nat) :
|
||||
theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
|
||||
x * Fin.ofNat n y = Fin.ofNat n (x.val * y) := by grind
|
||||
|
||||
/-! Shouldn't expect to work by `grind`: -/
|
||||
|
||||
theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) := by grind
|
||||
|
||||
theorem eq_zero_or_eq_succ {n : Nat} : ∀ i : Fin (n + 1), i = 0 ∨ ∃ j : Fin n, i = j.succ := by grind
|
||||
|
||||
theorem eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ j : Fin n, i = j.succ := by grind
|
||||
|
||||
theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by grind
|
||||
|
||||
instance subsingleton_zero : Subsingleton (Fin 0) := by grind
|
||||
|
||||
instance subsingleton_one : Subsingleton (Fin 1) := by grind
|
||||
|
||||
theorem forall_fin_succ {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P 0 ∧ ∀ i : Fin n, P i.succ := by grind
|
||||
|
||||
theorem exists_fin_succ {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨ ∃ i : Fin n, P i.succ := by grind
|
||||
|
||||
theorem forall_fin_zero {p : Fin 0 → Prop} : (∀ i, p i) ↔ True := by grind
|
||||
|
||||
theorem exists_fin_zero {p : Fin 0 → Prop} : (∃ i, p i) ↔ False := by grind
|
||||
|
||||
theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 := by grind
|
||||
|
||||
theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 := by grind
|
||||
|
||||
theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 := by grind
|
||||
|
||||
theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 := by grind
|
||||
|
||||
end Fin'
|
||||
|
|
|
|||
|
|
@ -83,6 +83,11 @@ example (a : Fin 2) : a ≠ 0 → a ≠ 1 → False := by
|
|||
/--
|
||||
trace: [grind.lia.model] a := 2
|
||||
[grind.lia.model] b := 0
|
||||
[grind.lia.model] ↑a := 2
|
||||
[grind.lia.model] ↑b := 0
|
||||
[grind.lia.model] ↑0 := 0
|
||||
[grind.lia.model] ↑1 := 1
|
||||
[grind.lia.model] ↑(a + b) := 2
|
||||
-/
|
||||
#guard_msgs (drop error, trace) in
|
||||
set_option trace.grind.lia.model true in
|
||||
|
|
@ -90,7 +95,10 @@ example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → Fa
|
|||
grind
|
||||
|
||||
-- We use `↑a` when pretty printing `ToInt.toInt a`
|
||||
/-- trace: [grind.debug.ring.basis] ↑a + ↑b + -1 * ((↑a + ↑b) % 3) + -3 * ((↑a + ↑b) / 3) = 0 -/
|
||||
/--
|
||||
trace: [grind.debug.ring.basis] ↑a + ↑b + -1 * ((↑a + ↑b) % 3) + -3 * ((↑a + ↑b) / 3) = 0
|
||||
[grind.debug.ring.basis] b = 0
|
||||
-/
|
||||
#guard_msgs (drop error, trace) in
|
||||
set_option trace.grind.debug.ring.basis true in
|
||||
example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → False := by
|
||||
|
|
|
|||
|
|
@ -48,46 +48,555 @@ example (i : Fin (n + 1)) : i.1 ≤ n := by grind
|
|||
|
||||
example {x y : Fin n} : x = y ↔ x ≤ y ∧ y ≤ x := by grind
|
||||
|
||||
example : (Fin.last 0 : Fin 1) = 0 := by grind
|
||||
|
||||
example (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := by grind
|
||||
|
||||
example {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
|
||||
(i.cast h).cast h' = i.cast (Eq.trans h h') := by grind
|
||||
|
||||
example (n : Nat) (j : Fin n) :
|
||||
j.succ.castSucc = (j.castSucc).succ := by grind
|
||||
|
||||
example {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := by grind
|
||||
|
||||
example {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) := by grind
|
||||
|
||||
example (i : Fin n) : i.succ.castSucc = i.castSucc.succ := by grind
|
||||
|
||||
example (h : n ≤ n) (i : Fin n) : i.castLE h = i := by grind
|
||||
|
||||
example (h : n ≤ m) (i : Fin n) :
|
||||
(i.castLE h).castSucc = i.castLE (by omega) := by grind
|
||||
|
||||
example (n : Nat) (i : Fin k) :
|
||||
(i.natAdd n).castSucc = (i.castSucc).natAdd n := by grind
|
||||
|
||||
example : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by grind
|
||||
|
||||
example [NeZero n] {x : Fin n} : x - x = 0 := by grind
|
||||
|
||||
example {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n := by grind
|
||||
|
||||
example {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n := by grind
|
||||
|
||||
example [i : NeZero n] (k : Fin n) : k * 1 = k := by grind
|
||||
open Std Fin
|
||||
|
||||
example (a b : Fin n) : a * b = b * a := by grind
|
||||
namespace Fin'
|
||||
|
||||
example (a b c : Fin n) : a * b * c = a * (b * c) := by grind
|
||||
theorem is_lt (a : Fin n) : (a : Nat) < n := by grind
|
||||
|
||||
example [NeZero n] (k : Fin n) : (1 : Fin n) * k = k := by grind
|
||||
/-! ### coercions and constructions -/
|
||||
|
||||
example [NeZero n] (k : Fin n) : k * 0 = 0 := by grind
|
||||
theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := by grind
|
||||
|
||||
example [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by grind
|
||||
theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := by grind
|
||||
|
||||
theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := by grind
|
||||
|
||||
theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩ := by grind [cases Fin]
|
||||
|
||||
theorem mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
|
||||
(⟨a, ha⟩ : Fin n) = ⟨b, hb⟩ ↔ a = b := by grind
|
||||
|
||||
theorem val_mk {m n : Nat} (h : m < n) : (⟨m, h⟩ : Fin n).val = m := by grind
|
||||
|
||||
theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := by grind
|
||||
|
||||
theorem val_ofNat (n : Nat) [NeZero n] (a : Nat) :
|
||||
(Fin.ofNat n a).val = a % n := by grind
|
||||
|
||||
theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val := by grind
|
||||
|
||||
theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val := by grind
|
||||
|
||||
theorem val_eq_zero (a : Fin 1) : a.val = 0 := by grind
|
||||
|
||||
theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
|
||||
(if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by grind
|
||||
|
||||
theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
|
||||
(if c then x else y).val = if c then x.val else y.val := by grind
|
||||
|
||||
open IntCast in
|
||||
theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
|
||||
(x : Fin n) = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs := by grind [Fin.intCast_def]
|
||||
|
||||
/-! ### order -/
|
||||
|
||||
theorem le_def {a b : Fin n} : a ≤ b ↔ a.1 ≤ b.1 := by grind
|
||||
|
||||
theorem lt_def {a b : Fin n} : a < b ↔ a.1 < b.1 := by grind
|
||||
|
||||
theorem not_le {a b : Fin n} : ¬ a ≤ b ↔ b < a := by grind
|
||||
|
||||
theorem not_lt {a b : Fin n} : ¬ a < b ↔ b ≤ a := by grind
|
||||
|
||||
theorem le_refl (a : Fin n) : a ≤ a := by grind
|
||||
|
||||
theorem lt_irrefl (a : Fin n) : ¬ a < a := by grind
|
||||
|
||||
theorem le_trans {a b c : Fin n} : a ≤ b → b ≤ c → a ≤ c := by grind
|
||||
|
||||
theorem lt_trans {a b c : Fin n} : a < b → b < c → a < c := by grind
|
||||
|
||||
theorem le_total (a b : Fin n) : a ≤ b ∨ b ≤ a := by grind
|
||||
|
||||
theorem lt_asymm {a b : Fin n} (h : a < b) : ¬ b < a := by grind
|
||||
|
||||
theorem ne_of_lt {a b : Fin n} (h : a < b) : a ≠ b := by grind
|
||||
|
||||
theorem ne_of_gt {a b : Fin n} (h : a < b) : b ≠ a := by grind
|
||||
|
||||
theorem le_of_lt {a b : Fin n} (h : a < b) : a ≤ b := by grind
|
||||
|
||||
theorem lt_of_le_of_lt {a b c : Fin n} : a ≤ b → b < c → a < c := by grind
|
||||
|
||||
theorem lt_of_lt_of_le {a b c : Fin n} : a < b → b ≤ c → a < c := by grind
|
||||
|
||||
theorem le_rfl {a : Fin n} : a ≤ a := by grind
|
||||
|
||||
theorem lt_iff_le_and_ne {a b : Fin n} : a < b ↔ a ≤ b ∧ a ≠ b := by grind
|
||||
|
||||
theorem lt_or_lt_of_ne {a b : Fin n} (h : a ≠ b) : a < b ∨ b < a := by grind
|
||||
|
||||
theorem lt_or_le (a b : Fin n) : a < b ∨ b ≤ a := by grind
|
||||
|
||||
theorem le_or_lt (a b : Fin n) : a ≤ b ∨ b < a := by grind
|
||||
|
||||
theorem le_of_eq {a b : Fin n} (hab : a = b) : a ≤ b := by grind
|
||||
|
||||
theorem ge_of_eq {a b : Fin n} (hab : a = b) : b ≤ a := by grind
|
||||
|
||||
theorem eq_or_lt_of_le {a b : Fin n} : a ≤ b → a = b ∨ a < b := by grind
|
||||
|
||||
theorem lt_or_eq_of_le {a b : Fin n} : a ≤ b → a < b ∨ a = b := by grind
|
||||
|
||||
theorem is_le (i : Fin (n + 1)) : i.1 ≤ n := by grind
|
||||
|
||||
theorem is_le' {a : Fin n} : a ≤ n := by grind
|
||||
|
||||
theorem le_antisymm_iff {x y : Fin n} : x = y ↔ x ≤ y ∧ y ≤ x := by grind
|
||||
|
||||
theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := by grind
|
||||
|
||||
theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := by grind
|
||||
|
||||
theorem rev_rev (i : Fin n) : rev (rev i) = i := by grind
|
||||
|
||||
theorem rev_le_rev {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by grind
|
||||
|
||||
theorem rev_inj {i j : Fin n} : rev i = rev j ↔ i = j := by grind
|
||||
|
||||
theorem rev_lt_rev {i j : Fin n} : rev i < rev j ↔ j < i := by grind
|
||||
|
||||
theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by grind
|
||||
|
||||
theorem fin_one_eq_zero (a : Fin 1) : a = 0 := by grind
|
||||
|
||||
theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := by grind
|
||||
|
||||
theorem zero_add [NeZero n] (k : Fin n) : (0 : Fin n) + k = k := by grind
|
||||
|
||||
theorem add_zero [NeZero n] (k : Fin n) : k + 0 = k := by grind
|
||||
|
||||
theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := by grind
|
||||
|
||||
theorem cast_cast {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
|
||||
(i.cast h).cast h' = i.cast (Eq.trans h h') := by grind
|
||||
|
||||
theorem castLE_refl (h : n ≤ n) (i : Fin n) : i.castLE h = i := by grind
|
||||
|
||||
theorem castSucc_castLE (h : n ≤ m) (i : Fin n) :
|
||||
(i.castLE h).castSucc = i.castLE (by omega) := by grind
|
||||
|
||||
theorem castSucc_natAdd (n : Nat) (i : Fin k) :
|
||||
(i.natAdd n).castSucc = (i.castSucc).natAdd n := by grind
|
||||
|
||||
theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := by grind
|
||||
|
||||
theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) := by grind
|
||||
|
||||
theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by grind
|
||||
|
||||
theorem sub_self [NeZero n] {x : Fin n} : x - x = 0 := by grind
|
||||
|
||||
theorem mul_one [i : NeZero n] (k : Fin n) : k * 1 = k := by grind
|
||||
|
||||
theorem mul_comm (a b : Fin n) : a * b = b * a := by grind
|
||||
|
||||
theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by grind
|
||||
|
||||
theorem one_mul [NeZero n] (k : Fin n) : (1 : Fin n) * k = k := by grind
|
||||
|
||||
theorem mul_zero [NeZero n] (k : Fin n) : k * 0 = 0 := by grind
|
||||
|
||||
theorem zero_mul [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by grind
|
||||
|
||||
theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := by grind
|
||||
|
||||
theorem mod_def (a m : Fin n) :
|
||||
a % m = Fin.mk (a.val % m.val) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) := by grind
|
||||
|
||||
theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ a.pos) := by grind
|
||||
|
||||
theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b.val) + a.val) % n) (Nat.mod_lt _ a.pos) := by grind
|
||||
|
||||
theorem pos' [Nonempty (Fin n)] : 0 < n := by grind
|
||||
|
||||
theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
|
||||
a = ⟨k, hk⟩ ↔ (a : Nat) = k := by grind
|
||||
|
||||
theorem ofNat_self {n : Nat} [NeZero n] : Fin.ofNat n n = 0 := by grind
|
||||
|
||||
theorem ofNat_val_eq_self [NeZero n] (x : Fin n) : (Fin.ofNat n x.val) = x := by
|
||||
-- mod_eq_of_lt might be plausible for the implication gadget?
|
||||
grind [Nat.mod_eq_of_lt]
|
||||
|
||||
theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b := by grind
|
||||
|
||||
theorem mk_lt_of_lt_val {b : Fin n} {a : Nat} (h : a < b) :
|
||||
(⟨a, Nat.lt_trans h b.is_lt⟩ : Fin n) < b := by grind
|
||||
|
||||
theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
|
||||
(⟨a, Nat.lt_of_le_of_lt h b.is_lt⟩ : Fin n) ≤ b := by grind
|
||||
|
||||
theorem mk_le_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) ≤ ⟨y, hy⟩ ↔ x ≤ y := by grind
|
||||
|
||||
theorem mk_lt_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) < ⟨y, hy⟩ ↔ x < y := by grind
|
||||
|
||||
theorem val_last (n : Nat) : (last n).1 = n := by grind
|
||||
|
||||
theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.pos) := by grind
|
||||
|
||||
theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := by grind
|
||||
|
||||
theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ := by grind
|
||||
|
||||
theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
|
||||
castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := by grind
|
||||
|
||||
theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
|
||||
Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i := by grind
|
||||
|
||||
theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
|
||||
Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) := by grind
|
||||
|
||||
theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := by grind
|
||||
|
||||
theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
|
||||
Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) := by grind
|
||||
|
||||
theorem cast_castLT {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
|
||||
Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) := by grind
|
||||
|
||||
theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := by grind
|
||||
|
||||
theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := by grind
|
||||
|
||||
theorem cast_refl (n : Nat) (h : n = n) : Fin.cast h = id := by grind
|
||||
|
||||
theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := by grind
|
||||
|
||||
theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := by grind
|
||||
|
||||
theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m := by grind
|
||||
|
||||
theorem castLT_castAdd (m : Nat) (i : Fin n) :
|
||||
castLT (castAdd m i) (castAdd_lt m i) = i := by grind
|
||||
|
||||
theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := by grind
|
||||
|
||||
theorem succ_last (n : Nat) : (last n).succ = last n.succ := by grind
|
||||
|
||||
theorem succ_eq_last_succ {n : Nat} {i : Fin n.succ} :
|
||||
i.succ = last (n + 1) ↔ i = last n := by grind
|
||||
|
||||
theorem castLT_castSucc {n : Nat} (a : Fin n) (h : (a : Nat) < n) :
|
||||
castLT a.castSucc h = a := by grind
|
||||
|
||||
theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := by grind
|
||||
|
||||
theorem le_coe_addNat (m : Nat) (i : Fin n) : m ≤ addNat i m := by grind
|
||||
|
||||
theorem cast_addNat_zero {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
|
||||
(addNat i 0).cast h = i.cast ((Nat.add_zero _).symm.trans h) := by grind
|
||||
|
||||
theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := by grind
|
||||
|
||||
theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := by grind
|
||||
|
||||
theorem pred_succ (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by grind
|
||||
|
||||
theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
|
||||
(natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := by grind
|
||||
|
||||
theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w =
|
||||
⟨i - 1, Nat.sub_lt_right_of_lt_add (Nat.pos_iff_ne_zero.2 (Fin.val_ne_of_ne w)) h⟩ := by grind
|
||||
|
||||
theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := by grind
|
||||
|
||||
theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
|
||||
subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := by grind
|
||||
|
||||
theorem subNat_zero (i : Fin n) (h : 0 ≤ (i : Nat)): Fin.subNat 0 i h = i := by grind
|
||||
|
||||
theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by grind
|
||||
|
||||
theorem pred_castSucc_succ (i : Fin n) :
|
||||
pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := by grind
|
||||
|
||||
theorem subNat_addNat (i : Fin n) (m : Nat) (h : m ≤ addNat i m := le_coe_addNat m i) :
|
||||
subNat m (addNat i m) h = i := by grind
|
||||
|
||||
theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
|
||||
@Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by grind
|
||||
|
||||
theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
|
||||
@Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by grind
|
||||
|
||||
theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
(hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
|
||||
(induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := by grind
|
||||
|
||||
theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
|
||||
(succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
|
||||
induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := by grind
|
||||
|
||||
theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
@Fin.cases n motive zero succ 0 = zero := by grind
|
||||
|
||||
theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
|
||||
@Fin.cases n motive zero succ i.succ = succ i := by grind
|
||||
|
||||
theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
{i : Nat} (h : i + 1 < n + 1) :
|
||||
@Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := by grind
|
||||
|
||||
theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
|
||||
(reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by grind
|
||||
|
||||
theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
|
||||
(i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
|
||||
succ i (reverseInduction zero succ i.succ) := by grind
|
||||
|
||||
theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
|
||||
(Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last := by grind
|
||||
|
||||
theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
|
||||
(i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i := by grind
|
||||
|
||||
theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
|
||||
addCases (motive := motive) left right (Fin.castAdd n i) = left i := by grind
|
||||
|
||||
theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
|
||||
addCases (motive := motive) left right (natAdd m i) = right i := by grind
|
||||
|
||||
theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
|
||||
(-x).val = if x = 0 then 0 else n - x.val := by grind
|
||||
|
||||
theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by grind
|
||||
|
||||
theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
|
||||
| ⟨_, _⟩, ⟨_, _⟩ => by grind
|
||||
|
||||
theorem le_last (i : Fin (n + 1)) : i ≤ last n := by grind
|
||||
|
||||
theorem eq_last_of_not_lt {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n := by grind
|
||||
|
||||
theorem val_lt_last {i : Fin (n + 1)} : i ≠ last n → (i : Nat) < n := by grind
|
||||
|
||||
theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := by grind
|
||||
|
||||
theorem succ_le_succ_iff {a b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b := by grind
|
||||
|
||||
theorem succ_lt_succ_iff {a b : Fin n} : a.succ < b.succ ↔ a < b := by grind
|
||||
|
||||
theorem succ_inj {a b : Fin n} : a.succ = b.succ ↔ a = b := by grind
|
||||
|
||||
theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := by grind
|
||||
|
||||
theorem le_coe_natAdd (m : Nat) (i : Fin n) : m ≤ natAdd m i := by grind
|
||||
|
||||
theorem last_le_iff {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n := by grind
|
||||
|
||||
-- From this point onwards we need `@[grind ext]` on `Fin.ext`.
|
||||
|
||||
|
||||
theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
|
||||
rev i = ⟨a, Nat.lt_succ_of_le (h ▸ Nat.le_add_right ..)⟩ := by grind
|
||||
|
||||
theorem castLE_succ {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
|
||||
castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by grind
|
||||
|
||||
theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h = last n' := by grind
|
||||
|
||||
theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := by grind
|
||||
|
||||
theorem castAdd_mk (m : Nat) (i : Nat) (h : i < n) :
|
||||
castAdd m ⟨i, h⟩ = ⟨i, Nat.lt_add_right m h⟩ := by grind
|
||||
|
||||
theorem castAdd_castLT (m : Nat) (i : Fin (n + m)) (hi : i.val < n) :
|
||||
castAdd m (castLT i hi) = i := by grind
|
||||
|
||||
theorem castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
|
||||
castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := by grind
|
||||
|
||||
theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
|
||||
(i.castAdd m).cast h = (i.cast (Nat.add_right_cancel h)).castAdd m := by grind
|
||||
|
||||
theorem cast_castAdd_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
|
||||
(i.castAdd m').cast h = i.castAdd m := by grind
|
||||
|
||||
theorem castAdd_castAdd {m n p : Nat} (i : Fin m) :
|
||||
(i.castAdd n).castAdd p = (i.castAdd (n + p)).cast (Nat.add_assoc ..).symm := by grind
|
||||
|
||||
theorem cast_succ_eq {n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :
|
||||
i.succ.cast h = (i.cast (Nat.succ.inj h)).succ := by grind
|
||||
|
||||
theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
|
||||
(i.cast h).succ = i.succ.cast (by rw [h]) := by grind
|
||||
|
||||
theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt_succ_of_lt h⟩ := by grind
|
||||
|
||||
theorem cast_castSucc {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
|
||||
i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := by grind
|
||||
|
||||
theorem castSucc_castLT (i : Fin (n + 1)) (h : (i : Nat) < n) :
|
||||
(castLT i h).castSucc = i := by grind
|
||||
|
||||
theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by grind
|
||||
|
||||
theorem addNat_one {i : Fin n} : addNat i 1 = i.succ := by grind
|
||||
|
||||
theorem addNat_mk (n i : Nat) (hi : i < m) :
|
||||
addNat ⟨i, hi⟩ n = ⟨i + n, Nat.add_lt_add_right hi n⟩ := by grind
|
||||
|
||||
theorem addNat_cast {n n' m : Nat} (i : Fin n') (h : n' = n) :
|
||||
addNat (i.cast h) m = (addNat i m).cast (congrArg (. + m) h) := by grind
|
||||
|
||||
theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
|
||||
(addNat i m).cast h = addNat (i.cast (Nat.add_right_cancel h)) m := by grind
|
||||
|
||||
theorem cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
|
||||
(addNat i m').cast h = addNat i m := by grind
|
||||
|
||||
theorem natAdd_mk (n i : Nat) (hi : i < m) :
|
||||
natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := by grind
|
||||
|
||||
theorem natAdd_zero {n : Nat} : natAdd 0 = Fin.cast (Nat.zero_add n).symm := by grind
|
||||
|
||||
theorem natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
|
||||
natAdd m (i.cast h) = (natAdd m i).cast (congrArg _ h) := by grind
|
||||
|
||||
theorem cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
|
||||
(natAdd m i).cast h = natAdd m (i.cast (Nat.add_left_cancel h)) := by grind
|
||||
|
||||
theorem cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
|
||||
(natAdd m' i).cast h = natAdd m i := by grind
|
||||
|
||||
theorem castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
|
||||
castAdd p (natAdd m i) = (natAdd m (castAdd p i)).cast (Nat.add_assoc ..).symm := by grind
|
||||
|
||||
theorem natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
|
||||
natAdd m (castAdd p i) = (castAdd p (natAdd m i)).cast (Nat.add_assoc ..) := by grind
|
||||
|
||||
theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
|
||||
natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) := by grind
|
||||
|
||||
theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
|
||||
(natAdd n i).cast (Nat.add_comm ..) = addNat i n := by grind
|
||||
|
||||
theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
|
||||
(addNat i m).cast (Nat.add_comm ..) = natAdd m i := by grind
|
||||
|
||||
theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := by grind
|
||||
|
||||
theorem addNat_last (n : Nat) :
|
||||
addNat (last n) m = (last (n + m)).cast (by omega) := by grind
|
||||
|
||||
theorem natAdd_eq_addNat (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n := by grind
|
||||
|
||||
theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := by grind
|
||||
|
||||
theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by grind
|
||||
|
||||
theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := by grind
|
||||
|
||||
theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
|
||||
Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
|
||||
⟨i, h⟩ := by grind
|
||||
|
||||
theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
|
||||
Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := by grind
|
||||
theorem addNat_subNat {i : Fin (n + m)} (h : m ≤ i) : addNat (subNat m i h) m = i := by grind
|
||||
|
||||
theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
|
||||
natAdd n (subNat n (i.cast (Nat.add_comm ..)) h) = i := by grind
|
||||
|
||||
theorem sub_ofNat [NeZero n] (x : Fin n) (y : Nat) :
|
||||
x - Fin.ofNat n y = Fin.ofNat n ((n - y % n) + x.val) := by grind
|
||||
|
||||
theorem succ_mk (n i : Nat) (h : i < n) :
|
||||
Fin.succ ⟨i, h⟩ = ⟨i + 1, Nat.succ_lt_succ h⟩ := by grind
|
||||
|
||||
/-! These could work, but need additional help from `grind`, because these annotations are bad: -/
|
||||
attribute [grind =] Fin.val_zero Fin.val_one Fin.le_def Fin.lt_def
|
||||
|
||||
theorem val_zero (n : Nat) [NeZero n] : ((0 : Fin n) : Nat) = 0 := by grind
|
||||
|
||||
theorem mk_zero : (⟨0, Nat.succ_pos n⟩ : Fin (n + 1)) = 0 := by grind
|
||||
|
||||
theorem zero_le [NeZero n] (a : Fin n) : 0 ≤ a := by grind
|
||||
|
||||
theorem zero_lt_one : (0 : Fin (n + 2)) < 1 := by grind
|
||||
|
||||
theorem not_lt_zero [NeZero n] (a : Fin n) : ¬a < 0 := by grind
|
||||
|
||||
theorem pos_iff_ne_zero [NeZero n] {a : Fin n} : 0 < a ↔ a ≠ 0 := by grind
|
||||
|
||||
theorem zero_eq_last_iff {n : Nat} : (0 : Fin (n + 1)) = last n ↔ n = 0 := by grind
|
||||
|
||||
theorem last_eq_zero_iff {n : Nat} : Fin.last n = 0 ↔ n = 0 := by grind
|
||||
|
||||
theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := by grind
|
||||
|
||||
theorem rev_last (n : Nat) : rev (last n) = 0 := by grind
|
||||
|
||||
theorem rev_zero (n : Nat) : rev 0 = last n := by grind
|
||||
|
||||
theorem val_one (n : Nat) : (1 : Fin (n + 2)).val = 1 := by grind
|
||||
|
||||
theorem mk_one : (⟨1, Nat.succ_lt_succ (Nat.succ_pos n)⟩ : Fin (n + 2)) = (1 : Fin _) := by grind
|
||||
|
||||
theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by grind
|
||||
|
||||
theorem succ_ne_zero {n} : ∀ k : Fin n, Fin.succ k ≠ 0 := by grind
|
||||
|
||||
theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := by grind
|
||||
|
||||
theorem mk_succ_pos (i : Nat) (h : i < n) :
|
||||
(0 : Fin (n + 1)) < ⟨i.succ, Nat.add_lt_add_right h 1⟩ := by grind
|
||||
|
||||
theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by grind
|
||||
|
||||
theorem le_zero_iff {n : Nat} {k : Fin (n + 1)} : k ≤ 0 ↔ k = 0 := by grind
|
||||
|
||||
theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 := by grind
|
||||
|
||||
theorem castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by grind
|
||||
|
||||
theorem castSucc_lt_succ {i : Fin n} : i.castSucc < i.succ := by grind
|
||||
|
||||
theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by grind
|
||||
|
||||
theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
|
||||
i.castSucc < j ↔ i.succ ≤ j := by grind
|
||||
|
||||
theorem castSucc_lt_castSucc_iff {a b : Fin n} :
|
||||
a.castSucc < b.castSucc ↔ a < b := by grind
|
||||
|
||||
theorem castSucc_lt_last (a : Fin n) : a.castSucc < last n := by grind
|
||||
|
||||
theorem castSucc_zero [NeZero n] : castSucc (0 : Fin n) = 0 := by grind
|
||||
|
||||
theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := by grind
|
||||
|
||||
theorem castSucc_pos [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc := by grind
|
||||
|
||||
theorem castSucc_succ (i : Fin n) : i.succ.castSucc = i.castSucc.succ := by grind
|
||||
|
||||
theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i := by grind
|
||||
|
||||
theorem pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} :
|
||||
i.pred hi = j ↔ i = j.succ := by grind
|
||||
|
||||
theorem pred_le_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
|
||||
a.pred ha ≤ b.pred hb ↔ a ≤ b := by grind
|
||||
|
||||
theorem pred_lt_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
|
||||
a.pred ha < b.pred hb ↔ a < b := by grind
|
||||
|
||||
theorem pred_inj :
|
||||
∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b := by grind
|
||||
|
||||
theorem pred_one {n : Nat} :
|
||||
Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt zero_lt_one)) = 0 := by grind
|
||||
|
||||
theorem val_eq_zero_iff [NeZero n] {a : Fin n} : a.val = 0 ↔ a = 0 := by grind
|
||||
|
||||
theorem val_ne_zero_iff [NeZero n] {a : Fin n} : a.val ≠ 0 ↔ a ≠ 0 := by grind
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue