Given your second property, I assume that your definition of exceptional or higher phenomena is “exactly one of these sentences is true” (and not “an odd number of these sentences is true” or “at least one of these sentences is true and at least one false ", which are other possible generalizations).
This is an exclusive or non-associative property. This means that you cannot simply define a higher degree of xor as xor (A1, ..., An) = xor (A1, xor (A2, ...)). You need a global definition, and this means that the type constructor must accept a list of arguments (or some other data structure, but the list is the most obvious choice).
Inductive xor : list Prop -> Prop := …
You now have two reasonable options: build your xor definition inductively from the first principles, or call a list predicate. The predicate of the list will be "there is a unique element in the list corresponding to this predicate." Since the standard list library does not define this predicate, and defining it is a bit more complicated than defining xor, we will construct xor inductively.
The argument is a list, so let's break down the cases:
- xor of the empty list is always false;
- list xor
(cons AL) is true if either of these two conditions is true:- A is true, and not one of the elements of L is true;
- A is false, and exactly one of the elements of L is true.
This means that we need to define an auxiliary predicate in nand sentence nand that characterize false sentence lists. There are many possibilities: collapse the /\ operator, enter manually, or call the list predicate (again, not in the standard list library). I will act manually, but folding /\ is another reasonable choice.
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.
The properties you want to prove are simple consequences of the inversion properties: for a given type, break the possibilities (if you have xor , then it is either xor_t or xor_f ). Here is a manual proof of the first; the second is very similar.
Lemma xor_tail : forall AL, xor (A::L) -> ~A -> xor L. Proof. intros. inversion_clear H. contradiction. assumption. Qed.
Another set of properties that you most likely want is the equivalence between nand and the inline connection. As an example, it is proved here that nand (A::nil) equivalent to ~A The proof that nand (A::B::nil) equivalent to ~A/\~B , etc., are simply more similar. In the forward direction, this is once again an inversion property (analyze possible constructors like nand ). In the opposite direction, this is a simple application of designers.
Lemma nand1 : forall A, nand (A::nil) <-> ~A. Proof. split; intros. inversion_clear H. assumption. constructor. assumption. constructor. Qed.
At some point, you will also need replacement and permutation properties. Here are a few key lemmas you might want to prove (it doesn't have to be very difficult, just introduce the right things):
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 KABL, xor (K++A::B::L) <-> xor (K::B::A::L)forall KLMN, xor (K++L++M++N) <-> xor (K++M++L++N)