Move `let ... in` out of goal

Stream: new members

[Marcus Rossel]

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]

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

[Reid Barton]

Normally we try to avoid using let in definitions

[Marcus Rossel]

Adam Topaz said:

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]

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]

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]

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]

@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.