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

Adding allrel predicate #558

Merged
merged 1 commit into from Sep 3, 2020
Merged

Adding allrel predicate #558

merged 1 commit into from Sep 3, 2020

Conversation

CohenCyril
Copy link
Member

Motivation for this change

This predicate is useful in stating that a sequence of matrices all commute.
This is a part of #207.

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

@CohenCyril
Copy link
Member Author

@gares, @pi8027, @strub can one of you assign themselves?

@CohenCyril CohenCyril added this to the 1.12.0 milestone Sep 1, 2020
@gares gares self-assigned this Sep 1, 2020
@gares
Copy link
Member

gares commented Sep 1, 2020

It looks ok to me, but I'm not in love with the are_ part of the name. Is it similar to something already existing?

mathcomp/ssreflect/seq.v Outdated Show resolved Hide resolved
mathcomp/ssreflect/seq.v Outdated Show resolved Hide resolved
mathcomp/ssreflect/seq.v Outdated Show resolved Hide resolved
@chdoc
Copy link
Member

chdoc commented Sep 1, 2020

Also, is it useful to have T : nonPropType rather than T : eqType while requiring r : rel T to be a boolean relation? I mean, the proof of are_allpairs_cons is nifty, but I would have expected a simpler proof based in are_allpairsP.

@CohenCyril
Copy link
Member Author

Also, is it useful to have T : nonPropType rather than T : eqType while requiring r : rel T to be a boolean relation? I mean, the proof of are_allpairs_cons is nifty, but I would have expected a simpler proof based in are_allpairsP.

It may happen that a relation is decidable even on some non discrete types (e.g. a pair of an ordered type with a no discrete type), and I would like to preserve the full generality of the theorem on such occurences.

@CohenCyril
Copy link
Member Author

CohenCyril commented Sep 1, 2020

It looks ok to me, but I'm not in love with the are_ part of the name. Is it similar to something already existing?

I went back and forth a lot in the naming: the working name was the ugly all11 (hence the 80 character overflow caused by sed)...
I am open to suggestions on the naming but I was pretty happy with this one being meaningful ("Are all pairs satisfying r on s?") and exposing the implementation using allpairs in the name itself..

@CohenCyril
Copy link
Member Author

Actually I would have gone for is except are is grammatically more accurate (since it is about a relation, not a predicate).

@chdoc
Copy link
Member

chdoc commented Sep 1, 2020

Well, the predicate states that "all pairs of s are in the relation r" (using the usual mathematical speak of relations as sets/predicates). So how about allpairs_in r s? For this one even the partial application allpairs_in r seems reasonable to me. Unfortunately in is used differently elsewhere.

@chdoc
Copy link
Member

chdoc commented Sep 1, 2020

In any event, are_allpairs r s is a proposition not a question. So even allpairs_are r s ("all pairs are r(-related)") seems preferable to me.

@gares
Copy link
Member

gares commented Sep 1, 2020

So even allpairs_are r s ("all pairs are r(-related)") seems preferable to me.

+1

To me the thing is messy because allpairs does not really build pairs but steals the name. If we had a pairs thing that builds the sequence of all pairs, we could use allpairs for your new concept, eg allpairs r xs := all (fixup r) (pairs xs xs).

@chdoc
Copy link
Member

chdoc commented Sep 1, 2020

To me the thing is messy because allpairs does not really build pairs but steals the name.

While the string "allpairs" appears in a considerable number of of lemmas, the definition allpairs seems to be virtually unused, because allpairs is (almost) always inlined. The only lemma about allpairs in ssreflect and algebra appears to be allpairs_tupleP. 🤔

@CohenCyril
Copy link
Member Author

To me the thing is messy because allpairs does not really build pairs but steals the name.

While the string "allpairs" appears in a considerable number of of lemmas, the definition allpairs seems to be virtually unused, because allpairs is (almost) always inlined. The only lemma about allpairs in ssreflect and algebra appears to be allpairs_tupleP.

allpairs actually immediately unfolds to the idiom [seq f x y | x <- s, y <- t x] which gives its name to the lemmas, and it is a rather historic convention (the self-expanding definition is newer as far as I remember). Moreover it indeed does not form pairs but applies a function symbol f to them (and this function symbol can be dependent), sometimes it's a pair, sometimes a sigT and sometimes something else, so it makes it more flexible to let f variable.

I'm all in favor of allpairs_areanyway!

@gares
Copy link
Member

gares commented Sep 2, 2020

I saw that, allpairs maps a function overs all the pairs, which could be named, to me, map_allpairs. Anyway, I'm OK with the renaming proposed by @chdoc

@CohenCyril
Copy link
Member Author

CohenCyril commented Sep 2, 2020

I fixed the names, made the proof shorter and more readable and introduced the mkseqP idiom.

@CohenCyril CohenCyril changed the title Adding are_allpairs predicate Adding allpairs_are predicate Sep 2, 2020
mathcomp/ssreflect/seq.v Outdated Show resolved Hide resolved
@CohenCyril
Copy link
Member Author

CohenCyril commented Sep 2, 2020

I have a new name suggestion: how about allrel?
Pros:

  • stands for "all related"
  • has rel and all in the name (and no more)
  • shorter

@chdoc
Copy link
Member

chdoc commented Sep 2, 2020

I have a new name suggestion: how about allrel?

I approve, in particular because it avoids the _, leading to nicer lemma names.

@CohenCyril CohenCyril changed the title Adding allpairs_are predicate Adding allrel predicate Sep 2, 2020
Copy link
Member

@chdoc chdoc left a comment

Choose a reason for hiding this comment

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

LGTM (apart from the grammar error in the changelog 😏 )

CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
@CohenCyril CohenCyril force-pushed the are_allpairs branch 3 times, most recently from 5ba0d6f to bf7d1d3 Compare September 3, 2020 01:17
@CohenCyril
Copy link
Member Author

CohenCyril commented Sep 3, 2020

@gares all good?

@gares gares merged commit d3950a3 into math-comp:master Sep 3, 2020
@CohenCyril CohenCyril deleted the are_allpairs branch September 3, 2020 13:55
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.

None yet

3 participants