Nat.le backport

Stream: mathlib4

[Scott Morrison]

I've been investigating backporting Lean4's version of Nat.le to Lean3.

protected def ble : ℕ → ℕ → bool
| 0     0     := tt
| 0     (m+1) := tt
| (n+1) 0     := ff
| (n+1) (m+1) := ble n m

protected def le (n m : ℕ) : Prop := nat.ble n m = true

Mostly it is fairly straightforward, but one annoying change is that we can no longer call cases h on a h : x ≤ 0 hypothesis. I worry that this difficulty is going to propagate throughout mathlib.

There's a related problem with induction h when h : x ≤ y, but this one might be solvable with a custom recursor.

[Scott Morrison]

What I've done so far is on the nat.le branch of https://github.com/leanprover-community/lean

[Scott Morrison]

library/init/data/nat/basic.lean has been fixed, but library/init/data/nat/lemmas.lean is still pending a knowing what to do with cases and induction.

[Scott Morrison]

(Linking to the previous discussion of this at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mario's.20FMM.202021.20talk/near/247742724.)

[Scott Morrison]

If anyone has a suggestion for an ergonomic replacement for the cases h step that would be great.

[Scott Morrison]

I could add/find a eq_zero_of_le_zero and call cases on that.

[Ruben Van de Velde]

cases le_zero_iff.mp h, seems to work too

[Scott Morrison]

Indeed. Using @Ruben Van de Velde's suggestion, and replacing one use of induction, Lean3 compiles with the backported definition.

[Scott Morrison]

https://github.com/leanprover-community/lean/pull/603

[Scott Morrison]

This should not be merged until there's a branch of mathlib that actually works with it. :-) mathlib uses induction on inequalities a lot, unfortunately.

[Scott Morrison]

I wanted to get some advice on the Nat.le backport.

We recently merged https://github.com/leanprover-community/lean/pull/603, backporting Lean4's definition of Nat.le to community Lean3.

I had made https://github.com/leanprover-community/mathlib/pull/8756, the companion PR to mathlib, which wasn't so bad.

However, while reviewing the PR to community Lean3, we discovered some timeout issues, which we resolved by making nat.le irreducible. I've just realised however, that this breaks https://github.com/leanprover-community/mathlib/pull/8756 again, and will necessitate lots of further changes.

These are all very doable, but I'm worried that people won't like them, so wanted to ask for advice before proceeding. A typical example is (in data.list.basic):

theorem exists_mem_of_length_pos : ∀ {l : list α}, 0 < length l → ∃ a, a ∈ l
| (b::l) _ := ⟨b, mem_cons_self _ _⟩

which now gives an error message non-exhaustive match, the following cases are missing: exists_mem_of_length_pos nil _.

The fix is easy, but sad:

theorem exists_mem_of_length_pos : ∀ {l : list α}, 0 < length l → ∃ a, a ∈ l
| nil h := by cases lt_irrefl _ h
| (b::l) _ := ⟨b, mem_cons_self _ _⟩

Options:
1) I just proceed with these changes for now.
2) Rethink making nat.le irreducible: I'd need help resolving the timeouts in tests in community Lean3.
3) Rethink the Nat.le backport entirely.
3) Someone has a clever idea!

[Scott Morrison]

(These are presumably questions for some combination of @Daniel Selsam and @Gabriel Ebner.)

[Daniel Selsam]

@Scott Morrison Thank you for trying to backport this. In light of all the issues you are hitting, we will revisit whether we can forward-port it instead. The forward-port is very delicate because it touches the kernel and the runtime, but Leo will take a shot at it this week.

[Scott Morrison]

Good luck. :-) For now I'll back out the backport PR to community Lean.

[Leonardo de Moura]

@Scott Morrison I modified the Nat.le in Lean 4. It is now equivalent to the one in Lean 3 and can be aligned by binport.