## Stream: new members

### Topic: different types of Lean expressions

#### Kevin Lacker (Oct 16 2020 at 20:18):

Sorry for a long question here but... I'm trying to write some tactics that look at expressions and I am a little confused about the different types of expression. I don't quite see how the docs at https://leanprover.github.io/reference/expressions.html and the src/meta/expr.lean code itself and the expressions in regular Lean code line up. The parts I think I understand:

• A variable is something like the x within example {x : \N} : x > 3 := sorry
• A constant is the 3
• A sort is what I would call a "type" in another programming language
• A metavariable is like the ?m_1 you get if you apply a lemma that doesn't totally unify
• pi, lambda, and application expressions are \all, \each, and function application

Questions:

• Can metavariables be expressed in actual Lean code? Or only in things like goals?
• What is a "local constant"?
• An expression like x = 2 with an infix operator, what sort of expression is that?
• If you define a lemma like lemma foo (x : \N) : x < 1 -> x < 2  then what sort of expression is foo later?

#### Floris van Doorn (Oct 16 2020 at 21:29):

• A variable is a bound variable. The internal representation of the second x in fun x, x is a variable (this will be var 0, google de Bruijn variables for more information)
• The 3 is not quite a constant, since it is actually a more complicated expression. But every definition, theorem, inductive (so roughly everything in the library with a name) is a constant
• A sort is a universe of types. nat is a type, but not a sort.
• Metavariables can not occur in definitions or theorems accepted by the Lean kernel. They only exist in incomplete definitions/theorems.
• With \each you probably mean \la.
• A local constant is the x in your first example. In a goal, the lines before the ⊢ is a list of local constants
• The expression x = 2 is a function application of the constant eq applied to an implicit argument, and then the variable x and the expression 2. See the goal here.
set_option pp.all true
example {x : ℕ} : x = 2  :=
begin

end


Try playing around with other pp options. You can see the options when tab-completing set_option pp. (or you can type #help options and search for pp.)

#### Kevin Lacker (Oct 16 2020 at 21:55):

okay, thanks! the set_option pp.all is quite helpful. why is ∀ its own special language thing and ∃ is just a normal old function? I had guessed they would be handled symmetrically

#### Kevin Buzzard (Oct 16 2020 at 21:56):

\forall is just the same as Pi, right? That's some inbuilt thing in the dependent type theory logic. \exists can be built from other stuff, so it's built from other stuff.

#### Kevin Lacker (Oct 16 2020 at 21:58):

why not build ∀ x : foo x as ¬ ∃ x : ¬ foo x then

#### Kevin Lacker (Oct 16 2020 at 21:59):

or is it like, you have to have one be primal, and ∀ is the one

#### Kevin Buzzard (Oct 16 2020 at 22:00):

I think this is just an implementation issue. The answer to "why is it like this in Lean" is "because Lean uses dependent type theory and Pi is a primitive and Sigma isn't in dependent type theory". One could imagine other logics where this wasn't the case.

#### Kevin Buzzard (Oct 16 2020 at 22:01):

I'm not sure there's anything profound about it -- I mean, it wouldn't affect my usage of lean if it were implemented in a different way, as long as the tactics did the same thing

OK

#### Kevin Buzzard (Oct 16 2020 at 22:03):

I guess one should take what I say about implementation issues with a pinch of salt though -- for me, if you have a lemma saying "forall x, foo x iff not exists x not foo x" then I can rewrite that lemma and who cares if it's definitionally true or not. People writing tactics might care a lot more about definitional equality.

#### Reid Barton (Oct 16 2020 at 22:15):

Well you do care because the lemma really starts "forall foo, ..." and to even apply it you need to know how to deal with a forall

#### Reid Barton (Oct 16 2020 at 22:16):

Kevin Lacker said:

why not build ∀ x : foo x as ¬ ∃ x : ¬ foo x then

¬ P is P -> false i.e. ∀ x : P, false

#### Kevin Buzzard (Oct 16 2020 at 22:18):

aah yes, even -> is defined using pi.

#### Kevin Lacker (Oct 16 2020 at 22:24):

that is certainly not what I expected but I suppose it is logical

#### Adam Topaz (Oct 16 2020 at 23:07):

I think you can simulate dependent Pi types with dependent Sigma types and plain old (nondependent) functions, right?

#### Adam Topaz (Oct 16 2020 at 23:17):

(Of course, I'm not saying this is a good thing to do.)

Last updated: Dec 20 2023 at 11:08 UTC