✔ Question about lia · Coq users

Hi,
I'm practicing on Codewar. I was trying to use lia in Psatz. But it seemed not compatible with ssreflect. Then I tried zifyand 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.

Alexander Gryzlov (Aug 04 2022 at 12:14):

Add From mathcomp Require Import zify., then you won't even need the coq_nat rewrites.

Alexander Gryzlov (Aug 04 2022 at 12:15):

TX Xia (Aug 04 2022 at 12:42):

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?

Théo Winterhalter (Aug 04 2022 at 12:45):

When you import ssreflect, it changes the scope for interpreting + and * I think.

TX Xia (Aug 04 2022 at 12:52):

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).

((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..

Gaëtan Gilbert (Aug 04 2022 at 12:56):

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

TX Xia (Aug 04 2022 at 13:02):

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

Notification Bot (Aug 04 2022 at 13:04):

Ana de Almeida Borges (Aug 04 2022 at 13:37):

A bit less verbose than Set Printing All is Unset Printing Notations, which in this case should do the same trick.

Enrico Tassi (Aug 05 2022 at 13:25):

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

Karl Palmskog (Aug 05 2022 at 14:10):

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

Karl Palmskog (Aug 05 2022 at 14:11):

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

Paolo Giarrusso (Aug 05 2022 at 16:40):

Karl Palmskog (Aug 05 2022 at 16:44):

Théo Zimmermann (Aug 05 2022 at 17:01):

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

Stream: Coq users

Topic: ✔ Question about lia

TX Xia (Aug 04 2022 at 09:20):