Равенство конечных отображений в coq (определено с помощью map2) - PullRequest
Новая
       24

Равенство конечных отображений в coq (определено с помощью map2)

0 голосов
/ 20 октября 2018

Предположим, я хочу определить тип мономов в Coq.Это будут конечные карты из некоторого упорядоченного набора переменных в nat, где, скажем, x²y³ представлен картой, которая отправляет x в 2, y в 3 и где все остальное получает значение по умолчанию, ноль.

основные определения не кажутся такими сложными: 

Require Import
  Coq.FSets.FMapFacts
  Coq.FSets.FMapList
  Coq.Structures.OrderedType.

Module Monomial (K : OrderedType).
  Module M := FMapList.Make(K).

  Module P := WProperties_fun K M.
  Module F := P.F.

  Definition Var : Type := M.key.
  Definition Monomial : Type := M.t nat.

  Definition mon_one : Monomial := M.empty _.

  Definition add_at (a : option nat) (b : option nat) : option nat :=
    match a, b with
      | Some aa, Some bb => Some (aa + bb)
      | Some aa, None => Some aa
      | None, Some bb => Some bb
      | None, None => None
    end.

  Definition mon_times (M : Monomial) (M' : Monomial) : Monomial :=
    M.map2 add_at M M'.

End Monomial.

На данный момент я хотел бы доказать что-то вроде: 

Lemma mon_times_comm : forall M M', mon_times M M' = mon_times M' M.

Я вижу, как доказать, что две картыEqual используют лемму Equal_mapsto_iff, но я действительно хотел бы сказать, что мой тип действительно представляет мономы и что умножение действительно коммутативно (и карты eq).

Ядовольно плохо для Coq: это разумная вещь, чтобы попытаться доказать?

Кроме того, я понимаю, что это может зависеть от реализации конечной карты: если FMapList был неправильный выбор, а другая реализация облегчает это,пожалуйста, укажите мне на это!

Ответы [ 2 ]

0 голосов
/ 21 октября 2018

Я могу видеть, как доказать, что две карты равны, используя лемму Equal_mapsto_iff, но я действительно хотел бы сказать, что мой тип действительно представляет мономы и что умножение действительно коммутативно (и карты эквивалентны).

Я довольно новичок в Coq: это разумная вещь, чтобы попытаться доказать?

Кроме того, я понимаю, что это может зависеть от конечной реализации карты: если FMapList был неправильнымВыбор и другая реализация делают это проще, пожалуйста, укажите мне на это!

Действительно, вы на правильном пути.Тип набора, который вы используете, не обладает тем свойством, что два набора с одинаковыми элементами определенно равны в Coq.Поскольку такие наборы реализованы в виде бинарных деревьев, у вас может быть Node(A, Node(B,C)) <> Node(Node(A,B),C).

В частности, наличие хорошего «типа набора» является чрезвычайно сложной задачей в Coq из-за нескольких проблем, см. Anwser Какчтобы определить set в coq без определения set в виде списка элементов для дальнейшего обсуждения.

Для правильной алгебры действительно требуется много сложной инфраструктуры, указатель @ ErikMD - правильный, выследует взглянуть на математику и связанные с ней документы, чтобы получить представление о современном уровне техники.Конечно, продолжайте экспериментировать!

0 голосов
/ 20 октября 2018

Что касается формализации мономов и многомерных полиномов в Coq, вы можете рассмотреть возможность использования библиотеки multinomials .Он доступен для OPAM: 

$ opam install coq-mathcomp-multinomials

и, естественно, подтверждает результат, аналогичный вашей mon_times_comm лемме: 

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
From mathcomp Require Import choice finfun tuple fintype ssralg bigop.
From SsrMultinomials Require Import freeg mpoly.

Lemma test1 (n : nat) (m1 m2 : 'X_{1..n}) : (m1 + m2 = m2 + m1)%MM.
Proof.
move=> *.
by rewrite addmC.
Qed.

Lemma test2 (n : nat) (R : comRingType) (p q : {mpoly R[n]}) :
  (p * q = q * p)%R.
Proof.
move=> *.
by rewrite mpoly_mulC.
Qed.

Обратите внимание, что библиотека многочленов построена на MathComp библиотека, которая тесно связана с расширением SSReflect языка доказательств Coq .

Наконец, обратите внимание, что эта библиотека очень удобна для разработки доказательств Coq, включающих полиномиальные полиномы, но ненапрямую не разрешать вычисления с этими типами данных Coq (Eval vm_compute in ...).Если вас также интересует этот аспект, вы также можете взглянуть на библиотеку CoqEAL (и, в частности, ее теорию multipoly.v , основанную на FMaps).

...