Are there any ergonomic ways to deal with finite types in Coq?

Question

I am trying to work with proofs about fixed-size bitvectors, or a map from a finite type to bool. What I'm finding is that "finite type" is actually somewhat nuanced.

There seem to be two standard ways of dealing with finite types:

1. Explicitly write each inhabitant as a constructor, as seen with Byte type in the standard library
2. Provide a type indexed by size: nat with one constructor that takes n: nat and proof that n < size

Explicitly writing each constructor is fine when there is only a few of them, but becomes intractable for a type with more than a few hundred inhabitants. Defining a total order on such a type require something like O(n^2) lines of code. For example:

(* type with 16 null-ary constructors *)
Inductive regi16 :=
| x0
| x1
| x2
| x3
...
| xd
| xe
| xf
.

Definition regi16lt (x y: regi16) :=
  match x with
  | x0 =>
    match y with
    | x0 => False
    | _ => True
    end
  | x1 =>
    match y with
    | x0 => False
    | x1 => False
    | _ => True
    end
  ...
  | xe =>
    match y with
    | xf => True
    | _ => False
    end
  | xf => False
  end
.

On the other hand, using a type that takes proof as part of its constructor means dragging that proof around everywhere. Example:

Record fintype (n: nat) := mkfin {
  val: nat;
  range: val < n
}

Lemma zlt: forall n, 0 < S n. Proof. lia. Qed.
Lemma slt: forall n m, n < m -> S n < S m. Proof. lia. Qed.

(* to express the last element of a finite type with 4 inhabitants *)
Check mkfin 4 3 (slt 2 3 (slt 1 2 (slt 0 1 (zlt 0)))).

Is there a better way to work with finite types?

Answer 1

I would suggest to look at the MathComp library, e.g., this book, for finite types, in particular the finType library, if you don't already know about it.

Answer 2

You do not need to write O(n^2) lines of code for n values. You can do something like this:

Definition regi16lt (x y: regi16) :=
match x, y with 
| x0, x0 => True 
| x1, x1 => True
| x2, x2 => True 
| x3, x3 => True
| _, _ => False
end.

In addition, you can encode finite type in Coq which is less painful to use is:

Record fintype (A : Type) : Type := mkfin {
  l : list A;
  Hfin : forall x : A, List.In x l
}.

Have a look at the [1] which has some encodings of finite type as well. There is similar definition [2] to the one I suggested but encoded as sigma type.

[1] https://github.com/uds-psl/coq-library-undecidability/tree/coq-8.16/theories/Shared/Libs/PSL/FiniteTypes [2] https://github.com/uds-psl/coq-library-undecidability/blob/coq-8.16/theories/Shared/Libs/DLW/Utils/fin_base.v#L24

Answer 3

In general, I would use finType from the MathComp library as suggested by @Pierre Jouvelot. There is also the Finite predicate from Coq.Logic.FinFun, which I would not recommend in most cases.

In this particular case, you could define your own fixed-size list:

Inductive fs_list (A : Type) : nat -> Type :=
  | fs_nil : fs_list A 0
  | fs_cons (n : nat) (a : A) (l : fs_list A n) : fs_list A (S n).

Optionally, if you want to have nice implicits:

Arguments fs_nil {A}.
Arguments fs_cons {A} {n}.

Doing so, you can define lt as a fixpoint that would work on a fixed-size list of any size; the type corresponding to the one of your example would be fs_list bool 16.

Answer 4

It is common in math to use the skeleton of the category of finite types. So for each natural number there is one and only one associated finite type. This can be useful but can also be very awkward without handwaving.

More structured encodings like the following can work out okay in some situations.

Inductive fin:=
| Sigma {n} (x: Vector.t fin n)
| Pi {n} (x: Vector.t fin n).

Inductive toset: fin -> Set :=
| lm {n} (A: Vector.t fin n): (forall x, toset (A[n])) -> toset A
| ex {n} (A: Vector.t fin n) x: toset (A[@ x]) -> toset (Sigma A).

Just want to say you don't always necessarily need to work directly with the skeleton. Not sure of the best way to slice it though.