Stream: math-comp users

Topic: Calculating in Zmodp


view this post on Zulip Sebastian Ertel (Mar 30 2023 at 14:18):

Hi,

I only recently started using mathcomp and often find myself tinkering with seemingly simple lemmas such as for example this one:

is_true (Zp1 != Zp0)

I found

Check Zp_nontrivial.
Zp_nontrivial
     :  p' : nat, is_true (Zp1 != 0)

Application of course fails:

apply Zp_nontrivial.
  Unable to unify "(Zp1 != 0) = true" with "(Zp1 != Zp0) = true".

But then there is the problem of converting from Zp to nat?

In fact, this is a recurring problem and I have not found the proper way to deal with it yet.
In 99% of the case, I have (in)equalities where I'm only interested in the nat representation of the Zp -Ordinal.
How do I transform such a Zp term into a nat term?
For example, how do I convert the above into

is_true (1 != 0)

Any advice would be greatly appreciated.

view this post on Zulip Pierre Jouvelot (Mar 30 2023 at 14:40):

A trick is to use

rewrite (inj_eq val_inj) /=.

to replace an equality on ordinals to an equality on nats.

You need to remember replace your equality by a boolean one, though, which you can do using reflection via eqP.

view this post on Zulip Alexander Gryzlov (Mar 30 2023 at 14:42):

In this particular case you can actually bypass manual injectivity reasoning withby apply: contra (Zp_nontrivial p')=>/eqP->.

view this post on Zulip Sebastian Ertel (Apr 04 2023 at 15:16):

Dears,
I'm sorry but even with the advice above I'm unable to finish off seemingly simple lemmas.
Here is an example (that is just a variant of the one above):

Lemma Zp1neqInZp0 : forall q:nat, 1 < q -> is_true (@Zp1 q != @inZp q 0).

I start with the advice from above to handle the inequality

move => q q_gt1.
apply: contra (Zp_nontrivial q).
rewrite /Zp1.

The goal now is

is_true (inZp 1 == inZp 0)  is_true (inZp 1 == 0)

Now there are 2 options:

  1. turn this into a propositional equality and go via f_equal
  2. continue with the boolean equality and follow the advice above

When following the first option, I fail to apply f_equal because what actually looks like a
perfect candidate for f_equal isn't:

move/eqP. f_equal.
rewrite /inZp.

The goal now is:

 Ordinal (n:=q.+1) (m:=1 %% q.+1) (ltn_pmod 1 (d:=q.+1) (ltn0Sn q)) =
 Ordinal (n:=q.+1) (m:=0 %% q.+1) (ltn_pmod 0 (d:=q.+1) (ltn0Sn q))
   is_true (Ordinal (n:=q.+2) (m:=1 %% q.+2) (ltn_pmod 1 (d:=q.+2) (ltn0Sn q.+1)) == 0)

The Ordinals do not only differ in m but also in the last argument.

If I try to follow the second option then the rewrites from above do not work out:

move/eqP. (* Going back to a boolean equality. *)
rewrite (inj_eq val_inj).

The error is

Error: The LHS of inj_eq
    (_ _ == _ _)
does not match any subterm of the goal

What am I missing here?

view this post on Zulip Notification Bot (Apr 04 2023 at 15:16):

Sebastian Ertel has marked this topic as unresolved.

view this post on Zulip Pierre Jouvelot (Apr 04 2023 at 15:27):

In this particular case, you probably need a - before the rewrite with inj_eq:

rewrite -(inj_eq val_inj) //=.

view this post on Zulip Laurent Théry (Apr 04 2023 at 15:38):

You can also take advantage of some computation of eqb and inZp :

Lemma Zp1neqInZp0 : forall q:nat, 1 < q -> is_true (@Zp1 q != @inZp q 0).
Proof. by case. Qed.

view this post on Zulip Sebastian Ertel (Apr 04 2023 at 18:51):

@Pierre Jouvelot, that was indeed the missing bit. Thanks a lot.
@Laurent Théry , wow, that solution is of course much neater. I checked again but the docs do not say anything about case doing any other computation. What is case doing to solve this goal?

view this post on Zulip Pierre Jouvelot (Apr 04 2023 at 19:54):

My understanding is that the case construct destructs the inductive top value (here q) into 0 and S q', and substitutes these values into the body of the forall, yielding two cases. The first case is trivially true (since 1 < 0 is false), while the second yields the expected inequality by partial evaluation of the body. @Laurent Théry could certainly explain this much better, though :smile:

view this post on Zulip Laurent Théry (Apr 04 2023 at 20:01):

@inZp q 1 constructs an ordinal on top of the modulo 1 %% (q.+1). By computaton, we get no information on this expression, it can be 0 if q = 0 or 1 if q > 0. Doing the case on q makes it becomes1 %% (q'.+2) and this time it computes to 1. So the goal becomes Zp 0 != Zp 1 and this is solve by computation of eqb.

view this post on Zulip Laurent Théry (Apr 04 2023 at 20:03):

not sure it is very clear....

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 09:54):

@Sebastian Ertel the other answers are correct but if you're wondering "what solved the goal", you might want to observe that by case means case; done — and done tries quite a few trivial steps (https://github.com/coq/coq/blob/v8.16/theories/ssr/ssreflect.v#L415-L421)


Last updated: Oct 13 2024 at 01:02 UTC