lean4 version of le_add_comm

Stream: lean4

[Chris Lovett]

What is the lean4 version of this proof that uses cases' from mathlib:
image.png

I tried this:

lemma le_add_comm (l m n : ℕ) : (m + l ≤ n + l) = (m ≤ n) := by
  cases' Classical.em (m ≤ n)
  case inl h =>
    simp [min, h]
  case inr h =>
    simp [min, h]

But it has unsolved goals like this:
image.png

I tried adding simp [min, h, Nat.le_of_add_le_add_right] thinking that since that proves a + b ≤ c + b → a ≤ c it would help me eliminate l in this goal and then simp could finish it using the hypothesis, but this didn't work either. Is there a tactic that eliminates l by subtracting l from both sides of the ≤ ?

[Mario Carneiro]

it's a simp lemma

[Mario Carneiro]

where did you find that lemma? I can't find min_add_add in any of {lean, mathlib, lean4, std4, mathlib4}

[Chris Lovett]

oh, hang on, no I added it in order to port min_add_add which is in the hitchhiker's guide to logic verification.

[Mario Carneiro]

do you have a MWE that compiles in lean 3?

[Mario Carneiro]

Assuming you have a working version of the lean 3 code, you can use simp? to find what additional lemmas it's using

[Chris Lovett]

This is the one I'm trying to port:

lemma min_add_add (l m n : ℕ) :
    min (m + l) (n + l) = min m n + l := by
  cases Classical.em (m ≤ n)
  case inl h =>
    simp [min, h]
  case inr h =>
    simp [min, h]

[Mario Carneiro]

the behavior of simp depends on all the lemmas tagged @[simp] in the library, and there are a ton of those and not all have been ported

[Mario Carneiro]

this works for me:

import Std.Data.Nat.Lemmas -- or something in mathlib4 that implies this

attribute [simp] Nat.add_le_add_iff_le_right

theorem min_add_add (l m n : Nat) :
    min (m + l) (n + l) = min m n + l := by
  cases Classical.em (m ≤ n)
  case inl h =>
    simp [min, h]
  case inr h =>
    simp [min, h]

[Chris Lovett]

Thanks!

[Chris Lovett]

Yeah, math lib provides lemma in import Mathlib.Tactic.Basic.

[Chris Lovett]

Ok, now that I have min_add_add, I'm also having trouble with length_zip, do we have a lean4 version of length_zip ?

def length {α : Type} : List α → ℕ
| [] => 0
| (_ :: xs) => (length xs) + 1

attribute [simp] Nat.add_le_add_iff_le_right

theorem min_add_add (l m n : Nat) :
    min (m + l) (n + l) = min m n + l := by
  cases Classical.em (m ≤ n)
  case inl h =>
    simp [min, h]
  case inr h =>
    simp [min, h]

set_option trace.Meta.Tactic.simp.rewrite true
lemma length_zip {α β : Type} (xs : List α) (ys : List β) :
    length (zip xs ys) = min (length xs) (length ys) := by
  induction' xs
  case nil => simp [length, min]
  case cons x xs' ih  => -- ih ⊢ length (zip (x :: xs') ys) = min (length (x :: xs')) (length ys)
    cases ys
    case nil => rfl
    case cons y ys' =>   -- ⊢ length (zip (x :: xs') (y :: ys')) = min (length (x :: xs')) (length (y :: ys'))
      simp [zip]         -- ⊢ length ((x, y) :: zip xs' ys') = min (length (x :: xs')) (length (y :: ys'))
      simp [length]      -- ⊢ length (zip xs' ys') + 1 = min (length xs' + 1) (length ys' + 1)
      simp [min_add_add]  -- ⊢ length (zip xs' ys') = min (length xs') (length ys')
      simp [ih]           -- why can't it make use of ih to solve this?

Here's the lean3 proof :

lemma length_zip {α β : Type} (xs : list α) (ys : list β) :
  length (zip xs ys) = min (length xs) (length ys) :=
begin
  induction' xs,
  case nil {
    refl },
  case cons : x xs' {
    cases' ys,
    case nil {
      refl },
    case cons : y ys' {
      simp [zip, length, ih ys', min_add_add] } }
end

and it could solve it,

0. [simplify.rewrite] [LoVe.zip.equations._eqn_3]: zip (x :: xs') (y :: ys') ==> (x, y) :: zip xs' ys'
0. [simplify.rewrite] [LoVe.length.equations._eqn_2]: length ((x, y) :: zip xs' ys') ==> length (zip xs' ys') + 1
0. [simplify.rewrite] [[anonymous]]: length (zip xs' ys') ==> min (length xs') (length ys')
0. [simplify.rewrite] [LoVe.length.equations._eqn_2]: length (x :: xs') ==> length xs' + 1
0. [simplify.rewrite] [LoVe.length.equations._eqn_2]: length (y :: ys') ==> length ys' + 1
0. [simplify.rewrite] [LoVe.min_add_add]: min (length xs' + 1) (length ys' + 1) ==> min (length xs') (length ys') + 1
0. [simplify.rewrite] [add_left_inj]: min (length xs') (length ys') + 1 = min (length xs') (length ys') + 1 ==> min (length xs') (length ys') = min (length xs') (length ys')
0. [simplify.rewrite] [eq_self_iff_true]: min (length xs') (length ys') = min (length xs') (length ys') ==> true

but I'm not sure how to do ih ys' in lean4, that part doesn't compile... saying

function expected at
  ih
term has type
  length (zip xs' (y :: ys')) = min (length xs') (length (y :: ys'))

I assume that is what helps it with the difference between zip (x :: xs') ys and zip xs' ys ?

[Notification Bot]

Chris Lovett has marked this topic as unresolved.

[Henrik Böving]

How about:

theorem length_zip {α β : Type} (xs : List α) (ys : List β) :
    (xs.zip ys).length = min xs.length ys.length := by
  induction xs generalizing ys with
  | nil => simp [List.length, min]
  | cons x xs' ih  =>
    cases ys
    case nil => rfl
    case cons y ys' =>
      simp_all[List.length, List.zip, min_add_add]

[Henrik Böving]

The key here is that I am generalzing over ys which allows me to apply the more general IH in the induction step. If you check it out we have:

ih : ∀ (ys : List β), List.length (List.zip xs' ys) = min (List.length xs') (List.length ys)
⊢ List.length (List.zip (x :: xs') (y :: ys')) = min (List.length (x :: xs')) (List.length (y :: ys'))

in the generalized vs:

ih : List.length (List.zip xs' (y :: ys')) = min (List.length xs') (List.length (y :: ys'))
⊢ List.length (List.zip (x :: xs') (y :: ys')) = min (List.length (x :: xs')) (List.length (y :: ys'))

in the non generalized variant. This will after all simplification get stuck on:

ih : List.length (List.zipWith Prod.mk xs' (y :: ys')) = min (List.length xs') (List.length ys' + 1)
⊢ List.length (List.zipWith Prod.mk xs' ys') = min (List.length xs') (List.length ys')

because ys' does not match (y :: ys') but if we universally quantify over ys we can just plug it in here and everything works out nicely.

[Chris Lovett]

Thanks works great, and makes sense, I see you also is simp_all so you didn't need to add ih to the simp list.

[Chris Lovett]

Nice that this generalizing ys syntax now reads very nicely with the proof explanation:

The presence of ∀-quantifiers is explained as follows. The induction’ tactic
automatically generalized the lemma statement so that the induction hypothesis
is not restricted to same fixed β and ys as the proof goal but can be used for
arbitrary values of β and ys. Such flexibility is rarely needed for types (e.g., β),
but here we need it for ys, because we want to instantiate the quantifier with ys’s
tail (called ys') and not with ys itself.

[Henrik Böving]

Note that I'm not using simp_all just to save simp[ih] but mainly because the ih also needs some simplification with the mentioned definitions and simp_all allows that in 1 instead of 2 steps.

Furthermore I believe that at least mathlib doesn't usually simplify using definitions right away but instead they will build an API such as length_nil: List.length [] = 0 etc and then use these API lemmata to prove things. This allows for change of definition afterwards without breaking all the downstream proofs

[Chris Lovett]

Thanks for the clarification, but I did notice this simp works too:

theorem length_zip₂ {α β : Type} (xs : List α) (ys : List β) :
    (xs.zip ys).length = min xs.length ys.length := by
  induction xs generalizing ys with
  | nil => simp [List.length, min]
  | cons x xs' ih  =>
    cases ys
    case nil => rfl
    case cons y ys' =>
      simp [List.length, List.zip, min_add_add, ih]

[Henrik Böving]

Hm, didnt work for me on the first try but maybe I was just being stupid /o\

[Chris Lovett]

Nice to know about simp_all thought, thanks :-)