diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/Equalities.v | 56 | ||||
| -rw-r--r-- | theories/Structures/Orders.v | 105 | ||||
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 322 |
3 files changed, 386 insertions, 97 deletions
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 2fbdff624..933c4ea0e 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -66,10 +66,19 @@ End HasEqDec. (** Having [eq_dec] is the same as having a boolean equality plus a correctness proof. *) -Module Type HasEqBool (Import E:Eq'). +Module Type HasEqb (Import T:Typ). Parameter Inline eqb : t -> t -> bool. - Parameter eqb_eq : forall x y, eqb x y = true <-> x==y. -End HasEqBool. +End HasEqb. + +Module Type EqbSpec (T:Typ)(X:HasEq T)(Y:HasEqb T). + Parameter eqb_eq : forall x y, Y.eqb x y = true <-> X.eq x y. +End EqbSpec. + +Module Type EqbNotation (T:Typ)(E:HasEqb T). + Infix "=?" := E.eqb (at level 70, no associativity). +End EqbNotation. + +Module Type HasEqBool (E:Eq) := HasEqb E <+ EqbSpec E E. (** From these basic blocks, we can build many combinations of static standalone module types. *) @@ -107,8 +116,10 @@ Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation. Module Type DecidableType' := DecidableType <+ EqNotation. Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation. Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation. -Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation. -Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation. +Module Type BooleanEqualityType' := + BooleanEqualityType <+ EqNotation <+ EqbNotation. +Module Type BooleanDecidableType' := + BooleanDecidableType <+ EqNotation <+ EqbNotation. Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation. (** * Compatibility wrapper from/to the old version of @@ -166,9 +177,12 @@ Module Dec2Bool (E:DecidableType) <: BooleanDecidableType Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType := E <+ HasEqBool2Dec. -(** In a BooleanEqualityType, [eqb] is compatible with [eq] *) -Module BoolEqualityFacts (Import E : BooleanEqualityType). +(** Some properties of boolean equality *) + +Module BoolEqualityFacts (Import E : BooleanEqualityType'). + +(** [eqb] is compatible with [eq] *) Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb. Proof. @@ -177,6 +191,34 @@ apply eq_true_iff_eq. now rewrite 2 eqb_eq, Exx', Eyy'. Qed. +(** Alternative specification of [eqb] based on [reflect]. *) + +Lemma eqb_spec x y : reflect (x==y) (x =? y). +Proof. +apply iff_reflect. symmetry. apply eqb_eq. +Qed. + +(** Negated form of [eqb_eq] *) + +Lemma eqb_neq x y : (x =? y) = false <-> x ~= y. +Proof. +now rewrite <- not_true_iff_false, eqb_eq. +Qed. + +(** Basic equality laws for [eqb] *) + +Lemma eqb_refl x : (x =? x) = true. +Proof. +now apply eqb_eq. +Qed. + +Lemma eqb_sym x y : (x =? y) = (y =? x). +Proof. +apply eq_true_iff_eq. now rewrite 2 eqb_eq. +Qed. + +(** Transitivity is a particular case of [eqb_compat] *) + End BoolEqualityFacts. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 99dfb19d5..1d0254397 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -65,20 +65,34 @@ Module Type LeIsLtEq (Import E:EqLtLe'). Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y. End LeIsLtEq. -Module Type HasCompare (Import E:EqLt'). +Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder. +Module Type StrOrder' := StrOrder <+ EqLtNotation. + +(** Versions with a decidable ternary comparison *) + +Module Type HasCmp (Import T:Typ). Parameter Inline compare : t -> t -> comparison. +End HasCmp. + +Module Type CmpNotation (T:Typ)(C:HasCmp T). + Infix "?=" := C.compare (at level 70, no associativity). +End CmpNotation. + +Module Type CmpSpec (Import E:EqLt')(Import C:HasCmp E). Axiom compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y). -End HasCompare. +End CmpSpec. + +Module Type HasCompare (E:EqLt) := HasCmp E <+ CmpSpec E. -Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder. Module Type DecStrOrder := StrOrder <+ HasCompare. +Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation <+ CmpNotation. + Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec. -Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq. +Module Type OrderedType' := OrderedType <+ EqLtNotation <+ CmpNotation. -Module Type StrOrder' := StrOrder <+ EqLtNotation. -Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation. -Module Type OrderedType' := OrderedType <+ EqLtNotation. -Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation. +Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq. +Module Type OrderedTypeFull' := + OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation. (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare]. But adding this redundant field allows to see an [OrderedType] as a @@ -167,50 +181,63 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder Local Coercion is_true : bool >-> Sortclass. Hint Unfold is_true. -Module Type HasLeBool (Import T:Typ). - Parameter Inline leb : t -> t -> bool. -End HasLeBool. - -Module Type HasLtBool (Import T:Typ). - Parameter Inline ltb : t -> t -> bool. -End HasLtBool. +Module Type HasLeb (Import T:Typ). + Parameter Inline leb : t -> t -> bool. +End HasLeb. -Module Type LeBool := Typ <+ HasLeBool. -Module Type LtBool := Typ <+ HasLtBool. +Module Type HasLtb (Import T:Typ). + Parameter Inline ltb : t -> t -> bool. +End HasLtb. -Module Type LeBoolNotation (E:LeBool). - Infix "<=?" := E.leb (at level 35). -End LeBoolNotation. +Module Type LebNotation (T:Typ)(E:HasLeb T). + Infix "<=?" := E.leb (at level 35). +End LebNotation. -Module Type LtBoolNotation (E:LtBool). - Infix "<?" := E.ltb (at level 35). -End LtBoolNotation. +Module Type LtbNotation (T:Typ)(E:HasLtb T). + Infix "<?" := E.ltb (at level 35). +End LtbNotation. -Module Type LeBool' := LeBool <+ LeBoolNotation. -Module Type LtBool' := LtBool <+ LtBoolNotation. +Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T). + Parameter leb_le : forall x y, Y.leb x y = true <-> X.le x y. +End LebSpec. -Module Type LeBool_Le (T:Typ)(X:HasLeBool T)(Y:HasLe T). - Parameter leb_le : forall x y, X.leb x y = true <-> Y.le x y. -End LeBool_Le. +Module Type LtbSpec (T:Typ)(X:HasLt T)(Y:HasLtb T). + Parameter ltb_lt : forall x y, Y.ltb x y = true <-> X.lt x y. +End LtbSpec. -Module Type LtBool_Lt (T:Typ)(X:HasLtBool T)(Y:HasLt T). - Parameter ltb_lt : forall x y, X.ltb x y = true <-> Y.lt x y. -End LtBool_Lt. +Module Type LeBool := Typ <+ HasLeb. +Module Type LtBool := Typ <+ HasLtb. +Module Type LeBool' := LeBool <+ LebNotation. +Module Type LtBool' := LtBool <+ LtbNotation. -Module Type LeBoolIsTotal (Import X:LeBool'). +Module Type LebIsTotal (Import X:LeBool'). Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true. -End LeBoolIsTotal. +End LebIsTotal. -Module Type TotalLeBool := LeBool <+ LeBoolIsTotal. -Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal. +Module Type TotalLeBool := LeBool <+ LebIsTotal. +Module Type TotalLeBool' := LeBool' <+ LebIsTotal. -Module Type LeBoolIsTransitive (Import X:LeBool'). +Module Type LebIsTransitive (Import X:LeBool'). Axiom leb_trans : Transitive X.leb. -End LeBoolIsTransitive. +End LebIsTransitive. + +Module Type TotalTransitiveLeBool := TotalLeBool <+ LebIsTransitive. +Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LebIsTransitive. + +(** Grouping all boolean comparison functions *) + +Module Type HasBoolOrdFuns (T:Typ) := HasEqb T <+ HasLtb T <+ HasLeb T. + +Module Type HasBoolOrdFuns' (T:Typ) := + HasBoolOrdFuns T <+ EqbNotation T <+ LtbNotation T <+ LebNotation T. -Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive. -Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive. +Module Type BoolOrdSpecs (O:EqLtLe)(F:HasBoolOrdFuns O) := + EqbSpec O O F <+ LtbSpec O O F <+ LebSpec O O F. +Module Type OrderFunctions (E:EqLtLe) := + HasCompare E <+ HasBoolOrdFuns E <+ BoolOrdSpecs E. +Module Type OrderFunctions' (E:EqLtLe) := + HasCompare E <+ CmpNotation E <+ HasBoolOrdFuns' E <+ BoolOrdSpecs E. (** * From [OrderedTypeFull] to [TotalTransitiveLeBool] *) diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index b328ae2e8..a447e8fb5 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -6,15 +6,76 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Import Basics OrdersTac. +Require Import Bool Basics OrdersTac. Require Export Orders. Set Implicit Arguments. Unset Strict Implicit. -(** * Properties of [OrderedTypeFull] *) +(** * Properties of [compare] *) -Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). +Module Type CompareFacts (Import O:DecStrOrder'). + + Local Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_eq_iff x y : (x ?= y) = Eq <-> x==y. + Proof. + case compare_spec; intro H; split; try easy; intro EQ; + contradict H; rewrite EQ; apply irreflexivity. + Qed. + + Lemma compare_eq x y : (x ?= y) = Eq -> x==y. + Proof. + apply compare_eq_iff. + Qed. + + Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y. + Proof. + case compare_spec; intro H; split; try easy; intro LT; + contradict LT; rewrite H; apply irreflexivity. + Qed. + + Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x. + Proof. + case compare_spec; intro H; split; try easy; intro LT; + contradict LT; rewrite H; apply irreflexivity. + Qed. + + Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y). + Proof. + rewrite compare_lt_iff; intuition. + Qed. + + Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x). + Proof. + rewrite compare_gt_iff; intuition. + Qed. + + Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. + + Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. + Proof. + intros x x' Hxx' y y' Hyy'. + case (compare_spec x' y'); autorewrite with order; now rewrite Hxx', Hyy'. + Qed. + + Lemma compare_refl x : (x ?= x) = Eq. + Proof. + case compare_spec; intros; trivial; now elim irreflexivity with x. + Qed. + + Lemma compare_antisym x y : (y ?= x) = CompOpp (x ?= y). + Proof. + case (compare_spec x y); simpl; autorewrite with order; + trivial; now symmetry. + Qed. + +End CompareFacts. + + + (** * Properties of [OrderedTypeFull] *) + +Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). Module OrderTac := OTF_to_OrderTac O. Ltac order := OrderTac.order. @@ -47,6 +108,18 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x. Proof. iorder. Qed. + Include CompareFacts O. + + Lemma compare_le_iff x y : compare x y <> Gt <-> x<=y. + Proof. + rewrite le_not_gt_iff. apply compare_ngt_iff. + Qed. + + Lemma compare_ge_iff x y : compare x y <> Lt <-> y<=x. + Proof. + rewrite le_not_gt_iff. apply compare_nlt_iff. + Qed. + End OrderedTypeFullFacts. @@ -84,50 +157,9 @@ Module OrderedTypeFacts (Import O: OrderedType'). Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x. - (** Some more about [compare] *) - - Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x. - Proof. - intros; elim_compare x y; intuition; try discriminate; order. - Qed. - - Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x. - Proof. - intros; rewrite compare_lt_iff; intuition. - Qed. - - Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y. - Proof. - intros; rewrite compare_gt_iff; intuition. - Qed. - - Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. - - Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. - Proof. - intros x x' Hxx' y y' Hyy'. - elim_compare x' y'; autorewrite with order; order. - Qed. - - Lemma compare_refl : forall x, (x ?= x) = Eq. - Proof. - intros; elim_compare x x; auto; order. - Qed. - - Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y). - Proof. - intros; elim_compare x y; simpl; autorewrite with order; order. - Qed. + Include CompareFacts O. + Notation compare_le_iff := compare_ngt_iff (only parsing). + Notation compare_ge_iff := compare_nlt_iff (only parsing). (** For compatibility reasons *) Definition eq_dec := eq_dec. @@ -162,10 +194,6 @@ Module OrderedTypeFacts (Import O: OrderedType'). End OrderedTypeFacts. - - - - (** * Tests of the order tactic Is it at least capable of proving some basic properties ? *) @@ -232,3 +260,195 @@ Qed. End OrderedTypeRev. +Unset Implicit Arguments. + +(** * Order relations derived from a [compare] function. + + We factorize here some common properties for ZArith, NArith + and co, where [lt] and [le] are defined in terms of [compare]. + Note that we do not require anything here concerning compatibility + of [compare] w.r.t [eq], nor anything concerning transitivity. +*) + +Module Type CompareBasedOrder (Import E:EqLtLe')(Import C:HasCmp E). + Include CmpNotation E C. + Include IsEq E. + Axiom compare_eq_iff : forall x y, (x ?= y) = Eq <-> x == y. + Axiom compare_lt_iff : forall x y, (x ?= y) = Lt <-> x < y. + Axiom compare_le_iff : forall x y, (x ?= y) <> Gt <-> x <= y. + Axiom compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y). +End CompareBasedOrder. + +Module Type CompareBasedOrderFacts + (Import E:EqLtLe') + (Import C:HasCmp E) + (Import O:CompareBasedOrder E C). + + Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y). + Proof. + case_eq (compare x y); intros H; constructor. + now apply compare_eq_iff. + now apply compare_lt_iff. + rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff. + Qed. + + Lemma compare_eq x y : (x ?= y) = Eq -> x==y. + Proof. + apply compare_eq_iff. + Qed. + + Lemma compare_refl x : (x ?= x) = Eq. + Proof. + now apply compare_eq_iff. + Qed. + + Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x. + Proof. + now rewrite <- compare_lt_iff, compare_antisym, CompOpp_iff. + Qed. + + Lemma compare_ge_iff x y : (x ?= y) <> Lt <-> y<=x. + Proof. + now rewrite <- compare_le_iff, compare_antisym, CompOpp_iff. + Qed. + + Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x). + Proof. + rewrite compare_gt_iff; intuition. + Qed. + + Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y). + Proof. + rewrite compare_lt_iff; intuition. + Qed. + + Lemma compare_nle_iff x y : (x ?= y) = Gt <-> ~(x<=y). + Proof. + rewrite <- compare_le_iff. + destruct compare; split; easy || now destruct 1. + Qed. + + Lemma compare_nge_iff x y : (x ?= y) = Lt <-> ~(y<=x). + Proof. + now rewrite <- compare_nle_iff, compare_antisym, CompOpp_iff. + Qed. + + Lemma lt_irrefl x : ~ (x<x). + Proof. + now rewrite <- compare_lt_iff, compare_refl. + Qed. + + Lemma lt_eq_cases n m : n <= m <-> n < m \/ n==m. + Proof. + rewrite <- compare_lt_iff, <- compare_le_iff, <- compare_eq_iff. + destruct (n ?= m); now intuition. + Qed. + +End CompareBasedOrderFacts. + +(** Basic facts about boolean comparisons *) + +Module Type BoolOrderFacts + (Import E:EqLtLe') + (Import C:HasCmp E) + (Import F:HasBoolOrdFuns' E) + (Import O:CompareBasedOrder E C) + (Import S:BoolOrdSpecs E F). + +Include CompareBasedOrderFacts E C O. + +(** Nota : apart from [eqb_compare] below, facts about [eqb] + are in BoolEqualityFacts *) + +(** Alternate specifications based on [BoolSpec] and [reflect] *) + +Lemma leb_spec0 x y : reflect (x<=y) (x<=?y). +Proof. + apply iff_reflect. symmetry. apply leb_le. +Qed. + +Lemma leb_spec x y : BoolSpec (x<=y) (y<x) (x<=?y). +Proof. + case leb_spec0; constructor; trivial. + now rewrite <- compare_lt_iff, compare_nge_iff. +Qed. + +Lemma ltb_spec0 x y : reflect (x<y) (x<?y). +Proof. + apply iff_reflect. symmetry. apply ltb_lt. +Qed. + +Lemma ltb_spec x y : BoolSpec (x<y) (y<=x) (x<?y). +Proof. + case ltb_spec0; constructor; trivial. + now rewrite <- compare_le_iff, compare_ngt_iff. +Qed. + +(** Negated variants of the specifications *) + +Lemma leb_nle x y : x <=? y = false <-> ~ (x <= y). +Proof. +now rewrite <- not_true_iff_false, leb_le. +Qed. + +Lemma leb_gt x y : x <=? y = false <-> y < x. +Proof. +now rewrite leb_nle, <- compare_lt_iff, compare_nge_iff. +Qed. + +Lemma ltb_nlt x y : x <? y = false <-> ~ (x < y). +Proof. +now rewrite <- not_true_iff_false, ltb_lt. +Qed. + +Lemma ltb_ge x y : x <? y = false <-> y <= x. +Proof. +now rewrite ltb_nlt, <- compare_le_iff, compare_ngt_iff. +Qed. + +(** Basic equality laws for boolean tests *) + +Lemma leb_refl x : x <=? x = true. +Proof. +apply leb_le. apply lt_eq_cases. now right. +Qed. + +Lemma leb_antisym x y : y <=? x = negb (x <? y). +Proof. +apply eq_true_iff_eq. now rewrite negb_true_iff, leb_le, ltb_ge. +Qed. + +Lemma ltb_irrefl x : x <? x = false. +Proof. +apply ltb_ge. apply lt_eq_cases. now right. +Qed. + +Lemma ltb_antisym x y : y <? x = negb (x <=? y). +Proof. +apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt. +Qed. + +(** Relation bewteen [compare] and the boolean comparisons *) + +Lemma eqb_compare x y : + (x =? y) = match compare x y with Eq => true | _ => false end. +Proof. +apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff. +destruct compare; now split. +Qed. + +Lemma ltb_compare x y : + (x <? y) = match compare x y with Lt => true | _ => false end. +Proof. +apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff. +destruct compare; now split. +Qed. + +Lemma leb_compare x y : + (x <=? y) = match compare x y with Gt => false | _ => true end. +Proof. +apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff. +destruct compare; split; try easy. now destruct 1. +Qed. + +End BoolOrderFacts. |