Skip to content

Commit

Permalink
refactor(data/fin): drop fin.cast_add_right (#9371)
Browse files Browse the repository at this point in the history 
This was a duplicate of `fin.nat_add`. Also simplify some definitions of equivalences.
  • Loading branch information
@urkud
urkud committed Sep 27, 2021
1 parent 850784c commit 9a30f8c
Show file tree
Hide file tree
Showing 2 changed files with 200 additions and 220 deletions.
149 changes: 46 additions & 103 deletions src/data/equiv/fin.lean
View file
Expand Up @@ -44,7 +44,7 @@ def fin_two_equiv : fin 2 ≃ bool :=

/-- The 'identity' equivalence between `fin n` and `fin m` when `n = m`. -/
def fin_congr {n m : ℕ} (h : n = m) : fin n ≃ fin m :=
equiv.subtype_equiv_right (λ x, by subst h)
(fin.cast h).to_equiv

@[simp] lemma fin_congr_apply_mk {n m : ℕ} (h : n = m) (k : ℕ) (w : k < n) :
fin_congr h ⟨k, w⟩ = ⟨k, by { subst h, exact w }⟩ :=
Expand All @@ -66,64 +66,40 @@ This is a version of `fin.pred_above` that produces `option (fin n)` instead of
mapping both `i.cast_succ` and `i.succ` to `i`. -/
def fin_succ_equiv' {n : ℕ} (i : fin (n + 1)) :
fin (n + 1) ≃ option (fin n) :=
have hx0 : ∀ {i x : fin (n + 1)}, i < x → x ≠ 0,
from λ i x hix, ne_of_gt (lt_of_le_of_lt i.zero_le hix),
have hiltx : ∀ {i x : fin (n + 1)}, ¬ i < x → ¬ x = i → x < i,
from λ i x hix hxi, lt_of_le_of_ne (le_of_not_lt hix) hxi,
have hxltn : ∀ {i x : fin (n + 1)}, ¬ i < x → ¬ x = i → (x : ℕ) < n,
from λ i x hix hxi, lt_of_lt_of_le (hiltx hix hxi) (nat.le_of_lt_succ i.2),
{ to_fun := λ x,
if hix : i < x
then some (x.pred (hx0 hix))
else if hxi : x = i
then none
else some (x.cast_lt (hxltn hix hxi)),
{ to_fun := i.insert_nth none some,
inv_fun := λ x, x.cases_on' i (fin.succ_above i),
left_inv := λ x,
if hix : i < x
then
have hi : i ≤ fin.cast_succ (x.pred (hx0 hix)),
by { simp only [fin.le_iff_coe_le_coe, fin.coe_cast_succ, fin.coe_pred],
exact nat.le_pred_of_lt hix },
by simp [dif_pos hix, option.cases_on'_some, fin.succ_above_above _ _ hi, fin.succ_pred]
else if hxi : x = i
then by simp [hxi]
else have hi : fin.cast_succ (x.cast_lt (hxltn hix hxi)) < i,
from lt_of_le_of_ne (le_of_not_gt hix) (by simp [hxi]),
by simp only [dif_neg hix, dif_neg hxi, option.cases_on'_some, fin.succ_above_below _ _ hi,
fin.cast_succ_cast_lt],
right_inv := λ x, by {
cases x,
{ simp },
{ dsimp,
split_ifs,
{ simp [fin.succ_above_above _ _ ((fin.lt_succ_above_iff _ _).1 h)] },
{ simpa [fin.succ_above_ne] using h_1 },
{ have : fin.cast_succ x < i,
{ rwa [fin.lt_succ_above_iff, not_le] at h },
simp [fin.succ_above_below _ _ this] } } } }
left_inv := λ x, fin.succ_above_cases i (by simp) (λ j, by simp) x,
right_inv := λ x, by cases x; dsimp; simp }

@[simp] lemma fin_succ_equiv'_at {n : ℕ} (i : fin (n + 1)) :
(fin_succ_equiv' i) i = none := by simp [fin_succ_equiv']

@[simp] lemma fin_succ_equiv'_succ_above {n : ℕ} (i : fin (n + 1)) (j : fin n) :
fin_succ_equiv' i (i.succ_above j) = some j :=
@fin.insert_nth_apply_succ_above n (λ _, option (fin n)) i _ _ _

lemma fin_succ_equiv'_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
(fin_succ_equiv' i) m.cast_succ = some m :=
by simp [fin_succ_equiv', dif_neg (not_lt_of_gt h), ne_of_lt h]
by rw [← fin.succ_above_below _ _ h, fin_succ_equiv'_succ_above]

lemma fin_succ_equiv'_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
(fin_succ_equiv' i) m.succ = some m :=
by simp [fin_succ_equiv', fin.le_cast_succ_iff, *] at *
by rw [← fin.succ_above_above _ _ h, fin_succ_equiv'_succ_above]

@[simp] lemma fin_succ_equiv'_symm_none {n : ℕ} (i : fin (n + 1)) :
(fin_succ_equiv' i).symm none = i := rfl

@[simp] lemma fin_succ_equiv'_symm_some {n : ℕ} (i : fin (n + 1)) (j : fin n) :
(fin_succ_equiv' i).symm (some j) = i.succ_above j :=
rfl

lemma fin_succ_equiv'_symm_some_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
(fin_succ_equiv' i).symm (some m) = m.cast_succ :=
by simp [fin_succ_equiv', ne_of_gt h, fin.succ_above, not_le_of_gt h]
fin.succ_above_below i m h

lemma fin_succ_equiv'_symm_some_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
(fin_succ_equiv' i).symm (some m) = m.succ :=
by simp [fin_succ_equiv', fin.succ_above, h.not_lt]
fin.succ_above_above i m h

lemma fin_succ_equiv'_symm_coe_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
(fin_succ_equiv' i).symm m = m.cast_succ :=
Expand All @@ -145,21 +121,15 @@ by cases n; refl

@[simp] lemma fin_succ_equiv_succ {n : ℕ} (m : fin n):
(fin_succ_equiv n) m.succ = some m :=
begin
cases n, { exact m.elim0 },
rw [fin_succ_equiv, fin_succ_equiv'_above (fin.zero_le _)],
end
fin_succ_equiv'_above (fin.zero_le _)

@[simp] lemma fin_succ_equiv_symm_none {n : ℕ} :
(fin_succ_equiv n).symm none = 0 :=
by cases n; refl
fin_succ_equiv'_symm_none _

@[simp] lemma fin_succ_equiv_symm_some {n : ℕ} (m : fin n) :
(fin_succ_equiv n).symm (some m) = m.succ :=
begin
cases n, { exact m.elim0 },
rw [fin_succ_equiv, fin_succ_equiv'_symm_some_above (fin.zero_le _)],
end
congr_fun fin.succ_above_zero m

@[simp] lemma fin_succ_equiv_symm_coe {n : ℕ} (m : fin n) :
(fin_succ_equiv n).symm m = m.succ :=
Expand Down Expand Up @@ -195,76 +165,49 @@ fin_succ_equiv'_symm_none _

/-- Equivalence between `fin m ⊕ fin n` and `fin (m + n)` -/
def fin_sum_fin_equiv : fin m ⊕ fin n ≃ fin (m + n) :=
{ to_fun := λ x, sum.rec_on x
(λ y, ⟨y.1, nat.lt_of_lt_of_le y.2 $ nat.le_add_right m n⟩)
(λ y, ⟨m + y.1, nat.add_lt_add_left y.2 m⟩),
inv_fun := λ x, if H : x.1 < m
then sum.inl ⟨x.1, H⟩
else sum.inr ⟨x.1 - m, nat.lt_of_add_lt_add_left $
show m + (x.1 - m) < m + n,
from (nat.add_sub_of_le $ le_of_not_gt H).symm ▸ x.2⟩,
left_inv := λ x, begin
cases x with y y,
{ simp [fin.ext_iff, y.is_lt], },
{ have H : ¬m + y.val < m := not_lt_of_ge (nat.le_add_right _ _),
simp [H, nat.add_sub_cancel_left, fin.ext_iff] }
end,
right_inv := λ x, begin
by_cases H : (x:ℕ) < m,
{ dsimp, rw [dif_pos H], simp },
{ dsimp, rw [dif_neg H], simp [fin.ext_iff, nat.add_sub_of_le (le_of_not_gt H)] }
end }
{ to_fun := sum.elim (fin.cast_add n) (fin.nat_add m),
inv_fun := λ i, @fin.add_cases m n (λ _, fin m ⊕ fin n) sum.inl sum.inr i,
left_inv := λ x, by { cases x with y y; dsimp; simp },
right_inv := λ x, by refine fin.add_cases (λ i, _) (λ i, _) x; simp }

@[simp] lemma fin_sum_fin_equiv_apply_left (i : fin m) :
(fin_sum_fin_equiv (sum.inl i) : fin (m + n)) = fin.cast_add n i := rfl

@[simp] lemma fin_sum_fin_equiv_apply_right (i : fin n) :
(fin_sum_fin_equiv (sum.inr i) : fin (m + n)) = fin.cast_add_right m i := rfl
(fin_sum_fin_equiv (sum.inr i) : fin (m + n)) = fin.nat_add m i := rfl

@[simp] lemma fin_sum_fin_equiv_symm_apply_left (x : fin (m + n)) (h : ↑x < m) :
fin_sum_fin_equiv.symm x = sum.inl ⟨x.1, h⟩ :=
by simp [fin_sum_fin_equiv, dif_pos h]
@[simp] lemma fin_sum_fin_equiv_symm_apply_cast_add (x : fin m) :
fin_sum_fin_equiv.symm (fin.cast_add n x) = sum.inl x :=
fin_sum_fin_equiv.symm_apply_apply (sum.inl x)

@[simp] lemma fin_sum_fin_equiv_symm_apply_right (x : fin (m + n)) (h : m ≤ ↑x) :
fin_sum_fin_equiv.symm x = sum.inr ⟨x.1 - m, nat.lt_of_add_lt_add_left $
show m + (x.1 - m) < m + n, from (nat.add_sub_of_le $ h).symm ▸ x.2⟩ :=
by simp [fin_sum_fin_equiv, dif_neg (not_lt.mpr h)]

@[simp] lemma fin_sum_fin_equiv_symm_apply_cast_add {m n : ℕ} (i : fin m) :
fin_sum_fin_equiv.symm (fin.cast_add n i) = sum.inl i :=
begin
rw [fin_sum_fin_equiv_symm_apply_left _ (fin.cast_add_lt _ _)],
simp
end

@[simp] lemma fin_sum_fin_equiv_symm_apply_cast_add_right {m n : ℕ} (i : fin m) :
fin_sum_fin_equiv.symm (fin.cast_add_right n i) = sum.inr i :=
begin
rw [fin_sum_fin_equiv_symm_apply_right _ (fin.le_cast_add_right _ _)],
simp
end
@[simp] lemma fin_sum_fin_equiv_symm_apply_nat_add (x : fin n) :
fin_sum_fin_equiv.symm (fin.nat_add m x) = sum.inr x :=
fin_sum_fin_equiv.symm_apply_apply (sum.inr x)

/-- The equivalence between `fin (m + n)` and `fin (n + m)` which rotates by `n`. -/
def fin_add_flip : fin (m + n) ≃ fin (n + m) :=
(fin_sum_fin_equiv.symm.trans (equiv.sum_comm _ _)).trans fin_sum_fin_equiv

@[simp] lemma fin_add_flip_apply_left {k : ℕ} (h : k < m)
@[simp] lemma fin_add_flip_apply_cast_add (k : fin m) (n : ℕ) :
fin_add_flip (fin.cast_add n k) = fin.nat_add n k :=
by simp [fin_add_flip]

@[simp] lemma fin_add_flip_apply_nat_add (k : fin n) (m : ℕ) :
fin_add_flip (fin.nat_add m k) = fin.cast_add m k :=
by simp [fin_add_flip]

@[simp] lemma fin_add_flip_apply_mk_left {k : ℕ} (h : k < m)
(hk : k < m + n := nat.lt_add_right k m n h)
(hnk : n + k < n + m := add_lt_add_left h n) :
fin_add_flip (⟨k, hk⟩ : fin (m + n)) = ⟨n + k, hnk⟩ :=
begin
dsimp [fin_add_flip, fin_sum_fin_equiv],
rw [dif_pos h],
refl,
end
by convert fin_add_flip_apply_cast_add ⟨k, h⟩ n

@[simp] lemma fin_add_flip_apply_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
fin_add_flip (⟨k, h₂⟩ : fin (m + n)) =
⟨k - m, lt_of_le_of_lt (nat.sub_le _ _) (by { convert h₂ using 1, simp [add_comm] })⟩ :=
@[simp] lemma fin_add_flip_apply_mk_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
fin_add_flip (⟨k, h₂⟩ : fin (m + n)) = ⟨k - m, sub_le_self'.trans_lt $ add_comm m n ▸ h₂⟩ :=
begin
dsimp [fin_add_flip, fin_sum_fin_equiv],
rw [dif_neg (not_lt.mpr h₁)],
refl,
convert fin_add_flip_apply_nat_add ⟨k - m, (sub_lt_iff_right h₁).2 _⟩ m,
{ simp [nat.add_sub_cancel' h₁] },
{ rwa add_comm }
end

/-- Rotate `fin n` one step to the right. -/
Expand All @@ -282,7 +225,7 @@ end
lemma fin_rotate_last' : fin_rotate (n+1) ⟨n, lt_add_one _⟩ = ⟨0, nat.zero_lt_succ _⟩ :=
begin
dsimp [fin_rotate],
rw fin_add_flip_apply_right,
rw fin_add_flip_apply_mk_right,
simp,
end

Expand Down

0 comments on commit 9a30f8c

Please sign in to comment.