Преобразуйте случайный список в список с зависимой типизацией в Coq

У меня есть следующее определение списка в Coq:

Variable A : Set.
Variable P : A -> Prop.
Hypothesis P_dec : forall x, {P x}+{~(P x)}.

Inductive plist : nat -> Set :=
   pnil : plist O
  | pcons : A -> forall n, plist n -> plist n
  | pconsp : forall (a:A) n, plist n -> P a -> plist (S n)
  .

Он описывает «список элементов типа A, где по крайней мере n из них выполняют предикат P».

Моя задача - создать функцию, которая будет преобразовывать случайный список в plist (с максимально возможным n). Моя попытка заключалась в том, чтобы сначала подсчитать все элементы, которые соответствуют P, а затем установить тип вывода в соответствии с результатом:

Fixpoint pcount (l : list A) : nat :=
  match l with
  | nil => O
  | h::t => if P_dec h then S(pcount t) else pcount t
  end.

Fixpoint plistIn (l : list A) : (plist (pcount l)) :=
  match l with
  | nil => pnil
  | h::t => match P_dec h with
          | left proof => pconsp h _ (plistIn t) proof
          | right _ => pcons h _ (plistIn t) 
          end
  end.

Однако я получаю сообщение об ошибке в строке с left proof:

Error:
In environment
A : Set
P : A -> Prop
P_dec : forall x : A, {P x} + {~ P x}
plistIn : forall l : list A, plist (pcount l)
l : list A
h : A
t : list A
proof : P h
The term "pconsp h (pcount t) (plistIn t) proof" has type
 "plist (S (pcount t))" while it is expected to have type
 "plist (pcount (h :: t))".

Проблема в том, что Coq не видит, что S (pcount t) равно pcount (h :: t), зная, что P h, что уже было доказано. Я не могу позволить Coq узнать эту правду.

Как правильно определить эту функцию? Возможно ли это вообще?


dependent-type coq
person radrow    schedule 13.03.2019    source источник

Ответы (1)


arrow_upward
5
arrow_downward

Вы можете использовать зависимое сопоставление с образцом, поскольку тип результата plist (pcount (h :: t)) зависит от того, является ли P_dec h left или right.

Ниже ключевое слово as вводит новую переменную p, а return указывает тип всего match выражения, параметризованного p.

Fixpoint plistIn (l : list A) : (plist (pcount l)) :=
  match l with
  | nil => pnil
  | h::t => match P_dec h as p return plist (if p then _ else _) with
          | left proof => pconsp h (pcount t) (plistIn t) proof
          | right _ => pcons h _ (plistIn t) 
          end
  end.

Тип plist (if p then _ else _) должен быть равен plist (pcount (h :: t)) при замене p := P_dec h. Затем в каждой ветви, скажем, left proof, вам нужно произвести plist (if left proof then _ else _) (что сводится к левой ветви).

Немного волшебно, что Coq может сделать вывод о том, что здесь указано в подчеркивании, но на всякий случай вы всегда можете указать это по буквам: if p then S (pcount t) else pcount t (что предназначено для точного соответствия определению pcount).

person Li-yao Xia    schedule 14.03.2019
comment
Не могли бы вы объяснить, почему return if p then plist (S (pcount t)) else plist (pcount t) with здесь не работает, или я должен задать другой вопрос? - person radrow; 14.03.2019
comment
Здесь все хорошо. Это не работает, потому что при проверке того, равно ли if P_dec h then plist (S (pcount t)) else plist (pcount t) plist (if P_dec h then S (pcount t) else pcount t), проверка типов учитывает только бета-эквивалентность, но эти два термина не являются бета-эквивалентами. Вы можете доказать (if ... then pcount ... else pcount ... ) = pcount (if ... then ... else ...) как теорему, но это = (пропозициональное равенство) является гораздо более слабым понятием равенства, чем бета-эквивалентность (или, точнее, дефиниционное равенство), которое используется проверкой типов. - person Li-yao Xia; 14.03.2019