2

Coq 8.7 integrates the popular Ssreflect library. Its libraries can hence be imported in the following manner:

From Coq Require Import ssreflect ssrfun ssrbool.

However, when I try to import ssrnat it complains that it's Unable to locate library ssrnat with prefix Coq, and I cannot find ssrnat in the Coq distribution on disk either. Was ssrnat deliberately not included for some reason, or folder into another module, or is there just something wrong with my installation?

LogicChains
  • 4,332
  • 2
  • 18
  • 27
  • 2
    Does `From mathcomp Require Import ssrnat.` work? – Anton Trunov Dec 16 '17 at 09:51
  • That gives "Cannot find a physical path bound to logical path matching suffix <> and prefix mathcomp." (I don't have mathcomp installed. Should I?). – LogicChains Dec 16 '17 at 09:56
  • Despite the fact the Coq Refman mentions `ssrnat`, it's not in the standard library as of now (my installation has only `ssreflect`, `ssrfun`, and `ssrbool` in `$HOME/.opam/4.06.0/lib/coq/plugins/ssr` directory). So, yes you should install mathcomp. Incidentally, [this question](https://stackoverflow.com/questions/43955082/how-to-install-ssreflect-and-mathcomp-in-linux) might help with installation. – Anton Trunov Dec 16 '17 at 10:29

1 Answers1

4

ssrnat is not included in the main Coq distribution, although some day we hope to provide an extended distribution where more libraries are available by default.

In Coq 8.7, only the tactic language itself ssreflect plus a few basic supporting libraries ssrfun ssrbool were included.

The reason we didn't include more is because ssrnat makes use of the math-comp mathematical hierarchy so this is a more "invasive" change.

Fortunately, thanks to the plugin being included, installing ssrnat is a very easy task.

ejgallego
  • 6,709
  • 1
  • 14
  • 29