introduce new constants and propositions

Stream: new members

[Alex Zhang]

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]

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]

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]

Enclose code in ``` triple back ticks (on their own lines)

[Kevin Buzzard]

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]

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]

Alternatively if you used set g := y = x with hg then you could rw hg at h

[Alex Zhang]

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]

I got it myself. I thinkrefl does the job.

[Kevin Buzzard]

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]

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]

@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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

Is that set non-empty?

[Alex Zhang]

non-empty like R

[Kevin Buzzard]

R is not a set in Lean

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Thanks for your explanations!

[Alex Zhang]

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]

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

[Alex Zhang]

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

[Alex Zhang]

Please share it if you get any interested one.