-
Notifications
You must be signed in to change notification settings - Fork 10
/
Complex.v
1556 lines (1327 loc) · 42.6 KB
/
Complex.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
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(**
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
---------------------------------------------------------------
This version modified to work without SSReflect,
or any other dependencies, as part of the QWIRE project
by Robert Rand and Jennifer Paykin (June 2017).
---------------------------------------------------------------
Additional lemmas added as part of work on projects in inQWIRE
(https://github.com/inQWIRE) 2019-2021.
*)
Require Export Prelim.
Require Export RealAux.
Require Export Summation.
(** This file defines complex numbers [C] as [R * R]. Operations are
given, and [C] is proved to be a field, a normed module, and a
complete space. *)
(** * The set of complex numbers *)
Definition C := (R * R)%type.
Declare Scope C_scope.
Delimit Scope C_scope with C.
Open Scope nat_scope.
Open Scope R_scope.
Open Scope C_scope.
Bind Scope nat_scope with nat.
Bind Scope R_scope with R.
Bind Scope C_scope with C.
Definition RtoC (x : R) : C := (x,0).
Coercion RtoC : R >-> C.
Lemma RtoC_inj : forall (x y : R),
RtoC x = RtoC y -> x = y.
Proof.
intros x y H.
now apply (f_equal (@fst R R)) in H.
Qed.
Lemma Ceq_dec (z1 z2 : C) : { z1 = z2 } + { z1 <> z2 }.
Proof.
destruct z1 as [x1 y1].
destruct z2 as [x2 y2].
destruct (Req_EM_T x1 x2) as [Eqx | Neqx]; [| right; congruence].
destruct (Req_EM_T y1 y2) as [Eqy | Neqy]; [subst; auto | right; congruence].
Qed.
(* lca, a great tactic for solving computations or basic equality checking *)
Lemma c_proj_eq : forall (c1 c2 : C), fst c1 = fst c2 -> snd c1 = snd c2 -> c1 = c2.
Proof. intros c1 c2 H1 H2. destruct c1, c2. simpl in *. subst. reflexivity. Qed.
(* essentially, we just bootsrap coq's lra *)
Ltac lca := eapply c_proj_eq; simpl; lra.
(** ** Constants and usual functions *)
(** 0 and 1 for complex are defined as [RtoC 0] and [RtoC 1] *)
Definition Ci : C := (0,1).
Notation C0 := (RtoC 0).
Notation C1 := (RtoC 1).
Notation C2 := (RtoC 2).
(** *** Arithmetic operations *)
Definition Cplus (x y : C) : C := (fst x + fst y, snd x + snd y).
Definition Copp (x : C) : C := (-fst x, -snd x).
Definition Cminus (x y : C) : C := Cplus x (Copp y).
Definition Cmult (x y : C) : C := (fst x * fst y - snd x * snd y, fst x * snd y + snd x * fst y).
Definition Cinv (x : C) : C := (fst x / (fst x ^ 2 + snd x ^ 2), - snd x / (fst x ^ 2 + snd x ^ 2)).
Definition Cdiv (x y : C) : C := Cmult x (Cinv y).
(* Added exponentiation *)
Fixpoint Cpow (c : C) (n : nat) : C :=
match n with
| 0%nat => 1
| S n' => Cmult c (Cpow c n')
end.
Infix "+" := Cplus : C_scope.
Notation "- x" := (Copp x) : C_scope.
Infix "-" := Cminus : C_scope.
Infix "*" := Cmult : C_scope.
Notation "/ x" := (Cinv x) : C_scope.
Infix "/" := Cdiv : C_scope.
Infix "^" := Cpow : C_scope.
(** * Showing that C is a field, and a vector space over itself *)
Global Program Instance C_is_monoid : Monoid C :=
{ Gzero := C0
; Gplus := Cplus
}.
Solve All Obligations with program_simpl; try lca.
Global Program Instance C_is_group : Group C :=
{ Gopp := Copp }.
Solve All Obligations with program_simpl; try lca.
Global Program Instance C_is_comm_group : Comm_Group C.
Solve All Obligations with program_simpl; lca.
Global Program Instance C_is_ring : Ring C :=
{ Gone := C1
; Gmult := Cmult
}.
Solve All Obligations with program_simpl; try lca; apply Ceq_dec.
Global Program Instance C_is_comm_ring : Comm_Ring C.
Solve All Obligations with program_simpl; lca.
Global Program Instance C_is_field : Field C :=
{ Ginv := Cinv }.
Next Obligation.
assert (H := R1_neq_R0).
contradict H.
apply (f_equal_gen fst fst) in H; simpl in H; easy.
Qed.
Next Obligation.
apply injective_projections ; simpl ; field;
contradict H; apply Rplus_sqr_eq_0 in H;
apply injective_projections ; simpl ; apply H.
Qed.
Global Program Instance C_is_module_space : Module_Space C C :=
{ Vscale := Cmult }.
Solve All Obligations with program_simpl; lca.
Global Program Instance C_is_vector_space : Vector_Space C C.
(** *** Other usual functions *)
Definition Re (z : C) : R := fst z.
Definition Im (z : C) : R := snd z.
Definition Cmod (x : C) : R := sqrt (fst x ^ 2 + snd x ^ 2).
Definition Cconj (x : C) : C := (fst x, (- snd x)%R).
Notation "a ^*" := (Cconj a) (at level 10) : C_scope.
Lemma Cmod_0 : Cmod 0 = R0.
Proof.
unfold Cmod.
simpl.
rewrite Rmult_0_l, Rplus_0_l.
apply sqrt_0.
Qed.
Lemma Cmod_1 : Cmod 1 = R1.
Proof.
unfold Cmod.
simpl.
rewrite Rmult_0_l, Rplus_0_r, 2!Rmult_1_l.
apply sqrt_1.
Qed.
Lemma Cmod_opp : forall x, Cmod (-x) = Cmod x.
Proof.
unfold Cmod.
simpl.
intros x.
apply f_equal.
ring.
Qed.
Lemma Cmod_triangle : forall x y, Cmod (x + y) <= Cmod x + Cmod y.
Proof.
intros x y ; unfold Cmod.
apply Rsqr_incr_0_var.
apply Rminus_le_0.
unfold Rsqr ; simpl ; ring_simplify.
unfold pow.
rewrite ?Rmult_1_r.
rewrite ?sqrt_sqrt ; ring_simplify.
replace (-2 * fst x * fst y - 2 * snd x * snd y)%R with (- (2 * (fst x * fst y + snd x * snd y)))%R by ring.
rewrite Rmult_assoc, <- sqrt_mult.
rewrite Rplus_comm.
apply -> Rminus_le_0.
apply Rmult_le_compat_l.
apply Rlt_le, Rlt_0_2.
apply Rsqr_incr_0_var.
apply Rminus_le_0.
unfold Rsqr; rewrite ?sqrt_sqrt ; ring_simplify.
replace (fst x ^ 2 * snd y ^ 2 - 2 * fst x * snd x * fst y * snd y +
snd x ^ 2 * fst y ^ 2)%R with ( (fst x * snd y - snd x * fst y)^2)%R
by ring.
apply pow2_ge_0.
repeat apply Rplus_le_le_0_compat ; apply Rmult_le_pos ; apply pow2_ge_0.
apply sqrt_pos.
apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
replace (fst x ^ 2 + 2 * fst x * fst y + fst y ^ 2 + snd x ^ 2 + 2 * snd x * snd y + snd y ^ 2)%R
with ((fst x + fst y)^2 + (snd x + snd y)^2)%R by ring.
apply Rplus_le_le_0_compat ; apply pow2_ge_0.
apply Rplus_le_le_0_compat ; apply pow2_ge_0.
apply Rplus_le_le_0_compat ; apply pow2_ge_0.
apply Rplus_le_le_0_compat ; apply sqrt_pos.
Qed.
Lemma Cmod_mult : forall x y, Cmod (x * y) = (Cmod x * Cmod y)%R.
Proof.
intros x y.
unfold Cmod.
rewrite <- sqrt_mult.
apply f_equal ; simpl ; ring.
apply Rplus_le_le_0_compat ; apply pow2_ge_0.
apply Rplus_le_le_0_compat ; apply pow2_ge_0.
Qed.
Lemma Rmax_Cmod : forall x,
Rmax (Rabs (fst x)) (Rabs (snd x)) <= Cmod x.
Proof.
intros [x y]; simpl.
rewrite <- !sqrt_Rsqr_abs.
apply Rmax_case ; apply sqrt_le_1_alt, Rminus_le_0 ;
unfold Rsqr; simpl ; ring_simplify ; try apply pow2_ge_0; auto.
Qed.
Lemma Cmod_2Rmax : forall x,
Cmod x <= sqrt 2 * Rmax (Rabs (fst x)) (Rabs (snd x)).
Proof.
intros [x y]; apply Rmax_case_strong; intros H0;
rewrite <- !sqrt_Rsqr_abs ;
rewrite <- ?sqrt_mult ;
try (apply Rle_0_sqr; auto);
try (apply Rlt_le, Rlt_0_2; auto) ;
apply sqrt_le_1_alt ; simpl ; [ rewrite Rplus_comm | ] ;
unfold Rsqr ; apply Rle_minus_r ; ring_simplify ;
apply Rsqr_le_abs_1 in H0 ; unfold pow; rewrite !Rmult_1_r; auto.
Qed.
Lemma C_neq_0 : forall c : C, c <> 0 -> (fst c) <> 0 \/ (snd c) <> 0.
Proof.
intros.
apply Classical_Prop.not_and_or.
rewrite <- pair_equal_spec.
unfold not in *.
replace ((fst c, snd c)) with c by apply surjective_pairing.
replace (0, 0)%C with (RtoC 0) by reflexivity.
assumption.
Qed.
(* some lemmas to help simplify addition/multiplication scenarios *)
Lemma Cplus_simplify : forall (a b c d : C),
a = b -> c = d -> (a + c = b + d)%C.
Proof. intros.
rewrite H, H0; easy.
Qed.
Lemma Cmult_simplify : forall (a b c d : C),
a = b -> c = d -> (a * c = b * d)%C.
Proof. intros.
rewrite H, H0; easy.
Qed.
(** ** C is a field *)
Lemma RtoC_plus (x y : R) : RtoC (x + y) = RtoC x + RtoC y.
Proof.
unfold RtoC, Cplus ; simpl.
rewrite Rplus_0_r; auto.
Qed.
Lemma RtoC_opp (x : R) : RtoC (- x) = - RtoC x.
Proof.
unfold RtoC, Copp ; simpl.
rewrite Ropp_0; auto.
Qed.
Lemma RtoC_minus (x y : R) : RtoC (x - y) = RtoC x - RtoC y.
Proof. unfold Cminus; rewrite <- RtoC_opp, <- RtoC_plus; auto. Qed.
Lemma RtoC_mult (x y : R) : RtoC (x * y) = RtoC x * RtoC y.
Proof.
unfold RtoC, Cmult ; simpl.
apply injective_projections ; simpl ; ring.
Qed.
Lemma RtoC_inv (x : R) : (x <> 0)%R -> RtoC (/ x) = / RtoC x.
Proof. intros Hx. apply injective_projections ; simpl ; field ; auto. Qed.
Lemma RtoC_div (x y : R) : (y <> 0)%R -> RtoC (x / y) = RtoC x / RtoC y.
Proof. intros Hy. apply injective_projections ; simpl ; field ; auto. Qed.
Lemma Cplus_comm (x y : C) : x + y = y + x.
Proof. apply injective_projections ; simpl ; apply Rplus_comm. Qed.
Lemma Cplus_assoc (x y z : C) : x + (y + z) = (x + y) + z.
Proof. apply injective_projections ; simpl ; apply sym_eq, Rplus_assoc. Qed.
Lemma Cplus_0_r (x : C) : x + 0 = x.
Proof. apply injective_projections ; simpl ; apply Rplus_0_r. Qed.
Lemma Cplus_0_l (x : C) : 0 + x = x.
Proof. apply injective_projections ; simpl ; apply Rplus_0_l. Qed.
Lemma Cplus_opp_r (x : C) : x + -x = 0.
Proof. apply injective_projections ; simpl ; apply Rplus_opp_r. Qed.
Lemma Copp_plus_distr (z1 z2 : C) : - (z1 + z2) = (- z1 + - z2).
Proof. apply injective_projections ; apply Ropp_plus_distr; auto. Qed.
Lemma Copp_minus_distr (z1 z2 : C) : - (z1 - z2) = z2 - z1.
Proof. apply injective_projections ; apply Ropp_minus_distr; auto. Qed.
Lemma Cmult_comm (x y : C) : x * y = y * x.
Proof. apply injective_projections ; simpl ; ring. Qed.
Lemma Cmult_assoc (x y z : C) : x * (y * z) = (x * y) * z.
Proof. apply injective_projections ; simpl ; ring. Qed.
Lemma Cmult_0_r (x : C) : x * 0 = 0.
Proof. apply injective_projections ; simpl ; ring. Qed.
Lemma Cmult_0_l (x : C) : 0 * x = 0.
Proof. apply injective_projections ; simpl ; ring. Qed.
Lemma Cmult_1_r (x : C) : x * 1 = x.
Proof. apply injective_projections ; simpl ; ring. Qed.
Lemma Cmult_1_l (x : C) : 1 * x = x.
Proof. apply injective_projections ; simpl ; ring. Qed.
Lemma Cinv_r (r : C) : r <> 0 -> r * /r = 1.
Proof.
intros H.
apply injective_projections ; simpl ; field.
contradict H.
apply Rplus_sqr_eq_0 in H.
apply injective_projections ; simpl ; apply H.
contradict H.
apply Rplus_sqr_eq_0 in H.
apply injective_projections ; simpl ; apply H.
Qed.
Lemma Cinv_l (r : C) : r <> 0 -> /r * r = 1.
Proof.
intros Zr.
rewrite Cmult_comm.
now apply Cinv_r.
Qed.
Lemma Cdiv_1_r : forall c, c / C1 = c.
Proof. intros. lca. Qed.
Lemma Cmult_plus_distr_l (x y z : C) : x * (y + z) = x * y + x * z.
Proof.
apply injective_projections ; simpl ; ring.
Qed.
Lemma Cmult_plus_distr_r (x y z : C) : (x + y) * z = x * z + y * z.
Proof.
apply injective_projections ; simpl ; ring.
Qed.
Lemma Copp_0 : Copp 0 = 0.
Proof. apply injective_projections; simpl ; ring. Qed.
Lemma Cmod_m1 : Cmod (Copp 1) = 1.
Proof. rewrite Cmod_opp. apply Cmod_1. Qed.
Lemma Cmod_eq_0 : forall x, Cmod x = 0 -> x = 0.
Proof.
intros x H.
unfold Cmod, pow in H.
rewrite 2!Rmult_1_r, <- sqrt_0 in H.
apply sqrt_inj in H.
apply Rplus_sqr_eq_0 in H.
now apply injective_projections.
apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
apply Rle_refl.
Qed.
Lemma Cmod_ge_0 : forall x, 0 <= Cmod x.
Proof.
intros x.
apply sqrt_pos.
Qed.
Lemma Cmod_gt_0 :
forall (x : C), x <> 0 <-> 0 < Cmod x.
Proof.
intros x ; split; intro Hx.
destruct (Cmod_ge_0 x); auto.
apply sym_eq, Cmod_eq_0 in H. tauto.
contradict Hx.
apply Rle_not_lt, Req_le.
rewrite Hx, Cmod_0; auto.
Qed.
Lemma Cmod_R : forall x : R, Cmod x = Rabs x.
Proof.
intros x.
unfold Cmod.
simpl.
rewrite Rmult_0_l, Rplus_0_r, Rmult_1_r.
apply sqrt_Rsqr_abs.
Qed.
Lemma Cmod_inv : forall x : C, x <> 0 -> Cmod (/ x) = Rinv (Cmod x).
Proof.
intros x Zx.
apply Rmult_eq_reg_l with (Cmod x).
rewrite <- Cmod_mult.
rewrite Rinv_r.
rewrite Cinv_r.
rewrite Cmod_R.
apply Rabs_R1.
exact Zx.
contradict Zx.
now apply Cmod_eq_0.
contradict Zx.
now apply Cmod_eq_0.
Qed.
Lemma Cmod_div (x y : C) : y <> 0 -> Cmod (x / y) = Rdiv (Cmod x) (Cmod y).
Proof.
intro Hy.
unfold Cdiv.
rewrite Cmod_mult.
rewrite Cmod_inv; auto.
Qed.
Lemma Cmod_real : forall (c : C),
fst c >= 0 -> snd c = 0 -> Cmod c = fst c.
Proof. intros.
unfold Cmod.
rewrite H0.
simpl.
autorewrite with R_db.
apply sqrt_square.
lra.
Qed.
Lemma Cmult_neq_0 (z1 z2 : C) : z1 <> 0 -> z2 <> 0 -> z1 * z2 <> 0.
Proof.
intros Hz1 Hz2 Hz.
assert (Cmod (z1 * z2) = 0).
rewrite Hz, Cmod_0; auto.
rewrite Cmod_mult in H.
apply Rmult_integral in H ; destruct H.
now apply Hz1, Cmod_eq_0.
now apply Hz2, Cmod_eq_0.
Qed.
Lemma Cmult_integral : forall c1 c2 : C, c1 * c2 = 0 -> c1 = 0 \/ c2 = 0.
Proof. intros.
destruct (Ceq_dec c1 0); try (left; easy).
destruct (Ceq_dec c2 0); try (right; easy).
apply (Cmult_neq_0 c1 c2) in n0; auto.
easy.
Qed.
Lemma Cminus_eq_contra : forall r1 r2 : C, r1 <> r2 -> r1 - r2 <> 0.
Proof.
intros ; contradict H ; apply injective_projections ;
apply Rminus_diag_uniq.
now apply (f_equal (@fst R R)) in H.
now apply (f_equal (@snd R R)) in H.
Qed.
Lemma Cminus_diag : forall r1 r2, r1 = r2 -> r1 - r2 = C0.
Proof. intros; subst; lca.
Qed.
Lemma Cminus_eq_0 : forall r1 r2 : C, r1 - r2 = C0 -> r1 = r2.
Proof. intros.
apply injective_projections;
apply Rminus_diag_uniq.
now apply (f_equal (@fst R R)) in H.
now apply (f_equal (@snd R R)) in H.
Qed.
Lemma Cmult_cancel_l : forall a c1 c2 : C,
a <> C0 ->
a * c1 = a * c2 -> c1 = c2.
Proof. intros.
apply (f_equal_gen (Cmult (/ a)) (Cmult (/ a))) in H0; auto.
do 2 rewrite Cmult_assoc in H0.
rewrite Cinv_l in H0; auto.
do 2 rewrite Cmult_1_l in H0.
easy.
Qed.
Lemma Cmult_cancel_r : forall a c1 c2 : C,
a <> C0 ->
c1 * a = c2 * a -> c1 = c2.
Proof. intros.
apply (Cmult_cancel_l a); auto.
rewrite Cmult_comm, H0; lca.
Qed.
Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.
Proof. apply (@G_field_theory C _ _ _ _ _ C_is_field). Qed.
Add Field C_field_field : C_field_theory.
(** * Content added as part of inQWIRE **)
Lemma Ci2 : Ci * Ci = -C1. Proof. lca. Qed.
Lemma Copp_mult_distr_r : forall c1 c2 : C, - (c1 * c2) = c1 * - c2.
Proof. intros; lca. Qed.
Lemma Copp_mult_distr_l : forall c1 c2 : C, - (c1 * c2) = - c1 * c2.
Proof. intros; lca. Qed.
Lemma Cplus_opp_l : forall c : C, - c + c = 0. Proof. intros; lca. Qed.
Lemma Cdouble : forall c : C, 2 * c = c + c. Proof. intros; lca. Qed.
Lemma Copp_involutive: forall c : C, - - c = c. Proof. intros; lca. Qed.
Lemma C0_imp : forall c : C, c <> 0 -> (fst c <> 0 \/ snd c <> 0)%R.
Proof. intros c H. destruct c. simpl.
destruct (Req_EM_T r 0), (Req_EM_T r0 0); subst; intuition. Qed.
Lemma C0_fst_neq : forall (c : C), fst c <> 0 -> c <> 0.
Proof. intros c. intros N E. apply N. rewrite E. reflexivity. Qed.
Lemma C0_snd_neq : forall (c : C), snd c <> 0 -> c <> 0.
Proof. intros c. intros N E. apply N. rewrite E. reflexivity. Qed.
Lemma RtoC_neq : forall (r : R), r <> 0 -> RtoC r <> 0.
Proof. intros. apply C0_fst_neq. easy. Qed.
(** Other useful facts *)
Lemma Copp_neq_0_compat: forall c : C, c <> 0 -> (- c)%C <> 0.
Proof.
intros c H.
apply C0_imp in H as [H | H].
apply C0_fst_neq.
apply Ropp_neq_0_compat.
assumption.
apply C0_snd_neq.
apply Ropp_neq_0_compat.
assumption.
Qed.
Lemma C1_neq_C0 : C1 <> C0.
Proof. apply C0_fst_neq.
simpl.
apply R1_neq_R0.
Qed.
Lemma Cconj_neq_0 : forall c : C, c <> 0 -> c^* <> 0.
Proof.
intros.
unfold Cconj.
apply C_neq_0 in H.
destruct H.
- apply C0_fst_neq.
simpl.
assumption.
- apply C0_snd_neq.
simpl.
apply Ropp_neq_0_compat.
assumption.
Qed.
Lemma nonzero_div_nonzero : forall c : C, c <> C0 -> / c <> C0.
Proof. intros.
unfold not; intros.
assert (H' : (c * (/ c) = c * C0)%C).
{ rewrite H0; easy. }
rewrite Cinv_r in H'; try easy.
rewrite Cmult_0_r in H'.
apply C1_neq_C0; easy.
Qed.
Lemma div_real : forall (c : C),
snd c = 0 -> snd (/ c) = 0.
Proof. intros.
unfold Cinv.
simpl.
rewrite H. lra.
Qed.
Lemma eq_neg_implies_0 : forall (c : C),
(-C1 * c)%C = c -> c = C0.
Proof. intros.
assert (H' : (- C1 * c + c = c + c)%C).
{ rewrite H; easy. }
assert (H'' : (- C1 * c + c = C0)%C).
{ lca. }
rewrite H'' in H'.
assert (H0 : (c + c = C2 * c)%C). lca.
rewrite H0 in H'.
destruct (Ceq_dec c C0); try easy.
assert (H1 : C2 <> C0).
apply C0_fst_neq.
simpl. lra.
assert (H2 : (C2 * c)%C <> C0).
apply Cmult_neq_0; try easy.
rewrite <- H' in H2. easy.
Qed.
Lemma Cinv_mult_distr : forall c1 c2 : C, c1 <> 0 -> c2 <> 0 -> / (c1 * c2) = / c1 * / c2.
Proof.
intros.
apply c_proj_eq.
- simpl.
repeat rewrite Rmult_1_r.
rewrite Rmult_div.
rewrite Rmult_div.
rewrite Rmult_opp_opp.
unfold Rminus.
rewrite <- Ropp_div.
rewrite <- Rdiv_plus_distr.
rewrite Rmult_plus_distr_r.
rewrite Rmult_plus_distr_l.
apply Rdiv_cancel.
lra.
* apply Rsum_nonzero. apply C0_imp in H. assumption.
* apply Rsum_nonzero. apply C0_imp in H0. assumption.
* apply Rsum_nonzero. apply C0_imp in H. assumption.
* apply Rsum_nonzero. apply C0_imp in H0. assumption.
- simpl.
repeat rewrite Rmult_1_r.
rewrite Rmult_div.
rewrite Rmult_div.
unfold Rminus.
rewrite <- Rdiv_plus_distr.
repeat rewrite Rmult_plus_distr_r.
repeat rewrite Rmult_plus_distr_l.
repeat rewrite <- Ropp_mult_distr_r.
repeat rewrite <- Ropp_mult_distr_l.
repeat rewrite <- Ropp_plus_distr.
apply Rdiv_cancel.
lra.
* apply Rsum_nonzero. apply C0_imp in H. assumption.
* apply Rsum_nonzero. apply C0_imp in H0. assumption.
* apply Rsum_nonzero. apply C0_imp in H. assumption.
* apply Rsum_nonzero. apply C0_imp in H0. assumption.
Qed.
Lemma Cinv_inv : forall c : C, c <> C0 -> / / c = c.
Proof. intros.
apply (Cmult_cancel_l (/ c)).
apply nonzero_div_nonzero; auto.
rewrite Cinv_l, Cinv_r; auto.
apply nonzero_div_nonzero; auto.
Qed.
Lemma Cconj_eq_implies_real : forall c : C, c = Cconj c -> snd c = 0%R.
Proof. intros.
unfold Cconj in H.
apply (f_equal snd) in H.
simpl in H.
assert (H' : (2 * snd c = 0)%R).
replace (2 * snd c)%R with (snd c + (- snd c))%R by lra.
lra.
replace (snd c) with (/2 * (2 * snd c))%R by lra.
rewrite H'; lra.
Qed.
(** * some C big_sum specific lemmas *)
Local Open Scope nat_scope.
(* TODO: these should all probably have better names *)
Lemma big_sum_rearrange : forall (n : nat) (f g : nat -> nat -> C),
(forall x y, x <= y -> f x y = (-C1) * (g (S y) x))%G ->
(forall x y, y <= x -> f (S x) y = (-C1) * (g y x))%G ->
big_sum (fun i => big_sum (fun j => f i j) n) (S n) =
(-C1 * (big_sum (fun i => big_sum (fun j => g i j) n) (S n)))%G.
Proof. induction n as [| n'].
- intros. lca.
- intros.
do 2 rewrite big_sum_extend_double.
rewrite (IHn' f g); try easy.
repeat rewrite Cmult_plus_distr_l.
repeat rewrite <- Cplus_assoc.
apply Cplus_simplify; try easy.
assert (H' : forall a b c, (a + (b + c) = (a + c) + b)%G).
intros. lca.
do 2 rewrite H'.
rewrite <- Cmult_plus_distr_l.
do 2 rewrite (@big_sum_extend_r C C_is_monoid).
do 2 rewrite (@big_sum_mult_l C _ _ _ C_is_ring).
rewrite Cplus_comm.
apply Cplus_simplify.
all : apply big_sum_eq_bounded; intros.
apply H; lia.
apply H0; lia.
Qed.
Local Close Scope nat_scope.
Lemma big_sum_ge_0 : forall f n, (forall x, 0 <= fst (f x)) -> (0 <= fst (big_sum f n))%R.
Proof.
intros f n H.
induction n.
- simpl. lra.
- simpl in *.
rewrite <- Rplus_0_r at 1.
apply Rplus_le_compat; easy.
Qed.
Lemma big_sum_gt_0 : forall f n, (forall x, 0 <= fst (f x)) ->
(exists y : nat, (y < n)%nat /\ 0 < fst (f y)) ->
0 < fst (big_sum f n).
Proof.
intros f n H [y [H0 H1]].
induction n.
- simpl. lia.
- simpl in *.
bdestruct (y <? n)%nat; bdestruct (y =? n)%nat; try lia.
+ assert (H' : 0 <= fst (f n)). { apply H. }
apply IHn in H2. lra.
+ apply (big_sum_ge_0 f n) in H.
rewrite H3 in H1.
lra.
Qed.
Lemma big_sum_member_le : forall (f : nat -> C) (n : nat), (forall x, 0 <= fst (f x)) ->
(forall x, (x < n)%nat -> fst (f x) <= fst (big_sum f n)).
Proof.
intros f.
induction n.
- intros H x Lt. inversion Lt.
- intros H x Lt.
bdestruct (Nat.ltb x n).
+ simpl.
rewrite <- Rplus_0_r at 1.
apply Rplus_le_compat.
apply IHn; easy.
apply H.
+ assert (E: x = n) by lia.
rewrite E.
simpl.
rewrite <- Rplus_0_l at 1.
apply Rplus_le_compat.
apply big_sum_ge_0; easy.
lra.
Qed.
Lemma big_sum_squeeze : forall (f : nat -> C) (n : nat),
(forall x, (0 <= fst (f x)))%R -> big_sum f n = C0 ->
(forall x, (x < n)%nat -> fst (f x) = fst C0).
Proof. intros.
assert (H2 : (forall x, (x < n)%nat -> (fst (f x) <= 0)%R)).
{ intros.
replace 0%R with (fst (C0)) by easy.
rewrite <- H0.
apply big_sum_member_le; try easy. }
assert (H3 : forall r : R, (r <= 0 -> 0 <= r -> r = 0)%R).
intros. lra.
simpl.
apply H3.
apply H2; easy.
apply H.
Qed.
Lemma big_sum_snd_0 : forall n f, (forall x, snd (f x) = 0) -> snd (big_sum f n) = 0.
Proof. intros. induction n.
- reflexivity.
- rewrite <- big_sum_extend_r.
unfold Cplus. simpl. rewrite H, IHn.
simpl; lra.
Qed.
Lemma Rsum_big_sum : forall n (f : nat -> R),
fst (big_sum (fun i => RtoC (f i)) n) = big_sum f n.
Proof.
intros. induction n.
- easy.
- simpl. rewrite IHn.
easy.
Qed.
Lemma big_sum_Cmod_0_all_0 : forall (f : nat -> C) (n : nat),
big_sum (fun i => Cmod (f i)) n = 0 ->
forall i, (i < n)%nat -> f i = C0.
Proof. induction n as [| n']; try nia.
intros; simpl in H.
assert (H' := H).
rewrite Rplus_comm in H; apply Rplus_eq_0_l in H.
apply Rplus_eq_0_l in H'.
all : try apply Rsum_ge_0; intros.
all : try apply Cmod_ge_0.
bdestruct (i <? n')%nat.
- apply IHn'; easy.
- bdestruct (i =? n')%nat; try lia; subst.
apply Cmod_eq_0; try easy.
Qed.
Lemma big_sum_triangle : forall f n,
Cmod (big_sum f n) <= big_sum (fun i => Cmod (f i)) n.
Proof. induction n as [| n'].
- simpl. rewrite Cmod_0; lra.
- simpl.
eapply Rle_trans; try apply Cmod_triangle.
apply Rplus_le_compat_r.
easy.
Qed.
(** * Lemmas about Cpow *)
Lemma RtoC_pow : forall r n, (RtoC r) ^ n = RtoC (r ^ n).
Proof.
intros.
induction n.
- reflexivity.
- simpl.
rewrite IHn.
rewrite RtoC_mult.
reflexivity.
Qed.
Lemma Cpow_nonzero_real : forall (r : R) (n : nat), (r <> 0 -> r ^ n <> C0)%C.
Proof.
intros.
rewrite RtoC_pow.
apply C0_fst_neq.
apply pow_nonzero.
lra.
Qed.
Lemma Cpow_nonzero : forall (c : C) (n : nat), (c <> C0 -> c ^ n <> C0)%C.
Proof.
intros.
induction n.
- simpl; apply C1_neq_C0.
- simpl.
apply Cmult_neq_0; easy.
Qed.
Lemma Cpow_add : forall (c : C) (n m : nat), (c ^ (n + m) = c^n * c^m)%C.
Proof.
intros. induction n. simpl. lca.
simpl. rewrite IHn. lca.
Qed.
Lemma Cpow_mult : forall (c : C) (n m : nat), (c ^ (n * m) = (c ^ n) ^ m)%C.
Proof.
intros. induction m. rewrite Nat.mul_0_r. easy.
replace (n * (S m))%nat with (n * m + n)%nat by lia.
simpl. rewrite Cpow_add. rewrite IHm. lca.
Qed.
Lemma Cpow_inv : forall (c : C) (n : nat), (forall n', (n' <= n)%nat -> c ^ n' <> 0) -> (/ c) ^ n = / (c ^ n).
Proof.
intros.
induction n.
- lca.
- simpl.
rewrite IHn; try assumption.
rewrite Cinv_mult_distr.
+ reflexivity.
+ assert (c ^ 1 <> 0).
{
apply H.
apply Nat.le_pred_le_succ.
simpl.
apply Nat.le_0_l.
}
simpl in H0.
rewrite Cmult_1_r in H0.
assumption.
+ apply H.
apply Nat.le_succ_diag_r.
+ intros.
apply H.
apply le_S.
assumption.
Qed.
Lemma Cpow_add_r : forall (c : C) (a b : nat), c ^ (a + b) = c ^ a * c ^ b.
Proof. induction a as [| a']; intros.
- lca.
- simpl; rewrite IHa'; lca.
Qed.
Lemma Cpow_mul_l : forall (c1 c2 : C) (n : nat), (c1 * c2) ^ n = c1 ^ n * c2 ^ n.
Proof. induction n as [| n']; intros.
- lca.
- simpl; rewrite IHn'; lca.
Qed.
Lemma Cmod_pow : forall x n, Cmod (x ^ n) = ((Cmod x) ^ n)%R.
Proof.
intros x n.
induction n; simpl.
apply Cmod_1.
rewrite Cmod_mult, IHn.
reflexivity.
Qed.
(** * Lemmas about Cmod *)
Lemma Cmod_Cconj : forall c : C, Cmod (c^*) = Cmod c.
Proof.
intro. unfold Cmod, Cconj. simpl.
replace (- snd c * (- snd c * 1))%R with (snd c * (snd c * 1))%R by lra.
easy.
Qed.
Lemma Cmod_real_pos :
forall x : C,
snd x = 0 ->
fst x >= 0 ->
x = Cmod x.
Proof.
intros.
unfold Cmod.
rewrite H.
replace (fst x ^ 2 + 0 ^ 2)%R with (fst x ^ 2)%R by lra.
rewrite sqrt_pow2 by lra.
destruct x; simpl in *.
rewrite H.
reflexivity.
Qed.
Lemma Cmod_sqr : forall c : C, (Cmod c ^2 = c^* * c)%C.
Proof.
intro.
rewrite RtoC_pow.
simpl.
rewrite Rmult_1_r.
rewrite <- Cmod_Cconj at 1.
rewrite <- Cmod_mult.
rewrite Cmod_real_pos; auto.
destruct c. simpl. lra.
destruct c. simpl. nra.
Qed.
Lemma Cmod_switch : forall (a b : C),
Cmod (a - b) = Cmod (b - a).
Proof. intros.
replace (b - a) with (- (a - b)) by lca.
rewrite Cmod_opp; easy.
Qed.
Lemma Cmod_triangle_le : forall (a b : C) (ϵ : R),
Cmod a + Cmod b < ϵ -> Cmod (a + b) < ϵ.
Proof. intros.
assert (H0 := Cmod_triangle a b).
lra.
Qed.
Lemma Cmod_triangle_diff : forall (a b c : C) (ϵ : R),
Cmod (c - b) + Cmod (b - a) < ϵ -> Cmod (c - a) < ϵ.
Proof. intros.
replace (c - a) with ((c - b) + (b - a)) by lca.
apply Cmod_triangle_le.
easy.
Qed.
(** * Lemmas about Cconj *)
Lemma Cconj_R : forall r : R, r^* = r. Proof. intros; lca. Qed.
Lemma Cconj_0 : 0^* = 0. Proof. lca. Qed.
Lemma Cconj_opp : forall C, (- C)^* = - (C^*). Proof. reflexivity. Qed.
Lemma Cconj_rad2 : (/ √2)^* = / √2. Proof. lca. Qed.
Lemma Cplus_div2 : /2 + /2 = 1. Proof. lca. Qed.
Lemma Cconj_involutive : forall c, (c^*)^* = c. Proof. intros; lca. Qed.
Lemma Cconj_plus_distr : forall (x y : C), (x + y)^* = x^* + y^*. Proof. intros; lca. Qed.
Lemma Cconj_mult_distr : forall (x y : C), (x * y)^* = x^* * y^*. Proof. intros; lca. Qed.
Lemma Cconj_minus_distr : forall (x y : C), (x - y)^* = x^* - y^*. Proof. intros; lca. Qed.
Lemma Cinv_Cconj : forall c : C, (/ (c ^*) = (/ c) ^*)%C.