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.
Module Type OrderedTypeOrig := OrderedType.OrderedType.
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.
Module Update_OT (O:OrderedTypeOrig) <: OrderedType. Include Update_DT O. (* Provides : t eq eq_equiv eq_dec *) Definition lt := O.lt.StrictOrder ltStrictOrder ltIrreflexive ltTransitive ltx:O.tHx:lt x xFalseTransitive ltexact O.lt_trans. Qed.Transitive ltProper (eq ==> eq ==> iff) ltProper (eq ==> eq ==> iff) ltProper (eq ==> eq ==> impl) ltx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x ylt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x ylt x' yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' ylt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH':O.eq x' ylt x' yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH':O.lt y x'lt x' yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' ylt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH':O.eq x' yO.eq x yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH':O.lt y x'lt x' yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' ylt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH':O.lt y x'lt x' yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' ylt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' ylt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' yH':O.eq x' y'lt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' yH':O.lt y' x'lt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' yH':O.eq x' y'O.eq x yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' yH':O.lt y' x'lt x' y'x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' yH':O.eq x' y'O.eq x' yx, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' yH':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.x, x':tHx:eq x x'y, y':tHy:eq y y'H:lt x yH0:lt x' yH':O.lt y' x'lt 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.forall x y : t, CompSpec eq lt x y (compare x y)
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 yforall x y : O.t, lt x y -> ~ eq x yapply (StrictOrder_Irreflexive y); auto. Qed.x, y:O.tL:lt y yE:eq x yFalseTransitive ltapply O.lt_strorder. Qed.Transitive ltforall x y : O.t, Compare lt eq x yintros x y; destruct (CompSpec2Type (O.compare_spec x y)); [apply EQ|apply LT|apply GT]; auto. Defined. End Backport_OT.forall x y : O.t, Compare lt eq x y
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 eqEquivalence eq(* refl *)forall x : O.t, eq x xforall x y : O.t, eq x y -> eq y xforall x y z : O.t, eq x y -> eq y z -> eq x zx:O.t(x ?= x) = Eqforall x y : O.t, eq x y -> eq y xforall x y z : O.t, eq x y -> eq y z -> eq x zx:O.tH:(x ?= x) = CompOpp (x ?= x)(x ?= x) = Eqforall x y : O.t, eq x y -> eq y xforall x y z : O.t, eq x y -> eq y z -> eq x z(* sym *)forall x y : O.t, eq x y -> eq y xforall x y z : O.t, eq x y -> eq y z -> eq x zx, y:O.tH:(x ?= y) = Eq(y ?= x) = Eqforall x y z : O.t, eq x y -> eq y z -> eq x z(* trans *) apply compare_trans. Qed.forall x y z : O.t, eq x y -> eq y z -> eq x zStrictOrder ltStrictOrder ltforall x : O.t, (x ?= x) = Lt -> Falsex:O.tH:(x ?= x) = LtFalseunfold eq in *; congruence. Qed.x:O.tH:(x ?= x) = LtH0:eq x xFalseforall x y z : O.t, lt x y -> eq y z -> lt x zforall x y z : O.t, lt x y -> eq y z -> lt x zx, y, z:O.tHxy:(x ?= y) = LtHyz:(y ?= z) = Eq(x ?= z) = Ltx, y, z:O.tHxy:(x ?= y) = LtHyz:(y ?= z) = EqHxz:(x ?= z) = EqEq = Ltx, y, z:O.tHxy:(x ?= y) = LtHyz:(y ?= z) = EqHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(x ?= y) = LtHyz:(z ?= y) = CompOpp EqHxz:(x ?= z) = EqEq = Ltx, y, z:O.tHxy:(x ?= y) = LtHyz:(y ?= z) = EqHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(x ?= y) = LtHyz:(z ?= y) = EqHxz:(x ?= z) = EqEq = Ltx, y, z:O.tHxy:(x ?= y) = LtHyz:(y ?= z) = EqHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(x ?= y) = LtHyz:(y ?= z) = EqHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(y ?= x) = CompOpp LtHyz:(y ?= z) = EqHxz:(x ?= z) = GtGt = Ltrewrite (compare_trans Hxy Hxz) in Hyz; discriminate. Qed.x, y, z:O.tHxy:(y ?= x) = GtHyz:(y ?= z) = EqHxz:(x ?= z) = GtGt = Ltforall x y z : O.t, eq x y -> lt y z -> lt x zforall x y z : O.t, eq x y -> lt y z -> lt x zx, y, z:O.tHxy:(x ?= y) = EqHyz:(y ?= z) = Lt(x ?= z) = Ltx, y, z:O.tHxy:(x ?= y) = EqHyz:(y ?= z) = LtHxz:(x ?= z) = EqEq = Ltx, y, z:O.tHxy:(x ?= y) = EqHyz:(y ?= z) = LtHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(y ?= x) = CompOpp EqHyz:(y ?= z) = LtHxz:(x ?= z) = EqEq = Ltx, y, z:O.tHxy:(x ?= y) = EqHyz:(y ?= z) = LtHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(y ?= x) = EqHyz:(y ?= z) = LtHxz:(x ?= z) = EqEq = Ltx, y, z:O.tHxy:(x ?= y) = EqHyz:(y ?= z) = LtHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(x ?= y) = EqHyz:(y ?= z) = LtHxz:(x ?= z) = GtGt = Ltx, y, z:O.tHxy:(x ?= y) = EqHyz:(z ?= y) = CompOpp LtHxz:(x ?= z) = GtGt = Ltrewrite (compare_trans Hxz Hyz) in Hxy; discriminate. Qed.x, y, z:O.tHxy:(x ?= y) = EqHyz:(z ?= y) = GtHxz:(x ?= z) = GtGt = LtProper (eq ==> eq ==> iff) ltProper (eq ==> eq ==> iff) ltProper (eq ==> eq ==> impl) ltx, y:O.tH:eq x yx0, y0:O.tH0:eq x0 y0H1:lt x x0(y ?= y0) = Ltx, y:O.tH:eq x yx0, y0:O.tH0:eq x0 y0H1:lt x x0lt y x0symmetry; auto. Qed. Definition compare := O.compare.x, y:O.tH:eq x yx0, y0:O.tH0:eq x0 y0H1:lt x x0eq y xforall 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.tCompSpec (fun x0 y0 : O.t => (x0 ?= y0) = Eq) (fun x0 y0 : O.t => (x0 ?= y0) = Lt) x y (x ?= y)x, y:O.tH:(x ?= y) = GtCompSpec (fun x0 y0 : O.t => (x0 ?= y0) = Eq) (fun x0 y0 : O.t => (x0 ?= y0) = Lt) x y Gtrewrite compare_sym, H; auto. Qed.x, y:O.tH:(x ?= y) = Gt(y ?= x) = Ltforall x y : O.t, {eq x y} + {~ eq x y}forall x y : O.t, {eq x y} + {~ eq x y}case (x ?= y); [ left | right | right ]; auto; discriminate. Defined. End OT_from_Alt.x, y:O.t{(x ?= y) = Eq} + {(x ?= y) <> Eq}
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.tO.compare y x = CompOpp (O.compare x y)x, y:O.tU:eq x yV:lt y xLt = CompOpp Eqx, y:O.tU:eq x yV:lt x yGt = CompOpp Eqx, y:O.tU:lt x yV:eq y xEq = CompOpp Ltx, y:O.tU:lt x yV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:eq x yV:lt y yLt = CompOpp Eqx, y:O.tU:eq x yV:lt x yGt = CompOpp Eqx, y:O.tU:lt x yV:eq y xEq = CompOpp Ltx, y:O.tU:lt x yV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:eq x yV:lt x yGt = CompOpp Eqx, y:O.tU:lt x yV:eq y xEq = CompOpp Ltx, y:O.tU:lt x yV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:eq x yV:lt y yGt = CompOpp Eqx, y:O.tU:lt x yV:eq y xEq = CompOpp Ltx, y:O.tU:lt x yV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:lt x yV:eq y xEq = CompOpp Ltx, y:O.tU:lt x yV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:lt x xV:eq y xEq = CompOpp Ltx, y:O.tU:lt x yV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:lt x yV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:lt x xV:lt y xLt = CompOpp Ltx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:lt y xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:lt x xV:eq y xEq = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtx, y:O.tU:lt y xV:lt x yGt = CompOpp Gtelim (StrictOrder_Irreflexive y); auto. Qed.x, y:O.tU:lt y yV:lt x yGt = CompOpp Gtforall x y : O.t, (x ?= y) = Eq <-> eq x yforall x y : O.t, (x ?= y) = Eq <-> eq x yforall x y : O.t, O.compare x y = Eq <-> eq x yx, y:O.tH:lt x yH0:eq x yLt = Eqx, y:O.tH:lt y xH0:eq x yGt = Eqx, y:O.tH:lt y yH0:eq x yLt = Eqx, y:O.tH:lt y xH0:eq x yGt = Eqx, y:O.tH:lt y xH0:eq x yGt = Eqelim (StrictOrder_Irreflexive y); auto. Qed.x, y:O.tH:lt y yH0:eq x yGt = Eqforall x y : O.t, (x ?= y) = Lt <-> lt x yforall x y : O.t, (x ?= y) = Lt <-> lt x yforall x y : O.t, O.compare x y = Lt <-> lt x yx, y:O.tH:eq x yH0:lt x yEq = Ltx, y:O.tH:lt y xH0:lt x yGt = Ltx, y:O.tH:eq x yH0:lt y yEq = Ltx, y:O.tH:lt y xH0:lt x yGt = Ltx, y:O.tH:lt y xH0:lt x yGt = Ltelim (StrictOrder_Irreflexive x); auto. Qed.x, y:O.tH:lt y xH0:lt x xGt = Ltforall x y : O.t, (x ?= y) = Gt <-> lt y xforall x y : O.t, (x ?= y) = Gt <-> lt y xx, y:O.t(x ?= y) = Gt <-> lt y xapply compare_Lt. Qed.x, y:O.t(y ?= x) = CompOpp Gt <-> lt y xforall (c : comparison) (x y z : O.t), (x ?= y) = c -> (y ?= z) = c -> (x ?= z) = cforall (c : comparison) (x y z : O.t), (x ?= y) = c -> (y ?= z) = c -> (x ?= z) = cdestruct c; unfold compare; rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt; transitivity y; auto. Qed. End OT_to_Alt.c:comparisonx, y, z:O.t(x ?= y) = c -> (y ?= z) = c -> (x ?= z) = c