Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Finite sets library.
 * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
 * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
 *              91405 Orsay, France *)

Require Import OrderedType Orders.
Set Implicit Arguments.

Some alternative (but equivalent) presentations for an Ordered Type

inferface.

The original interface

Module Type OrderedTypeOrig := OrderedType.OrderedType.

An interface based on compare

Module Type OrderedTypeAlt.

 Parameter t : Type.

 Parameter compare : t -> t -> comparison.

 Infix "?=" := compare (at level 70, no associativity).

 Parameter compare_sym :
   forall x y, (y?=x) = CompOpp (x?=y).
 Parameter compare_trans :
   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.

End OrderedTypeAlt.

From OrderedTypeOrig to OrderedType.

Module Update_OT (O:OrderedTypeOrig) <: OrderedType.

 Include Update_DT O.  (* Provides : t eq eq_equiv eq_dec *)

 Definition lt := O.lt.

 

StrictOrder lt

StrictOrder lt

Irreflexive lt

Transitive lt
x:O.t
Hx:lt x x

False

Transitive lt

Transitive lt
exact O.lt_trans. Qed.

Proper (eq ==> eq ==> iff) lt

Proper (eq ==> eq ==> iff) lt

Proper (eq ==> eq ==> impl) lt
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y

lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y

lt x' y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H':O.eq x' y

lt x' y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H':O.lt y x'
lt x' y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H':O.eq x' y

O.eq x y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H':O.lt y x'
lt x' y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H':O.lt y x'

lt x' y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y

lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
H':O.eq x' y'

lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
H':O.lt y' x'
lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
H':O.eq x' y'

O.eq x y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
H':O.lt y' x'
lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
H':O.eq x' y'

O.eq x' y
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
H':O.lt y' x'
lt x' y'
x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
H0:lt x' y
H':O.lt y' x'

lt x' y'
elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *. Qed. Definition compare x y := match O.compare x y with | EQ _ => Eq | LT _ => Lt | GT _ => Gt end.

forall x y : t, CompSpec eq lt x y (compare x y)

forall x y : t, CompSpec eq lt x y (compare x y)
intros; unfold compare; destruct O.compare; auto. Qed. End Update_OT.

From OrderedType to OrderedTypeOrig.

Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.

 Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *)

 Definition lt := O.lt.

 

forall x y : O.t, lt x y -> ~ eq x y

forall x y : O.t, lt x y -> ~ eq x y
x, y:O.t
L:lt y y
E:eq x y

False
apply (StrictOrder_Irreflexive y); auto. Qed.

Transitive lt

Transitive lt
apply O.lt_strorder. Qed.

forall x y : O.t, Compare lt eq x y

forall x y : O.t, Compare lt eq x y
intros x y; destruct (CompSpec2Type (O.compare_spec x y)); [apply EQ|apply LT|apply GT]; auto. Defined. End Backport_OT.

From OrderedTypeAlt to OrderedType.

Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.

 Definition t := t.

 Definition eq x y := (x?=y) = Eq.
 Definition lt x y := (x?=y) = Lt.

 

Equivalence eq

Equivalence eq

forall x : O.t, eq x x

forall x y : O.t, eq x y -> eq y x

forall x y z : O.t, eq x y -> eq y z -> eq x z
(* refl *)
x:O.t

(x ?= x) = Eq

forall x y : O.t, eq x y -> eq y x

forall x y z : O.t, eq x y -> eq y z -> eq x z
x:O.t
H:(x ?= x) = CompOpp (x ?= x)

(x ?= x) = Eq

forall x y : O.t, eq x y -> eq y x

forall x y z : O.t, eq x y -> eq y z -> eq x z

forall x y : O.t, eq x y -> eq y x

forall x y z : O.t, eq x y -> eq y z -> eq x z
(* sym *)
x, y:O.t
H:(x ?= y) = Eq

(y ?= x) = Eq

forall x y z : O.t, eq x y -> eq y z -> eq x z

forall x y z : O.t, eq x y -> eq y z -> eq x z
(* trans *) apply compare_trans. Qed.

StrictOrder lt

StrictOrder lt

forall x : O.t, (x ?= x) = Lt -> False
x:O.t
H:(x ?= x) = Lt

False
x:O.t
H:(x ?= x) = Lt
H0:eq x x

False
unfold eq in *; congruence. Qed.

forall x y z : O.t, lt x y -> eq y z -> lt x z

forall x y z : O.t, lt x y -> eq y z -> lt x z
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(y ?= z) = Eq

(x ?= z) = Lt
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(y ?= z) = Eq
Hxz:(x ?= z) = Eq

Eq = Lt
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(y ?= z) = Eq
Hxz:(x ?= z) = Gt
Gt = Lt
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(z ?= y) = CompOpp Eq
Hxz:(x ?= z) = Eq

Eq = Lt
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(y ?= z) = Eq
Hxz:(x ?= z) = Gt
Gt = Lt
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(z ?= y) = Eq
Hxz:(x ?= z) = Eq

Eq = Lt
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(y ?= z) = Eq
Hxz:(x ?= z) = Gt
Gt = Lt
x, y, z:O.t
Hxy:(x ?= y) = Lt
Hyz:(y ?= z) = Eq
Hxz:(x ?= z) = Gt

Gt = Lt
x, y, z:O.t
Hxy:(y ?= x) = CompOpp Lt
Hyz:(y ?= z) = Eq
Hxz:(x ?= z) = Gt

Gt = Lt
x, y, z:O.t
Hxy:(y ?= x) = Gt
Hyz:(y ?= z) = Eq
Hxz:(x ?= z) = Gt

Gt = Lt
rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. Qed.

forall x y z : O.t, eq x y -> lt y z -> lt x z

forall x y z : O.t, eq x y -> lt y z -> lt x z
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(y ?= z) = Lt

(x ?= z) = Lt
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(y ?= z) = Lt
Hxz:(x ?= z) = Eq

Eq = Lt
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(y ?= z) = Lt
Hxz:(x ?= z) = Gt
Gt = Lt
x, y, z:O.t
Hxy:(y ?= x) = CompOpp Eq
Hyz:(y ?= z) = Lt
Hxz:(x ?= z) = Eq

Eq = Lt
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(y ?= z) = Lt
Hxz:(x ?= z) = Gt
Gt = Lt
x, y, z:O.t
Hxy:(y ?= x) = Eq
Hyz:(y ?= z) = Lt
Hxz:(x ?= z) = Eq

Eq = Lt
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(y ?= z) = Lt
Hxz:(x ?= z) = Gt
Gt = Lt
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(y ?= z) = Lt
Hxz:(x ?= z) = Gt

Gt = Lt
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(z ?= y) = CompOpp Lt
Hxz:(x ?= z) = Gt

Gt = Lt
x, y, z:O.t
Hxy:(x ?= y) = Eq
Hyz:(z ?= y) = Gt
Hxz:(x ?= z) = Gt

Gt = Lt
rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. Qed.

Proper (eq ==> eq ==> iff) lt

Proper (eq ==> eq ==> iff) lt

Proper (eq ==> eq ==> impl) lt
x, y:O.t
H:eq x y
x0, y0:O.t
H0:eq x0 y0
H1:lt x x0

(y ?= y0) = Lt
x, y:O.t
H:eq x y
x0, y0:O.t
H0:eq x0 y0
H1:lt x x0

lt y x0
x, y:O.t
H:eq x y
x0, y0:O.t
H0:eq x0 y0
H1:lt x x0

eq y x
symmetry; auto. Qed. Definition compare := O.compare.

forall x y : O.t, CompSpec eq lt x y (compare x y)

forall x y : O.t, CompSpec eq lt x y (compare x y)
x, y:O.t

CompSpec (fun x0 y0 : O.t => (x0 ?= y0) = Eq) (fun x0 y0 : O.t => (x0 ?= y0) = Lt) x y (x ?= y)
x, y:O.t
H:(x ?= y) = Gt

CompSpec (fun x0 y0 : O.t => (x0 ?= y0) = Eq) (fun x0 y0 : O.t => (x0 ?= y0) = Lt) x y Gt
x, y:O.t
H:(x ?= y) = Gt

(y ?= x) = Lt
rewrite compare_sym, H; auto. Qed.

forall x y : O.t, {eq x y} + {~ eq x y}

forall x y : O.t, {eq x y} + {~ eq x y}
x, y:O.t

{(x ?= y) = Eq} + {(x ?= y) <> Eq}
case (x ?= y); [ left | right | right ]; auto; discriminate. Defined. End OT_from_Alt.
From the original presentation to this alternative one.
Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.

 Definition t := t.
 Definition compare := compare.

 Infix "?=" := compare (at level 70, no associativity).

 

forall x y : O.t, (y ?= x) = CompOpp (x ?= y)

forall x y : O.t, (y ?= x) = CompOpp (x ?= y)
x, y:O.t

O.compare y x = CompOpp (O.compare x y)
x, y:O.t
U:eq x y
V:lt y x

Lt = CompOpp Eq
x, y:O.t
U:eq x y
V:lt x y
Gt = CompOpp Eq
x, y:O.t
U:lt x y
V:eq y x
Eq = CompOpp Lt
x, y:O.t
U:lt x y
V:lt y x
Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:eq x y
V:lt y y

Lt = CompOpp Eq
x, y:O.t
U:eq x y
V:lt x y
Gt = CompOpp Eq
x, y:O.t
U:lt x y
V:eq y x
Eq = CompOpp Lt
x, y:O.t
U:lt x y
V:lt y x
Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:eq x y
V:lt x y

Gt = CompOpp Eq
x, y:O.t
U:lt x y
V:eq y x
Eq = CompOpp Lt
x, y:O.t
U:lt x y
V:lt y x
Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:eq x y
V:lt y y

Gt = CompOpp Eq
x, y:O.t
U:lt x y
V:eq y x
Eq = CompOpp Lt
x, y:O.t
U:lt x y
V:lt y x
Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:lt x y
V:eq y x

Eq = CompOpp Lt
x, y:O.t
U:lt x y
V:lt y x
Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:lt x x
V:eq y x

Eq = CompOpp Lt
x, y:O.t
U:lt x y
V:lt y x
Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:lt x y
V:lt y x

Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:lt x x
V:lt y x

Lt = CompOpp Lt
x, y:O.t
U:lt y x
V:eq y x
Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:lt y x
V:eq y x

Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:lt x x
V:eq y x

Eq = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y
Gt = CompOpp Gt
x, y:O.t
U:lt y x
V:lt x y

Gt = CompOpp Gt
x, y:O.t
U:lt y y
V:lt x y

Gt = CompOpp Gt
elim (StrictOrder_Irreflexive y); auto. Qed.

forall x y : O.t, (x ?= y) = Eq <-> eq x y

forall x y : O.t, (x ?= y) = Eq <-> eq x y

forall x y : O.t, O.compare x y = Eq <-> eq x y
x, y:O.t
H:lt x y
H0:eq x y

Lt = Eq
x, y:O.t
H:lt y x
H0:eq x y
Gt = Eq
x, y:O.t
H:lt y y
H0:eq x y

Lt = Eq
x, y:O.t
H:lt y x
H0:eq x y
Gt = Eq
x, y:O.t
H:lt y x
H0:eq x y

Gt = Eq
x, y:O.t
H:lt y y
H0:eq x y

Gt = Eq
elim (StrictOrder_Irreflexive y); auto. Qed.

forall x y : O.t, (x ?= y) = Lt <-> lt x y

forall x y : O.t, (x ?= y) = Lt <-> lt x y

forall x y : O.t, O.compare x y = Lt <-> lt x y
x, y:O.t
H:eq x y
H0:lt x y

Eq = Lt
x, y:O.t
H:lt y x
H0:lt x y
Gt = Lt
x, y:O.t
H:eq x y
H0:lt y y

Eq = Lt
x, y:O.t
H:lt y x
H0:lt x y
Gt = Lt
x, y:O.t
H:lt y x
H0:lt x y

Gt = Lt
x, y:O.t
H:lt y x
H0:lt x x

Gt = Lt
elim (StrictOrder_Irreflexive x); auto. Qed.

forall x y : O.t, (x ?= y) = Gt <-> lt y x

forall x y : O.t, (x ?= y) = Gt <-> lt y x
x, y:O.t

(x ?= y) = Gt <-> lt y x
x, y:O.t

(y ?= x) = CompOpp Gt <-> lt y x
apply compare_Lt. Qed.

forall (c : comparison) (x y z : O.t), (x ?= y) = c -> (y ?= z) = c -> (x ?= z) = c

forall (c : comparison) (x y z : O.t), (x ?= y) = c -> (y ?= z) = c -> (x ?= z) = c
c:comparison
x, y, z:O.t

(x ?= y) = c -> (y ?= z) = c -> (x ?= z) = c
destruct c; unfold compare; rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt; transitivity y; auto. Qed. End OT_to_Alt.