Using a module's definition in Coq

Question

The following code states that it defines finite sets in Coq with the axiom of extensionality:

(** A library for finite sets with extensional equality.

    Author: Brian Aydemir. *)

Require Import FSets.
Require Import ListFacts.
Require Import Coq.Logic.ProofIrrelevance.


(* *********************************************************************** *)
(** * Interface *)

(** The following interface wraps the standard library's finite set
    interface with an additional property: extensional equality. *)

Module Type S.

  Declare Module E : UsualOrderedType.
  Declare Module F : FSetInterface.S with Module E := E.

  Parameter eq_if_Equal :
    forall s s' : F.t, F.Equal s s' -> s = s'.

End S.


(* *********************************************************************** *)
(** * Implementation *)

(** For documentation purposes, we hide the implementation of a
    functor implementing the above interface.  We note only that the
    implementation here assumes (as an axiom) that proof irrelevance
    holds. *)

Module Make (X : UsualOrderedType) <: S with Module E := X.

  (* begin hide *)

  Module E := X.
  Module F := FSetList.Make E.
  Module OFacts := OrderedType.OrderedTypeFacts E.

  Lemma eq_if_Equal :
    forall s s' : F.t, F.Equal s s' -> s = s'.
  Proof.
    intros [s1 pf1] [s2 pf2] Eq.
    assert (s1 = s2).
      unfold F.MSet.Raw.t in *.
      eapply Sort_InA_eq_ext; eauto.
      intros; eapply E.lt_trans; eauto.
      1 : {
        apply F.MSet.Raw.isok_iff.
        auto.
      }
      1 : {
        apply F.MSet.Raw.isok_iff.
        auto.
      }
    subst s1.
    assert (pf1 = pf2).
    apply proof_irrelevance.
    subst pf2.
    reflexivity.
  Qed.

  (* end hide *)

End Make.

How can I define a function with signature from finite sets to finite sets using this module?

larsr larsr · Accepted Answer · 2020-09-22T07:08:37

You need to define a Module (call it M) that implements the UsualOrderedType module type for the type you want to make finite sets out of, and then build another Module with Make M which contains an implementation of finite sets for your type.

Module M <: UsualOrderedType.
   ...
End M.
Module foo := Make M.
Check foo.F.singleton.

Note that you need to declare the module type with <: instead of just :, otherwise you are hiding the fact that the module is defined for (in the example below) nat behind an opaque type t.

Say you want to make finite sets of nats:

(* Print the module type to see all the things you need to define. *)

Print Module Type UsualOrderedType. 

Require Import PeanonNat.

Module NatOrdered <: UsualOrderedType .   (* note the `<:` *)
  Definition t:=nat.
  Definition eq:=@eq nat.
  Definition lt:=lt.
  Definition eq_refl:=@eq_refl nat.
  Definition eq_sym:=@eq_sym nat.
  Definition eq_trans:=@eq_trans nat.
  Definition lt_trans:=Nat.lt_trans.
  (* I wrote Admitted where I didn't provide an implementation *)
  Definition lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Admitted.
  Definition compare : forall x y : t, Compare lt eq x y. Admitted.
  Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Admitted.
End NatOrdered.

Now you can create a module that uses this ordered type.

Module foo := Make NatOrdered.

Print foo.F.  (* to see everything that is defined for the FSetList *)
Import foo.  (* get F in our namespace so we can say F.t instead of foo.F.t, etc. *)

Now we can use our F module. The finite sets have type F.t and the elements have type F.elt which is coercible to nat since we know they come from NatOrdered.

Lets build a function that uses stuff from F.

Definition f: F.elt -> F.t.
  intros x. apply (F.singleton x).
Defined.

Print F.
Goal F.cardinal (F.union (f 1) (f 2)) = 2.
  compute.

Ok. That gets stuck halfway through the computation because I didn't implement compare above. I was lazy and just wrote Admitted. But you can do it! :-)

Using a module's definition in Coq

1 Answers