About `Nat.all`/`Nat.any`

Stream: lean4

[François G. Dorais]

The following came about in a budding side project for UnicodeBasic that aims to prove/verify relationships between Unicode properties. Since the Unicode standard is basically just a bunch of tables, these properties can only be checked by exhaustion. There are over 1.1 million code points to check so this is not a trivial task!

My plan is that for user-facing code I will replace these exhaustive tests by a custom axiom Unicode.checked that works like sorry. I still need to run the actual checks on a regular basis to justify the claims made by this axiom. This is where Nat.all/Nat.any come into play and I ran into some issues and questions along the way...

1. Reduction

The kernel currently reduces Nat.all/Nat.any. This is fine for Nat.all 17 _, say, but it inevitably leads to deep recursion for Nat.all 1114112 _. In proofs, this makes it impossible to use some tactics that attempt to reduce such hypotheses.

My current workaround is to use Nat.all_eq_finRange_all/Nat.any_eq_finRange_any as early as possible but that doesn't resolve all the deep recursion issues. Locally marking Nat.all/Nat.any as irreducible helps a bit but doesn't fully solve the problem.

Should Nat.all/Nat.any be marked irreducible? Perhaps with a simproc to only reduce reasonably small cases? Or is there a better workaround?

2. Definition

The current definition for Nat.all is this:

@[specialize] def all : (n : Nat) → (f : (i : Nat) → i < n → Bool) → Bool
  | 0,      f => true
  | succ n, f => all n (fun i h => f i (by omega)) && f n (by omega)

This is not tail recursive but in the same file there is a tail recursive Nat.allTR which is csimp for Nat.all.

However, this tiny variant is already tail recursive:

@[specialize] def allRev : (n : Nat) → (f : (i : Nat) → i < n → Bool) → Bool
  | 0,      f => true
  | succ n, f => f n (by omega) && allRev n (fun i h => f i (by omega))

The explanation is that while && is propositionally commutative, it is not definitionally commutative. The two definitions are provably equal but not definitionally equal.

Should Nat.all be replaced by Nat.allRev to avoid the csimp?

(The same holds for Nat.any with && replaced by || and so on...)

3. Compilation

While Nat.all and Nat.allRev from above are provably equal, they compile differently.

For example: Nat.all 4 p compiles essentially the same way as:

(((true && p 0) && p 1) && p 2) && p 3

But Nat.allRev p compiles essentially the same way as:

p 3 && (p 2 && (p 1 && (p 0 && true)))

These are different. If p 0 = true, p 1 = false, p 2 = false, p 3 = true then:

• Nat.all 4 p evaluates p 0 and p 1 but doesn't evaluate p 2 and p 3.
• Nat.allRev 4 p evaluates p 3 and p 2 but doesn't evaluate p 0 and p 1.

This is not a serious concern unless p is not really pure. For example, if p is partial and p 3 is undefined but p 0, p 1, p 2 are all defined as above, then Nat.all 4 p is defined but Nat.allRev 4 p is undefined. (Same for Nat.any with && replaced by || and so on...)

Does any code out there rely on the order of evaluation for Nat.all/Nat.any? A quick check suggests that all code in core doesn't depend on evaluation order for Nat.all/Nat.any.

[Kim Morrison]

I would be happy to have Nat.allRev and anyRev in addition, but I think the runtime behaviours shouldn't be changed.

[Robin Arnez]

What about using Nat.allRev / Nat.anyRev for kernel behavior and then csimping to something with the current runtime behavior?

[Kim Morrison]

That seems very confusing. Just let people specify what behaviour they want by calling the relevant function.

[Robin Arnez]

Hmm yeah it seems like the kernel can't really handle either of Nat.all / Nat.allRev well for large numbers and the performance is also not significantly different so I guess there is no point in changing anything.

[François G. Dorais]

Those are fair assessments: the *Rev versions are just barely more efficient than the *TR versions. It's not really worth adding them without a specific need.

That resolves 2 and 3, but not 1. Is there a smart way to prevent deep recursion with Nat.all/Nat.any?

[Robin Arnez]

How quickly do you get into such a situation? Can you provide an #mwe?

[François G. Dorais]

Not quite a #mwe but this is a real life example (with no imports required) extracted from batteries#1344:

/-- Returns `true` if `p` returns true for every `Char`. -/
protected def Char.all (p : Char → Bool) : Bool :=
  Nat.all 1114112 fun c h =>
    if h₁ : c < 55296 then
      p <| Char.ofNatAux c <| .inl h₁
    else if h₂ : 57343 < c then
      p <| Char.ofNatAux c <| .inr ⟨h₂, h⟩
    else
      true

theorem Char.exists_eq_false_of_all_eq_false (h : Char.all p = false) :
    ∃ c, p c = false := by
  simp only [Char.all, Nat.all_eq_finRange_all, List.all_eq_false] at h
  match h with
  | ⟨⟨n, hn⟩, ⟨_, h⟩⟩ =>
    simp only [Bool.eq_false_iff]
    split at h
    · refine ⟨ofNatAux n (.inl ?_), h⟩; assumption
    · split at h
      · refine ⟨ofNatAux n (.inr ⟨?_, hn⟩), h⟩; assumption
      · simp at h

This better illustrates my workarounds than the actual problem.

A quick example is on the last line, h: ¬true = true so contradiction was my go-to but it hangs (this is probably an issue with contradiction itself since simp_all does a lot better).

Before finding this working proof, I ran into other deep recursion issues until I realized that Nat.all_eq_finRange_all really helps. I'd have to go back in time to figure out what issues I ran into before then.