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.

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

first step to integrate grobner to coqeal #70

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

thery
Copy link

@thery thery commented Dec 14, 2022

Adding the file grobner.v

@palmskog
Copy link
Member

This is great! But I think we need some documentation as well in the README.md to advertise the fact that we have a Gröbner basis and Buchberger algorithm formalization. It may be easiest to do this in a followup PR once this one is merged - I can do that documentation PR if @proux01 is OK with it.

@proux01
Copy link
Collaborator

proux01 commented Dec 14, 2022

@palmskog sure, feel free to open a separate documentation PR based on the current one, I'll rebase/merge it after the current one.

@proux01
Copy link
Collaborator

proux01 commented Dec 14, 2022

@thery thanks for the submission. I'd like to take some time to review it reasonably carefully, so please don't expect anything before next week.

Copy link
Collaborator

@proux01 proux01 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@thery I had only a rather quick look, but here are already a few comments.

theory/grobner.v Outdated Show resolved Hide resolved
theory/grobner.v Outdated
Comment on lines 160 to 165
Definition plt p q : bool :=
has (fun m2 =>
[&& m2 \notin msupp p,
all (fun m1 => ((m1 < m2)%O || (m1 \in msupp q))) (msupp p) &
all (fun m1 => ((m1 <= m2)%O || (m1 \in msupp p))) (msupp q)])
(msupp q).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it's a lexicographic order, why not defining it as

Import Order.DefaultSeqLexiOrder.

Definition ple p q : bool := (sort >=%O (msupp p) <= sort >=%O (msupp q))%O.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've used it but I am not sure it makes my life easier.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not expecting it to make life easier by itself, but it seems to me that some lemmas in grobner.v are just generic properties on lexicographic orders. If they are not in order.v they could be added first in ssrcomplents (and later backported). I would expect this to simplify proofs in grobner.v while providing more reusable material.

Qed.

Lemma plt_msuppl (p q r : {mpoly R[n]}) :
perm_eq (msupp p) (msupp q) -> (p < r) = (q < r).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's rather a question related to multinomials, but those perm_eq make me wonder whether msupp should not be defined as sort >=%O (dom p) or something like that?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is that there is many notion of orders in polynomial. There is no reason to fix one.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure but not fixing any order means msupp currently has no canonical form, hence this kind of lemmas with perm_eq. Multinomials chose an order on monomials, I think it makes some sense to use it to make msupp canonical (as offered in math-comp/multinomials#66 ). Even if this order is somewhat arbitrary, it seems better than no order.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe msupp should take an order as parameter?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe. Can I let you try that in multinomials? ( math-comp/multinomials#66 should be a good starting point)

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am trying

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

not very successful. It starts going wrong here.
Now that mlead is parametrized most theorems need extra properties on the order that I don't know
how to package.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't have any good solution right now.
Best short term solution is probably to use a functor to put generic lemmas taking a module with the order properties as argument. This functor could then be instantiated to get the lemmas for any specific order.
A better solution would probably be to have order structures on relations (o : rel T) instead of just types (T), like Monoid in bigop, maybe something to discuss in a forthcoming MathComp meeting (maybe @pi8027 would have a better idea).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants