Трудности в доказательстве равенства с использованием библиотеки Coq MSet - PullRequest
Новая
       2

Трудности в доказательстве равенства с использованием библиотеки Coq MSet

1 голос
/ 23 марта 2020

Я использую библиотеку Coq MSet в своей разработке, и у меня возникают некоторые проблемы с использованием обобщенного переписывания с использованием значений MSet. Ниже у меня есть упрощенная версия моей проблемы:

Сначала нам нужно определить модули для MSet. 

Module NSet := Make Nat_as_OT.
Module NSetDec := MSetDecide.WDecide NSet.

И у меня есть функция следующего типа: 

Parameter calc : NSet.t -> string -> bool.

Я хочу переписать установленные равенства, присутствующие в вызовах функции calc. Для этого я попытался определить экземпляр типа Proper следующим образом. 

Instance calc_proper 
  : Proper (NSet.Equal ==> @eq string ==> @eq bool) calc.
Proof.
   intros S S' H s s' H1.
   rewrite H1.
   rewrite H. (** error here! *)

Я сомневаюсь, как завершить sh такой экземпляр. Когда я пытаюсь выполнить последний rewrite, Coq возвращает следующее сообщение об ошибке: 

  Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
   UNDEFINED EVARS:
   ?X33==[S S' H s s' H1 |- relation bool] (internal placeholder) {?r}
   ?X34==[S S' H s s' H1 |- relation string] (internal placeholder) {?r0}
   ?X35==[S S' H s s' H1 (do_subrelation:=do_subrelation)
           |- Proper (NSet.Equal ==> ?r0 ==> ?r) calc] (internal placeholder) {?p}
   ?X36==[S S' H s s' H1 |- ProperProxy ?r0 s'] (internal placeholder) {?p0}
   ?X38==[S S' H s s' H1 |- relation bool] (internal placeholder) {?r1}
   ?X39==[S S' H s s' H1 (do_subrelation:=do_subrelation)
           |- Proper (?r ==> ?r1 ==> flip impl) eq] (internal placeholder) {?p1}
   ?X40==[S S' H s s' H1 |- ProperProxy ?r1 (calc S' s')] (internal placeholder) {?p2}
           TYPECLASSES:?X33 ?X34 ?X35 ?X36 ?X38 ?X39 ?X40

. Кажется, что в моем коде отсутствуют некоторые экземпляры. Минимальный пример, который демонстрирует проблему, доступен в следующем gist.

1 Ответ

1 голос
/ 23 марта 2020

Экземпляр Proper является частью обязательств, которые вам необходимо иметь для использования rewrite в первую очередь. Вам нужно доказать это, используя более элементарные методы.

...