Hi,

I'm practicing on Codewar. I was trying to use `lia`

in `Psatz`

. But it seemed not compatible with ssreflect. Then I tried `zify`

and it worked fine.

My question is: why this code would yield `Tactic failure: Cannot find witness.`

while I thought I've made everything in `coq_nat`

scope.

```
From mathcomp Require Import all_ssreflect.
Require Import Psatz.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Goal forall n : nat, (n + 2) * (n + 2) * (n + 2) =
(n + 1) * (n + 1) * (n + 1) + 3 * (n + 1) * (n + 1) + 3 * (n + 1) + 1.
Proof.
move=>n.
rewrite -[(n + 2) * (n + 2) * (n + 2)]/(((n + 2) * (n + 2) * (n + 2))%coq_nat).
rewrite -[(n + 1) * (n + 1) * (n + 1) + 3 * (n + 1) * (n + 1) + 3 * (n + 1) + 1]/(((n + 1) * (n + 1) * (n + 1) + 3 * (n + 1) * (n + 1) + 3 * (n + 1) + 1)%coq_nat).
lia.
Qed.
```

Add `From mathcomp Require Import zify.`

, then you won't even need the `coq_nat`

rewrites.

You need to have https://github.com/math-comp/mczify installed for this.

I know that, that's what I've done on my computer.

The thing is that I tried to use both `lia`

and `ssreflect`

on codewar so I was hoping to be able to understand why lia wouldn't work in this case.

Everything works fine without ssreflect.

```
Require Import Psatz.
Goal forall n : nat, (n + 2) * (n + 2) * (n + 2) =
(n + 1) * (n + 1) * (n + 1) + 3 * (n + 1) * (n + 1) + 3 * (n + 1) + 1.
Proof.
lia.
Qed.
```

But if I add `From mathcomp Require Import all_ssreflect.`

to the code above. Then for my goal, isn't every expression stay the same definition? Is there some quick fix for this particular case so that `lia`

would work?

When you import ssreflect, it changes the scope for interpreting `+`

and `*`

I think.

If I add

```
rewrite -[(n + 2) * (n + 2) * (n + 2)]/(((n + 2) * (n + 2) * (n + 2))%coq_nat).
rewrite -[(n + 1) * (n + 1) * (n + 1) + 3 * (n + 1) * (n + 1) + 3 * (n + 1) + 1]/(((n + 1) * (n + 1) * (n + 1) + 3 * (n + 1) * (n + 1) + 3 * (n + 1) + 1)%coq_nat).
```

So that the goal becomes

```
((n + 2) * (n + 2) * (n + 2))%coq_nat =
((n + 1) * (n + 1) * (n + 1) + 3 * (n + 1) * (n + 1) + 3 * (n + 1) + 1)%coq_nat
```

Do I change every operation back to the original coq definition? But it does not seem to work with lia still..

you can Set Printing All to perhaps better understand what the notations are hiding

Oh thanks I think I get it now. That's a good suggestion, I didn't know this option.

TX Xia has marked this topic as resolved.

A bit less verbose than `Set Printing All`

is `Unset Printing Notations`

, which in this case should do the same trick.

You may also look at the packages mczify and algebra-tactics which bind lia and ring to mathcomp

it seems the underlying problem here was that Coq Codewars does not include mczify and/or algebra-tactics

now if only there were a standard set of Coq packages, in something one might call a "distribution", and mczify+algebra-tactics was included there, and competition websites could install that by default

So are those packages in the Coq platform already?

It might be worth opening an issue on the code wars repository to suggest them to install the platform...

It’s true that @Karl Palmskog ‘s sass is more fun 😇

it seems my sarcasm attempts all end up in.... additional TODO items

no new issue needed: https://github.com/codewars/runner/issues/189

voting that link might help — they say

:+1: reaction might help to get this request prioritized.

Last updated: Sep 30 2023 at 06:01 UTC