Характеристическая функция союза

Question

В конструктивной обстановке, такой как Coq, я ожидаю, что доказательство дизъюнкции A \/ B будет либо доказательством A, либо доказательством B. Если я переформулирую это для подмножеств типа X, это говорит о том, что если у меня есть доказательство того, что x находится в A union B, то у меня либо доказательство того, что x находится в A, либо доказательство что x находится в B. Поэтому я хочу определить характеристическую функцию объединения путем анализа кейсов,

Definition characteristicUnion (X : Type) (A B : X -> Prop)
           (x : X) (un : A x \/ B x) : nat.

Будет равно 1, если x в A, и 0, если x в B. Однако Coq не позволяет мне destruct un, потому что «Анализ случая на множестве сортировки не допускается для индуктивного определения или».

Есть ли другой способ в Coq моделировать подмножества типа X, который позволил бы мне построить эти характеристические функции на объединениях? Мне не нужно извлекать программы, поэтому я полагаю, что простое отключение предыдущей ошибки при анализе случаев подойдет мне.

Имейте в виду, что я не хочу моделировать подмножества как A : X -> bool. Это было бы неоправданно сильнее: мне не нужны законы исключенного среднего, такие как «либо x в A, либо x не в A».

Answer 1

Я думаю, что объединение подмножеств также должно быть подмножеством.Мы можем сделать это, определив объединение как точечная дизъюнкция:

Definition subset (X : Type) : Type := X -> Prop.
Definition union {X : Type}(A B : subset X) : subset X := fun x => A x \/ B x.

Answer 2

Как отмечает @ András Kovács, Coq не позволяет вам «извлекать» информацию, относящуюся к вычислениям, из типов в Prop, чтобы можно было использовать некоторые более продвинутые функции. По этой теме было проведено много исследований, в том числе в последнее время Univalent Foundations / HoTT, но это выходит за рамки этого вопроса.

В вашем случае вы действительно хотите использовать тип { A } + { B }, который позволит вам делать то, что вы хотите.