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

Params instances are not used for setoid_rewrite with types #20044

Open
quarkcool opened this issue Jan 14, 2025 · 0 comments · May be fixed by #20045
Open

Params instances are not used for setoid_rewrite with types #20044

quarkcool opened this issue Jan 14, 2025 · 0 comments · May be fixed by #20045
Labels
kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated.

Comments

@quarkcool
Copy link
Contributor

Description of the problem

Params instances are a (undocumented) feature to control setoid rewriting behaviour (see https://gitlab.mpi-sws.org/iris/stdpp/-/blob/b391a3c262be1c10672a5456144c12a5f3290734/stdpp/base.v#L329)

They are indeed used while rewriting in Prop (i.e. with Corelib.Classes.Morphisms machinery) but not in Type (i.e. with Corelib.Classes.CMorphisms machinery)

I have a working small fix (to come in a separate pull request), which basically entails aligning the implementations between the two files mentioned above

Small Rocq / Coq file to reproduce the bug

Require Export
  Corelib.Classes.CMorphisms.

(* Small test file to show that partial_application_tactic doesn't use Params instances *)

Definition R (x y : unit) : Type := unit.

Instance :
  Reflexive R.
Proof.
  intros x.
  constructor.
Qed.

Instance :
  Proper (R ==> R ==> flip arrow) R.
Proof.
  intros [] [] _ [] [] _ _.
  constructor.
Qed.

Instance :
  forall x, Proper (R ==> flip arrow) (R x).
Proof.
  intros x.
  partial_application_tactic;
    typeclasses eauto.
Abort.

Instance : Params R 1 := {}.
Instance :
  forall x, Proper (R ==> flip arrow) (R x).
Proof.
  intros x.
  (* should fail in the presence of a params instance, but doesn't *)
  Fail partial_application_tactic.
Abort.

Version of Rocq / Coq where this bug occurs

9.0+alpha

Last version of Rocq / Coq where the bug did not occur

No response
@quarkcool quarkcool added kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Jan 14, 2025
@quarkcool quarkcool linked a pull request Jan 14, 2025 that will close this issue
Open
6 tasks
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. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix CMorphisms partial_application_tactic to correctly leverage Params instances quarkcool/coq
1 participant
@quarkcool