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

rewrite@A helper tactic diverges on to_O_natural_compose #744

Closed
mikeshulman opened this issue Apr 3, 2015 · 0 comments · Fixed by #747
Closed

rewrite@A helper tactic diverges on to_O_natural_compose #744

mikeshulman opened this issue Apr 3, 2015 · 0 comments · Fixed by #747

Comments

@mikeshulman
Copy link
Contributor

As noticed at #743, the following code appears to spin forever:

Require Import HoTT.
Module Foo (Os : ReflectiveSubuniverses).
  Module Import Os_Theory := ReflectiveSubuniverses_Theory Os.
  Goal Unit.
    let lem' := preconcat_any @to_O_natural_compose in
    pose proof lem' as H.
    left_associate_concat_in H.
  Abort.
End Foo.
@mikeshulman mikeshulman mentioned this issue Apr 3, 2015
Merged
@JasonGross JasonGross mentioned this issue Apr 7, 2015
Merged
JasonGross added a commit that referenced this issue Apr 7, 2015
@JasonGross
Fix [rewrite@A]
0178072 
When the hypothesis contained [a @ (b @ c)] where the implicit arguments
to [concat] did not match the implicit arguments inferred for [@concat _
_ _ _ a (@concat _ _ _ _ b c)] (according to [pattern]),
[left_associate_concat_in] looped, repeatedly finding [a @ (b @ c)], and
failing to associate it to the left, introducing constant transports
that did nothing.

This is now fixed, by picking up and passing the implicit arguments,
explicitly.

The comment in Modalities/ReflectiveSubuniverse.v has been updated; a
naive use of [rewrite@A] causes the subsequent rewrite to fail.  I
haven't tracked it down, but I suspect @mikeshulman wouldn't have much
trouble updating the file.

This fixes #744; the test is now added to Tests.v.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix [rewrite@A] JasonGross/HoTT
1 participant
@mikeshulman