# Zulip Chat Archive

## Stream: new members

### Topic: introduce new constants and propositions

#### Alex Zhang (May 24 2021 at 11:09):

How can I introduce new constants and propositions? For example, how to set x=5 or use h to name a proposition x=y (without claiming h is true or false)?

#### Kevin Buzzard (May 24 2021 at 11:11):

Can you give a more concrete example of what you mean? In a tactic proof you can write `let x := 5`

or `let h := x=y`

but I'm not sure if that's what you mean.

#### Alex Zhang (May 24 2021 at 11:20):

Here is a silly example:

```
import data.real.basic
example (x : ℝ) : x=x :=
begin
let y:ℝ :=5,
let g:= y=x,
by_cases g,
end
```

Then I got state:

```
2 goals
x : ℝ,
y : ℝ := 5,
g : Prop := y = x,
h : g
⊢ x = x
x : ℝ,
y : ℝ := 5,
g : Prop := y = x,
h : ¬g
⊢ x = x
```

In the first goal, why did I get `h:g`

instead of `h: y=x`

. Can I somehow change h to `h: y=x`

?

#### Kevin Buzzard (May 24 2021 at 11:21):

Enclose code in ` ``` `

triple back ticks (on their own lines)

#### Kevin Buzzard (May 24 2021 at 11:23):

`g`

is defined to be the *type*, `y = x`

, i.e. the true-false *statement* "y = x". We don't care if this is true or false, we're just defining the mathematical statement.

#### Kevin Buzzard (May 24 2021 at 11:25):

`g`

is defined to be `y = x`

, and the answer to "why did I get `h : g`

is "because you did cases on `g`

". You can indeed change `h`

to `h : y = x`

using the `change`

tactic. Try `change y = x at h`

#### Kevin Buzzard (May 24 2021 at 11:28):

Alternatively if you used `set g := y = x with hg`

then you could `rw hg at h`

#### Alex Zhang (May 24 2021 at 11:31):

Thank you very much, Kevin!

If I change the code to

```
import data.real.basic
example (x : ℝ) : x=x :=
begin
let y:ℝ :=5,
let g:= y=x,
have h: y=5,
end
```

How can I close the first goal `⊢ y=5`

?

#### Alex Zhang (May 24 2021 at 11:36):

I got it myself. I think`refl`

does the job.

#### Kevin Buzzard (May 24 2021 at 11:38):

Yes, `let`

is definitional. `y = 5`

is true by definition of `y`

, and `refl`

closes goals of the form `A = B`

if `A`

and `B`

have the same definition.

#### Kevin Buzzard (May 24 2021 at 11:38):

This is why you can prove `n + 0 = n`

by `refl`

if `n`

is a natural number, but you can't prove `0 + n = n`

by `refl`

.

#### Alex Zhang (May 24 2021 at 12:41):

@Kevin Buzzard

In the following example, how to introduce a new y in `\R`

?

```
import data.real.basic
example (x : ℝ) : x=x :=
begin
end
```

#### Kevin Buzzard (May 24 2021 at 12:42):

Why would you want to introduce a variable without a definition?

#### Kevin Buzzard (May 24 2021 at 12:42):

I'm not sure this is ever the correct logical next step in a proof.

#### Kevin Buzzard (May 24 2021 at 12:43):

I suspect that any time you think you're doing that, you're just in the process of making a definition which you haven't spotted yet.

#### Kevin Buzzard (May 24 2021 at 12:44):

If you really want a variable without a definition, you can put it before the colon in the statement of the example. But you can see that it won't do you any good.

#### Kevin Buzzard (May 24 2021 at 12:44):

Or you could do `have y : \R := 37`

and because you used `have`

not `let`

, Lean will forget the value of `y`

in the sense that it won't tell you what it is, even though secretly it will still be 37.

#### Alex Zhang (May 24 2021 at 12:45):

The reason I am interested in this is that in many math proofs, we start with something like "fix an arbitrary y in some set..."

#### Kevin Buzzard (May 24 2021 at 12:45):

Is that set non-empty?

#### Alex Zhang (May 24 2021 at 12:45):

non-empty like R

#### Kevin Buzzard (May 24 2021 at 12:45):

R is not a set in Lean

#### Kevin Buzzard (May 24 2021 at 12:46):

But if you have a type and a proof that it's nonempty, then you can choose an element of this type.

#### Kevin Buzzard (May 24 2021 at 12:47):

Alex Zhang said:

The reason I am interested in this is that in many math proofs, we start with something like "fix an arbitrary y in some set..."

This is an appealing-sounding belief, in the sense that it *sounds* like the kind of thing that one might do and which might be helpful, but it's not helpful for proving $x=x$ so it might be worth coming back to this conversation only when you've found a situation where it *is* helpful.

#### Kevin Buzzard (May 24 2021 at 12:48):

In your case, you want to choose an arbitrary real number, and so as I say the way to do this is `have y : \R := 37`

. Then `y`

will be 37 but you will not be able to access this proof, so as far as you are concerned `y`

is an arbitrary real number.

#### Kevin Buzzard (May 24 2021 at 12:50):

If you don't like that, then you surely like the fact that you are not allowed to choose a random term of a type until you have proved that the type is nonempty. Without that hypothesis you would be able to prove false things. So before you can choose a random element of the real numbers, I would like you to supply me with a proof that the real numbers are nonempty. And the moment you name a real number I will let that be `y`

but I won't tell you that this is what I did.

#### Kevin Buzzard (May 24 2021 at 12:52):

This sounds odd to you perhaps, but this is because you are working under the hypothesis that you are pretty sure that sometimes mathematicians say "now let y in S be arbitrary" whereas I am suggesting that actually they don't say this, except when they are in the middle of doing something else, and when you're doing the something else you'll have a "for all y,..." goal and you can do `intro y`

to get the `y`

which you believe should be available in general. *That* `y`

is the kind of y which you are expecting to see, but as I say you can only see it in some wider context.

#### Alex Zhang (May 24 2021 at 12:54):

Yeah,x=x is just a silly theorem used as an example. What I am interested in general is, in the proof of a theorem, how we can do something like "let y be an element in R" like we always do in a usual math proof. I think in a usual math proof if we suppose y to be in some set S but S is empty, then whatever results about y are vacuously true.

#### Kevin Buzzard (May 24 2021 at 12:55):

I told you: you write `have y : \R := 37`

#### Kevin Buzzard (May 24 2021 at 12:56):

like we always do in a usual math proof.

Can you please show me a full "usual math proof" (in words, not in Lean) which involves choosing an arbitrary real number? Again I am saying that you *believe* that we "always" do this in a maths proof, but you have shown no examples of this yet, and you've just agreed that you don't need to do this when proving x=x. I'm arguing that we only ever do this in a context where the goal is "for all y, ...", and in this situation you do it by `intro y`

.

#### Kevin Buzzard (May 24 2021 at 12:58):

In short, you only let y be random when you're trying to prove something for all y. You're trying to let y be random in a situation where we're not doing this, and so I can just let y be 37 and not tell you.

#### Alex Zhang (May 24 2021 at 12:58):

Kevin Buzzard said:

This sounds odd to you perhaps, but this is because you are working under the hypothesis that you are pretty sure that sometimes mathematicians say "now let y in S be arbitrary" whereas I am suggesting that actually they don't say this, except when they are in the middle of doing something else, and when you're doing the something else you'll have a "for all y,..." goal and you can do

`intro y`

to get the`y`

which you believe should be available in general.That`y`

is the kind of y which you are expecting to see, but as I say you can only see it in some wider context.

I think it would usually be the case you mentioned in this answer.

#### Kevin Buzzard (May 24 2021 at 12:58):

OK so the answer to your question is that you do it with `intro y`

.

#### Kevin Buzzard (May 24 2021 at 12:59):

But that it will only work if the goal is of an appropriate form.

#### Kevin Buzzard (May 24 2021 at 13:00):

And what I am trying to teach is that if the goal is not of this form, then you never want to do what you think you want to do. You only do it when you are in the middle of defining a function or proving a theorem for all real numbers.

#### Alex Zhang (May 24 2021 at 13:01):

Thanks for your explanations!

#### Alex Zhang (May 24 2021 at 13:03):

Kevin Buzzard said:

And what I am trying to teach is that if the goal is not of this form, then you never want to do what you think you want to do. You only do it when you are in the middle of defining a function or proving a theorem for all real numbers.

I think when we do say "let y be in R...", we are indeed in these cases.

#### Eric Rodriguez (May 24 2021 at 13:06):

Alex, can you name a specific proof where you do this and you're not implicitly trying to prove a forall?

#### Alex Zhang (May 24 2021 at 13:08):

I think the easy examples currently in my head can all be summarized into the cases Kevin mentioned.

#### Alex Zhang (May 24 2021 at 13:10):

Please share it if you get any interested one.

Last updated: Dec 20 2023 at 11:08 UTC