Stream: math-comp users

Topic: ✔ Calculating in Zmodp


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

view this post on Zulip Notification Bot (Mar 31 2023 at 07:42):

Sebastian Ertel has marked this topic as resolved.

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

view this post on Zulip Sebastian Ertel (Apr 03 2023 at 07:22):

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

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

view this post on Zulip Notification Bot (Apr 05 2023 at 10:45):

Sebastian Ertel has marked this topic as resolved.

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

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

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