From 80b9812920299c47bf08ed2d9196b4e3a5bcbcd1 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 22 Mar 2024 08:51:10 +0100 Subject: [PATCH] remove backported lemmas to ssreflect --- theories/xmathcomp/various.v | 130 ----------------------------------- 1 file changed, 130 deletions(-) diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index d4057eb..6921947 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -5,136 +5,6 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -(*********************) -(* package ssreflect *) -(*********************) - -(***********) -(* ssrbool *) -(***********) - -Lemma classicPT (P : Type) : classically P <-> ((P -> False) -> False). -Proof. -split; first by move=>/(_ false) PFF PF; suff: false by []; apply: PFF => /PF. -by move=> PFF []// Pf; suff: False by []; apply: PFF => /Pf. -Qed. - -Lemma classic_sigW T (P : T -> Prop) : - classically (exists x, P x) <-> classically (sig P). -Proof. by split; apply: classic_bind => -[x Px]; apply/classicW; exists x. Qed. - -Lemma classic_ex T (P : T -> Prop) : - ~ (forall x, ~ P x) -> classically (ex P). -Proof. -move=> NfNP; apply/classicPT => exPF; apply: NfNP => x Px. -by apply: exPF; exists x. -Qed. - -(*******) -(* seq *) -(*******) - -Lemma subset_mapP (X Y : eqType) (f : X -> Y) (s : seq X) (s' : seq Y) : - {subset s' <= map f s} <-> exists2 t, all (mem s) t & s' = map f t. -Proof. -split => [|[r /allP/= rE ->] _ /mapP[x xr ->]]; last by rewrite map_f ?rE. -elim: s' => [|x s' IHs'] subss'; first by exists [::]. -have /mapP[y ys ->] := subss' _ (mem_head _ _). -have [x' x's'|t st ->] := IHs'; first by rewrite subss'// inE x's' orbT. -by exists (y :: t); rewrite //= ys st. -Qed. -Arguments subset_mapP {X Y}. - -(*********) -(* bigop *) -(*********) - -Lemma big_rcons_idx (R : Type) (idx : R) (op : R -> R -> R) (I : Type) - (i : I) (r : seq I) (P : pred I) (F : I -> R) - (idx' := if P i then op (F i) idx else idx) : - \big[op/idx]_(j <- rcons r i | P j) F j = \big[op/idx']_(j <- r | P j) F j. -Proof. by elim: r => /= [|j r]; rewrite ?(big_nil, big_cons)// => ->. Qed. - -Lemma big_change_idx (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) - (x : R) (r : seq I) (P : pred I) (F : I -> R) : - op (\big[op/idx]_(j <- r | P j) F j) x = \big[op/x]_(j <- r | P j) F j. -Proof. -elim: r => [|i r]; rewrite ?(big_nil, big_cons, Monoid.mul1m)// => <-. -by case: ifP => // Pi; rewrite Monoid.mulmA. -Qed. -Lemma big_rcons (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) - i r (P : pred I) F : - \big[op/idx]_(j <- rcons r i | P j) F j = - op (\big[op/idx]_(j <- r | P j) F j) (if P i then F i else idx). -Proof. by rewrite big_rcons_idx -big_change_idx Monoid.mulm1. Qed. - -(********) -(* path *) -(********) - -Lemma sortedP T x (s : seq T) (r : rel T) : - reflect (forall i, i.+1 < size s -> r (nth x s i) (nth x s i.+1)) (sorted r s). -Proof. -elim: s => [|y [|z s]//= IHs]/=; do ?by constructor. -apply: (iffP andP) => [[ryz rzs] [|i]// /IHs->//|rS]. -by rewrite (rS 0); split=> //; apply/IHs => i /(rS i.+1). -Qed. - -(*********) -(* tuple *) -(*********) - -Section tnth_shift. -Context {T : Type} {n1 n2} (t1 : n1.-tuple T) (t2 : n2.-tuple T). - -Lemma tnth_lshift i : tnth [tuple of t1 ++ t2] (lshift n2 i) = tnth t1 i. -Proof. -have x0 := tnth_default t1 i; rewrite !(tnth_nth x0). -by rewrite nth_cat size_tuple /= ltn_ord. -Qed. - -Lemma tnth_rshift j : tnth [tuple of t1 ++ t2] (rshift n1 j) = tnth t2 j. -Proof. -have x0 := tnth_default t2 j; rewrite !(tnth_nth x0). -by rewrite nth_cat size_tuple ltnNge leq_addr /= addKn. -Qed. -End tnth_shift. - -(*********) -(* prime *) -(*********) - -Lemma primeNsig (n : nat) : ~~ prime n -> (2 <= n)%N -> - { d : nat | (1 < d < n)%N & (d %| n)%N }. -Proof. -move=> primeN_n le2n; case/pdivP: {+}le2n => d /primeP[lt1d prime_d] dvd_dn. -exists d => //; rewrite lt1d /= ltn_neqAle dvdn_leq 1?andbT //; last first. - by apply: (leq_trans _ le2n). -by apply: contra primeN_n => /eqP <-; apply/primeP. -Qed. - -Lemma totient_gt1 n : (totient n > 1)%N = (n > 2)%N. -Proof. -case: n => [|[|[|[|n']]]]//=; set n := n'.+4; rewrite [RHS]isT. -have [pn2|/allPn[p]] := altP (@allP _ (eq_op^~ 2%N) (primes n)); last first. - rewrite mem_primes/=; move: p => [|[|[|p']]]//; set p := p'.+3. - move=> /andP[p_prime dvdkn]. - have [//|[|k]// cpk ->] := (@pfactor_coprime _ n p_prime). - rewrite totient_coprime ?coprimeXr 1?coprime_sym//. - rewrite totient_pfactor ?logn_gt0 ?mem_primes ?p_prime// mulnCA. - by rewrite (@leq_trans p.-1) ?leq_pmulr ?muln_gt0 ?expn_gt0 ?totient_gt0. -have pnNnil : primes n != [::]. - apply: contraTneq isT => pn0. - by have := @prod_prime_decomp n isT; rewrite prime_decompE pn0/= big_nil. -have := @prod_prime_decomp n isT; rewrite prime_decompE. -case: (primes n) pnNnil pn2 (primes_uniq n) => [|p [|p' r]]//=; last first. - move=> _ eq2; rewrite !inE [p](eqP (eq2 _ _)) ?inE ?eqxx//. - by rewrite [p'](eqP (eq2 _ _)) ?inE ?eqxx// orbT. -move=> _ /(_ _ (mem_head _ _))/eqP-> _; rewrite big_cons big_nil muln1/=. -case: (logn 2 n) => [|[|k]]// ->. -by rewrite totient_pfactor//= expnS mul1n leq_pmulr ?expn_gt0. -Qed. - (********************) (* package fingroup *) (********************)