← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/modules/Przyklad.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/modules/Przyklad.v
 
1
Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) 
 
2
  (th el : T) := if s then th else el.
 
3
 
 
4
Implicit Arguments ifte.
 
5
 
 
6
Lemma Reflexivity_provable :
 
7
 forall (A : Set) (a : A) (s : {a = a} + {a <> a}),
 
8
 exists x : _, s = left _ x.
 
9
intros.
 
10
elim s.
 
11
intro x.
 
12
split with x; reflexivity.
 
13
 
 
14
intro.
 
15
 absurd (a = a); auto.
 
16
 
 
17
Qed.
 
18
 
 
19
Lemma Disequality_provable :
 
20
 forall (A : Set) (a b : A),
 
21
 a <> b -> forall s : {a = b} + {a <> b}, exists x : _, s = right _ x.
 
22
intros.
 
23
elim s.
 
24
intro.
 
25
 absurd (a = a); auto.
 
26
 
 
27
intro.
 
28
split with b0; reflexivity.
 
29
 
 
30
Qed.
 
31
 
 
32
Module Type ELEM.
 
33
  Parameter T : Set.
 
34
  Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}.
 
35
End ELEM.
 
36
                                        
 
37
Module Type SET (Elt: ELEM).
 
38
  Parameter T : Set.
 
39
  Parameter empty : T.
 
40
  Parameter add : Elt.T -> T -> T.
 
41
  Parameter find : Elt.T -> T -> bool.
 
42
 
 
43
  (* Axioms *)
 
44
 
 
45
  Axiom find_empty_false : forall e : Elt.T, find e empty = false.
 
46
 
 
47
  Axiom find_add_true : forall (s : T) (e : Elt.T), find e (add e s) = true.
 
48
 
 
49
  Axiom
 
50
    find_add_false :
 
51
      forall (s : T) (e e' : Elt.T), e <> e' -> find e (add e' s) = find e s.
 
52
 
 
53
End SET.
 
54
 
 
55
Module FuncDict (E: ELEM).
 
56
  Definition T := E.T -> bool.
 
57
  Definition empty (e' : E.T) := false.
 
58
  Definition find (e' : E.T) (s : T) := s e'.
 
59
  Definition add (e : E.T) (s : T) (e' : E.T) :=
 
60
    ifte (E.eq_dec e e') true (find e' s).
 
61
 
 
62
  Lemma find_empty_false : forall e : E.T, find e empty = false.
 
63
    auto.
 
64
  Qed.
 
65
 
 
66
  Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
 
67
 
 
68
    intros.
 
69
    unfold find, add in |- *.
 
70
    elim (Reflexivity_provable _ _ (E.eq_dec e e)).
 
71
    intros.
 
72
     rewrite H.
 
73
    auto.
 
74
 
 
75
  Qed.
 
76
 
 
77
  Lemma find_add_false :
 
78
   forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
 
79
    intros.
 
80
    unfold add, find in |- *.
 
81
    cut (exists x : _, E.eq_dec e' e = right _ x).
 
82
    intros.
 
83
    elim H0.
 
84
    intros.
 
85
     rewrite H1.
 
86
    unfold ifte in |- *.
 
87
    reflexivity.
 
88
 
 
89
    apply Disequality_provable.
 
90
    auto.
 
91
 
 
92
  Qed.
 
93
 
 
94
End FuncDict.
 
95
 
 
96
Module F : SET := FuncDict.
 
97
 
 
98
 
 
99
Module Nat.
 
100
  Definition T := nat.
 
101
  Lemma eq_dec : forall a a' : T, {a = a'} + {a <> a'}.
 
102
     decide equality.
 
103
  Qed.
 
104
End Nat.
 
105
 
 
106
 
 
107
Module SetNat := F Nat. 
 
108
 
 
109
 
 
110
Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. 
 
111
apply SetNat.find_empty_false. 
 
112
Qed.
 
113
 
 
114
(***************************************************************************)
 
115
Module Lemmas (G: SET) (E: ELEM).
 
116
 
 
117
  Module ESet := G E.
 
118
 
 
119
  Lemma commute :
 
120
   forall (S : ESet.T) (a1 a2 : E.T),
 
121
   let S1 := ESet.add a1 (ESet.add a2 S) in
 
122
   let S2 := ESet.add a2 (ESet.add a1 S) in
 
123
   forall a : E.T, ESet.find a S1 = ESet.find a S2. 
 
124
  
 
125
    intros.
 
126
    unfold S1, S2 in |- *.
 
127
    elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2;
 
128
     try  rewrite <- H1; try  rewrite <- H2;
 
129
     repeat
 
130
      (try ( rewrite ESet.find_add_true; auto);
 
131
        try ( rewrite ESet.find_add_false; auto); auto).
 
132
  Qed.
 
133
End Lemmas.
 
134
 
 
135
 
 
136
Inductive list (A : Set) : Set :=
 
137
  | nil : list A
 
138
  | cons : A -> list A -> list A.
 
139
 
 
140
Module ListDict (E: ELEM). 
 
141
  Definition T := list E.T.
 
142
  Definition elt := E.T.
 
143
   
 
144
  Definition empty := nil elt.
 
145
  Definition add (e : elt) (s : T) := cons elt e s.
 
146
  Fixpoint find (e : elt) (s : T) {struct s} : bool :=
 
147
    match s with
 
148
    | nil => false
 
149
    | cons e' s' => ifte (E.eq_dec e e') true (find e s')
 
150
    end.
 
151
 
 
152
  Definition find_empty_false (e : elt) := refl_equal false.
 
153
 
 
154
  Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
 
155
    intros.
 
156
    simpl in |- *.
 
157
    elim (Reflexivity_provable _ _ (E.eq_dec e e)).
 
158
    intros.
 
159
     rewrite H.
 
160
    auto.
 
161
 
 
162
  Qed.
 
163
  
 
164
 
 
165
  Lemma find_add_false :
 
166
   forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
 
167
    intros.
 
168
    simpl in |- *.
 
169
    elim (Disequality_provable _ _ _ H (E.eq_dec e e')).
 
170
    intros.
 
171
     rewrite H0.
 
172
    simpl in |- *.
 
173
    reflexivity.
 
174
  Qed.    
 
175
  
 
176
 
 
177
End ListDict.
 
178
 
 
179
 
 
180
Module L : SET := ListDict.
 
181
 
 
182
 
 
183
 
 
184
 
 
185
 
 
186
 
 
187