Ssreflect Users Discussion List

[georges gonthier <>]

  The easiest is to not select occurrences and just change p to pdiv p 
everywhere, including in the type of m, changing back later if needed 
(unlikely, since pdiv p is always a prime).
If you really want to be selective, then note that indeed ‘Z_p does not 
appear in the goal because Ltac erases type casts, so only the structures 
inferred from ‘Z_p will actually appear in the goal.
All of these are parametrised by (part of) the modulus index - the n in ‘I_n.
    More precisely, as ‘Z_p is notation for ‘I_(Zp_trunc p).+2, structures 
that are generic to ordinal have a (Zp_trunc p).+2 parameter, additive group 
structures and operations have a (Zp_trunc p).+1 parameter, and 
multiplicative ones a (Zp_trunc p) parameter. Here the eqType hidden argument 
of == in in inZp p != 0 :> ‘Z_p falls in the first category, and the inZp 
operation and the 0 fall in the second.
  In all cases either
     rewrite -[in Zp_trunc p](pdiv_id p_pr) or rewrite -[p as q in Zp_trunc 
q]pdiv_id //
will do exactly the job required, and not rewrite occurrences of p in 
(Zp_trunc (p ^ i.+1)) which are linked to the type of m (namely ‘I_(Zp_trunc 
(p ^ i.+1)).+2).
   Georges

> Le 26 sept. 2019 à 11:56, Florent Hivert 
> <>
>  a écrit :
> 
> On Thu, Sep 26, 2019 at 10:43:16AM +0200, Laurent Thery wrote:
>> One way to do this is to explicitly mention the m that needs to be
>> rewritten.
>> 
>> rewrite -(pdiv_id Hp) in m |- *.
> 
> Thanks to Laurent trick, it is easy to change a 'Z_p into a 'F_p...  
> However,
> It is very tricky to find where. Here is an example:
> 
> Variables (p : nat) (p_pr : prime p).
> Lemma bla (i : nat) (m : 'Z_(p ^ i.+1)) :
>  inZp m != 0 :> 'Z_p -> m \is a GRing.unit.
> 
> The only solution I've found is :
> 
>  rewrite -{1 2 4}(pdiv_id p_pr).
> 
> using "set printing all to figure out which one of the 9 occurrences of p
> needs to be rewritten. I tried
> 
>  rewrite -[in 'Z_p](pdiv_id p_pr).
> 
> and got
> 
>  term 'Z_p does not match any subterm of the goal
> 
> Does someone have any other trick to select the right occurrences ?
> 
> Thanks for the help,
> 
> Best,
> 
> Florent