## Stream: math-comp users

### Topic: Conversion 'I_p <-> 'Z_p

#### Sebastian Ertel (Apr 12 2023 at 09:49):

Dear mathcomp-ers,

In the below script, I'm defining conversions `intoZp : 'I_p -> 'Z_p` and `fromZp : 'Z_p -> 'I_p`.
But in order to do so, I need to cast the `p` using `Zp_cast`.
When I now want to show `fromZp (intoZp x) = x`, I'm stuck dealing with the rewrite terms for the casts.
I was hoping that I could cancel out the two casts `(Zp_cast p_gt1)` and `-(Zp_cast p_gt1)` but I could not see how this is easily possible.
What would be the proper way of dealing with such rewrite terms?

I kept the script in one piece for easy copy-pasting into jsCoq or similar.

``````Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_algebra
fingroup.fingroup prime ssrnat ssreflect ssrfun ssrbool ssrnum.
Set Warnings "notation-overridden,ambiguous-paths".

Open Scope ring_scope.
Import GroupScope GRing.Theory.

Parameter gT : finGroupType.
Parameter prime_order : prime #|gT|.

Definition p := #|gT|.

Lemma p_gt1 : (1 < p)%N.
Proof.
apply (prime_gt1 prime_order).
Qed.

(* Fails because the [p] needs to be converted. *)
Fail Definition intoZp : 'I_p -> 'Z_p := enum_val.

(* Detour via nat (implicit coercion). *)
Definition intoZp : 'I_p -> 'Z_p := inZp.

(* Direct conversion via cast using the fact [1 < p]. *)
Definition intoZp' : 'I_p -> 'Z_p.
Proof.
rewrite -(Zp_cast p_gt1) //=.
Defined.

Fail Definition fromZp : 'Z_p -> 'I_p := enum_rank.

(* We cannot reuse the proof because its type needs to be converted. *)
Fail Definition fromZp : 'Z_p -> 'I_p :=
fun x =>
match x with
| Ordinal m m_lt_p => Ordinal m_lt_p
end.

(* The same as above but with casting the type of the proof. *)
Definition fromZp : 'Z_p -> 'I_p.
Proof.
case => m.
rewrite (Zp_cast p_gt1) => m_lt_p.
exact (Ordinal m_lt_p).
Defined.

(* But now I need to deal with these clunky rewrite terms. *)
Lemma intoZp_fromZp : forall x : 'I_p,
fromZp (intoZp' x) = x.
Proof.
rewrite /intoZp'/fromZp => x.
rewrite /eq_rect_r/eq_rect //=.
case: x => m m_lt_p //=.
Abort.

(* The alternative definition via [inZp] is not much better. *)
Lemma intoZp_fromZp' : forall x : 'I_p,
fromZp (intoZp x) = x.
Proof.
rewrite /intoZp/fromZp/inZp => x.
rewrite /eq_rect_r/eq_rect //=.
case: x => m m_lt_p //=.
Abort.
``````

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

Maybe you should use the fact that `'Z_p.+2` is convertible to `'I_p.+2`

#### Sebastian Ertel (Apr 12 2023 at 13:19):

Thanks for this idea @Laurent Théry .

This works for explicit specifications of `'I_p.-2.+2`

``````Definition fromZp'' (q:nat) : 'Z_q.+2 -> 'I_q.+2 := fun x => x.
Definition intoZp'' (q:nat) : 'I_q.+2 -> 'Z_q.+2 := fun x => x.

Definition fromZp''' (q:nat) : 'Z_q -> 'I_q.-2.+2 := fun x => x.
``````

But I do not find a way to construct such an explicit type from additional arguments
that restrict `q` (without using `Zp_cast`):

``````Definition into (q:nat) (H: (1 < q)%N) : 'I_q -> 'I_q.-2.+2.
``````

#### Laurent Théry (Apr 12 2023 at 19:11):

I am not 100% these convertions are useful but I would do something like this.

``````Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_algebra
fingroup.fingroup prime ssrnat ssreflect ssrfun ssrbool ssrnum.
Set Warnings "notation-overridden,ambiguous-paths".

Open Scope ring_scope.
Import GroupScope GRing.Theory.

Parameter gT : finGroupType.
Parameter prime_order : prime #|gT|.

Definition p := #|gT|.

Definition intoZp {p} : 'I_p -> 'Z_p :=
if p is _.+2 then id else (fun _ => ord0).

Definition fromZp {p} : (1 < p)%N -> 'Z_p -> 'I_p :=
if p is p'.+2 then  (fun _ => id) else
(fun H => False_rect _ (Bool.diff_false_true H)).

Lemma fact1 p (p_gt1 : (1 < p)%N) q : intoZp (fromZp p_gt1 q) = q.
Proof. by case: p p_gt1 q => [|[]]. Qed.

Lemma fact2 p (p_gt1 : (1 < p)%N) q : fromZp p_gt1 (intoZp q) = q.
Proof. by case: p p_gt1 q => [|[]]. Qed.
``````

Last updated: Jul 23 2024 at 20:01 UTC