Stream: Coq users

Topic: ✔ Question about lia


view this post on Zulip TX Xia (Aug 04 2022 at 09:20):

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.

view this post on Zulip Alexander Gryzlov (Aug 04 2022 at 12:14):

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

view this post on Zulip Alexander Gryzlov (Aug 04 2022 at 12:15):

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

view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Aug 04 2022 at 12:45):

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

view this post on Zulip TX Xia (Aug 04 2022 at 12:52):

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

view this post on Zulip Gaëtan Gilbert (Aug 04 2022 at 12:56):

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

view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 04 2022 at 13:04):

TX Xia has marked this topic as resolved.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 05 2022 at 16:40):

So are those packages in the Coq platform already?

view this post on Zulip Karl Palmskog (Aug 05 2022 at 16:44):

indeed: https://github.com/coq/platform/blob/2022.04.1/doc/README~8.15~2022.04.md#coq-platform-2022041-with-coq-8152-extended-level

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Aug 05 2022 at 18:02):

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

view this post on Zulip Karl Palmskog (Aug 05 2022 at 18:14):

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

view this post on Zulip Paolo Giarrusso (Aug 05 2022 at 18:15):

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

view this post on Zulip Paolo Giarrusso (Aug 05 2022 at 18:16):

voting that link might help — they say

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


Last updated: Mar 28 2024 at 18:02 UTC