Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Automation for ring/field family tactics parametrized over a variable

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automation for ring/field family tactics parametrized over a variable


Chronological Thread 
  • From: Samuel Gruetter <gruetter AT mit.edu>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Automation for ring/field family tactics parametrized over a variable
  • Date: Wed, 4 Sep 2019 18:08:31 +0000
  • Accept-language: en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gruetter AT mit.edu; spf=Pass smtp.mailfrom=gruetter AT mit.edu; spf=None smtp.helo=postmaster AT outgoing-exchange-1.mit.edu
  • Ironport-phdr: 9a23:g+WJjh0tcI4LaBFrsmDT+DRfVm0co7zxezQtwd8ZseIWI/ad9pjvdHbS+e9qxAeQG9mCsbQd1Led6vmwEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCejbb9oMRm7rwXcusYLjYd/Kas61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9Zwgbpbrhy/uhJ/34DaboKbNPV8f6PSYdwUSmVaU8ZNTCNMGJ+wY5cTA+cDO+tTsonzp0EJrRu7HQSiGfngyjpVhnDo2a0xzuUvERvb3AM+A9IOrGrbrM/oP6oVXuC11rTIwivfb/NKxzj98pPFchUgofGQR75/b9feyVQ2Gg7Dk16ep4vlPzaP2eQMtWiW9+VgVeOzi24ntgF+uSKjydsrionMgI8e11PK9T1hzYooJtC0Ukp2bcS6HJZTrS2WKot7Tts/T212uys20LMLtYOhcCUExpkr3QDTZ+KHfoSQ/x7uV/ydLDNiiH9qYr6zmgu+/Eemx+bhTMe7ykxKoTBAktTUtnACyRjT6s+fR/t640ehxTmP1wfS6uFCLkA4jLTUKpE9zb4wjJUTt0vDETHvlEnrlqOWc0Qk+vSy5+v5f7rmu4eQN45yig7gLqQjgtGzDOciPgUKRWSX5+ex2Kf+8UD5WLlKi+c5kqjdsJDUP8Qboau5Dhda0oY59hawESum0MgGknkdN19FfROHj5TzN17QPf/4EO+zg06wnzdz2/DGIrrhD43RIXjEibftZKpy60pByAUo1t1f/JJVCrQZIP3pQEPxtdrYDgU4MwOu2ernBs99hcsiXjfFCaiAdajWrFWg5+Q1IuDKapVf8GL2LOFg7Przh1c4n0UcdO+nx81ERmq/G6FdKkCEbH6krc0cHHsWsxB2GOPwlVCeTTNJT3OzQ+Qx6ixtW9HuNpvKWo342O/J5yy8BJADPjkaWGDJKm/hcsC/Y9lJcDibc51kkyBCWLS8Gdd4iEOe8TTiwr8iFdL6vy0VsZW5hYpy+vHckhA0+nl5H8+d2meCQiQt2GYJW3k70L0t+RUsmGfG6rBxhrljLfIW4vpIVgkgMpuNnel7F5b/Vh+TJ9o=

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
>



Archive powered by MHonArc 2.6.18.

Top of Page