The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I know of 3 ways to reprensent finite types:

Record fin1 (n:nat) := { v : nat; ranged : v <  n }.

Fixpoint fin2 (n:nat) := match n with O => emptySet | S n => option (fin2 n) end.

Inductive fin3 : nat -> Type := X : forall n, fin3 (S n) | Y : forall n, fin3 n -> fin3 (S n).

I often find the second one a good one for low-level stuff.

The third one seems nice, but in fact indice manipulation is really annoying if you do not use a complete enough library to deal with it (I think Coq has some implemented in stdlib).

The first one remains interesting when you have stuff with a lot of arithmetic (in this case, you should forget the other two).

If you do a lot of computationnal things, you may also want to replace the definition of "lt" with something more computationnal, like

Fixpoint lt (m n : nat) : Prop := match n with O => False | S n => match m with O => True | S m => lt m n end end.

Beside that, as Robert wrote you can define:

Record domfun (m n : nat) := DF { df : nat -> nat; dom_spe : forall x, x<m -> (f x) < n }.

This allows you to write things like:

Notation "⟦ f ⟧" := (@df _ _ f).

Notation "« f »" := (@dom_spe _ _ _).

Definition compose (m n o : nat) (f : domfun n o) (g : domfun m n) : domfun m o :=

  DF (fun x => ⟦f⟧ (⟦g⟧ x))
     (fun x (ltxm:x<m) => «f» («g» ltxm)).

or

Definition compose (m n o : nat) (f : domfun n o) (g : domfun m n) : domfun m o.

refine (DF (fun x => ⟦f⟧ (⟦g⟧ x)) _).

Proof.
…

Defined. (* And not Qed, as you still want df to be accessible. *)

Or with completely separated definitions (for example in separated files):

Definition compose_fun (m n o : nat) (f : domfun n o) (g : domfun m n) : nat -> nat :=
  fun x => ⟦f⟧ (⟦g⟧ x).
…

Lemma compose_spe (m n o : nat) (f : domfun n o) (g : domfun m n) : forall x, x<m -> compose_fun m n o f g x < o.
Proof. … Qed.
…

Definition compose (m n o : nat) (f : domfun n o) (g : domfun m n) : domfun m o :=

  DF (compose_fun m n o f g) (compose_spe m n o f g).

In all these writings, you have a rather clear separation on computation and proof and you do not play too much with constructors and projectors.

2015-08-18 22:50 GMT+02:00 Vadim Zaliva <vzaliva AT cmu.edu>:

Hi!

I am dealing with proofs which involve class of functions which domain is natural
numbers from 0 to some ’n’ and the range is also natural numbers from 0 to some ‘m’.
Currently I formalized them in Coq as follows:


Definition index_map_spec (domain range: nat) :=
  forall n : nat, n < domain -> {v : nat | v < range}.

For example, an identity function would be:

  Program Definition identity_index_map
          (dr: nat):
    index_map_spec dr dr
    :=
      fun i _ => i.

Are there are other, alternative representations for such functions? My current one works but
proofs look a big messy as expressions end up littered with projection function applications.

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva