## Stream: math-comp users

### Topic: ✔ Calculating in Zmodp

#### Sebastian Ertel (Mar 31 2023 at 07:41):

Thanks a lot for the advice. Both are good helpers.
I believe that the `rewrite (inj_eq val_inj)` trick is essentially the same as using `eqP` to turn the boolean equality into a propositional one and afterwards using `f_equal`. Right?
Of course, this only works if `val` is the only input that differs.

(For the record, of course the above suggestions cannot easily finish off the goal without requiring that `1 < p` for the `p` of `Zp` holds .)

#### Notification Bot (Mar 31 2023 at 07:42):

Sebastian Ertel has marked this topic as resolved.

#### Alexander Gryzlov (Mar 31 2023 at 22:20):

Sebastian Ertel said:

Thanks a lot for the advice. Both are good helpers.
I believe that the `rewrite (inj_eq val_inj)` trick is essentially the same as using `eqP` to turn the boolean equality into a propositional one and afterwards using `f_equal`. Right?
Of course, this only works if `val` is the only input that differs.

(For the record, of course the above suggestions cannot easily finish off the goal without requiring that `1 < p` for the `p` of `Zp` holds .)

Not exactly, it's converts boolean equality on subtypes into boolean equality on their value projections.

#### Sebastian Ertel (Apr 03 2023 at 07:22):

Ah yes, you are right. Thanks again for this clarification.

#### Sebastian Ertel (Apr 05 2023 at 10:44):

Thank very much for the answers.
@Paolo Giarrusso, yes, that was actually what I was trying to understand. It is not `case` that "performs the computation" but actually the `by` which executes `done`.

I was able to "visualize" this for me by writing it more verbosely.

``````Lemma Zp1neqInZp0 :  forall p:nat, (1 < p)%N -> is_true (@Zp1 p != @inZp p 0).
Proof.
case.
- move => //=.
- move => //=.
Qed.
``````

Thanks a lot for your great help!

#### Notification Bot (Apr 05 2023 at 10:45):

Sebastian Ertel has marked this topic as resolved.

#### Laurent Théry (Apr 05 2023 at 11:27):

You can also have a slow motion :

``````Lemma Zp1neqInZp0 :  forall p:nat, (1 < p)%N -> is_true (@Zp1 p != @inZp p 0).
Proof.
case.
- rewrite -[1 < 0]/false.
by [].
- move=> n _.
rewrite -[_ != _]/(1 != 0 %[mod n.+2]).
rewrite -[1 %% _]/1.
rewrite -[0 %% _]/0.
by [].
Qed.
``````
``````
``````

#### Laurent Théry (Apr 05 2023 at 12:27):

And without the case :

``````Lemma Zp1neqInZp0 :  forall p:nat, (1 < p)%N -> is_true (@Zp1 p != @inZp p 0).
Proof.
move=> q Hq.
rewrite -[_ != _]/(1 != 0 %[mod q.+1]).
rewrite -[0 %% _]/0.
Fail rewrite -[1 %% _]/1.
Qed.
``````

#### Sebastian Ertel (Apr 05 2023 at 14:03):

It is slow but certainly speeds up my understanding of things ;)
Thanks a lot!

Last updated: Jul 25 2024 at 16:02 UTC