Elimination-by-exhaustion for Fin n (really, UIntN)

Stream: lean4

[neil]

I'm getting back to work on my little de-/serialization framework and I'd like to start proving some roundtrip equality properties, i.e. theorems of the form v = deserialize (serialize v).

One of my representable types is UInt8 (really, a standin for "some fixed-width integer"). I can probably adjust my de-/serialization (henceforth "serdes") functions so that I can prove roundtrip algebraically, but given that these functions have computable implementations, it's a lot easier to just prove it by exhaustion. That also means that the proof is independent of the implementation, which is helpful since I'm changing stuff frequently.

Now, given any particular UInt8 (or Nat, or Fin 256) value, I have a short tactic proof which demonstrates the roundtrip equality. However, I can't figure out how to actually do a proof by exhaustion on UInt8 (or Fin, for that matter). The eliminators for Fin seem to all be inductive, which isn't useful.

If I could get an exhaustion eliminator, I could just do something like cases n using exhaustive_eliminator <;> my_tactic, which feels natural.

I found #lean4 > About `Nat.all`/`Nat.any` which references Nat.all and Nat.all_eq_finRange_all, but I wasn't successfully able to adapt that idea to my problem. I also don't know if building up a big chain of \ands is as useful as building up a chain of &&s (since I need to work in Prop as opposed to Bool).

I also found #lean4 > Pattern matching on Fin isn't exhaustive for large matches @ 💬 , which seems like it could be directly relevant, but I haven't tried to actually understand it yet; it certainly didn't make immediate sense to me.

So, is there some straightforward proof-by-exhaustion eliminator for UInt8/BitVec/Fin?

[neil]

(there are also some weird questions which arise from the specifics of my functions, including that I have to do stuff like simp[Vector.range, Array.range, Array.ofFn, Array.ofFn.go] to get some (what I think are) basic equalities to actually go through, and that if I try to prove roundtrip using a Fin to instantiate/destruct a UInt8
it's a nightmare, but going via Nat seems to play nicer with the simplifier, but I digress)

[Kenny Lau]

fin_cases in Mathlib?

[Robin Arnez]

UInt8 is like, pretty large though

[neil]

UInt8 is 256 values, which is sufficiently close to 1 for me

[Robin Arnez]

and if you say you run some kind of tactic afterwards you're going to have a proof that takes a while to elaborate

[Robin Arnez]

Which kind of tactic do you want to run later?

[neil]

it's actually just a big call to simp[...]

[neil]

since the functions are calculable, there's not really anything interesting to do; you just have to evaluate them completely

[Robin Arnez]

Hmm well that might still take a minute or so

[neil]

that said, I must be unfamiliar with lean, because my tactic is

    simp[parseInt8, serializeInt8]
    simp[Vector.range, Array.range, Array.ofFn, Array.ofFn.go]

and, coming from Rocq, the second simp call feels like it should not be necessary

[neil]

is there a better way to tell lean to just evaluate a term than these simp commands? given that simp is, you know, more than just evaluation

[Robin Arnez]

Can you point me to the source code again?

[neil]

let me excise it and post it here

[Robin Arnez]

and well you usually evaluate using rfl; but I suppose your proof is more than just evaluation

[neil]

-- Implementing example roundtrip ser/des for UInt8 / Vector Bool 8
def parseInt8 (b : Vector Bool 8) : UInt8 :=
  -- [1, 2, 4, ..., 128]
  let coeffs := ((Vector.range 8).map (2 ^ ·))
  -- use b as a bitmask
  let summer := fun (on, coeff) acc => acc + (if on then coeff else 0)
  let value := (b.zip coeffs).foldr summer 0
  .ofNat value


def serializeInt8 (i : UInt8) : Vector Bool 8 :=
  let n := i.toNat
  -- NOTE: we /don't/ want to reverse this because we're going to do a foldr on
  -- digitifier.
  let coeffs := ((Vector.range 8).map (2 ^ ·))
  let digitifier := fun coeff ((n : Nat), (acc : Array Bool)) =>
    if n >= coeff then (n - coeff, #[true] ++ acc)
                  else (n, #[false] ++ acc)
    -- (if n >= coeff then n - coeff else n, #[(n ≥ coeff : Bool)] ++ acc)
  let mask := coeffs.foldr digitifier (n, #[])
  -- proofs
  let digitifierSize : forall coeff n acc,
    (digitifier coeff (n, acc)).snd.size = acc.size + 1 := by
    intros coeff n acc ; unfold digitifier
    -- proceed by cases on n ≥ coeff
    by_cases heq : n ≥ coeff <;> simp[heq, Nat.add_comm]
  let h : mask.snd.size = 8 := by
    have helper : coeffs = #v[1, 2, 4, 8, 16, 32, 64, 128] := by
      -- Why does `simp` not want to just compute this constant??
      simp[coeffs, Vector.range, Array.range, Array.ofFn, Array.ofFn.go]
    unfold mask ; rw[helper]
    simp[digitifierSize]
  Vector.mk mask.snd h

[neil]

note that this is not pretty because I just needed to have /some/ way to de-/serialize these values

[neil]

so.. this is what I came up with

[Robin Arnez]

Yeah right that simp call is literally just rfl

[neil]

if I wanted to prove this algebraically, I think I would make "digitifier" and "summer" real functions and prove that they're inverses, but... I don't want to do that

[neil]

yup, but it seems that the compiler cannot see that definitional equality

[Robin Arnez]

huh?

[Robin Arnez]

rfl works for me at that position

[neil]

oh really? let me try that

[neil]

wow it does!

[neil]

it feels really weird that rfl succeeds where simp makes no progress

[Robin Arnez]

Well, simp only unfolds abbrevs and other things tagged reducible but it's not for evaluation really

[Robin Arnez]

If you want it to unfold something, you need to tell it to

[neil]

yeah, I figured as much but didn't realize rfl would actually be useful here. I have Rocq brain I guess

[Robin Arnez]

Heh, well, I guess I have another question though

[Robin Arnez]

Why Vector Bool?

[Robin Arnez]

That's basically 64 bit per Bool?

[neil]

I'm not really caring about the particulars of the representations at this point

[neil]

I'm also new enough to Lean that I haven't really bothered to learn the stdlib/built in types, cos I have some deadlines related to my PhD work, and I'd rather get more of the domain-relevant stuff done before then, then rewrite this to actually be efficient and choose good data structures. For now, I'm just trying to have a demonstrator with a rich enough type system that I can prove some theories about

[Robin Arnez]

Hmm well still can you point me to a github (if you have one)

[neil]

I have it private for now. Would you like me to add you?

[neil]

this repo being private, that is (it's in the same repo as a bunch of my PhD materials because that's what my advisors requested).

[neil]

Robin Arnez said:

and well you usually evaluate using rfl; but I suppose your proof is more than just evaluation

so, in Rocq there's simp, which just does evaluation, reflexivity, which does deeper evaluation and some rewriting and terminates the proof, and auto, which does proof search. Lean doesn't seem to have an equivalent for Rocq's simp, which is a shame because sometimes it's really helpful to just try to evaluate some terms when working through a proof without asserting that the proof should finish

[Henrik Böving]

Just letting reduction run is usually a bad idea, it can cause performance issues and make it very difficult for you to refactor your code further down the line as your proofs are now bound to the precise reduction behavior of your definitions. For that reason you should prefer to build up a simp or grind set of theorems that you can then let the automation apply.

[neil]

that is true!

[neil]

it would be nice if there /were/ some way to do it though, a la eval!, since these things can be useful when prototyping or developing new features (at least, in the sorts of smaller developments I tend to be working on)

[Robin Arnez]

reduce exists but you should only use it for prototyping (import Mathlib.Tactic.DefEqTransformations)

[neil]

I do also find it interesting that a lot of this sort of functionality is in Mathlib instead of closer to the core of the language or base developer experience

[Robin Arnez]

Well it's not really useful in complete proofs

[Robin Arnez]

and #reduce does something similar

[Robin Arnez]

(but as a command)

[neil]

yeah, it's not useful in complete proofs, but, at least the way I got used to working in Rocq, it's useful in the development of proofs. I'm not yet in the habit of making sure my developments integrate nicely with automation--namely tagging thms appropriately and making sure they have consistent forms--but I assume that once that becomes natural, then my desire for these sorts of features will lessen

[neil]

ok Robin you were right:

def UInt8_roundtrip_ex_fin : .ofFin (4 : Fin 256) = parseInt8 (serializeInt8 (.ofFin (4 : Fin 256))) := by
  rfl

-- this times out lol
theorem UInt8_roundtrip : forall (u : Fin 256),
  (.ofFin u) = parseInt8 (serializeInt8 (.ofFin u)) := by
  intro u
  fin_cases u <;> rfl

[neil]

wait WOW it's got even stranger behavior: this somehow discharges 180 of the 256 goals, and of the remaining 76, you can check that they should be discharged by rfl by checking the individual value using the example definition above.

I'm assuming this is related to it timing out, but producing really weird output as a result

[Robin Arnez]

For these cases, decide +revert usually works better since it doesn't create new goals (instead of fin_cases u <;> rfl)

[Robin Arnez]

(and the proof term is tiny)

[Robin Arnez]

But it will probably still take forever (and throw maximum recursion depth reached)

[neil]

it succeeds if I set maxHeartbeats to 500000 (from 200000)

[Robin Arnez]

I see

[neil]

so... why is this so slow? is it elaborating the 256 goals? Naively, I would expect this sort of thing to be pretty quick: a relatively small enumeration, producing relatively small terms (I guess you have triangle(256) constructors, but that still feels like not a very big number?), with a relatively quick tactic to discharge each goal

[neil]

also, Kenny, thanks for the solution, forgot to mention it earlier :)

[Kenny Lau]

yeah you have 256 goals, what happens if you follow Robin's advice to use decide +revert?

[neil]

Robin Arnez said:

But it will probably still take forever (and throw maximum recursion depth reached)

decide +revert terminates pretty quickly with max recursion depth exceeded, I'm going to see if I can binary search to find the threshold where it passes (though I suppose the time is more interesting than the depth limit...)

[neil]

also, asides: import Mathlib.Tactics was adding 4s to my build time on its own somehow, plus one of my functions (def segment) collides with something in mathlib... are there comprehensive docs on the import system? I haven't really been able to find any in all my time using Lean.

[neil]

neil said:

it succeeds if I set maxHeartbeats to 500000 (from 200000)

fin_cases u <;> rfl seems to take around 45s to build

[neil]

set_option maxHeartbeats 500000 in
set_option maxRecDepth 10000 in
theorem UInt8_roundtrip : forall (u : Fin 256),
  (.ofFin u) = parseInt8 (serializeInt8 (.ofFin u)) := by
  intro u
  -- fin_cases u <;> rfl
  decide +revert

$ time lake build
...
Build completed successfully.
lake build  29.43s user 6.26s system 103% cpu 34.593 total

[neil]

so decide +revert seems to take about 2/3rds as long as fin_cases, though this is not a rigorous benchmarking because I... should actually go to sleep pretty soon

[neil]

(note also that decide +revert means that I can drop the dependency on Mathlib.Tactic, which brings the time down to 21s, but that's no longer a ceteris-paribus comparison)

[Robin Arnez]

I'd recommend you to just use a simpler definition:

def BitVec.ofFnLE (f : Fin n → Bool) : BitVec n :=
  go 0#0 (Nat.zero_le _)
where
  go {k : Nat} (b : BitVec k) (h : k ≤ n) : BitVec n :=
    if h' : k = n then
      b.cast h'
    else
      have : k < n := Nat.lt_of_le_of_ne h h'
      go (b.cons (f ⟨k, this⟩)) this

@[simp]
theorem BitVec.getElem_ofFnLE {f : Fin n → Bool} {i : Nat} (h : i < n) :
    (BitVec.ofFnLE f)[i] = f ⟨i, h⟩ := by
  let rec go {k : Nat} (b : BitVec k) (h : k ≤ n) {i : Nat} (hi : i < n) :
      (ofFnLE.go f b h)[i] = if _ : i < k then b[i] else f ⟨i, hi⟩ := by
    fun_induction ofFnLE.go <;> grind
  simp [ofFnLE, go]

def parseInt8 (i : Vector Bool 8) : UInt8 :=
  UInt8.ofBitVec (BitVec.ofFnLE fun x => i[x.val])

def serializeInt8 (i : UInt8) : Vector Bool 8 :=
  Vector.ofFn fun x => i.toBitVec[x.val]

def parseInt16 (i : Vector Bool 16) : UInt16 :=
  UInt16.ofBitVec (BitVec.ofFnLE fun x => i[x.val])

def serializeInt16 (i : UInt16) : Vector Bool 16 :=
  Vector.ofFn fun x => i.toBitVec[x.val]

-- ...

theorem parseInt8_serializeInt8 (i : UInt8) : parseInt8 (serializeInt8 i) = i := by
  rw [← UInt8.toBitVec_inj]
  ext k h
  simp [parseInt8, serializeInt8]

theorem serializeInt8_parseInt8 (i : Vector Bool 8) : serializeInt8 (parseInt8 i) = i := by
  ext k h
  simp [parseInt8, serializeInt8]

theorem parseInt16_serializeInt16 (i : UInt16) : parseInt16 (serializeInt16 i) = i := by
  rw [← UInt16.toBitVec_inj]
  ext k h
  simp [parseInt16, serializeInt16]

theorem serializeInt16_parseInt16 (i : Vector Bool 16) : serializeInt16 (parseInt16 i) = i := by
  ext k h
  simp [parseInt16, serializeInt16]

-- ...

[neil]

you're suggesting that the perf bottleneck is in the rfl steps, then?

[neil]

oh wait

[neil]

I mean, yeah, but for the moment I was mostly just interested in how to even approach a proof-by-exhaustion for these sorts of inductive, rather than enumerated, types in Lean

[Kenny Lau]

the enumeration is the Fintype

[Kenny Lau]

the lean philosophy is that you shouldn't rely too much on the unique "underlying" definition

[Kenny Lau]

fin_cases relies on Fintype

[Kenny Lau]

decide +revert is also Fintype

[Robin Arnez]

Well, there is also a special instance decide uses to make forall _ : Fin n not rely on Fintype

[neil]

Kenny Lau said:

the lean philosophy is that you shouldn't rely too much on the unique "underlying" definition

I mean, you're relying on the unique properties of the underlying definitions somehow: either that the de-/serialization functions are easy to prove things about algebraically, or that the types they range over are "easy" to work over exhaustively, where "easy" in the former refers to "difficulty to produce a proof" and in the latter means "performance"

[neil]

also, just for fun, I "manually" elaborated this exercise into 256 separate statements, and that seems to be a hair quicker, but not anything really significant (35s using rfl, 40s using decide +revert, though presumably the +revert is now superfluous)

[neil]

neil said:

I mean, yeah, but for the moment I was mostly just interested in how to even approach a proof-by-exhaustion for these sorts of inductive, rather than enumerated, types in Lean

and what this has taught me is that it seems like I should anticipate that I will be proving things algebraically, so the particulars of the function definitions matter.

[neil]

thanks for all the info, you guys :)

[Robin Arnez]

The Lean philosophy is basically what you see with my ofFnLE example:

def BitVec.ofFnLE (f : Fin n → Bool) : BitVec n :=
  go 0#0 (Nat.zero_le _)
where
  go {k : Nat} (b : BitVec k) (h : k ≤ n) : BitVec n :=
    if h' : k = n then
      b.cast h'
    else
      have : k < n := Nat.lt_of_le_of_ne h h'
      go (b.cons (f ⟨k, this⟩)) this

@[simp]
theorem BitVec.getElem_ofFnLE {f : Fin n → Bool} {i : Nat} (h : i < n) :
    (BitVec.ofFnLE f)[i] = f ⟨i, h⟩ := by
  let rec go {k : Nat} (b : BitVec k) (h : k ≤ n) {i : Nat} (hi : i < n) :
      (ofFnLE.go f b h)[i] = if _ : i < k then b[i] else f ⟨i, hi⟩ := by
    fun_induction ofFnLE.go <;> grind
  simp [ofFnLE, go]

Basically: First write a definition and then write enough characterizing lemmas that you don't need to rely on the definition afterwards.

[Robin Arnez]

If you only want one lemma (deserialize_serialize for every encoding/decoding function) this might not be as important though

[Wuyang]

Sounds like fin_cases could help here, maybe try it on Fin 256 and check roundtrip equality. Could also explore faster term evaluation than simp.

You might find more approaches like this on LeanFinder (www.leanfinder.org).

[Wuyang]

(deleted)

[leanfinder]

Failure! Bot is unavailable

[Wuyang]

@leanfinder Lean proof by exhaustion for UInt8 or Fin types to verify serialize-deserialize roundtrip equality

[leanfinder]

Here’s what I found:

• theorem UInt8.val_injective : Function.Injective val run_cmd "The function val : UInt8 → ℕ that extracts the underlying natural number from an unsigned 8-bit integer is injective. That is, for any two unsigned 8-bit integers x and y, if val x = val y, then x = y." (score: 0.697)

• theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl "For unsigned 8-bit integers $x$ and $y$, if their natural number representations are equal, i.e., $x.\text{toNat} = y.\text{toNat}$, then $x$ and $y$ are equal as unsigned 8-bit integers." (score: 0.680)

• theorem getElem_ofFn (f : Fin n → UInt8) (i) (h : i < (ofFn f).size) : (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ := get_ofFn f ⟨i, h⟩ "For a function $f \colon \mathrm{Fin}\,n \to \mathrm{UInt8}$ and an index $i$ such that $i < (\mathrm{ofFn}\,f).\mathrm{size}$, the $i$-th element of the ByteArray constructed from $f$ via $\mathrm{ofFn}$ is equal to $f(i)$.

In symbols:
$(\mathrm{ofFn}\,f)[i] = f(\langle i, \mathrm{size\_ofFn}\,f \mathbin{\bullet} h \rangle).$" (score: 0.676)

• theorem UInt8.natCast_def (n : ℕ) : (n : UInt8) = ⟨n⟩ run_cmd "For any natural number $n$, the canonical cast of $n$ to an 8-bit unsigned integer is equal to the truncation of $n$ modulo 256, i.e., $(n : \text{UInt8}) = \langle n \rangle$." (score: 0.674)
• theorem get_ofFn (f : Fin n → UInt8) (i : Fin (ofFn f).size) : (ofFn f).get i = f (i.cast (size_ofFn f)) := by simp [get, Fin.cast] "For a function $f \colon \mathrm{Fin}\,n \to \mathrm{UInt8}$ and an index $i \in \mathrm{Fin}\,(\mathrm{ofFn}\,f).\mathrm{size}$, the $i$-th element of the ByteArray constructed from $f$ via $\mathrm{ofFn}$ is equal to $f(i)$, considering the appropriate casting of $i$.

In symbols:
$(\mathrm{ofFn}\,f).\mathrm{get}\,i = f(i.\mathrm{cast}\,(\mathrm{size\_ofFn}\,f)).$" (score: 0.673)

• theorem UInt8.ext_iff {x y : UInt8} : x = y ↔ x.toNat = y.toNat := ⟨congrArg _, UInt8.ext⟩ "For unsigned 8-bit integers $x$ and $y$, $x = y$ if and only if their natural number representations are equal, i.e., $x.\text{toNat} = y.\text{toNat}$. This establishes that equality of UInt8 values can be determined by comparing their corresponding natural numbers." (score: 0.672)
• theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl "For any unsigned 8-bit integer $x$, the value obtained by converting $x$ to a natural number using x.toNat is equal to the value obtained by accessing its internal representation as a natural number, i.e., $x.\text{val.val} = x.\text{toNat}$." (score: 0.672)

• theorem data_ofFn (f : Fin n → UInt8) : (ofFn f).data = .ofFn f := by induction n with | zero => rfl | succ n ih => simp [ofFn_succ, Array.ofFn_succ, ih, Fin.last] "For a function $f : \text{Fin}(n) \to \text{UInt8}$, the data of the byte array constructed using $\text{ofFn}(f)$ is the same as constructing the data directly from $f$. In symbols: $\text{(ofFn}(f)\text{).data} = \text{ofFn}(f)$. This is proved by induction on $n$." (score: 0.670)

• theorem UInt8.val_ofNat (n) : (no_index (OfNat.ofNat n) : UInt8).val = OfNat.ofNat n := rfl "For any natural number $n$, the value of $n$ when interpreted as an 8-bit unsigned integer (UInt8) is equal to $n$ itself, i.e., $\text{UInt8}(n).\text{val} = n$. This holds because the conversion does not alter the value within the range of UInt8." (score: 0.668)

• definition UInt8.toChar (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.toBitVec.isLt (by decide))⟩ "The function converts an unsigned 8-bit integer n to a Unicode character, provided that n represents a valid UTF-8 code point (which is always true for values between 0 and 255 inclusive)." (score: 0.667)

[Aaron Liu]

try decide +revert +kernel

[Aaron Liu]

the +kernel makes it faster to succeed but slower to fail

[Aaron Liu]

I think you also won't have to bump the rec depth

[François G. Dorais]

I've noticed that a few fold-like functions are no longer tail recursive with the new compiler. Did you check with v4.21.0?

[neil]

François G. Dorais said:

I've noticed that a few fold-like functions are no longer tail recursive with the new compiler. Did you check with v4.21.0?

I bumped to 4.22.0-rc4 because I added mathlib as a dependency (and presumably that's what the latest mathlib requires). I may try reverting the lean version since I can just use decide +revert, which doesn't require anything from mathlib.

[neil]

Aaron Liu said:

the +kernel makes it faster to succeed but slower to fail

oh yeah, WAY faster (about 10s) and doesn't require bumping either heartbeats or recursion depth

[neil]

I suppose I should just be using Shift-K (open documentation) on everything suggested. kernel seems like what I wanted: I know that this will succeed, and I don't need any elaboration

[neil]

using +native gets it down to 5s, which is much closer to my expectations, and fine for now. Thanks again, Aaron!

[neil]

so I've settled on

theorem UInt8_roundtrip : forall (u : UInt8),
  u = parseInt8 (serializeInt8 u) := by
  intro u
  -- unwrap the UInt8 into its BitVec8 and then into its Fin 256, which has a
  -- Decidable instance.
  match u with | ⟨⟨fin⟩⟩ => decide +revert +native

which is the overall result that I needed. And it runs in 5s, so I have no problem leaving it in there like this, and I can just swap +native for +kernel if I want to trust less code.

Thanks everyone!

[Kenny Lau]

neil said:

using +native gets it down to 5s, which is much closer to my expectations, and fine for now. Thanks again, Aaron!

it is not recommended to use +native

[Robin Arnez]

+native adds a dependency on the (somewhat unsound) axiom Lean.trustCompiler (i.e. no, you can't trust the compiler all the time lol)

[neil]

yeah, I'm just using +native to keep my builds a bit snappier, since lean doesn't have partial compilation, right?
I might also make some sort of wrapper tactic that switches between native/kernel depending on the build environment: kernel for CI, native for local.

also, as a side note, and not something I bothered to actually test: it seemed that I got a considerable speedup when I pulled this theorem into a smaller file, from the relatively large file it was originally in (something like 3-500 lines, I would guess). So is there some sort of relationship between the size of individual files or modules and compile times, even if the code itself is otherwise identical?