Writing a Fintype instance

Stream: new members

[Sam Collins]

Hello, I'm new to Lean and new to Zulip so apologies if I'm doing something wrong.

I have a type:

def BVec (n : Nat) : Fin n -> Bool

I wish to be able to use fin_cases on a specific BVec n when n is known. For example, fin_cases a where a : BVec 1 should give me two cases ![false] and ![true] to work with. I believe to be able to do this, I must write an instance of Fintype for BVec n (not sure on the terminology here):

instance Fintype (BVec n) where
    elems := sorry
    complete := sorry

However I am having great trouble filling in elems (let alone complete). I'm aware that fin_cases works on Fin n -> Bool but it gives me very generic cases using multisets or something, which isn't very useful for me. In my case I can represent each case with e.g. ![false, true].

I would appreciate any help on this, thanks.

[Quang Dao]

You can express BVec in terms of existing mathlib definitions, namely docs#finFunctionFinEquiv and docs#finTwoEquiv. That should give you Fintype for free

[Sam Collins]

@Quang Dao Interesting, thanks. I'll look into that and possibly use those definitions for BVec. Would you recommend something similar for BFun n? It's currently defined as:

def BFun (n : Nat) := BVec n -> Bool

Out of interest, if I were to stick with my definition of BVec n, how would one go about writing an instance of Fintype for it? Or is this a case where that's very difficult or impossible, and there's really no reason to define Boolean vectors like that?

For a wider scope on what I'm trying to accomplish, I'm trying to prove Post's Theorem of Functional Completeness in the field of Boolean functions using Lean4.

[Sam Collins]

To be honest I don't yet entirely know what it means to "express BVec in terms of existing mathlib definitions" :sweat_smile:

[Etienne Marion]

This works:

import Mathlib

def BVec (n : Nat) := Fin n → Bool

instance (n : Nat) : Fintype (BVec n) := by
  unfold BVec
  infer_instance

Lean knows that Fin n and Bool are fintypes and that the arrow between two fintypes gives a fintype, so once you unfold the definition you can just type infer_instance which will automatically close the goal by typeclass inference.

Here is a shorter version which does the same:

import Mathlib

def BVec (n : Nat) := Fin n → Bool

instance (n : Nat) : Fintype (BVec n) := inferInstanceAs (Fintype (Fin n → Bool))

[Sam Collins]

@Etienne Marion Thanks. When I call fin_cases on a BVec 1 it produces something that uses Multiset.Pi.cons 0 0 true and Multiset.Pi.empty fun a ↦ Bool. simp doesn't do anything with these, whereas before I split into cases of ![true] and ![false] (with a sorry to show this is possible) and after rwing these into the goal,simp proved it.

[Sam Collins]

Here is the full code I had, which worked (but contains sorry and isn't as neat as fin_cases a <;> simp):

def narrow (a : BVec (n + 1)) : BVec n :=
    fun ⟨i, h⟩ => a ⟨i, Nat.lt_succ_of_lt h⟩

def xor_all (n : Nat) (a : BVec n) (b : BVec n) : Bool :=
    match n with
    | 0 => false
    | k + 1 => xor_all k (narrow a) (narrow b) ^^ (a k && b k)

def linear_fun (c : BVec (n + 1)) : BFun n :=
    fun a => c n ^^ xor_all n a (narrow c)

def linear (f : BFunAll) := ∃ c : BVec (f.fst + 1), linear_fun c = f.snd

def L : Set BFunAll := {f | linear f}

theorem bvec_1_is_true_or_false (a : BVec 1) : a = ![true] ∨ a = ![false] := sorry

/-- example proof that all 1-ary Boolean functions are linear -/
example (f : BFun 1) : ⟨1, f⟩ ∈ L := by
    show linear ⟨1, f⟩
    unfold linear
    use ![f ![false] ^^ f ![true], f ![false]]
    unfold linear_fun
    repeat unfold xor_all
    repeat unfold narrow
    funext a
    cases bvec_1_is_true_or_false a with
    | inl h₀ =>
        rw [h₀]
        simp
    | inr h₁ =>
        rw [h₁]
        simp

[Etienne Marion]

There is some code missing it does not work in the online editor

[Sam Collins]

Prepend the following:

-- import Mathlib is probably also fine
import Mathlib.Tactic
-- probably not necessary
variable {n : ℕ}

def BVec (n : ℕ) := Fin n -> Bool

def BFun (n : ℕ) := BVec n -> Bool

def BFunAll := Σ n : ℕ, BFun n

My apologies

[Sam Collins]

(I think import Mathlib is also fine but my peer added import Mathlib.Tactic instead for some reason)

[Etienne Marion]

I am not familiar with fin_cases but I guess that the issue here is that the way the fintype instance is provided for an arrow type uses multisets, but it does not give the cases you like. This makes me think that if you want to prove this using fin_cases you'll have to fill in the instance explicitely, but that would mean proving what you want to avoid so it's not a real solution.

[Etienne Marion]

So I'm not sure how to proceed here.

[Sam Collins]

@Etienne Marion Using fin_cases isn't a necessity, it's just that writing an instance of Fintype for BVec n that behaves nicely would allow me to avoid writing individual theorems for splitting a BVec n into cases. I don't even know how to prove such theorems (hence the sorry) and I shouldn't need them at all because clearly BVec n is a finite type. Do you have any idea how to complete the proof where it says sorry? Or do you have any idea how to use the equivalences suggested by @Quang Dao above to write an instance of Fintype that behaves nicely? I've tried the following:

instance (n : Nat) : Fintype (BVec n) := by
    unfold BVec
    have h : Fintype (Fin (2 ^ n)) := sorry
    rw [finFunctionFinEquiv.invFun] at h
    rw [finTwoEquiv] at h
    exact h

but it doesn't work.

Thanks for the help!

[Etienne Marion]

This works:

theorem bvec_1_is_true_or_false (a : BVec 1) : a = ![true] ∨ a = ![false] := by
  unfold BVec
  obtain h | h := Bool.eq_false_or_eq_true (a 0)
  · left
    ext x
    rw [Subsingleton.elim x 0, h]
    rfl
  · right
    ext x
    rw [Subsingleton.elim x 0, h]
    rfl

Though it's probably not the best solution.

[Sam Collins]

Thanks. It's taking me a while to wrap my head around why that works, but I'm sure I'll get there :sweat_smile:

[Etienne Marion]

An element of BVec 1 is just a function form Fin 1 to Bool. So I'm saying: either a 0 = true or a 0 = false. Then the ext tactic says that to prove two functions are equal it suffices to prove that they coincide everywhere, so we taxe x : Fin 1 and want to prove a x = true or a x = false depending on the case. But as all elements in Fin 1 are equal (it is a docs#Subsingleton), we have x = 0.

[Sam Collins]

Managed to write an equivalence relation between BVec n and Fin (2 ^ n) (turned out to be very easy):

def bvec_n_equiv_fin_2_n : BVec n ≃ Fin (2 ^ n) where
  toFun i :=
    let f : Fin n -> Fin 2 :=
      fun x => finTwoEquiv.invFun (i x)
    finFunctionFinEquiv.toFun f
  invFun b :=
    let f : Fin n -> Fin 2 :=
      finFunctionFinEquiv.invFun b
    fun x => finTwoEquiv.toFun (f x)
  left_inv i := by simp
  right_inv b := by simp

Not sure whether I can use this to write an instance of Fintype (BVec n) that behaves nicely?

[Sam Collins]

Think I got it working:

@[simp]
def bvec_n_equiv_fin_2_n : BVec n ≃ Fin (2 ^ n) where
  toFun a :=
    let f := fun i => finTwoEquiv.invFun (a i)
    finFunctionFinEquiv.toFun f
  invFun b :=
    let f := finFunctionFinEquiv.invFun b
    fun i => finTwoEquiv.toFun (f i)
  left_inv a := by simp
  right_inv b := by simp

attribute [simp] finTwoEquiv finFunctionFinEquiv

instance : Fintype (BVec n) :=
  Fintype.ofEquiv (Fin (2 ^ n)) bvec_n_equiv_fin_2_n.symm

def narrow (a : BVec (n + 1)) : BVec n :=
  fun ⟨i, h⟩ => a ⟨i, Nat.lt_succ_of_lt h⟩

def xor_all (n : Nat) (a : BVec n) (b : BVec n) : Bool :=
  match n with
  | 0 => false
  | k + 1 => xor_all k (narrow a) (narrow b) ^^ (a k && b k)

def linear_fun (c : BVec (n + 1)) : BFun n :=
  fun a => c n ^^ xor_all n a (narrow c)

def linear (f : BFunAll) := ∃ c : BVec (f.fst + 1), linear_fun c = f.snd

def L : Set BFunAll := {f | linear f}

@[simp]
theorem vec_1_is_fun_1 (x : Bool) : ![x] = fun _ => x := by funext i; fin_cases i; simp

/-- example proof that all 1-ary Boolean functions are linear -/
example (f : BFun 1) : ⟨1, f⟩ ∈ L := by
  show linear ⟨1, f⟩
  unfold linear
  use ![f ![false] ^^ f ![true], f ![false]]
  unfold linear_fun
  repeat unfold xor_all
  repeat unfold narrow
  funext a
  fin_cases a <;> simp

[Matt Diamond]

FYI we have docs#BitVec if you want to take advantage of existing library code (like docs#BitVec.xor, docs#BitVec.truncate, etc.)

totally understand if you want to roll your own for learning purposes, though

[Matt Diamond]

weirdly there's no Fintype instance for BitVec even though it's just a wrapper around Fin (2 ^ n)...

I'm curious if there's an easier way, but you can just do this:

import Mathlib

def finTwoPowEquivBitVec : Fin (2 ^ n) ≃ BitVec n :=
⟨BitVec.ofFin, BitVec.toFin, fun _ => rfl, fun _ => rfl⟩

instance : Fintype (BitVec n) := Fintype.ofEquiv _ finTwoPowEquivBitVec

[Sam Collins]

@Matt Diamond We (myself and my peers) were aware of BitVec, but thought that because indexing it to retrieve an individual Bool requires bit fiddling (?), it might be harder to use it in proofs that need to reason about individual bits that are defined in terms of something else. Not sure whether this makes sense, we're all new to Lean and are basically guessing at this point, but I'm fairly convinced that we should try using BitVecs and see whether we encounter any issues, rather than writing them off from the start, since multiple different sources have suggested using them, including yourself (although I'm not sure whether any of these sources have used them to prove results in Boolean functions).

[Matt Diamond]

@Sam Collins Yes, it's certainly not as direct as just having a function from Fin n to Bool, but there's an API in place which handles bit extraction for you (i.e. docs#BitVec.getLsb' and docs#BitVec.getMsb', along with a docs#GetElem instance which allows you to simply write b[i]), so the implementation details should hopefully not be too much of an inconvenience.