Stream: math-comp users

Topic: ✔ cast in 'Z_p


view this post on Zulip Florent Hivert (Feb 13 2024 at 10:11):

I need to prove the following goal:

  p : nat
  p_pr : prime p
  a, b : 'Z_(p ^ 1)
  ============================
  a != 0 -> b != 0 -> a * b != 0

The command

 rewrite expn1 in a b |- *.

allows to easily get rid of the p ^ 1. Now I would like MC to understand that I'm in 'F_p, I try to do

  rewrite -(Fp_Zcast p_pr) in a b |- *.

And it leads to a dependent type error. How can I solve this problem ? I can try to use the ismorphism

  have eq_p := (Fp_Zcast p_pr); pose f := cast_ord (esym eq_p).

but now I need to prove that fis a ring morphism. I find it currently painful. Is there simpler way ?

view this post on Zulip Cyril Cohen (Feb 13 2024 at 10:26):

Indeed! If you redefine Fp_Zcast it works, I think this should be fixed in mc.

Lemma Fp_Zcast [p : nat] : prime p -> Zp_trunc (pdiv p) = Zp_trunc p.
Proof. by move=> /Fp_Zcast[[]]. Qed.

Lemma test (p : nat) (p_pr : prime p) (a b : 'Z_(p ^ 1)) :
  a != 0 -> b != 0 -> a * b != 0.
Proof.
rewrite -Fp_Zcast // in a b *.
exact: mulf_neq0.
Qed.

view this post on Zulip Florent Hivert (Feb 13 2024 at 10:28):

Cyril Cohen said:

Indeed! If you redefine Fp_Zcast it works, I think this should be fixed in mc.

Lemma Fp_Zcast [p : nat] : prime p -> Zp_trunc (pdiv p) = Zp_trunc p.
Proof. by move=> /Fp_Zcast[[]]. Qed.
````

Neat ! I'm sumbitting a pull request !

view this post on Zulip Notification Bot (Feb 13 2024 at 10:33):

Cyril Cohen has marked this topic as resolved.


Last updated: Jul 15 2024 at 21:02 UTC