setcoqcomplement

Coq proof that complement is involutive

How can I prove that the complement of a set is involutive? 

  Require Import Ensembles. Arguments In {_}. Arguments Complement {_}.

  Variables (T:Type) (A:Ensemble T).
  Axiom set_eq: forall (E1 E2:Ensemble T), (forall x, E1 x <-> E2 x) -> E1 = E2.

  Lemma complement_involutive: 
      forall x, In (Complement (Complement A)) x -> In A x.

EDIT: Assuming decidable (In A x) enables firstorder to prove the lemma completely.

Solution

  • complement_involutive is exactly ~ ~ A x -> A x which is well-known to be equivalent to excluded middle, in this case in Type, thus not provable in Coq without assuming it as an axiom. See this answer https://math.stackexchange.com/questions/1370805/why-cant-you-prove-the-law-of-the-excluded-middle-in-intuitionistic-logic-for