-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathsemialgebraic.v
4207 lines (3788 loc) · 171 KB
/
semialgebraic.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
(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
(*****************************************************************************)
(* This file defines types {SAset F^n} for semi-algebraic sets and *)
(* {SAfun F^n -> F^m} for semi-algebraic functions, where F has a structure *)
(* of real closed field and n and m are natural numbers. *)
(* {SAset F^n} is constructed as a quotient of formulae and is equipped with *)
(* a structure of predType 'rV_n and choiceType. *)
(* Given F : rcfType and n : nat, we define: *)
(* SAset0 == the empty set *)
(* SAset1 x == the singleton containing x *)
(* SAsub s1 s2 == s1 is included in s2 *)
(* SAset_meet s1 s2 == the intersection of s1 and s2 *)
(* SAset_join s1 s2 == the union of s1 and s2 *)
(* SAset_top == the full set *)
(* SAset_sub s1 s2 == the difference s1 minus s2 *)
(* These operations equip {SAset F^n} with a structure of distributive *)
(* lattice with top, bottom and complement. *)
(* Given F : rcfType and n, m : nat, we define: *)
(* SAgraph f == the graph of f *)
(* SAimset f s == the image of s by f *)
(* SAabs == the absolute value as a semi-algebraic function *)
(* SAid == the identity of F^n as a semi-algebraic function *)
(* SAcomp f g == the composite of f and g *)
(* *)
(*****************************************************************************)
Require Import ZArith Init.
From HB Require Import structures.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
From mathcomp Require Import fintype div tuple finfun generic_quotient bigop.
From mathcomp Require Import finset perm ssralg ssrint poly polydiv ssrnum.
From mathcomp Require Import mxpoly binomial interval finalg complex zmodp.
From mathcomp Require Import mxpoly mpoly mxtens qe_rcf ordered_qelim realalg.
From mathcomp Require Import matrix finmap order finset classical_sets topology.
From mathcomp Require Import normedtype polyrcf polyorder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory Num.Theory Num.Def.
Import ord.
Import Order.Theory Order.Syntax.
Import numFieldTopology.Exports.
From SemiAlgebraic Require Import auxresults formula.
Local Open Scope type_scope.
Local Open Scope fset_scope.
Local Open Scope fmap_scope.
Local Open Scope quotient_scope.
Local Open Scope classical_set_scope.
Local Open Scope nat_scope.
Local Open Scope ring_scope.
Declare Scope sa_scope.
Delimit Scope sa_scope with SA.
Local Open Scope sa_scope.
Reserved Notation "{ 'SAset' F }"
(format "{ 'SAset' F }").
Reserved Notation "{ 'SAfun' T }"
(format "{ 'SAfun' T }").
Section Ngraph.
Variable (n : nat) (F : Type).
Definition ngraph (m : nat) (x : 'rV[F]_m) := [tuple x ord0 i | i < m].
Definition ngraph_tnth k (t : k.-tuple F) :
ngraph (\row_(i < k) (tnth t i)) = t.
Proof.
apply/val_inj; rewrite /= -map_tnth_enum; apply/eq_map => i.
by rewrite mxE.
Qed.
Definition ngraph_nth k (x : F) (t : k.-tuple F) :
ngraph (\row_(i < k) (nth x t i)) = t.
Proof.
rewrite -{2}[t]ngraph_tnth; congr ngraph; apply/rowP => i.
by rewrite !mxE -tnth_nth.
Qed.
Lemma nth_ngraph k x0 (t : 'rV[F]_k) (i : 'I_k) :
nth x0 (ngraph t) i = t ord0 i.
Proof. by rewrite -tnth_nth tnth_map tnth_ord_tuple. Qed.
Lemma ngraph_nil (t : 'rV[F]_0) : ngraph t = [tuple of nil].
Proof. by apply/eq_from_tnth => - []. Qed.
Fact size_ngraph (m : nat) (t : 'rV[F]_m) : size (ngraph t) = m.
Proof. by rewrite size_tuple. Qed.
Fact cat_ffunE (x0 : F) (m : nat) (t : 'rV[F]_m) (p : nat)
(u : 'rV[F]_p) (i : 'I_(m + p)) :
(row_mx t u) ord0 i
= if (i < m)%N then nth x0 (ngraph t) i else nth x0 (ngraph u) (i - m).
Proof.
by rewrite mxE; case: splitP => j ->; rewrite ?(addnC, addnK) nth_ngraph.
Qed.
Fact ngraph_cat (m : nat) (t : 'rV[F]_m) (p : nat) (u : 'rV[F]_p) :
ngraph (row_mx t u) = ngraph t ++ ngraph u :> seq F.
Proof.
case: m t => [|m] t.
by rewrite row_thin_mx ngraph_nil.
apply: (@eq_from_nth _ (t ord0 ord0)) => [|i].
by rewrite size_cat ?size_ngraph.
rewrite size_ngraph=> lt_i_mp; rewrite nth_cat.
have -> : i = nat_of_ord (Ordinal lt_i_mp) by [].
by rewrite nth_ngraph (cat_ffunE (t ord0 ord0)) size_ngraph.
Qed.
Lemma ngraph_bij k : bijective (@ngraph k).
Proof.
exists (fun (x : k.-tuple F) => (\row_(i < k) (tnth x i))) => x.
by apply/rowP => i; rewrite mxE tnth_mktuple.
by rewrite ngraph_tnth.
Qed.
Lemma take_ngraph m (x : 'rV[F]_(n + m)) :
take n (ngraph x) = ngraph (lsubmx x).
Proof.
move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}.
by rewrite ngraph_cat take_cat size_ngraph ltnn subnn take0 cats0.
Qed.
Lemma drop_ngraph m (x : 'rV[F]_(n + m)) :
drop n (ngraph x) = ngraph (rsubmx x).
Proof.
move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}.
by rewrite ngraph_cat drop_cat size_ngraph ltnn subnn drop0.
Qed.
End Ngraph.
Section Var_n.
Variable F : rcfType.
Variable n : nat.
(* We define a relation in formulae *)
Definition equivf (f g : formula F) :=
rcf_sat [::] (nquantify O n Forall ((f ==> g) /\ (g ==> f))).
Lemma equivf_refl : reflexive equivf.
Proof. by move=> f; apply/rcf_satP; apply: nforall_is_true => e /=. Qed.
Lemma equivf_sym : ssrbool.symmetric equivf.
Proof.
move=> f g; rewrite /equivf; move: [::] => e.
move: O => i; move: (f ==> g)%oT (g ==> f)%oT => f' g' {f} {g}.
move: i e; elim: n=> [i e | n' iHn' i e].
by rewrite !nquantify0; apply/rcf_satP/rcf_satP => [[fg gf] | [gf fg]]; split.
rewrite !nquantSout /=.
apply/rcf_satP/rcf_satP => /= [h x | h x];
move/(_ x)/rcf_satP : h => h; apply/rcf_satP.
+ by rewrite -iHn'.
+ by rewrite iHn'.
Qed.
Lemma equivf_trans : transitive equivf.
Proof.
move=> f g h; rewrite /equivf; move: [::] => e.
move: e O; elim: n => [|m ih] e i.
+ rewrite !nquantify0; move/rcf_satP => [h1 h2]; move/rcf_satP => [h3 h4].
apply/rcf_satP; split => [Hg | Hh].
- by apply: h3; apply: h1.
- by apply: h2; apply: h4.
+ rewrite !nquantSout.
move/rcf_satP => fg; move/rcf_satP => hf; apply/rcf_satP => x.
apply/rcf_satP; apply: ih; apply/rcf_satP.
- exact: fg.
- exact: hf.
Qed.
(* we show that equivf is an equivalence *)
Definition equivf_equiv := EquivRel equivf equivf_refl equivf_sym equivf_trans.
(* equiv_formula *)
Definition sub_equivf :=
(@sub_r _ _ {formula_n _} equivf_equiv).
Definition SAtype := {eq_quot sub_equivf}.
Definition SAtype_of of phant (F ^ n) := SAtype.
Identity Coercion id_type_of : SAtype_of >-> SAtype.
Local Notation "{ 'SAset' }" := (SAtype_of (Phant (F ^ n))).
Coercion SAtype_to_form (A : SAtype) : {formula_n _} := repr A.
(* we recover some structure for the quotient *)
HB.instance Definition SAset_quotType := Quotient.on SAtype.
HB.instance Definition Aset_eqType := Equality.on SAtype.
HB.instance Definition Aset_choiceType := Choice.on SAtype.
HB.instance Definition Aset_eqQuotType := EqQuotient.on SAtype.
HB.instance Definition Aset_of_quotType := Quotient.on {SAset}.
HB.instance Definition Aset_of_eqType := Equality.on {SAset}.
HB.instance Definition Aset_of_choiceType := Choice.on {SAset}.
HB.instance Definition Aset_of_eqQuotType := EqQuotient.on {SAset}.
End Var_n.
Notation "{ 'SAset' F }" := (SAtype_of (Phant F)) : type_scope.
Section Interpretation.
Variable F : rcfType. (* is also a realDomainType *)
Variable n : nat.
Definition interp := fun (f : {formula_n F}) =>
[pred v : 'rV[F]_n | rcf_sat (ngraph v) f].
Definition pred_of_SAset (s : {SAset F^n}) :
pred ('rV[F]_n) := interp (repr s).
Canonical SAsetPredType := PredType pred_of_SAset.
End Interpretation.
Section SemiAlgebraicSet.
Variable F : rcfType.
Variable n : nat.
Fact rcf_sat_tuple (t : n.-tuple F) (f : {formula_n F}) :
rcf_sat t f = ((\row_(i < n) (tnth t i)) \in
[pred y : 'rV[F]_n | rcf_sat (ngraph (\row_(i < n) (tnth t i))) f]).
Proof. by rewrite inE ngraph_tnth. Qed.
Fact holds_tuple (t : n.-tuple F) (s : {SAset F^n}) :
reflect (holds t s) ((\row_(i < n) (tnth t i)) \in s).
Proof.
apply: (iffP idP) => [h | ].
by apply/rcf_satP; rewrite rcf_sat_tuple.
by move/rcf_satP; rewrite rcf_sat_tuple.
Qed.
Lemma holds_equivf (t : n.-tuple F) (f g : {formula_n F}) :
sub_equivf f g -> holds t f -> holds t g.
Proof. by move/rcf_satP/nforallP; move/(_ t) => [h _]. Qed.
Lemma rcf_sat_equivf (t : n.-tuple F) (f g : {formula_n F}) :
sub_equivf f g -> rcf_sat t f = rcf_sat t g.
Proof.
move=> h; apply/rcf_satP/rcf_satP; apply: holds_equivf => //.
by rewrite /sub_equivf /= equivf_sym.
Qed.
Fact rcf_sat_repr_pi (t : n.-tuple F) (f : {formula_n F}) :
rcf_sat t (repr (\pi_{SAset F^n} f)) = rcf_sat t f.
Proof. by case: piP => ? /eqmodP /rcf_sat_equivf ->. Qed.
Fact holds_repr_pi (t : n.-tuple F) (f : {formula_n F}) :
holds t (repr (\pi_{SAset F^n} f)) <-> holds t f.
Proof. by split; apply: holds_equivf; rewrite /sub_equivf -eqmodE reprK. Qed.
Lemma equivf_exists (f g : {formula_n F}) (i : nat) :
equivf n f g -> (equivf n ('exists 'X_i, f) ('exists 'X_i, g))%oT.
Proof.
rewrite /equivf; move/rcf_satP/nforallP => h.
apply/rcf_satP/nforallP => u /=.
have [lt_in|leq_ni] := ltnP i n.
by split=> -[x hxf]; exists x; move: hxf;
move/(_ [tuple of (set_nth 0 u (Ordinal lt_in) x)]) : h;
rewrite cat0s /= => -[].
split=> -[x].
rewrite set_nth_over ?size_tuple // rcons_cat /=.
move/holds_take; rewrite take_size_cat ?size_tuple // => holds_ug.
exists 0; rewrite set_nth_nrcons ?size_tuple // rcons_nrcons -nseq_cat.
by apply/holds_cat_nseq; move: holds_ug; move/(_ u) : h => [].
move/holds_fsubst.
rewrite fsubst_id; last
by rewrite (contra (@in_fv_formulan _ _ _ _)) // -leqNgt.
move=> holds_uf; exists x; apply/holds_fsubst.
rewrite fsubst_id; last
by rewrite (contra (@in_fv_formulan _ _ _ _)) // -leqNgt.
by move: holds_uf; move/(_ u) : h; rewrite cat0s /=; move => [].
Qed.
Lemma pi_form (f : {formula_n F}) (x : 'rV[F]_n) :
(x \in \pi_{SAset F^n} f) = rcf_sat (ngraph x) f.
Proof. by rewrite inE; apply/rcf_satP/rcf_satP => ?; apply/holds_repr_pi. Qed.
Lemma SAsetP (s1 s2 : {SAset F^n}) : reflect (s1 =i s2) (s1 == s2).
Proof.
move: s1 s2; apply: quotW => f1; apply: quotW => f2.
apply: (iffP idP) => [/eqP <-|] //.
rewrite eqmodE /equivf => h; apply/rcf_satP/nforallP => u.
split; move/holds_repr_pi/holds_tuple; [rewrite h | rewrite -h];
by move/holds_tuple/holds_repr_pi.
Qed.
End SemiAlgebraicSet.
Section Comprehension.
Variables (F : rcfType) (n : nat) (f : formula F).
Definition SAset_comprehension := \pi_({SAset F^n}) (cut n f).
Lemma SAin_setP x : reflect (holds (ngraph x) f) (x \in SAset_comprehension).
Proof.
apply/(iffP (rcf_satP _ _)) => [/holds_repr_pi/holds_subst|hf].
by rewrite -{1}[ngraph x : seq _]cats0 subst_env_iota_catl ?size_ngraph.
apply/holds_repr_pi/holds_subst.
by rewrite -[ngraph x : seq _]cats0 subst_env_iota_catl ?size_ngraph.
Qed.
End Comprehension.
Notation "[ 'set' : T | f ]" := ((@SAset_comprehension _ _ (f)%oT) : T)
(at level 0, only parsing) : sa_scope.
Notation "[ 'set' | f ]" := (@SAset_comprehension _ _ (f)%oT)
(at level 0, f at level 99, format "[ 'set' | f ]") : sa_scope.
Section Ops.
Variables (F : rcfType) (n : nat).
Definition SAset_seq (r : seq 'rV[F]_n) : {SAset F^n} :=
[set | \big[Or/False]_(x <- r)
\big[And/True]_(i < n) ('X_i == (x ord0 i)%:T)%oT ].
Lemma inSAset_seq r x : x \in SAset_seq r = (x \in r).
Proof.
apply/SAin_setP/idP => [/holdsOr [y][+][_] /holdsAnd hy|xr].
congr in_mem; apply/rowP => i.
move: hy => /(_ i); rewrite mem_index_enum /= (nth_map i) ?size_enum_ord//.
by rewrite nth_ord_enum => ->.
apply/holdsOr; exists x; split=> //; split=> //.
apply/holdsAnd => i _ _ /=.
by rewrite (nth_map i) ?size_enum_ord// nth_ord_enum.
Qed.
Definition SAset0 : {SAset F^n} := SAset_seq [::].
Lemma inSAset0 (x : 'rV[F]_n) : x \in SAset0 = false.
Proof. by rewrite inSAset_seq. Qed.
Lemma inSAset1 (x y : 'rV[F]_n) : x \in SAset_seq [:: y] = (x == y).
Proof. by rewrite inSAset_seq in_cons in_nil orbF. Qed.
Definition SAsetT : {SAset F^n} := [set | True%oT ].
Lemma inSAsetT (x : 'rV[F]_n) : x \in SAsetT.
Proof. exact/SAin_setP. Qed.
Definition SAsetU (f g : {SAset F^n}) :=
\pi_({SAset F^n}) (formulan_or f g).
Lemma inSAsetU f g x : x \in SAsetU f g = (x \in f) || (x \in g).
Proof.
rewrite /SAsetU pi_form !inE.
by apply/rcf_satP/orP; (case=> [l|r]; [left|right]; apply/rcf_satP).
Qed.
Definition SAsetU1 x f := SAsetU (SAset_seq [:: x]) f.
Lemma inSAsetU1 x f y : y \in SAsetU1 x f = (y == x) || (y \in f).
Proof. by rewrite inSAsetU inSAset1. Qed.
Definition SAsetI (f g : {SAset F^n}) :=
\pi_({SAset F^n}) (formulan_and f g).
Lemma inSAsetI f g x : x \in SAsetI f g = (x \in f) && (x \in g).
Proof.
rewrite /SAsetI pi_form !inE.
by apply/rcf_satP/andP => [/=|] [l r]; split; apply/rcf_satP.
Qed.
Definition SAsetC (s : {SAset F^n}) := \pi_{SAset F^n} (formulan_not s).
Lemma inSAsetC f x : x \in SAsetC f = ~~ (x \in f).
Proof.
rewrite /SAsetC pi_form !inE.
apply/rcf_satP/negP => /= [hn /rcf_satP//|hn h].
by apply/hn/rcf_satP.
Qed.
Definition SAsetD (s1 s2 : {SAset F^n}) : {SAset F^n} :=
SAsetI s1 (SAsetC s2).
Lemma inSAsetD s1 s2 x : x \in SAsetD s1 s2 = (x \in s1) && ~~ (x \in s2).
Proof. by rewrite inSAsetI inSAsetC. Qed.
Definition SAsetD1 s x := SAsetD s (SAset_seq [:: x]).
Lemma inSAsetD1 s x y : y \in SAsetD1 s x = (y \in s) && (y != x).
Proof. by rewrite inSAsetD inSAset1. Qed.
Definition SAsetX m (s1 : {SAset F^n}) (s2 : {SAset F^m}) : {SAset F^(n + m)} :=
[set | s1 /\ subst_formula (iota n m) s2 ].
Lemma inSAsetX m (s1 : {SAset F^n}) (s2 : {SAset F^m}) (x : 'rV[F]_(n + m)) :
x \in SAsetX s1 s2 = (lsubmx x \in s1) && (rsubmx x \in s2).
Proof.
move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}.
apply/SAin_setP/andP => /= -[]; rewrite ngraph_cat.
move=> /holds_take + /holds_subst.
rewrite take_size_cat ?size_ngraph// subst_env_iota_catr ?size_ngraph//.
by split; apply/rcf_satP.
move=> ls rs; split.
by apply/holds_take; rewrite take_size_cat ?size_ngraph//; apply/rcf_satP.
apply/holds_subst; rewrite subst_env_iota_catr ?size_ngraph//.
exact/rcf_satP.
Qed.
Definition SAset_sub s1 s2 := SAsetD s1 s2 == SAset0.
Lemma SAset_subP s1 s2 : reflect {subset s1 <= s2} (SAset_sub s1 s2).
Proof.
apply/(iffP idP) => [/SAsetP|] s12; last first.
by apply/SAsetP => x; rewrite inSAsetD inSAset0; apply/negP => /andP[/s12 ->].
move=> x x1; apply/negP => /negP x2.
suff: x \in SAset0 by rewrite inSAset0.
by rewrite -s12 inSAsetD x1.
Qed.
Definition SAset_proper s1 s2 := SAset_sub s1 s2 && ~~ SAset_sub s2 s1.
End Ops.
Definition SAset_cast (F : rcfType) (n m : nat) (s : {SAset F^n}) : {SAset F^m} :=
[set | (\big[And/True]_(i <- iota n (m-n)) ('X_i == 0)) /\
nquantify m (n-m) Exists s].
Notation "[ 'set' x1 ; .. ; xn ]" :=
(SAset_seq (cons x1 .. (cons xn nil) .. )): sa_scope.
Notation "A :|: B" := (SAsetU A B) : sa_scope.
Notation "x |: A" := (SAsetU1 x A) : sa_scope.
Notation "A :&: B" := (SAsetI A B) : sa_scope.
Notation "~: A" := (SAsetC A) : sa_scope.
Notation "A :\: B" := (SAsetD A B) : sa_scope.
Notation "A :\ x" := (SAsetD1 A x) : sa_scope.
Notation "A :*: B" := (SAsetX A B) (at level 35) : sa_scope.
Notation "A :<=: B" := (SAset_sub A B) (at level 49) : sa_scope.
Notation "A :<: B" := (SAset_proper A B) (at level 49) : sa_scope.
Definition SAset_itv (F : rcfType) (I : interval F) :=
let 'Interval l u := I in
(match l with
| BSide false lb => [set | lb%:T <% 'X_0]
| BSide true lb => [set | lb%:T <=% 'X_0]
| BInfty false => SAset0 F 1
| BInfty true => SAsetT F 1
end) :&: (
match u with
| BSide false ub => [set | 'X_0 <=% ub%:T]
| BSide true ub => [set | 'X_0 <% ub%:T]
| BInfty false => SAsetT F 1
| BInfty true => SAset0 F 1
end).
Arguments SAset_itv : simpl never.
Lemma inSAset_itv (F : rcfType) (I : interval F) (x : 'rV[F]_1) :
(x \in SAset_itv I) = (x 0 0 \in I).
Proof.
rewrite in_itv; case: I => l u.
rewrite inSAsetI; congr andb.
case: l => [+ t|]; case=> /=; last first.
- exact/inSAset0.
- exact/inSAsetT.
- by apply/SAin_setP/idP => /=; rewrite enum_ordSl/=.
- by apply/SAin_setP/idP => /=; rewrite enum_ordSl/=.
case: u => [+ t|]; case=> /=; last first.
- exact/inSAsetT.
- exact/inSAset0.
- by apply/SAin_setP/idP => /=; rewrite enum_ordSl/=.
- by apply/SAin_setP/idP => /=; rewrite enum_ordSl/=.
Qed.
Definition SAset_pos (F : rcfType) : {SAset F^1} :=
SAset_itv `]0, +oo[%R.
Section SAsetTheory.
Variables (F : rcfType) (n : nat).
Implicit Types (A B C : {SAset F^n}) (x y z : 'rV[F]_n) (s t : seq 'rV[F]_n).
Lemma eqEsubset A B : (A == B) = (A :<=: B) && (B :<=: A).
Proof.
apply/SAsetP/andP => [AB|[] /SAset_subP AB /SAset_subP BA x].
by split; apply/SAset_subP => x; rewrite AB.
by apply/idP/idP => [/AB|/BA].
Qed.
Lemma subEproper A B : (A :<=: B) = (A == B) || (A :<: B).
Proof. by rewrite eqEsubset -andb_orr orbN andbT. Qed.
Lemma properEneq A B : (A :<: B) = (A != B) && (A :<=: B).
Proof. by rewrite andbC eqEsubset negb_and andb_orr [X in X || _]andbN. Qed.
(* lt_def does things the other way. Should we have a fixed convention? *)
Lemma properEneq' A B : (A :<: B) = (B != A) && (A :<=: B).
Proof. by rewrite properEneq eq_sym. Qed.
Lemma proper_neq A B : A :<: B -> A != B.
Proof. by rewrite properEneq; case/andP. Qed.
Lemma eqEproper A B : (A == B) = (A :<=: B) && ~~ (A :<: B).
Proof. by rewrite negb_and negbK andb_orr andbN eqEsubset. Qed.
Lemma sub0set A : SAset0 F n :<=: A.
Proof. by apply/SAset_subP => x; rewrite inSAset0. Qed.
Lemma subset0 A : (A :<=: SAset0 F n) = (A == SAset0 F n).
Proof. by rewrite eqEsubset sub0set andbT. Qed.
Lemma proper0 A : (SAset0 F n :<: A) = (A != SAset0 F n).
Proof. by rewrite properEneq sub0set andbT eq_sym. Qed.
Lemma set0Vmem A : (A = SAset0 F n) + {x | x \in A}.
Proof.
case/boolP: (A == SAset0 F n) => [/eqP|] A0; first by left.
right; move: A A0; apply: quotW => /= f; rewrite eqmodE /=.
move=> /rcf_satP/n_nforall_formula/nexistsP P.
apply: sigW; move: P => [x hx] /=; exists (\row_(i < n) x`_i).
rewrite inE ngraph_nth rcf_sat_repr_pi.
move/rcf_satP: hx; rewrite cat0s !simp_rcf_sat; case: rcf_sat => //=.
by rewrite implybF negbK big_nil => /rcf_satP/holds_subst.
Qed.
Lemma proper0P A : reflect (exists x, x \in A) (SAset0 F n :<: A).
Proof.
rewrite proper0; have [->|[x xA]] := set0Vmem A.
by rewrite eqxx/=; apply/Bool.ReflectF => -[x]; rewrite inSAset0.
suff ->: (A != SAset0 F n) by apply/Bool.ReflectT; exists x.
by apply/eqP => A0; rewrite A0 inSAset0 in xA.
Qed.
Lemma subsetT A : A :<=: SAsetT F n.
Proof. by apply/SAset_subP => x; rewrite inSAsetT. Qed.
Lemma subTset A : (SAsetT F n :<=: A) = (A == SAsetT F n).
Proof. by rewrite eqEsubset subsetT. Qed.
Lemma properT A : (A :<: SAsetT F n) = (A != SAsetT F n).
Proof. by rewrite properEneq subsetT andbT. Qed.
Lemma perm_SAset_seq s t :
perm_eq s t -> SAset_seq s = SAset_seq t.
Proof.
by move=> st; apply/eqP/SAsetP => x; rewrite !inSAset_seq (perm_mem st).
Qed.
Lemma SAset_nil : SAset_seq [::] = SAset0 F n.
Proof. by []. Qed.
Lemma SAset_cons x s : SAset_seq (x :: s) = x |: SAset_seq s.
Proof. by apply/eqP/SAsetP => y; rewrite inSAsetU1 !inSAset_seq in_cons. Qed.
Lemma SAset_cat s t : SAset_seq (s ++ t) = SAset_seq s :|: SAset_seq t.
Proof. by apply/eqP/SAsetP => y; rewrite inSAsetU !inSAset_seq mem_cat. Qed.
Lemma SAset_rev s : SAset_seq (rev s) = SAset_seq s.
Proof. exact/perm_SAset_seq/permPl/perm_rev. Qed.
Lemma SAset0U A : SAset0 F n :|: A = A.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetU inSAset0. Qed.
Lemma SAsetUC A B : A :|: B = B :|: A.
Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetU orbC. Qed.
Lemma SAsetUA A B C : A :|: (B :|: C) = A :|: B :|: C.
Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetU orbA. Qed.
Lemma SAsetU_comprehension (f g : formula F) :
[set| f] :|: [set| g] = [set| f \/ g] :> {SAset F^n}.
Proof.
apply/eqP/SAsetP => x; rewrite inSAsetU; apply/orP/SAin_setP => /=.
by case=> /SAin_setP xfg; [left|right].
by case=> xfg; [left|right]; apply/SAin_setP.
Qed.
HB.instance Definition _ :=
Monoid.isComLaw.Build {SAset F^n}
(SAset0 F n) (@SAsetU F n) SAsetUA SAsetUC SAset0U.
Lemma SAsetIC A B : A :&: B = B :&: A.
Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetI andbC. Qed.
Lemma SAsetIA A B C : A :&: (B :&: C) = A :&: B :&: C.
Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetI andbA. Qed.
Lemma SAsetI0 A :
A :&: SAset0 F n = SAset0 F n.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAset0 andbF. Qed.
Lemma SAsetTI A : SAsetT F n :&: A = A.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAsetT. Qed.
Lemma SAsetIT A : A :&: SAsetT F n = A.
Proof. by rewrite SAsetIC SAsetTI. Qed.
Lemma SAsetI_comprehension (f g : formula F) :
[set| f] :&: [set| g] = [set| f /\ g] :> {SAset F^n}.
Proof.
apply/eqP/SAsetP => x; rewrite inSAsetI; apply/andP/SAin_setP.
by move=> [] /SAin_setP xf /SAin_setP yf /=; split.
by move=> /= [] xf yf; split; apply/SAin_setP.
Qed.
HB.instance Definition _ :=
Monoid.isComLaw.Build {SAset F^n}
(SAsetT F n) (@SAsetI F n) SAsetIA SAsetIC SAsetTI.
Lemma SAsetCK A :
~: ~: A = A.
Proof. by apply/eqP/SAsetP => x; rewrite !inSAsetC negbK. Qed.
Lemma SAsetCU A B : ~: (A :|: B) = ~: A :&: ~: B.
Proof.
by apply/eqP/SAsetP => x; rewrite inSAsetI !inSAsetC inSAsetU negb_or.
Qed.
Lemma SAsetCI A B : ~: (A :&: B) = ~: A :|: ~: B.
Proof.
by apply/eqP/SAsetP => x; rewrite inSAsetU !inSAsetC inSAsetI negb_and.
Qed.
Lemma SAsetC_comprehension (f : formula F) :
~: [set | f] = [set | Not f] :> {SAset F^n}.
Proof.
apply/eqP/SAsetP => x; rewrite inSAsetC !inE.
apply/negP/SAin_setP => [fP|/nn_formula + /SAin_setP fP //].
by apply/nn_formula => fP'; apply/fP/SAin_setP.
Qed.
Lemma SAsubset_refl : reflexive (@SAset_sub F n).
Proof. by move=> A; apply/SAset_subP. Qed.
Lemma SAsubset_anti : antisymmetric (@SAset_sub F n).
Proof. by move=> A B /andP[] AB BA; apply/eqP; rewrite eqEsubset AB. Qed.
Lemma SAsubset_trans : transitive (@SAset_sub F n).
Proof.
by move=> A B C /SAset_subP BA /SAset_subP AC; apply/SAset_subP => x /BA /AC.
Qed.
Lemma SAsetIUr A B C : A :&: (B :|: C) = (A :&: B) :|: (A :&: C).
Proof.
by apply/eqP/SAsetP => x; rewrite inSAsetI !inSAsetU !inSAsetI andb_orr.
Qed.
Lemma SAsetIUl A B C : (A :|: B) :&: C = (A :&: C) :|: (B :&: C).
Proof. by rewrite ![_ :&: C]SAsetIC SAsetIUr. Qed.
Lemma SAsetUIr A B C : A :|: (B :&: C) = (A :|: B) :&: (A :|: C).
Proof.
by apply/eqP/SAsetP => x; rewrite inSAsetU !inSAsetI !inSAsetU orb_andr.
Qed.
Lemma SAsetDIr A B :
A :\: (A :&: B) = A :\: B.
Proof.
apply/eqP/SAsetP => x.
by rewrite !inSAsetI !inSAsetC inSAsetI negb_and andb_orr andbN.
Qed.
Lemma SAsubsetI A B C : A :<=: B :&: C = (A :<=: B) && (A :<=: C).
Proof.
apply/SAset_subP/andP => [ABC|[/SAset_subP AB]/SAset_subP AC x xA]; last first.
by rewrite inSAsetI (AB _ xA) (AC _ xA).
by split; apply/SAset_subP => x /ABC; rewrite inSAsetI => /andP[].
Qed.
Lemma SAsubsetIl A B : A :&: B :<=: A.
Proof. by apply/SAset_subP => x; rewrite inSAsetI => /andP[]. Qed.
Lemma SAsubsetIidl A B : (A :<=: A :&: B) = (A :<=: B).
Proof. by rewrite SAsubsetI SAsubset_refl. Qed.
Lemma SAsubsetEI A B : A :<=: B = (A :&: B == A).
Proof. by rewrite eqEsubset SAsubsetIl SAsubsetIidl. Qed.
Lemma SAsubsetED A B :
A :<=: B = (A :\: B == SAset0 F n).
Proof.
rewrite -subset0; apply/SAset_subP/SAset_subP => AB x.
by rewrite inSAsetD => /andP[] /AB + /negP.
move=> xA; apply/negP => /negP xB.
have /AB: x \in A :\: B by rewrite inSAsetD xA.
by rewrite inSAset0.
Qed.
Lemma SAsetI_idem : idempotent (@SAsetI F n).
Proof.
by move=> A; apply/eqP; rewrite eqEsubset SAsubsetIl SAsubsetIidl SAsubset_refl.
Qed.
Lemma SAsetKU A B : A :&: (B :|: A) = A.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAsetU orKb. Qed.
Lemma SAsetKU' B A : A :&: (A :|: B) = A.
Proof. by rewrite SAsetUC SAsetKU. Qed.
Lemma SAsetKI A B : A :|: (B :&: A) = A.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetU inSAsetI andKb. Qed.
Lemma SAsetKI' B A : A :|: (A :&: B) = A.
Proof. by rewrite SAsetIC SAsetKI. Qed.
Lemma SAsetICr A : A :&: ~: A = SAset0 F n.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAsetC andbN inSAset0. Qed.
Lemma SAset0I A : SAset0 F n :&: A = SAset0 F n.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetI inSAset0. Qed.
Lemma SAsetID0 A B : SAsetI B (SAsetD A B) = (SAset0 F n).
Proof. by rewrite /SAsetD [A :&: _]SAsetIC SAsetIA SAsetICr SAset0I. Qed.
Lemma SAsetUCr A : A :|: ~: A = SAsetT F n.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetU inSAsetC orbN inSAsetT. Qed.
Lemma SAsetUID A B : A :&: B :|: A :\: B = A.
Proof. by rewrite -SAsetIUr SAsetUCr SAsetIT. Qed.
Notation "\bigcap_( i <- r | P ) f" :=
(\big[@SAsetI _ _/SAsetT _ _]_(i <- r | P) f)
(at level 41, f at level 41, r, P at level 50).
Lemma inSAset_bigcap (I : Type) (r : seq I) (P : pred I)
(f : I -> {SAset F^n}) (x : 'rV[F]_n) :
(x \in \bigcap_(i <- r | P i) f i) = all (fun i => P i ==> (x \in f i)) r.
Proof.
elim: r => /= [|i r IHr]; first by rewrite big_nil inSAsetT.
by rewrite big_cons; case: (P i) => //; rewrite inSAsetI IHr.
Qed.
Notation "\bigcup_( i <- r | P ) f" :=
(\big[@SAsetU _ _/SAset0 _ _]_(i <- r | P) f)
(at level 41, f at level 41, r, P at level 50).
Lemma inSAset_bigcup (I : Type) (r : seq I) (P : pred I)
(f : I -> {SAset F^n}) (x : 'rV[F]_n) :
(x \in \bigcup_(i <- r | P i) f i) = has (fun i => P i && (x \in f i)) r.
Proof.
elim: r => /= [|i r IHr]; first by rewrite big_nil inSAset0.
by rewrite big_cons; case: (P i) => //; rewrite inSAsetU IHr.
Qed.
Lemma SAsetIbigcupr A (I : Type) (r : seq I) (P : pred I)
(f : I -> {SAset F^n}) :
A :&: \bigcup_(i <- r | P i) f i = \bigcup_(i <- r | P i) (A :&: f i).
Proof.
elim: r => [|i r IHr]; first by rewrite !big_nil SAsetI0.
by rewrite !big_cons; case: (P i) => //; rewrite SAsetIUr IHr.
Qed.
Lemma SAsetIbigcup (I J : Type) (r : seq I) (P : pred I) (f : I -> {SAset F^n})
(s : seq J) (Q : pred J) (g : J -> {SAset F^n}) :
(\bigcup_(i <- r | P i) f i) :&: (\bigcup_(j <- s | Q j) g j)
= \bigcup_(ij <- allpairs pair r s | P (fst ij) && Q (snd ij))
(f (fst ij) :&: g (snd ij)).
Proof.
elim: r => /= [|i r IHr]; first by rewrite !big_nil SAset0I.
rewrite big_cons big_cat/= big_map/=; case: (P i) => /=; last first.
by rewrite big_pred0_eq SAset0U.
by rewrite SAsetIUl -IHr SAsetIbigcupr.
Qed.
Lemma SAsetCbigcap (I : Type) (r : seq I) (P : pred I) (f : I -> {SAset F^n}) :
(~: \bigcap_(i <- r | P i) f i) = \bigcup_(i <- r | P i) ~: f i.
Proof.
apply/eqP/SAsetP => x; rewrite inSAsetC inSAset_bigcap inSAset_bigcup.
rewrite -has_predC; elim: r => [//|] i r IHr /=.
by rewrite negb_imply IHr inSAsetC.
Qed.
Lemma SAsetCbigcup (I : Type) (r : seq I) (P : pred I) (f : I -> {SAset F^n}) :
(~: \bigcup_(i <- r | P i) f i) = \bigcap_(i <- r | P i) ~: f i.
Proof.
rewrite -[RHS]SAsetCK SAsetCbigcap; congr (~: _).
by apply/eq_bigr => i _; rewrite SAsetCK.
Qed.
Lemma SAset0X (s : {SAset F^n}) :
SAset0 F 0 :*: s = SAset0 F n.
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetX !inSAset0. Qed.
Lemma SAsetX0 (s : {SAset F^n}) :
s :*: SAset0 F 0 = SAset0 F (n + 0).
Proof. by apply/eqP/SAsetP => x; rewrite inSAsetX !inSAset0 andbF. Qed.
Lemma rcf_sat_subst (e : seq F) (s : seq nat) (f : formula F) :
rcf_sat e (subst_formula s f) = rcf_sat (subst_env s e) f.
Proof. by apply/rcf_satP/rcf_satP => /holds_subst. Qed.
Lemma inSAset_pos (x : 'rV[F]_1) : x \in SAset_pos F = (0 < x ord0 ord0).
Proof. by rewrite inSAset_itv in_itv/= andbT. Qed.
Lemma SAset_cast_id m (A : {SAset F^m}) : SAset_cast m A = A.
Proof.
apply/eqP/SAsetP => x; apply/SAin_setP/rcf_satP => /= [[] _|hx];
rewrite subnn nquantify0//.
by split=> //; apply/holdsAnd.
Qed.
Lemma SAset_cast_le m k (A : {SAset F^m}) : (k <= m)%N ->
SAset_cast k A = [set | nquantify k (m - k) Exists A].
Proof.
rewrite -subn_eq0 => /eqP km; apply/eqP/SAsetP => x.
apply/Bool.eq_iff_eq_true.
rewrite [X in X <-> _](iff_sym (rwP (SAin_setP _ _))).
rewrite [X in _ <-> X](iff_sym (rwP (SAin_setP _ _))).
rewrite km big_nil/=.
by split=> // -[].
Qed.
Lemma SAset_cast_ge m k (A : {SAset F^m}) : (m <= k)%N ->
SAset_cast k A
= [set | A /\ \big[And/True]_(i <- iota m (k - m)) ('X_i == 0)].
Proof.
rewrite -subn_eq0 => /eqP km; apply/eqP/SAsetP => x.
apply/Bool.eq_iff_eq_true.
rewrite [X in X <-> _](iff_sym (rwP (SAin_setP _ _))).
rewrite [X in _ <-> X](iff_sym (rwP (SAin_setP _ _))).
rewrite km nquantify0/=.
by split=> -[].
Qed.
Lemma inSAset_cast m (s : {SAset F^n}) (x : 'rV[F]_m) (mn : m = n) :
x \in SAset_cast m s = (castmx (erefl, mn) x \in s).
Proof.
by move: x (mn); rewrite mn => x nn; rewrite SAset_cast_id castmx_id.
Qed.
Lemma inSAset_castDn m k (A : {SAset F^(m+k)}) (x : 'rV[F]_m) :
reflect (exists y : 'rV[F]_(m+k), y \in A /\ x = lsubmx y)
(x \in SAset_cast m A).
Proof.
rewrite SAset_cast_le ?leq_addr// subDnCA// subnn addn0.
rewrite -[X in nquantify X](size_ngraph x).
apply/(iffP (SAin_setP _ _)) => [/nexistsP [y] hxy|[y][yA]->].
exists (row_mx x (\row_i tnth y i)); rewrite row_mxKl; split=> //.
by apply/rcf_satP; rewrite ngraph_cat ngraph_tnth.
apply/nexistsP; exists (ngraph (rsubmx y)); rewrite -ngraph_cat hsubmxK.
exact/rcf_satP.
Qed.
Lemma inSAset_castnD m k (A : {SAset F^m}) (x : 'rV[F]_(m+k)) :
x \in SAset_cast (m+k) A = (lsubmx x \in A) && (rsubmx x == 0).
Proof.
rewrite SAset_cast_ge ?leq_addr//.
apply/SAin_setP/andP => /=;
rewrite -holds_take take_ngraph holdsAnd /= => -[/rcf_satP hx].
move=> h0; split=> //; apply/eqP/rowP => i.
move/(_ (@unsplit m k (inr i))): h0.
rewrite nth_ngraph mem_iota subnKC ?leq_addr//= -addnS leq_add//.
move=> /(_ Logic.eq_refl Logic.eq_refl).
by rewrite !mxE.
move=> /eqP /rowP x0; split=> // => i.
rewrite mem_iota subnKC ?leq_addr// => /andP[mi im] _.
rewrite (nth_ngraph _ _ (Ordinal im)) -(splitK (Ordinal im)).
move: mi; rewrite leqNgt -{1}[i%N]/(Ordinal im : nat).
case: splitP => // j _ _.
by move: (x0 j); rewrite !mxE.
Qed.
Lemma SAset_cast_trans k m A : (minn n k <= m)%N ->
SAset_cast k (SAset_cast m A) = SAset_cast k A.
Proof.
case: (ltnP m n) => [mn|nm _]; last first.
case/orP: (leq_total m k) => [mk|km].
rewrite -(subnKC mk) -(subnKC nm) [X in (k-X)%N]subnKC//.
apply/eqP/SAsetP => x.
rewrite 2!inSAset_castnD.
move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}.
move: (lsubmx l) (rsubmx l) (hsubmxK l) => ll lr <- {l}.
rewrite SAset_cast_ge; last by rewrite subnKC// subnKC// (leq_trans nm mk).
apply/andP/SAin_setP => /=;
rewrite holdsAnd -holds_take -(take_takel _ (@leq_addr (m-n) n)%N);
rewrite !take_ngraph !row_mxKl (rwP (rcf_satP _ _));
rewrite subDnCA ?leq_addr// subDnCA// subnn addn0 addnC.
move=> [] /andP[] llA /eqP -> /eqP ->; split=> //= i.
rewrite mem_iota addnA => /andP[+ ilt] _.
rewrite -[i%N]/(Ordinal ilt : nat) nth_ngraph mxE.
case: (splitP (Ordinal ilt)) => j ->; rewrite mxE//.
by case: (splitP j) => j' ->; rewrite leqNgt ?ltn_ord// mxE.
move=> [llA /= h0]; split; last first.
apply/eqP/rowP => i.
move/(_ (unsplit (inr i) : 'I_(n + (m - n) + (k - m))%N)): h0.
rewrite nth_ngraph !mxE unsplitK.
by rewrite mem_iota addnA ltn_ord/= -addnA leq_addr; apply.
apply/andP; split=> //.
apply/eqP/rowP => i; move: h0.
move=> /(_ (unsplit (inl (unsplit (inr i))) :
'I_(n + (m - n) + (k - m))%N)).
rewrite nth_ngraph !mxE unsplitK mxE unsplitK.
by rewrite mem_iota addnA ltn_ord/= leq_addr; apply.
case/orP: (leq_total n k) => [nk|kn].
rewrite -(subnKC km) -(subnKC nk) [X in (m-X)%N]subnKC//.
apply/eqP/SAsetP => x.
rewrite inSAset_castnD.
move: (lsubmx x) (rsubmx x) (hsubmxK x) => l r <- {x}.
apply/inSAset_castDn/andP => [[y]|[lA] /eqP ->];
rewrite SAset_cast_ge -?addnA ?leq_addr//.
move: (lsubmx y) (rsubmx y) (hsubmxK y).
move=> yl yr <- {y} [] /[swap] <- {yl} /SAin_setP/= [] /holds_take.
rewrite -(take_takel _ (@leq_addr (k - n)%N n)) !take_ngraph !row_mxKl.
move=> /rcf_satP lA /holdsAnd.
rewrite subDnCA ?leq_addr// subDnCA// subnn addn0 addnC /= => h0.
split=> //; apply/eqP/rowP => i; move: h0.
move=> /(_ (unsplit (inl (unsplit (inr i))) :
'I_(n + (k - n) + (m - k))%N)).
rewrite nth_ngraph !mxE unsplitK mxE unsplitK mem_iota addnA ltn_ord/=.
by rewrite leq_addr; apply.
exists (row_mx (row_mx l 0) 0); rewrite row_mxKl; split=> //.
apply/SAin_setP => /=; split.
apply/holds_take.
rewrite -(take_takel _ (@leq_addr (k - n)%N n)) !take_ngraph !row_mxKl.
exact/rcf_satP.
apply/holdsAnd => i; rewrite mem_iota subDnCA ?leq_addr// subDnCA// subnn.
rewrite addn0 [X in (n + X)%N]addnC /= addnA => /andP[+ ilt] _.
rewrite -[i%N]/(Ordinal ilt : nat) nth_ngraph mxE.
case: (splitP (Ordinal ilt)) => j ->; rewrite mxE//.
by case: (splitP j) => j' ->; rewrite leqNgt ?ltn_ord// mxE.
move: A; rewrite -(subnKC nm) -(subnKC kn) [X in (m - X)%N]subnKC// -addnA.
move=> A.
apply/eqP/SAsetP => x; apply/inSAset_castDn/inSAset_castDn => -[y].
rewrite [_ _ A]SAset_cast_ge ?addnA ?leq_addr//.
move=> -[] /SAin_setP /= [] /holds_take + _.
rewrite takeD take_ngraph drop_ngraph take_ngraph -ngraph_cat => yA -> {x}.
exists (row_mx (lsubmx y) (lsubmx (rsubmx y))); split; first exact/rcf_satP.
by rewrite row_mxKl.
move=> [] /rcf_satP yA -> {x}.
exists (row_mx (lsubmx y) (row_mx (rsubmx y) 0)).
split; last by rewrite row_mxKl.
rewrite [_ _ A]SAset_cast_ge ?addnA ?leq_addr//; apply/SAin_setP => /=; split.
apply/holds_take.
rewrite takeD take_ngraph drop_ngraph take_ngraph -ngraph_cat row_mxKr.
by rewrite !row_mxKl hsubmxK.
apply/holdsAnd => i; rewrite {1}addnA subnKC// subnKC// mem_iota.
rewrite -{1 2}(subnKC kn) -addnA => /andP[] + ilt _ /=.
rewrite -[i%N]/(Ordinal ilt : nat) nth_ngraph.
rewrite mxE; case: splitP => j ->.
by rewrite leqNgt (leq_trans (ltn_ord j) (leq_addr _ _)).
rewrite leq_add2l mxE; case: splitP => j' ->; last by rewrite mxE.
by rewrite leqNgt ltn_ord.
rewrite geq_min leqNgt mn/= => km.
rewrite SAset_cast_le// SAset_cast_le ?(ltnW mn)//.
rewrite SAset_cast_le ?(ltnW (leq_ltn_trans km mn))//.
apply/eqP/SAsetP => x; rewrite -[X in nquantify X](size_ngraph x).
apply/SAin_setP/SAin_setP => /nexistsP [y] => /rcf_satP.
rewrite -[in X in rcf_sat _ X](subnKC km).
rewrite -[y]ngraph_tnth -ngraph_cat => /SAin_setP.
have mE: (k + (m - k))%N = size (ngraph x ++ y).
by rewrite size_cat size_ngraph size_tuple subnKC.
rewrite [X in nquantify X]mE -{2}[y]ngraph_tnth -ngraph_cat.
move=> /nexistsP [] {mE}.
rewrite ngraph_cat (subnKC km) ngraph_tnth => z hA.
apply/nexistsP.
have ->: (n - k)%N = (n - m + m - k)%N by rewrite subnK// (ltnW mn).
have /eqP scat: size (y ++ z) = (n - m + m - k)%N.
by rewrite size_cat !size_tuple addnC addnBA.
by exists (Tuple scat) => /=; rewrite catA.
move=> /rcf_satP hy; apply/nexistsP.
have /eqP ts: size (take (m - k)%N y) = (m - k)%N.
by rewrite size_takel// size_tuple leq_sub// ltnW.
exists (Tuple ts); rewrite -[in X in holds _ X](subnKC km).
rewrite -[Tuple ts]ngraph_tnth -ngraph_cat.
apply/rcf_satP/SAin_setP.
have mE: (k + (m - k))%N = size (ngraph x ++ Tuple ts).
by rewrite size_cat size_ngraph size_tuple subnKC.
rewrite [X in nquantify X]mE -{2}[Tuple ts]ngraph_tnth -ngraph_cat.
apply/nexistsP.
rewrite ngraph_cat subnKC//.
have /eqP ds: size (drop (m - k)%N y) = (n - m)%N.
rewrite size_drop size_tuple subnBA// addnC subnKC//.
exact/(ltnW (leq_ltn_trans km mn)).
by exists (Tuple ds); rewrite -catA ngraph_tnth/= cat_take_drop.
Qed.
End SAsetTheory.
Section SAsetTheory.
Variables (F : rcfType) (n : nat).
Implicit Types (A B C : {SAset F^n}) (x y z : 'rV[F]_n) (s t : seq 'rV[F]_n).
Lemma SAset_castXl m (s : {SAset F^n}) (t : {SAset F^m}) :
t != SAset0 F m -> SAset_cast n (s :*: t) = s.
Proof.
have [->|[] x0 xt _] := set0Vmem t; first by rewrite eqxx.
apply/eqP/SAsetP => x.
apply/inSAset_castDn/idP => [[y [+ ->]]|xs].
by rewrite inSAsetX => /andP[+ _].
by exists (row_mx x x0); rewrite inSAsetX row_mxKl row_mxKr xs.
Qed.
Definition SAset_disjoint (s1 s2 : {SAset F^n}) :=
s1 :&: s2 == SAset0 F n.
Lemma SAset_disjointC (s1 s2 : {SAset F^n}) :
SAset_disjoint s1 s2 = SAset_disjoint s2 s1.
Proof. by rewrite /SAset_disjoint SAsetIC. Qed.
Definition SAset_trivI (I : {fset {SAset F^n}}) :=