rocq-prover / rocq-prover/stdlib
rtn1_trans name clash
Nobody has claimed this yet.
- Dominant language
- Rocq Prover
- Stars
- 42
- Forks
- 38
- Avg merge
- 14h 6m
- Merged PRs (30d)
- 3
Description
Version
The Coq Proof Assistant, version 8.6 (December 2016)
compiled on Dec 29 2016 23:38:14 with OCaml 4.02.3
However, the issue is probably present in the latest version ( 8.7.2) as well
[edit: fails on current master too]
Operating system
Debian Linux
Description of the problem
This is a reopen of issue coq/coq#2152. The name clash is still present
in Relations. While rtn1_trans was renamed to clos_rtn1_rt in
Relations/Operators_Properties.v but it was re-added as a notation at the end
(at line 435). The notation is not visible in the documentation.
Code to reproduce the bug:
Require Import Relations.
Lemma rtn1_trans_test1 A R x y z (Ht:clos_refl_trans_n1 A R x y) (H1:R y z):
(clos_refl_trans_n1 _ R x z).
Proof.
(*The fully qualified name works*)
eapply Coq.Relations.Relation_Operators.rtn1_trans; eauto.
Qed.
Lemma rtn1_trans_test2 A R x y z (Ht:clos_refl_trans_n1 A R x y) (H1:R y z):
(clos_refl_trans_n1 _ R x z).
Proof.
eapply rtn1_trans; eauto. (*Fails*)
Qed.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Inspect Relations/Operators_Properties.v around the notation near line 435, then run the two Coq lemmas in the issue to confirm the qualified and unqualified behavior. Done means the rtn1_trans name clash is resolved and the reproduction no longer fails; add or update a regression test if the surrounding test structure supports it.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Bug
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 45/100