feat: lemmas characterising zipWith(All) via get?

[semorrison]

No description provided.

[joehendrix]

Will the match need to generate variable names if this is a simp rule? We could avoid it with something like the following:

theorem zipWith_get? {f : α → β → γ} :
    (List.zipWith f as bs).get? i =
        if p : i < as.length ∧ i < bs.length then
          some (f (as.get ⟨i, p.left⟩) (bs.get ⟨i, p.right⟩))
        else
          none := by
  induction as generalizing bs i with
  | nil => simp [Nat.not_lt_zero]
  | cons a as aih =>
    cases bs with
      | nil => simp [Nat.not_lt_zero]
      | cons b bs =>
        cases i <;> simp_all [Nat.zero_lt_succ, Nat.succ_lt_succ_iff]

[semorrison]

@joehendrix, sorry, I don't understand what the concern is with variable names. In my application I can simp by this lemma just fine, and get a goal something like:

⊢ Option.getD
    (match List.get? xs i, List.get? ys i with
    | some a, some b => some (a * b)
    | x, x_1 => none)
    0 =
  Option.getD (List.get? xs i) 0 * Option.getD (List.get? ys i) 0

[semorrison]

Is it the x and x_1 names that you're concerned about?

[semorrison]

(You might be able to see from my example why I wanted a match on xs.get? i, ys.get? i: in my application the next step is cases xs.get? i <;> cases ys.get? i, which operates on both the LHS (i.e. the result of this lemma), and the RHS.)

[joehendrix]

@semorrison I was thinking thinking of all the names that potentially need to be synthesized in the match (a, b, and the two underscores). Those could be brittle if user's need to refer to them since it depends on what other variables are in scope.

One could also write the lemmas as the code below:

theorem zipWith_get? {f : α → β → γ} : (List.zipWith f as bs).get? i = f <$> as.get? i <*> bs.get? i := by ...

I think this is more elegant than my initial suggestion, but I don't think there is a similar elegant lemma for zipWithAll.

I was also thinking if we could integrate simp and linear arithmetic, then it may be advantageous to go directly to right-hand sides with arithmetic conditions. We could postpone that sort of decision until linear arithmetic is integrated.

[semorrison]

I'm skeptical that this naming collision problem is any worse than having a lambda on the right hand side.

e.g. the line above in this file is:

theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i := by

Are the r and p problematic? If not, why are the names in the match statement different?

[digama0]

Agreed with Scott, generally speaking it shouldn't matter what variable names are used inside lambdas and match expressions, the names only become relevant once they enter the context via intro x or similar and all such mechanisms provide a way to give a name (and if not you can always use rename_i or next to name them).

In any case, it's not a simp lemma so it doesn't really matter for the purposes of this PR, this is just one option available to the user, if it results in a bad or inconvenient goal they can use something else.