Ssreflect Users Discussion List

[Florent Hivert <>]

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