← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/rtauto/Rtauto.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:
contrib/rtauto/Rtauto.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
(* $Id: Rtauto.v 7639 2005-12-02 10:01:15Z gregoire $ *)
 
10
 
 
11
 
 
12
Require Export List.
 
13
Require Export Bintree.
 
14
Require Import Bool.
 
15
Unset Boxed Definitions.
 
16
 
 
17
Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 
18
Ltac clean:=try (simpl;congruence).
 
19
 
 
20
Inductive form:Set:=
 
21
  Atom : positive -> form
 
22
| Arrow : form -> form -> form
 
23
| Bot
 
24
| Conjunct : form -> form -> form 
 
25
| Disjunct : form -> form -> form.
 
26
 
 
27
Notation "[ n ]":=(Atom n).
 
28
Notation "A =>> B":= (Arrow A B) (at level 59, right associativity).
 
29
Notation "#" := Bot.
 
30
Notation "A //\\ B" := (Conjunct A B) (at level 57, left associativity).
 
31
Notation "A \\// B" := (Disjunct A B) (at level 58, left associativity).
 
32
 
 
33
Definition ctx := Store form.
 
34
 
 
35
Fixpoint pos_eq (m n:positive) {struct m} :bool :=
 
36
match m with
 
37
  xI mm => match n with xI nn => pos_eq mm nn | _ => false end
 
38
| xO mm => match n with xO nn => pos_eq mm nn | _ => false end
 
39
| xH => match n with xH => true | _ => false end
 
40
end. 
 
41
 
 
42
Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
 
43
induction m;simpl;destruct n;congruence ||
 
44
(intro e;apply f_equal with positive;auto).
 
45
Qed.
 
46
 
 
47
Fixpoint form_eq (p q:form) {struct p} :bool :=
 
48
match p with
 
49
  Atom m => match q with Atom n => pos_eq m n | _ => false end
 
50
| Arrow p1 p2 => 
 
51
match q with 
 
52
  Arrow q1 q2 => form_eq p1 q1 && form_eq p2 q2 
 
53
| _ => false end
 
54
| Bot => match q with Bot => true | _ => false end
 
55
| Conjunct p1 p2 => 
 
56
match q with 
 
57
  Conjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
 
58
| _ => false 
 
59
end
 
60
| Disjunct p1 p2 => 
 
61
match q with 
 
62
  Disjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
 
63
| _ => false 
 
64
end
 
65
end. 
 
66
 
 
67
Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q.
 
68
induction p;destruct q;simpl;clean.
 
69
intro h;generalize (pos_eq_refl _ _ h);congruence.
 
70
caseq (form_eq p1 q1);clean.
 
71
intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
 
72
caseq (form_eq p1 q1);clean.
 
73
intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
 
74
caseq (form_eq p1 q1);clean.
 
75
intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
 
76
Qed.
 
77
 
 
78
Implicit Arguments form_eq_refl [p q].
 
79
 
 
80
Section with_env.
 
81
 
 
82
Variable env:Store Prop.
 
83
 
 
84
Fixpoint interp_form (f:form): Prop :=
 
85
match f with
 
86
[n]=> match get n env with PNone => True | PSome P => P end
 
87
| A =>> B => (interp_form A) -> (interp_form B)
 
88
| # => False
 
89
| A //\\ B => (interp_form A) /\ (interp_form B)
 
90
| A \\// B => (interp_form A) \/ (interp_form B)
 
91
end.
 
92
 
 
93
Notation "[[ A ]]" := (interp_form A).
 
94
 
 
95
Fixpoint interp_ctx (hyps:ctx) (F:Full hyps) (G:Prop) {struct F} : Prop :=
 
96
match F with
 
97
  F_empty => G
 
98
| F_push H hyps0 F0 =>  interp_ctx hyps0 F0  ([[H]] -> G)
 
99
end.
 
100
 
 
101
Require Export BinPos.
 
102
 
 
103
Ltac wipe := intros;simpl;constructor.  
 
104
 
 
105
Lemma compose0 : 
 
106
forall hyps F (A:Prop),
 
107
 A -> 
 
108
 (interp_ctx hyps F A).
 
109
induction F;intros A H;simpl;auto.
 
110
Qed.
 
111
 
 
112
Lemma compose1 : 
 
113
forall hyps F (A B:Prop),
 
114
 (A -> B) ->
 
115
 (interp_ctx hyps F A) ->
 
116
 (interp_ctx hyps F B).
 
117
induction F;intros A B H;simpl;auto.
 
118
apply IHF;auto.
 
119
Qed.
 
120
 
 
121
Theorem compose2 : 
 
122
forall hyps F (A B C:Prop),
 
123
 (A -> B -> C) -> 
 
124
 (interp_ctx hyps F A) ->
 
125
 (interp_ctx hyps F B) ->
 
126
 (interp_ctx hyps F C).
 
127
induction F;intros A B C H;simpl;auto.
 
128
apply IHF;auto.
 
129
Qed.
 
130
 
 
131
Theorem compose3 : 
 
132
forall hyps F (A B C D:Prop),
 
133
 (A -> B -> C -> D) -> 
 
134
 (interp_ctx hyps F A) -> 
 
135
 (interp_ctx hyps F B) ->
 
136
 (interp_ctx hyps F C) ->
 
137
 (interp_ctx hyps F D).
 
138
induction F;intros A B C D H;simpl;auto.
 
139
apply IHF;auto.
 
140
Qed.
 
141
 
 
142
Lemma weaken : forall hyps F f G,
 
143
 (interp_ctx hyps F G) ->
 
144
 (interp_ctx (hyps\f)  (F_push f hyps F) G).
 
145
induction F;simpl;intros;auto.
 
146
apply compose1 with ([[a]]-> G);auto.
 
147
Qed.
 
148
 
 
149
Theorem project_In : forall hyps F g, 
 
150
In g hyps F ->
 
151
interp_ctx hyps F [[g]].
 
152
induction F;simpl.
 
153
contradiction.
 
154
intros g H;destruct H.
 
155
subst;apply compose0;simpl;trivial.
 
156
apply compose1 with [[g]];auto.
 
157
Qed.
 
158
 
 
159
Theorem project : forall hyps F p g, 
 
160
get  p hyps = PSome g->
 
161
interp_ctx hyps F [[g]].
 
162
intros hyps F p g e; apply project_In.
 
163
apply get_In with p;assumption.
 
164
Qed.
 
165
 
 
166
Implicit Arguments project [hyps p g].
 
167
 
 
168
Inductive proof:Set :=
 
169
  Ax : positive -> proof
 
170
| I_Arrow : proof -> proof
 
171
| E_Arrow : positive -> positive -> proof -> proof
 
172
| D_Arrow : positive -> proof -> proof -> proof
 
173
| E_False : positive -> proof
 
174
| I_And: proof -> proof -> proof
 
175
| E_And: positive -> proof -> proof
 
176
| D_And: positive -> proof -> proof
 
177
| I_Or_l: proof -> proof
 
178
| I_Or_r: proof -> proof
 
179
| E_Or: positive -> proof -> proof -> proof
 
180
| D_Or: positive -> proof -> proof
 
181
| Cut: form -> proof -> proof -> proof.
 
182
 
 
183
Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
 
184
 
 
185
Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool :=
 
186
 match P with
 
187
   Ax i => 
 
188
     match get i hyps with
 
189
         PSome F => form_eq F gl
 
190
 | _ => false
 
191
    end 
 
192
| I_Arrow p =>
 
193
   match gl with
 
194
      A  =>> B  => check_proof (hyps \ A) B p
 
195
   | _ => false        
 
196
    end 
 
197
| E_Arrow i j p =>
 
198
   match get i hyps,get j hyps with
 
199
       PSome A,PSome (B =>>C) =>
 
200
         form_eq A B && check_proof (hyps \ C) (gl) p
 
201
    | _,_ => false
 
202
    end
 
203
| D_Arrow i p1 p2 => 
 
204
   match get i hyps with
 
205
      PSome  ((A =>>B)=>>C) =>
 
206
     (check_proof ( hyps \ B =>> C \ A) B p1) && (check_proof (hyps \ C) gl p2)
 
207
    | _ => false
 
208
  end
 
209
| E_False i =>
 
210
  match get i hyps with
 
211
    PSome # => true
 
212
  | _ => false
 
213
  end
 
214
| I_And p1 p2 =>
 
215
   match gl with
 
216
      A //\\ B =>
 
217
      check_proof hyps A p1 && check_proof hyps B p2
 
218
      | _ => false
 
219
      end
 
220
| E_And i p => 
 
221
   match get i hyps with
 
222
      PSome  (A //\\ B) => check_proof (hyps \ A \ B) gl p
 
223
    | _=> false
 
224
   end
 
225
| D_And i p => 
 
226
   match get i hyps with
 
227
      PSome  (A //\\ B =>> C) => check_proof (hyps \ A=>>B=>>C) gl p
 
228
    | _=> false
 
229
   end
 
230
| I_Or_l p =>
 
231
   match gl with
 
232
      (A \\// B) => check_proof hyps A p
 
233
      | _ => false
 
234
      end
 
235
| I_Or_r p =>
 
236
   match gl with
 
237
      (A \\// B) => check_proof hyps B p
 
238
      | _ => false
 
239
      end
 
240
| E_Or i p1 p2 =>
 
241
  match get i hyps with
 
242
  PSome (A \\// B) =>
 
243
  check_proof (hyps \ A) gl p1 && check_proof (hyps \ B) gl p2
 
244
  | _=> false
 
245
  end
 
246
| D_Or i p => 
 
247
   match get i hyps with
 
248
      PSome  (A \\// B =>> C) =>
 
249
      (check_proof (hyps \ A=>>C \ B=>>C) gl p)
 
250
    | _=> false
 
251
   end
 
252
| Cut A p1 p2 =>
 
253
  check_proof hyps A p1 && check_proof (hyps \ A) gl p2
 
254
end. 
 
255
 
 
256
Theorem interp_proof: 
 
257
forall p hyps F gl, 
 
258
check_proof hyps gl p = true -> interp_ctx hyps F [[gl]].
 
259
 
 
260
induction p;intros hyps F gl.
 
261
 
 
262
(* cas Axiom *)
 
263
Focus 1.
 
264
simpl;caseq (get p hyps);clean.
 
265
intros f nth_f e;rewrite <- (form_eq_refl e).
 
266
apply project with p;trivial.
 
267
 
 
268
(* Cas Arrow_Intro *)
 
269
Focus 1.
 
270
destruct gl;clean.
 
271
simpl;intros.
 
272
change (interp_ctx (hyps\gl1)  (F_push gl1 hyps F) [[gl2]]).
 
273
apply IHp;try constructor;trivial.
 
274
 
 
275
(* Cas Arrow_Elim *)
 
276
Focus 1.
 
277
simpl check_proof;caseq (get p hyps);clean.
 
278
intros f ef;caseq (get p0 hyps);clean.
 
279
intros f0 ef0;destruct f0;clean.
 
280
caseq (form_eq f f0_1);clean.
 
281
simpl;intros e check_p1.
 
282
generalize  (project  F ef) (project  F ef0) 
 
283
(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1);
 
284
clear check_p1 IHp p p0 p1 ef ef0.
 
285
simpl.
 
286
apply compose3.
 
287
rewrite (form_eq_refl e).
 
288
auto.
 
289
 
 
290
(* cas Arrow_Destruct *)
 
291
Focus 1.
 
292
simpl;caseq (get p1 hyps);clean.
 
293
intros f ef;destruct f;clean.
 
294
destruct f1;clean.
 
295
caseq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
 
296
intros check_p1 check_p2.
 
297
generalize (project F ef)
 
298
(IHp1 (hyps \ f1_2 =>> f2 \ f1_1)   
 
299
(F_push f1_1 (hyps \ f1_2 =>> f2)
 
300
 (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1)
 
301
(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2).
 
302
simpl;apply compose3;auto.
 
303
 
 
304
(* Cas False_Elim *)
 
305
Focus 1.
 
306
simpl;caseq (get p hyps);clean.
 
307
intros f ef;destruct f;clean.
 
308
intros _; generalize (project F ef).
 
309
apply compose1;apply False_ind.
 
310
 
 
311
(* Cas And_Intro *)
 
312
Focus 1.
 
313
simpl;destruct gl;clean.
 
314
caseq (check_proof hyps gl1 p1);clean.
 
315
intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2).
 
316
apply compose2 ;simpl;auto.
 
317
 
 
318
(* cas And_Elim *)
 
319
Focus 1.
 
320
simpl;caseq (get p hyps);clean.
 
321
intros f ef;destruct f;clean.
 
322
intro check_p;generalize  (project F ef)
 
323
(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p).
 
324
simpl;apply compose2;intros [h1 h2];auto.
 
325
 
 
326
(* cas And_Destruct *)
 
327
Focus 1.
 
328
simpl;caseq (get p hyps);clean.
 
329
intros f ef;destruct f;clean.
 
330
destruct f1;clean.
 
331
intro H;generalize  (project F ef)
 
332
(IHp (hyps \ f1_1 =>> f1_2 =>> f2)  
 
333
(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl.
 
334
apply compose2;auto.
 
335
 
 
336
(* cas Or_Intro_left *)
 
337
Focus 1.
 
338
destruct gl;clean.
 
339
intro Hp;generalize (IHp hyps F gl1 Hp).
 
340
apply compose1;simpl;auto.
 
341
 
 
342
(* cas Or_Intro_right *)
 
343
Focus 1.
 
344
destruct gl;clean.
 
345
intro Hp;generalize (IHp hyps F gl2 Hp).
 
346
apply compose1;simpl;auto.
 
347
 
 
348
(* cas Or_elim *)
 
349
Focus 1.
 
350
simpl;caseq (get p1 hyps);clean.
 
351
intros f ef;destruct f;clean.
 
352
caseq (check_proof (hyps \ f1) gl p2);clean.
 
353
intros check_p1 check_p2;generalize (project F ef)
 
354
(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1)
 
355
(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2);
 
356
simpl;apply compose3;simpl;intro h;destruct h;auto.
 
357
 
 
358
(* cas Or_Destruct *)
 
359
Focus 1.
 
360
simpl;caseq (get p hyps);clean.
 
361
intros f ef;destruct f;clean.
 
362
destruct f1;clean.
 
363
intro check_p0;generalize (project F ef)
 
364
(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2)
 
365
(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) 
 
366
 (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl.
 
367
apply compose2;auto.
 
368
 
 
369
(* cas Cut *)
 
370
Focus 1.
 
371
simpl;caseq (check_proof hyps f p1);clean.
 
372
intros check_p1 check_p2;
 
373
generalize (IHp1 hyps F f check_p1) 
 
374
(IHp2 (hyps\f) (F_push f hyps F) gl check_p2);
 
375
simpl; apply compose2;auto.
 
376
Qed.
 
377
 
 
378
Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True.
 
379
intros gl prf;caseq (check_proof empty gl prf);intro check_prf.
 
380
change (interp_ctx empty F_empty [[gl]]) ;
 
381
apply interp_proof with prf;assumption.
 
382
trivial.
 
383
Qed.
 
384
 
 
385
End with_env.
 
386
 
 
387
(*
 
388
(* A small example *)
 
389
Parameters A B C D:Prop.
 
390
Theorem toto:A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
 
391
exact (Reflect (empty \ A \ B \ C)
 
392
([1] //\\ ([2] \\// [3]) =>> [1] //\\ [2] \\// [1] //\\ [3])
 
393
(I_Arrow (E_And 1 (E_Or 3 
 
394
  (I_Or_l (I_And (Ax 2) (Ax 4))) 
 
395
  (I_Or_r (I_And (Ax 2) (Ax 4))))))).
 
396
Qed.
 
397
Print toto.
 
398
*)