constants and variables

Stream: new members

[Patrick Thomas]

Is scoping the only difference between constants and variables in Lean?

[Kenny Lau]

constants are axioms while variables is just a shorthand to insert "forall" in the following theorems

[Kenny Lau]

so for example classical.choice is a constant

[Patrick Thomas]

"forall" as an assumed hypothesis in all the following theorems?

[Patrick Thomas]

I guess I'm not certain how that differs from an axiom.

[Kenny Lau]

I have struggled explaining it before, but I guess I'll still try

[Mario Carneiro]

constant never goes out of scope, it's as permanent as a def

[Kenny Lau]

def f : nat -> nat := fun x, x+1 is the same as:

variable (n : nat)
def f : nat := n + 1

[Kenny Lau]

but if you do:

constant n : nat
def g : nat := n + 1

then you're declaring a constant n and g is now a natural number, not a function

[Kenny Lau]

f 3 evaluates to 4 while g 3 is a type mismatch because the type of g is nat

[Mario Carneiro]

f (f n) works but g (g n) doesn't make sense

[Kenny Lau]

g n doesn't make sense to start with?

[Mario Carneiro]

My point being that there is no analog of f (f n) for g

[Mario Carneiro]

you can't substitute for a constant

[Patrick Thomas]

So it is like constants and variables in C? I.e. const float pi = 3.14, versus int x = 0. pi can never take a different value, but x can?

[Kenny Lau]

well Lean is a functional programming language like Haskell, unlike the more conventional programming languages (C, Java, Python) which are imperative languages

[Kenny Lau]

but Lean constant would be C const with a "secret" value

[Kenny Lau]

where variable is just the input to functions

[Patrick Thomas]

I think I kind of see. I started reading a tutorial on Haskell earlier this week. Does it have something similar that I will run across?

[Kenny Lau]

I don't know Haskell but I don't think so

[Patrick Thomas]

Is a variable the same as a variable in the lambda calculus?

[Kenny Lau]

yes

[Patrick Thomas]

Ah. I have not gotten to the typed lambda calculus yet. Will I see constants there?

[Mario Carneiro]

Constants are like Haskell compiler intrinsic functions

[Mario Carneiro]

they are functions, you can see that they have been declared as such, but you can't see the definition

[Mario Carneiro]

Haskell doesn't really have an equivalent to the variables command. Scopes are handled differently in Haskell - you can think of the whole program as being in a single shared scopes where all your definitions are like let bindings. Lean is not like that - there are no variable scopes that span multiple definitions

[Patrick Thomas]

I guess I haven't gotten that far yet.

[Patrick Thomas]

Are constants the same as the "term constants" mentioned here: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

[Mario Carneiro]

yes

[Patrick Thomas]

Thank you

[Kevin Buzzard]

One other difference is that users are hugely discouraged from ever using constants ever. I'm not sure there's a single one in mathlib. But there are variables everywhere

[Ayush Agrawal]

Hi guys! I wanted to be clear on the idea of constants and variables..
Is it correct to map the notion of constants to existential quantifiers (or something arbitrary?) and the variables to universal quantifiers?
I am sensing this notion from the type of the theorems below:

constants p q : Prop
theorem t1 : p → q → p := λ hp : p, λ hq : q, hp

#check t1 -- t1 : p → q → p

variables p q : Prop
theorem t1' (hp : p) (hq : q) : p := hp

#check t1' --t1' : ∀ (p q : Prop), p → q → p

Let me know if I am right!