different types of Lean expressions

Stream: new members

[Kevin Lacker]

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]

• 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.)

• If foo occurs in an expression, it is the constant expr.const `foo []. In metaprogramming you can treat it as a declaration: https://github.com/leanprover-community/lean/blob/master/library/init/meta/declaration.lean

[Kevin Lacker]

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]

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

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

[Kevin Lacker]

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

[Kevin Buzzard]

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]

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

[Kevin Lacker]

OK

[Kevin Buzzard]

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]

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]

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]

aah yes, even -> is defined using pi.

[Kevin Lacker]

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

[Adam Topaz]

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

[Adam Topaz]

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