Skip to content
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

adapt to coq#19611 #1377

Merged
merged 1 commit into from
Oct 30, 2024
Merged

adapt to coq#19611 #1377

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 classical/functions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1253,7 +1253,7 @@ Lemma odflt_unbind : odflt x = unbind (fun=> x) idfun. Proof. by []. Qed.
HB.instance Definition _ := Inv.Build _ _ (odflt x) some.

HB.instance Definition _ := SplitBij.copy (odflt x)
[the {bij some @` A >-> A} of unbind (fun=> x) idfun].
[the {splitbij some @` A >-> A} of @unbind (option T) T (fun=> x) idfun].

End Odflt.

Expand Down
2 changes: 1 addition & 1 deletion classical/mathcomp_extra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ Lemma ler_sqrt {R : rcfType} (a b : R) :
(0 <= b -> (Num.sqrt a <= Num.sqrt b) = (a <= b))%R.
Proof.
have [b_gt0 _|//|<- _] := ltgtP; last first.
by rewrite sqrtr0 -sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF.
by rewrite sqrtr0 -[RHS]sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF.
have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt// ?qualifE/= ?ltW.
by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW.
Qed.
Expand Down
2 changes: 1 addition & 1 deletion theories/exp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -974,7 +974,7 @@ have ap0 : (0 < a `^ p)%R by rewrite powR_gt0.
have bq0 : (0 < b `^ q)%R by rewrite powR_gt0.
have := @concave_ln _ (@Itv.mk _ `[0, 1] _ q01)%R _ _ ap0 bq0.
have pq' : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK.
rewrite !convRE/= /onem -pq' -ler_expR expRD (mulrC p^-1).
rewrite !convRE/= /onem -pq' -[_ <= ln _]ler_expR expRD (mulrC p^-1).
rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF// (mulrC q^-1).
rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF//.
rewrite lnK ?posrE// lnK ?posrE// => /le_trans; apply.
Expand Down