← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Logic/DecidableTypeEx.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Logic/DecidableTypeEx.v
 
1
(***********************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 
3
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
 
4
(*   \VV/  *************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the      *)
 
6
(*         *       GNU Lesser General Public License Version 2.1       *)
 
7
(***********************************************************************)
 
8
 
 
9
(* $Id: DecidableTypeEx.v 11699 2008-12-18 11:49:08Z letouzey $ *)
 
10
 
 
11
Require Import DecidableType OrderedType OrderedTypeEx.
 
12
Set Implicit Arguments.
 
13
Unset Strict Implicit.
 
14
 
 
15
(** * Examples of Decidable Type structures. *)
 
16
 
 
17
(** A particular case of [DecidableType] where 
 
18
    the equality is the usual one of Coq. *)
 
19
 
 
20
Module Type UsualDecidableType.
 
21
 Parameter Inline t : Type.
 
22
 Definition eq := @eq t.
 
23
 Definition eq_refl := @refl_equal t.
 
24
 Definition eq_sym := @sym_eq t.
 
25
 Definition eq_trans := @trans_eq t.
 
26
 Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
 
27
End UsualDecidableType.
 
28
 
 
29
(** a [UsualDecidableType] is in particular an [DecidableType]. *)
 
30
 
 
31
Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
 
32
 
 
33
(** an shortcut for easily building a UsualDecidableType *)
 
34
 
 
35
Module Type MiniDecidableType. 
 
36
 Parameter Inline t : Type.
 
37
 Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
 
38
End MiniDecidableType. 
 
39
 
 
40
Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
 
41
 Definition t:=M.t. 
 
42
 Definition eq := @eq t.
 
43
 Definition eq_refl := @refl_equal t.
 
44
 Definition eq_sym := @sym_eq t.
 
45
 Definition eq_trans := @trans_eq t.
 
46
 Definition eq_dec := M.eq_dec.
 
47
End Make_UDT.
 
48
 
 
49
(** An OrderedType can now directly be seen as a DecidableType *)
 
50
 
 
51
Module OT_as_DT (O:OrderedType) <: DecidableType := O.
 
52
 
 
53
(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *)
 
54
 
 
55
Module Nat_as_DT <: UsualDecidableType := Nat_as_OT.
 
56
Module Positive_as_DT <: UsualDecidableType := Positive_as_OT.
 
57
Module N_as_DT <: UsualDecidableType := N_as_OT.
 
58
Module Z_as_DT <: UsualDecidableType := Z_as_OT.
 
59
 
 
60
(** From two decidable types, we can build a new DecidableType 
 
61
   over their cartesian product. *)
 
62
 
 
63
Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
 
64
 
 
65
 Definition t := prod D1.t D2.t.
 
66
 
 
67
 Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y).
 
68
 
 
69
 Lemma eq_refl : forall x : t, eq x x.
 
70
 Proof. 
 
71
 intros (x1,x2); red; simpl; auto.
 
72
 Qed.
 
73
 
 
74
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
 
75
 Proof. 
 
76
 intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
 
77
 Qed.
 
78
 
 
79
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
 
80
 Proof. 
 
81
 intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto.
 
82
 Qed.
 
83
 
 
84
 Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
 
85
 Proof.
 
86
 intros (x1,x2) (y1,y2); unfold eq; simpl.
 
87
 destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition.
 
88
 Defined.
 
89
 
 
90
End PairDecidableType.
 
91
 
 
92
(** Similarly for pairs of UsualDecidableType *)
 
93
 
 
94
Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
 
95
 Definition t := prod D1.t D2.t.
 
96
 Definition eq := @eq t.
 
97
 Definition eq_refl := @refl_equal t.
 
98
 Definition eq_sym := @sym_eq t.
 
99
 Definition eq_trans := @trans_eq t.
 
100
 Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
 
101
 Proof.
 
102
 intros (x1,x2) (y1,y2); 
 
103
 destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); 
 
104
 unfold eq, D1.eq, D2.eq in *; simpl; 
 
105
 (left; f_equal; auto; fail) || 
 
106
 (right; intro H; injection H; auto).
 
107
 Defined.
 
108
 
 
109
End PairUsualDecidableType.