Stream: new members

Topic: Extract Subexpression in Proof

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


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

Marcus Rossel (Mar 06 2021 at 15:27):

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

Marcus Rossel (Mar 06 2021 at 15:27):

set does change the goal automatically.

Eric Wieser (Mar 06 2021 at 15:55):

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

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