Учитывая ваше второе свойство, я предполагаю, что ваше определение исключительных или более высоких арностей «точно одно из этих утверждений истинно» (а не «нечетное число этих предложений истинно» или «хотя бы одно из этих предложений»). верно, и, по крайней мере, одно является ложным »(это другие возможные обобщения).
Это эксклюзивное или не ассоциативное свойство. Это означает, что вы не можете просто определить xor более высокой арности как xor (A1,…, An) = xor (A1, xor (A2,…)). Вам нужно глобальное определение, и это означает, что конструктор типов должен принимать список аргументов (или некоторую другую структуру данных, но список является наиболее очевидным выбором).
Inductive xor : list Prop -> Prop := …
Теперь у вас есть два разумных выбора: построить ваше определение xor индуктивно из первых принципов или вызвать предикат списка. Предикат списка будет «в списке есть уникальный элемент, соответствующий этому предикату». Поскольку стандартная библиотека списков не определяет этот предикат, и определить его немного сложнее, чем определить xor, мы будем строить xor индуктивно.
Аргумент представляет собой список, поэтому давайте разберем случаи:
- xor пустого списка всегда ложно;
- xor списка
(cons A L) истинно, если выполняется любое из этих двух условий:
- A истинно, и ни один из элементов L не истинен;
- A ложно, и точно один из элементов L истинен.
Это означает, что нам нужно определить вспомогательный предикат в списках предложений, nand, характеризующий списки ложных предложений. Здесь есть много возможностей: сложить оператор /\, ввести вручную или вызвать предикат списка (опять же, не в стандартной библиотеке списков). Я буду вводить вручную, но складывание /\ - еще один разумный выбор.
Require Import List.
Inductive nand : list Prop -> Prop :=
| nand_nil : nand nil
| nand_cons : forall (A:Prop) L, ~A -> nand L -> nand (A::L).
Inductive xor : list Prop -> Prop :=
| xor_t : forall (A:Prop) L, A -> nand L -> xor (A::L)
| xor_f : forall (A:Prop) L, ~A -> xor L -> xor (A::L).
Hint Constructors nand xor.
Свойства, которые вы хотите доказать, являются простыми следствиями инверсии свойств: для заданного типа разбейте возможности (если у вас есть xor, это либо xor_t, либо * 1033). *). Вот ручное доказательство первого; вторая очень похожа.
Lemma xor_tail : forall A L, xor (A::L) -> ~A -> xor L.
Proof.
intros. inversion_clear H.
contradiction.
assumption.
Qed.
Другой набор свойств, который вам, вероятно, понадобится, - это эквивалентность между nand и встроенным соединением. Например, вот доказательство того, что nand (A::nil) эквивалентно ~A. Доказательство того, что nand (A::B::nil) эквивалентно ~A/\~B и т. Д., Является всего лишь одним и тем же. В прямом направлении это снова свойство инверсии (проанализируйте возможные конструкторы типа nand). В обратном направлении это простое применение конструкторов.
Lemma nand1 : forall A, nand (A::nil) <-> ~A.
Proof.
split; intros.
inversion_clear H. assumption.
constructor. assumption. constructor.
Qed.
Вам также могут понадобиться свойства подстановки и перестановки в какой-то момент. Вот несколько ключевых лемм, которые вы, возможно, захотите доказать (они не должны быть очень сложными, просто наведите правильные вещи):
forall A1 B2 L, (A1<->A2) -> (xor (A1::L) <-> xor (A2::L))forall K L1 L2, (xor L1 <-> xor L2) -> (xor (K++L1) <-> xor (K++L2))forall K A B L, xor (K++A::B::L) <-> xor (K::B::A::L)forall K L M N, xor (K++L++M++N) <-> xor (K++M++L++N)