Import Nsatz redefines "0" and "1"

[andres-erbsen]

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

[SkySkimmer]

It seems to have problems with mixed types, simplified:

Goal forall (x:Z) (H:x == x), 0 = 0 :> R.
  intros;nsatz.
(* 
In environment
x : Z
The term "0 - 0 :: 0 :: nil" has type "list R" while it is expected to have type "list Z".
*)

[JasonGross]

@andres-erbsen we should factor out our nsatz wrapper that threads the types from Fiat Crypto and summit it as a PR. (And maybe make a PR for fsatz/handling of division in another PR while we're at it?)

[andres-erbsen]

@SkySkimmer are you sure the minimized example has the same root cause as my example? I didn't think I had mixed types there, but possibly I missed some. I added succeeding goal on Q after making the bad example on Z.

[SkySkimmer]

Yes, in

Require Import QArith Nsatz.

Local Close Scope Q_scope.

Goal forall
  (x : Z)
  (r : Z) (Hr : r*r = x)
  (s : Z) (Hs : s*s = x)
  (t : Z) (Hs : t*t = x)
  (isr : Z) (Hisr : isr*(s - r) = 1)
  (ist : Z) (Hisr : ist*(s - t) = 1)
  (irt : Z) (Hirt : irt*(r - t) = 1)
  , 0 = 1.

the conclusion 0 = 1 is in R but the hypotheses are in Z

[andres-erbsen]

Oh, it's R not Q... yeah, I don't think nsatz should deal with multi-type problems. But also Require Import nsatz should not make 0=1 mean R! Here's my preferred minimized form of the original issue:

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).
Abort.

[silene]

Is the R_scope really open in you case? Keep in mind that, when you import Nsatz, you also import the following notations:

Class Zero (A : Type) := zero : A.
Notation "0" := zero.
Class One (A : Type) := one : A.
Notation "1" := one.

So, you get some random meaning for 0 and 1 depending on what the typeclass resolution mechanism decides.