As an exercise in learning Coq, I've implemented a proof-carrying version of the partial-ordering relation: https://github.com/aweinstock314/coq-stuff/blob/a183

As an exercise in learning Coq, I've implemented a proof-carrying version of the partial-ordering relation: https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e957c0038996a5a65fcb4391967660a/poset_lattice.v#L3-L24 https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e95... There's four different types there: POSET, POSET_PROOFS, Pord, and POSET'. - POSET only has an underlying type t and a function "leq" that takes two elements of type t and returns a bool (but doesn't enforce semantics of that bool). - POSET_PROOFS embeds a POSET, and carries three proofs (reflexivity, antisymmetry, and transitivity) certifying that the underlying "leq" function is actually the less-than-or-equal function of a partial ordering. - Pord is a result type with 4 values meant to denote the exhaustive possiblities of "strictly less"/"equal"/"strictly greater"/"uncomparable". - POSET' has a type t', a function "pcomp" that takes two elements of type t' and returns a Pord, and a proof for transitivity in the "strictly less" case. POSET' has fewer fields to instantiate, but POSET_PROOFS allows writing proofs that are closer to traditional math. Fortunately, the fact that it's possible to write conversions between POSET_PROOFS and POSET' (done in the code as "from" and "to" in the POSET_ISOMORPHIMS module right below) indicate that they have the same properties.