First contribution to mathlib

Stream: new members

[Sven Manthe]

I have some lemmas and functions for lists I'd like to commit to Mathlib. Would you like to have a look at them before I make a pull request? (Background: I'm formalizing Borel Determinacy, and decided to commit some prerequisites to Mathlib before I finish. Until now, I just made some two line commits.)

First some general lemmas:

import Mathlib.Tactic
theorem List.ext' {x y : List α} (h : x.length ≤ y.length)
  (h' : ∀ n<y.length, x.get? n = y.get? n) : x = y := by
  apply List.ext; intro n; rcases Nat.lt_or_ge n y.length with hn | hn
  exact h' _ hn; simp[List.get?_eq_none.mpr hn, le_trans h hn]
theorem List.prefix_concat_iff {x y : List α} {a : α}: x <+: y ++ [a] ↔ x <+: y ∨ x = y ++ [a] := by
  constructor
  { intro ⟨z, h⟩; induction' z using List.reverseRecOn with z
    right; rw[List.append_nil] at h; exact h
    left; rw[← List.append_assoc] at h; use z; exact List.append_inj_left' h rfl }
  rintro (h | rfl); exact List.IsPrefix.trans h (List.prefix_append _ _); exact List.prefix_rfl
theorem List.prefix_take_iff {x y : List α} {n : ℕ}: x <+: y.take n ↔ x <+: y ∧ x.length ≤ n := by
  constructor
  { intro h; constructor
    exact List.IsPrefix.trans h (List.take_prefix _ _)
    replace h := h.length_le; simp at h; exact h.left }
  { intro ⟨hp, hl⟩; have hl' := hp.length_le; rw[List.prefix_iff_eq_take] at *
    rw[hp, List.take_take]; simp[hl, hl'] }
@[simp] theorem List.append_left_cancel_nil_left {x y : List α}: x ++ y = x ↔ y = [] := by
  constructor <;> intro h; apply List.append_cancel_left (as := x); all_goals simp[h]
@[simp] theorem List.append_left_cancel_nil_right {x y : List α}: x = x ++ y ↔ y = [] :=
  by rw[eq_comm, append_left_cancel_nil_left]
example (x y z : List α) (h : x ++ y ++ z = x) : y = [] := by simp at h; tauto
@[simp] theorem List.head_tail (x : List α) (h : x ≠ []) : (x.head h) :: x.tail = x := by
  cases x <;> simp; simp at h
theorem List.ne_nil_prefix {x y : List α} (hx : x ≠ []) (h : x <+: y) : y ≠ [] := by
  rintro rfl; apply hx; exact List.prefix_nil.mp h
theorem List.get_eq_prefix {x y : List α} {n} (hn : n < x.length) (h : x <+: y) :
  List.get x ⟨n, hn⟩ = List.get y ⟨n, by linarith[h.length_le]⟩ := by
  obtain ⟨_, rfl⟩ := h; symm; apply List.get_append
theorem List.head_eq_prefix {x y : List α} (hx : x ≠ []) (h : x <+: y) :
  x.head hx = y.head (ne_nil_prefix hx h) := by
    cases x <;> cases y <;> simp at *; simp at hx
    all_goals {obtain ⟨_, h⟩ := h; injection h}
@[simp] theorem List.head_replicate {n} {a : α} (h : List.replicate n a ≠ []) :
  List.head _ h = a := by
  cases n <;> simp at *; exfalso; exact h rfl
theorem List.get?_append_or_none (x y : List α) n :
  x.get? n = (x ++ y).get? n ∨ x.get? n = none := by
  rcases lt_or_ge n x.length with h | h
  rw[List.get?_append h]; tauto
  simp; tauto
theorem List.concat_prefix_of_length_lt {x y : List α} (h : x <+: y) (hl : x.length < y.length) :
  x ++ [y.get ⟨x.length, hl⟩] <+: y := by
  use y.drop (x.length + 1); dsimp; nth_rw 1[List.prefix_iff_eq_take.mp h]
  convert List.take_append_drop (x.length + 1) y using 2
  rw[← List.take_concat_get, List.concat_eq_append]; rfl

Furthermore, List.zip and List.zipWith only support a finite number of arguments. Here is the obvious generalization:

import Mathlib.Tactic
abbrev eval (a : α) {β: α → Type*} (f : ∀ a, β a) := f a
abbrev List.mapEval {α: Type*} {β: α → Type*} (a : α) (x : List (∀ a, β a)) := x.map (eval a)
def zipFun {α: Type*} {β: α → Type*} {n : ℕ} (f : (a : α) → List (β a))
  (h : ∀ a, (f a).length = n) :
   List ((a : α) → β a) := match n with
  | 0 => []
  | n + 1 => (fun a ↦ (f a).head (List.ne_nil_of_length_eq_succ (h a)))
    :: zipFun (fun a ↦ (f a).tail) ((by simp[h]) : ∀ a, List.length _ = n)
@[simp] theorem List.mapEval_zip {β: α → Type*} (f : (a : α) → List (β a)) (h : ∀ a, (f a).length = n) :
 (zipFun f h).mapEval a = f a := by
  revert f; induction' n with n ih
  intro f h; specialize h a; simp[List.length_eq_zero] at h; simp[zipFun, h]
  intro f h; specialize ih (fun a ↦ (f a).tail) (by intro a; simp[h a]); specialize h a
  dsimp at ih; simp[zipFun, ih]
@[simp] theorem List.zip_mapEval {β: α → Type*} (x : List ((a : α) → β a)) :
  zipFun x.mapEval (n := x.length) (by simp) = x := by
  induction' x with a x ih; rfl
  dsimp at ih; simp[zipFun, ih]
theorem List.mapEval_joint_epi {β: α → Type*} {x y : List (∀ a, β a)} (hl : x.length = y.length)
  (h : ∀ a, x.mapEval a = y.mapEval a) : x = y := by
  rw[← zip_mapEval x, ← zip_mapEval y]; congr 1; ext1; apply h
@[simp] theorem List.zipFun_len {β: α → Type*} (f : (a : α) → List (β a)) (h : ∀ a, (f a).length = n) :
  (zipFun f h).length = n := by
  revert f; induction' n with _ ih <;> simp[zipFun]
  intro _ _; apply ih
@[simp] theorem List.zipFun_zero {β: α → Type*} (f : (a : α) → List (β a)) (h : ∀ a, (f a).length = 0) :
  zipFun f h = [] := by apply List.eq_nil_of_length_eq_zero; simp
@[simp] theorem List.zipFun_append {β: α → Type*} (f g : (a : α) → List (β a))
  (hf : ∀ a, (f a).length = m) (hg : ∀ a, (g a).length = n) :
  zipFun f hf ++ zipFun g hg = zipFun (n := m + n) (fun a ↦ f a ++ g a) (by simp[hf, hg]) := by
  revert f; induction' m with m ih <;> intro f hf
  simp[List.eq_nil_of_length_eq_zero (hf _)]
  specialize ih (fun a ↦ (f a).tail) (by simp[hf])
  simp[zipFun, Nat.succ_add]
  have hf' : ∀ a, f a ≠ [] := by intro a h; specialize hf a; simp[h] at hf
  constructor
  { ext a; apply Option.some_injective; simp_rw[← List.head?_eq_head]; symm
    apply List.head?_append_of_ne_nil _ (hf' a) }
  rw[ih]; congr; ext1 a; symm; apply List.tail_append_of_ne_nil _ _ (hf' a)
theorem List.zipFun_mono {β: α → Type*} (f g : (a : α) → List (β a))
  (hf : ∀ a, (f a).length = m) (hg : ∀ a, (g a).length = n) (hm : m ≤ n) (h : ∀ a, f a <+: g a) :
  zipFun f hf <+: zipFun g hg := by
  use zipFun (n := n-m) (fun a ↦ List.drop m (g a)) (by simp[hg])
  simp; congr; simp[hm]; ext1 a; nth_rw 2[← List.take_append_drop m (g a)]
  congr; rw[← hf a]; apply List.prefix_iff_eq_take.mp (h a)

[Yaël Dillies]

Your List.ext' almost already exists

[Yaël Dillies]

It's basically docs#List.nthLe

[Yaël Dillies]

I think you should make a pull request. It's much easier to give you feedback through the GitHub interface

[Sven Manthe]

Are you sure your link is correct? List.nthLe seems to be just a copy of the function List.get, but my List.ext' is kind of an extensionality lemma

[Yaël Dillies]

Sorry, I meant docs#List.ext_nthLe

[Sven Manthe]

As suggested, I will open a pull request. Can you suggest where to add these? Maybe the definition of zip in Data.List.Basic and the remainder in Data.List.Lemmas?

[Yaël Dillies]

Something like that, yeah

[Sven Manthe]

Oh, I'm aware of both docs#List.ext and docs#List.ext_get (=List.ext_nthLe), but my version is somehow intermediate between both of them

[Yaël Dillies]

Your version should be called List.ext_get? I guess?

[Sven Manthe]

Maybe. But maybe docs#List.ext should be called List.ext_get?, and my version should have an even longer name

[Yaël Dillies]

At this point, it's up to you

[Sven Manthe]

Would it be a good idea to rename List.ext? Since there are many extensionality lemmas for lists, the name doesn't seem nice, but then backward compatibility may be preferable...

[Yaël Dillies]

Yes, it would be good, but note that it's in Std, not mathlib

[Sven Manthe]

Thanks, I didn't notice that. My results should probably still be added to mathlib and not just to Std (e.g., they could have mathlib dependencies)? And in this case one maybe just should create an alias List.ext_get? of List.ext

[Yaël Dillies]

Sure, that's one way to proceed

[Sven Manthe]

For reference: I added a pull request for the first part (https://github.com/leanprover-community/mathlib4/pull/11626)