What exactly does `meta def` do?

Stream: new members

[Chris M]

Can I think of meta def as just defining a tactic? Or does it do more than that? (I'm guessing if all it did was define a tactic it would've been called tactic def).

[Johan Commelin]

meta turns off termination checks for recursive calls.

[Johan Commelin]

So you can define recursive functions without bothering to prove that they terminate (maybe the actually don't, but who cares, just make sure you only give inputs where termination is fine).

[Chris M]

(deleted)

[Johan Commelin]

But everything that uses a meta def/lemma in it's proof or definition will also need to be meta. It's a bit like a virus (-;

[Johan Commelin]

Basically (but I'm not an expert) meta turns Lean into a functional programming language without all the proofy bits.

[Kenny Lau]

meta def contradiction : false := contradiction

[Mario Carneiro]

The other thing meta does is it gives you access to the various meta constants implemented in C++

[Kenny Lau]

meta def Cantor : Type :=
Cantor → Prop

[Chris M]

So my impression was that tactics are its own class of objects within the language, but they are just terms for which termination checking is turned off? I'm a bit confused by this.

[Mario Carneiro]

it also has other technical effects like turning off universe checks, positivity checks in inductives, and the proofy part of the equation compiler

[Mario Carneiro]

tactic A is a lean type like most others, although it is meta meaning that anything of this type has to also be meta

[Kenny Lau]

meta inductive Cantor : Type
| intro : (Cantor → Prop) → Cantor

#check Cantor.intro.inj -- Cantor.intro ?M_1 = Cantor.intro ?M_2 → ?M_1 = ?M_2

[Mario Carneiro]

lean tactics are functional programs using the same term syntax as regular terms used in definitions and proofs

[Mario Carneiro]

however they use various hooks into the lean elaborator which are written in C++ and provided as opaque constants on the lean side

[Kenny Lau]

import logic.function.basic

meta inductive Cantor : Type
| intro : (Cantor → Prop) → Cantor

#check function.cantor_injective Cantor.intro (λ _ _, Cantor.intro.inj) -- false

[Kenny Lau]

a freshly made contradiction

[Kenny Lau]

@Mario Carneiro why does meta theorem give me error?

[Mario Carneiro]

probably because lean thinks this is a stupid thing to do

[Mario Carneiro]

this works for me though

meta theorem foo : true := trivial

[Kenny Lau]

oh, as in, whenever I "abuse" meta theorem

[Kenny Lau]

import logic.function.basic

meta inductive Cantor : Type
| intro : (Cantor → Prop) → Cantor

meta theorem contradiction : false :=
function.cantor_injective Cantor.intro (λ _ _, Cantor.intro.inj) -- false

[Kenny Lau]

"invalid definition, it uses untrusted declaration 'Cantor'"

[Kenny Lau]

oh and why can't I recurse inside a meta structure?

[Kenny Lau]

meta structure Cantor : Type :=
(s : Cantor → Prop) -- unknown identifier 'Cantor'

[Mario Carneiro]

You can't recurse in structures period

[Mario Carneiro]

making these things work in meta defs requires special hacks because the name scoping doesn't naturally make it happen

[Mario Carneiro]

I'm not sure why you are collecting meta proofs of false though

[Chris M]

I've been looking at this link, https://leanprover-community.github.io/extras/tactic_writing.html, and I would like to test my understanding of the Lean language.

Is the following correct?

When we write something like lemma foo : .... := term where term doesn't contain any tactic blocks like begin ... end or by, then Lean only parses and type checks your code. But when we write e.g. a begin ... end block, then Lean parses, compiles and executes the code within the begin ... end block during type checking, just as if e.g. in C++ we would have actually built and run the code. So in a sense, Lean contains a "compiler and execution environment within a type checker". After running this code, each begin ... end block produces a non-meta term, which is then type checked as a non-meta term. If it fails this type check, the begin ... end block produces an error.

Regarding tactic writing (), this means the following:
We can essentially think of any begin ... end block as contain code that we will actually compile and run, just like any other language like C++, except this compilation and running will happen automatically, meaning you never have to press the "Run" button in your IDE. Moreover, we are not allowed to use terms within the begin ... end blocks that don't have the meta keyword, and conversely, we're only allowed to use terms with the meta keyword within begin ... end blocks. In short, meta terms are treated as objects that one can actually run, whereas non-meta terms are only type checked.

However, unlike C++, the Lean "meta-language" is a functional language, and so should be treated like e.g. Haskell.

To summarize, Lean essentially consists of "two separate languages", and an interface between them: the Lean "proof-language" consists of all terms without the meta keyword, and the Lean "meta-language" consists of those with the meta keyword. The meta-language behaves like a normal functional language. The proof-language has a special type system designed along the lines of the Curry-Howard isomorphism and is only type-checked but never executed. The interface between the proof- and meta-language are the tactic blocks begin ... end and by, which tell the meta-language compiler to compile and execute the contents of the block as source code in the meta-language, and interpreting the output as source code of the proof-language. It then replaces the begin ... end block with this source code, and leaves it to the proof-language type checker to type check it as code in the proof-language.

Is this a correct view of how Lean works internally? Will it lead me astray if I would write tactics? Even if it wouldn't lead me astray, I'd still be interested in where I'm wrong on the details.

[Kenny Lau]

Chris M said:

We can essentially think of any begin ... end block as contain code that we will actually compile and run, just like any other language like C++, except this compilation and running will happen automatically, meaning you never have to press the "Run" button in your IDE.

This only happens because VSCode runs Lean automatically. If you wrote Lean in a normal text editing software you still have to compile / run it elsewhere.

[Kyle Miller]

@Chris M Lean compiles all definitions that aren't noncomputable to bytecode. It turns out "only parsing and type checking" for dependent types can involve evaluating lots of code (for example, rfl proofs), though I'm not sure how much is bytecode evaluation and how much is term reduction.

Here's my rough understanding/guess for how some of this works, assuming nothing is noncomputable:

• Lean parses your definition (be it a def or lemma), and constructs a term full of metavariables for all the implicits. This includes thinking of begin ... end blocks as a big metavariable, I think.

• Then it does some depending type checking to figure out what it can. This gives the begin ... end blocks types, possibly with metavariables.

• The tactic language is procedural/monadic, modifying a tactic state that comes from the begin ... end block's type, while simultaneously constructing a term that will replace the block.

• Eventually, if everything worked out, the definition is a complete term.

I'm not sure the precise way this is enforced, but every definition that uses a term with a meta definition must itself be marked meta. Being marked meta confers this and other privileges, like relaxing well-foundedness of recursion. Then, you as a mathematician know that you should not extend the Curry-Howard isomorphism to the types of meta definitions since otherwise you would believe in contradictions.

Going the other way, every meta definition can use all the (computable) non-meta definitions it wants.

[Rob Lewis]

So, I'm literally recording some videos about this today, in preparation for the LFTCM Monday afternoon session. Keep an eye out for some links soon.

You have most of it right. Let's set some terminology: meta-Lean is "Lean with the meta keyword." In some sense, all the meta keyword does is disable termination checking. Meta-Lean is an extension of non-meta Lean, in that any non-meta declaration can also be used in meta declarations. Meta-Lean is trivially unsound (see meta def t : false := t) so it's not interesting for writing proofs.

But you can evaluate meta declarations using #eval. This evaluation happens in the VM, which is not trusted code. So another reading of meta is "for evaluation only," non-meta is "for evaluation and proof."

The VM overrides certain declarations during evaluation. For instance, nats are not represented as the familiar inductive type in the VM. Importantly, a lot of Lean internals that are exposed as meta constants or defs in Lean (expr, env, all the atomic tactics) are overridden. This is confusing, because it's what "meta" should mean. In practice most (but not all) of the reflected Lean stuff has the meta keyword, and some reflected Lean stuff doesn't strictly need to be meta.

The code that appears between begin and end is a meta-Lean expression. It has type tactic unit, effectively a function tactic_state -> tactic_state. (tactic_state is a meta constant in Lean, a C++ data structure in the VM.) begin..end and by are hooks that will construct the tactic_state at the start point, evaluate your tactic script on this tactic state, and deal with the output. Part of the tactic state is a (partially) constructed Lean expression. When this term is fully constructed, it's sent to the kernel to check. Indeed, this term is a result of executing your metaprogram, it doesn't contain the metaprogram you wrote itself. (But it's not necessarily non-meta. You can write a tactic script to produce a meta expr. meta example : expr := by exact expr.var 0) The kernel will never see the script between begin..end, just its output.

[Chris M]

So the "Lean kernel" is what I've called "proof-language type checker"?

[Chris M]

VM = virtual machine?

[Rob Lewis]

Chris M said:

So the "Lean kernel" is what I've called "proof-language type checker"?

Effectively yes. I may have been a little brief -- the script between begin..end does get type checked, in that it has to have type tactic unit.

[Rob Lewis]

Chris M said:

VM = virtual machine?

Yep.

[Chris M]

"In some sense, all the meta keyword does is disable termination checking."
This I still don't really understand. It seems to me that it also completely changes the way that the Lean compiler deals with it?

Is it more correct to say:
Lean-expressions and meta-lean expressions are treated in two separate ways. In particular, meta-lean expressions within begin ... end blocks are compiled to lean-expressions before any lean-expression type checking is performed. Moreover, their type checker is the same, except that the meta-lean type checker has disabled termination checking. Moreover, the actual type systems are different, in that some types are only recognized by the meta-type system (such as the type tactic unit).

[Kyle Miller]

(I'm writing this because I have some interest in internals, and I would appreciate being corrected.)

The stuff about a VM is purely optimization. Since meta definitions don't take part in mathematical truth, it's OK to evaluate such code in a faster way, even if the VM might be less trusted to be correct. (Though what Rob was saying about some meta definitions being replaced by C++ implementations might be another reason: it helps keep the Lean kernel smaller and easier to trust if it doesn't also have to be able to reduce general meta terms too?)

I was looking through some of how the parser works, and begin ... end blocks are (seemingly) parsed into a special term (an external action) that contains a term that should be a tactic unit. I presume the way it then works is that when the Lean compiler sends parsed definitions to the kernel, these terms, including the external actions, are type checked and, once the context around the external action is figured out as much as can be, the kernel asks the outer-layer compiler to fill in the hole. In this particular case, this involves the compiler evaluating the tactic unit with respect to the context, producing a term -- some amount of type checking needs to have been done by this point so the goal window has anything to say, so to speak.

I'm hazy about lots of specifics here, but one conceptual model that seems OK is that you can think of most of the C++ code, the meta definitions, and the non-meta definitions as being the outer-layer compiler, and a subset of the C++ code and the non-meta definitions are the Lean kernel and math. The overlap is that it's as if each non-meta definition also creates a companion meta definition. The outer layer is responsible for interfacing with the real world and directs the Lean kernel, and there is some protocol (for example, begin ... end blocks) for the Lean kernel to ask the outer layer for more information during its type checking process.

I couldn't find the process by which the outer layer checks the types of its meta definitions. I'm guessing there is some provision in the Lean kernel for this.

It seems the way disabling termination checking works is (1) that meta definitions are allowed to refer to the function being defined and (2) that the equation compiler is able to construct terms making use of this, whereas non-meta definitions cannot do so and instead need to resolve into the actual recursors for the given inductive types. For example, compare these two definitions of factorial:

def f : ℕ → ℕ
| 0 := 1
| (n+1) := (n+1) * f n

meta def f' : ℕ → ℕ
| 0 := 1
| (n+1) := (n+1) * f' n

The first, when #printed is roughly

def f : ℕ → ℕ :=
λ (a : ℕ),
  a.brec_on
    (λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ) a),
       (λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ) a),
          a.cases_on (λ (_F : nat.below (λ (a : ℕ), ℕ) 0), id_rhs ℕ 1)
            (λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ) a.succ), id_rhs ℕ ((a + 1) * _F.fst.fst))
            _F)
         a
         _F)

and the second is

meta def f' : ℕ → ℕ :=
λ (a : ℕ), a.cases_on (id_rhs ℕ 1) (λ (a : ℕ), id_rhs ℕ ((a + 1) * f' a))

(the pretty printer actually shows the f' in square brackets, but this does not seem to be meaningful syntax.)

[Mario Carneiro]

(As if there weren't enough explanations on the thread already:) There are two important and orthogonal properties that a lean term can have. (1) It can participate in the standard consistent CIC dependent type theory (as e.g described in my thesis), and (2) it can be evaluable by the lean virtual machine. These properties are negatively marked: a term lacking property (1) is called meta, and a term lacking property (2) is called noncomputable, and you are required to put these markings as appropriate on all definitions.

In particular, all four combinations of the two properties are possible: a meta def has (2), a def has (1) and (2), a noncomputable def has (1), and a noncomputable meta def has neither (this last class is basically useless).

All definitions go through lean's elaborator, which is responsible for inferring all the missing arguments. (This may involve running tactics but we'll get back to that.) From there definitions with (1) go to the small trusted kernel to be re-typechecked, and they also end up in the proof output format, while definitions with (2) go to the compiler to be turned into VM bytecode. A definition with both (1) and (2) gets both kernel typechecked and compiled to VM bytecode.

Because tactics are meant to be run, they must have property (2), but they need not have property (1). In particular, since most of the core primitives are meta, including the type tactic itself, tactics are always meta meaning they lack property (1). But that doesn't mean that you can't use non-meta definitions, as long as they are computable. A good example of a library with both (1) and (2) is list A and the functions manipulating it. This is used in both proofs (for example, to define finiteness) as well as in computations (running functions to filter lists of hypotheses and the like).

When the lean elaborator hits a begin ... end block, it elaborates the contents of the block in a special parser mode into a tactic, typechecks it as a tactic unit (not using the kernel, just the elaborator's basic haskell-like typechecker), compiles it to bytecode on the spot (so it needs to be computable, i.e. property (2)), and then runs it, whereupon the tactic will fill in the hole at the location of the begin ... end with a term (which may be non-meta, and is required to be if the definition itself is non-meta).

[Mario Carneiro]

Kyle Miller said:

The stuff about a VM is purely optimization. Since meta definitions don't take part in mathematical truth, it's OK to evaluate such code in a faster way, even if the VM might be less trusted to be correct.

Unfortunately it's not that simple. For definitions in both (1) and (2), we can say that the VM implementation (2) is just an optimization on the semantics (1), but there are definitions in (2) that don't even have a semantics in (1) and for those we have to just take the VM behavior as defining the meaning of the term.

[Mario Carneiro]

In particular, for definitions in (1) and (2) one property we have not proven but believe to be true (and will take steps to ensure) is that the VM will only ever compute a function in accordance with what the theory says it should, i.e. if the VM says f a = b then you can prove that in the kernel. There are lots of reasons why this is hard to state precisely much less prove, though.

[Mario Carneiro]

Kyle Miller said:

I couldn't find the process by which the outer layer checks the types of its meta definitions. I'm guessing there is some provision in the Lean kernel for this.

The lean elaborator has its own typechecker, basically a more complicated version of the kernel typechecker that includes support for metavariables, typeclass inference, tactic running and the like. There are terms that typecheck in the kernel but not the elaborator and vice versa.

[Mario Carneiro]

Chris M said:

"In some sense, all the meta keyword does is disable termination checking."
This I still don't really understand. It seems to me that it also completely changes the way that the Lean compiler deals with it?

Hopefully what I've said above makes this clearer, but to directly address this point: Because meta determines whether the term has property (1) or not, the compiler actually doesn't care about it at all. The elaborator cares about it because it allows it to relax some checks, and the kernel cares about it because it won't see a meta definition at all while it will be asked to typecheck a non-meta definition, but the compiler will do the same thing on a meta definition as on a non-meta definition.

[Kyle Miller]

@Mario Carneiro Thanks for elaborating about the elaborator. That's interesting there's a sort of parallel implementation of a typechecker. To check: once it passes the elaborator's typechecker, it's "correct," but then the elaborated term is certified by the kernel? (Barring complications you mentioned about terms that check in one but not the other, and vice versa.)

[Mario Carneiro]

Yes, the elaborator typechecker is at the level of "if it's not correct the user will get a really messy looking error so we'd really like it to be correct" rather than "if it's not correct then lean and possibly mathematics is fundamentally broken"

[Chris M]

@Mario Carneiro, is there a more detailed explanation of the elaborator typechecker somewhere?

Also, I thought "compiler" refers to the entire collection of parser, elaborator, kernel, etc. But does it only refer to the process of compiling to bytecode for evaluation?

[Mario Carneiro]

I'm using "compiler" to refer specifically to the lean -> bytecode compiler. It's true that sometimes we also use the term "lean is compiling" for the overall process but it's more like a typechecker than a compiler at that level

[Mario Carneiro]

As for a more detailed explanation of the elaborator, nope it's just a whole mess of code that does what it does. I can give more specifics about parts of it if you want though

[Mario Carneiro]

(I should note that I learned most of what I know about the elaboration process by watching its behavior from the outside. I've done very little C++ hacking on it)

[Chris M]

Ok the specific question I have is: you suggested that the elaborator's type checker has knowledge of CIC. I was a bit surprised by this, since I would guess that within begin ... end blocks, it doesn't need any knowledge of this, since the types are things like tactic unit and tactic expr.

[Chris M]

Is it correct that the elaborator only needs knowledge of CIC in order to fill in implicit variables?

[Mario Carneiro]

tactic unit isn't making a lot of use of CIC but it's there. tactic : Type -> Type and unit : Type, this is an application and you have to match the types

[Mario Carneiro]

If you wanted to you could use a fancy dependent type for data structures in tactics, but it's not done most of the time because it isn't necessary

[Mario Carneiro]

But look to haskell to see uses for various kinds of near-dependent types in programming applications

[Kyle Miller]

Doesn't the evaluation of a tactic involve elaborating the constructed terms?

[Mario Carneiro]

There is a tactic called to_expr : pexpr -> tactic expr that can be used to explicitly invoke the elaborator on a pre-term, but you don't have to use it

[Mario Carneiro]

A tactic is responsible for producing fully elaborated terms, but it can also invent them from whole cloth. For example, norm_num and ring do this for efficiency reasons

[Chris M]

By "fully elaborated" you mean, no implicit arguments?

[Mario Carneiro]

No metavariables

[Mario Carneiro]

Actually that's not quite true, a tactic can produce terms with metavariables but usually it will add them as subgoals before returning

[Mario Carneiro]

if it doesn't you get a very user unfriendly error "term contains metavariables" which is not associated to the tactic

[Kenny Lau]

we've all learnt how the elaborator works without ever seeing the code

[Chris M]

metavariables are the sequence ?M_1, ?M_2, ..., is that right?

[Mario Carneiro]

That's how they get printed, yes

[Chris M]

Is it correct to say that the kernel has an understanding of implicit arguments but not of meta variables?

[Kyle Miller]

Here's something I've been wondering: when exactly does a begin ... end block execute? I've been assuming Lean attempts to elaborate everything possible until it gets stuck in some sense, and then at this point it executes these blocks. But, you're saying "term contains metavariables" is an error, so maybe getting stuck is not allowed: it has to be able to elaborate everything outside these blocks first.

[Mario Carneiro]

Here's an example of a tactic that puts a metavariable in the term without making a goal for it, and as a result it appears to work fine but you get an error at the very end

meta def bad_tac : tactic unit :=
do tactic.split,
  g::gs ← tactic.get_goals,
  tactic.set_goals gs

example (p q : Prop) (h : q) : p ∧ q :=
begin
  -- ⊢ p ∧ q
  bad_tac,
  -- ⊢ q
  exact h,
end -- tactic failed, result contains meta-variables

[Chris M]

Chris M said:

Is it correct to say that the kernel has an understanding of implicit arguments but not of meta variables?

To rephrase this, is it correct to say that after elaboration is finished, the elaborator has replaced all begin ... end blocks with proof terms, and has filled in all meta variables and implicit arguments?

[Mario Carneiro]

Implicit arguments are an indication to insert a metavariable at this place in the application, which will then be inferred by unification or typeclass inference

[Mario Carneiro]

A fully elaborated term contains no metavariables. It doesn't really make sense to say that they don't have implicit arguments because that's not a property of a term

[Mario Carneiro]

But basically yes

[Chris M]

Mario Carneiro said:

Here's an example of a tactic that puts a metavariable in the term without making a goal for it, and as a result it appears to work fine but you get an error at the very end

meta def bad_tac : tactic unit :=
do tactic.split,
  g::gs ← tactic.get_goals,
  tactic.set_goals gs

example (p q : Prop) (h : q) : p ∧ q :=
begin
  -- ⊢ p ∧ q
  bad_tac,
  -- ⊢ q
  exact h,
end -- tactic failed, result contains meta-variables

Is there a way to actually view the result that this tactic produces?

[Mario Carneiro]

Kyle Miller said:

Here's something I've been wondering: when exactly does a begin ... end block execute? I've been assuming Lean attempts to elaborate everything possible until it gets stuck in some sense, and then at this point it executes these blocks. But, you're saying "term contains metavariables" is an error, so maybe getting stuck is not allowed: it has to be able to elaborate everything outside these blocks first.

Tactics are evaluated after most other parts of elaboration (they are delayed as long as possible, so that as much information as possible is available). There can still be metavariables in the term

[Mario Carneiro]

example (p q : Prop) (h : q) : p ∧ q :=
begin
  tactic.result >>= tactic.trace, -- ?m_1
  -- ⊢ p ∧ q
  bad_tac,
  tactic.result >>= tactic.trace, -- ⟨?m_1, ?m_2⟩
  -- ⊢ q
  exact h,
  tactic.result >>= tactic.trace, -- ⟨?m_1, h⟩
end -- tactic failed, result contains meta-variables

[Kyle Miller]

Where exactly does the "term contains metavariables" happen? Is it at the end of a tactic block, or once all the tactic blocks are evaluated and the next stage detects metavariables still exist?

[Mario Carneiro]

I'm actually not entirely sure. I think at the end of the tactic block: the tactic is initialized with the metavariable corresponding to the hole at the location of the begin-end, and at the end it is required to have unified that metavariable with some term that does not contain metavariables (except possibly metavariables from the external context, i.e. in the type of the term?)

[Mario Carneiro]

example (p : nat → Prop) (h : ∀ x, p x) : ∃ x, p x :=
⟨_, begin
  apply h _,
end⟩ -- tactic failed, result contains meta-variables

[Kyle Miller]

@Mario Carneiro A quick reading of elaborator::invoke_tactic in lean/src/frontends/lean/elaborator.cpp suggests it's at the end of a tactic block.

[Mario Carneiro]

a quick test reveals the same

[Mario Carneiro]

or if you prefer

example (p : nat → Prop) (h : ∀ x, p x) : ∃ x, p x :=
begin
  split,
  exact begin
    apply h _
  end, -- tactic failed, result contains meta-variables
  exact 0,
end

[Chris M]

Johan Commelin said:

meta turns off termination checks for recursive calls.

I've been thinking more about this and want to test if I understand correctly what these "termination checks" are. Is the following correct?

By "termination checks" you are referring to the fact that Lean's type system doesn't allow for certain types of recursion. The halting problem is undecidable so Lean's recursion checking also rules out functions that halt, but basically it employs certain rules such that if the rules aren't satisfied, a term does not type check.

More specifically these rules are the following:

1. Definitions of functions on "normal" types (non-inductive types) are not allowed any recursion whatsoever.

2. Definitions of functions on inductive types are allowed to recurse "backward" along the constructors, meaning for example that if there is a constructor | intro : indType1 \to indType1 for inductive type indType1, then we can define a function f recursively by

def f : indType1 \to indType1
| intro (x) := f(x)
| ...

Where in the body of f(intro (x)) we are only allowed to use x and not any newly constructors of indType1

3. Any other recursion is forbidden without using the meta keyword.

[Mario Carneiro]

Note that (unlike Coq) Lean's foundations don't have any notion of a "termination checker". Instead, the termination checks are a consequence of the equation compiler, which gets a bunch of equations and tries to figure out how to turn them into recursor applications. If you improve the equation compiler, the termination checks can change

[Mario Carneiro]

The equation compiler actually tries a few different compilation strategies on your definition, in order of generality:

1. Definition by cases (non-recursive)
2. Structural recursion
3. Bounded recursion
4. Well founded recursion

Actually it doesn't really use (2) even though that's the simplest compilation strategy, which sometimes leads to problems when (3) and (4) don't apply. But most of the time when you write a recursive definition (3) is doing the work, and the rules for (3) essentially match your description. For (4), the rule is that any recursive calls must be less according to the provided well founded relation. This is good for definitions where f n depends on f (n / 2), for example.