equality and its negation!

Refl.ml

module False = struct
  (** This empty type represents falsehood. No proof (term) of
      it exists. *)
  type t = |

  (** [ex_falso_quodlibet] states that if we have the proof of
      falsehood, then we can prove anything. *)
  let ex_falso_quodlibet : 'a. t -> 'a = function
    | _ -> .
end

module Negation = struct
  (** The [Negation.t] of [a] represents its negation. *)
  type 'a t = 'a -> False.t

  (** [make_double_negation a] states that if you have [a],
      then you can conclude [¬¬a] (read: not not [a]). *)
  let make_double_negation : 'a. 'a -> 'a t t = fun x f -> f x
end

module Eq : sig
  (** [Eq.t] represents equality. *)
  type (_, _) t = Refl : 'a. 'a -> ('a, 'a) t

  (** [reflexivity a] states that if we have [a], then we have
      [a = a]. *)
  val reflexivity : 'a. 'a -> ('a, 'a) t

  (** [symmetry eq_a_b] states that if we have [a = b], then we
      have [b = a]. *)
  val symmetry : 'a 'b. ('a, 'b) t -> ('b, 'a) t

  (** [transitivity eq_a_b eq_b_c] states that if we have
      [a = b] and [b = c], then we have [a = c]. *)
  val transitivity
    : 'a 'b 'c.
    ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t

  module Induction : sig
    (** [Induction] is a proof of induction on equality, which
        also happens to match Leibniz's definition of equality. *)

    module type ARGS = sig
      (** [ARGS] regroups all the required arguments for the
          induction. *)

      (** [ty] is *some* type. It really doesn't matter which
          one. We will take the example of weathers.
          
          Note that the parameter is used here as a way to
          discriminate between specific inhabitants of [ty]. *)
      type _ ty

      (** [x] is a discriminant for [ty] that represents some
          value of that type. For our example, let's say that
          it's the rain. *)
      type x

      (** [_p] is an unfortunate implementation detail: OCaml
          does not let us constraint parameters of abstract
          types directly. *)
      type 'a _p

      (** [p] represents a proposition about ['a], which is a
          member of [ty]. It could be the statement:
          "Given a weather, the floor is wet." *)
      type 'a p = 'a _p constraint 'a = 'b ty

      (** [px] is a proof that [p] holds for [x] specifically.
          Indeed, rain makes the floor wet. *)
      val px : x ty p

      (** [a] is another discriminant for [ty]. *)
      type a

      (** [eq_x_a] is a proof that [x = a]. [a] is also the
          rain! *)
      val eq_x_a : (x, a) t
    end

    module type TYPE = sig
      (** [TYPE] represents the conclusion of the induction
          principle applied to some instance of [ARGS]. *)

      (** [Args] is all the hypotheses needed. *)
      module Args : ARGS

      open Args

      (** [pa] is the proof that the weather [a] makes the
          floor wet. *)
      val pa : a ty p
    end

    (** [Make Args] builds the conclusion of the induction
        based on the hypotheses [Args]. *)
    module Make : (_ : ARGS) -> TYPE

    (** [induction] states that given a type [ty], a value
        [x : ty], a proposition [P (a : ty)] and a proof of
        [P x], then for every [a : ty] that is equal to [x],
        we can conclude [P a].
        
        We know that the rain makes the floor wet, so every
        weather that is the same as the rain also makes the
        floor wet. *)
    val induction : (module ARGS) -> (module TYPE)
  end
end = struct
  type (_, _) t = Refl : 'a. 'a -> ('a, 'a) t

  let reflexivity : type a. a -> (a, a) t = fun a -> Refl a

  let symmetry : type a b. (a, b) t -> (b, a) t = function
    | Refl a -> Refl a

  let transitivity
    : type a b c. (a, b) t -> (b, c) t -> (a, c) t
    =
    fun (Refl a) (Refl _) -> Refl a

  module Induction = struct
    module type ARGS = sig
      type x
      type _ ty
      type 'a _p
      type 'a p = 'a _p constraint 'a = 'b ty

      val px : x ty p

      type a

      val eq_x_a : (x, a) t
    end

    module type TYPE = sig
      module Args : ARGS
      open Args

      val pa : a ty p
    end

    module Make (Args : ARGS) : TYPE = struct
      module Args = Args
      open Args

      let pa : a ty p =
        match eq_x_a with
        | Refl x -> px
    end

    let induction : (module ARGS) -> (module TYPE) =
      fun (module I) -> (module Make (I))
  end
end

module Neq = struct
  (** [Neq] represents the non-equality. *)
  type ('a, 'b) t = ('a, 'b) Eq.t Negation.t

  (** [symmetry] states that if [a ≠ b], then we can conclude
      that [b ≠ a]. *)
  let symmetry : type a b. (a, b) t -> (b, a) t =
    fun f x -> f (Eq.symmetry x)

  (** [neq_eq_neq] states that given two terms [a] and [b],
      [a = b] and [a ≠ b] are not equal. *)
  let neq_eq_neq : type a b. ((a, b) Eq.t, (a, b) t) t
    = function
    | _ -> .
end