Преобразуйте случайный список в зависимо типизированный список в Coq - PullRequest
Новая
       46

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

3 голосов
/ 13 марта 2019

У меня есть следующее определение списка в 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, что уже доказано. Я не могу позволить Коку узнать эту правду.

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

1 Ответ

5 голосов
/ 14 марта 2019

Вы можете использовать зависимое сопоставление с шаблоном, так как тип результата 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).

...