simpl converting nat to %Nrec

[felipeqc]

Hi, I was testing Coq 8.5 so that I could try native_compute, but I was not able to compile my library. I'm not using NaTrec, but sometimes simpl converts numbers to %Nrec and the nat lemmas stop working. Here's an example:

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.

Variable l: seq nat. Variable idx: nat.

Lemma test: nth 0 (0 :: l) (idx.+1 + 0) = nth 0 l idx. Proof.
Fail (rewrite /= addn0). rewrite addn0 /= //. Qed.

Thanks, Felipe

[thery]

On 02/06/2016 05:15 PM, Felipe wrote:

Hi, I was testing Coq 85 so that I could try native_compute, but I was not able to compile my library I'm not using NaTrec, but sometimes simpl converts numbers to %Nrec and the nat lemmas stop working Here's an example:

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq

Variable l: seq nat Variable idx: nat

Lemma test: nth 0 (0 :: l) (idx+1 + 0) = nth 0 l idx Proof

Fail (rewrite /= addn0) rewrite addn0 /= // Qed

Strange

this usually occurs when you unfold some definitions but it should not when you do nothing.

How did you install math-comp, with opam or from the github site?

can you also try using the following Require:

From mathcomp Require Import all_ssreflect.

does it change something?

Laurent

[felipeqc]

I installed it from github: wget https://github.com/math-comp/math-comp/tarball/mathcomp-1.6, and then I compiled ssreflect alone: cd mathcomp/ssreflect make && make install

I tried importing all_ssreflect, but I still get the same problem when I run simpl:

============================ nth 0 l (idx + 0)%Nrec = nth 0 l idx

[thery]

On 02/06/2016 05:37 PM, Felipe wrote:

I installed it from github: wget https://github.com/math-comp/math-comp/tarball/mathcomp-1.6, and then I compiled ssreflect alone: cd mathcomp/ssreflect make && make install

I tried importing all_ssreflect, but I still get the same problem when I run simpl:

nth 0 l (idx + 0)%Nrec = nth 0 l idx

— Reply to this email directly or view it on GitHub https://github.com/math-comp/math-comp/issues/23#issuecomment-180807553.

Very strange I've recompiled the tarbal and I still have no problem with rewrite /=.

Which version of coq are you using?

Laurent

[ejgallego]

Hi Felipe, indeed that's strange, I couldn't reproduce it either.

Could you try reproducing with the version at https://x80.org/rhino-coq/ ? Thanks

[felipeqc]

I was able to reproduce the problem in rhino-coq. Please have a look

[ejgallego]

Indeed I can reproduce it now, thanks!

You can use rewrite -addnE to temporally alleviate the problem.

[thery]

On 02/06/2016 06:47 PM, Emilio Jesús Gallego Arias wrote:

Indeed I can reproduce it now, thanks!

— Reply to this email directly or view it on GitHub https://github.com/math-comp/math-comp/issues/23#issuecomment-180819822.

Is the problem solved?

[ejgallego]

Well, I'm not sure this should be considered a bug indeed; a more expert person should comment.

The issue is that the inner match on nth forces the idx.+1 + 0 redex, thus the addn_rec term is revealed and -addnE must be used if you want to recover the intended idx + 0.

AFAICS this is not easy to avoid. Also, it looks like original lemma can be proved with by rewrite addn0 which avoids this problem altogether.

[felipeqc]

Yeah, fixing the proof is easy. It was just that it used to work in the previous version.

Maybe simpl became more aggressive in Coq 8.5. But if this only happens in this case it should be fine.

[ejgallego]

Umm, I see the same behaviour in Coq 8.4 + ssreflect 1.5.

[gares]

I'm afraid this problem has little to do with ssreflect, since /= calls Coq's simpl and AFAICT the definition of nth or addn didn't change. I'm closing this.