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

Trying to recompute the inductive structure of the main (co)-inductive types when checking the guard condition #17950

Closed
wants to merge 12 commits into from
Closed

Trying to recompute the inductive structure of the main (co)-inductive types when checking the guard condition #17950

wants to merge 12 commits into from

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Aug 9, 2023 •
edited

This should have been done for a very long time already: we recompute dynamically the recursive structure of the decreasing argument of fixpoints.

We could have introduced a notion of parametric recursive structure (precomputed "recarg") and instantiate the parameter dynamically (this is what we made in a first attempt of the PR actually), however we would have failed to support examples requiring a computation after instantiation of the parameters as in:

Inductive list (b : bool) A B :=
| nil : list b A B
| cons : (if b then A else B) -> list b A B -> list b A B.

Inductive tree := Foo : list true tree unit -> tree.

Fixpoint f (l : list true tree unit) {struct l} :=
  match l with
  | nil _ _ _ => 0
  | cons _ _ _ (Foo l') _ => f l'
  end.

Closes #9045, #12781, #13855, #15932.

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

Depends on #18229 and #18242.

To do:

  • double-check that we are not doing something wrong
  • check performance, possibly compute recargs lazily
  • decide if precomputation of recargs is still useful

@herbelin herbelin requested review from a team as code owners August 9, 2023 18:33
@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 Aug 9, 2023
@herbelin herbelin marked this pull request as draft August 9, 2023 18:34
@herbelin herbelin added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: inductives Inductive types, fixpoints, etc. part: coinductives CoInductive types, cofixpoints etc. labels Aug 9, 2023
@herbelin herbelin added this to the 8.19+rc1 milestone Aug 9, 2023
@herbelin herbelin force-pushed the master+parameterized-wf-paths branch 3 times, most recently from 73518b7 to 2cfe1e6 Compare August 10, 2023 16:48
@herbelin
Copy link
Member Author

@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 Aug 10, 2023
@herbelin herbelin force-pushed the master+parameterized-wf-paths branch from 2cfe1e6 to 05a1083 Compare September 2, 2023 17:35
@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 Sep 2, 2023
This was referenced Oct 30, 2023
Merged
Closed
@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 Nov 15, 2023
@herbelin herbelin mentioned this pull request Nov 21, 2023
Merged
@SkySkimmer SkySkimmer removed this from the 8.19+rc1 milestone Nov 22, 2023
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Dec 15, 2023

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Dec 15, 2023
@herbelin
Reconstruction of the intent of the use of history in Rtree.inter.
a383e84 
For efficiency, Rtree.inter tries to preserve as much of the common
structure of the two trees to intersect, so expansions are done
lazily.

Rtree.inter uses an history and I understand that this history is used
to ensure that only a finite number of expansions is needed to manage
overlapping expansions.

My understanding is that the effective expansion of variables is
missing when using this history: this is a reason for an
incompletenesses of Rtree.inter, which sometimes falls and fails in an
unsupported Rec/Var case.

The commit is fixing this, by instantiating the variables before using
the history.

A typical example of incompleteness before the fix is when comparing
the following equivalent trees:

  Rec{Mrec[Wrapper, 0],
      [(Rec{Nested[Unwrapper, 0], [(), (#1:0)]})]}

and

  Rec{Nested[Wrapper, 0],
      [(Rec{Mrec[Unwrapper, 0], [(), (Rec{Nested[Wrapper, 0], [(#1:0)]})]})]}

(example from success/fix.v)
@herbelin
Slight reorganization of inductive_of_mutfix.
e2629d8
@herbelin
Rtree: Renaming Param into Var to be able to reuse Param for parameters.
97a085b
@herbelin
Hack to deal with remaining evars in fixpoints.
9ca91bf
@herbelin
Removing an extra space.
c5c4954
@herbelin
Introduce an optimized version of recursive tree expansion.
df86f67 
The trick is to not duplicate the nested recursive calls but to refer
to them using a variable.

E.g., in
  μX.F(μY.G(X,Y))
we do not expand the body into
  F(μY.G(μX.F(X,μY.G(X,Y)),Y))
but into
  F(μY.G(μX.F(X,Y),Y))
@herbelin
Well-foundedness paths: identify Nested(NestedInd(ind)) with Mrec(ind).
d361f2e
@herbelin herbelin added the needs: merge of dependency This PR depends on another PR being merged first. label Dec 23, 2023
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 23, 2023
@herbelin herbelin force-pushed the master+parameterized-wf-paths branch from 05a1083 to 688ade6 Compare December 23, 2023 16:03
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. 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 Dec 23, 2023
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 23, 2023
@herbelin herbelin force-pushed the master+parameterized-wf-paths branch from 688ade6 to a689b14 Compare December 23, 2023 22:29
@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 Dec 23, 2023
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 24, 2023
@herbelin herbelin force-pushed the master+parameterized-wf-paths branch from a689b14 to 346d104 Compare December 24, 2023 00:10
@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 Dec 24, 2023
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 25, 2023
@herbelin herbelin force-pushed the master+parameterized-wf-paths branch from 346d104 to 693e030 Compare December 25, 2023 08:26
@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 Dec 25, 2023
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 25, 2023
@herbelin herbelin force-pushed the master+parameterized-wf-paths branch from 693e030 to 9e2b86d Compare December 25, 2023 23:54
@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 Dec 25, 2023
@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 Jan 8, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Feb 7, 2024

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Feb 7, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Mar 8, 2024

This PR was not rebased after 30 days despite the warning, it is now closed.

@coqbot-app coqbot-app bot closed this Mar 8, 2024
@SkySkimmer SkySkimmer mentioned this pull request Apr 22, 2024
Closed
@herbelin herbelin changed the title Taking the inductive structure of the parameters of the main (co)-inductive types into account when checking the guard condition Trying to recompute the inductive structure of the main (co)-inductive types when checking the guard condition May 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: merge of dependency This PR depends on another PR being merged first. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: coinductives CoInductive types, cofixpoints etc. part: inductives Inductive types, fixpoints, etc. stale This PR will be closed unless it is rebased.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Incorrect error for Fixpoint principal argument checking
2 participants
@herbelin @SkySkimmer