Stream: math-comp users

Topic: Conversion 'I_p <-> 'Z_p


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

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

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

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