Skip to content

Instantly share code, notes, and snippets.

@jonsterling
Last active January 2, 2016 04:48
Show Gist options
  • Save jonsterling/8252466 to your computer and use it in GitHub Desktop.
Save jonsterling/8252466 to your computer and use it in GitHub Desktop.
Constructive proofs in SML's module language
(* 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment