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

uninteresting lemma? #382

Closed
affeldt-aist opened this issue May 28, 2021 · 2 comments · Fixed by #180
Closed

uninteresting lemma? #382

affeldt-aist opened this issue May 28, 2021 · 2 comments · Fixed by #180
Milestone
0.3.10

Comments

@affeldt-aist
Copy link
Member

affeldt-aist commented May 28, 2021 •
edited
Loading

analysis/theories/nngnum.v

Lines 179 to 182 in 8a8036f

(* TODO: general purpose lemma? add to mathcomp? *)
Lemma filter_andb I r (a P : pred I) :
[seq i <- r | P i && a i] = [seq i <- [seq j <- r | P j] | a i].
Proof. by elim: r => //= i r ->; case P. Qed.

during the 2021-05-27 meeting it was said to backport it to MathComp
but since it can be proven as

under eq_filter do rewrite andbC.
by rewrite filter_predI.

I wonder whether we should not jut get rid of it.
@affeldt-aist affeldt-aist added this to the 0.3.8 milestone May 28, 2021
@CohenCyril
Copy link
Member

I see... yes let's remove it.

@affeldt-aist affeldt-aist mentioned this issue May 28, 2021
Merged
3 tasks
@affeldt-aist
Copy link
Member Author

This will be taken care of by PR #180

@affeldt-aist affeldt-aist modified the milestones: 0.3.8, 0.3.9 May 29, 2021
@affeldt-aist affeldt-aist modified the milestones: 0.3.9, 0.3.10 Jun 14, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.3.10
Development

Successfully merging a pull request may close this issue.

Mathcomp master PseudoMetricNormedZmod math-comp/analysis
2 participants
@CohenCyril @affeldt-aist