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.

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`

.

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

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:

- turn this into a propositional equality and go via
`f_equal`

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

Sebastian Ertel has marked this topic as unresolved.

In this particular case, you probably need a `-`

before the `rewrite`

with `inj_eq`

:

```
rewrite -(inj_eq val_inj) //=.
```

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

@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?

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:

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

.

not sure it is very clear....

@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