Неположительное возникновение из-за полиморфной функции - PullRequest
Новая
       22

Неположительное возникновение из-за полиморфной функции

0 голосов
/ 07 мая 2018

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

Это прекрасно работает: 

Require Import Coq.Lists.List.
Import ListNotations.

Inductive Foo :=  MkFoo : list Foo -> Foo.

И вот так:

Inductive Foo :=  MkFoo : forall (l : list Foo), Foo.

Но это не удается 

Inductive Foo :=  MkFoo : forall (l : list Foo), l <> [] -> Foo.

с 

Non strictly positive occurrence of "Foo"
in "forall l : list Foo, l <> [] -> Foo".

Я предполагаю, что это потому, что [] на самом деле @nil Foo и Coq не нравится это появление Foo.

В настоящее время я работаю над этим, используя вектор, например 

Require Import Coq.Vectors.Vector.

Inductive Foo :=  MkFoo : forall n (l : Vector.t Foo n), n <> 0 -> Foo.

, но осложнения, которые возникают из-за использованиязависимых структур данных в Coq заставляет меня задуматься:

Есть ли способ использовать простые списки в MkFoo и по-прежнему включать предложения об этом списке?

1 Ответ

0 голосов
/ 08 мая 2018

Я думаю, что нет способа включить это ограничение непосредственно в определение, к сожалению. Я вижу два пути вперед:

  1. Измените определение mkFoo, чтобы оно заняло заголовок списка в качестве дополнительного аргумента: 

    mkFoo : Foo -> list Foo -> Foo

  2. Определите Foo без каких-либо ограничений и определите отдельный предикат правильной формы: 

    Require Import Coq.Lists.List.

Inductive Foo := mkFoo : list Foo -> Foo.

Definition isEmpty {T : Type} (x : list T) :=
  match x with
  | nil => true
  | _   => false
  end.

Fixpoint wfFoo (x : Foo) : Foo :=
  match x with
  | mkFoo xs => negb (isEmpty xs) && forallb wfFoo xs
  end.

    Затем вы можете показать, что все функции на Foo, которые вам небезразличны, уважают wfFoo. Также возможно использовать подмножества типов для упаковки элементов Foo с доказательствами wfFoo, гарантируя, что клиентам Foo никогда не придется прикасаться к неправильно сформированным элементам. Поскольку wfFoo определено как логическое свойство, уравнение wfFoo x = true не имеет отношения к доказательствам, что гарантирует, что тип { x : Foo | wfFoo x = true } хорошо себя ведет. Библиотека математических компонентов обеспечивает хорошую поддержку для этого типа конструкции.

...