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

Jump to bottom

Adding some trigonometry in realType #383

Merged
merged 45 commits into from
Dec 22, 2021
Merged

Adding some trigonometry in realType #383

merged 45 commits into from
Dec 22, 2021

Conversation

thery
Copy link
Member

@thery thery commented Jun 1, 2021 •
edited by affeldt-aist
Loading

This is just an attempt and is not meant to be merged.

We have added an extra file in exp.v that contains the defs of functions like exp sinand cos.

NB: lemma sum_group (now big_nat_mul) submitted to mathcomp (math-comp/math-comp#782)

NB: lemmas divr_eq (now eqr_div) and sqrtrV submitted to mathcomp (math-comp/math-comp#789)

@affeldt-aist affeldt-aist marked this pull request as draft June 1, 2021 00:52
@thery
Copy link
Member Author

thery commented Jun 1, 2021 •
edited
Loading

Don't understand why the CI fails, it works on my machine.
I cannot do a Require Import Nsatz because there is a Notation clash on -->
but the tactic should be there

Fixed

@thery thery added the experiment 🧪 This issue/PR is very experimental label Jun 1, 2021
@CohenCyril
Copy link
Member

Looks really promising to me :)

CohenCyril
CohenCyril reviewed Jun 1, 2021
View reviewed changes
theories/exp.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist mentioned this pull request Jun 3, 2021
Open
CohenCyril
CohenCyril reviewed Jun 7, 2021
View reviewed changes
theories/exp.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist marked this pull request as ready for review June 8, 2021 09:09
@affeldt-aist affeldt-aist added enhancement ✨ This issue/PR is about adding new features enhancing the library and removed experiment 🧪 This issue/PR is very experimental labels Jun 8, 2021
@affeldt-aist affeldt-aist mentioned this pull request Jun 9, 2021
Merged
@thery
Copy link
Member Author

thery commented Jul 8, 2021

This PR depends on #385. As soon as it is merged we can remove the file inverse_continuous.v

@thery thery force-pushed the exp branch 2 times, most recently from b01380e to b0b6bc4 Compare July 8, 2021 23:36
@affeldt-aist affeldt-aist mentioned this pull request Sep 13, 2021
Merged
1 task
@affeldt-aist
Copy link
Member

Should we try to submit sqrtrV and divr_eq to MathComp before its 1.13 release?

@affeldt-aist affeldt-aist mentioned this pull request Sep 24, 2021
Merged
1 task
@thery
Copy link
Member Author

thery commented Oct 14, 2021

@affeldt-aist what is left to be done?

@affeldt-aist
Copy link
Member

@affeldt-aist what is left to be done?

I think it is mostly about putting the lemmas in the right files.

@thery thery changed the title Initial attempt to have some trigonometry in realType Adding some trigonometry in realType Oct 14, 2021
CohenCyril
CohenCyril reviewed Oct 14, 2021
View reviewed changes
theories/exp.v Outdated Show resolved Hide resolved
@thery
Copy link
Member Author

thery commented Oct 14, 2021

is it normal the CI does not make it to build big_enough?

@CohenCyril
Copy link
Member

is it normal the CI does not make it to build big_enough?

I'm clueless, I've been banging my head on it since this morning in another repo...
https://github.com/math-comp/Abel/pull/71/checks?check_run_id=3894379682

@affeldt-aist affeldt-aist mentioned this pull request Oct 15, 2021
Merged
1 task
CohenCyril
CohenCyril reviewed Oct 15, 2021
View reviewed changes
theories/topology.v Outdated Show resolved Hide resolved
affeldt-aist and others added 14 commits December 21, 2021 18:07
@affeldt-aist
use more notations and changelog
1c85ddd 
- use more mono, morph, etc. notations
- split exp.v into two files
@thery @affeldt-aist
typo
951c733
@affeldt-aist
doc, changelog, shorter proofs
d9b22cf 
- cos_inj using ltr_cos
- complete changelog and shorten proofs
- header to nsatz_realType.v
@thery @affeldt-aist
derivation results
aaf0e76 
- derivative of ln
- derivation of acos asin atan
- derivative of atan without axiom
@affeldt-aist
complete changelog
5b59d1f
@thery @affeldt-aist
Thanks to Yves no admit!
b8431ac
@affeldt-aist
minor improvements and fixes
290206f 
- generalize is_derive1_id
- rename following mathcomp
- update w.r.t. master
- fix changelog
- proof optimization
@thery @affeldt-aist
Add multi rule for unfolding functional expression
2b6ea0f 
- rename chain -> comp
- remove comment
- moving cvg
@affeldt-aist
minor improvements
1bc5787 
- use bounded_fun in cvg_series_bounded
- move continuous/shift lemmas and multirule
@thery @affeldt-aist
update changelog
3faf423
@affeldt-aist
remove *_group2 lemma
b3e81d7
@thery @affeldt-aist
fixes and simplification
8483da7 
- simplify proofs using is_derive_0_cst
- renaming rcfE -> fctE
- remove [arguments]
@thery @affeldt-aist
introduction of formal series
3c332e7 
- update comment in exp.v
- minor fixes (missing nl, in trigo.v)
- more pseries
@thery @affeldt-aist
fix is_derive automation
d64c4b6 
- fix is_derive resolution
- more precise pattern for Hint
@affeldt-aist
Copy link
Member

I made a last pass and hopefully addressed comments from the last meeting. Ready to merge.

@affeldt-aist
fixes
4fc2788 
- formatting, documentation, changelog, rebase
@affeldt-aist affeldt-aist merged commit af7eb34 into math-comp:master Dec 22, 2021
@CohenCyril
Copy link
Member

45 commits 😢

@CohenCyril
Copy link
Member

45 commits cry

next time, please squash

@thery
Copy link
Member Author

thery commented Dec 22, 2021 •
edited
Loading

@CohenCyril can't we configure github so that it automatically squashes merge?

@thery thery deleted the exp branch December 22, 2021 20:41
@CohenCyril
Copy link
Member

@CohenCyril can't we configure github so that it automatically squashes merge?

Not that I know of...

@thery
Copy link
Member Author

thery commented Dec 22, 2021

@CohenCyril it seems it is possible :
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/configuring-commit-squashing-for-pull-requests

@affeldt-aist
Copy link
Member

Note that several contiguous commits were actually squashed before merge (commits that were just minor fixes or that were actually incremental progress).

@thery
Copy link
Member Author

thery commented Dec 23, 2021

@CohenCyril it seems it is possible :
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/configuring-commit-squashing-for-pull-requests

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

Assignees
No one assigned
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Milestone
0.3.12
Development

Successfully merging this pull request may close these issues.
4 participants
@thery @CohenCyril @affeldt-aist @gares