How to define a specific field in Coq

Question

I am trying to construct GF(2) in Coq using the standard library definition of a field over the standard library's boolean implementation.

to be clear:

• "true" should be the field's "1" element.

• "false" should be the field's "0" element.

• "xorb" should be addititon.

• "andb" should be multiplication.

I'd expect that I should have to pass this information to some record from here and provide a correctness proof. However, I can't figure out how to set this up.

Answer 1

In the standard library field structure, you first need to exhibit the ring structure on which this field will rest. For this ring structure we need to figure out what serves as the opposite function and what serves as the subtraction function. The answer is: the opposite is the identity function and the subtraction is also xorb. So we first want to express that false, true, xorb, andb, xorb, and (fun x => x) constitute a ring. In the case, of Coq, we also need to specify what equivalence relation we will use to identify two terms of the ring, in this case we pick the plain equality @eq bool. To describe such a ring structure, we need to create an object of type.

 Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).

The simplest way to do that, is to just say that we want to do it, without providing the value for the structure, and use proof mode to help discover all the propositions that need to be verified.

Definition GF2_ring :
   Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).

The answer of the system just repeats the expected type. We can now tell Coq that we want to apply the record constructor.

apply Ring_theory.mk_rt.

This creates 9 goals, each of which verifies one of the expected properties of a ring: neutral element properties, associativity, commutativity, distributivity, and property of the opposite function.

You can search for existing theorems expressing all these properties, but another possibility is to verify these properties by checking all possible cases for all variables. This is done in the following complete proof.

Require Import Field.

Definition GF2_ring :
   Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).
Proof.
apply Ring_theory.mk_rt;
  solve[now intros [] | now intros [] [] | now intros [] [] []].
Qed.

A similar proof structure can be used to complete the field structure.

Definition GF2_Field :
  field_theory false true xorb andb xorb (fun x => x) andb (fun x => x) (@eq bool).
constructor; try solve[exact GF2_ring | now easy ].
now intros [] abs; auto; try case abs.
Qed.

Now, what does give to you? The ring_theory and field_theory actually intermediate tools for the implimentation of the ring and field tactics. So you can use the object GF2_Field in the Add Field command, but in the case of GF(2), these tactics are not as useful as in the case of number fields.

If you are interested in algebraic structures, I think you should rather look at developments like mathematical components or math classes.