lean4lean: bump to bce3448, and a request to reconsider tutorial/096-097

[digama0]

Bumps the lean4lean checker to bce3448 (fixing a performance issue on mathlib test).

---

Separately, we think tutorial/096_projMaybeProp and tutorial/097_projMaybePropPast should be either rather
than accept. The new version will continue to reject them.

tutorial/096_projMaybeProp

lean4lean rejects this one deliberately, and we would like to argue the question is unsettled
rather than that we are incomplete.

The tutorial's own text for 095_MaybeProp states the rule we are applying:

The recursor eliminates into Prop only, since the kernel cannot rule out that MaybeProp is a
proposition. Whichever way a kernel answers that question while checking this declaration, it has
to answer it the same way when the fields are projected out again (projMaybeProp) — the
exemption that lets a proposition carry fields from any universe and the ban on projecting data
out of one are a matched pair.

The kernel answers "it might be a proposition" when it generates the recursor:

MaybeProp.rec : {motive : MaybeProp → Prop} →
  (∀ (field : PUnit) (proof : field = field) (tail : True), motive (MaybeProp.mk field proof tail)) →
    ∀ (t : MaybeProp), motive t

Accepting projMaybeProp answers the opposite way at the projection. fun x => x.0 cannot be
written with that recursor — the motive would have to be fun _ => PUnit.{u}, of type
MaybeProp → Sort u, and Lean's own kernel rejects the attempt with application type mismatch.
So under the expected outcome, Expr.proj computes something the type's own eliminator cannot.
lean4lean declines to be more powerful at proj than at rec, which is why it tests
isNeverZero where Lean tests !isAlwaysZero.

We are not claiming Lean is unsound here. The soundness argument in the test description is
correct: the field bound u ≤ u survives instantiation, so wherever the structure is a
proposition its fields are too. The claim is only that a kernel may reasonably answer this either
way, which is what either is for — compare nested-nonuniform-param, whose description says
that since it is not a demonstrated unsoundness "it is not settled whether a checker should accept
or reject it".

There is also a third position that is consistent in the other direction: let recursor generation
eliminate large whenever every constructor field's universe is bounded by the inductive's — which
is precisely the fact that makes this projection sound. Then MaybeProp.rec would be
large-eliminating and projMaybeProp would be spellable, and both checks would accept. That is a
change to recursor generation rather than to the projection rule, which is part of why we think
the present situation is an open question rather than a defect on either side.

tutorial/097_projMaybePropPast

This one we ask for as a consequence, and we want to be candid that it is weaker.

In isolation, fun x => x.2 : MaybeProp.{u} → True is expressible with the recursor — True is
a proposition, so motive := fun _ => True is fine, and Lean accepts
MaybeProp.rec (motive := fun _ => True) (fun _ _ tail => tail) x. lean4lean rejects it only
because infer_proj walks the constructor telescope generically: reaching field 2 means
substituting x.0 into proof's type first, even though the result type True does not depend
on it.

But that is exactly what the test's own description says:

A kernel that rejects projMaybeProp therefore rejects this one as well, at field 0 rather than
at field 2.

So it is a rider on 096 rather than an independent question, and scoring both charges the same
choice twice. If 096 stays accept then 097 should too, and we will simply fail both.

Either outcome is fine by us — if you would rather keep both as accept and have the divergence
recorded on our side, we have already documented it in lean4lean's divergences.md.

[nomeata]

That's a good discussion, but a bump PR isn't quite the right place.

I expect we will revisit some of these questions proper in the near future and make it less ambiguous what lean kernels should support and what not. Until then I suggest to support no less than what the official kernel supports (so that proof and meta code out there can rely on it).

If there is behavior that is

• more permissive than lean's (or more restictive in clearly not practically relevant ways)
• very plausibly sound
• desirable in some other way (e.g. easier to implement, verify or just more consistent)

then I'm game to labeling such behavior difference as expected: either (and maybe move it out of the kernel). If your proposed changes fit the bill, then please do open a PR for that.

[digama0]

• Most of lean4lean's divergences are making it more restrictive than lean, not less. That's the nature of writing a kernel which only accepts things with a good soundness story. I think if you aren't going to test broken preludes then you also shouldn't mandate weird behavior like this through the test suite.
• The difference here is obviously not practically relevant - the elaborator won't even let you write structures which are sometimes prop and sometimes not:

/--
error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
  Sort u

Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`
-/
#guard_msgs in
structure Wrap (α : Sort u) : Sort u where
  val : α 

• This is more consistent in that it refuses projections that are not expressible using eliminators.

As mentioned, the alternative is to relax the restrictions on inductives, but this will change the generated recursors so I don't want to unilaterally make such a change as it will cause lean imports to become unreadable by lean4lean. If you make the change in lean I'll update lean4lean correspondingly.

[nomeata]

This means leanprover/lean4#14893 wouldn't fly anymore, right?

[nomeata]

At least for cases like Wrap or PSigma' I agree that the recursor is simply unnecessary restrictive; my personal opinion is that this should be lifted. This would resolve the projections-are-stronger-than-eliminator tension in the nice way. Great!

Of course you want to stay compatible, but there are ways to do that. E.g. a flag. Or, if you want the proof to apply, generate a T._rec_as_it_should_be and T.rec becomes the ore limited lean version.

There are probably more ways for you to not feel blocked by the arena tests checking for the official behavior. But if it makes you happy, please do submit a PR that moves these checks out of the tutorial and into new tests marked either; this is not worth arguing about.