chore: adaptations for nightly-2024-05-11 #12853
Conversation
| @@ -779,6 +780,7 @@ theorem zero_ne_one' [NeZero n] : (0 : Fin (n + 1)) ≠ 1 := Fin.ne_of_lt one_po | |||
|
|
|||
| #align fin.succ_zero_eq_one' Fin.succ_zero_eq_one | |||
|
|
|||
| unseal Nat.modCore in | |||
There was a problem hiding this comment.
I'm not particularly happy with this. How would I discover the need to add this unseal, after seeing the rfl fail on @Eq (Fin (n✝ + 1 + 1).succ) (succ 1) 2?
There was a problem hiding this comment.
I'm not happy either. Any ideas?
We could just make Nat.modCore semireducible again, of course.
Or try harder to make Nat.mod reduce when the first argument is any fully known value and it's reducibly smaller than the second.
There was a problem hiding this comment.
Or use a structurally recursive definition of Nat.mod (with fuel)
There was a problem hiding this comment.
Ah, I think I found the snag why I couldn’t make that work initially. I tried
def mod' (n m : Nat) := match n with
| 0 => 0
| _ => if n < m then n else Nat.modCore n m
but it wouldn’t reduce where I wanted it to.
I now see why. Note that
example : decide (m+3 ≤ 2) = false := rfl -- does not work
example : decide (2 < m+3) = false := rfl -- works
So
def mod' (n m : Nat) := match n with
| 0 => 0
| _ => if m ≤ n then Nat.modCore n m else n
might do what we want (namely reduce when n is 0, or when n is known and m is known enough.) The definition of modCore should have given me a hint. Will try.
There was a problem hiding this comment.
Thanks for nudging me to try harder, I think I found the right magic incarnation to make this work:
leanprover/lean4#4145
There was a problem hiding this comment.
Okay, we will wait on this PR until nightly-2024-05-14 lands containing leanprover/lean4#4145!
In leanprover/lean4#4061, well-founded definitions become irreducible by default, and hence some `rfl` proofs stop working. This pre-emptively backports some of the adaptations from #12853.
this refined upon #4098 and makes `Nat.mod` reduce on even more literals. The key observation that I missed earlier is that `if m ≤ n` reduces better than `if n < m`. Also see discussion at leanprover-community/mathlib4#12853 (comment)
this refined upon #4098 and makes `Nat.mod` reduce on even more literals. The key observation that I missed earlier is that `if m ≤ n` reduces better than `if n < m`. Also see discussion at leanprover-community/mathlib4#12853 (comment)
|
I'll open a new PR now that we're at nightly-2024-05-14. |
In leanprover/lean4#4061, well-founded definitions become irreducible by default, and hence some `rfl` proofs stop working. This pre-emptively backports some of the adaptations from #12853.
In leanprover/lean4#4061, well-founded definitions become irreducible by default, and hence some `rfl` proofs stop working. This pre-emptively backports some of the adaptations from #12853.
These are mostly adaptations for leanprover/lean4#4061.
Some are no problem:
rflproofs that no longer work, and we replace with proofs by the appropriate lemmas.But I think the cases where we use
unsealmight need further attention.