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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
|
Require Import vericert.common.Vericertlib.
Require Import vericert.hls.Sat.
Definition predicate : Type := positive.
Inductive pred_op : Type :=
| Pvar: (bool * predicate) -> pred_op
| Ptrue: pred_op
| Pfalse: pred_op
| Pand: pred_op -> pred_op -> pred_op
| Por: pred_op -> pred_op -> pred_op.
Declare Scope pred_op.
Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op.
Notation "A ∨ B" := (Por A B) (at level 25) : pred_op.
Notation "⟂" := (Pfalse) : pred_op.
Notation "'T'" := (Ptrue) : pred_op.
Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool :=
match p with
| Pvar (b, p') => if b then a (Pos.to_nat p') else negb (a (Pos.to_nat p'))
| Ptrue => true
| Pfalse => false
| Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a
| Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a
end.
Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) :=
match a with
| nil => nil
| l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b)
end.
Lemma satFormula_concat:
forall a b agn,
satFormula a agn ->
satFormula b agn ->
satFormula (a ++ b) agn.
Proof. induction a; crush. Qed.
Lemma satFormula_concat2:
forall a b agn,
satFormula (a ++ b) agn ->
satFormula a agn /\ satFormula b agn.
Proof.
induction a; simplify;
try apply IHa in H1; crush.
Qed.
Lemma satClause_concat:
forall a a1 a0,
satClause a a1 ->
satClause (a0 ++ a) a1.
Proof. induction a0; crush. Qed.
Lemma satClause_concat2:
forall a a1 a0,
satClause a0 a1 ->
satClause (a0 ++ a) a1.
Proof.
induction a0; crush.
inv H; crush.
Qed.
Lemma satClause_concat3:
forall a b c,
satClause (a ++ b) c ->
satClause a c \/ satClause b c.
Proof.
induction a; crush.
inv H; crush.
apply IHa in H0; crush.
inv H0; crush.
Qed.
Lemma satFormula_mult':
forall p2 a a0,
satFormula p2 a0 \/ satClause a a0 ->
satFormula (map (fun x : list lit => a ++ x) p2) a0.
Proof.
induction p2; crush.
- inv H. inv H0. apply satClause_concat. auto.
apply satClause_concat2; auto.
- apply IHp2.
inv H; crush; inv H0; crush.
Qed.
Lemma satFormula_mult2':
forall p2 a a0,
satFormula (map (fun x : list lit => a ++ x) p2) a0 ->
satClause a a0 \/ satFormula p2 a0.
Proof.
induction p2; crush.
apply IHp2 in H1. inv H1; crush.
apply satClause_concat3 in H0.
inv H0; crush.
Qed.
Lemma satFormula_mult:
forall p1 p2 a,
satFormula p1 a \/ satFormula p2 a ->
satFormula (mult p1 p2) a.
Proof.
induction p1; crush.
apply satFormula_concat; crush.
inv H. inv H0.
apply IHp1. auto.
apply IHp1. auto.
apply satFormula_mult';
inv H; crush.
Qed.
Lemma satFormula_mult2:
forall p1 p2 a,
satFormula (mult p1 p2) a ->
satFormula p1 a \/ satFormula p2 a.
Proof.
induction p1; crush.
apply satFormula_concat2 in H; crush.
apply IHp1 in H0.
inv H0; crush.
apply satFormula_mult2' in H1. inv H1; crush.
Qed.
Fixpoint trans_pred (p: pred_op) :
{fm: formula | forall a,
sat_predicate p a = true <-> satFormula fm a}.
refine
(match p with
| Pvar (b, p') => exist _ (((b, Pos.to_nat p') :: nil) :: nil) _
| Ptrue => exist _ nil _
| Pfalse => exist _ (nil::nil) _
| Pand p1 p2 =>
match trans_pred p1, trans_pred p2 with
| exist _ p1' _, exist _ p2' _ => exist _ (p1' ++ p2') _
end
| Por p1 p2 =>
match trans_pred p1, trans_pred p2 with
| exist _ p1' _, exist _ p2' _ => exist _ (mult p1' p2') _
end
end); split; intros; simpl in *; auto; try solve [crush].
- destruct b; auto. apply negb_true_iff in H. auto.
- destruct b. inv H. inv H0; auto. apply negb_true_iff. inv H. inv H0; eauto. contradiction.
- apply satFormula_concat.
apply andb_prop in H. inv H. apply i in H0. auto.
apply andb_prop in H. inv H. apply i0 in H1. auto.
- apply satFormula_concat2 in H. simplify. apply andb_true_intro.
split. apply i in H0. auto.
apply i0 in H1. auto.
- apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto.
apply i0 in H0. auto.
- apply orb_true_intro.
apply satFormula_mult2 in H. inv H. apply i in H0. auto.
apply i0 in H0. auto.
Defined.
Definition sat_pred (p: pred_op) :
({al : alist | sat_predicate p (interp_alist al) = true}
+ {forall a : asgn, sat_predicate p a = false}).
refine
( match trans_pred p with
| exist _ fm _ =>
match satSolve fm with
| inleft (exist _ a _) => inleft (exist _ a _)
| inright _ => inright _
end
end ).
- apply i in s0. auto.
- intros. specialize (n a). specialize (i a).
destruct (sat_predicate p a). exfalso.
apply n. apply i. auto. auto.
Defined.
Definition sat_pred_simple (p: pred_op) :=
match sat_pred p with
| inleft (exist _ al _) => Some al
| inright _ => None
end.
#[local] Open Scope pred_op.
Fixpoint negate (p: pred_op) :=
match p with
| Pvar (b, pr) => Pvar (negb b, pr)
| T => ⟂
| ⟂ => T
| A ∧ B => negate A ∨ negate B
| A ∨ B => negate A ∧ negate B
end.
Notation "¬ A" := (negate A) (at level 15) : pred_op.
Lemma negate_correct :
forall h a, sat_predicate (negate h) a = negb (sat_predicate h a).
Proof.
induction h; crush.
- repeat destruct_match; subst; crush; symmetry; apply negb_involutive.
- rewrite negb_andb; crush.
- rewrite negb_orb; crush.
Qed.
|
