Zulip Chat Archive

Stream: new members

Topic: Extract Subexpression in Proof


view this post on Zulip Marcus Rossel (Mar 06 2021 at 15:24):

Is it possible to give a name to specific subexpressions in a proof?
E.g. if the goal state is:

(foo bar baz 1 2 3) + (foo bar baz 1 2 3) - (foo bar baz 1 2 3) = (foo bar baz 1 2 3)

... then can I change this somehow to: ?

e : nat
h_e : e = foo bar baz 1 2 3
 e + e - e = e

view this post on Zulip Kevin Buzzard (Mar 06 2021 at 15:25):

generalize -- actually that's not quite what you want. How about just set e := foo bar baz 123 with h_e? I don't know if that changes the goal but you could just rw \l h_e or change the goal to e (set is definitional).

view this post on Zulip Marcus Rossel (Mar 06 2021 at 15:27):

The set e := ... with ... is exactly what I needed. Thanks :)

view this post on Zulip Marcus Rossel (Mar 06 2021 at 15:27):

set does change the goal automatically.

view this post on Zulip Eric Wieser (Mar 06 2021 at 15:55):

Doesn't generalize work here in exactly the same way?

view this post on Zulip Kevin Buzzard (Mar 06 2021 at 18:23):

I don't think it would give you h_e


Last updated: May 11 2021 at 23:11 UTC