forall₂ nth_le

Stream: Is there code for X?

[Martin Dvořák]

MWE:

private lemma forall₂_nth_le {α β : Type*}
  {x : list α} {y : list β} {R : α → β → Prop} {i : ℕ}
  (i_lt_len_x : i < x.length) (i_lt_len_y : i < y.length)
  (ass : list.forall₂ R x y) :
  R (x.nth_le i i_lt_len_x) (y.nth_le i i_lt_len_y) :=
begin
  sorry,
end

[Eric Wieser]

I don't think docs#list.forall₂ has much API

[Martin Dvořák]

Do you think it is a lemma that I should prove and then add to mathlib?

[Eric Wieser]

Can you state it as an iff and prove that instead?

[Patrick Johnson]

Either i_lt_len_x or i_lt_len_y is redundant, since forall₂ implies x.length = y.length

example {α β : Type*} {x : list α} {y : list β} {R : α → β → Prop} :
  list.forall₂ R x y ↔ ∀ i h₁, ∃ h₂, R (x.nth_le i h₁) (y.nth_le i h₂) :=
begin
  sorry
end

[Martin Dvořák]

I'll give it a try on Monday. Thanks for the suggestion!

[Eric Wieser]

The exists in that statement is probably sufficient justification to have the original non-iff version too, since I imagine it's more convenient for the forwards direction

[Martin Dvořák]

Patrick Johnson said:

Either i_lt_len_x or i_lt_len_y is redundant, since forall₂ implies x.length = y.length

example {α β : Type*} {x : list α} {y : list β} {R : α → β → Prop} :
  list.forall₂ R x y ↔ ∀ i h₁, ∃ h₂, R (x.nth_le i h₁) (y.nth_le i h₂) :=
begin
  sorry
end

I don't think the formulation is correct.

[Martin Dvořák]

Counterexample:

example {α β : Type} {R : α → β → Prop} (b : β) : ¬ (∀ x : list α, ∀ y : list β,
  (∀ i h₁, ∃ h₂, R (x.nth_le i h₁) (y.nth_le i h₂)) → list.forall₂ R x y) :=
begin
  push_neg,
  use [[], [b]],
  split,
  {
    intros i imposs,
    exfalso,
    rw list.length at imposs,
    exact nat.not_lt_zero i imposs,
  },
  {
    finish,
  },
end

[Yaël Dillies]

Yeah, the → works, but not ←

[Martin Dvořák]

Do you have a preference on how the statement of the theorem should be changed?
https://github.com/leanprover-community/mathlib/blob/21a7cf2220dd6167b3c077eb2c04e9db4538dc67/src/data/list/forall2.lean#L159

[Patrick Johnson]

Why not state it exactly as the docstring says?

forall₂ R l₁ l₂ means that l₁ and l₂ have the same length, and whenever a is the nth element of l₁, and b is the nth element of l₂, then R a b is satisfied.

Statement:

lemma list.forall₂_iff' {α β : Type*}
  {R : α → β → Prop} {l₁ : list α} {l₂ : list β} :
  list.forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧
  ∀ i h₁ h₂, R (l₁.nth_le i h₁) (l₂.nth_le i h₂) :=
begin
  sorry
end

[Martin Dvořák]

PR: https://github.com/leanprover-community/mathlib/pull/16073

[Eric Wieser]

Can you split out all the variable renaming to its own PR?

[Eric Wieser]

Or maybe, just make a PR that adds the new lemma; it's not clear to me whether the renaming is a net improvement

[Martin Dvořák]

I thought it would be OK to do it together. Patrick Johnson wanted me to rename r to R, so I wanted to include the change before PRing it, and it didn't look good when I renamed r to R only in my theorem.

[Patrick Johnson]

Patrick Johnson wanted me to rename r to R

The snippet I posted is just an example. I'm not insisting on anything.

[Martin Dvořák]

OK, sorry.

[Martin Dvořák]

I suggest we first discuss whether we want r or R to be used throughout the file. Should I create a new thread for it, possibly in the "PR reviews" stream? If you agree on R in the end, I will strongly prefer to continue with reviewing the single PR as it is.

[Yaël Dillies]

I think we care more about not overediting files than variable name consistency.

[Eric Wieser]

It's best not to mix high-effort, highly-opinionated, low-value changes (ie renaming everything) with simpler high-value changes (like your new lemmas)

[Eric Wieser]

Because then everyone argues about the stuff that didn't need to change in the first place, and your new lemma ends up unecessarily being held hostage by the rest of the PR

[Martin Dvořák]

Should I revert the changes of the variable names and keep this PR on? Or should I create a new branch in the mathlib repository, copypaste the new lemmata to it (losing the edit history), and PR from there?

[Eric Wieser]

I'd just revert the variable name changes; you can always recover them from the history later if you want to suggest appling them in a subsequent PR.

[Eric Wieser]

Here's a much shorter proof for the forwards direction:

theorem forall₂.nth_le :
  ∀ {x : list α} {y : list β} (h : forall₂ R x y) {i : ℕ} (hx : i < x.length) (hy : i < y.length),
    R (x.nth_le i hx) (y.nth_le i hy)
| (a₁ :: l₁) (a₂ :: l₂) (forall₂.cons ha hl) 0        hx hy := ha
| (a₁ :: l₁) (a₂ :: l₂) (forall₂.cons ha hl) (succ i) hx hy := hl.nth_le _ _