A Tutorial on Using Modules

Coq's module system can be used to parameterise proofs over structures. For instance rather than writing min and max functions, lemma and tactics for nat, Z, Q, etc., we can write the proofs once for an abstract decidable total order and then instanciate these functions, lemmas and tactics for each structure.

This tutorial uses unicode characters and hence requires the Utf8 Module.

Require Import Utf8.

The first step is to write a Module Type in a file that contains the signature of the abstract structure to work from. This will be the signature of a decidable total order. A Module Type is just a listing of Parameters and Axioms. In this case we also add a Notation to make the syntax nicer.

(* File: DecidableOrder.v
 * Part 1
 *)
Module Type Sig.
  Parameter A : Type.
  Parameter le : A ⇒ A ⇒ Prop.
  Infix "≤" := le : order_scope.
  Open Scope order_scope.
  Axiom le_refl : ∀ x, x ≤ x.
  Axiom le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y.
  Axiom le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
  Axiom le_total : ∀ x y, {x ≤ y} + {y ≤ x}.
  Parameter le_dec : ∀ x y, {x ≤ y} +{¬ x ≤ y}.
End Sig.

Now we can write a module functor. A module functor is a Module that takes one or more Modules of some Module Types as parameters. For example we can create a Module that defines a min function and lemmas for any Module that has the above Module Type signature. The first thing we do is Import the Module parameter in order to have access to its parameters without having to use the DotNotation. Notice that we also get access to the Notation defined in the Module Type.

(* File: DecidableOrder.v
 * Part 2
 *)
Module Min (Ord : Sig).
  Import Ord.
  Hint Resolve le_refl.

  Definition min a b : A := if (le_dec a b) then a else b.

  Lemma case_min : ∀ P : A ⇒ Type, ∀ x y, (x ≤ y ⇒ P x) ⇒ (y ≤ x ⇒ P y) ⇒ P (min x y).
  Proof.
    intros.
    unfold min.
    destruct (le_dec x y).
    tauto.
    destruct (le_total x y).
    absurd (le x y); assumption.
    tauto.
  Qed.

  Lemma min_glb : ∀ x y z, z ≤ x ⇒ z ≤ y ⇒ z ≤ min x y.
  Proof.
    intros.
    apply case_min; tauto.
  Qed.

  Lemma min_sym : ∀ x y, min x y = min y x.
  Proof.
    intros.
    set (H:=le_antisym).
    do 2 apply case_min; auto.
  Qed.

  Lemma min_left : ∀ x y, min x y ≤ x.
  Proof.
    intros.
    apply case_min; auto.
  Qed.

  Lemma min_right : ∀ x y, min x y ≤ y.
  Proof.
    intros.
    apply case_min; auto.
  Qed.
End Min.

Suppose you have a data type, such as Qpositive, that has a decidable total order and we want to make an instance of min and its lemmas for it. We first must create a module satisfying the module signature. The <: notation says that we are making a Module that (transparently) satisfies a given Module Type. We are then required to have inside our module a list of Definitions and Lemmas that have the same name and types as those listed in the module type's signature. This work is specific to Qpositive and therefore it should go into a different file.

(* File: QpositiveOrder.v
 * Part 1
 *)
Require Import utf8.
Require Export Qpositive_order.
Require DecidableOrder.

Module QDecidableOrderSig <: DecidableOrder.Sig.
  Definition A := Qpositive.
  Definition le := Qpositive_le.
  Definition le_refl := Qpositive_le_refl.
  Definition le_antisym := Qpositive_le_antisym.
  Definition le_trans := Qpositive_le_trans.
  Definition le_total := Qpositive_le_total.

  Infix "≤" := le : Qpos_scope.
  Bind Scope Qpos_scope with Qpositive.
  Open Scope Qpos_scope.

  Lemma le_dec : ∀ x y, {x ≤ y} + {¬ x ≤ y}.
  Proof.
    intros.
    unfold le, Qpositive_le.
    decide equality (Qpositive_le_bool x y) true.
  Defined.
End QDecidableOrderSig.

To use the module functor, we must apply it to this module and give the resulting module a name. Then we can do whatever we want with the resulting module, such as exporting it.

Module Order := DecidableOrder.Min QDecidableOrderSig.
Export QDecidableOrderSig.
Export Order.
Print min.

prints:

min = fun a b : A => if le_dec a b then a else b
     : A ⇒  A ⇒  A

That is the basics of how to use modules.

Advanced Module Work

Suppose we want to also define a max function. We could redo all the same sort of work that we did for min; however the proofs are all almost identical. We would like to reuse that work we did creating min to also create max. To accomplish this we note that max is dual to min. That is to say that max is the min function of the reversed ordering. For any decidable total ordering, the reverse ordering is also a decidable total ordering. We can make a module functor that creates this dual order. The Dual module defined below will take a module of our decidable total order signature, but also produce a module statisfying our decidable total order signature.

(* File: DecidableOrder.v
 * Part 3
 *)
Module Dual (Ord : Sig) <: Sig.
  Definition A := Ord.A.
  Definition le a b : Prop := Ord.le b a.

  Infix "≤" := le : order_scope.
  Open Scope order_scope.

  Definition le_refl := Ord.le_refl.

  Lemma le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x=y.
  Proof.
    unfold le.
    set (H:=Ord.le_antisym).
    auto.
  Qed.

  Lemma le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
  Proof.
    unfold le.
    intuition.
    apply Ord.le_trans with y; assumption.
  Qed.

  Lemma le_total : ∀ x y, {x ≤ y} + {y ≤ x}.
  Proof.
    unfold le.
    set (H:=Ord.le_total).
    auto.
  Defined.

  Definition le_dec : ∀ x y, {x ≤ y} + {¬x ≤ y}.
    unfold le.
    set (H:=Ord.le_dec).
    auto.
  Defined.
End Dual.

Now we create a Max module that imports that creates an instance of the Min module for the dual ordering. We cannot just export the Max module because the names are all wrong. Instead we create the proper names and types for the items in the Max module as follows.

(* File: DecidableOrder.v
 * Part 4
 *)
Module Max (Ord : Sig).
  Import Ord.
  Module DualOrd := Dual Ord.
  Module Max := Min DualOrd.
  Definition max := Max.min.
  Definition case_max
    : ∀ P : A ⇒ Type, ∀ x y, (y ≤ x ⇒ P x) ⇒ (x ≤ y ⇒ P y) ⇒ P (max x y)
    := Max.case_min.
  Definition max_lub : ∀ x y z, x ≤ z ⇒ y ≤ z ⇒ max x y ≤ z := Max.min_glb.
  Definition max_sym : ∀ x y, max x y = max y x := Max.min_sym.
  Definition max_left : ∀ x y, x ≤ (max x y) := Max.min_left.
  Definition max_right : ∀ x y, y ≤ (max x y) := Max.min_right.
End Max.

Finally we can create a single module that exports both the Min and Max modules.

(* File: DecidableOrder.v
 * Part 5
 *)
Module MinMax (Ord : Sig).
  Export Ord.
  Module MinOrd := Min Ord.
  Export MinOrd.
  Module MaxOrd := Max Ord.
  Export MaxOrd.
End MinMax.

With min and max in hand we can prove properties involving both of them. For example, we can prove that min distributed over max. This goes into another module.

(* File: DecidableOrder.v
 * Part 6
 *)
Module DistributivityA (Ord : Sig).
  Module MinMaxOrd := MinMax Ord.
  Import MinMaxOrd.

  Lemma min_max_distr : ∀ x y z, (min x (max y z)) = (max (min x y) (min x z)).
  Proof.
    intros.
    set (H:=le_antisym).
    set (H0:=(le_trans x y z)).
    set (H1:=(le_trans x z y)).
    set (H2:=(le_trans z x y)).
    set (H3:=(le_trans y x z)).
    repeat apply case_min; repeat apply case_max; auto.
  Qed.
End DistributivityA.

We can prove the dual lemma that states that max distributes over min by using the same dualizing technique that we used to define max in terms of min. This can be combined with the above into one distributivity module.

(* File: DecidableOrder.v
 * Part 7
 *)
Module DistributivityB (Ord : Sig).
  Module MinMaxOrd := MinMax Ord.
  Import MinMaxOrd.
  Module DualOrd := Dual Ord.
  Module DualDistrib := DistributivityA DualOrd.

  Definition max_min_distr
    : ∀ x y z, (max x (min y z)) = (min (max x y) (max x z))
    := DualDistrib.min_max_distr.
End DistributivityB.

Module Distributivity  (Ord : Sig).
  Module MinMaxOrd := MinMax Ord.
  Export MinMaxOrd.
  Module DistributivityAOrd := DistributivityA Ord.
  Export DistributivityAOrd.
  Module DistributivityBOrd := DistributivityB Ord.
  Export DistributivityBOrd.
End Distributivity.

Finally at the end of the file, we place a Theory Module that exports all of the modules that we have defined.

(* File: DecidableOrder.v
 * Part 8
 *)
Module Theory (Ord : Sig).
  Module DistributivityOrd := Distributivity Ord.
  Export DistributivityOrd.
End Theory.

This Theory module functor can be instantiated and exported inside the QpositiveOrder.v file.

(* File: QpositiveOrder.v
 * Part 2
 *)
Module Order := DecidableOrder.Theory QDecidableOrderSig.
Export Order.