Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC