Is this equality definitional?

Stream: general

[Mike Shulman]

I'm stumped by the following in Lean 3 (haven't tried Lean 4):

def weird_zero : ℕ → ℕ → ℕ
| 0 0 := 0
| 0 (n+1) := weird_zero 0 n
| (m+1) 0 := weird_zero m 0
| (m+1) (n+1) := weird_zero m n

#eval weird_zero 0 0 -- yields 0
#reduce weird_zero 0 0 -- yields 0

def test : weird_zero 0 0 = 0 := rfl -- fails

I suppose it must be something to do with the simultaneous/nested recursion on m and n, since replacing either the 0 (n+1) or (m+1) 0 clause with 0 makes it work. But I can't guess how that can matter, because regardless of whatever strange kind of recursion is going on behind the scenes, weird_zero 0 0 is a concrete closed term that normalizes to 0 with either eval or reduce. So why doesn't it likewise get normalized in the definition of test?

[Mauricio Collares]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Base.20case.20of.20recursive.20definition sounds related

[Mike Shulman]

Yes, that seems to be the same issue. But the discussion there doesn't explain to me how weird_zero 0 0 can reduce to 0 with eval and reduce, yet rfl doesn't typecheck at weird_zero 0 0 = 0. It's contrary to all my experience with other dependent-type-theory-based proof assistants. It's not as if rfl is some weird tactic that's doing some fancy stuff that isn't invariant under definitional equality or doesn't notice definitional equality. I mean, maybe it is, but writing the explicit term eq.refl 0 also fails.

[Mike Shulman]

Is weird_zero 0 0 definitionally equal to 0 or not?

If so, then it seems that Lean's typechecking does not respect definitional equality, since weird_zero 0 0 = 0 is definitionally equal to 0 = 0, but eq.refl 0 has the latter type and not the former.

If not, then it seems that eval and reduce are doing some sort of "generalized computation" that doesn't preserve definitional equality. Which, I suppose, is a thing that one could do. But then there ought to be some other command that only performs definitional computations, right?

[Mauricio Collares]

AFAIK, #eval runs in the VM, while #reduce runs in the kernel. But see Mario's message at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/not.20p.20versus.20p.20implies.20false/near/209606830 for a possible reason for rfl failing in cases where definitional equality holds.

[Mike Shulman]

Thanks for the link. But Mario explicitly says that Lean's definitional equality check is semantically equivalent to reducing both sides to a normal form. So since in this case both sides have the same normal form 0, shouldn't they should be judged as equal by the definitional equality checker whatever other fancy stuff it's doing?

[Mauricio Collares]

You're right, my bad. I'll wait for the experts to answer :)

[Jason Rute]

haven't tried Lean 4

For what it's worth, your weird_zero doesn't compile in Lean 4 as is:

def weird_zero : Nat → Nat → Nat -- termination error
| 0, 0 => 0
| 0, (n+1) => weird_zero 0 n
| (m+1), 0 => weird_zero m 0
| (m+1), (n+1) => weird_zero m n

I get the error:

fail to show termination for
  weird_zero
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    weird_zero 0 n

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    weird_zero m 0

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

[Adam Topaz]

FWIW I tried the pascal example from the other thread in lean4 and got similar behaviour. (Presumably wierd_error will behave similarly if you provide the termination proof.)

[Mike Shulman]

Coq doesn't accept it either, but Agda does.

[Jason Rute]

Ok, this works in Lean 4:

def weird_zero (n m : Nat) : Nat :=
match n, m with
| 0, 0 => 0
| 0, n+1 => weird_zero 0 n
| m+1, 0 => weird_zero m 0
| m+1, n+1 => weird_zero m n
termination_by weird_zero n m => (n, m)

#eval weird_zero 0 0 -- yields 0
#reduce weird_zero 0 0 -- yields 0

def test : weird_zero 0 0 = 0 := rfl -- passes

[Jason Rute]

(I copied the code from this example. I still have no idea how the termination checker works.)

[Mike Shulman]

Ok, that's fairly nice. I'm still curious what's going on in Lean 3, though.

[Leonardo de Moura]

For more information about termination_by:
https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html#well-founded-recursion-and-induction

[Leonardo de Moura]

The Lean 3 version is also using well founded recursion. You can use the #print command to see how the frontend compiled the declaration.

[Mike Shulman]

#print weird_zero gives me

def weird_zero : ℕ → ℕ → ℕ :=
weird_zero._main

[Mike Shulman]

What I really want to know is why eq.refl 0 doesn't typecheck at weird_zero 0 0 = 0.

[Jason Rute]

@Mike Shulman You can print weird_zero._main (and so on ...) but it gets pretty hairy.

[Leonardo de Moura]

We have to keep going:

#print weird_zero._main
#print weird_zero._main._pack
/-
def weird_zero._main._pack : Π (_x : Σ' (a : ℕ), ℕ), (λ (_x : Σ' (a : ℕ), ℕ), ℕ) _x :=
λ (_x : Σ' (a : ℕ), ℕ),
  well_founded.fix _
    (λ (_x : Σ' (a : ℕ), ℕ),
       psigma.cases_on _x
         (λ (fst snd : ℕ),
            nat.cases_on fst
              (nat.cases_on snd
                 (id_rhs ((Π (_y : Σ' (a : ℕ), ℕ), has_well_founded.r _y ⟨0, 0⟩ → ℕ) → ℕ)
  ...
-/

[Mauricio Collares]

I also want to understand the answer to Mike's question, to be honest: If #reduce weird_zero 0 0 returns 0, why does rfl not prove weird_zero 0 0 = 0? Is #reduce doing more powerful things? If so, is there a #command to "emulate" what the kernel is doing?

[Jason Rute]

The plot gets stranger: In the Lean 3 official online editor (which I assume is running 3.4.2) it again works. The rfl succeeds. So whatever is broken is broken in the community version of Lean 3.

[Leonardo de Moura]

Mike Shulman said:

What I really want to know is why eq.refl 0 doesn't typecheck at weird_zero 0 0 = 0.

The #reduce and the frontend type checker are using different settings to decide which declarations can be delta reduced.
#reduce uses transparency_mode::All and will reduce even theorems if needed. Since weird_zero is defined using well-founded recursion, theorems needed to be reduced. The type checker in the Lean 3 frontend is using a more conservative setting in the community version. I think this was an intentional change in the community version to address nasty performance issues. @Gabriel Ebner do you remember the issue?

[Mauricio Collares]

I've verified that Mike's example works in Lean 3.28.0 and not in Lean 3.29.0, so I think a relevant PR is https://github.com/leanprover-community/lean/pull/562 ("backport(type_context.cpp): wf should not compute"), but perhaps this is orthogonal to the transparency issue above (all I could find for that was https://github.com/leanprover-community/lean/pull/211, but this landed way earlier)

[Mauricio Collares]

It's a bit unexpected that this is a backport and yet the equivalent example works in Lean 4

[Mike Shulman]

Hmm, interesting. Is there a way for the user to alter the attributes or settings so that rfl will work?

[Matt Diamond]

this may be the relevant thread for the PR Mauricio linked: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport.3Awf-refl

[Mario Carneiro]

The issue was that we don't want proofs to be computed to a normal form because they aren't designed for such anyway. We would end up with some weird incentives to avoid propext and other axioms (which will block computation)

[Mario Carneiro]

Basically, "every closed term of nat normalizes to a numeral" is just false for lean as actually practiced

[Mario Carneiro]

Even before that PR, wf reduction was really flaky because of these issues

[Mario Carneiro]

To reiterate an example I used recently:

set_option pp.all true
#check show ℕ, from eq.rec_on (eq_true_intro (@id true)) 2 -- closed term of type ℕ
#reduce show ℕ, from eq.rec_on (eq_true_intro (@id true)) 2
-- @eq.rec.{1 1} Prop (true → true) (λ (_x : Prop), nat) (nat.succ (nat.succ nat.zero)) true
--   (@propext (true → true) true
--      (@iff.intro (true → true) true (λ (hl : true → true), true.intro) (λ (hr a : true), a)))

Even if we reduce proofs, we get stuck whenever any axioms are used. Definitions by well founded recursion are often susceptible to variants on this if the proof of well foundedness uses simp or rw

[Mike Shulman]

So many things go wrong when you don't have univalence... (-:O

[Mario Carneiro]

Or you can just use theorems for rewriting. simp proves this just fine

[Mario Carneiro]

It's impossible to have all the definitional equalities you would like, unless you accept an extensional type theory. m + 0 = m and 0 + m = m are equally true to any mathematician

[Mario Carneiro]

I personally think that we should put as little weight on the DTT side of things as we can. You have to really contort the mathematics to fit into the framework even if you invest in an expansive and useful defeq

[Mario Carneiro]

and the underlying theory becomes monstrously complicated when you go that route

[Mario Carneiro]

After spending a while on these kinds of systems, it's amazing to me how much this is just a non-issue in HOL based systems

[Mike Shulman]

I didn't mean to start an argument, just making a tongue-in-cheek observation. (-:

[Mike Shulman]

FWIW, your example of m + 0 = m and 0 + m = m can both be made to hold definitionally using nu-equality or rewriting type theory. But I think what it actually illustrates is the folly of conflating definitional equality with mathematical equality. They are equally true to any mathematician, and indeed they are equally propositionally true in DTT.

[Mike Shulman]

So if all you want to do is formalize set-based mathematics, then perhaps indeed there's not much use for dependent types or definitional equality. Those of us who want to do higher-typed mathematics do seem to need the latter. But even apart from that, definitional equality is foundational to the computational interpretation of DTT as a programming language. I ran into this issue because I'm teaching a class using Lean with a lot of computer science students in it, and so we're doing some basic functional programming, and for that purpose it's important to actually have things compute.

[Mike Shulman]

It's very weird if you write a program that computes when you run it, but when you start trying to prove things about it, it doesn't compute any more during your proof!

[Mario Carneiro]

I'd love to have a tactic that will prove that a computation under the VM erasing map preserves propositional equality, but as far as I can tell that would need no less than full HoTT style reasoning

[Mario Carneiro]

because you can get casts and casts upon casts and so on

[Mike Shulman]

Mario Carneiro said:

as far as I can tell that would need no less than full HoTT style reasoning

The solution seems obvious to me... (-:O