Как реализовать удаление с доказательством членства в качестве аргумента в Coq?

Question

data _∈_ {X : Set} (x : X) : (xs : List X) → Set where
  here! : {xs : List X} → x ∈ x ∷ xs
  there : {xs : List X} {y : X} (pr : x ∈ xs) → x ∈ y ∷ xs

remove : {X : Set} {x : X} (xs : List X) (pr : x ∈ xs) → List X
remove (_ ∷ xs) here!      = xs
remove (y ∷ xs) (there pr) = y ∷ remove xs pr

Я пытаюсь перевести приведенное выше определение с Агды на Кок и сталкиваюсь с трудностями.

Inductive Any {A : Type} (P : A -> Type) : list A -> Prop :=
  | here : forall {x : A} {xs : list A}, P x -> Any P (x :: xs)
  | there : forall {x : A} {xs : list A}, Any P xs -> Any P (x :: xs).

Definition In' {A : Type} (x : A) xs := Any (fun x' => x = x') xs.

Fixpoint remove {A : Type} {x : A} {l : list A} (pr : In' x l) : list A :=
  match l, pr with
  | [], _ => []
  | _ :: ls, here _ _ => ls
  | x :: ls, there _ pr => x :: remove pr
  end.

Incorrect elimination of "pr0" in the inductive type "@Any":
the return type has sort "Type" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

В дополнение к этой ошибке, если я уйду из дела [], Coq попросит предоставить его, несмотря на абсурд.

До этого момента я думал, что Agda и Coq - это одни и те же языки с разным интерфейсом, но теперь я начинаю думать, что они разные под капотом. Есть ли способ повторить функцию удаления в Coq, и если нет, какую альтернативу вы бы порекомендовали?

Редактировать : Я также хочу сохранить доказательства между In и In'. Первоначально я сделал In' a Type, а не Prop, но это сделало следующее доказательство неудачным с ошибкой типа.

Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | [] ⇒ False
  | x' :: l' ⇒ x' = x ∨ In x l'
  end.

Theorem In_iff_In' : 
  forall {A : Type} (x : A) (l : list A), 
  In x l <-> In' x l.
Proof. 
intros.
split.
- intros.
  induction l.
  + inversion H.
  + simpl in H.
    destruct H; subst.
    * apply here. reflexivity.
    * apply there. apply IHl. assumption.
- intros.
  induction H.
  + left. subst. reflexivity.
  + right. assumption.
Qed.

In environment
A : Type
x : A
l : list A
The term "In' x l" has type "Type" while it is expected to have type 
"Prop" (universe inconsistency).

Здесь In взято из главы Logic SF. У меня есть решение принципа голубиных ям в Агде, поэтому я хочу эту биекцию, чтобы преобразовать ее в форму, которую требует упражнение.

Edit2

Theorem remove_lemma :
  forall {A} {x} {y} {l : list A} (pr : In' x l) (pr' : In' y l),
  x = y \/ In' y (remove pr).

Я также откровенно сталкиваюсь с непоследовательностью вселенных в этом определении, даже когда использую Type при определении In'.

Answer 1

Вам необходимо использовать информативное подтверждение членства.Прямо сейчас ваш Any принимает значения в Prop, что в силу его ограничений на удаление (см. Полученное вами сообщение об ошибке) соответствует аксиоме forall (P: Prop) (x y: P), x = y.Это означает, что если у вас есть какой-то термин, который зависит от термина, тип которого находится в Prop (как в случае с remove), он должен использовать только тот факт, что такой термин существует, а не то, каким термином он является конкретно,Как правило, вы не можете использовать исключение (обычно сопоставление с образцом) на Prop для создания чего-либо, кроме того, что также является Prop.

. Существуют три принципиально различных доказательства In' 1 [1; 2; 1; 3; 1; 4], и,в зависимости от того, какое доказательство используется, remove p может быть [2; 1; 4; 1; 4], [1; 2; 3; 1; 4] или [1; 2; 1; 3; 4].Поэтому вывод существенно зависит от конкретного доказательства.

Чтобы это исправить, вы можете просто заменить Prop в Inductive Any {A : Type} (P : A -> Type) : list A -> Prop на Type. ¹ Теперь мы можемисключите не Prop типы, и ваше определение remove работает как написано.

---

Чтобы ответить на ваши изменения, я думаю, что самая большая проблема заключается в том, что некоторые из ваших теорем / определений нуждаются в In'быть Prop (потому что они зависят от неинформативных доказательств), а другим нужно информативное доказательство.

Я думаю, что вам лучше всего оставить In' как Type, но затем доказать неинформативные версиитеоремы.В стандартной библиотеке, в Coq.Init.Logic, есть индуктивный тип inhabited.

Inductive inhabited (A: Type): Prop :=
| inhabits: A -> inhabited A.

. Он принимает тип и, по существу, забывает что-либо конкретное о его терминах, помня только, обитаем ли он или нет.Я думаю, что ваша теорема и лемма доказуемы, если вы просто замените In' x l на inhabited (In' x l).Мне удалось доказать вариант вашей теоремы, вывод которого просто In x l <-> inhabited (In' x l).Ваше доказательство в основном сработало, но мне пришлось использовать следующую простую лемму за один шаг:

Lemma inhabited_there {A: Type} {P: A -> Type} {x: A} {xs: list A}:
  inhabited (Any P xs) -> inhabited (Any P (x :: xs)).

Примечание: хотя inhabited A - это просто Prop версия A, и мы имеем A -> inhabited A, мы не можем доказать inhabited A -> A в целом, потому что это будет включать в себя выбор произвольного элемента A. ²

---

1. Я такжепредложил Set здесь и раньше, но это не работает, так как индуктивный тип зависит от A, который находится в Type.

2. На самом деле, я считаю, что доказательствоАссистент Лин использует нечто очень похожее для своей аксиомы выбора.