Zulip Chat Archive

Stream: lean4

Topic: mathport:whnf-power


Daniel Selsam (Mar 20 2021 at 21:14):

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 (Mar 20 2021 at 21:48):

These kinds of computations were already problematic in lean 3

Mario Carneiro (Mar 20 2021 at 21:49):

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

Mario Carneiro (Mar 20 2021 at 21:57):

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 (Mar 20 2021 at 22:36):

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 (Mar 20 2021 at 22:53):

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 (Mar 20 2021 at 22:55):

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 (Mar 20 2021 at 22:56):

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 (Mar 20 2021 at 22:56):

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 (Mar 20 2021 at 22:58):

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 (Mar 20 2021 at 22:59):

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

Daniel Selsam (Mar 20 2021 at 23:32):

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


Last updated: Dec 20 2023 at 11:08 UTC