diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-13 14:39:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-13 14:39:51 +0000 |
commit | aa49d0523c769de01bc66f0f2b9e663ff0731cd6 (patch) | |
tree | 77a7c3f3837275d62a50e750dfb24ad6dd8d19cd /theories/Structures/DecidableTypeEx.v | |
parent | 562c684cd19c37e04901743c73933ea12148940b (diff) |
MSets: a new generation of FSets
Same global ideas (in particular the use of modules/functors), but:
- frequent use of Type Classes inside interfaces/implementation.
For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence.
A class StrictOrder for lt in OrderedType. Extensive use of Proper
and rewrite.
- now that rewrite is mature, we write specifications of set operators
via iff instead of many separate requirements based on ->. For instance
add_spec : In y (add x s) <-> E.eq y x \/ In x s.
Old-style specs are available in the functor Facts.
- compare is now a pure function (t -> t -> comparison) instead of
returning a dependent type Compare.
- The "Raw" functors (the ones dealing with e.g. list with no
sortedness proofs yet, but morally sorted when operating on them)
are given proper interfaces and a generic functor allows to obtain
a regular set implementation out of a "raw" one.
The last two points allow to manipulate set objects that are completely free
of proof-parts if one wants to. Later proofs will rely on type-classes
instance search mechanism.
No need to emphasis the fact that this new version is severely incompatible
with the earlier one. I've no precise ideas yet on how allowing an easy
transition (functors ?). For the moment, these new Sets are placed alongside
the old ones, in directory MSets (M for Modular, to constrast with forthcoming
CSets, see below). A few files exist currently in version foo.v and foo2.v,
I'll try to merge them without breaking things. Old FSets will probably move
to a contrib later.
Still to be done:
- adapt FMap in the same way
- integrate misc stuff like multisets or the map function
- CSets, i.e. Sets based on Type Classes : Integration of code contributed by
S. Lescuyer is on the way.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures/DecidableTypeEx.v')
-rw-r--r-- | theories/Structures/DecidableTypeEx.v | 109 |
1 files changed, 109 insertions, 0 deletions
diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v new file mode 100644 index 000000000..022102f70 --- /dev/null +++ b/theories/Structures/DecidableTypeEx.v @@ -0,0 +1,109 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +Require Import DecidableType OrderedType OrderedTypeEx. +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Examples of Decidable Type structures. *) + +(** A particular case of [DecidableType] where + the equality is the usual one of Coq. *) + +Module Type UsualDecidableType. + Parameter Inline t : Type. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Parameter eq_dec : forall x y, { eq x y }+{~eq x y }. +End UsualDecidableType. + +(** a [UsualDecidableType] is in particular an [DecidableType]. *) + +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 now directly be seen as a DecidableType *) + +Module OT_as_DT (O:OrderedType) <: DecidableType := O. + +(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) + +Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. +Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. +Module N_as_DT <: UsualDecidableType := N_as_OT. +Module Z_as_DT <: UsualDecidableType := 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) <: UsualDecidableType. + 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. |