rocq-prover / rocq-prover/stdlib
nsatz fails when Zpos is present
Open
Nobody has claimed this yet.
- Dominant language
- Rocq Prover
- Stars
- 42
- Forks
- 38
- Avg merge
- 14h 6m
- Merged PRs (30d)
- 3
Description
Version
8.8.0
Description of the problem
This code fails, but it should not
Require Import Coq.ZArith.ZArith.
Require Import Coq.nsatz.Nsatz.
Goal forall (x:positive) (y:Z), Zpos x = Zpos x -> y = y.
Proof. intros. nsatz. (* Error:
In nested Ltac calls to "nsatz", "nsatz_default", "nsatz_generic",
"reify_goal" and "change x with (interpret3 e l)", last call failed.
Not convertible.
*)
Note that running zify before nsatz causes it to succeed.
cc @letouzey @andres-erbsen
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
Reproduce the provided goal with the nsatz entry point and compare it with the successful path that runs zify first. Read the nsatz_default, nsatz_generic, and reify_goal calls named in the error. Done means the original proof succeeds without requiring zify, with regression coverage for the Zpos case.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 48/100