CODEWITHSUNDEEP
coq
Dev
Dev

Reputation: 1

Unable to use coq's NDiv after importing

I am trying to use the functionality from NDiv in coq's standard library (visible here: https://coq.inria.fr/library/Coq.Numbers.Natural.Abstract.NDiv.html), so I enter the two lines below into coqide:

Require Import NDiv.
Check div_unique_exact.

But it results in an output of

Error: The reference div_unique_exact was not found in the current environment

I am not sure where the problem is. I also use imports such as List Arth Bool and Classical_Prop without problem. Thanks for any help.

Upvotes: 0

Views: 62

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

Note that NDiv starts with

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

The entire file is wrapped in this Module Type, which means that every lemma you see is only defined when you pass in module arguments to this module type functor. You probably want something like Require Import NArith. (or Require Import ZArith.), whence you can see if Coq can find div_unique_exact with Locate. If I do

Require Import Coq.NArith.NArith.
Locate div_unique_exact.

I get

Constant Coq.NArith.BinNat.N.div_unique_exact
  (shorter name to refer to it in current context is N.div_unique_exact)
Constant Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_unique_exact
  (shorter name to refer to it in current context is BinInt.Z.Private_Div.NZQuot.div_unique_exact)
Constant Coq.Arith.PeanoNat.Nat.div_unique_exact
  (shorter name to refer to it in current context is PeanoNat.Nat.div_unique_exact)
Constant Coq.NArith.BinNat.N.Private_NZDiv.div_unique_exact
  (shorter name to refer to it in current context is N.Private_NZDiv.div_unique_exact)
Constant Coq.Arith.PeanoNat.Nat.Private_NZDiv.div_unique_exact
  (shorter name to refer to it in current context is PeanoNat.Nat.Private_NZDiv.div_unique_exact)
Constant Coq.ZArith.BinInt.Z.Private_NZDiv.div_unique_exact
  (shorter name to refer to it in current context is BinInt.Z.Private_NZDiv.div_unique_exact)
Constant Coq.ZArith.BinInt.Z.div_unique_exact
  (shorter name to refer to it in current context is BinInt.Z.div_unique_exact)

and so we see that the first entry shows that the following will succeed:

Check N.div_unique_exact.

Upvotes: 2

Related Questions