The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

You can probably define ring and field structures for a generic n, but you
still need to do one "Add Ring" command for each n.
But n can be a Section Variable, so if you have lemmas which work for all n,
you can first define n as a Section Variable, and then do "Add Ring" inside
the Section. For example, we do so here:
https://github.com/mit-plv/coqutil/blob/2f8a6b209f/src/Word/Properties.v#L447
The feature which is missing, IMHO, is something like a parametrized "Add
Ring" command, or a "ring" tactic which takes the ring structure as an
argument and does not depend on an "Add Ring" vernacular.
And another caveat to be aware of is that you can't do "Add Ring" inside a
Section if you're using Universe Polymorphism, see 
https://github.com/coq/coq/issues/9201.

On Wed, 2019-09-04 at 02:53 -0700, Xuanrui Qi wrote:
> Hello all,
> 
> I am looking for a way to use the ring/field family of tactics for
> rings & fields parametrized over a value. One canonical example would
> be the Galois fields, say the family of fields GF(2^n). 
> 
> Each member of this family form a field, but I don't want to define
> `field_theory` structures for each of GF(2), GF(4), GF(8), etc. Is
> there a way I can do this just once and get `field` for free for each
> of GF(2), GF(4), GF(8), etc.?
> 
> I know for rings there is ring_morph, but that doesn't exactly look
> like what I want. From what I understand, it is used to derive `ring`
> via a ring morphism (e.g., from Z to Z[x]).
> 
> What should I do for my use case?
> 
> Best,
> Xuanrui
>