diff --git a/classical_sets.v b/classical_sets.v index 4a0d38823..31ac19361 100644 --- a/classical_sets.v +++ b/classical_sets.v @@ -163,7 +163,7 @@ Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin. Definition set A := A -> Prop. Definition in_set T (P : set T) : pred T := [pred x | `[

]]. -Canonical set_predType T := @mkPredType T (set T) (@in_set T). +Canonical set_predType T := @PredType T (set T) (@in_set T). Lemma in_setE T (P : set T) x : x \in P = P x :> Prop. Proof. by rewrite propeqE; split => [] /asboolP. Qed. diff --git a/derive.v b/derive.v index 1ff793bb9..d57ff2563 100644 --- a/derive.v +++ b/derive.v @@ -397,7 +397,7 @@ suff /diff_locally /hdf -> : differentiable f x. apply/diffP; apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\ forall y, f y = f (lim x) + df (y - lim x) +o_(y \near x) (y - lim x))). exists df; split=> //; apply: eqaddoEx => z. -rewrite (hdf _ dxf) !addrA lim_id /funcomp /= subrK [f _ + _]addrC addrK. +rewrite (hdf _ dxf) !addrA lim_id /(_ \o _) /= subrK [f _ + _]addrC addrK. rewrite -addrA -[LHS]addr0; congr (_ + _). apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP. by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x). @@ -1345,7 +1345,7 @@ Proof. move=> cvfx; apply/Logic.eq_sym. (* should be inferred *) have atrF := at_right_proper_filter x. -apply: flim_map_lim => A /cvfx /locallyP [_ /posnumP[e] xe_A]. +apply: (@flim_map_lim _ _ _ (at_right _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A]. by exists e%:num => // y xe_y; rewrite ltr_def => /andP [xney _]; apply: xe_A. Qed. @@ -1355,7 +1355,7 @@ Proof. move=> cvfx; apply/Logic.eq_sym. (* should be inferred *) have atrF := at_left_proper_filter x. -apply: flim_map_lim => A /cvfx /locallyP [_ /posnumP[e] xe_A]. +apply: (@flim_map_lim _ _ _ (at_left _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A]. exists e%:num => // y xe_y; rewrite ltr_def => /andP [xney _]. by apply: xe_A => //; rewrite eq_sym. Qed. diff --git a/normedtype.v b/normedtype.v index 2719f40ac..85d8401d7 100644 --- a/normedtype.v +++ b/normedtype.v @@ -795,7 +795,7 @@ Proof. by symmetry; apply: locally_flim_unique; apply/cvg_ex; exists x. Qed. Lemma flim_lim {F} {FF : ProperFilter F} (l : V) : F --> l -> lim F = l. -Proof. by move=> Fl; have Fcv := cvgP Fl; apply: flim_unique. Qed. +Proof. by move=> Fl; have Fcv := cvgP Fl; apply: (@flim_unique F). Qed. Lemma flim_map_lim {T : Type} {F} {FF : ProperFilter F} (f : T -> V) (l : V) : f @ F --> l -> lim (f @ F) = l. diff --git a/topology.v b/topology.v index f651609a4..78892aa03 100644 --- a/topology.v +++ b/topology.v @@ -804,12 +804,12 @@ Proof. by move=> ????? PQR FP; apply: filter_app2; apply: filter_app FP. Qed. Lemma filterS2 (T : Type) (F : set (set T)) : Filter F -> forall P Q R : set T, (forall x, P x -> Q x -> R x) -> F P -> F Q -> F R. -Proof. by move=> ???? /filterE; apply: filter_app2. Qed. +Proof. by move=> ? ? ? ? ?; apply: filter_app2; apply: filterE. Qed. Lemma filterS3 (T : Type) (F : set (set T)) : Filter F -> forall P Q R S : set T, (forall x, P x -> Q x -> R x -> S x) -> F P -> F Q -> F R -> F S. -Proof. by move=> ????? /filterE; apply: filter_app3. Qed. +Proof. by move=> ? ? ? ? ? ?; apply: filter_app3; apply: filterE. Qed. Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) : F (fun=> P) -> P. @@ -1948,7 +1948,7 @@ Lemma cluster_flimE F : Proof. move=> FF; rewrite predeqE => p. split=> [clFp|[G Gproper [cvGp sFG]] A B]; last first. - by move=> /sFG GA /cvGp GB; apply/filter_ex; apply: filterI. + by move=> /sFG GA /cvGp GB; apply: (@filter_ex _ G); apply: filterI. exists (filter_from (\bigcup_(A in F) [set A `&` B | B in locally p]) id). apply filter_from_proper; last first. by move=> _ [A FA [B p_B <-]]; have := clFp _ _ FA p_B. @@ -2009,7 +2009,7 @@ have GF : ProperFilter G. move=> C1 C2 F1 F2; exists (C1 `&` C2); first exact: filterI. by move=> ?[?[]]; split; split. by move=> C /(filterI FfA) /filter_ex [_ [[p ? <-]]]; eexists p. -case: Aco; first by exists (f @` A) => // ? []. +case: (Aco G); first by exists (f @` A) => // ? []. move=> p [Ap clsGp]; exists (f p); split; first exact/imageP. move=> B C FB /fcont; rewrite in_setE /= locally_filterE => /(_ Ap) p_Cf. have : G (A `&` f @^-1` B) by exists B. @@ -2055,7 +2055,7 @@ suff UAF : ProperFilter (\bigcup_(H in A) projT1 H). exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH B HB /=. by exists H. apply Build_ProperFilter. - by move=> B [H AH HB]; have [HF _] := projT2 H; apply: filter_ex. + by move=> B [H AH HB]; have [HF _] := projT2 H; apply: (@filter_ex _ _ HF). split; first by exists G => //; apply: filterT. move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC. @@ -2199,7 +2199,7 @@ Lemma filter_finI (T : pointedType) (F : set (set T)) (D : set (set T)) (f : set T -> set T) : ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f. Proof. -move=> FF sDFf D' sD; apply/filter_ex; apply: filter_bigI. +move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI. by move=> A /sD; rewrite in_setE => /sDFf. Qed. @@ -2253,8 +2253,8 @@ rewrite predeqE => A; split=> [Aco I D f [g gcl feAg] finIf|Aco F FF FA]. exists p => j Dj; rewrite feAg //; split=> //; apply: gcl => // B. by apply: clfinIfp; exists (f j); [apply: finI_from1|rewrite feAg // => ? []]. have finIAclF : finI F (fun B => A `&` closure B). - apply: filter_finI => B FB; apply: filterI => //; apply: filterS FB. - exact: subset_closure. + apply: (@filter_finI _ F) => B FB. + by apply: filterI => //; apply: filterS FB; apply: subset_closure. have [|p AclFIp] := Aco _ _ _ _ finIAclF. by exists closure=> //; move=> ??; apply: closed_closure. exists p; split=> [|B C FB p_C]; first by have /AclFIp [] := FA. @@ -2608,7 +2608,7 @@ Lemma flim_closeP (F : set (set M)) (l : M) : ProperFilter F -> F --> l <-> ([cvg F in M] /\ close (lim F) l). Proof. move=> FF; split=> [Fl|[cvF]Cl]. - by have /cvgP := Fl; split=> //; apply: flim_close. + by have /cvgP := Fl; split=> //; apply: (@flim_close F). by apply: flim_trans (close_limxx Cl). Qed.