mathport:whnf-power

Stream: lean4

[Daniel Selsam]

Meta was not able to type-check fin.coe_two, and it took me a while to figure out why. The short answer is that Lean4's whnf is more conservative than lean3's type_context.whnf or lean4's kernel. In particular,

1. the major premise of a recursor is no longer unfolded with TransparencyMode.all
2. constants (not applications) that are theorems are not unfolded (which prevented nat.lt_wf from exposing a constructor)

This means that well_founded is less likely to compute inside MetaM. Is this a big issue? If so, I suggest we just add the change to the mathlib4 fork of lean4.

[Mario Carneiro]

These kinds of computations were already problematic in lean 3

[Mario Carneiro]

With luck, there aren't too many explicit defeq evaluations of well founded recursive definitions

[Mario Carneiro]

Here's a fix for coe_two, but a lot of tactics make it hard to do this proof because they are eager to use rfl to close the goal. Probably it would be better to patch lean 3 to make it less aggressive

@[simp] lemma val_two {n : ℕ} : (2 : fin (n+3)).val = 2 :=
by have := @coe_val_of_lt (n+2) 2 (le_add_left 3 n); rwa [nat.cast_bit0, nat.cast_one] at this

@[simp] lemma coe_two {n : ℕ} : ((2 : fin (n+3)) : ℕ) = 2 := val_two

[Daniel Selsam]

Even if we don't make the change, I don't think anything needs to be back-ported for this one -- the auto-porter works fine (since this issue is in MetaM not the kernel), and strategy X can be used to prove these theorems in lean4 during the manual porting phase.

[Mario Carneiro]

I think these kinds of proofs should be avoided regardless (reduction of definitions by well founded recursion should work in all cases or not at all)

[Mario Carneiro]

which is why I am more inclined to label the lean 4 behavior as "right" and backport the limitations to lean 3. Unfolding and reducing proofs to make rfl work has no place in lean.

[Daniel Selsam]

I agree, though this policy could be adopted during the manual stage of the port. It is up to you whether to backport -- it would have the advantage that the delaborated proofs would already be good style (but I don't know how to estimate the cost of the backport)

[Mario Carneiro]

Reducing proofs doesn't work most of the time anyway because it doesn't take long before you run into an axiom like propext

[Mario Carneiro]

It would be interesting to investigate a reduction algorithm like the one in my thesis, where acc.rec is reduced by defeq replacing the major premise with an expression like acc.mk (acc.inv h) and using that to take another step

[Mario Carneiro]

this has the advantage that you never have to unfold proofs, but it doesn't necessarily terminate

[Daniel Selsam]

I made a github issue to track the backport: https://github.com/dselsam/mathport/issues/20