How do I write bitwise logic in lean4 with mathlib?

Question

I want to prove that a circuit decomposition into Toffoli gates is correct. In order to do this, I'm trying to explain to Lean what it means to apply a Toffoli gate to bits (flip the target bit if the two control bits are on). But I keep getting stuck on basic details related to decidability, termination, syntax, and naming.

• I tried making a state which was a Set Nat. But then I couldn't seem to evaluate everything because Lean didn't seem to believe that a \in b was decidable. That's reasonable for general sets I suppose, but mine are finite integer sets. I then tried making my own set, which was just a list of unique integers, but couldn't convince Lean that my "flip if integer is list" method would terminate, despite all the recursive cases descending into the list. I don't really want to be using representations where these kinds of issues keep cropping up, since my ability to solve them is very limited.

• My favorite approach in other languages is to use bit packed integers for this. I tried doing this in Lean, but I can't find out where Lean or MathLib define how to say things like "compute the bitwise xor of these two integers" or "left shift this integer".

I asked ChatGPT and it just told me "here's what it would look like if it worked but this won't work: [thing that doesn't work]".

Anyways, strategic advice on the correct way to go would probably be helpful. But mostly I'd just like to get unstuck on the syntax for bitwise arithmetic:

structure Toffoli where
  a : Nat
  b : Nat
  t : Nat

structure SimState where
  bit_packed_state : Nat

def SimState.after
    (s : SimState)
    (op : Toffoli)
    : SimState
    :=
  let m := s.bit_packed_state

  -- syntax error on should-be-bitwiseand '&', should-be-leftshift '<<'
  let a := (m & (1 << op.a)) != 0

  -- syntax error on should-be-bitwiseand '&', should-be-leftshift '<<'
  let b := (m & (1 << op.b)) != 0

  -- syntax error on should-be-bitwisexor '^', should-be-leftshift '<<;
  let m2 := m ^ ((a && b) << op.t)

  SimState.mk m2

Answer 1

To answer the title question, the operations on Nat, UInt8, and similar types are written with three symbols: &&&, |||, ^^^, <<<, and >>>. (I believe these operations, like most low-level Nat arithmetic operations, are implemented efficiently with arbitrary precision arithmetic packages, and should be quite fast.)

---

To answer the heart of your question, it looks like you want a finite set that you can use for computation, and maybe also prove theorems about.

Set is for arbitrary sets, including infinite ones, so it doesn't have computation. FinSet (Mathlib) is for finite sets and has a good library of mathematics, but it is defined as a quotient of lists, so it can't compute either.

The closest things to, say, set in Python that I know of are Lean.RBTree, Std.RBSet, Lean.PersistentHashSet, and Lean.HashSet. (They are the set versions of the respective map-like data structures Lean.RBMap, Std.HashMap, Lean.PersistentHashMap, and Lean.HashMap.) The first two set data structures are (I think) the same. The first three are "persistent" meaning you won't duplicate the whole data structure if you add an element to it. The last is implemented with Array, so you should be careful to use destructive/in-place updates to avoid duplicating it in memory (and destructive updates can even help in improving the performance of persistent data structures).

If you don't care about performance, there is also Lean.AssocList which is a map implemented as a list of key-value pairs. (AssocList Nat Unit acts as a set of Nats.)

If you want to prove things about your sets, I'm not sure how built up the library is for the mathematical properties of these data structures. You will have to do some digging. (For which moogle.ai might help.)

---

Finally, for implementing bit sets from Nat or UIntX, I don't think this has been done completely in Lean, but there are a number of similar things. The closest is Std.BitVec, which is a low-cost abstraction around Nat representing fixed-length bit vectors. Nat.bitwise and Nat.bits (Mathlib) are some other work in this direction. Also, you could implement your own bit sets directly from Nat, UInt8, Std.Bitvec, or ByteArray. As you point out, implementing the basic set operations is pretty simple.