← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/micromega/CheckerMaker.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/CheckerMaker.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 Setoid.
 
16
Require Import Decidable.
 
17
Require Import List.
 
18
Require Import Refl.
 
19
 
 
20
Set Implicit Arguments.
 
21
 
 
22
Section CheckerMaker.
 
23
 
 
24
(* 'Formula' is a syntactic representation of a certain kind of propositions. *)
 
25
Variable Formula : Type.
 
26
 
 
27
Variable Env : Type.
 
28
 
 
29
Variable eval : Env -> Formula -> Prop.
 
30
 
 
31
Variable Formula' : Type.
 
32
 
 
33
Variable eval' : Env -> Formula' -> Prop.
 
34
 
 
35
Variable normalise : Formula -> Formula'.
 
36
 
 
37
Variable negate : Formula -> Formula'.
 
38
 
 
39
Hypothesis normalise_sound :
 
40
  forall (env : Env) (t : Formula), eval env t -> eval' env (normalise t).
 
41
 
 
42
Hypothesis negate_correct :
 
43
  forall (env : Env) (t : Formula), eval env t <-> ~ (eval' env (negate t)).
 
44
 
 
45
Variable Witness : Type.
 
46
 
 
47
Variable check_formulas' : list Formula' -> Witness -> bool.
 
48
 
 
49
Hypothesis check_formulas'_sound :
 
50
  forall (l : list Formula') (w : Witness),
 
51
    check_formulas' l w = true ->
 
52
      forall env : Env, make_impl (eval' env) l False.
 
53
 
 
54
Definition normalise_list : list Formula -> list Formula' := map normalise.
 
55
Definition negate_list : list Formula -> list Formula' := map negate.
 
56
 
 
57
Definition check_formulas (l : list Formula) (w : Witness) : bool :=
 
58
  check_formulas' (map normalise l) w.
 
59
 
 
60
(* Contraposition of normalise_sound for lists *)
 
61
Lemma normalise_sound_contr : forall (env : Env) (l : list Formula),
 
62
  make_impl (eval' env) (map normalise l) False -> make_impl (eval env) l False.
 
63
Proof.
 
64
intros env l; induction l as [| t l IH]; simpl in *.
 
65
trivial.
 
66
intros H1 H2. apply IH. apply H1. now apply normalise_sound.
 
67
Qed.
 
68
 
 
69
Theorem check_formulas_sound :
 
70
  forall (l : list Formula) (w : Witness),
 
71
    check_formulas l w = true -> forall env : Env, make_impl (eval env) l False.
 
72
Proof.
 
73
unfold check_formulas; intros l w H env. destruct l as [| t l]; simpl in *.
 
74
pose proof (check_formulas'_sound H env) as H1; now simpl in H1.
 
75
intro H1. apply normalise_sound in H1.
 
76
pose proof (check_formulas'_sound H env) as H2; simpl in H2.
 
77
apply H2 in H1. now apply normalise_sound_contr.
 
78
Qed.
 
79
 
 
80
(* In check_conj_formulas', t2 is supposed to be a list of negations of
 
81
formulas. If, for example, t1 = [A1, A2] and t2 = [~ B1, ~ B2], then
 
82
check_conj_formulas' checks that each of [~ B1, A1, A2] and [~ B2, A1, A2] is
 
83
inconsistent. This means that A1 /\ A2 -> B1 and A1 /\ A2 -> B1, i.e., that
 
84
A1 /\ A2 -> B1 /\ B2. *)
 
85
 
 
86
Fixpoint check_conj_formulas'
 
87
  (t1 : list Formula') (wits : list Witness) (t2 : list Formula') {struct wits} : bool :=
 
88
match t2 with
 
89
| nil => true
 
90
| t':: rt2 =>
 
91
  match wits with
 
92
  | nil => false
 
93
  | w :: rwits =>
 
94
    match check_formulas' (t':: t1) w with
 
95
    | true => check_conj_formulas' t1 rwits rt2
 
96
    | false => false
 
97
    end
 
98
  end
 
99
end.
 
100
 
 
101
(* checks whether the conjunction of t1 implies the conjunction of t2 *)
 
102
 
 
103
Definition check_conj_formulas
 
104
  (t1 : list Formula) (wits : list Witness) (t2 : list Formula) : bool :=
 
105
    check_conj_formulas' (normalise_list t1) wits (negate_list t2).
 
106
 
 
107
Theorem check_conj_formulas_sound :
 
108
  forall (t1 : list Formula) (t2 : list Formula) (wits : list Witness),
 
109
    check_conj_formulas t1 wits t2 = true ->
 
110
      forall env : Env, make_impl (eval env) t1 (make_conj (eval env) t2).
 
111
Proof.
 
112
intro t1; induction t2 as [| a2 t2' IH].
 
113
intros; apply make_impl_true.
 
114
intros wits H env.
 
115
unfold check_conj_formulas in H; simpl in H.
 
116
destruct wits as [| w ws]; simpl in H. discriminate.
 
117
case_eq (check_formulas' (negate a2 :: normalise_list t1) w);
 
118
intro H1; rewrite H1 in H; [| discriminate].
 
119
assert (H2 : make_impl (eval' env) (negate a2 :: normalise_list t1) False) by
 
120
now apply check_formulas'_sound with (w := w). clear H1.
 
121
pose proof (IH ws H env) as H1. simpl in H2.
 
122
assert (H3 : eval' env (negate a2) -> make_impl (eval env) t1 False)
 
123
by auto using normalise_sound_contr. clear H2.
 
124
rewrite <- make_conj_impl in *.
 
125
rewrite make_conj_cons. intro H2. split.
 
126
apply <- negate_correct. intro; now elim H3. exact (H1 H2).
 
127
Qed.
 
128
 
 
129
End CheckerMaker.