show_term fails while tactic doesn't

Stream: lean4

[Jun Yoshida]

I am confused about proof-by-term and proof-by-tactic, so let me ask some beginner questions.
I thought that "genuine proofs" are written in terms of terms while tactics are a kind of scripts generating them.
But now, I am a little bit unsure about it seeing the following code where show_term fails in two different levels:

import Std.Tactic.Basic

def f : Nat → Nat
| 0 => 0
| n+1 => n

-- "Try this" fails
theorem f_def : f = fun n => n.casesOn 0 id :=
  show_term by rfl

-- `show_term` itself fails
theorem f_apply (n : Nat) : f n = n.casesOn 0 id :=
  /- show_term -/ by dsimp [f, f.match_1]

My questions are

• Why do these show_term fail?
• Can we write the proofs of f_def and f_apply above without use of tactics?
• I don't doubt the soundness, but why is the failure of show_term acceptable in this point of view?

[Mario Carneiro]

show_term is not really at fault here, it is elaboration that is acting strangely

[Mario Carneiro]

this proof works:

theorem f_def : f = fun n => n.casesOn 0 id :=
  by delta f f.match_1; exact rfl

but removing the delta fails

[Mario Carneiro]

I believe the reason is because these definitions have "smart unfolding" lemmas (f._sunfold) which, when present, suppress unfolding of the unapplied constant

[Jun Yoshida]

I see delta does the trick in f_apply too:

theorem f_apply' (n : Nat) : f n = n.casesOn 0 id :=
  show_term by delta f f.match_1; exact rfl

Why doesn't show_term go well with dsimp?

[Mario Carneiro]

it's not show_term, it is the re-elaboration of the term that is the issue

[Mario Carneiro]

The output of all of these tactics is the term Eq.refl f, but if you ask the elaborator to prove that Eq.refl f is a proof of f = fun n => n.casesOn 0 id it fails (even though it really is a proof of this and the kernel will agree)

[Mario Carneiro]

because it refuses to unfold f unapplied

[Damiano Testa]

Does adding set_option pp.all in before show_term give something that works?

[Mario Carneiro]

the story is similar for f n = ... instead of f = ..., the smart unfolding lemma says not to unfold f _ unless _ unifies against one of the patterns, here 0 and n+1

[Mario Carneiro]

no it won't help, the term is just Eq.refl f and there is no hidden argument in there other than the type

[Jun Yoshida]

@Mario Carneiro Do you mean Term.elabTermEnsuringType in the implementation of show_term?

local elab (name := showTermImpl) tk:"show_term_impl " t:term : term <= ty => do
  let e ← Term.elabTermEnsuringType t ty
  Term.synthesizeSyntheticMVarsNoPostponing
  addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
  pure e

[Mario Carneiro]

regarding the second example of a failure in show_term, it's actually the no_implicit_lambda% combinator that is failing

[Mario Carneiro]

I don't see a particularly good reason for this, but I think the elaborator wasn't expecting to end up in this position and it's possible that one of these methods ends up re-asserting the type and failing by surprise

[Mario Carneiro]

note that this also fails

theorem f_apply (n : Nat) : f n = n.casesOn 0 id :=
   no_implicit_lambda% (by dsimp [f, f.match_1])

[Mario Carneiro]

oh wait, no the dsimp doesn't close the goal

[Mario Carneiro]

theorem f_apply' (n : Nat) : f n = n.casesOn 0 id :=
  show_term by dsimp [f, f.match_1]; rfl

works

[Mario Carneiro]

it seems that dsimp doesn't close rfl goals wrapped in a noImplicitLambda annotation

[Jun Yoshida]

I also checked that replacing show_term with (redefined) show_term_impl also works in f_apply. Can you explain what no_implicit_lambda% does and why show_term uses it?

[Mario Carneiro]

no_implicit_lambda% prevents elabTerm from automatically introducing lambdas when the goal is an implicit forall type like \forall {x : Nat}, x = x

[Jun Yoshida]

Thank you, I think I now understand the reason of the error in f_apply example.
And as for my second question, it seems no way to write the proof of f_def without tactics. Is there any way to say "please unfold this definition" in the term-mode?

[Mario Carneiro]

delta% could conceivably be a term elaborator, but otherwise I think not

[Jun Yoshida]

So, I have to correct my naive picture about proof-by-term vs proof-by-tactic in the first post.

• The former is strictly weaker than the latter in view of the ability for proofs.
• This is because tactics not only generate terms but also convince the kernel of definitional equality.
• The full provability in the theoretical type system of Lean is available only with tactics.

Are they all right?

[Patrick Massot]

No. You are confusing the elaborator and the kernel

[Henrik Böving]

The theory behind Lean has no idea about tactics, tactics, at their core, generate terms of type docs#Lean.Expr which get typechecked by the kernel. In theory you can write these terms out yourself as well, always.

[Mario Carneiro]

When you write terms in the source language, they are being elaborated and typechecked by the elaborator. This is the one that gives you the nice errors and has support for unification, inference and so on. Both term mode and tactic mode are mechanisms for talking to the elaborator, they just have slightly different syntax. Once the elaborator has decided everything is okay it creates a term and sends it to the kernel, which typechecks the term again. For the elaborator to be correct, its typechecker needs to be an underestimate of what the kernel can accept, but it need not be exactly the same, and there are some cases where it deliberately hides a definitional equality that the kernel would accept, such as when you assert an @[irreducible] def is equal to its unfolding.

[Mario Carneiro]

If you write a tactic or term elaborator yourself, you can choose to bypass the normal elaborator procedure and produce a term for the kernel directly without typechecking it. In this case you can get around the additional limitations of the elaborator's typechecker, but if you produce something the kernel doesn't accept then it will produce a relatively low level error and someone will report a bug in your tactic. This is a useful technique if you know your tactic will produce well typed terms and you don't want to pay the cost of two typechecks. ring does this because it produces potentially large terms that are correct by construction, and delta also does this to unfold irreducible defs and the like.

[Joachim Breitner]

So is there a source syntax for terms that get fed to the kernel directly and only?

[Jun Yoshida]

@Mario Carneiro Thank you very much for the very detailed explanation. Now I see my confusion very clearly. The points are

• Any elaborator may introduce additional layer of validity, and even the default term elaborator used by def/theorem does; such as the transparency of definitions. This seems reasonable to me in view of Lean as a programming language.
• As a result, a term elaborator may reject a term syntax tree because of this layer even if it is equivalent to a Lean.Expr tree which is valid from the kernel point of view.
• In my example, it is not the kernel but the term elaborator that reject the proof of f_def and f_apply. Because f.match_1 has a special kind of transparency, maybe?
• With tactic, it is easier to control validity layers than the default term elaborator; e.g. delta, unfold, dsimp, ... But the result value is anyway of type Lean.Expr. It doesn't matter for the kernel whether it is created by a term elaborator, by tactic, or else.

[Jun Yoshida]

Oh, my post is almost just rephrasing of yours. But it means I am finally right?

[Mario Carneiro]

Because f.match_1 has a special kind of transparency, maybe?

It has a "smart unfolding lemma", used for match expressions, which when present causes the elaborator to only unfold when the discriminant has the form of one of the patterns

[Mario Carneiro]

The point of this mechanism is to avoid unfolding a + b into some brecOn mess during unification, and unfold a + succ b to succ (a + b) instead of succ <brecOn nonsense>

[Jun Yoshida]

Thank you for supplementary comment. That "smart unfolding" is reasonable from some point of views. It also prevents f (n+1) from becoming Nat.rec 0 (fun n _ => n) and keeps the reasonable form of the term using f. Even though it is the culprit in the f_def example, I don't want to see such a raw recursor so often in my daily proof writing.