1
$\begingroup$

In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running #print on the internal definition that the compiler produces. It produces the following error:

16:12: type mismatch at application
  ᾰ.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
term
  λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0
has type
  nat.below (λ (ᾰ : ℕ), ℕ) 0 → ℕ : Type
but is expected to have type
  ?m_1 0 : Sort ?

Why is there an error when I'm just pasting code from the output of the Lean compiler? Is there some special context needed for internal definitions to be interpreted correctly? What is the best way to take an internal definition and convert it into something that will type check properly?

I'm using Lean 3.46 with lean-mode in Emacs.

The example code:

def leanfib : ℕ → ℕ
| nat.zero := nat.zero
| (nat.succ nat.zero) := (nat.succ nat.zero)
| (nat.succ (nat.succ n)) := (leanfib (nat.succ n)) + (leanfib n)

#eval list.map leanfib (list.range 12)
#print leanfib
#print leanfib._main

def «print of leanfib._main» : ℕ → ℕ :=
λ (ᾰ : ℕ),
  ᾰ.brec_on
    (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
       (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
          ᾰ.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
            (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ.succ),
               ᾰ.cases_on (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 1), id_rhs ℕ 1)
                 (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ.succ.succ),
                    id_rhs ℕ (_F.fst.fst + _F.fst.snd.fst.fst))
                 _F)
            _F)
         ᾰ
         _F)

EDIT: Jason Rute's answer and followup comments helped me find the right conversation on the Lean zulip chat forum to resolve my issue. Basically, if you are having trouble with "round trip" errors from the pretty printer, the first step is to activate an option: set_option pp.all true. After setting this option, the output of #print on that function becomes much much more verbose and complicated, but does typecheck correctly. I had a feeling that activating this option is in some sense applying "excessive force". After doing some digging in the source, it turns out that this is indeed that case: setting the "pp.all" option to true (as of version 3.46) is equivalent to setting the following:

set_option pp.implicit true
set_option pp.proofs true
set_option pp.coercions true
set_option pp.notation false
set_option pp.universes true
set_option pp.full_names true
set_option pp.beta false
set_option pp.numerals false
set_option pp.strings false
set_option pp.binder_types true
set_option pp.generalized_field_notation false

I was able to repair the "type-check-ability" of this example by combining the full force of "pp.all" with the lighter touch of setting "pp.generalized_field_notation" to false, which produces the following output:

def «print (with pp.generalized_field_notation=false) of leanfib._main» : ℕ → ℕ :=
λ (ᾰ : ℕ),
  nat.brec_on ᾰ
    (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
       (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
          nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
            (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ ᾰ)),
               nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 1), id_rhs ℕ 1)
                 (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ (nat.succ ᾰ))),
                    id_rhs ℕ (_F.fst.fst + _F.fst.snd.fst.fst))
                 _F)
            _F)
         ᾰ
         _F)

This is much simpler than what is produced by printing with "pp.all", but still has the error: invalid 'nat.cases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known. However, by looking at the big ugly term that gets printed with "pp.all" (which I haven't reproduced here because it is so big and ugly), I was able to determine the type of the lambda that encloses the term that produces the error. Then this version can be fixed by annotating that type, as follows:

def «repaired print (with pp.generalized_field_notation=false) of leanfib._main» : ℕ → ℕ :=
λ (ᾰ : ℕ),
  nat.brec_on ᾰ
    (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
       let t₁ : Π (ᾰ : ℕ), nat.below.{1} (λ (ᾰ : ℕ), ℕ) ᾰ → ℕ :=
       (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) ᾰ),
          nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 0), id_rhs ℕ 0)
            (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ ᾰ)),
               nat.cases_on ᾰ (λ (_F : nat.below (λ (ᾰ : ℕ), ℕ) 1), id_rhs ℕ 1)
                 (λ (ᾰ : ℕ) (_F : nat.below (λ (ᾰ : ℕ), ℕ) (nat.succ (nat.succ ᾰ))),
                    id_rhs ℕ (_F.fst.fst + _F.fst.snd.fst.fst))
                 _F)
            _F) in t₁ ᾰ _F)

In summary, the original term that got printed by the pretty printer was indeed close to the right thing. The version printed by using option "pp.generalized_field_notation" is even closer to the right thing, but still needs some type information. This type information can be obtained by looking at the version that gets printed by using "pp.all".

$\endgroup$

1 Answer 1

1
$\begingroup$

This is a known problem in Lean 3. Output from the pretty printer will sometimes not parse back into Lean. You can find a lot about this on the Lean Zulip discussed as the round-trip issue with the pretty printer. I heard it will be better in Lean 4 and at least there used to be notes about it in the delaborator code for Lean 4.

Edit: Applying set_option pp.all true can often lead to output which is parsable, although incredibly verbose.

However, if you find a specific thing which is broken in Lean 3, I would file a GitHub issue at https://github.com/leanprover-community/lean. I’ve heard some issues are hard to fix, but others might be a one line change if you file an issue with a MWE.)

$\endgroup$
5
  • $\begingroup$ If you can recall where the issue was discussed that would be helpful to me, that way I could go learn more about the issue. For example, it might help me understand how to modify the definition of «print of leanfib._main» so that it can typecheck. Basically, I'm trying to understand what the equation compiler produces behind the scenes. Presumably whatever it is printing is pretty close to the correct thing, but just a tiny bit off. $\endgroup$
    – ttbo
    Aug 17, 2022 at 5:19
  • $\begingroup$ Honestly, you would benefit from moving this conversation from here to the Lean Zulip so you can have a back and forth with the maintainers, but here is one place it was discussed a while ago: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/…. But in general search for “round-trip” and “round trip” on the Lean Zulip. $\endgroup$
    – Jason Rute
    Aug 17, 2022 at 9:40
  • $\begingroup$ Actually here are two more recent discussions: leanprover.zulipchat.com/#narrow/stream/113489-new-members/…, leanprover.zulipchat.com/#narrow/stream/113489-new-members/… $\endgroup$
    – Jason Rute
    Aug 17, 2022 at 9:59
  • $\begingroup$ Thanks, these links helped me resolve my problem completely. I edited the question to describe how I resolved the problem with the information I found. $\endgroup$
    – ttbo
    Aug 18, 2022 at 20:06
  • $\begingroup$ I should have mentioned pp.all in my answer. I just updated it, but I’m glad you found your solution. $\endgroup$
    – Jason Rute
    Aug 18, 2022 at 20:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.