## Stream: new members

### Topic: Move let ... in out of goal

#### Marcus Rossel (Jan 15 2021 at 15:56):

Say I have a goal:

η : some_type
b c z : int
⊢ η ≈ let a := b + c in {x := a, y := z}


Is it possible to move the let a := b + c in out of the goal, by introducing a new hypothesis for a? So that:

η : some_type
a b c z : int
h_a : a = b + c
⊢ η ≈ {x := a, y := z}


Or something along those lines...

#### Adam Topaz (Jan 15 2021 at 15:59):

I guess you could use the let tactic with change. Can you give a #mwe ?

#### Reid Barton (Jan 15 2021 at 16:02):

Normally we try to avoid using let in definitions

#### Marcus Rossel (Jan 15 2021 at 16:09):

I guess you could use the let tactic with change. Can you give a #mwe ?

Here's an MWE:

structure some_type := (x : int) (y : int)

def some_func (b c z : int) : some_type :=
let a := b + c in {x := a, y := z}

example (b c z : int) : ∀ η : some_type, η = (some_func b c z) :=
begin
intro η,
unfold some_func,

end


#### Marcus Rossel (Jan 15 2021 at 16:10):

Reid Barton said:

Normally we try to avoid using let in definitions

Oh interesting, how do you replace them? E.g. right now I'm trying to prove a lemma about the following function:

private noncomputable def propagate_edges (v : value) : network.graph → list network.graph.edge → network.graph
| η [] := η
| η (eₕ :: eₜ) :=
let rtr := (η.data eₕ.dst.rtr) in
let input' := rtr.input.update_nth eₕ.dst.prt v in
let rtr' := {reactor . input := input', ..rtr} in
let η' := η.update_data eₕ.dst.rtr rtr' in
propagate_edges η' eₜ


I know that I technically could remove all of the let in expressions, but that would make it unreadable.

#### Adam Topaz (Jan 15 2021 at 16:15):

Well, for your immediate question, you can do this

structure some_type := (x : int) (y : int)

def some_func (b c z : int) : some_type :=
let a := b + c in {x := a, y := z}

example (b c z : int) : ∀ η : some_type, η = (some_func b c z) :=
begin
intro η,
unfold some_func,
dsimp,
sorry
end


#### Reid Barton (Jan 15 2021 at 16:30):

Marcus Rossel said:

Reid Barton said:

Normally we try to avoid using let in definitions

Oh interesting, how do you replace them?

Some combination of auxiliary top-level definitions and just writing expressions inline; though really in math we tend not to encounter definitions like this in the first place

#### Marcus Rossel (Jan 15 2021 at 16:35):

@Reid Barton Ok that makes sense. In this case propagates_edges performs one step of a computation, and splitting that up further would really just be splitting for its own sake.

Last updated: May 14 2021 at 07:19 UTC