← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/bugs/opened/shouldnotfail/1596.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/opened/shouldnotfail/1596.v
 
1
 
 
2
Require Import Relations.
 
3
Require Import FSets.
 
4
Require Import Arith.
 
5
 
 
6
Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false.
 
7
  destruct b;try tauto.
 
8
Qed.
 
9
 
 
10
Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with
 
11
Definition t := (X.t * Y.t)%type.
 
12
  Definition t := (X.t * Y.t)%type.
 
13
 
 
14
  Definition eq (xy1:t) (xy2:t) := 
 
15
    let (x1,y1) := xy1 in
 
16
      let (x2,y2) := xy2 in
 
17
        (X.eq x1 x2) /\ (Y.eq y1 y2).
 
18
 
 
19
  Definition lt (xy1:t) (xy2:t) := 
 
20
    let (x1,y1) := xy1 in
 
21
      let (x2,y2) := xy2 in
 
22
        (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)).
 
23
 
 
24
  Lemma eq_refl : forall (x:t),(eq x x).
 
25
    destruct x.
 
26
    unfold eq.
 
27
    split;[apply X.eq_refl | apply Y.eq_refl].
 
28
  Qed.
 
29
 
 
30
  Lemma eq_sym : forall (x y:t),(eq x y)->(eq y x).
 
31
    destruct x;destruct y;unfold eq;intro.
 
32
    elim H;clear H;intros.
 
33
    split;[apply X.eq_sym | apply Y.eq_sym];trivial.
 
34
  Qed.
 
35
 
 
36
  Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
 
37
    unfold eq;destruct x;destruct y;destruct z;intros.
 
38
    elim H;clear H;intros.
 
39
    elim H0;clear H0;intros.
 
40
    split;[eapply X.eq_trans | eapply Y.eq_trans];eauto.
 
41
  Qed.
 
42
 
 
43
  Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
 
44
    unfold lt;destruct x;destruct y;destruct z;intros.
 
45
    case H;clear H;intro.
 
46
    case H0;clear H0;intro.
 
47
    left.
 
48
    eapply X.lt_trans;eauto.
 
49
    elim H0;clear H0;intros.
 
50
    left.
 
51
    case (X.compare t0 t4);trivial;intros.
 
52
    generalize (X.eq_sym H0);intro.
 
53
    generalize (X.eq_trans e H2);intro.
 
54
    elim (X.lt_not_eq H H3).
 
55
    generalize (X.lt_trans l H);intro.
 
56
    generalize (X.eq_sym H0);intro.
 
57
    elim (X.lt_not_eq H2 H3).
 
58
    elim H;clear H;intros.
 
59
    case H0;clear H0;intro.
 
60
    left.
 
61
    case (X.compare t0 t4);trivial;intros.
 
62
    generalize (X.eq_sym H);intro.
 
63
    generalize (X.eq_trans H2 e);intro.
 
64
    elim (X.lt_not_eq H0 H3).
 
65
    generalize (X.lt_trans H0 l);intro.
 
66
    generalize (X.eq_sym H);intro.
 
67
    elim (X.lt_not_eq H2 H3).
 
68
    elim H0;clear H0;intros.
 
69
    right.
 
70
    split.
 
71
    eauto.
 
72
    eauto.
 
73
  Qed.
 
74
 
 
75
  Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
 
76
    unfold lt, eq;destruct x;destruct y;intro;intro.
 
77
    elim H0;clear H0;intros.
 
78
    case H.
 
79
    intro.
 
80
    apply (X.lt_not_eq H2 H0).
 
81
    intro.
 
82
    elim H2;clear H2;intros.
 
83
    apply (Y.lt_not_eq H3 H1).
 
84
  Qed.
 
85
 
 
86
  Definition compare : forall (x y:t),(Compare lt eq x y).
 
87
    destruct x;destruct y.
 
88
    case (X.compare t0 t2);intro.
 
89
    apply LT.
 
90
    left;trivial.
 
91
    case (Y.compare t1 t3);intro.
 
92
    apply LT.
 
93
    right.
 
94
    tauto.
 
95
    apply EQ.
 
96
    split;trivial.
 
97
    apply GT.
 
98
    right;auto.
 
99
    apply GT.
 
100
    left;trivial.
 
101
  Defined.
 
102
 
 
103
  Hint Immediate eq_sym.
 
104
  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. 
 
105
End OrderedPair.
 
106
 
 
107
Module MessageSpi.
 
108
  Inductive message : Set :=
 
109
  | MNam : nat -> message.
 
110
 
 
111
  Definition t := message.
 
112
 
 
113
  Fixpoint message_lt (m n:message) {struct m} : Prop :=
 
114
    match (m,n) with
 
115
      | (MNam n1,MNam n2) => n1 < n2
 
116
    end.
 
117
 
 
118
  Module Ord <: OrderedType with Definition t := message with Definition eq :=
 
119
@eq message.
 
120
    Definition t := message.
 
121
    Definition eq := @eq message.
 
122
    Definition lt := message_lt.
 
123
 
 
124
    Lemma eq_refl : forall (x:t),eq x x.
 
125
      unfold eq;auto.
 
126
    Qed.
 
127
 
 
128
    Lemma eq_sym : forall (x y:t),(eq x y )->(eq y x).
 
129
      unfold eq;auto.
 
130
    Qed.
 
131
 
 
132
    Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
 
133
      unfold eq;auto;intros;congruence.
 
134
    Qed.
 
135
 
 
136
    Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
 
137
      unfold lt.
 
138
      induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros.
 
139
      omega.
 
140
    Qed.
 
141
 
 
142
    Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
 
143
      unfold eq;unfold lt.
 
144
      induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate
 
145
H0);injection H0;intros.
 
146
      elim (lt_irrefl n);try omega.
 
147
    Qed.
 
148
 
 
149
    Definition compare : forall (x y:t),(Compare lt eq x y).
 
150
      unfold lt, eq.
 
151
      induction x;destruct y;intros;try (apply LT;simpl;trivial;fail);try
 
152
(apply
 
153
GT;simpl;trivial;fail).
 
154
      case (lt_eq_lt_dec n n0);intros;try (case s;clear s;intros).
 
155
      apply LT;trivial.
 
156
      apply EQ;trivial.
 
157
      rewrite e;trivial.
 
158
      apply GT;trivial.
 
159
    Defined.
 
160
 
 
161
    Hint Immediate eq_sym.
 
162
    Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
 
163
  End Ord.
 
164
 
 
165
  Theorem eq_dec : forall (m n:message),{m=n}+{~(m=n)}.
 
166
    intros.
 
167
    case (Ord.compare m n);intro;[right | left | right];try (red;intro).
 
168
    elim (Ord.lt_not_eq m n);auto.
 
169
    rewrite e;auto.
 
170
    elim (Ord.lt_not_eq n m);auto.
 
171
  Defined.
 
172
End MessageSpi.
 
173
 
 
174
Module MessagePair := OrderedPair MessageSpi.Ord MessageSpi.Ord.
 
175
 
 
176
Module Type Hedge := FSetInterface.S with Module E := MessagePair.
 
177
 
 
178
Module A (H:Hedge).
 
179
  Definition hedge := H.t.
 
180
 
 
181
  Definition message_relation := relation MessageSpi.message.
 
182
 
 
183
  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.message) := H.In (m,n)
 
184
h.
 
185
 
 
186
  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
 
187
    | SynInc : forall (m n:MessageSpi.message),(h m
 
188
n)->(hedge_synthesis_relation h m n).
 
189
 
 
190
  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message)
 
191
(n:MessageSpi.message) {struct m} : bool :=
 
192
    if H.mem (m,n) h 
 
193
      then true 
 
194
      else false.
 
195
 
 
196
  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
 
197
(relation_of_hedge h).
 
198
 
 
199
  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
 
200
(m n:MessageSpi.message),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec
 
201
h m n).
 
202
    unfold hedge_synthesis_spec;unfold relation_of_hedge.
 
203
    induction m;simpl;intro.
 
204
    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
 
205
    apply SynInc;apply H.mem_2;trivial.
 
206
    rewrite H in H0.  (* !! possible here !! *)
 
207
    discriminate H0.
 
208
  Qed.
 
209
End A.
 
210
 
 
211
Module B (H:Hedge).
 
212
  Definition hedge := H.t.
 
213
 
 
214
  Definition message_relation := relation MessageSpi.t.
 
215
 
 
216
  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.t) := H.In (m,n) h.
 
217
 
 
218
  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
 
219
    | SynInc : forall (m n:MessageSpi.t),(h m n)->(hedge_synthesis_relation h m
 
220
n).
 
221
 
 
222
  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t)
 
223
{struct m} : bool :=
 
224
    if H.mem (m,n) h 
 
225
      then true 
 
226
      else false.
 
227
 
 
228
  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
 
229
(relation_of_hedge h).
 
230
 
 
231
  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
 
232
(m n:MessageSpi.t),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec h m
 
233
n).
 
234
    unfold hedge_synthesis_spec;unfold relation_of_hedge.
 
235
    induction m;simpl;intro.
 
236
    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
 
237
    apply SynInc;apply H.mem_2;trivial.
 
238
    
 
239
    rewrite H in H0. (* !! impossible here !! *)
 
240
    discriminate H0.
 
241
  Qed.
 
242
End B.
 
 
b'\\ No newline at end of file'