Skip to content

Making Theorem with more flexible + code cleanup - #18743

Merged
coqbot-app[bot] merged 6 commits into
rocq-prover:masterfrom
herbelin:master+more-flexible-theorem-with
May 16, 2024
Merged

Making Theorem with more flexible + code cleanup#18743
coqbot-app[bot] merged 6 commits into
rocq-prover:masterfrom
herbelin:master+more-flexible-theorem-with

Conversation

@herbelin

@herbelin herbelin commented Mar 4, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

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: rocq-prover/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 Bot commented Mar 6, 2024

Copy link
Copy Markdown
Contributor

🔴 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
@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 Apr 23, 2024
@herbelin
herbelin force-pushed the master+more-flexible-theorem-with branch from c71959f to 24f0e34 Compare April 24, 2024 20:09
@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 Apr 24, 2024
@SkySkimmer

SkySkimmer commented May 6, 2024

Copy link
Copy Markdown
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 6, 2024
@herbelin
herbelin force-pushed the master+more-flexible-theorem-with branch from 24f0e34 to df1b51f Compare May 6, 2024 17:26
@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 6, 2024
@herbelin
herbelin force-pushed the master+more-flexible-theorem-with branch 2 times, most recently from 8e76c4a to d22cb11 Compare May 6, 2024 17:45
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label May 6, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request May 6, 2024
@herbelin
Change log for rocq-prover#18743
44d083f
@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 6, 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 May 7, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request May 8, 2024
@herbelin
Change log for rocq-prover#18743
d5887d5
@herbelin
herbelin force-pushed the master+more-flexible-theorem-with branch from 44d083f to d5887d5 Compare May 8, 2024 09:56
@herbelin

herbelin commented May 13, 2024

Copy link
Copy Markdown
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.

@SkySkimmer

SkySkimmer commented May 15, 2024

Copy link
Copy Markdown
Contributor

@coqbot run full ci

SkySkimmer
SkySkimmer reviewed May 15, 2024
View reviewed changes
Comment thread pretyping/pretyping.ml Outdated
@herbelin herbelin mentioned this pull request May 15, 2024
Merged
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 rocq-prover#18743
79d2443
ejgallego
ejgallego approved these changes May 15, 2024
View reviewed changes

@ejgallego ejgallego left a comment

Copy link
Copy Markdown
Contributor

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

SkySkimmer commented May 16, 2024

Copy link
Copy Markdown
Contributor

@coqbot merge now

@coqbot-app

coqbot-app Bot commented May 16, 2024

Copy link
Copy Markdown
Contributor

@SkySkimmer: Please take care of the following overlays:

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

@herbelin herbelin mentioned this pull request May 28, 2024
Merged
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
+1 more reviewer
@ejgallego ejgallego ejgallego approved these changes
Reviewers whose approvals may not affect merge requirements

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
Status: Done

Milestone

8.20+rc1

Development

Successfully merging this pull request may close these issues.

3 participants

@herbelin @SkySkimmer @ejgallego