## Stream: new members

### Topic: cases

#### Iocta (Jul 05 2020 at 04:47):

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 (Jul 05 2020 at 04:48):

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 (Jul 05 2020 at 04:50):

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 (Jul 05 2020 at 04:50):

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

#### Bryan Gin-ge Chen (Jul 05 2020 at 04:51):

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 (Jul 05 2020 at 04:54):

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 (Jul 05 2020 at 04:54):

lean#296 is still open...

#### Bryan Gin-ge Chen (Jul 05 2020 at 05:00):

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 (Jul 05 2020 at 05:00):

I was parsing it wrong, it's

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


#### Iocta (Jul 05 2020 at 05:15):

cases seems similar to specialize for this?

#### Bryan Gin-ge Chen (Jul 05 2020 at 05:36):

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

#### Yury G. Kudryashov (Jul 05 2020 at 05:58):

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

#### Scott Morrison (Jul 05 2020 at 09:57):

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

Last updated: May 11 2021 at 21:10 UTC