Constructive proofs in SML's module language

proofs.sml

(* It is not possible in Standard ML to construct an identity type (or any other
 * indexed type), but that does not stop us from speculating. We can specify with
 * a signature equality should mean, and then use a functor to say, "If there
 * were a such thing as equality, then we could prove these things with it."
 * Likewise, we can use the same trick to define the booleans and their
 * induction principle at the type-level, and speculate what proofs we could
 * make if we indeed had the booleans and their induction principle.
 *
 * Functions may be defined by asserting their inputs and outputs as
 * propositional equalities in a signature; these "functions" do not compute,
 * but you will find that (with enough patience) it is possible to prove things
 * about them using the induction principle we have posited.
 *)

signature EQUALITY =
sig
  type ('a, 'b) eq
  val refl  : ('a, 'a) eq
  val symm  : ('a, 'b) eq -> ('b, 'a) eq
  val trans : ('a, 'b) eq -> ('b, 'c) eq -> ('a, 'c) eq

  functor CONG (P : sig type 'a p end) :
  sig
    val cong : ('a, 'b) eq -> ('a P.p, 'b P.p) eq
  end
end

signature BOOL =
sig
  type tt
  type ff

  functor IND (P : sig type 'b p end) :
  sig
    val induction : tt P.p -> ff P.p -> 'b P.p
  end
end

signature BOOL_LIB =
sig
  include BOOL
  include EQUALITY

  type 'b not
  val not_tt : (tt not, ff) eq
  val not_ff : (ff not, tt) eq

  type ('a, 'b) conj
  val tt_and_x : ((tt, 'x) conj, 'x) eq
  val ff_and_x : ((ff, 'x) conj, ff) eq
end

functor REASONING (B : BOOL_LIB) =
struct
  open B

  (* Π[x : bool]. not (not x) = x *)
  functor NOTNOT_ID (X : sig type x end) =
  struct
    type 'b goal = ('b not not, 'b) eq

    structure CONG = CONG(type 'a p = 'a not)
    structure IND = IND(type 'b p = 'b goal)

    val proof : X.x goal =
      let open IND CONG in
        induction (trans (cong not_tt) not_ff) (trans (cong not_ff) not_tt)
      end
  end

  (* Π[x,y : bool]. x & y = y & x *)
  functor CONJ_COMMUTATIVE (X : sig type x type y end) =
  struct
    type ('x, 'y) goal = (('x, 'y) conj, ('y, 'x) conj) eq

    structure IND_x = IND(type 'b p = ('b, X.y) goal)
    structure IND_tt_y = IND(type 'b p = (tt, 'b) goal)
    structure IND_ff_y = IND(type 'b p = (ff, 'b) goal)

    val proof : (X.x, X.y) goal =
      IND_x.induction
        (IND_tt_y.induction refl (trans tt_and_x (symm ff_and_x)))
        (IND_ff_y.induction (trans ff_and_x (symm tt_and_x)) refl)
  end
end