Zulip Chat Archive

For context, I'm following an exposition about random walks on the integers. I'm trying to talk about "the first time that position is k" , but it's possible that position doesn't hit k within the allotted time N, in which case "the first time" could be N+1 or infinity or something. Lean wants me to say [decideable s = {}] ("you'll know if position hits k or not") but I heard it's good to avoid decideable when possible. What should I do?

import data.nat.basic
import data.set.basic
import data.finset.basic

open set nat real finset

open_locale big_operators

noncomputable theory

universe u

variable α : set ℕ

def first_at (N :ℕ) (position : ℕ → ℕ) (k : ℕ) : ℕ :=
let s := {n : ℕ | n < N ∧ position n = k}
in cond (s = {}) N (inf s)

Kenny Lau (Oct 27 2020 at 08:14):

#backticks

Kenny Lau (Oct 27 2020 at 08:15):

you need a newline after the starting triple backtick

Kenny Lau (Oct 27 2020 at 08:15):

if you don't care about decidability, just put open_locale classical

Johan Commelin (Oct 27 2020 at 08:18):

cond is for bool, whereas if .. then .. else .. is for Props

Iocta (Oct 27 2020 at 08:19):

Which one do I want here?

Johan Commelin (Oct 27 2020 at 08:19):

s = {} is a Prop

Iocta (Oct 27 2020 at 08:20):

import data.real.basic
import data.nat.basic
import data.set.basic
import data.finset.basic
import measure_theory.probability_mass_function


open set nat real finset

open_locale big_operators classical

noncomputable theory

universe u

variable α : set ℕ

def first_at (N :ℕ) (position : ℕ → ℕ) (k : ℕ) : ℕ :=
let s := {n : ℕ | n < N ∧ position n = k}
in if (s = {}) then N else (inf s)

Iocta (Oct 27 2020 at 08:20):

type mismatch at application
  inf s
term
  s
has type
  set ℕ : Type
but is expected to have type
  finset ?m_1 : Type ?

Johan Commelin (Oct 27 2020 at 08:20):

If you want Lean to be able to compute first_at, then I suggest that you use (finset.range N).filter (\lam n, position n = k)

Johan Commelin (Oct 27 2020 at 08:20):

There you go, so that's another argument for using finset

Johan Commelin (Oct 27 2020 at 08:21):

You could then write

if hs : s.nonempty then s.inf' hs else N

on the final line

Iocta (Oct 27 2020 at 08:29):

def first_at' (N :ℕ) (position : ℕ → ℕ) (k : ℕ) : ℕ :=
let s := (finset.range N).filter (λn, position n = k)
in if hs : s.nonempty then s.inf' hs else N

invalid field notation, 'inf'' is not a valid "field" because environment does not contain 'finset.inf''
  s
which has type
  finset ℕ