-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSquareConvex.ec
160 lines (137 loc) · 5.79 KB
/
SquareConvex.ec
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
require import Distr.
require import List.
require import AllCore List Binomial.
require import Ring StdRing StdOrder StdBigop Discrete RealSeq RealSeries.
(*---*) import IterOp Bigint Bigreal Bigreal.BRA.
(*---*) import IntOrder RealOrder RField.
require import Finite.
require (*--*) FinType.
require import AllCore List Binomial.
require import Ring StdRing StdOrder StdBigop Discrete.
require import RealFun RealSeq RealSeries.
(*---*) import IterOp Bigint Bigreal Bigreal.BRA.
(*---*) import IntOrder RealOrder RField.
require import Finite.
require (*--*) FinType.
section.
op square (x : real) : real = x ^ 2.
(* basics *)
local lemma iji : forall d, 0%r <= d => d <= 1%r => d - 1%r <= 0%r.
move => d p1 p2. smt(). qed.
local lemma iyi : forall d a, d <= 0%r => a >= 0%r => d * a <= 0%r.
move => d p1 p2. smt(). qed.
local lemma sq_lemma1p : forall (a b : real), (a + b)^2 = a^2 + 2%r*a*b + b^2.
by smt(@Real). qed.
local lemma sq_lemma1m : forall (a b : real), (a - b)^2 = a^2 - 2%r*a*b + b^2.
by smt(@Real). qed.
local lemma sq_lemma2 : forall (a b : real), (a * b)^2 = a^2 * b^2.
by smt(@Real). qed.
local lemma sq_lemma5 : 1%r ^ 2 = 1%r.
by smt(@Real). qed.
local lemma sq_lemma6 : forall (a b c : real) , a - (b - c) = a - b + c.
smt(). qed.
local lemma sq_lemma7 : forall (a b c : real) , a + (b - c) = a + b - c.
by smt(). qed.
local lemma sq_lemma8 : forall (a b c : real), a * (b * c) = a * b * c.
by smt(). qed.
local lemma sq_lemma9 : forall (a b c : real) , a + (b + c) = a + b + c.
by smt(). qed.
local lemma sq_lemma10 : forall (a b c d : real), a * (b -c + d) = a*b -a*c + a *d .
by smt(). qed.
local lemma sq_lemma11 : forall (a : real), a * a = a^2.
by smt(@Real). qed.
local lemma sq_lemma3 : forall (a b c : real), (a - b) * c = a*c - b * c.
by smt(). qed.
local lemma sq_lemma3' : forall (c a b : real), c * (a - b) = a*c - b * c.
by smt(). qed.
local lemma sq_lemma4 : forall (a b c : real), (a + b) * c = a*c + b * c.
by smt(). qed.
local lemma sq_lemma4' : forall (a b c : real), c * (a + b) = a*c + b * c.
by smt(). qed.
local lemma sq_lemmapos : forall (a : real), a^2 >= 0%r.
smt(@Real). qed.
(* smt(@Real sq_lemma4' sq_lemma4 sq_lemma3 sq_lemma3' sq_lemma11 sq_lemma10 sq_lemma9 sq_lemma8 sq_lemma7 sq_lemma6 sq_lemma5 sq_lemma2 sq_lemma1p sq_lemma1m) *)
lemma square_convex : forall (a b : real), convex square a b.
move => a b.
simplify convex. move => d p1.
simplify square.
pose z := (1%r - d).
have : z <= 1%r.
smt().
move => zp.
have s1 : (d * a + z * b) ^ 2 = (d * a)^2
+ 2%r * (d * a) * (z * b) + (z * b)^2. smt(sq_lemma1p sq_lemma1m). rewrite s1.
have s2 : (d * a)^2 + 2%r * (d * a) * (z * b) + (z * b)^2
= d^2 * a^2 + 2%r * (d * a) * (z * b) + z^2 * b^2.
smt (sq_lemma2). rewrite s2.
have eqts : d ^ 2 * a ^ 2 + 2%r * (d * a) * (z * b)
+ z ^ 2 * b ^ 2 - d * a ^ 2 - z * b ^ 2 <= 0%r.
have ze : z = 1%r - d. smt(). rewrite ze.
rewrite (sq_lemma1m (1%r) d).
simplify.
rewrite (sq_lemma3 1%r d (b ^ 2)).
simplify.
rewrite (sq_lemma3 1%r d b). simplify.
rewrite sq_lemma5.
rewrite (sq_lemma4 (1%r - 2%r * d) (d^2) (b^2)). simplify.
rewrite (sq_lemma3' (2%r * (d * a)) b (d *b)).
rewrite (sq_lemma3 1%r ((2%r) * d) (b^2)).
simplify.
rewrite (sq_lemma6 ((d ^ 2) * a ^ 2 + (b * (2%r * (d * a))
- d * b * (2%r * (d * a))) + (b ^ 2 - 2%r * d * b ^ 2 + d ^ 2 * b ^ 2)
- d * a ^ 2) (b ^ 2) (d * b ^ 2)).
rewrite (sq_lemma7 (d ^ 2 * a ^ 2) (b * (2%r * (d * a)))
(d * b * (2%r * (d * a)))).
rewrite (sq_lemma8 2%r d a).
rewrite (sq_lemma8 (d*b) (2%r * d) a).
rewrite (sq_lemma8 (d*b) 2%r d).
rewrite (sq_lemma8 b (2%r * d) a).
rewrite (sq_lemma8 b 2%r d).
rewrite (sq_lemma9 (d ^ 2 * a ^ 2 + b * 2%r * d * a - d * b * 2%r * d * a)
(b ^ 2 - 2%r * d * b ^ 2) (d ^ 2 * b ^ 2)).
rewrite (sq_lemma7 (d ^ 2 * a ^ 2 + b * 2%r * d * a - d * b * 2%r * d * a)
(b ^ 2) (2%r * d * b ^ 2)).
have me : d ^ 2 * a ^ 2 + b * 2%r * d * a - d * b * 2%r * d * a
+ b ^ 2 - 2%r * d * b ^ 2 + d ^ 2 * b ^ 2 - d * a ^ 2 - b ^ 2
+ d * b ^ 2
= d ^ 2 * a ^ 2 + b * 2%r * d * a
- d * b * 2%r * d * a - 2%r * d * b ^ 2
+ d ^ 2 * b ^ 2 - d * a ^ 2 + d * b ^ 2.
smt (sq_lemma1p sq_lemma1m sq_lemma2 sq_lemma3 sq_lemma3'
sq_lemma4 sq_lemma4' sq_lemma5 sq_lemma6 sq_lemma7
sq_lemma8 sq_lemma9).
rewrite me.
have me2 : d ^ 2 * a ^ 2 + b * 2%r * d * a - d * b * 2%r * d * a
- 2%r * d * b ^ 2 +
d ^ 2 * b ^ 2 - d * a ^ 2 + d * b ^ 2
= d ^ 2 * a ^ 2 + b * 2%r * d * a - d * b * 2%r * d * a
- d * b ^ 2 + d ^ 2 * b ^ 2 - d * a ^ 2.
smt().
rewrite me2.
have me3 : d * (d - 1%r) * (a - b)^2 = d ^ 2 * a ^ 2
+ b * 2%r * d * a - d * b * 2%r * d * a - d * b ^ 2
+ d ^ 2 * b ^ 2 - d * a ^ 2.
rewrite (sq_lemma1m a b).
rewrite (sq_lemma3' d d 1%r).
rewrite (sq_lemma10 (d * d - 1%r * d) (a ^ 2) (2%r * a * b) (b ^ 2)). simplify.
rewrite (sq_lemma3 (d * d) d (a ^2)). rewrite (sq_lemma3 (d * d) d (b ^2)).
rewrite (sq_lemma3 (d * d) d (2%r * a * b)).
rewrite (sq_lemma11 d).
rewrite (sq_lemma6 (d ^ 2 * a ^ 2 - d * a ^ 2) (d ^ 2 * (2%r * a * b))
(d * (2%r * a * b))).
rewrite (sq_lemma7 (d ^ 2 * a ^ 2 - d * a ^ 2 - d ^ 2 * (2%r * a * b)
+ d * (2%r * a * b)) (d ^ 2 * b ^ 2) (d * b ^ 2)).
have : d ^ 2 * (2%r * a * b) = d * b * 2%r * d * a.
rewrite - (sq_lemma11 d). smt().
move => q. rewrite q.
have : d * (2%r * a * b) = b * 2%r * d * a. smt().
move => qq. rewrite qq. smt().
rewrite - me3.
have : d * (d - 1%r) * (a - b) ^ 2 = (d - 1%r) * (d * (a - b) ^ 2). smt().
move => wo. rewrite wo.
have ko : (d-1%r) <= 0%r. clear me me2 me3 wo ze s2 s1 zp. smt().
have ok : ((a - b) ^ 2) >= 0%r. smt(sq_lemmapos).
have okk : (d * (a - b) ^ 2) >= 0%r. smt().
smt(). smt().
qed.
end section.