Skip to content

Port analysis to new rewrite goals order #1919

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
proux01 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Port analysis to new rewrite goals order #1919

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion theories/borel_hierarchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ From mathcomp Require Import measure lebesgue_measure measurable_realfun.
(* *)
(******************************************************************************)

Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Expand Down
4 changes: 2 additions & 2 deletions theories/cantor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ From mathcomp Require Import cardinality reals topology.
(* *)
(******************************************************************************)

Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Expand Down Expand Up @@ -196,7 +196,7 @@ Unshelve. all: end_near. Qed.
Let apx_prefix b c n :
(forall i, (i < n)%N -> b i = c i) -> branch_apx b n = branch_apx c n.
Proof.
elim: n => //= n IH inS; rewrite IH; first by rewrite inS.
elim: n => //= n IH inS; rewrite IH; last by rewrite inS.
by move=> ? ?; exact/inS/ltnW.
Qed.

Expand Down
254 changes: 126 additions & 128 deletions theories/charge.v
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion theories/convex.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ From mathcomp Require Import reals topology.

Reserved Notation "x <| p |> y" (format "x <| p |> y", at level 49).

Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Expand Down
54 changes: 27 additions & 27 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau.
(* *)
(******************************************************************************)

Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Expand Down Expand Up @@ -196,9 +196,9 @@ Lemma differentiable_continuous (x : V) (f : V -> W) :
differentiable f x -> {for x, continuous f}.
Proof.
move=> /diff_locallyP [dfc]; rewrite -addrA.
rewrite (littleo_bigO_eqo (cst (1 : R))); last first.
rewrite (littleo_bigO_eqo (cst (1 : R))).
by apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1; near do by [].
rewrite addfo; first by move=> /eqolim; rewrite cvg_comp_shift add0r.
rewrite addfo; last by move=> /eqolim; rewrite cvg_comp_shift add0r.
by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
Unshelve. all: by end_near. Qed.

Expand Down Expand Up @@ -335,7 +335,7 @@ Lemma deriveE (f : V -> W) (a v : V) :
differentiable f a -> 'D_v f a = 'd f a v.
Proof.
rewrite /derive => /diff_locally -> /=; set k := 'o _.
evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=.
rewrite funeqE=> h.
by rewrite -[_ - _]addrA addrC subrKA scalerDr addrC linearZ scalerA /g.
apply: cvg_lim => //.
Expand All @@ -348,7 +348,7 @@ rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
rewrite /g2.
have [->|v0] := eqVneq v 0.
rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst.
rewrite (_ : (fun _ => _) = cst 0); last exact: cvg_cst.
by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0.
apply/cvgrPdist_lt => e e0.
rewrite nearE /=; apply/nbhs_ballP.
Expand All @@ -361,7 +361,7 @@ rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //.
have /Hi/le_lt_trans -> // : ball 0 i (j *: v).
by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ.
rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulKf ?gt_eqF// normfV invrK.
rewrite ltr_pdivrMl; last by rewrite pmulr_rgt0 // normr_gt0.
rewrite ltr_pdivrMl; first by rewrite pmulr_rgt0 // normr_gt0.
rewrite normrZ mulrC -mulrA.
by rewrite ltr_pMl ?ltr1n // pmulr_rgt0 ?normm_gt0 // normr_gt0.
Qed.
Expand Down Expand Up @@ -422,7 +422,7 @@ Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\
Proof.
split; first exact: cst_continuous.
apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _).
by rewrite littleoE; last exact: littleo0_subproof.
by rewrite littleoE; first exact: littleo0_subproof.
Qed.

Variables (V W : normedModType R).
Expand Down Expand Up @@ -477,7 +477,7 @@ Fact dlin (V' W' : normedModType R) (f : {linear V' -> W'}) x :
Proof.
move=> df; apply: eqaddoE; rewrite funeqE => y /=.
rewrite linearD addrC -[LHS]addr0; congr (_ + _).
by rewrite littleoE; last exact: littleo0_subproof. (*fixme*)
by rewrite littleoE; first exact: littleo0_subproof. (*fixme*)
Qed.

(* TODO: generalize *)
Expand Down Expand Up @@ -529,7 +529,7 @@ apply/ler_gtP => _ /posnumP[e]; rewrite ler_pdivrMr //.
have /oid /nbhs_ballP [_ /posnumP[d] dfe] := [elaborate gt0 e].
set k := ((d%:num / 2) / (PosNum xn0)%:num)^-1.
rewrite -{1}(@scalerKV _ _ k _ x) /k // linearZZ normrZ.
rewrite -ler_pdivlMl; last by rewrite gtr0_norm.
rewrite -ler_pdivlMl; first by rewrite gtr0_norm.
rewrite mulrCA (@le_trans _ _ (e%:num * `|k^-1 *: x|)) //; last first.
by rewrite ler_pM // normrZ normfV.
apply: dfe; rewrite -ball_normE /= sub0r normrN normrZ.
Expand Down Expand Up @@ -592,7 +592,7 @@ Global Instance is_diffD (f g df dg : V -> W) x :
is_diff x f df -> is_diff x g dg -> is_diff x (f + g) (df + dg).
Proof.
move=> dfx dgx; apply: DiffDef; first exact: differentiableD.
by rewrite diffD; first (congr (_ + _); apply: diff_val).
by rewrite diffD; last (congr (_ + _); apply: diff_val).
Qed.

Lemma differentiable_sum n (f : 'I_n -> V -> W) (x : V) :
Expand Down Expand Up @@ -988,7 +988,7 @@ move=> /le_trans -> //; rewrite [leLHS]mulrC ler_pM ?mulr_ge0 //.
near: h; exists (`|x| / 2); first by rewrite /= divr_gt0 ?normr_gt0.
move=> h; rewrite /= distrC subr0 => lthhx; rewrite addrC -[h]opprK.
apply: le_trans (@ler_dist_dist _ R _ _).
rewrite normrN [leRHS]ger0_norm; last first.
rewrite normrN [leRHS]ger0_norm.
rewrite subr_ge0; apply: ltW; apply: lt_le_trans lthhx _.
by rewrite ler_pdivrMr // -{1}(mulr1 `|x|) ler_pM // ler1n.
rewrite lerBrDr -lerBrDl (splitr `|x|).
Expand Down Expand Up @@ -1144,7 +1144,7 @@ Fact der_add f g (x v : V) : derivable f x v -> derivable g x v ->
0^' --> 'D_v f x + 'D_v g x.
Proof.
move=> df dg.
evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=; last first.
evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=.
rewrite funeqE => h.
by rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr /fg.
exact: cvgD.
Expand Down Expand Up @@ -1195,7 +1195,7 @@ Fact der_opp f (x v : V) : derivable f x v ->
(fun h => h^-1 *: (((- f) \o shift x) (h *: v) - (- f) x)) @
0^' --> - 'D_v f x.
Proof.
move=> df; evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
move=> df; evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=.
by rewrite funeqE => h; rewrite !scalerDr !scalerN -opprD -scalerBr /g.
exact: cvgN.
Qed.
Expand Down Expand Up @@ -1231,7 +1231,7 @@ Fact der_scal f (k : R) (x v : V) : derivable f x v ->
(fun h => h^-1 *: ((k \*: f \o shift x) (h *: v) - (k \*: f) x)) @
0^' --> k *: 'D_v f x.
Proof.
move=> df; evar (h : R -> W); rewrite [X in X @ _](_ : _ = h) /=; last first.
move=> df; evar (h : R -> W); rewrite [X in X @ _](_ : _ = h) /=.
rewrite funeqE => r.
by rewrite scalerBr !scalerA mulrC -!scalerA -!scalerBr /h.
exact: cvgZl_tmp.
Expand Down Expand Up @@ -1296,7 +1296,7 @@ Fact der_mult f g x v :
0^' --> f x *: 'D_v g x + g x *: 'D_v f x.
Proof.
move=> df dg.
evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=; last first.
evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=.
rewrite funeqE => h.
have -> : (f * g) (h *: v + x) - (f * g) x =
f (h *: v + x) *: (g (h *: v + x) - g x) + g x *: (f (h *: v + x) - f x).
Expand Down Expand Up @@ -1428,7 +1428,7 @@ 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).
rewrite (_ : _ ^~ _ = (fun x => x * x ^+ n)); last first.
rewrite (_ : _ ^~ _ = (fun x => x * x ^+ n)).
by apply/funext => y; rewrite exprS.
by apply: derivableM; first exact: derivable_id.
Qed.
Expand Down Expand Up @@ -1471,7 +1471,7 @@ have [_ [t tA <-]] : exists2 y, (f @` A) y & sup (f @` A) - k^-1 < y.
by apply: sup_adherent => //; rewrite invr_gt0.
rewrite ltrBlDr -ltrBlDl.
suff : sup (f @` A) - f t > k^-1 by move=> /ltW; rewrite leNgt => /negbTE ->.
rewrite invf_plt ?posrE ?subr_gt0 ?AfsupfA//; last exact/mem_set.
rewrite invf_plt ?posrE ?subr_gt0 ?AfsupfA//; first exact/mem_set.
by rewrite (le_lt_trans (ler_norm _))// imVfltk//; exact: imageP.
Qed.

Expand Down Expand Up @@ -1540,7 +1540,7 @@ Lemma derive1_at_max (R : realFieldType) (f : R -> R) (a b c : R) :
Proof.
move=> leab fdrvbl cab cmax; apply: DeriveDef; first exact: fdrvbl.
apply/eqP; rewrite eq_le; apply/andP; split.
rewrite ['D_1 f c]cvg_at_rightE; last exact: fdrvbl.
rewrite ['D_1 f c]cvg_at_rightE; first exact: fdrvbl.
apply: limr_le.
have /fdrvbl dfc := cab.
rewrite -(cvg_at_rightE (fun h : R => h^-1 *: ((f \o shift c) _ - f c))) //.
Expand All @@ -1554,7 +1554,7 @@ apply/eqP; rewrite eq_le; apply/andP; split.
move=> h; rewrite /= distrC subr0 /= in_itv /= -ltrBrDr.
move=> /(le_lt_trans (ler_norm _)) -> /ltr_pDl -> //.
by rewrite (itvP cab).
rewrite ['D_1 f c]cvg_at_leftE; last exact: fdrvbl.
rewrite ['D_1 f c]cvg_at_leftE; first exact: fdrvbl.
apply: limr_ge.
have /fdrvbl dfc := cab; rewrite -(cvg_at_leftE (fun h => h^-1 *: ((f \o shift c) _ - f c))) //.
apply: cvg_trans dfc; apply: cvg_app.
Expand All @@ -1575,7 +1575,7 @@ Lemma derive1_at_min (R : realFieldType) (f : R -> R) (a b c : R) :
Proof.
move=> leab fdrvbl cab cmin; apply: DeriveDef; first exact: fdrvbl.
apply/eqP; rewrite -oppr_eq0; apply/eqP.
rewrite -deriveN; last exact: fdrvbl.
rewrite -deriveN; first exact: fdrvbl.
suff df : is_derive c 1 (- f) 0 by rewrite derive_val.
apply: derive1_at_max leab _ (cab) _ => t tab; first exact/derivableN/fdrvbl.
by rewrite lerN2; apply: cmin.
Expand Down Expand Up @@ -1606,7 +1606,7 @@ exists ((a + b) / 2) => //; apply: derive1_at_max (ltW ltab) fdrvbl (midab) _.
move=> t tab.
suff fcst s : s \in `]a, b[%R -> f s = f cmax by rewrite !fcst.
move=> sab.
apply/eqP; rewrite eq_le fcmax; last by rewrite in_itv /= !ltW ?(itvP sab).
apply/eqP; rewrite eq_le fcmax; first by rewrite in_itv /= !ltW ?(itvP sab).
suff -> : f cmax = f cmin by rewrite fcmin // in_itv /= !ltW ?(itvP sab).
by move: cmaxeaVb cmineaVb; rewrite 2!inE => -[|] -> [|] ->.
Qed.
Expand All @@ -1626,7 +1626,7 @@ have gcont : {within `[a, b], continuous g}.
have gaegb : g a = g b.
rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
rewrite [_ *: _]mulrC divfK; first by rewrite addrC subrK.
rewrite [_ *: _]mulrC divfK; last by rewrite addrC subrK.
by apply: lt0r_neq0; rewrite subr_gt0.
have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
exists c; first exact: cab.
Expand Down Expand Up @@ -1705,7 +1705,7 @@ suff : {in Interval (BSide sa a) (BSide sb b) &, {homo (- f) : x y / x <= y}}.
by move=> h y x iy ix xy; move: (h x y ix iy xy); rewrite opprfctE lerNl opprK.
apply: ger0_derive1_le.
- move => x xab; exact/derivableN/df.
- move => x xab; rewrite derive1E deriveN; last exact: df.
- move => x xab; rewrite derive1E deriveN; first exact: df.
by rewrite -derive1E oppr_ge0 dfle0.
by move=> x; exact/continuousN/cf.
Qed.
Expand Down Expand Up @@ -1812,7 +1812,7 @@ suff : {in Interval (BSide sa a) (BSide sb b) &, {homo (- f) : x y / x < y}}.
by move=> h x y ix iy xy; move: (h y x iy ix xy); rewrite opprfctE ltrNl opprK.
apply: gtr0_derive1_lt.
- move => x xab; exact/derivableN/df.
- move => x xab; rewrite derive1E deriveN; last exact: df.
- move => x xab; rewrite derive1E deriveN; first exact: df.
by rewrite -derive1E oppr_gt0 dflt0.
by move=> x; exact/continuousN/cf.
Qed.
Expand Down Expand Up @@ -2063,7 +2063,7 @@ Lemma derive1_comp (R : realFieldType) (f g : R -> R) x :
(g \o f)^`() x = g^`()%classic (f x) * f^`()%classic x.
Proof.
move=> /derivable1_diffP df /derivable1_diffP dg.
rewrite derive1E'; last exact/differentiable_comp.
rewrite derive1E'; first exact/differentiable_comp.
rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1.
by rewrite [LHS]linearZ mulrC.
Qed.
Expand Down Expand Up @@ -2240,9 +2240,9 @@ Proof.
apply/funext => x; elim/poly_ind: p => [|p r ih].
by rewrite deriv0 hornerC horner0_ext derive1_cst.
rewrite derivD hornerD hornerD_ext.
rewrite derive1E deriveD//; [|exact: derivable_horner..].
rewrite derive1E deriveD//; [exact: derivable_horner..|].
rewrite -!derive1E hornerC_ext derive1_cst addr0.
rewrite horner_scale_ext derive1E deriveM//; last exact: derivable_horner.
rewrite horner_scale_ext derive1E deriveM//; first exact: derivable_horner.
rewrite derive_id -derive1E -ih derivC horner0 addr0 derivM hornerD !hornerE.
by rewrite derivX hornerE mulr1 addrC mulrC scaler1.
Qed.
Expand Down
Loading
Loading