Several questions about constants

Stream: maths

[tica]

Hello,

I have several questions.

What is the difference between these different writings? When to use one or the other?

constant a : Π n, n + 2 = 7
constant a' (n: ℕ): n + 2 = 7
constant a'' : ∀ n, n + 2 = 7

Why can't I write it like this?

constant a''' : λ n: ℕ, n + 2 = 7

But it works when I define a function. (the different writings all work with the keyword def)

def a := λ n: ℕ, n + 2 = 7

\\
A constant and an axiom are the same thing.
So I can do this:

constant a : Π n, n + 2 = 7
example : 2 + 2 = 7 := a 2

Why can't I do

constant a : Π n, n + 2 = 7
example (hq : a) : 2 + 2 = 7 := a 2 --error

'a' is a proposition though, so I should be able to put it as a hypothesis.

Last question, what is really the difference between a constant and a variable?

Sorry for all the questions.

Thanks

[Riccardo Brasca]

Note that a is not a proposition. The proposition is Π n, n + 2 = 7 and a is a proof of it.

[Riccardo Brasca]

I mean, a proof you suppose to have.

[tica]

ok thanks it works like this:

example (hq: Π n, n + 2 = 7): 2 + 2 = 7 :=
begin
apply hq,
end

so 'a' is only usable as a theorem.

Do you have an idea for my other questions?

[Yaël Dillies]

\lambda and \Pi simply mean different things. The former lets you build elements of the latter.

[Alexander Bentkamp]

tica said:

What is the difference between these different writings? When to use one or the other?

constant a : Π n, n + 2 = 7
constant a' (n: ℕ): n + 2 = 7
constant a'' : ∀ n, n + 2 = 7

They are all the same. You can use #check a to see that.

[Alexander Bentkamp]

tica said:

Why can't I write it like this?

constant a''' : λ n: ℕ, n + 2 = 7

But it works when I define a function. (the different writings all work with the keyword def)

def a := λ n: ℕ, n + 2 = 7

The right hand side of the : must always be a type or sort. In your example, λ n: ℕ, n + 2 = 7 is a function, which is not a type. λ creates functions. Π creates a function type.

[Alexander Bentkamp]

Note that this is not a constant vs def issue. This will give the same error:

def a : λ n: ℕ, n + 2 = 7 := sorry

[tica]

But why can I use \Pi as a function if it is only a type ?

constant a : Π n, n + 2 = 7
example : 2 + 2 = 7 := a 2

Everything that is declared constant is always true?
constant P: Prop means that P must be considered true?
So that's the difference with variables?

[Yaël Dillies]

No, you're confusing types and their terms. \Pi n, n + 2 = 7 is a proposition (if you #check it, you will see it has type Prop). \la n, n + 2 = 7, is a predicate on the naturals, aka a function nat -> Prop`.

[Yaël Dillies]

constant P : Prop declares a new proposition you don't know anything about. In particular, you have no idea whether it is true or false. The way to make P be considered true would be to have constant h : P, that is that you have a proof of P.

[tica]

Oh ok, thanks you