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

Maybe you should use the fact that `'Z_p.+2`

is convertible to `'I_p.+2`

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

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