Zulip Chat Archive

Stream: general

Topic: how to _really_ use `let`

Eric Rodriguez (Apr 21 2021 at 11:28):

let is often confusing me, for example in the same way that Manuel is confused in this comment chain, but sometimes even simp struggles with it:

import tactic

example {α : Type*} (a : α) [decidable_eq α] (arr : α  option α) : false :=
  let f := λ t : α  option α, λ k, (λ x : α, if x = a then k else t x),
  suffices : function.injective (f arr), by sorry,
  intros x y h, rw function.funext_iff at h, specialize h a,
  -- simp only [f, if_true, eq_self_iff_true] at h, assumption
  -- this line effectively does `simp only [f]`
  simp only [f] at h, simp only [if_true, eq_self_iff_true] at h, assumption

Is there a way to work more harmoniously with let?

Eric Wieser (Apr 21 2021 at 12:12):

The unhelpful answer here is "make a standalone definition instead". The nice thing about that answer in this case is that that definition already exists, its docs#function.update.

Eric Rodriguez (Apr 21 2021 at 12:16):

is there much disadvantage to using a dite when an ite will do? (in the way function.update does)

Mario Carneiro (Apr 21 2021 at 12:16):

function.update uses dite because it supports a dependent function type

Mario Carneiro (Apr 21 2021 at 12:17):

In your case the function is not dependent so ite is fine

Mario Carneiro (Apr 21 2021 at 12:17):

but if you are reusing function.update I wouldn't worry about the distinction

Eric Wieser (Apr 21 2021 at 12:17):

Note the implementation of function.update is:

/-- Replacing the value of a function at a given point by a given value. -/
def update (f : Πa, β a) (a' : α) (v : β a') (a : α) : β a :=
if h : a = a' then eq.rec v h.symm else f a

so the h is used

Horatiu Cheval (Apr 21 2021 at 16:34):

Are lets in general safe to use in definitions you intend to reason about or should they be avoided? I had cases where some lets would appear in proofs after some simplifications, but eventually they simplified out, but I'm still worried at some point I might get a let that gets more significantly in the way.

Yakov Pechersky (Apr 21 2021 at 16:35):

It's hard to rewrite across a let.

Last updated: Aug 03 2023 at 10:10 UTC