The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Hi all, I did some experimentation with finite types.

I had some stuff in mind:
- have easy union of finite sets (I have a '0(1)' one)
- avoid arithmetic stuff, so no need of "<,≤,+,length,S,…"
- have a rather efficient implementation
- have a nice extraction

So the basic approach to have a finite type is the following way:

Inductive index : nat → Set :=
| First : ∀ card, index (S card)
| Next : ∀ card, index card → index (S card)
.

This type is good for teaching, but is rather inefficient for a lot of
things.

So a better thing is to represent them as:

Definition index (n : N) := {m:N|m<n}.

(where N is a binary representation of natural numbers)

It is a lot more efficient for a lot of things, but will need a lot of
arithmetic in its use.

Some time ago I tried to define a type similar to 'nat', it was the
type 'finite' defined by:
finite = Sin : finite (*for single*)
       | Mul : finite → finite → finite.
(I first thought of this type to encode other types, as the sum of two
types was an easy thing with it)

Sin                                           ~ 1
Mul Sin Sin                                   ~ 2
Mul Sin (Mul Sin Sin) ≡ Mul (Mul Sin Sin) Sin ~ 3
and so on…

Then I defined my 'index' type as

Inductive index : finite → Set :=
| Is : index Sin (* only inhabitant of a singleton *)
| Il : ∀ l r, index l → index (Mul l r)
       (* an inhabitant of the left component *)
| Il : ∀ l r, index l → index (Mul l r)
       (* an inhabitant of the right component *)
.

I was rather satisfied with it, because union of two finite sets was a
piece of cake, and given a inhabitant of (Mul f g), it was easy to tell
if it came from f or g.

My two first points were satisfied with it. The two last point were not
that bad. It is not as efficient as it could be, since balance is not
guaranteed, and its extracted version is:

type index =
  Is | Il of finite * finite * index | Ir of finite * finite * index

It has also some badpoint, in the fact that it uses some dependant
type, which often are heavy to use (for instance to define decidable
equality). Lately I significantly improved this version, so that the
index type extracted is:

type index =
  Is | Il of index | Ir of index

I am rather satisfied with this version, and wanted to share some of
the tricks I used with the mailing list (I didn't browse the web, so
this implementation may be well known, and I have reinvented the wheel).

I also used some trick to avoid relying on proof irrelevance during
the definition of the decidable equality. To remove the 'finite' of the
indice and have it as parameter (in fact not truly a parameter, but I
do not remember its technical name), I had to add some Prop content in
the inductive part, I converted this proof directly on the singleton
Prop (ie. True) or empty Prop (ie. False) according to the environment.

I think that somehow there lacks a finite type library in the Coq
standard library. I do not pretend I followed the right path, so if you
have some interesting idea on this developement, I would be happy to
read them.

==========================================================================
(** * The Finite module is used for identifiers. It is in a separate
file as it extracts using Obj.magic, and I prefer not to have it pollute
      other files. *)
Require Import Utf8.

Unset Elimination Schemes.
Set Implicit Arguments.

(** Miscallenous stuff *)

Notation "⋖ H ⇒ e ⋗" := (match H with eq_refl => e end).
Notation "⋖ H | P ⇒ e ⋗" := (match H in _=y return P y with eq_refl =>
e end). Notation "⋖ H ⋗" := (match H with end).

Inductive optEq (A : Type) (a b : A) : Type :=
  | IsEq : a = b → optEq a b
  | NotEq : optEq a b
  .

Definition optProp T (t u : T) (x : optEq t u) : Prop :=
  match x with NotEq => False | _ => True end.

Definition eq_dec2 (A : Type) (f : ∀ (a b : A), optEq a b)
                    (H : ∀ a, optProp (f a a))
                    : ∀ (a b : A), {a=b}+{a≠b} :=
  λ a b, match f a b as s return f a b = s → {a = b} + {a ≠ b} with
  | IsEq e => λ _, left e
  | _ => λ L, right (λ (K : a=b), ⋖⋖K⇒L⋗:f b b = NotEq b b|λ x, optProp
x⇒H b⋗) end eq_refl.

(** True stuff *)

Inductive finite :=
| Sin : finite
| Mul : finite → finite → finite
.

Definition isSin : finite → Prop :=
  λ f, match f with Sin => True | _ => False end.
Definition isMul : finite → Prop :=
  λ f, match f with Sin => False | _ => True end.

Definition fl : ∀ f, isMul f → finite :=
  λ f, match f with Mul l _ => λ _, l | Sin => λ H, ⋖H⋗ end.
Definition fr : ∀ f, isMul f → finite :=
  λ f, match f with Mul _ r => λ _, r | Sin => λ H, ⋖H⋗ end.

Inductive index (f : finite) : Type :=
| Is : isSin f → index f
| Il : ∀ H, index (fl f H) → index f
| Ir : ∀ H, index (fr f H) → index f
.

Definition sIsSin : ∀ f (a b : isSin f), a = b :=
  λ f, match f with
       | Sin => λ a b, match a, b with I, I => eq_refl I end
       | Mul _ _ => λ H, ⋖H⋗
       end.
Definition sIsMul : ∀ f (a b : isMul f), a = b :=
  λ f, match f with
       | Sin => λ H, ⋖H⋗
       | Mul _ _ => λ a b, match a, b with I, I => eq_refl I end
       end.

Definition is := Is Sin I.
Definition il l r := Il (Mul l r) I.
Definition ir l r := Ir (Mul l r) I.

(** ** decidability of equality on [index f] *)
Fixpoint index_dec_aux f (a b : index f) {struct a} : optEq a b.
refine (
  match a as i return optEq i _ with
  | Is Ha => IsEq _ (* a *)
  | Il Ha a' =>
    match b as i return optEq _ i with
    | Il Hb b' => match index_dec_aux _ a' ⋖sIsMul f Hb Ha ⇒ b'⋗ with
                  | IsEq eq => IsEq _ (* b *)
                  | _ => NotEq _ _
                  end
    | _ => NotEq _ _
    end
  | Ir Ha a' =>
    match b as i return optEq _ i with
    | Ir Hb b' => match index_dec_aux _ a' ⋖sIsMul f Hb Ha ⇒ b'⋗ with
                  | IsEq eq => IsEq _ (* c *)
                  | _ => NotEq _ _
                  end
    | _ => NotEq _ _
    end
  end
).
Proof. (* a *) clear.
  abstract (destruct f as [|l r]; simpl in *; destruct Ha;
            destruct b as [Hb|Hb b'|Hb b']; destruct Hb;
            split).
Proof. (* b *) clear - eq.
  abstract (destruct f as [|l r]; simpl in *; destruct Ha; destruct Hb;
            simpl in *; destruct eq; split).
Proof. (* c *) clear - eq.
  abstract (destruct f as [|l r]; simpl in *; destruct Ha; destruct Hb;
            simpl in *; destruct eq; split).
Defined.

Lemma index_dec2 : ∀ f (a : index f), optProp (index_dec_aux a a).
Proof.
  fix 2; intros f [Ha|Ha a|Ha a]; [split| |];
  simpl; destruct f; destruct Ha; simpl in *;
  generalize (index_dec2 _ a); destruct (index_dec_aux a a); simpl;
  auto.
Qed.

Definition index_dec f := eq_dec2 (@index_dec_aux f) (@index_dec2 f).