cases

Stream: new members

[Iocta]

What are the cases lines doing?

import data.real.basic
import algebra.pi_instances
import tuto_lib

notation `|`x`|` := abs x

variables (u v w : ℕ → ℝ) (l l' : ℝ)

example (hu : seq_limit u l) (hv : seq_limit v l') :
seq_limit (u + v) (l + l') :=
begin
  intros ε ε_pos,
  cases hu (ε/2) (by linarith) with N₁ hN₁,
  cases hv (ε/2) (by linarith) with N₂ hN₂,
  use max N₁ N₂,
  intros n hn,
  cases ge_max_iff.mp hn with hn₁ hn₂,
  have fact₁ : |u n - l| ≤ ε/2,
    from hN₁ n (by linarith),  -- note the use of `from`.
                               -- This is an alias for `exact`,
                               -- but reads nicer in this context
  have fact₂ : |v n - l'| ≤ ε/2,
    from hN₂ n (by linarith),
  calc
  |(u + v) n - (l + l')| = |u n + v n - (l + l')|   : rfl
                     ... = |(u n - l) + (v n - l')| : by congr' 1 ; ring
                     ... ≤ |u n - l| + |v n - l'|   : by apply abs_add
                     ... ≤  ε                       : by linarith,
end

[Iocta]

I think cases is breaking up the "and" that's built into the forall, but then what's (ε/2) (by linarith) about?

[Bryan Gin-ge Chen]

I'm guessing because you haven't given a #mwe, but most likely the type of the term hu (ε/2) (by linarith) is something like ∃ N, hN. Then cases ... with N hN creates terms N and hN in the context from that term.

[Iocta]

https://github.com/leanprover-community/tutorials/blob/master/src/exercises/05_sequence_limits.lean#L106

[Bryan Gin-ge Chen]

Section 7.3 of TPiL talks about how exists is an inductively defined proposition: https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#inductively-defined-propositions Section 7.6 talks about how cases decomposes inductively defined propositions.

[Bryan Gin-ge Chen]

We had a discussion a while back about how this seems to be kind of hard for new people to figure out: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/A.20tutorial.20of.20Lean.20for.20mere.20mortals/near/199571350

[Bryan Gin-ge Chen]

lean#296 is still open...

[Bryan Gin-ge Chen]

I looked at the code and indeed...

hu : seq_limit u l

And seq_limit u l := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε, which is short for ∀ ε, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ εso:

hu (ε/2) (by linarith) : ∃ N, ∀ n ≥ N, |u n - l| ≤ (ε / 2)

Here, Lean infers that by linarith must have the type ε/2 > 0, and indeed, the tactic linarith is able to prove this, so it typechecks.

[Iocta]

I was parsing it wrong, it's

  cases ((hu (ε/2)) (by linarith)) with N₁ hN₁,

[Iocta]

cases seems similar to specialize for this?

[Bryan Gin-ge Chen]

Not that I can see. What were you thinking, exactly?

[Yury G. Kudryashov]

cases can split any inductive type, not only and. In this case it splits ∃ N, ... into N and hN : ∀ n ≥ N, ....

[Scott Morrison]

This is a good example where using obtain would result in easier-to-read code.