Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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...

view this post on Zulip Adam Topaz (Jan 15 2021 at 15:59):

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

view this post on Zulip Reid Barton (Jan 15 2021 at 16:02):

Normally we try to avoid using let in definitions

view this post on Zulip Marcus Rossel (Jan 15 2021 at 16:09):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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