Zulip Chat Archive

Stream: new members

Topic: Introduce variable

leafGecko (Sep 09 2021 at 20:54):

Hi all,
Is it possible that I introduce a new existential variable inside the proof when it does not appear inside the goal? Like a (x: R). Or is it strictly unnecessary ...
and can I introduce a theorem / lemma to environment so that linarith can make use of it?

leafGecko (Sep 09 2021 at 20:54):

simply have x: R, generates a goal R, which (I presume) is wanting me to prove that R has a member?

Mario Carneiro (Sep 09 2021 at 20:58):

You can use have bla : x < 0 := ... to introduce an assertion x < 0 to the context, or have bla : x < 0, { proof } which makes you prove the assertion by tactics in proof

Mario Carneiro (Sep 09 2021 at 20:58):

You can also add arguments to linarith, like linarith [x_lt_zero]

Jake Levinson (Sep 10 2021 at 04:36):

Be aware that if you want to introduce a proposition e.g. h : x < 0, then have h : x < 0 := { my_proof }, is fine.

But if you want to introduce a value / piece of data, and need to remember what it is, e.g. x := y+1, then you should use set x := y+1 with hx, which will add x : R := y+1 and hx : x = y + 1 to the context, and you can then use rw hx later on if needed (and linarith should detect it in this case). By contrast if you write have x := y+1 then the context will only have x : R and will not remember the value you defined x with.

Johan Commelin (Sep 10 2021 at 05:05):

@leafGecko If you have a proof of nonempty X in your context, then you can extract from it a random x : X. But otherwise you can just pull a x : X out of nowhere, because X might be empty.

Eric Wieser (Sep 10 2021 at 07:35):


Last updated: Dec 20 2023 at 11:08 UTC