forked from affeldt-aist/coq-robot
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ssr_ext.v
344 lines (268 loc) · 11.2 KB
/
ssr_ext.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
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
(* coq-robot (c) 2017 AIST and INRIA. License: LGPL v3. *)
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp
Require Import eqtype ssrnat seq choice fintype tuple finfun.
From mathcomp
Require Import bigop ssralg ssrnum ssrint div rat poly closed_field polyrcf.
From mathcomp
Require Import matrix mxalgebra tuple mxpoly zmodp binomial.
From mathcomp
Require Import perm finset path fingroup complex.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(*
OUTLINE:
1. Section extra_ssrbool
2. various lemmas about ssralg and ssrnum
3. section extra_perm3
4. Section extra_linear
notation 'e_i
5. Section extra_complex
*)
Section extra_ssrbool.
Lemma rew_condAr (a b c : bool) : a = b && c -> (b -> c = a).
Proof. by case: b. Qed.
Inductive and6 (P1 P2 P3 P4 P5 P6 : Prop) : Prop :=
And6 of P1 & P2 & P3 & P4 & P5 & P6.
Inductive and9 (P1 P2 P3 P4 P5 P6 P7 P8 P9 : Prop) : Prop :=
And9 of P1 & P2 & P3 & P4 & P5 & P6 & P7 & P8 & P9.
Notation "[ /\ P1 , P2 , P3 , P4 , P5 & P6 ]" := (and6 P1 P2 P3 P4 P5 P6) : type_scope.
Notation "[ /\ P1 , P2 , P3 , P4 , P5 , P6 , P7 , P8 & P9 ]" :=
(and9 P1 P2 P3 P4 P5 P6 P7 P8 P9) : type_scope.
Lemma and6P (b1 b2 b3 b4 b5 b6 : bool) :
reflect [/\ b1, b2, b3, b4, b5 & b6] [&& b1, b2, b3, b4, b5 & b6].
Proof.
by case b1; case b2; case b3; case b4; case b5; case b6; constructor; try by case.
Qed.
Lemma and9P (b1 b2 b3 b4 b5 b6 b7 b8 b9 : bool) :
reflect [/\ b1, b2, b3, b4, b5, b6, b7, b8 & b9]
[&& b1, b2, b3, b4, b5, b6, b7, b8 & b9].
Proof.
by case b1; case b2; case b3; case b4; case b5; case b6; case b7; case b8; case b9;
constructor; try by case.
Qed.
End extra_ssrbool.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Lemma ifnot01 (i : 'I_2) : (i != 0) = (i == 1).
Proof. by case: i => -[] // []. Qed.
Lemma ifnot01P (i : 'I_2) : (i != 0) <-> (i == 1).
Proof. by rewrite ifnot01. Qed.
Lemma thirdI3 (i j : 'I_3) : i != j -> exists k, (k != i) && (k != j).
Proof.
move=> neq_ij; exists (- i - j).
by case: i j neq_ij => -[i0|[i1|[i2|//]]] [[|[|[]]]].
Qed.
Lemma ifnot0 (i : 'I_3) : (i != 0) = (i == 1) || (i == 2%:R).
Proof. by move: i; do !case=>//. Qed.
Lemma ifnot0P (i : 'I_3) : (i != 0) <-> (i == 1) || (i == 2%:R).
Proof. by rewrite ifnot0. Qed.
Lemma ifnot1 (i : 'I_3) : (i != 1) = (i == 0) || (i == 2%:R).
Proof. by move: i; do !case=>//. Qed.
Lemma ifnot2 (i : 'I_3) : (i != 2%:R) = (i == 0) || (i == 1).
Proof. by move: i; do !case=>//. Qed.
Lemma Neqxx (R : numDomainType) (x : R) : (-x == x) = (x == 0).
Proof.
apply/idP/idP => [|/eqP ->]; last by rewrite oppr0.
by rewrite -subr_eq0 -opprD -mulr2n -mulNrn mulrn_eq0 /= eqr_oppLR oppr0.
Qed.
Lemma Neqxx_mat (R : numFieldType) n m (u : 'M[R]_(m, n)) :
(- u == u) = (u == 0).
Proof.
apply/idP/idP => [|/eqP ->]; last by rewrite oppr0.
by rewrite -subr_eq0 -opprD -mulr2n -scaler_nat oppr_eq0 scaler_eq0 pnatr_eq0.
Qed.
Lemma sqr_normr (R : realDomainType) (k : R) : `| k | ^+ 2 = k ^+ 2.
Proof. by rewrite real_normK ?num_real. Qed.
Lemma ler_norml1 (R : realDomainType) (x y : R) : `|x| <= y -> x <= y.
Proof. by rewrite ler_norml => /andP[]. Qed.
Lemma pnatf_unit (R : numFieldType) n : n.+1%:R \is a @GRing.unit R.
Proof. by rewrite unitfE pnatr_eq0. Qed.
Lemma lift0E m (i : 'I_m.+1) : fintype.lift ord0 i = i.+1%:R.
Proof. by apply/val_inj; rewrite Zp_nat /= modn_small // ltnS. Qed.
Module Simp.
Ltac ord :=
do ?[rewrite !lift0E
|rewrite ord1
|rewrite -[ord_max]natr_Zp /=
|rewrite -[widen_ord _ _]natr_Zp /=
|rewrite -[fintype.lift _ _]natr_Zp /=
|rewrite -[Ordinal _]natr_Zp /=
|rewrite -[_ + _ : 'I__]natr_Zp /=
|rewrite -[_ * _ : 'I__]natr_Zp /=
|rewrite -[- _ : 'I__]natr_Zp /=].
Ltac r := rewrite ?(Monoid.simpm,
mulr0,mul0r,mul1r,mulr1,addr0,add0r,
mulr1n,mulNr,mulrN,opprK,oppr0,
scale0r, scaler0, scaleN1r, scale1r,
eqxx).
End Simp.
Lemma liftE0 m (i : 'I_m.+2) : fintype.lift i ord0 = (i == 0)%:R.
Proof. by Simp.ord; rewrite -val_eqE /=; case: (val i). Qed.
Lemma liftE1 m (i : 'I_m.+3) : fintype.lift i 1 = (i <= 1).+1%:R.
Proof. by Simp.ord; case: (val i) => [|[]]. Qed.
(*Lemma sum1E_gen {T : ringType} (f : 'I_1 -> T) P : \sum_(i < 1 | P i) f i = (P ord0)%:R * f 0.
Proof.
case/boolP : (P ord0) => P0; rewrite ?(mul1r,mul0r).
by rewrite (bigD1 ord0) //= big1 ?addr0 // => i; rewrite (ord1 i) eqxx andbF.
by rewrite big1 // => /= i; rewrite (ord1 i) (negbTE P0).
Qed. *)
Lemma sum1E (T : ringType) (f : 'I_1 -> T) : \sum_(i < 1) f i = f 0.
Proof. by rewrite big_ord1. Qed.
Lemma sum2E (T : ringType) (f : 'I_2 -> T) : \sum_(i < 2) f i = f 0 + f 1.
Proof. by rewrite !(big_ord1, big_ord_recr) /=; Simp.ord. Qed.
Lemma sum3E (T : ringType) (f : 'I_3 -> T) : \sum_(i < 3) f i = f 0 + f 1 + f 2%:R.
Proof. by rewrite !(big_ord1, big_ord_recr) /=; Simp.ord. Qed.
Lemma sum4E (T : ringType) (f : 'I_4 -> T) : \sum_(i < 4) f i = f 0 + f 1 + f 2%:R + f 3%:R.
Proof. by rewrite !(big_ord1, big_ord_recr) /=; Simp.ord. Qed.
Lemma scaler_eq1 (F : fieldType) (R : lmodType F) (k : F) (a : R) :
a != 0 -> k *: a = a -> k = 1.
Proof.
move=> a0 /eqP; rewrite -{2}(scale1r a) -subr_eq0 -scalerBl.
by rewrite scaler_eq0 (negbTE a0) subr_eq0 orbF => /eqP.
Qed.
Lemma scaler_eqN1 (F : fieldType) (R : lmodType F) (k : F) (a : R) :
a != 0 -> - k *: a = a -> k = - 1.
Proof. by move=> a0 /scaler_eq1 => /(_ a0) /eqP; rewrite eqr_oppLR => /eqP. Qed.
Section extra_perm3.
Definition perm3_def (i j : 'I_3) : 'I_3 ^ 3 :=
[ffun x : 'I_3 => if i == j then x else
[fun z : 'I_3 => - (i + j) with 1 |-> i, 2%:R |-> j] x].
Fact perm3_subproof (i j : 'I_3) : injective (perm3_def i j).
Proof.
move=> x y; rewrite ?ffunE; have [//|neq_ij /=] := altP (i =P j).
move => hxy; apply/val_inj; move: x y i j hxy neq_ij.
by do 4![move=> [[|[|[|?]]] ?] //=].
Qed.
Definition perm3 i j : 'S_3 := perm (@perm3_subproof i j).
CoInductive I3_spec i j : bool -> bool -> 'I_3 -> Type :=
| I3Spec_i : I3_spec i j true false i
| I3Spec_j : I3_spec i j false true j
| I3Spec_k : I3_spec i j false false (- (i + j)).
Lemma I3P i j k : i != j -> I3_spec i j (i == k) (j == k) k.
Proof.
move=> neq_ij.
have -> : k = if i == k then i else if j == k then j else - (i + j).
by apply/val_inj; move: i j k neq_ij; do 3![case=> [[|[|[|?]]] ?]].
by move: i j k neq_ij; do 3![case=> [[|[|[|?]]] ?] //=]; constructor.
Qed.
Lemma odd_perm312 : perm3 1 2%:R = false :> bool.
Proof.
suff ->: perm3 1 2%:R = 1%g by rewrite odd_perm1.
by apply/permP=>-[[|[|[|//]]] ?]; apply/val_inj; rewrite ?permE ?ffunE.
Qed.
Lemma odd_perm310 : perm3 1 0 = true :> bool.
Proof.
suff -> : perm3 1 0 = tperm (0 : 'I__) 2%:R by rewrite odd_tperm.
by apply/permP=>-[[|[|[|//]]] ?]; apply/val_inj; rewrite ?permE ?ffunE.
Qed.
Lemma odd_perm302 : perm3 0 2%:R = true :> bool.
Proof.
suff -> : perm3 0 2%:R = tperm (0 : 'I__) 1%R by rewrite !odd_tperm /=.
by apply/permP=>-[[|[|[|//]]] ?]; apply/val_inj; rewrite ?permE ?ffunE.
Qed.
Lemma odd_perm321 : perm3 2%:R 1 = true :> bool.
Proof.
suff ->: perm3 2%:R 1 = tperm (1%R : 'I__) 2%:R by rewrite !odd_tperm /=.
by apply/permP=>-[[|[|[|//]]] ?]; apply/val_inj; rewrite ?permE ?ffunE.
Qed.
Lemma odd_perm301 : perm3 0 1 = false :> bool.
Proof.
suff -> : perm3 0 1 = (tperm (1 : 'I__) 2%:R * tperm (0 : 'I__) 1%:R)%g.
by rewrite odd_permM !odd_tperm /=.
by apply/permP => -[[|[|[|?]]] ?]; do !rewrite ?permE ?ffunE //=; Simp.ord.
Qed.
Lemma odd_perm320 : perm3 2%:R 0 = false :> bool.
Proof.
suff -> : perm3 2%:R 0 = (tperm (1 : 'I__) 1%:R * tperm (1 : 'I__) 2%:R)%g.
by rewrite odd_permM !odd_tperm /=.
by apply/permP => -[[|[|[|?]]] ?]; do !rewrite ?permE ?ffunE //=; Simp.ord.
Qed.
Definition odd_perm3 :=
(odd_perm301, odd_perm302, odd_perm310, odd_perm312, odd_perm320, odd_perm321).
End extra_perm3.
Reserved Notation "u '``_' i"
(at level 3, i at level 2, left associativity, format "u '``_' i").
Notation "u '``_' i" := (u (GRing.zero (Zp_zmodType O)) i) : ring_scope.
Notation "''e_' i" := (delta_mx 0 i)
(format "''e_' i", at level 3) : ring_scope.
Local Open Scope ring_scope.
Section extra_linear.
Lemma mxE_col_row (T : Type) n (M : 'M[T]_n) i j : M i j = (col j (row i M)) 0 0.
Proof. by rewrite !mxE. Qed.
Variable R : ringType.
Lemma row_mx_eq0 m n1 n2 (A1 : 'M[R]_(m, n1)) (A2 : 'M_(m, n2)) :
(row_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0).
Proof.
apply/eqP/andP; last by case=> /eqP -> /eqP ->; rewrite row_mx0.
by rewrite -row_mx0 => /eq_row_mx [-> ->].
Qed.
Lemma col_mx_eq0 m1 m2 n (A1 : 'M[R]_(m1, n)) (A2 : 'M_(m2, n)) :
(col_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0).
Proof.
by rewrite -) !trmx0 tr_col_mx row_mx_eq0.
Qed.
Lemma col_mx_row_mx m1 n1 (A : 'M[R]_(m1, n1)) n2 m2 :
col_mx (row_mx A (0 : 'M_(m1, n2))) (0 : 'M_(m2, n1 + n2)) = row_mx (col_mx A 0) 0.
Proof.
set a : 'M_(m2, _ + n2) := 0.
have -> : a = row_mx (0 : 'M_(m2, n1)) 0 by rewrite row_mx0.
by rewrite -block_mxEv block_mxEh col_mx0.
Qed.
Definition mx_lin1 n (M : 'M[R]_n) : {linear 'rV[R]_n -> 'rV[R]_n} :=
mulmxr_linear 1 M.
Definition lin1_mx' n (f : 'rV[R]_n -> 'rV[R]_n) : linear f ->
{M : {linear 'rV[R]_n -> 'rV[R]_n} & forall x, f x = M x}.
Proof.
move=> H.
have @g : {linear 'rV[R]_n -> 'rV[R]_n}.
exists f; exact: (GRing.Linear.class_of_axiom H).
by exists g.
Defined.
Lemma mulmx_trE n (v : 'rV[R]_n) i j : (v^T *m v) i j = v 0 i * v 0 j.
Proof.
by rewrite mxE (bigD1 ord0) //= big1 ?mxE ?addr0 // => i0; rewrite (ord1 i0).
Qed.
(* courtesy of GG *)
Lemma mxdirect_delta (F : fieldType) (T : finType) (n : nat) (P : pred T) f :
{in P & , injective f} ->
mxdirect (\sum_(i | P i) <<'e_(f i) : 'rV[F]_n>>)%MS.
Proof.
pose fP := image f P => Uf; have UfP: uniq fP by apply/dinjectiveP.
suffices /mxdirectP: mxdirect (\sum_i <<'e_i : 'rV[F]_n>>).
rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_filter.
by move/mxdirectP; rewrite mxdirect_addsE => /andP[].
apply/mxdirectP=> /=; transitivity (mxrank (1%:M : 'M[F]_n)).
apply/eqmx_rank; rewrite submx1 mx1_sum_delta summx_sub_sums // => i _.
by rewrite -(mul_delta_mx (0 : 'I_1)) genmxE submxMl.
rewrite mxrank1 -[LHS]card_ord -sum1_card.
by apply/eq_bigr=> i _; rewrite /= mxrank_gen mxrank_delta.
Qed.
End extra_linear.
Section extra_complex.
Variable R : rcfType.
Implicit Types x : R[i].
Implicit Types a b k : R.
Lemma opp_conjc a b : (- (a -i* b) = (- a +i* b))%C.
Proof. by apply/eqP; rewrite eq_complex /= opprK !eqxx. Qed.
Lemma Re_scale x k : k != 0 -> complex.Re (x / k%:C%C) = complex.Re x / k.
Proof.
move=> k0; case: x => a b /=.
rewrite expr0n /= addr0 mul0r -mulrN opprK mulr0 addr0.
by rewrite expr2 invrM // ?unitfE // (mulrA k) divff // mul1r.
Qed.
Lemma ReNiIm x : complex.Re (x * - 'i%C) = complex.Im x.
Proof. by case: x => a b; simpc. Qed.
Lemma complexZ1 a b k : ((k * a) +i* (k * b) = k%:C * (a +i* b))%C.
Proof. by simpc. Qed.
Lemma complexZ2 a b k : ((k * a) -i* (k * b) = k%:C * (a -i* b))%C.
Proof. by simpc. Qed.
Lemma ReZ x k : complex.Re (k%:C%C * x) = k * complex.Re x.
Proof. case: x => a b /=; by rewrite mul0r subr0. Qed.
Lemma ImZ x k : complex.Im ((k%:C)%C * x) = k * complex.Im x.
Proof. by case: x => a b /=; rewrite mul0r addr0. Qed.
Definition complexZ := (complexZ1, @complexZ2).
Lemma normci : `|'i| = 1 :> R[i].
Proof. by rewrite normc_def /= expr0n add0r expr1n sqrtr1. Qed.
End extra_complex.