## 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 :=
begin
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,
-- DOESN'T WORK:
-- simp only [f, if_true, eq_self_iff_true] at h, assumption
-- this line effectively does simp only [f]
-- DOES WORK:
simp only [f] at h, simp only [if_true, eq_self_iff_true] at h, assumption
end


Is there a way to work more harmoniously with let?

#### 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