rocq-prover / rocq-prover/stdlib

Import Nsatz redefines "0" and "1"

Open
#12 6 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Rocq Prover
Stars
42
Forks
38
Avg merge
14h 6m
Merged PRs (30d)
3

Description

Description of the problem
Set Printing All.
Require Import ZArith.
Local Open Scope Z_scope.

Goal True.
  unify (0=1) (Z.zero = Z.one).
Abort.

Require Import Nsatz.
Goal True.
  unify (0=1) (Z.zero = Z.one). (* fails *)
Abort.

Original report:

```coq Require Import QArith Nsatz. Local Open Scope Q_scope.

Goal forall
(x : Q)
(r : Q) (Hr : rr == x)
(s : Q) (Hs : ss == x)
(t : Q) (Hs : tt == x)
(isr : Q) (Hisr : isr(s - r) == 1)
(ist : Q) (Hisr : ist*(s - t) == 1)
(irt : Q) (Hirt : irt*(r - t) == 1)
, 0 == 1.
Proof.
intros.
nsatz.
Qed.

Local Close Scope Q_scope.

Goal forall
(x : Z)
(r : Z) (Hr : rr = x)
(s : Z) (Hs : ss = x)
(t : Z) (Hs : tt = x)
(isr : Z) (Hisr : isr(s - r) = 1)
(ist : Z) (Hisr : ist*(s - t) = 1)
(irt : Z) (Hirt : irt*(r - t) = 1)
, 0 = 1.
Proof.
intros.
(* nsatz. )
(
In environment
x, r, s, t, isr, ist, irt : Z
The term "0 - 1 :: 0 :: nil" has type "list Rdefinitions.RbaseSymbolsImpl.R"
while it is expected to have type "list Z".
)
Set Printing All.
Set Ltac Backtrace.
nsatz.
(
In nested Ltac calls to "nsatz", "nsatz_default",
"nsatz_generic", "lterm_goal", "lterm_goal", "lterm_goal",
"lterm_goal", "lterm_goal", "lterm_goal" and "(@cons _ b1 (@cons _ b2 l))"
(with
l:=@cons Rdefinitions.RbaseSymbolsImpl.R
(@subtraction Rdefinitions.RbaseSymbolsImpl.R
(@sub_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)
(@zero Rdefinitions.RbaseSymbolsImpl.R
(@zero_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops))
(@one Rdefinitions.RbaseSymbolsImpl.R
(@one_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)))
(@cons Rdefinitions.RbaseSymbolsImpl.R
(@zero Rdefinitions.RbaseSymbolsImpl.R
(@zero_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops))
(@nil Rdefinitions.RbaseSymbolsImpl.R)),
g:=@equality Rdefinitions.RbaseSymbolsImpl.R
(@eq_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)
(@subtraction Rdefinitions.RbaseSymbolsImpl.R
(@sub_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)
(@zero Rdefinitions.RbaseSymbolsImpl.R
(@zero_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops))
(@one Rdefinitions.RbaseSymbolsImpl.R
(@one_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)))
(@zero Rdefinitions.RbaseSymbolsImpl.R
(@zero_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)),
b2:=@zero Z
(@zero_notation Z Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z) Zops),
b1:=@subtraction Z
(@sub_notation Z Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z) Zops)
(@multiplication Z Z
(@mul_notation Z Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z) Zops)
irt
(@subtraction Z
(@sub_notation Z Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp
(@eq Z) Zops) r t))
(@one Z
(@one_notation Z Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z) Zops))),
last term evaluation failed.
In environment
x, r, s, t, isr, ist, irt : Z
The term
"@cons Rdefinitions.RbaseSymbolsImpl.R
(@subtraction Rdefinitions.RbaseSymbolsImpl.R
(@sub_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)
(@zero Rdefinitions.RbaseSymbolsImpl.R
(@zero_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops))
(@one Rdefinitions.RbaseSymbolsImpl.R
(@one_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops)))
(@cons Rdefinitions.RbaseSymbolsImpl.R
(@zero Rdefinitions.RbaseSymbolsImpl.R
(@zero_notation Rdefinitions.RbaseSymbolsImpl.R
(Rdefinitions.IZR Z0) (Rdefinitions.IZR (Zpos xH))
Rdefinitions.RbaseSymbolsImpl.Rplus
Rdefinitions.RbaseSymbolsImpl.Rmult Rdefinitions.Rminus
Rdefinitions.RbaseSymbolsImpl.Ropp
(@eq Rdefinitions.RbaseSymbolsImpl.R) Rops))
(@nil Rdefinitions.RbaseSymbolsImpl.R))" has type
"list Rdefinitions.RbaseSymbolsImpl.R" while it is expected to have type
"list Z".
*)
Qed.


</details>

I remember running into numerous similar issues before I started reporting bugs; this is why fiat-crypto has its own `nsatz_compute` wrapper that threads the ring instance.

#### Coq Version

8.16.1

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start by running the minimal Set Printing All, ZArith, and Nsatz reproduction in the issue, then compare how numeral notation is resolved before and after importing Nsatz. Review the nsatz behavior and the mentioned fiat-crypto nsatz_compute wrapper; done means importing Nsatz no longer changes the interpretation of 0 and 1 or causes the shown Z goal to fail.

Written by the indexing model from the issue text.

Assessment

Domain
tooling
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.