-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathcad.v
286 lines (240 loc) · 10.4 KB
/
cad.v
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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
(*****************************************************************************)
(* some doc here *)
(*****************************************************************************)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype div.
From mathcomp Require Import tuple finfun generic_quotient bigop finset perm ssralg poly.
From mathcomp Require Import polydiv ssrnum mxpoly binomial finalg zmodp.
From mathcomp Require Import mxtens qe_rcf ordered_qelim mxpoly realalg.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory Num.Theory.
Import ord.
Local Open Scope nat_scope.
Local Open Scope ring_scope.
Local Open Scope quotient_scope.
Section EqFormula.
Variable (T : eqType).
Fixpoint formula_eq (f1 f2 : formula T) := match f1, f2 with
| Bool b1, Bool b2 => b1 == b2
| Equal t1 u1, Equal t2 u2 => (t1 == t2) && (u1 == u2)
| Lt t1 u1, Lt t2 u2 => (t1 == t2) && (u1 == u2)
| Le t1 u1, Le t2 u2 => (t1 == t2) && (u1 == u2)
| Unit t1, Unit t2 => (t1 == t2)
| And f1 g1, And f2 g2 => (formula_eq f1 f2) && (formula_eq g1 g2)
| Or f1 g1, Or f2 g2 => (formula_eq f1 f2) && (formula_eq g1 g2)
| Implies f1 g1, Implies f2 g2 => (formula_eq f1 f2) && (formula_eq g1 g2)
| Not f1, Not f2 => formula_eq f1 f2
| Exists i1 f1, Exists i2 f2 => (i1 == i2) && (formula_eq f1 f2)
| Forall i1 f1, Forall i2 f2 => (i1 == i2) && (formula_eq f1 f2)
| _, _ => false
end.
Lemma formula_eqP : Equality.axiom formula_eq.
Proof.
move=> f1 f2; apply: (iffP idP) => [|<-]; last first.
by elim: f1 {f2}=> x //= y; rewrite ?eqxx // => f ->; rewrite y.
elim: f1 f2.
- by move=> b1 f //=; case: f => //=; move=> b2 /eqP ->.
- by move=> t1 t2 f; case: f => //= u1 u2 /andP [/eqP -> /eqP ->].
- by move=> t1 t2 f; case: f => //= u1 u2 /andP [/eqP -> /eqP ->].
- by move=> t1 t2 f; case: f => //= u1 u2 /andP [/eqP -> /eqP ->].
- by move=> t1 f //=; case: f => //=; move=> t2 /eqP ->.
- move=> f1 hf f2 hg f; case: f => //= g1 g2 /andP [h1 h2].
by rewrite (hf g1) // (hg g2).
- move=> f1 hf f2 hg f; case: f => //= g1 g2 /andP [h1 h2].
by rewrite (hf g1) // (hg g2).
- move=> f1 hf f2 hg f; case: f => //= g1 g2 /andP [h1 h2].
by rewrite (hf g1) // (hg g2).
- by move=> f h1 g; case: g => //= g h2; rewrite (h1 g).
- by move=> i f1 h f2 /=; case: f2 => //= i2 g /andP [/eqP -> h2]; rewrite (h g).
- by move=> i f1 h f2 /=; case: f2 => //= i2 g /andP [/eqP -> h2]; rewrite (h g).
Qed.
Canonical formula_eqMixin := EqMixin formula_eqP.
Canonical formula_eqType := Eval hnf in EqType (formula T) formula_eqMixin.
End EqFormula.
Section ChoiceFormula.
Variable (T : choiceType).
Fixpoint encode_term (t : GRing.term T) := match t with
| GRing.Var i => GenTree.Node (2*i) [::]
| GRing.Const x => GenTree.Leaf x
| GRing.NatConst i => GenTree.Node ((2*i).+1) [::]
| GRing.Add x y => GenTree.Node O ((encode_term x)::(encode_term y)::nil)
| GRing.Opp x => GenTree.Node O ((encode_term x)::nil)
| GRing.NatMul x i => GenTree.Node ((2*i).+2) ((encode_term x)::nil)
| GRing.Mul x y => GenTree.Node 1 ((encode_term x)::(encode_term y)::nil)
| GRing.Inv x => GenTree.Node 1 ((encode_term x)::nil)
| GRing.Exp x i => GenTree.Node ((2*i).+3) ((encode_term x)::nil)
end.
Fixpoint decode_term (t : GenTree.tree T) := match t with
| GenTree.Leaf x => GRing.Const x
| GenTree.Node i s => match s with
| [::] => if (i %% 2)%N == O then GRing.Var T (i %/ 2) else GRing.NatConst T ((i.-1) %/ 2)
| e1::e2::l => if i == O then GRing.Add (decode_term e1) (decode_term e2)
else GRing.Mul (decode_term e1) (decode_term e2)
| e::l => if i == O then GRing.Opp (decode_term e) else
if i == 1%N then GRing.Inv (decode_term e) else
if (i %% 2)%N == O then GRing.NatMul (decode_term e) ((i.-2) %/ 2)
else GRing.Exp (decode_term e) ((i-3) %/ 2)
end
end.
Lemma encode_termK : cancel encode_term decode_term.
Proof.
move=> t.
elim: t.
move=> n /=.
+ by rewrite modnMr eqxx mulKn.
+ by move=> r.
+ by move=> n /=; rewrite {1}mulnC -addn1 modnMDl mulKn.
+ by move=> t1 h1 t2 h2 /=; rewrite h1 h2.
+ by move=> t h /=; rewrite h.
+ by move=> t h n /=; rewrite -addn2 {1}mulnC modnMDl h mulKn.
+ by move=> t1 h1 t2 h2 /=; rewrite h1 h2.
+ by move=> t h /=; rewrite h.
+ by move=> t h n /=; rewrite -addn3 {1}mulnC modnMDl /= h addnK mulKn.
Qed.
(* works *)
(* Definition my_tree := GenTree.tree T. *)
(* Canonical my_tree_of_eqType := [eqType of my_tree]. *)
(* Canonical my_tree_of_choiceType := [choiceType of my_tree]. *)
Definition my_term := GRing.term T.
Canonical my_term_of_eqType := [eqType of my_term].
Fail Canonical my_term_of_choiceType := [choiceType of my_term].
Definition my_term_ChoiceMixin := CanChoiceMixin encode_termK.
Canonical my_term_choiceType := ChoiceType my_term my_term_ChoiceMixin.
(* Definition my_formula := formula T. *)
Canonical my_formula_of_eqType := [eqType of formula T].
Fixpoint encode_formula (f : formula T) := match f with
| Bool b => GenTree.Node b [::]
| Equal t1 t2 => GenTree.Node O ((encode_term t1)::(encode_term t2)::nil)
| Lt t1 t2 => GenTree.Node 1 ((encode_term t1)::(encode_term t2)::nil)
| Le t1 t2 => GenTree.Node 2 ((encode_term t1)::(encode_term t2)::nil)
| Unit t => GenTree.Node O ((encode_term t)::nil)
| And f1 f2 => GenTree.Node 3 ((encode_formula f1)::(encode_formula f2)::nil)
| Or f1 f2 => GenTree.Node 4 ((encode_formula f1)::(encode_formula f2)::nil)
| Implies f1 f2 => GenTree.Node 5 ((encode_formula f1)::(encode_formula f2)::nil)
| Not f => GenTree.Node 1 ((encode_formula f)::nil)
| Exists i f => GenTree.Node (2*i).+2 ((encode_formula f)::nil)
| Forall i f => GenTree.Node (2*i).+3 ((encode_formula f)::nil)
end.
Fixpoint decode_formula (t : GenTree.tree T) := match t with
| GenTree.Leaf x => Unit (Const x)
| GenTree.Node i s => match s with
| [::] => if i == O then Bool false else Bool true
| e1::e2::l => match i with
| 0 => Equal (decode_term e1) (decode_term e2)
| 1 => Lt (decode_term e1) (decode_term e2)
| 2 => Le (decode_term e1) (decode_term e2)
| 3 => And (decode_formula e1) (decode_formula e2)
| 4 => Or (decode_formula e1) (decode_formula e2)
| _ => Implies (decode_formula e1) (decode_formula e2)
end
| e::l => if i == O then Unit (decode_term e) else
if i == 1%N then Not (decode_formula e) else
if (i %% 2)%N == O then Exists ((i.-2) %/ 2) (decode_formula e)
else Forall ((i-3) %/ 2) (decode_formula e)
end
end.
Lemma encode_formulaK : cancel encode_formula decode_formula.
Proof.
move=> f.
elim: f.
+ by move=> b /=; case: b.
+ by move=> t1 t2 /=; rewrite !encode_termK.
+ by move=> t1 t2 /=; rewrite !encode_termK.
+ by move=> t1 t2 /=; rewrite !encode_termK.
+ by move=> t /=; rewrite !encode_termK.
+ by move=> f1 h1 f2 h2 /=; rewrite h1 h2.
+ by move=> f1 h1 f2 h2 /=; rewrite h1 h2.
+ by move=> f1 h1 f2 h2 /=; rewrite h1 h2.
+ by move=> f hf /=; rewrite hf.
+ by move=> i f hf /=; rewrite hf -addn2 {1}mulnC modnMDl mulKn /=.
+ by move=> i f hf /=; rewrite hf -addn3 {1}mulnC modnMDl /= addnK mulKn.
Qed.
Definition formula_ChoiceMixin := CanChoiceMixin encode_formulaK.
Canonical formula_choiceType := ChoiceType (formula T) formula_ChoiceMixin.
End ChoiceFormula.
Section Cad.
Variable R : rcfType. (* is also a realDomainType *)
Fixpoint nquantify (n : nat) (f : formula R) := match n with
| O => f
| S m => Forall m (nquantify m f)
end.
Variable (n : nat).
(* We define a relation in formulas *)
Local Notation equivf_notation f g :=
(rcf_sat [::] (nquantify n ((f ==> g) /\ (g ==> f)))).
Definition equivf f g := equivf_notation f g.
Lemma equivf_refl : reflexive equivf.
Proof.
move=> f; apply/rcf_satP.
by move: [::]; elim: n => [//= | m ih /= x x0].
Qed.
Lemma equivf_sym : symmetric equivf.
Proof.
move=> f g; rewrite /equivf; move: [::].
elim: n => [e |m ih e].
by apply/rcf_satP/rcf_satP; move => [h1 h2]; split.
by apply/rcf_satP/rcf_satP => /= h x; apply/rcf_satP;
[rewrite -ih | rewrite ih]; apply/rcf_satP; apply: h.
Qed.
Lemma equivf_trans : transitive equivf.
Proof.
move=> f g h; rewrite /equivf; move: [::].
elim: n => [e |m ih e] /=.
move/rcf_satP => [ /= h1 h2].
move/rcf_satP => [ /= h3 h4].
apply/rcf_satP; split => h5; first by apply: h3; apply: h1.
by apply: h2; apply: h4.
move/rcf_satP => /= h1; move/rcf_satP => /= h2; apply/rcf_satP => /= x.
apply/rcf_satP; apply: ih; apply/rcf_satP.
exact: h1.
exact: h2.
Qed.
(* we show that equivf is an equivalence *)
Canonical equivf_equiv := EquivRel equivf equivf_refl equivf_sym equivf_trans.
Definition type := {eq_quot equivf}.
Definition type_of of phant R := type.
Notation "{ 'formula' T }" := (type_of (Phant T)).
Fixpoint fv_term (t : GRing.term R) : seq nat :=
match t with
| 'X_i => [::i]
| t1 + t2 | t1 * t2 => undup (fv_term t1 ++ fv_term t2)
| - t1 | t1 *+ _ | t1 ^+ _ | t1^-1 => fv_term t1
| _ => [::]
end%T.
Fixpoint fv_formula (f : ord.formula R) : seq nat :=
match f with
| Bool _ => [::]
| (t1 == t2) | (t1 <% t2)| (t1 <=% t2) => undup (fv_term t1 ++ fv_term t2)
| (Unit t1) => fv_term t1
| (f1 /\ f2) | (f1 \/ f2) | (f1 ==> f2) => undup (fv_formula f1 ++ fv_formula f2)
| (~ f1) => fv_formula f1
| ('exists 'X_i, f1) | ('forall 'X_i, f1) => rem i (fv_formula f1)
end%oT.
Definition nform : pred_class := fun f : formula R =>
rformula f && all (fun x => (x < n)%N) (fv_formula f).
(* Lemma holds_rcons_zero (e : seq R) (f : formula R) : holds (rcons e 0) f<-> holds e f. *)
(* Proof. *)
(* eq_holds *)
(* Qed. *)
(* Lemma holds_cat_zeros (e : seq R) (f : formula R) *)
Lemma holds_forall (i : nat) (e : seq R) (f : formula R) : holds e (Forall i f) -> holds e f.
Proof.
move/(_ (nth 0 e i)); apply: eq_holds.
rewrite /GRing.same_env.
apply: (ftrans (@nth_set_nth _ _ _ _ _)) => j /=.
have [-> | ] := eqVneq i j; rewrite ?eqxx // eq_sym.
by move/negbTE ->.
Qed.
Lemma forall_is_true (f : formula R) :
(forall (e : seq R), holds e f) ->
forall (i : nat) (e : seq R), holds e (Forall i f).
Proof. by move=> h i e /= x. Qed.
(* Fact and_sym (e : seq R) (f g : formula R) : holds e (f /\ g) <-> holds e (g /\ f). *)
(* Proof. *)
(* rewrite /=. *)
(* Qed. *)
(* Lemma quantify_and (e : seq R) (f g : formula R) *)
End Cad.