linting

CHANGELOG_UNRELEASED.md

@@ -92,14 +92,14 @@
   + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
     `max_fun_continuous`.
 
-- in file `functions.v`,
-  + new lemmas `uncurryK`, and `curryK`.
+- in file `boolp.v`,
+  + new lemmas `uncurryK`, and `curryK`
 - in file `weak_topology.v`,
-  + new lemma `continuous_comp_weak`.
+  + new lemma `continuous_comp_weak`
 - in file `function_spaces.v`,
-  + new definitions `eval`.
+  + new definition `eval`
   + new lemmas `continuous_curry_fun`, `continuous_curry_joint_cvg`, 
-    `eval_continuous`, and `compose_continuous`.
+    `eval_continuous`, and `compose_continuous`
 
 ### Changed
 

classical/boolp.v

@@ -969,3 +969,9 @@ Lemma inhabited_witness: inhabited T -> T.
 Proof. by rewrite inhabitedE => /cid[]. Qed.
 
 End Inhabited.
+
+Lemma uncurryK {X Y Z : Type} : cancel (@uncurry X Y Z) curry.
+Proof. by move=> f; rewrite funeq2E. Qed.
+
+Lemma curryK {X Y Z : Type} : cancel curry (@uncurry X Y Z).
+Proof. by move=> f; rewrite funeqE=> -[]. Qed.

classical/functions.v

@@ -2665,9 +2665,3 @@ End function_space_lemmas.
 
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : f\^-1\^-1%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
-
-Lemma uncurryK  {X Y Z : Type} : cancel (@uncurry X Y Z) curry.
-Proof. by move=> f; rewrite funeq2E => ? ?. Qed.
-
-Lemma curryK  {X Y Z : Type} : cancel curry (@uncurry X Y Z).
-Proof. by move=> f; rewrite funeqE; case=> ? ?. Qed.

theories/function_spaces.v

@@ -1441,11 +1441,11 @@ Lemma continuous_curry_fun (f : U * V -> W) :
   continuous f -> continuous (curry f).
 Proof. by case/continuous_curry. Qed.
 
-Lemma continuous_curry_joint_cvg (f : U * V -> W) (u : U) (v : V) : 
-  continuous f -> curry f z.1 z.2 @[z --> (u,v)] --> curry f u v.
-Proof. 
-move=> cf D /cf; rewrite ?nbhs_simpl /curry /=; apply: filterS => z.
-by move=> ?; rewrite /= -surjective_pairing.
+Lemma continuous_curry_joint_cvg (f : U * V -> W) (u : U) (v : V) :
+  continuous f -> curry f z.1 z.2 @[z --> (u, v)] --> curry f u v.
+Proof.
+move=> cf D /cf; rewrite !nbhs_simpl /curry /=; apply: filterS => z ? /=.
+by rewrite -surjective_pairing.
 Qed.
 
 Lemma continuous_uncurry_regular (f : U -> V -> W) :
@@ -1557,44 +1557,42 @@ End cartesian_closed.
 
 End currying.
 
-Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y  := 
+Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
   uncurry (id : continuousType X Y -> (X -> Y)).
 
 Section composition.
 
 Local Import ArrowAsCompactOpen.
 
-Lemma eval_continuous {X Y : topologicalType} : 
+Lemma eval_continuous {X Y : topologicalType} :
   locally_compact [set: X] -> regular_space X -> continuous (@eval X Y).
 Proof.
-move=> ? ?; apply: continuous_uncurry_regular => //.
+move=> lcX rsX; apply: continuous_uncurry_regular => //.
   exact: weak_continuous.
 by move=> ?; exact: cts_fun.
 Qed.
 
-Lemma compose_continuous {X Y Z : topologicalType} : 
+Lemma compose_continuous {X Y Z : topologicalType} :
   locally_compact [set: X] -> @regular_space X ->
   locally_compact [set: Y] -> @regular_space Y ->
-  continuous (uncurry 
+  continuous (uncurry
     (comp : continuousType Y Z -> continuousType X Y -> continuousType X Z)).
 Proof.
-move=> ? ? lY rY; apply: continuous_comp_weak.
+move=> lX rX lY rY; apply: continuous_comp_weak.
 set F := _ \o _.
 rewrite -[F]uncurryK; apply: continuous_curry_fun.
-pose g := uncurry F \o prodAr \o (@swap _ _); simpl in *.
-have -> : uncurry F = uncurry F \o prodAr \o prodA.
-  by rewrite funeqE; case; case.
+pose g := uncurry F \o prodAr \o swap; rewrite /= in g *.
+have -> : uncurry F = uncurry F \o prodAr \o prodA by rewrite funeqE => -[[]].
 move=> z; apply: continuous_comp; first exact: prodA_continuous.
-have -> : uncurry F \o prodAr = 
-    uncurry F \o prodAr \o (@swap _ _) \o (@swap _ _).
-  by rewrite funeqE; case; case.
+have -> : uncurry F \o prodAr = uncurry F \o prodAr \o swap \o swap.
+  by rewrite funeqE => -[[]].
 apply: continuous_comp; first exact: swap_continuous.
-pose h (fxg : continuousType X Y * X * continuousType Y Z) : Z := 
-  eval (fxg.2, ((eval fxg.1))).
-have <- : h = uncurry F \o prodAr \o (@swap _ _).
-  by rewrite /h/g/uncurry/swap/F funeqE; case; case.
+pose h (fxg : continuousType X Y * X * continuousType Y Z) : Z :=
+  eval (fxg.2, (eval fxg.1)).
+have <- : h = uncurry F \o prodAr \o swap.
+  by rewrite /h/g/uncurry/swap/F funeqE => -[[]].
 rewrite /h.
-apply: (@continuous2_cvg _ _ _ _ _ _ (snd) (eval \o fst) (curry eval)).
+apply: (@continuous2_cvg _ _ _ _ _ _ snd (eval \o fst) (curry eval)).
 - by apply: continuous_curry_joint_cvg; exact: eval_continuous.
 - exact: cvg_snd.
 - by apply: cvg_comp; [exact: cvg_fst | exact: eval_continuous].

theories/topology_theory/weak_topology.v

@@ -212,10 +212,10 @@ Qed.
 
 End weak_order_refine.
 
-Lemma continuous_comp_weak {Y : choiceType} {X Z : topologicalType} (w : Y -> Z) 
-  (f : X -> (weak_topology w)) :
+Lemma continuous_comp_weak {Y : choiceType} {X Z : topologicalType} (w : Y -> Z)
+  (f : X -> weak_topology w) :
   continuous (w \o f) -> continuous f.
 Proof.
 move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf.
-by apply: open_nbhs_nbhs; split.
+exact: open_nbhs_nbhs.
 Qed.