coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Xuanrui Qi <xqi01 AT cs.tufts.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Automation for ring/field family tactics parametrized over a variable
Date: Wed, 04 Sep 2019 02:53:18 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xqi01 AT cs.tufts.edu; spf=Pass smtp.mailfrom=xqi01 AT cs.tufts.edu; spf=None smtp.helo=postmaster AT vm-delivery1.eecs.tufts.edu
Ironport-phdr: 9a23:+1SX0xQQ3Sq14LWGGT67w9JcvNpsv+yvbD5Q0YIujvd0So/mwa69YheN2/xhgRfzUJnB7Loc0qyK6vqmADNdqs/R+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiooQnLq8Ubg4tvJqksxhbKv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqR9izYDUfo+bOuZxca3Sct4BSmpNQtxcWjZdDo6mbYYCCfcKM+ZCr4n6olsDtRqxBRS2C+Pp0D9Im3721rAh3eQgDArL2wMhH8sPsHjIsdn4L7sdUfuvwKnU0DXDYe9W2Szn5IfWbx8hvOiBULRtesTfzkkvEhnKjlSWqYH9MDKVy/4Cs26B7+p9VOKvkm8npxttrTiow8chjJTCiIENyl3c6Cl0zpo5Kce5RUN0e9KoDpVduzuUOoZ0Ws8vQW9ltDw+x7AIo5K3YSgHxZo9yxLCaPGKcI6F6Q/5WumLOzd3nndldaq/hxms9UigzfXxVtex0FpTsyVKjN3MtnET1xPN8MiGSuZx8l2/1jmRyw/T8ftIIVwplarVN54h2aQ8mYQOvkTeBiP2mUP2g7GKdkg85+Sl5fjrbq/nq5KTLYN4lA/zPr4gl8G9Geg4NxIBX2mf+eSyzr3j+kj5Ta1Fj/0vk6nVrI3WKN8Hqa6iGQNVzpsj6xijDze9ytgXg2QILE9ddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd9V14UEWGvJDLXKHrnVtAq4++spOfSNLLYU8GLtMvl9vtblljklhFEBZu+k0YZBOyPwJehvP0jMOSmkudwGC2pf5lNvHtyvs0WLVHtoX1j3Wqs94j8hD4f/UdXIXcaxnbKdx2G2EoAEPzkaWGDJKm/hcsC/Y9lJcDibe5MzmSdCSaWvV5Rn2B2z5lejluhXa9HM8yhdjqrNkdh44+qJxEMs8Hl4AsCczWyXXjgyk24DXHkqwa5jugpwxkrRiaU=

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

--
Xuanrui Qi

xqi01 AT cs.tufts.edu
me AT xuanruiqi.com
https://www.xuanruiqi.com

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] Automation for ring/field family tactics parametrized over a variable, Xuanrui Qi, 09/04/2019
- Re: [Coq-Club] Automation for ring/field family tactics parametrized over a variable, Samuel Gruetter, 09/04/2019