Lean doesn't unfold HAnd.hAnd

Stream: lean4

[Jun Yoshida]

The rfl in the second line in the following code produces an error:

example : 0x10 * 0x10 = 0x100 := rfl
example : 0x10 &&& 0x10 = 0x10 := rfl -- error

What is the difference between these operators?
I note that the second is a definitional equality as the following compiles:

example : 0x10 &&& 0x10 = 0x10 := by
  conv => lhs; pattern HAnd.hAnd; change Nat.land

[pcpthm]

This is because Nat.bitwise used by the definition of Nat.land is using a well-founded recursion. My understanding is that reduction of a well-founded recursion is possibly non-terminating and thus isn't applied blindly.
I also want to know what is the best way to deal with such functions.

[Jun Yoshida]

That sounds right. I tried providing a hand-made instance and verified the following compiles:

def land' (x y : Nat) : Nat := aux x x y Nat.le.refl
  where
    aux : (n x y : Nat) → n ≥ x → Nat
    | 0, _, _, _ => 0
    | _+1, 0, _, _ => 0
    | _+1, 1, y, _ => y % 2
    | n+1, x+2, y, h =>
      have : x/2 + 1 ≤ n := Nat.le_of_lt_succ $ calc
        x/2 + 1 = (x+2)/2 := Eq.symm $ Nat.add_div_right x (Nat.zero_lt_succ 1)
        _       < (x+2)   := Nat.div_lt_self (Nat.zero_lt_succ _) (Nat.lt_succ_self 1)
        _       ≤ n+1     := h
      aux n (x/2 + 1) (y/2) this <<< 1

instance : AndOp Nat := ⟨land'⟩

example : 0x10 &&& 0x10 = 0x10 := rfl

[Jun Yoshida]

reduction of a well-founded recursion is possibly non-terminating

I was surprised that the following takes 4-5 seconds to compile:

example : 0xFF &&& 0xFF = 0xFF := by conv => lhs; whnf

[Jun Yoshida]

IMHO, Nat.bitwise should be written without well-founded recursion.

[Shreyas Srinivas]

If you are using mathlib4, there is a version called bitwise' whose definition is lean3 style. Perhaps that helps?

[Shreyas Srinivas]

There are corresponding land', lor', etc.

[Jun Yoshida]

I checked the source of Mathlib4/Init/Data/Nat/Bitwise.lean in mathlib4. It looks depending on binaryRec which uses well-founded recursion, right?

[Shreyas Srinivas]

True. Normally when using bitwise, unfold followed by cases works

[Jun Yoshida]

Are there any technique to handle such functions with elaborator/tactic? For example, it is boring and actually hard to prove things like 0xFEEDFFFFFFFF &&& 0xFFFFDEADFFFF &&& 0xFFFFFFFFBEEF = 0xFEEDDEADBEEF by unfolding definitions by hand. With the current implementation of Nat.land, it is, I think, hard also for Lean compiler since it takes a lot of time and memories.

[Mario Carneiro]

This is a job for norm_num

[Mario Carneiro]

it's not a high priority though :(

[James Gallicchio]

Jun Yoshida said:

IMHO, Nat.bitwise should be written without well-founded recursion.

(I think doing it structurally would be waaaay slower, since IIRC the kernel has special handling for div/mod on nats?)

[Jun Yoshida]

Mario Carneiro said:

This is a job for norm_num

Cool! It enables "proof by (tedious) computation" that I sometimes see in papers. Thank you for letting me know. Yet, I have to tell the plugin how to handle with bit operators...

[Jun Yoshida]

James Gallicchio said:

(I think doing it structurally would be waaaay slower, since IIRC the kernel has special handling for div/mod on nats?)

Nat.land, Nat.lor, ... are anyway implemented by C codes, so I think they can be more "proof-oriented" in Lean codes.

[Jun Yoshida]

I found that Lean server (in VS code REPL) crashes with the following:

example : 0xFEEDFFFFFFFF &&& 0xFFFFDEADFFFF &&& 0xFFFFFFFFBEEF = 0xFEEDDEADBEEF := by conv => lhs;

[Mario Carneiro]

Jun Yoshida said:

James Gallicchio said:

(I think doing it structurally would be waaaay slower, since IIRC the kernel has special handling for div/mod on nats?)

Nat.land, Nat.lor, ... are anyway implemented by C codes, so I think they can be more "proof-oriented" in Lean codes.

Not exactly. The C code for Nat.land et al is only used by the compiler, not the kernel, so if you are trying to use it in a proof by rfl or by decide you still have to care about the performance of the lean model of the operation.

[Mario Carneiro]

Only +,-,*,/,%,< on Nat are overridden in the kernel as well as the compiler

[Jun Yoshida]

Ah, that is right. I am sorry for my imprecise statement. I am not sure that well-founded recursion is faster than stractural recursion from kernel point of view. In my experience, wf seems slower.

[Mario Carneiro]

It is more complex. More importantly, it often simply doesn't reduce due to hitting a theorem, which is treated the same as opaque and will block reduction to a constructor. Reducing proofs by well founded recursion requires reducing the proof of well foundedness, so this usually gets stuck

[James Gallicchio]

And with those large nats I would imagine that doing 2^48 reduction steps would not be performant in the kernel, compared to doing 48 steps + reducing the well-foundedness proof

[Mario Carneiro]

You can implement it as doing 48 steps without reducing any well-foundedness proof by doing structural induction on a fuel variable. Even if the initial value of the fuel variable is 2^48 or so it won't step any more than necessary because the kernel works from the outside in using whnf to evaluate stuff so if 48 steps of recursion suffices then it won't work out the rest

[Mario Carneiro]

which looks like what Jun Yoshida 's land' function is doing

[James Gallicchio]

Ahh I see, sorry for misunderstanding

[Jun Yoshida]

Thank you for elaborating my example. Yes, every well-founded recursion w.r.t. Nat.lt can be transformed into a structural recursion in the same idea. But, writing examples, I realized that the resulting functions become complicated and far from the straightforward implementation. I now agree that definitions should be kept concise. Reduction is not always the best way to prove equations.

[Jun Yoshida]

So, what should I do is probably to write the proof of hAnd_eq_land' : ∀ (x y : Nat), x &&& y = land' x y and to do something like rw [hAnd_eq_land']; cong => lhs; whnf.

[Jun Yoshida]

Thank you for comments and advice.

[Mario Carneiro]

I think another way to spell congr => lhs; whnf is rfl