В стандартной структуре полей библиотеки сначала нужно показать структуру кольца, на которой будет лежать это поле.Для этой кольцевой структуры нам нужно выяснить, что служит противоположной функцией, а что - функцией вычитания.Ответ таков: обратная функция тождества и вычитание также xorb.Итак, сначала мы хотим выразить, что false, true, xorb, andb, xorb и (fun x => x) составляют кольцо.В случае Coq нам также необходимо указать, какое отношение эквивалентности мы будем использовать для идентификации двух членов кольца, в этом случае мы выбираем простое равенство @eq bool.Чтобы описать такую кольцевую структуру, нам нужно создать объект типа.
Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).
Самый простой способ сделать это - просто сказать, что мы хотим сделать это, не предоставляя значение для структурыи используйте режим доказательства , чтобы помочь обнаружить все предложения, которые необходимо проверить.
Definition GF2_ring :
Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).
Ответ системы просто повторяет ожидаемый тип.Теперь мы можем сказать Coq, что хотим применить конструктор записи.
apply Ring_theory.mk_rt.
Это создает 9 целей, каждая из которых проверяет одно из ожидаемых свойств кольца: свойства нейтрального элемента, ассоциативность, коммутативность, дистрибутивностьи свойство противоположной функции.
Вы можете искать существующие теоремы, выражающие все эти свойства, но другой возможностью является проверка этих свойств путем проверки всех возможных случаев для всех переменных.Это сделано в следующем полном доказательстве.
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.
Аналогичная структура доказательства может использоваться для завершения структуры поля.
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.
Теперь, что вам дает?ring_theory и field_theory фактически являются промежуточными инструментами для реализации тактики ring и field.Таким образом, вы можете использовать объект GF2_Field в команде Add Field, но в случае GF (2) эта тактика не так полезна, как в случае числовых полей.
Если вы заинтересованы в алгебраическомструктуры, я думаю, вы должны смотреть на такие разработки, как математические компоненты или математические классы .