diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/Make.test-suite | 2 | ||||
| -rw-r--r-- | mathcomp/Makefile.common | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 6 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 14 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 20 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 31 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 51 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 38 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 6 |
12 files changed, 175 insertions, 16 deletions
diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite index 2be741b..0b51909 100644 --- a/mathcomp/Make.test-suite +++ b/mathcomp/Make.test-suite @@ -1,4 +1,4 @@ -test_suite/hierarchy_test.v +test_suite/test_hierarchy_all.v test_suite/test_ssrAC.v test_suite/test_guard.v diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 857ddef..b6b71ea 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -56,11 +56,10 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile # Test suite --------------------------------------------------------- -test_suite/hierarchy_test.v: build - mkdir -p test_suite - COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/hierarchy_test.v +test_suite/test_hierarchy_all.v: build + COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/test_hierarchy_all.v -Makefile.test-suite.coq: test_suite/hierarchy_test.v +Makefile.test-suite.coq: test_suite/test_hierarchy_all.v $(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq # Global config, build, clean and distclean -------------------------- @@ -128,6 +127,9 @@ endif %.vo: __always__ Makefile.coq +$(COQMAKE) $@ +test_suite/%.vo: __always__ Makefile.test-suite.coq + +$(COQMAKE_TESTSUITE) $@ + doc: __always__ Makefile.coq mkdir -p _build_doc/ cp -r $(COQFILES) -t _build_doc/ --parents diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 2bde8dd..9a3c7d7 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -835,6 +835,9 @@ Qed. Lemma mulrnAC x m n : x *+ m *+ n = x *+ n *+ m. Proof. by rewrite -!mulrnA mulnC. Qed. +Lemma iter_addr_0 n (m : V) : iter n (+%R m) 0 = m *+ n. +Proof. by elim: n => //= n ->; rewrite mulrS. Qed. + Lemma sumrN I r P (F : I -> V) : (\sum_(i <- r | P i) - F i = - (\sum_(i <- r | P i) F i)). Proof. by rewrite (big_morph _ opprD oppr0). Qed. @@ -856,6 +859,9 @@ Lemma sumr_const (I : finType) (A : pred I) (x : V) : \sum_(i in A) x = x *+ #|A|. Proof. by rewrite big_const -iteropE. Qed. +Lemma sumr_const_nat (m n : nat) (x : V) : \sum_(n <= i < m) x = x *+ (m - n). +Proof. by rewrite big_const_nat iter_addr_0. Qed. + Lemma telescope_sumr n m (f : nat -> V) : n <= m -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n. Proof. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 6198b44..45cd336 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2016,6 +2016,11 @@ Lemma ler_sum I (r : seq I) (P : pred I) (F G : I -> R) : \sum_(i <- r | P i) F i <= \sum_(i <- r | P i) G i. Proof. exact: (big_ind2 _ (lexx _) ler_add). Qed. +Lemma ler_sum_nat (m n : nat) (F G : nat -> R) : + (forall i, (m <= i < n)%N -> F i <= G i) -> + \sum_(m <= i < n) F i <= \sum_(m <= i < n) G i. +Proof. by move=> le_FG; rewrite !big_nat ler_sum. Qed. + Lemma psumr_eq0 (I : eqType) (r : seq I) (P : pred I) (F : I -> R) : (forall i, P i -> 0 <= F i) -> (\sum_(i <- r | P i) (F i) == 0) = (all (fun i => (P i) ==> (F i == 0)) r). diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 5f1b7d7..c6b2dfc 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1823,7 +1823,7 @@ Lemma prod_nat_const n : \prod_(i in A) n = n ^ #|A|. Proof. by rewrite big_const -Monoid.iteropE. Qed. Lemma sum_nat_const_nat n1 n2 n : \sum_(n1 <= i < n2) n = (n2 - n1) * n. -Proof. by rewrite big_const_nat; elim: (_ - _) => //= ? ->. Qed. +Proof. by rewrite big_const_nat iter_addn_0 mulnC. Qed. Lemma prod_nat_const_nat n1 n2 n : \prod_(n1 <= i < n2) n = n ^ (n2 - n1). Proof. by rewrite big_const_nat -Monoid.iteropE. Qed. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index bd58e01..1391b5b 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -208,7 +208,7 @@ Arguments eqVneq {T} x y, {T x y}. Section Contrapositives. Variables (T1 T2 : eqType). -Implicit Types (A : pred T1) (b : bool) (x : T1) (z : T2). +Implicit Types (A : pred T1) (b : bool) (P : Prop) (x : T1) (z : T2). Lemma contraTeq b x y : (x != y -> ~~ b) -> b -> x = y. Proof. by move=> imp hyp; apply/eqP; apply: contraTT hyp. Qed. @@ -219,6 +219,12 @@ Proof. by move=> imp hyp; apply/eqP; apply: contraNT hyp. Qed. Lemma contraFeq b x y : (x != y -> b) -> b = false -> x = y. Proof. by move=> imp /negbT; apply: contraNeq. Qed. +Lemma contraPeq P x y : (x != y -> ~ P) -> P -> x = y. +Proof. by move => imp HP; apply: contraTeq isT => /imp /(_ HP). Qed. + +Lemma contra_not_eq P x y : (x != y -> P) -> ~ P -> x = y. +Proof. by move => imp; apply: contraPeq => /imp HP /(_ HP). Qed. + Lemma contraTneq b x y : (x = y -> ~~ b) -> b -> x != y. Proof. by move=> imp; apply: contraTN => /eqP. Qed. @@ -228,6 +234,9 @@ Proof. by move=> imp; apply: contraNN => /eqP. Qed. Lemma contraFneq b x y : (x = y -> b) -> b = false -> x != y. Proof. by move=> imp /negbT; apply: contraNneq. Qed. +Lemma contraPneq P x y : (x = y -> ~ P) -> P -> x != y. +Proof. by move => imp; apply: contraPN => /eqP. Qed. + Lemma contra_eqN b x y : (b -> x != y) -> x = y -> ~~ b. Proof. by move=> imp /eqP; apply: contraL. Qed. @@ -246,6 +255,9 @@ Proof. by move=> imp; apply: contraNF => /imp->. Qed. Lemma contra_neqT b x y : (~~ b -> x = y) -> x != y -> b. Proof. by move=> imp; apply: contraNT => /imp->. Qed. +Lemma contra_neq_not P x y : (P -> x = y) -> x != y -> ~ P. +Proof. by move => imp;apply: contraNnot => /imp->. Qed. + Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 -> z1 != z2) -> z1 = z2 -> x1 = x2. Proof. by move=> imp /eqP; apply: contraTeq. Qed. diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 9fb79a2..6495ef6 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -608,6 +608,26 @@ Proof. by apply: same_connect1 => /=. Qed. Lemma same_fconnect1_r x y : fconnect f x y = fconnect f x (f y). Proof. by apply: same_connect1r x => /=. Qed. +Lemma fcard_gt0P (a : {pred T}) : + fclosed f a -> reflect (exists x, x \in a) (0 < fcard f a). +Proof. +move=> clfA; apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x. +exists (froot f x); rewrite inE roots_root /=; last exact: fconnect_sym. +by rewrite -(closed_connect clfA (connect_root _ x)). +Qed. + +Lemma fcard_gt1P (A : {pred T}) : + fclosed f A -> + reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ fconnect f x y) + (1 < fcard f A). +Proof. +move=> clAf; apply: (iffP card_gt1P) => [|[x xA [y yA not_xfy]]]. + move=> [x [y [/andP [/= rfx xA] /andP[/= rfy yA] xDy]]]. + by exists x; try exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy). +exists (froot f x), (froot f y); rewrite !inE !roots_root ?root_connect //=. +by split => //; rewrite -(closed_connect clAf (connect_root _ _)). +Qed. + End orbit_inj. Hint Resolve orbit_uniq : core. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index e608d2b..9bd8c1f 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -352,6 +352,9 @@ case: (pickP (mem A)) => [x Ax | A0]; [by right; exists x | left]. by apply/setP=> x; rewrite inE; apply: A0. Qed. +Lemma set_enum A : [set x | x \in enum A] = A. +Proof. by apply/setP => x; rewrite inE mem_enum. Qed. + Lemma enum_set0 : enum set0 = [::] :> seq T. Proof. by rewrite (eq_enum (in_set _)) enum0. Qed. @@ -636,6 +639,9 @@ Proof. by apply/setP=> x; rewrite !inE. Qed. Lemma setCT : ~: [set: T] = set0. Proof. by rewrite -setC0 setCK. Qed. +Lemma properC A B : (~: B \proper ~: A) = (A \proper B). +Proof. by rewrite !properE !setCS. Qed. + (* difference *) Lemma setDP A B x : reflect (x \in A /\ x \notin B) (x \in A :\: B). @@ -817,11 +823,26 @@ Proof. by rewrite setDE subsetIr. Qed. Lemma sub1set A x : ([set x] \subset A) = (x \in A). Proof. by rewrite -subset_pred1; apply: eq_subset=> y; rewrite !inE. Qed. +Variant cards_eq_spec A : seq T -> {set T} -> nat -> Type := +| CardEq (s : seq T) & uniq s : cards_eq_spec A s [set x | x \in s] (size s). + +Lemma cards_eqP A : cards_eq_spec A (enum A) A #|A|. +Proof. +by move: (enum A) (cardE A) (set_enum A) (enum_uniq A) => s -> <-; constructor. +Qed. + Lemma cards1P A : reflect (exists x, A = [set x]) (#|A| == 1). Proof. apply: (iffP idP) => [|[x ->]]; last by rewrite cards1. -rewrite eq_sym eqn_leq card_gt0 => /andP[/set0Pn[x Ax] leA1]. -by exists x; apply/eqP; rewrite eq_sym eqEcard sub1set Ax cards1 leA1. +by have [[|x []]// _] := cards_eqP; exists x; apply/setP => y; rewrite !inE. +Qed. + +Lemma cards2P A : reflect (exists x y : T, x != y /\ A = [set x; y]) + (#|A| == 2). +Proof. +apply: (iffP idP) => [|[x] [y] [xy ->]]; last by rewrite cards2 xy. +have [[|x [|y []]]//=] := cards_eqP; rewrite !inE andbT => neq_xy. +by exists x, y; split=> //; apply/setP => z; rewrite !inE. Qed. Lemma subset1 A x : (A \subset [set x]) = (A == [set x]) || (A == set0). @@ -964,6 +985,12 @@ Qed. Lemma properD A B C : (A \proper B :\: C) -> (A \proper B) && [disjoint A & C]. Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed. +Lemma properCr A B : (A \proper ~: B) = (B \proper ~: A). +Proof. by rewrite -properC setCK. Qed. + +Lemma properCl A B : (~: A \proper B) = (~: B \proper A). +Proof. by rewrite -properC setCK. Qed. + End setOps. Arguments set1P {T x a}. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index abed211..7e440ab 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -624,13 +624,17 @@ Proof. by apply: (iffP idP) => [/eqP/mem_card1[x inA]|[x /eq_card1/eqP//]]; exists x. Qed. -Lemma fintype_le1P : reflect (forall x, all_equal_to x) (#|T| <= 1). +Lemma card_le1_eqP A : + reflect {in A &, forall x, all_equal_to x} (#|A| <= 1). Proof. -apply: (iffP card_le1P)=> [inT x y|all_eq x _ y]; last first. - by rewrite (all_eq x) !inE eqxx. -by suff: y \in T by rewrite (inT x)// => /eqP. +apply: (iffP card_le1P) => [Ale1 x y xA yA /=|all_eq x xA y]. + by apply/eqP; rewrite -[_ == _]/(y \in pred1 x) -Ale1. +by rewrite inE; case: (altP (y =P x)) => [->//|]; exact/contra_neqF/all_eq. Qed. +Lemma fintype_le1P : reflect (forall x : T, all_equal_to x) (#|T| <= 1). +Proof. apply: (iffP (card_le1_eqP {:T})); [exact: in2T | exact: in2W]. Qed. + Lemma fintype1 : #|T| = 1 -> {x : T | all_equal_to x}. Proof. by move=> /mem_card1[x ex]; exists x => y; suff: y \in T by rewrite ex => /eqP. @@ -788,6 +792,40 @@ move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB). by rewrite (eq_subset eAB). Qed. +Lemma card_geqP {A n} : + reflect (exists s, [/\ uniq s, size s = n & {subset s <= A}]) (n <= #|A|). +Proof. +apply: (iffP idP) => [n_le_A|[s] [uniq_s size_s /subsetP subA]]; last first. + by rewrite -size_s -(card_uniqP _ uniq_s); exact: subset_leq_card. +exists (take n (enum A)); rewrite take_uniq ?enum_uniq // size_take. +split => //; last by move => x /mem_take; rewrite mem_enum. +case: (ltnP n (size (enum A))) => // size_A. +by apply/eqP; rewrite eqn_leq size_A -cardE n_le_A. +Qed. + +Lemma card_gt1P A : + reflect (exists x y, [/\ x \in A, y \in A & x != y]) (1 < #|A|). +Proof. +apply: (iffP card_geqP) => [[s] []|[x] [y] [xA yA xDy]]. + case: s => [|a [|b []]]//=; rewrite inE andbT => aDb _ subD. + by exists a, b; rewrite aDb !subD ?inE ?eqxx ?orbT. +exists [:: x; y]; rewrite /= !inE xDy. +by split=> // z; rewrite !inE => /pred2P[]->. +Qed. + +Lemma card_gt2P A : + reflect (exists x y z, + [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x]) + (2 < #|A|). +Proof. +apply: (iffP card_geqP) => [[s] []|[x] [y] [z] [[xD yD zD] [xDy xDz yDz]]]. + case: s => [|x [|y [|z []]]]//=; rewrite !inE !andbT negb_or -andbA. + case/and3P => xDy xDz yDz _ subA. + by exists x, y, z; rewrite xDy yDz eq_sym xDz !subA ?inE ?eqxx ?orbT. +exists [:: x; y; z]; rewrite /= !inE negb_or xDy xDz eq_sym yDz; split=> // u. +by rewrite !inE => /or3P [] /eqP->. +Qed. + Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A]. Proof. by congr (_ == 0); apply: eq_card => x; apply: andbC. Qed. @@ -866,6 +904,7 @@ Hint Resolve subxx_hint : core. Arguments pred0P {T P}. Arguments pred0Pn {T P}. Arguments card_le1P {T A}. +Arguments card_le1_eqP {T A}. Arguments card1P {T A}. Arguments fintype_le1P {T}. Arguments fintype1P {T}. @@ -873,6 +912,10 @@ Arguments subsetP {T A B}. Arguments subsetPn {T A B}. Arguments subset_eqP {T A B}. Arguments card_uniqP {T s}. +Arguments card_geqP {T A n}. +Arguments card_gt0P {T A}. +Arguments card_gt1P {T A}. +Arguments card_gt2P {T A}. Arguments properP {T A B}. (**********************************************************************) diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 920f393..dec68a3 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2008,6 +2008,12 @@ Proof. by rewrite -cats1 prefix_subseq. Qed. Lemma subseq_uniq s1 s2 : subseq s1 s2 -> uniq s2 -> uniq s1. Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed. +Lemma take_uniq s n : uniq s -> uniq (take n s). +Proof. exact/subseq_uniq/take_subseq. Qed. + +Lemma drop_uniq s n : uniq s -> uniq (drop n s). +Proof. exact/subseq_uniq/drop_subseq. Qed. + End Subseq. Prenex Implicits subseq. diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index b1498cd..892705b 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -202,3 +202,41 @@ End inj_can_sym_in_on. Arguments inj_can_sym_in_on {aT rT aD rD f g}. Arguments inj_can_sym_on {aT rT aD f g}. Arguments inj_can_sym_in {aT rT rD f g}. + +(* additional contra lemmas involving [P,Q : Prop] *) + +Section Contra. +Implicit Types (P Q : Prop) (b : bool). + +Lemma contra_not P Q : (Q -> P) -> (~ P -> ~ Q). Proof. by auto. Qed. + +Lemma contraPnot P Q : (Q -> ~ P) -> (P -> ~ Q). Proof. by auto. Qed. + +Lemma contraTnot b P : (P -> ~~ b) -> (b -> ~ P). +Proof. by case: b; auto. Qed. + +Lemma contraNnot P b : (P -> b) -> (~~ b -> ~ P). +Proof. rewrite -{1}[b]negbK; exact: contraTnot. Qed. + +Lemma contraPT P b : (~~ b -> ~ P) -> P -> b. +Proof. by case: b => //= /(_ isT) nP /nP. Qed. + +Lemma contra_notT P b : (~~ b -> P) -> ~ P -> b. +Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed. + +Lemma contra_notN P b : (b -> P) -> ~ P -> ~~ b. +Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed. + +Lemma contraPN P b : (b -> ~ P) -> (P -> ~~ b). +Proof. by case: b => //=; move/(_ isT) => HP /HP. Qed. + +Lemma contraFnot P b : (P -> b) -> b = false -> ~ P. +Proof. by case: b => //; auto. Qed. + +Lemma contraPF P b : (b -> ~ P) -> P -> b = false. +Proof. by case: b => // /(_ isT). Qed. + +Lemma contra_notF P b : (b -> P) -> ~ P -> b = false. +Proof. by case: b => // /(_ isT). Qed. +End Contra. + diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 39c8451..6837eb1 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -403,7 +403,7 @@ Proof. by rewrite -implyNb -ltnNge; apply/implyP; apply: ltnW. Qed. (* Helper lemmas to support generalized induction over a nat measure. *) (* The idiom for a proof by induction over a measure Mxy : nat involving *) (* variables x, y, ... (e.g., size x + size y) is *) -(* have [m leMn] := ubnP Mxy; elim: n => // n IHn in x y ... leMn ... *. *) +(* have [n leMn] := ubnP Mxy; elim: n => // n IHn in x y ... leMn ... *. *) (* after which the current goal (possibly modified by generalizations in the *) (* in ... part) can be proven with the extra context assumptions *) (* n : nat *) @@ -416,11 +416,11 @@ Proof. by rewrite -implyNb -ltnNge; apply/implyP; apply: ltnW. Qed. (* The leMn statement is convertible to Mxy <= n; if it is necessary to *) (* have _exactly_ leMn : Mxy <= n, the ltnSE helper lemma may be used as *) (* follows *) -(* have [m] := ubnP Mxy; elim: n => // n IHn in x y ... * => /ltnSE-leMn. *) +(* have [n] := ubnP Mxy; elim: n => // n IHn in x y ... * => /ltnSE-leMn. *) (* We also provide alternative helper lemmas for proofs where the upper *) (* bound appears in the goal, and we assume nonstrict (in)equality. *) (* In either case the proof will have to dispatch an Mxy = 0 case. *) -(* have [m defM] := ubnPleq Mxy; elim: n => [|n IHn] in x y ... defM ... *. *) +(* have [n defM] := ubnPleq Mxy; elim: n => [|n IHn] in x y ... defM ... *. *) (* yields two subgoals, in which Mxy has been replaced by 0 and n.+1, *) (* with the extra assumption defM : Mxy <= 0 / Mxy <= n.+1, respectively. *) (* The second goal also has the inductive assumption *) |