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

simpl doesn't work on primitive coinductive records #7982

Closed
ppedrot opened this issue Jul 2, 2018 · 1 comment · Fixed by #18577
Closed

simpl doesn't work on primitive coinductive records #7982

ppedrot opened this issue Jul 2, 2018 · 1 comment · Fixed by #18577
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: coinductives CoInductive types, cofixpoints etc.
Milestone
8.20+rc1

Comments

@ppedrot
Copy link
Member

ppedrot commented Jul 2, 2018 •
edited by herbelin

Version

Coq 8.8

Description of the problem

The following script displays the error:

Set Primitive Projections.

CoInductive stream (A : Type) := cons { hd : A; tl : stream A }.

CoFixpoint const {A} (x : A) := cons A x (const x).

Goal forall A x, (@const A x).(tl _) = const x.
Proof.
intros.
simpl.
match goal with [ |- ?x = ?x ] => idtac end.

Last line fail while it succeeds when the Primitive Projection option is not set. For some reason, cbn works.
@Alizter Alizter added kind: bug An error, flaw, fault or unintended behaviour. part: coinductives CoInductive types, cofixpoints etc. simpl labels Jan 4, 2022
@SkySkimmer SkySkimmer mentioned this issue Feb 15, 2022
Merged
1 task
@SkySkimmer SkySkimmer removed the simpl label Feb 15, 2022
herbelin added a commit to herbelin/github-coq that referenced this issue Jan 28, 2024
@herbelin
Fixes coq#7982: support for reduction of primitive projection of cofi…
5e2f940 
…x in "simpl".
This was referenced Jan 28, 2024
Merged
Open
@herbelin
Copy link
Member

Fixed in #18577.

herbelin added a commit to herbelin/github-coq that referenced this issue Feb 1, 2024
@herbelin
Fixes coq#7982: support for reduction of primitive projection of cofi…
946fa37 
…x in "simpl".
herbelin added a commit to herbelin/github-coq that referenced this issue Feb 4, 2024
@herbelin
Fixes coq#7982: support for reduction of primitive projection of cofi…
eeb5b71 
…x in "simpl".
herbelin added a commit to herbelin/github-coq that referenced this issue Feb 7, 2024
@herbelin
Fixes coq#7982: support for reduction of primitive projection of cofi…
5496e00 
…x in "simpl".
coqbot-app bot added a commit that referenced this issue Feb 21, 2024
@coqbot-app @ppedrot
Merge PR #18577: Fixes #7982: add support for reduction of primitive …
7e99e53 
…projection of cofixpoints in "simpl" reduction strategy

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
@coqbot-app coqbot-app bot added this to the 8.20+rc1 milestone Feb 21, 2024
louiseddp pushed a commit to louiseddp/coq that referenced this issue Feb 27, 2024
@herbelin @louiseddp
Fixes coq#7982: support for reduction of primitive projection of cofi…
d63805a 
…x in "simpl".
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: coinductives CoInductive types, cofixpoints etc.
Projects
None yet
Milestone
8.20+rc1
4 participants
@herbelin @ppedrot @SkySkimmer @Alizter