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