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.