← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Sets/Finite_sets.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/Sets/Finite_sets.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
(****************************************************************************)
 
9
(*                                                                          *)
 
10
(*                         Naive Set Theory in Coq                          *)
 
11
(*                                                                          *)
 
12
(*                     INRIA                        INRIA                   *)
 
13
(*              Rocquencourt                        Sophia-Antipolis        *)
 
14
(*                                                                          *)
 
15
(*                                 Coq V6.1                                 *)
 
16
(*                                                                          *)
 
17
(*                               Gilles Kahn                                *)
 
18
(*                               Gerard Huet                                *)
 
19
(*                                                                          *)
 
20
(*                                                                          *)
 
21
(*                                                                          *)
 
22
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
 
23
(* to the Newton Institute for providing an exceptional work environment    *)
 
24
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 
25
(****************************************************************************)
 
26
 
 
27
(*i $Id: Finite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
28
 
 
29
Require Import Ensembles.
 
30
 
 
31
Section Ensembles_finis.
 
32
  Variable U : Type.
 
33
 
 
34
  Inductive Finite : Ensemble U -> Prop :=
 
35
    | Empty_is_finite : Finite (Empty_set U)
 
36
    | Union_is_finite :
 
37
      forall A:Ensemble U,
 
38
        Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).
 
39
 
 
40
  Inductive cardinal : Ensemble U -> nat -> Prop :=
 
41
    | card_empty : cardinal (Empty_set U) 0
 
42
    | card_add :
 
43
      forall (A:Ensemble U) (n:nat),
 
44
        cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n).
 
45
 
 
46
End Ensembles_finis.
 
47
 
 
48
Hint Resolve Empty_is_finite Union_is_finite: sets v62.
 
49
Hint Resolve card_empty card_add: sets v62.
 
50
 
 
51
Require Import Constructive_sets.
 
52
 
 
53
Section Ensembles_finis_facts.
 
54
  Variable U : Type.
 
55
  
 
56
  Lemma cardinal_invert :
 
57
    forall (X:Ensemble U) (p:nat),
 
58
      cardinal U X p ->
 
59
      match p with
 
60
        | O => X = Empty_set U
 
61
        | S n =>
 
62
          exists A : _,
 
63
            (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
 
64
      end.
 
65
  Proof.
 
66
    induction 1; simpl in |- *; auto.
 
67
    exists A; exists x; auto.
 
68
  Qed.
 
69
 
 
70
  Lemma cardinal_elim :
 
71
    forall (X:Ensemble U) (p:nat),
 
72
      cardinal U X p ->
 
73
      match p with
 
74
        | O => X = Empty_set U
 
75
        | S n => Inhabited U X
 
76
      end.
 
77
  Proof.
 
78
    intros X p C; elim C; simpl in |- *; trivial with sets.
 
79
  Qed.
 
80
 
 
81
End Ensembles_finis_facts.