feat(data/fin/tuple/basic): injectivity of fin.cons x xs (#17779)

Author: eric-wieser

src/data/fin/tuple/basic.lean

@@ -120,19 +120,58 @@ end
 
 /-- Recurse on an `n+1`-tuple by splitting it into a single element and an `n`-tuple. -/
 @[elab_as_eliminator]
-def cons_induction {P : (Π i : fin n.succ, α i) → Sort v}
+def cons_cases {P : (Π i : fin n.succ, α i) → Sort v}
   (h : ∀ x₀ x, P (fin.cons x₀ x)) (x : (Π i : fin n.succ, α i)) : P x :=
 _root_.cast (by rw cons_self_tail) $ h (x 0) (tail x)
 
-@[simp] lemma cons_induction_cons {P : (Π i : fin n.succ, α i) → Sort v}
+@[simp] lemma cons_cases_cons {P : (Π i : fin n.succ, α i) → Sort v}
   (h : Π x₀ x, P (fin.cons x₀ x)) (x₀ : α 0) (x : Π i : fin n, α i.succ) :
-  @cons_induction _ _ _ h (cons x₀ x) = h x₀ x :=
+  @cons_cases _ _ _ h (cons x₀ x) = h x₀ x :=
 begin
-  rw [cons_induction, cast_eq],
+  rw [cons_cases, cast_eq],
   congr',
   exact tail_cons _ _
 end
 
+/-- Recurse on an tuple by splitting into `fin.elim0` and `fin.cons`. -/
+@[elab_as_eliminator]
+def cons_induction {α : Type*} {P : Π {n : ℕ}, (fin n → α) → Sort v}
+  (h0 : P fin.elim0)
+  (h : ∀ {n} x₀ (x : fin n → α), P x → P (fin.cons x₀ x)) : Π {n : ℕ} (x : fin n → α), P x
+| 0 x := by convert h0
+| (n + 1) x := cons_cases (λ x₀ x, h _ _ $ cons_induction _) x
+
+lemma cons_injective_of_injective {α} {x₀ : α} {x : fin n → α} (hx₀ : x₀ ∉ set.range x)
+  (hx : function.injective x) :
+  function.injective (cons x₀ x : fin n.succ → α) :=
+begin
+  refine fin.cases _ _,
+  { refine fin.cases _ _,
+    { intro _,
+      refl },
+    { intros j h,
+      rw [cons_zero, cons_succ] at h,
+      exact hx₀.elim ⟨_, h.symm⟩ } },
+  { intro i,
+    refine fin.cases _ _,
+    { intro h,
+      rw [cons_zero, cons_succ] at h,
+      exact hx₀.elim ⟨_, h⟩ },
+    { intros j h,
+      rw [cons_succ, cons_succ] at h,
+      exact congr_arg _ (hx h), } },
+end
+
+lemma cons_injective_iff {α} {x₀ : α} {x : fin n → α} :
+  function.injective (cons x₀ x : fin n.succ → α) ↔ x₀ ∉ set.range x ∧ function.injective x  :=
+begin
+  refine ⟨λ h, ⟨_, _⟩, and.rec cons_injective_of_injective⟩,
+  { rintros ⟨i, hi⟩,
+    replace h := @h i.succ 0,
+    simpa [hi, succ_ne_zero] using h, },
+  { simpa [function.comp] using h.comp (fin.succ_injective _) },
+end
+
 @[simp] lemma forall_fin_zero_pi {α : fin 0 → Sort*} {P : (Π i, α i) → Prop} :
   (∀ x, P x) ↔ P fin_zero_elim :=
 ⟨λ h, h _, λ h x, subsingleton.elim fin_zero_elim x ▸ h⟩
@@ -143,7 +182,7 @@ end
 
 lemma forall_fin_succ_pi {P : (Π i, α i) → Prop} :
   (∀ x, P x) ↔ (∀ a v, P (fin.cons a v)) :=
-⟨λ h a v, h (fin.cons a v), cons_induction⟩
+⟨λ h a v, h (fin.cons a v), cons_cases⟩
 
 lemma exists_fin_succ_pi {P : (Π i, α i) → Prop} :
   (∃ x, P x) ↔ (∃ a v, P (fin.cons a v)) :=

src/data/fin/tuple/nat_antidiagonal.lean

@@ -68,16 +68,17 @@ def antidiagonal_tuple : Π k, ℕ → list (fin k → ℕ)
 lemma mem_antidiagonal_tuple {n : ℕ} {k : ℕ} {x : fin k → ℕ} :
   x ∈ antidiagonal_tuple k n ↔ ∑ i, x i = n :=
 begin
-  induction k with k ih generalizing n,
-  { cases n,
+  revert n,
+  refine fin.cons_induction _ _ x,
+  { intro n,
+    cases n,
     { simp },
-    { simp [eq_comm] }, },
-  { refine fin.cons_induction (λ x₀ x, _) x,
+    { simp [eq_comm] } },
+  { intros k x₀ x ih n,
     simp_rw [fin.sum_cons, antidiagonal_tuple, list.mem_bind, list.mem_map,
-      list.nat.mem_antidiagonal, fin.cons_eq_cons, exists_eq_right_right, ih, prod.exists],
-    split,
-    { rintros ⟨a, b, rfl, rfl, rfl⟩, refl },
-    { rintro rfl, exact ⟨_, _, rfl, rfl, rfl⟩, } },
+      list.nat.mem_antidiagonal, fin.cons_eq_cons, exists_eq_right_right, ih,
+      @eq_comm _ _ (prod.snd _), and_comm (prod.snd _ = _), ←prod.mk.inj_iff, prod.mk.eta,
+      exists_prop, exists_eq_right] },
 end
 
 /-- The antidiagonal of `n` does not contain duplicate entries. -/

src/data/list/range.lean

@@ -301,8 +301,21 @@ theorem of_fn_eq_map {α n} {f : fin n → α} :
   of_fn f = (fin_range n).map f :=
 by rw [← of_fn_id, map_of_fn, function.right_id]
 
-theorem nodup_of_fn {α n} {f : fin n → α} (hf : function.injective f) :
+theorem nodup_of_fn_of_injective {α n} {f : fin n → α} (hf : function.injective f) :
   nodup (of_fn f) :=
 by { rw of_fn_eq_pmap, exact (nodup_range n).pmap (λ _ _ _ _ H, fin.veq_of_eq $ hf H) }
 
+theorem nodup_of_fn {α n} {f : fin n → α} :
+  nodup (of_fn f) ↔ function.injective f :=
+begin
+  refine ⟨_, nodup_of_fn_of_injective⟩,
+  refine fin.cons_induction _ (λ n x₀ xs ih, _) f,
+  { intro h,
+    exact function.injective_of_subsingleton _ },
+  { intro h,
+    rw fin.cons_injective_iff,
+    simp_rw [of_fn_succ, fin.cons_succ, nodup_cons, fin.cons_zero, mem_of_fn] at h,
+    exact h.imp_right ih }
+end
+
 end list