How to Install Ssreflect and Mathcomp in Linux

How to install SSReflect and MathComp in Linux?

I'm on Ubuntu 16.04. Let's take a step back and begin by installing OPAM:

$ sudo apt update && sudo apt install opam
$ opam --version
1.2.2
$ opam init     # agree to modify your dot-files
$ eval `opam config env`
$ ocamlc -version
4.02.3

Next, you may want to switch from Ubuntu's pretty old OCaml version to a more recent one. This step is optional and it takes around 10 min.

$ opam switch 4.04.1
$ eval `opam config env`
$ ocamlc -version
4.04.1

Now, let's add the following repository to be able to install math-comp:

$ opam repo add coq-released https://coq.inria.fr/opam/released

And, finally, install ssreflect:

$ opam install coq-mathcomp-ssreflect

OPAM will figure out the dependencies (including Coq), download and install what we have asked!

Nix: installing ssreflect

There are a few things that you need to be aware of:

• Nix is a source-based package manager with a binary cache. A lot of packages are pre-built and available in the binary cache, thus their installation doesn't take long; some packages (in particular development libraries) are not pre-built and Nix, when installing them will take the time it needs to compile them. Please be patient: you will only need to wait for the full compilation the first time (and yes, math-comp emits lots of warning upon compilation); next times, the package will be already available in your local Nix store.

• Since OPAM is also source-based, using OPAM instead of Nix won't make you save time. You can't mixup Nix-installed Coq with OPAM installed SSReflect because the latter will want the former as an OPAM dependency.

• The Nix way to use libraries is not to install them but to load them with nix-shell instead. nix-shell will "install" the libraries and set some environment variables for you (e.g. $COQPATH in this case).

• You can also compile the package from source yourself using a Nix-installed Coq but you cannot run make install because this would try to install SSReflect at the same place where Coq is installed but the Nix store is non-mutable. Instead you could skip this step, and set up $COQPATH manually.

• Indeed, the compilation of the full math-comp takes very long. There is a Coq ssreflect package which is lighter. You can get it using:

  nix-shell -p coqPackages_8_6.ssreflect
  

Is ssrnat included in Coq 8.7?

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.

Type coercion from nat to rat

So, _%:Q is a notation for _%:R as documented in rat.v
Then doing Search _ Num.le _%:R or Search _ (_%:R <= _%:R) leads to ler_nat which is the right lemma to apply, as in:

Lemma X (n m : nat) : (n <= m)%N -> n%:Q <= m%:Q.
Proof. by move=> le_nm; rewrite ler_nat. Qed.

Coq file generated by WP does not compile

First, indeed you need coq < 8.8 (e.g. 8.7.2) if you want to use it with Frama-C/WP, as newer versions are not supported for the moment.

Second, the order in which you have installed your packages is relevant. In particular, if the appropriate version of coq has been installed after frama-c, WP did not compile and install its coq libraries, which are the ones that are missing here. Thus, you may want to do opam reinstall frama-c to compile the package against a compatible coq version.

Coq: How to apply axioms deeper in the goal?

I removed unused variables from MT3:

Axiom MT3 :
  forall z : MT, z = c(a(z),b(z)) <-> a(z) <> z /\ b(z) <> z.

We can use the remember tactic to kind of "extract" a term from inside a larger term (and remember this connection in an equation):

Lemma MT1A x :
  x = a (c (example, b example)) ->
  x = example /\ a x <> x /\ b x <> x.
Proof.
  unfold example; intros H.
  rewrite <-MT3.
  remember (c (NIL, e NIL)) as f eqn:F.
  pose proof (MT1 _ _ _ F) as [F1 F2].
  remember (c (f, b f)) as g eqn:G.
  pose proof (MT1 _ _ _ G) as [G1 G2].
  split; congruence.
Qed.

---

Related Topics