← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/bugs/closed/shouldsucceed/1507.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:
test-suite/bugs/closed/shouldsucceed/1507.v
 
1
(*
 
2
   Implementing reals a la Stolzenberg
 
3
 
 
4
   Danko Ilik, March 2007
 
5
   svn revision: $Id: 1507.v 10068 2007-08-10 12:06:59Z notin $
 
6
 
 
7
   XField.v -- (unfinished) axiomatisation of the theories of real and
 
8
               rational intervals.
 
9
*)
 
10
 
 
11
Definition associative (A:Type)(op:A->A->A) := 
 
12
  forall x y z:A, op (op x y) z = op x (op y z).
 
13
 
 
14
Definition commutative (A:Type)(op:A->A->A) := 
 
15
  forall x y:A, op x y = op y x.
 
16
 
 
17
Definition trichotomous (A:Type)(R:A->A->Prop) :=
 
18
  forall x y:A, R x y \/ x=y \/ R y x.
 
19
 
 
20
Definition relation (A:Type) := A -> A -> Prop.
 
21
Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x.
 
22
Definition transitive (A:Type)(R:relation A) := 
 
23
  forall x y z:A, R x y -> R y z -> R x z.
 
24
Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x.
 
25
 
 
26
Record interval (X:Set)(le:X->X->Prop) : Set :=
 
27
  interval_make {
 
28
    interval_left : X;
 
29
    interval_right : X;
 
30
    interval_nonempty : le interval_left interval_right
 
31
  }.
 
32
 
 
33
Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
 
34
  Icar    := interval grnd le;
 
35
  Iplus   : Icar -> Icar -> Icar;
 
36
  Imult   : Icar -> Icar -> Icar;
 
37
  Izero   : Icar;
 
38
  Ione    : Icar;
 
39
  Iopp    : Icar -> Icar;
 
40
  Iinv    : Icar -> Icar;
 
41
  Ic      : Icar -> Icar -> Prop; (* consistency *)
 
42
  (* monoids *)
 
43
  Iplus_assoc    : associative Icar Iplus;
 
44
  Imult_assoc    : associative Icar Imult;
 
45
  (* abelian groups *)
 
46
  Iplus_comm     : commutative Icar Iplus;
 
47
  Imult_comm     : commutative Icar Imult;
 
48
  Iplus_0_l      : forall x:Icar, Ic (Iplus Izero x) x;
 
49
  Iplus_0_r      : forall x:Icar, Ic (Iplus x Izero) x;
 
50
  Imult_0_l      : forall x:Icar, Ic (Imult Ione x) x;
 
51
  Imult_0_r      : forall x:Icar, Ic (Imult x Ione) x;
 
52
  Iplus_opp_r    : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero);
 
53
  Imult_inv_r    : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione;
 
54
  (* distributive laws *)
 
55
  Imult_plus_distr_l : forall x x' y y' z z' z'', 
 
56
    Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' ->
 
57
    Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z''));
 
58
  (* order and lattice structure *)
 
59
  Ilt          : Icar -> Icar -> Prop;
 
60
  Ilc          := fun (x y:Icar) => Ilt x y \/ Ic x y;
 
61
  Isup         : Icar -> Icar -> Icar;
 
62
  Iinf         : Icar -> Icar -> Icar;
 
63
  Ilt_trans    : transitive _ lt;
 
64
  Ilt_trich    : forall x y:Icar, Ilt x y \/ Ic x y \/ Ilt y x;
 
65
  Isup_lub     : forall x y z:Icar, Ilc x z -> Ilc y z -> Ilc (Isup x y) z;
 
66
  Iinf_glb     : forall x y z:Icar, Ilc x y -> Ilc x z -> Ilc x (Iinf y z);
 
67
  (* order preserves operations? *)
 
68
  (* properties of Ic *)
 
69
  Ic_refl   : reflexive _ Ic;
 
70
  Ic_sym    : symmetric _ Ic
 
71
}.
 
72
 
 
73
Definition interval_set (X:Set)(le:X->X->Prop) := 
 
74
  (interval X le) -> Prop. (* can be Set as well *)
 
75
Check interval_set.
 
76
Check Ic.
 
77
Definition consistent (X:Set)(le:X->X->Prop)(TI:I X le)(p:interval_set X le) :=
 
78
  forall I J:interval X le, p I -> p J -> (Ic X le TI) I J.
 
79
Check consistent.
 
80
(* define 'fine' *)
 
81
 
 
82
Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake {
 
83
  Ncar    := interval_set grnd le;
 
84
  Nplus   : Ncar -> Ncar -> Ncar;
 
85
  Nmult   : Ncar -> Ncar -> Ncar;
 
86
  Nzero   : Ncar;
 
87
  None    : Ncar;
 
88
  Nopp    : Ncar -> Ncar;
 
89
  Ninv    : Ncar -> Ncar;
 
90
  Nc      : Ncar -> Ncar -> Prop; (* Ncistency *)
 
91
  (* monoids *)
 
92
  Nplus_assoc    : associative Ncar Nplus;
 
93
  Nmult_assoc    : associative Ncar Nmult;
 
94
  (* abelian groups *)
 
95
  Nplus_comm     : commutative Ncar Nplus;
 
96
  Nmult_comm     : commutative Ncar Nmult;
 
97
  Nplus_0_l      : forall x:Ncar, Nc (Nplus Nzero x) x;
 
98
  Nplus_0_r      : forall x:Ncar, Nc (Nplus x Nzero) x;
 
99
  Nmult_0_l      : forall x:Ncar, Nc (Nmult None x) x;
 
100
  Nmult_0_r      : forall x:Ncar, Nc (Nmult x None) x;
 
101
  Nplus_opp_r    : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero);
 
102
  Nmult_inv_r    : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None;
 
103
  (* distributive laws *)
 
104
  Nmult_plus_distr_l : forall x x' y y' z z' z'', 
 
105
    Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' ->
 
106
    Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z''));
 
107
  (* order and lattice structure *)
 
108
  Nlt          : Ncar -> Ncar -> Prop;
 
109
  Nlc          := fun (x y:Ncar) => Nlt x y \/ Nc x y;
 
110
  Nsup         : Ncar -> Ncar -> Ncar;
 
111
  Ninf         : Ncar -> Ncar -> Ncar;
 
112
  Nlt_trans    : transitive _ lt;
 
113
  Nlt_trich    : forall x y:Ncar, Nlt x y \/ Nc x y \/ Nlt y x;
 
114
  Nsup_lub     : forall x y z:Ncar, Nlc x z -> Nlc y z -> Nlc (Nsup x y) z;
 
115
  Ninf_glb     : forall x y z:Ncar, Nlc x y -> Nlc x z -> Nlc x (Ninf y z);
 
116
  (* order preserves operations? *)
 
117
  (* properties of Nc *)
 
118
  Nc_refl   : reflexive _ Nc;
 
119
  Nc_sym    : symmetric _ Nc
 
120
}.
 
121