Instances for dependent function types #1383

Tragicus · 2024-11-05T15:46:02Z

Motivation for this change

Generalizes the instances on function types to dependent function types. The same generalization is happening in mathcomp (see math-comp/math-comp#1256) and it needs to be done here first for backwards compatibility.

Checklist

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

Read this Checklist
Put a milestone if possible
Check labels

affeldt-aist · 2024-11-06T13:53:59Z

altreals/realseq.v

@@ -303,7 +303,7 @@ Lemma ncvgM u v lu lv : ncvg u lu%:E -> ncvg v lv%:E ->
 Proof.
 move=> cu cv; pose a := u \- lu%:S; pose b := v \- lv%:S.
 have eq: (u \* v) =1 (lu * lv)%:S \+ ((lu%:S \* b) \+ (a \* v)).
-  move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.
+move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.


Suggested change

move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.

move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.

affeldt-aist · 2024-11-06T13:55:28Z

classical/functions.v

 Next Obligation.
-by move=> T M ; apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0.
+by move=> T M f g h; apply/functional_extensionality_dep => x /=; rewrite addrA.


We have funext for non-dependent functional extensionality.
Maybe we should introduce funext_dep for uniformity and to save some typing.

affeldt-aist · 2024-11-06T13:56:00Z

classical/functions.v

+Proof.
+by apply/funext => x/=; rewrite mulrC. Qed.


Suggested change

Proof.

by apply/funext => x/=; rewrite mulrC. Qed.

Proof. by apply/funext => x/=; rewrite mulrC. Qed.

affeldt-aist · 2024-11-06T13:57:06Z

theories/derive.v

@@ -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.


This looks indeed a bit better ^_^.

affeldt-aist · 2024-11-06T14:00:05Z

theories/derive.v

@@ -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 (f:=GRing.sub_fun _ _))/eqoP.


It is desirable to avoid using (f:= ...) because it relies on the naming of a variable that is likely to change. (There are instances of this issue below with df:=.)

affeldt-aist · 2024-11-06T14:01:02Z

theories/derive.v

@@ -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).
+apply: differentiableD; [exact:g|exact:h].


Suggested change

apply: differentiableD; [exact:g|exact:h].

by apply: differentiableD; [exact:g|exact:h].

affeldt-aist · 2024-11-06T14:02:06Z

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 (g:[email protected] R)) //; last first.


Maybe avoid the (g:= ...) syntax if possible.

affeldt-aist · 2024-11-06T14:04:22Z

theories/lebesgue_measure.v

@@ -1002,7 +1002,9 @@ Qed.

 Lemma measurable_funB D f g : measurable_fun D f ->
  measurable_fun D g -> measurable_fun D (f \- g).
-Proof. by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp. Qed.
+Proof.
+move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp.


Suggested change

move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp.

by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp.

affeldt-aist · 2024-11-06T14:15:09Z

theories/lebesgue_integral.v

@@ -251,7 +251,7 @@ Context d (aT : measurableType d) (rT : realType).
 Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT).
 Proof.
 split=> [|f g|f g]; rewrite !inE/=.
- exact: measurable_cst.
+- exact: measurable_cst (1 : rT).


Mmmhhh... There are now plenty of lemma applications with blah_cst lemmas that now require an explicit mention of the constant in question. This looks problematic.

affeldt-aist · 2024-11-06T14:21:29Z

theories/derive.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)).


Indeed, if I remove the (1 : R) type checking does not seem to terminate. Do you know why?

affeldt-aist

What is the justification for the mandatory addition of constants for the application of blah_cst lemmas? Do we know where the problem comes from?

affeldt-aist · 2024-11-06T14:40:15Z

I observe that this PS shares similarities with PR #1379 while the latter is marked as draft. Maybe you intended this one as well to be a draft?

Tragicus · 2024-11-06T15:47:54Z

What is the justification for the mandatory addition of constants for the application of blah_cst lemmas? Do we know where the problem comes from?

cst is not dependent (and can not be), so I can not define the operations on dependent functions using it. Then, when Rocq tries to unify cst ?c with 1 : U -> V, it reduces the problem to fun=> ?c = fun t : U => GRing.one ((fun=> V) t) and then to ?c = GRing.one ((fun=> V) t). This fails because ?c can not use t in its instantiation. I believe I have a solution for that, but it needs to be integrated into Coq, so it will take some time, and the impact looks minor according to the CI.

Tragicus · 2024-11-06T15:49:48Z

I extracted this from the other PR and extended it when I realized I needed to generalize things here first. It is ready for review.

affeldt-aist reviewed Nov 6, 2024

View reviewed changes

affeldt-aist self-requested a review November 6, 2024 14:21

affeldt-aist requested changes Nov 6, 2024

View reviewed changes

affeldt-aist mentioned this pull request Nov 6, 2024

Structures with one operation math-comp/math-comp#1256

Open

7 tasks

instances for dependent function types

b6c10bc

Tragicus force-pushed the dep-inst branch from 38a49d4 to b6c10bc Compare November 6, 2024 16:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Instances for dependent function types #1383

Instances for dependent function types #1383

Tragicus commented Nov 5, 2024

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024 •

edited

Loading

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024

affeldt-aist Nov 6, 2024

affeldt-aist left a comment •

edited

Loading

affeldt-aist commented Nov 6, 2024

Tragicus commented Nov 6, 2024

Tragicus commented Nov 6, 2024

	move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.
	move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.

	Proof.
	by apply/funext => x/=; rewrite mulrC. Qed.
	Proof. by apply/funext => x/=; rewrite mulrC. Qed.

	apply: differentiableD; [exact:g\|exact:h].
	by apply: differentiableD; [exact:g\|exact:h].

	move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp.
	by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp.

Instances for dependent function types #1383

Are you sure you want to change the base?

Instances for dependent function types #1383

Conversation

Tragicus commented Nov 5, 2024

Motivation for this change

Checklist

Reminder to reviewers

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

affeldt-aist Nov 6, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

affeldt-aist left a comment • edited Loading

Choose a reason for hiding this comment

affeldt-aist commented Nov 6, 2024

Tragicus commented Nov 6, 2024

Tragicus commented Nov 6, 2024

affeldt-aist Nov 6, 2024 •

edited

Loading

affeldt-aist left a comment •

edited

Loading