diff options
Diffstat (limited to 'theories/Logic/DecidableTypeEx.v')
-rw-r--r-- | theories/Logic/DecidableTypeEx.v | 71 |
1 files changed, 69 insertions, 2 deletions
diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v index a4f99de2..9c928598 100644 --- a/theories/Logic/DecidableTypeEx.v +++ b/theories/Logic/DecidableTypeEx.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableTypeEx.v 8933 2006-06-09 14:08:38Z herbelin $ *) +(* $Id: DecidableTypeEx.v 10739 2008-04-01 14:45:20Z herbelin $ *) Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. @@ -18,7 +18,7 @@ Unset Strict Implicit. the equality is the usual one of Coq. *) Module Type UsualDecidableType. - Parameter t : Set. + Parameter Inline t : Type. Definition eq := @eq t. Definition eq_refl := @refl_equal t. Definition eq_sym := @sym_eq t. @@ -30,6 +30,22 @@ End UsualDecidableType. Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. +(** an shortcut for easily building a UsualDecidableType *) + +Module Type MiniDecidableType. + Parameter Inline t : Type. + Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. +End MiniDecidableType. + +Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. + Definition t:=M.t. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Definition eq_dec := M.eq_dec. +End Make_UDT. + (** An OrderedType can be seen as a DecidableType *) Module OT_as_DT (O:OrderedType) <: DecidableType. @@ -48,3 +64,54 @@ Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT). Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT). Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT). Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT). + +(** From two decidable types, we can build a new DecidableType + over their cartesian product. *) + +Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. + + Definition t := prod D1.t D2.t. + + Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y). + + Lemma eq_refl : forall x : t, eq x x. + Proof. + intros (x1,x2); red; simpl; auto. + Qed. + + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof. + intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. + Qed. + + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. + Qed. + + Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. + Proof. + intros (x1,x2) (y1,y2); unfold eq; simpl. + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition. + Defined. + +End PairDecidableType. + +(** Similarly for pairs of UsualDecidableType *) + +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: DecidableType. + Definition t := prod D1.t D2.t. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. + Proof. + intros (x1,x2) (y1,y2); + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); + unfold eq, D1.eq, D2.eq in *; simpl; + (left; f_equal; auto; fail) || + (right; intro H; injection H; auto). + Defined. + +End PairUsualDecidableType. |