Stream: math-comp users

Topic: Calculating in Zmodp

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.

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 `nat`s.

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

Alexander Gryzlov (Mar 30 2023 at 14:42):

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

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

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

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 `Ordinal`s 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?

Notification Bot (Apr 04 2023 at 15:16):

Sebastian Ertel has marked this topic as unresolved.

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) //=.
``````

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

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?

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:

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 becomes`1 %% (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`.

Laurent Théry (Apr 04 2023 at 20:03):

not sure it is very clear....

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: Jul 23 2024 at 21:01 UTC