← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/micromega/Tauto.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/micromega/Tauto.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
(* Micromega: A reflexive tactic using the Positivstellensatz           *)
 
10
(*                                                                      *)
 
11
(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
 
12
(*                                                                      *)
 
13
(************************************************************************)
 
14
 
 
15
Require Import List.
 
16
Require Import Refl.
 
17
Require Import Bool.
 
18
 
 
19
Set Implicit Arguments.
 
20
 
 
21
 
 
22
  Inductive BFormula (A:Type) : Type :=
 
23
  | TT   : BFormula A 
 
24
  | FF   : BFormula A
 
25
  | X : Prop -> BFormula A
 
26
  | A : A -> BFormula A 
 
27
  | Cj  : BFormula A -> BFormula A -> BFormula A
 
28
  | D   : BFormula A-> BFormula A -> BFormula A
 
29
  | N  : BFormula A -> BFormula A
 
30
  | I : BFormula A-> BFormula A-> BFormula A. 
 
31
 
 
32
  Fixpoint eval_f (A:Type)  (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop :=
 
33
    match f with
 
34
      | TT => True
 
35
      | FF => False
 
36
      | A a =>  ev a
 
37
      | X p => p
 
38
      | Cj e1 e2 => (eval_f  ev e1) /\ (eval_f ev e2)
 
39
      | D e1 e2  => (eval_f  ev e1) \/ (eval_f  ev e2)
 
40
      | N e     => ~ (eval_f  ev e)
 
41
      | I f1 f2 => (eval_f  ev f1) -> (eval_f  ev f2)
 
42
    end.
 
43
 
 
44
 
 
45
  Lemma map_simpl : forall A B f l, @map A B f l = match l with 
 
46
                                                 | nil => nil
 
47
                                                 | a :: l=> (f a) :: (@map A B f l)
 
48
                                               end.
 
49
  Proof.
 
50
    destruct l ; reflexivity.
 
51
  Qed.
 
52
 
 
53
 
 
54
 
 
55
  Section S.
 
56
 
 
57
    Variable Env   : Type.
 
58
    Variable Term  : Type.
 
59
    Variable eval  : Env -> Term -> Prop.
 
60
    Variable Term' : Type.  
 
61
    Variable eval'  : Env -> Term' -> Prop.
 
62
 
 
63
 
 
64
 
 
65
    Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
 
66
 
 
67
 
 
68
    Definition clause := list  Term'.
 
69
    Definition cnf := list clause.
 
70
 
 
71
    Variable normalise : Term -> cnf.
 
72
    Variable negate : Term -> cnf.
 
73
 
 
74
 
 
75
    Definition tt : cnf := @nil clause.
 
76
    Definition ff : cnf :=  cons (@nil Term') nil.
 
77
 
 
78
 
 
79
    Definition or_clause_cnf (t:clause) (f:cnf) : cnf :=
 
80
      List.map (fun x => (t++x)) f.
 
81
    
 
82
    Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
 
83
      match f with
 
84
        | nil => tt
 
85
        | e :: rst => (or_cnf rst f') ++ (or_clause_cnf e f')
 
86
      end.
 
87
    
 
88
 
 
89
    Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf :=
 
90
      f1 ++ f2.
 
91
    
 
92
    Fixpoint xcnf (pol : bool) (f : BFormula Term)  {struct f}: cnf :=
 
93
      match f with
 
94
        | TT => if pol then tt else ff
 
95
        | FF => if pol then ff else tt
 
96
        | X p => if pol then ff else ff (* This is not complete - cannot negate any proposition *)
 
97
        | A x => if pol then normalise x else negate x
 
98
        | N e  => xcnf (negb pol) e
 
99
        | Cj e1 e2 => 
 
100
          (if pol then and_cnf else or_cnf) (xcnf pol e1) (xcnf pol e2)
 
101
        | D e1 e2  => (if pol then or_cnf else and_cnf) (xcnf pol e1) (xcnf pol e2)
 
102
        | I e1 e2 => (if pol then or_cnf else and_cnf) (xcnf (negb pol) e1) (xcnf pol e2)
 
103
      end.
 
104
 
 
105
  Definition eval_cnf (env : Term' -> Prop) (f:cnf) := make_conj  (fun cl => ~ make_conj  env cl) f.
 
106
  
 
107
 
 
108
  Lemma eval_cnf_app : forall env x y, eval_cnf (eval' env) (x++y) -> eval_cnf (eval' env) x /\ eval_cnf (eval' env) y.
 
109
  Proof.
 
110
    unfold eval_cnf.
 
111
    intros.
 
112
    rewrite make_conj_app in H ; auto.
 
113
  Qed.
 
114
    
 
115
 
 
116
  Lemma or_clause_correct : forall env t f, eval_cnf (eval' env) (or_clause_cnf t f) -> (~ make_conj  (eval' env) t) \/ (eval_cnf (eval' env) f).
 
117
  Proof.
 
118
    unfold eval_cnf.
 
119
    unfold or_clause_cnf.
 
120
    induction f.
 
121
    simpl.
 
122
    intros ; right;auto.
 
123
    (**)
 
124
    rewrite map_simpl.
 
125
    intros.
 
126
    rewrite make_conj_cons in H.
 
127
    destruct H as [HH1 HH2].
 
128
    generalize (IHf HH2) ; clear IHf ; intro.
 
129
    destruct H.
 
130
    left ; auto.
 
131
    rewrite make_conj_cons.
 
132
    destruct (not_make_conj_app _ _ _ (no_middle_eval' env) HH1).
 
133
    tauto.
 
134
    tauto.
 
135
  Qed.
 
136
 
 
137
 Lemma eval_cnf_cons : forall env a f,  (~ make_conj  (eval' env) a) -> eval_cnf (eval' env) f -> eval_cnf (eval' env) (a::f).
 
138
 Proof.
 
139
   intros.
 
140
   unfold eval_cnf in *.
 
141
   rewrite make_conj_cons ; eauto.
 
142
 Qed.
 
143
 
 
144
  Lemma or_cnf_correct : forall env f f', eval_cnf (eval' env) (or_cnf f f') -> (eval_cnf (eval' env)  f) \/ (eval_cnf (eval' env) f').
 
145
  Proof.
 
146
    induction f.
 
147
    unfold eval_cnf.
 
148
    simpl.
 
149
    tauto.
 
150
    (**)
 
151
    intros.
 
152
    simpl in H.
 
153
    destruct (eval_cnf_app _ _ _ H).
 
154
    clear H.
 
155
    destruct (IHf _ H0).
 
156
    destruct (or_clause_correct _ _ _ H1).
 
157
    left.
 
158
    apply eval_cnf_cons ; auto.
 
159
    right ; auto.
 
160
    right ; auto.
 
161
  Qed.
 
162
 
 
163
  Variable normalise_correct : forall env t, eval_cnf (eval' env) (normalise t) -> eval env t.
 
164
 
 
165
  Variable negate_correct : forall env t, eval_cnf  (eval' env) (negate t) -> ~ eval env t.
 
166
 
 
167
 
 
168
  Lemma xcnf_correct : forall f pol env, eval_cnf (eval' env) (xcnf pol f) -> eval_f (eval env) (if pol then f else N f).
 
169
  Proof.
 
170
    induction f.
 
171
    (* TT *)
 
172
    unfold eval_cnf.
 
173
    simpl.
 
174
    destruct pol ; simpl ; auto.
 
175
    (* FF *)
 
176
    unfold eval_cnf.
 
177
    destruct pol; simpl ; auto.
 
178
    (* P *)
 
179
    simpl.
 
180
    destruct pol ; intros ;simpl.
 
181
    unfold eval_cnf in H.
 
182
    (* Here I have to drop the proposition *)
 
183
    simpl in H.
 
184
    tauto.
 
185
    (* Here, I could store P in the clause *)
 
186
    unfold eval_cnf in H;simpl in H.
 
187
    tauto.
 
188
    (* A *)
 
189
    simpl.
 
190
    destruct pol ; simpl.
 
191
    intros.
 
192
    apply normalise_correct  ; auto.
 
193
    (* A 2 *)
 
194
    intros.
 
195
    apply  negate_correct ; auto.
 
196
    auto.
 
197
    (* Cj *)
 
198
    destruct pol ; simpl.
 
199
    (* pol = true *)
 
200
    intros.
 
201
    unfold and_cnf in H.
 
202
    destruct (eval_cnf_app  _ _ _ H).
 
203
    clear H.
 
204
    split.
 
205
    apply (IHf1 _ _ H0).
 
206
    apply (IHf2 _ _ H1).
 
207
    (* pol = false *)
 
208
    intros.
 
209
    destruct (or_cnf_correct _ _ _ H).
 
210
    generalize (IHf1 false  env H0).
 
211
    simpl.
 
212
    tauto.
 
213
    generalize (IHf2 false  env H0).
 
214
    simpl.
 
215
    tauto.
 
216
    (* D *)
 
217
    simpl.
 
218
    destruct pol.
 
219
    (* pol = true *)
 
220
    intros.
 
221
    destruct (or_cnf_correct _ _ _ H).
 
222
    generalize (IHf1 _  env H0).
 
223
    simpl.
 
224
    tauto.
 
225
    generalize (IHf2 _  env H0).
 
226
    simpl.
 
227
    tauto.
 
228
    (* pol = true *)
 
229
    unfold and_cnf.
 
230
    intros.
 
231
    destruct (eval_cnf_app  _ _ _ H).
 
232
    clear H.
 
233
    simpl.
 
234
    generalize (IHf1 _ _ H0).
 
235
    generalize (IHf2 _ _ H1).
 
236
    simpl.
 
237
    tauto.
 
238
    (**)
 
239
    simpl.
 
240
    destruct pol ; simpl.
 
241
    intros.
 
242
    apply (IHf false) ; auto.
 
243
    intros.
 
244
    generalize (IHf _ _ H).
 
245
    tauto.
 
246
    (* I *)
 
247
    simpl; intros.
 
248
    destruct pol.
 
249
    simpl.
 
250
    intro.
 
251
    destruct (or_cnf_correct _ _ _ H).
 
252
    generalize (IHf1 _ _ H1).
 
253
    simpl in *.
 
254
    tauto.
 
255
    generalize (IHf2 _ _ H1).
 
256
    auto.
 
257
    (* pol = false *)
 
258
    unfold and_cnf in H.
 
259
    simpl in H.
 
260
    destruct (eval_cnf_app _ _ _ H).
 
261
    generalize (IHf1 _ _ H0).    
 
262
    generalize (IHf2 _ _ H1).    
 
263
    simpl.
 
264
    tauto.
 
265
  Qed.
 
266
 
 
267
 
 
268
  Variable Witness : Type.
 
269
  Variable checker : list Term' -> Witness -> bool.
 
270
  
 
271
  Variable checker_sound : forall t  w, checker t w = true -> forall env, make_impl (eval' env)  t False.
 
272
 
 
273
  Fixpoint cnf_checker (f : cnf) (l : list Witness)  {struct f}: bool :=
 
274
    match f with
 
275
      | nil => true
 
276
      | e::f => match l with 
 
277
                  | nil => false
 
278
                  | c::l => match checker e c with
 
279
                              | true => cnf_checker f l
 
280
                              |   _  => false
 
281
                            end
 
282
                end
 
283
      end.
 
284
 
 
285
  Lemma cnf_checker_sound : forall t  w, cnf_checker t w = true -> forall env, eval_cnf  (eval' env)  t.
 
286
  Proof.
 
287
    unfold eval_cnf.
 
288
    induction t.
 
289
    (* bc *)
 
290
    simpl.
 
291
    auto.
 
292
    (* ic *)
 
293
    simpl.
 
294
    destruct w.
 
295
    intros ; discriminate.
 
296
    case_eq (checker a w) ; intros ; try discriminate.
 
297
    generalize (@checker_sound _ _ H env).
 
298
    generalize (IHt _ H0 env) ; intros.
 
299
    destruct t.
 
300
    red ; intro.
 
301
    rewrite <- make_conj_impl in H2.
 
302
    tauto.
 
303
    rewrite <- make_conj_impl in H2.
 
304
    tauto.
 
305
  Qed.
 
306
 
 
307
 
 
308
  Definition tauto_checker (f:BFormula Term) (w:list Witness) : bool :=
 
309
    cnf_checker (xcnf true f) w.
 
310
 
 
311
  Lemma tauto_checker_sound : forall t  w, tauto_checker t w = true -> forall env, eval_f  (eval env)  t.
 
312
  Proof.
 
313
    unfold tauto_checker.
 
314
    intros.
 
315
    change (eval_f (eval env) t) with (eval_f (eval env) (if true then t else TT Term)).
 
316
    apply (xcnf_correct t true).
 
317
    eapply cnf_checker_sound ; eauto.
 
318
  Qed.
 
319
 
 
320
 
 
321
 
 
322
 
 
323
End S.
 
324