From b432124e904a23948f09f90846d92ef3472de041 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 26 Mar 2007 14:59:27 +0000 Subject: PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only OrderedType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9730 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/FMapPositive.v | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'theories/FSets') diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 10f6d44f3..70c221027 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -16,6 +16,7 @@ Require Import Bool. Require Import ZArith. Require Import OrderedType. +Require Import OrderedTypeEx. Require Import FMapInterface. Set Implicit Arguments. @@ -36,9 +37,12 @@ Open Scope positive_scope. usual order (see [OrderedTypeEx]), we use here a lexicographic order over bits, which is more natural here (lower bits are considered first). *) -Module PositiveOrderedTypeBits <: OrderedType. +Module PositiveOrderedTypeBits <: UsualOrderedType. Definition t:=positive. Definition eq:=@eq positive. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. Fixpoint bits_lt (p q:positive) { struct p } : Prop := match p, q with @@ -52,15 +56,6 @@ Module PositiveOrderedTypeBits <: OrderedType. Definition lt:=bits_lt. - Lemma eq_refl : forall x : t, eq x x. - Proof. red; auto. Qed. - - Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof. red; auto. Qed. - - Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof. red; intros; transitivity y; auto. Qed. - Lemma bits_lt_trans : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z. Proof. induction x. -- cgit v1.2.3