Instances for dependent function types

classical/boolp.v

@@ -106,8 +106,11 @@ Proof. by have [propext _] := extensionality; apply: propext. Qed.
 
 Ltac eqProp := apply: propext; split.
 
+Lemma funext_dep {T} {U : T -> Type} (f g : forall t, U t) : (forall t, f t = g t) -> f = g.
+Proof. exact/functional_extensionality_dep. Qed.
+
 Lemma funext {T U : Type} (f g : T -> U) : (f =1 g) -> f = g.
-Proof. by case: extensionality=> _; apply. Qed.
+Proof. exact/funext_dep. Qed.
 
 Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q).
 Proof. by apply: propext; split=> [->|/propext]. Qed.

classical/cardinality.v

@@ -1340,7 +1340,7 @@ Section zmod.
 Context (aT : Type) (rT : zmodType).
 Lemma fimfun_zmod_closed : zmod_closed (@fimfun aT rT).
 Proof.
-split=> [|f g]; rewrite !inE/=; first exact: finite_image_cst.
+split=> [|f g]; rewrite !inE/=; first exact: (finite_image_cst 0).
 by move=> fA gA; apply: (finite_image11 (fun x y => x - y)).
 Qed.
 HB.instance Definition _ :=

classical/functions.v

@@ -2568,61 +2568,132 @@ Qed.
 
 Obligation Tactic := idtac.
 
-Program Definition fct_zmodMixin (T : Type) (M : zmodType) :=
-  @GRing.isZmodule.Build (T -> M) \0 (fun f x => - f x) (fun f g => f \+ g)
+Definition add_fun {aT} {rT : aT -> nmodType} (f g : forall x, rT x) x := f x + g x.
+Definition opp_fun {aT} {rT : aT -> zmodType} (f : forall x, rT x) x := - f x.
+Definition sub_fun {aT} {rT : aT -> zmodType} (f g : forall x, rT x) x := f x - g x.
+Definition mul_fun {aT} {rT : aT -> semiRingType} (f g : forall x, rT x) x := f x * g x.
+Definition scale_fun {aT} {R} {rT : aT -> lmodType R} (k : R) (f : forall x, rT x) x := k *: f x.
+
+Notation "f \+ g" := (add_fun f g) : ring_scope.
+Notation "\- f" := (opp_fun f) : ring_scope.
+Notation "f \- g" := (sub_fun f g) : ring_scope.
+Notation "f \* g" := (mul_fun f g) : ring_scope.
+Notation "k \*: f" := (scale_fun k f) : ring_scope.
+
+Arguments add_fun {_ _} f g _ /.
+Arguments opp_fun {_ _} f _ /.
+Arguments sub_fun {_ _} f g _ /.
+Arguments mul_fun {_ _} f g _ /.
+Arguments scale_fun {_ _ _} k f _ /.
+
+Program Definition fct_zmodMixin (T : Type) (M : T -> zmodType) :=
+  @GRing.isZmodule.Build (forall t, M t) (fun=> 0) (fun f => \- f) (fun f g => f \+ g)
      _ _ _ _.
-Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite addrA. Qed.
-Next Obligation. by move=> T M f g; rewrite funeqE=> x /=; rewrite addrC. Qed.
-Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite add0r. Qed.
-Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite addNr. Qed.
-HB.instance Definition _ (T : Type) (M : zmodType) := fct_zmodMixin T M.
-
-Program Definition fct_ringMixin (T : pointedType) (M : ringType) :=
-  @GRing.Zmodule_isRing.Build (T -> M) (cst 1) (fun f g => f \* g) _ _ _ _ _ _.
-Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite mulrA. Qed.
-Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite mul1r. Qed.
-Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite mulr1. Qed.
-Next Obligation. by move=> T M f g h; rewrite funeqE=> x/=; rewrite mulrDl. Qed.
-Next Obligation. by move=> T M f g h; rewrite funeqE=> x/=; rewrite mulrDr. Qed.
 Next Obligation.
-by move=> T M ; apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0.
+by move=> T M f g h; apply/funext_dep => x /=; rewrite addrA.
 Qed.
-HB.instance Definition _ (T : pointedType) (M : ringType) := fct_ringMixin T M.
+Next Obligation.
+by move=> T M f g; apply/funext_dep => x /=; rewrite addrC.
+Qed.
+Next Obligation.
+by move=> T M f; apply/funext_dep => x /=; rewrite add0r.
+Qed.
+Next Obligation.
+by move=> T M f; apply/funext_dep => x /=; rewrite addNr.
+Qed.
+HB.instance Definition _ (T : Type) (M : T -> zmodType) := fct_zmodMixin M.
 
-Program Definition fct_comRingType (T : pointedType) (M : comRingType) :=
-  GRing.Ring_hasCommutativeMul.Build (T -> M) _.
+Program Definition fct_ringMixin (T : pointedType) (M : T -> ringType) :=
+  @GRing.Zmodule_isRing.Build (forall t, M t) (fun=> 1) (fun f g => f \* g) _ _ _ _ _ _.
+Next Obligation.
+by move=> T M f g h; apply/funext_dep => x /=; rewrite mulrA.
+Qed.
 Next Obligation.
-by move=> T M f g; rewrite funeqE => x; rewrite /GRing.mul/= mulrC.
+by move=> T M f; apply/funext_dep => x /=; rewrite mul1r.
 Qed.
-HB.instance Definition _ (T : pointedType) (M : comRingType) :=
-  fct_comRingType T M.
+Next Obligation.
+by move=> T M f; apply/funext_dep => x /=; rewrite mulr1.
+Qed.
+Next Obligation.
+by move=> T M f g h; apply/funext_dep => x/=; rewrite mulrDl.
+Qed.
+Next Obligation.
+by move=> T M f g h; apply/funext_dep => x/=; rewrite mulrDr.
+Qed.
+Next Obligation.
+by move=> T M ; apply/eqP => /(congr1 (fun f => f point)) /eqP; rewrite oner_eq0.
+Qed.
+HB.instance Definition _ (T : pointedType) (M : T -> ringType) := fct_ringMixin M.
+
+Program Definition fct_comRingType (T : pointedType) (M : T -> comRingType) :=
+  GRing.Ring_hasCommutativeMul.Build (forall t, M t) _.
+Next Obligation.
+by move=> T M f g; apply/funext_dep => x; apply/mulrC.
+Qed.
+HB.instance Definition _ (T : pointedType) (M : T -> comRingType) :=
+  fct_comRingType M.
 
 Section fct_lmod.
-Variables (U : Type) (R : ringType) (V : lmodType R).
-Program Definition fct_lmodMixin := @GRing.Zmodule_isLmodule.Build R (U -> V)
+Variables (U : Type) (R : ringType) (V : U -> lmodType R).
+Program Definition fct_lmodMixin := @GRing.Zmodule_isLmodule.Build R (forall u, V u)
   (fun k f => k \*: f) _ _ _ _.
-Next Obligation. by move=> k f v; rewrite funeqE=> x; exact: scalerA. Qed.
-Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite scale1r. Qed.
 Next Obligation.
-by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr.
+by move=> k f v; apply/funext_dep => x; exact: scalerA.
+Qed.
+Next Obligation.
+by move=> f; apply/funext_dep => x /=; rewrite scale1r.
+Qed.
+Next Obligation.
+by move=> f g h; apply/funext_dep => x /=; rewrite scalerDr.
 Qed.
 Next Obligation.
-by move=> f g h; rewrite funeqE => x /=; rewrite scalerDl.
+by move=> f g h; apply/funext_dep => x /=; rewrite scalerDl.
 Qed.
 HB.instance Definition _ := fct_lmodMixin.
 End fct_lmod.
 
-Lemma fct_sumE (I T : Type) (M : zmodType) r (P : {pred I}) (f : I -> T -> M)
+Lemma add_funE (T : pointedType) (M : T -> zmodType) (f g : forall t, M t) :
+  (f + g) = f \+ g.
+Proof. exact/funext_dep. Qed.
+
+Lemma opp_funE (T : Type) (M : T -> zmodType) (f : forall t, M t) : - f = \- f.
+Proof. exact/funext_dep. Qed.
+
+Lemma sub_funE (T : Type) (M : T -> zmodType) (f g : forall t, M t) :
+  (f - g) = f \- g.
+Proof. exact/funext_dep. Qed.
+
+Lemma fct_sumE (I T : Type) (M : T -> zmodType) r (P : {pred I}) (f : I -> forall t, M t)
     (x : T) :
   (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
 Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
 
+Lemma mul_funE (T : pointedType) (M : T -> ringType) (f g : forall t, M t) :
+  (f * g) = f \* g.
+Proof. exact/funext_dep. Qed.
+
+Lemma scale_funE (T : Type) (R : ringType) (M : T -> lmodType R) (k : R) (f : forall t, M t) :
+  k *: f = k \*: f.
+Proof. exact/funext_dep. Qed.
+
 Lemma mul_funC (T : Type) {R : comSemiRingType} (f : T -> R) (r : R) :
   r \*o f = r \o* f.
 Proof. by apply/funext => x/=; rewrite mulrC. Qed.
 
 End function_space.
 
+Notation "f \+ g" := (add_fun f g) : ring_scope.
+Notation "\- f" := (opp_fun f) : ring_scope.
+Notation "f \- g" := (sub_fun f g) : ring_scope.
+Notation "f \* g" := (mul_fun f g) : ring_scope.
+Notation "k \*: f" := (scale_fun k f) : ring_scope.
+
+Arguments add_fun {_ _} f g _ /.
+Arguments opp_fun {_ _} f _ /.
+Arguments sub_fun {_ _} f g _ /.
+Arguments mul_fun {_ _} f g _ /.
+Arguments scale_fun {_ _ _} k f _ /.
+
 Section function_space_lemmas.
 Local Open Scope ring_scope.
 Import GRing.Theory.

theories/derive.v

@@ -224,7 +224,7 @@ Section diff_locally_converse_tentative.
 (* and thus a littleo of 1, and so is id *)
 (* This can be generalized to any dimension *)
 Lemma diff_locally_converse_part1 (f : R -> R) (a b x : R) :
-  f \o shift x = cst a + b *: idfun +o_ 0 id -> f x = a.
+  f \o shift x = cst a + b *: (@idfun R) +o_ 0 id -> f x = a.
 Proof.
 rewrite funeqE => /(_ 0) /=; rewrite add0r => ->.
 by rewrite -[LHS]/(_ 0 + _ 0 + _ 0) /cst [X in a + X]scaler0 littleo_lim0 ?addr0.
@@ -253,12 +253,12 @@ Lemma derivable_nbhs (f : V -> W) a v :
 Proof.
 move=> df; apply/eqaddoP => _/posnumP[e].
 rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first.
-  rewrite /at_point opprD -![(_ + _ : _ -> _) _]/(_ + _) scale0r add0r.
+  rewrite /at_point opprD !add_funE !opp_funE/= scale0r add0r.
   by rewrite addrA subrr add0r normrN scale0r !normr0 mulr0.
 have /eqolimP := df.
 move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]).
 apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0.
-rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
+rewrite /= opprD !add_funE !opp_funE.
 rewrite /cst /= [`|1|]normr1 mulr1 => dfv.
 rewrite addrA -[X in X + _]scale1r -(@mulVf _ h) //.
 rewrite mulrC -scalerA -scalerBr normrZ.
@@ -276,7 +276,7 @@ move=> df; apply/cvg_ex; exists ('D_v f a).
 apply/(@eqolimP _ _ _ (dnbhs_filter_on _))/eqaddoP => _/posnumP[e].
 have /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]) := df.
 rewrite /= !(near_simpl, near_withinE); apply: filter_app; near=> h.
-rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
+rewrite /= opprD !add_funE !opp_funE.
 rewrite /cst /= [`|1|]normr1 mulr1 addrA => dfv hN0.
 rewrite -[X in _ - X]scale1r -(@mulVf _ h) //.
 rewrite -scalerA -scalerBr normrZ normfV ler_pdivrMl ?normr_gt0 //.
@@ -398,7 +398,7 @@ Variable R : numFieldType.
 Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\
   cst a \o shift x = cst (cst a x) + \0 +o_ 0 id.
 Proof.
-split; first exact: cst_continuous.
+split; first exact: (@cst_continuous _ _ 0).
 apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _).
 by rewrite littleoE; last exact: littleo0_subproof.
 Qed.
@@ -412,7 +412,7 @@ Fact dadd (f g : V -> W) x :
 Proof.
 move=> df dg; split => [?|]; do ?exact: continuousD.
 apply/(@eqaddoE R); rewrite funeqE => y /=; rewrite -[(f + g) _]/(_ + _).
-by rewrite ![_ (_ + x)]diff_locallyx// addrACA addox addrACA.
+by rewrite add_funE ![_ (_ + x)]diff_locallyx// addrACA addox addrACA.
 Qed.
 
 Fact dopp (f : V -> W) x :
@@ -521,8 +521,8 @@ Lemma diff_unique (V W : normedModType R) (f : V -> W)
   continuous df -> f \o shift x = cst (f x) + df +o_ 0 id ->
   'd f x = df :> (V -> W).
 Proof.
-move=> dfc dxf; apply/subr0_eq; rewrite -[LHS]/(_ \- _).
-apply/littleo_linear0/eqoP/eq_some_oP => /=; rewrite funeqE => y /=.
+move=> dfc dxf; apply/subr0_eq/(@littleo_linear0 _ _ (GRing.sub_fun _ _))/eqoP.
+apply/eq_some_oP => /=; rewrite funeqE => y /=.
 have hdf h : (f \o shift x = cst (f x) + h +o_ 0 id) ->
     h = f \o shift x - cst (f x) +o_ 0 id.
   move=> hdf; apply: eqaddoE.
@@ -544,7 +544,7 @@ by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x).
 Qed.
 
 Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0.
-Proof. by apply/diff_unique; have [] := dcst a x. Qed.
+Proof. by apply/(@diff_unique _ _ _ \0); have [] := dcst a x. Qed.
 
 Variables (V W : normedModType R).
 
@@ -558,7 +558,10 @@ Proof. exact: DiffDef (differentiable_cst _ _) (diff_cst _ _). Qed.
 Lemma diffD (f g : V -> W) x :
   differentiable f x -> differentiable g x ->
   'd (f + g) x = 'd f x \+ 'd g x :> (V -> W).
-Proof. by move=> df dg; apply/diff_unique; have [] := dadd df dg. Qed.
+Proof.
+move=> df dg.
+by apply/(@diff_unique _ _ _ (GRing.add_fun _ _)); have [] := dadd df dg.
+Qed.
 
 Lemma differentiableD (f g : V -> W) x :
   differentiable f x -> differentiable g x -> differentiable (f + g) x.
@@ -576,7 +579,8 @@ Qed.
 Lemma differentiable_sum n (f : 'I_n -> V -> W) (x : V) :
   (forall i, differentiable (f i) x) -> differentiable (\sum_(i < n) f i) x.
 Proof.
-by elim/big_ind : _ => // ? ? g h ?; apply: differentiableD; [exact:g|exact:h].
+elim/big_ind : _ => //[_|? ? g h ?]; first exact/(@differentiable_cst _ 0).
+by apply: differentiableD; [exact:g|exact:h].
 Qed.
 
 Lemma diffN (f : V -> W) x :
@@ -614,7 +618,10 @@ Proof. by move=> /differentiableP df /differentiableP dg. Qed.
 
 Lemma diffZ (f : V -> W) k x :
   differentiable f x -> 'd (k *: f) x = k \*: 'd f x :> (V -> W).
-Proof. by move=> df; apply/diff_unique; have [] := dscale k df. Qed.
+Proof.
+move=> df.
+by apply/(@diff_unique _ _ _ (GRing.scale_fun _ _)); have [] := dscale k df.
+Qed.
 
 Lemma differentiableZ (f : V -> W) k x :
   differentiable f x -> differentiable (k *: f) x.
@@ -1152,7 +1159,7 @@ Global Instance is_derive_sum n (h : 'I_n -> V -> W) (x v : V)
   (dh : 'I_n -> W) : (forall i, is_derive x v (h i) (dh i)) ->
   is_derive x v (\sum_(i < n) h i) (\sum_(i < n) dh i).
 Proof.
-by elim/big_ind2 : _ => // [|] *; [exact: is_derive_cst|exact: is_deriveD].
+by elim/big_ind2 : _ => // [|] *; [exact/(is_derive_cst 0)|exact: is_deriveD].
 Qed.
 
 Lemma derivable_sum n (h : 'I_n -> V -> W) (x v : V) :
@@ -1324,7 +1331,10 @@ by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl.
 Qed.
 
 Lemma derivableX f n (x v : V) : derivable f x v -> derivable (f ^+ n) x v.
-Proof. by case: n => [_|n /derivableP]; [rewrite expr0|]. Qed.
+Proof.
+case: n => [_|n /derivableP]; last by [].
+by rewrite expr0; apply/(derivable_cst (1 : R)).
+Qed.
 
 Lemma deriveX f n (x v : V) : derivable f x v ->
   'D_v (f ^+ n.+1) x = (n.+1%:R * f x ^+ n) *: 'D_v f x.
@@ -1378,7 +1388,7 @@ Proof. by rewrite derive1E derive_cst. Qed.
 Lemma exprn_derivable {R : numFieldType} n (x : R) v :
   derivable (@GRing.exp R ^~ n) x v.
 Proof.
-elim: n => [/=|n ih]; first by rewrite (_ : _ ^~ _ = 1).
+elim: n => [/=|n ih]; first by rewrite (_ : _ ^~ _ = cst 1).
 rewrite (_ : _ ^~ _ = (fun x => x * x ^+ n)); last first.
   by apply/funext => y; rewrite exprS.
 by apply: derivableM; first exact: derivable_id.
@@ -1573,7 +1583,7 @@ have gcont : {within `[a, b], continuous g}.
   move=> x; apply: continuousD _ ; first by move=>?; exact: fcont.
   by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous.
 have gaegb : g a = g b.
-  rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
+  rewrite /g !add_funE !opp_funE.
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
   rewrite [_ *: _]mulrA mulrC mulrA mulVf.
     by rewrite mul1r addrCA subrr addr0.

theories/esum.v

@@ -587,9 +587,10 @@ move=> /cvgrPdist_lt cvgAB; apply/cvgrPdist_lt => e e0.
 move: cvgAB => /(_ _ e0) [N _/= hN] /=.
 near=> n.
 rewrite distrC subr0.
-have -> : (C_ = A_ \- B_)%R.
+have -> : (C_ = A_ - B_)%R.
   apply/funext => k.
-  rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//.
+  rewrite /= /A_ /C_ /B_ sub_funE/=.
+  rewrite -sumrN -big_split/= -summable_fine_sum//.
   apply eq_bigr => i Pi; rewrite -fineB//.
   - by rewrite [in LHS](funeposneg f).
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos.

theories/ftc.v

@@ -839,7 +839,8 @@ set f  := fun x => if x == a then r else if x == b then l else F^`() x.
 have fE : {in `]a, b[, F^`() =1 f}.
   by move=> x; rewrite in_itv/= => /andP[ax xb]; rewrite /f gt_eqF// lt_eqF.
 have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}.
-  move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp //; last first.
+  move=> x /[dup]xab /andP[ax xb].
+  rewrite (@derive1_comp _ _ (@GRing.opp R)) //; last first.
     apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP.
       by case: Fab => + _ _; exact.
     by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo.
@@ -886,7 +887,8 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
 - have [/= dF rF lF] := Fab.
   have := derivable_oo_continuous_bnd_within PGFbFa.
   move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]; split => /=.
-  - move=> x xab; apply/derivable1_diffP; apply: differentiable_comp => //.
+- move=> x xab; apply/derivable1_diffP.
+  apply: (differentiable_comp (g:[email protected] R)) => //.
     apply: differentiable_comp; apply/derivable1_diffP.
       by case: Fab => + _ _; exact.
     by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo.
@@ -909,7 +911,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
     rewrite gtr0_norm// ?subr_gt0//.
     by near: t; exact: nbhs_left_ltBl.
 apply: eq_integral_itv_bounded.
-- rewrite mulrN; apply: measurableT_comp => //.
+  - rewrite mulrN; apply: (measurableT_comp (f:[email protected] R)) => //.
   apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //.
     by move=> x; rewrite inE/= => xab; rewrite !fctE fE.
   by move: mGFF'; apply: measurable_funS => //; exact: subset_itv_oo_cc.
@@ -994,13 +996,14 @@ have mF' : measurable_fun `]a, b[ F^`().
   apply: subspace_continuous_measurable_fun => //.
   by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'.
 rewrite integral_itv_bndoo//; last first.
-  rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first.
+  rewrite (compA _ -%R) -(compA G -%R) (_ : -%R \o -%R = id); last first.
     by apply/funext => y; rewrite /= opprK.
-  apply: measurable_funM => //; apply: measurableT_comp => //.
+  apply: measurable_funM => //.
+  apply: (measurableT_comp (f:[email protected] R)) => //.
   apply: (@eq_measurable_fun _ _ _ _ _ (- F^`())%R).
     move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//.
     by case: Fab => + _ _; apply.
-  exact: measurableT_comp.
+  exact: (measurableT_comp (f:[email protected] R)).
 rewrite [in RHS]integral_itv_bndoo//; last exact: measurable_funM.
 apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN.
 - by rewrite opprK -derive1E.