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

Making Theorem with more flexible + code cleanup #18743

Merged
merged 6 commits into from May 16, 2024
Merged

Making Theorem with more flexible + code cleanup #18743

merged 6 commits into from May 16, 2024

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Mar 4, 2024 •
edited

The PR simplifies Theorem with and makes it more flexible:

  • We accept, if coinductive, that the conclusions have the same or different coinductive types in any order.
  • When the conclusions are coinductive and enough hypotheses are inductive, we postpone the decision between fix and cofix to Qed-time.
  • We simplify and reorganize the code. For instance, mutual_info had two redundant copies of the possible recursion indices.

Depends on PR #18741 (merged) and #18742.

  • Added / updated test-suite.
  • Added changelog.

Overlay: mattam82/Coq-Equations#584

@herbelin herbelin added kind: cleanup Code removal, deprecation, refactorings, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: merge of dependency This PR depends on another PR being merged first. part: vernac High level command interpretation. part: inductives Inductive types, fixpoints, etc. labels Mar 4, 2024
@herbelin herbelin added this to the 8.20+rc1 milestone Mar 4, 2024
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 4, 2024
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 4, 2024
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from 9993056 to 0f62e92 Compare March 4, 2024 18:58
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 4, 2024
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 5, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 5, 2024
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from 0f62e92 to 534020c Compare March 5, 2024 18:24
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Mar 5, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Mar 6, 2024

🔴 CI failure at commit 534020c without any failure in the test-suite

✔️ Corresponding job for the base commit 5dcfab5 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-menhir
  • You can also pass me a specific list of targets to minimize as arguments.

@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from 534020c to 00979f2 Compare March 6, 2024 18:02
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from 00979f2 to d1a30de Compare March 6, 2024 18:11
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from d1a30de to 08bb4a3 Compare March 6, 2024 19:57
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from 08bb4a3 to 82fc99e Compare March 6, 2024 21:34
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 6, 2024
@herbelin herbelin mentioned this pull request Mar 7, 2024
Merged
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels May 13, 2024
@herbelin
Copy link
Member Author

I believe this to be ready. Most of the PR is about simplifying the code, while the first commit removes the (useless) restriction of corecursive Theorem with to statements in the same coinductive type.

@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 14, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request May 14, 2024
@herbelin
Change log for coq#18743
c71359b
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from f25fccc to c71359b Compare May 14, 2024 17:15
@coqbot-app coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels May 14, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request May 14, 2024
@herbelin
Change log for coq#18743
802b9e7
herbelin added a commit to herbelin/github-coq that referenced this pull request May 14, 2024
@herbelin
Change log for coq#18743
3b96c71
@SkySkimmer
Copy link
Contributor

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 15, 2024
SkySkimmer
SkySkimmer reviewed May 15, 2024
View reviewed changes
pretyping/pretyping.ml Outdated Show resolved Hide resolved
@herbelin herbelin mentioned this pull request May 15, 2024
Open
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 15, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label May 15, 2024
herbelin and others added 6 commits May 15, 2024 15:47
@herbelin
Removing overly strong restriction in tactic "fix".
f671bb2 
No strict requirement to be in the same inductive type. For instance,
we could be in "tree" and "list tree".

We could alternatively test whether there is a circularity between the
types, but that may be costly.
@herbelin @SkySkimmer
Support in search_guard for checking both if a fix or a cofix + simpl…
5b90d5d 
…ifications

Examples of simplifications:
- keeping only one the two redundant copies of possible recursion
  indices in "mutual_info"
- simplifying a check that Program Co/Fixpoint is guarded so far
- "prg_fixkind" was basically another name for "compute_guard": we
  change the flow of information so that they play the same role

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
@herbelin
Simplifying "Theorem with" and making it more flexible.
8c05b0b 
- We accept, if coinductive, that the conclusions have the same or
  different coinductive types in any order.
- When the conclusions are coinductive and enough hypotheses are
  inductive, we postpone the decision between fix and cofix to
  Qed-time.
@herbelin
Overlay for equations
c099ea8
@herbelin
Treating possible guard the same in the 3 functions declaring mutual …
ae777ef 
…definitions.

That is in:
- start_mutual_with_initialization (interactive)
- add_mutual_definition (Program)
- declare_mutually_recursive (non-interactive)
@herbelin
Change log for coq#18743
79d2443
@herbelin herbelin force-pushed the master+more-flexible-theorem-with branch from d79e3fc to 79d2443 Compare May 15, 2024 13:48
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels May 15, 2024
ejgallego
ejgallego approved these changes May 15, 2024
View reviewed changes
Copy link
Member

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

Thanks Hugo! LGTM (I only looked at the part I'm familiar with tho)

@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d40c5e9 into coq:master May 16, 2024
6 checks passed
Proof Handling automation moved this from TODO to Done May 16, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented May 16, 2024

@SkySkimmer: Please take care of the following overlays:

  • 18743-herbelin-master+more-flexible-theorem-with.sh

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

@SkySkimmer SkySkimmer SkySkimmer left review comments

@ejgallego ejgallego ejgallego approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: inductives Inductive types, fixpoints, etc. part: vernac High level command interpretation.
Projects
Proof Handling
  
Done
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@herbelin @SkySkimmer @ejgallego