如何在Coq中证明集合的补运算具有对合性？

To prove that the complement operation is involutive (meaning the double complement of a set equals the original set), we can build on your existing code and leverage the given decidability assumption for set membership alongside Coq's firstorder tactic. Here's a complete, step-by-step solution:

First, let's recap your initial setup:

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.

Step 1: Add the Decidability Hypothesis #

Since we're told In A x is decidable, we formalize this as a hypothesis:

Hypothesis In_A_dec : forall x, {In A x} + {~In A x}.

This tells Coq that for any element x, we can definitively determine whether it's in set A or not—critical for resolving double negation in intuitionistic logic.

Step 2: Prove Both Directions of Membership Equivalence #

The involutive property requires showing In (Complement (Complement A)) x and In A x are equivalent for all x. Let's prove each direction separately:

Forward Direction (Your Original Lemma)

Lemma complement_involutive_forward: forall x, In (Complement (Complement A)) x -> In A x.
Proof.
  intros x H.
  unfold Complement in H.  (* Translates double complement to ~~In A x *)
  firstorder using In_A_dec.  (* Automatically resolves double negation with decidability *)
Qed.

Reverse Direction

Lemma complement_involutive_reverse: forall x, In A x -> In (Complement (Complement A)) x.
Proof.
  intros x H.
  unfold Complement.  (* Translates goal to ~~In A x *)
  firstorder using In_A_dec.  (* Uses decidability to confirm the double negation holds *)
Qed.

Step 3: Conclude the Set Equality #

Using your set_eq axiom, we can combine the two lemmas to prove the double complement equals the original set:

Theorem complement_involutive: Complement (Complement A) = A.
Proof.
  apply set_eq.  (* Applies your equality axiom for sets *)
  intros x.
  split.  (* Breaks the equivalence into two implications *)
  - apply complement_involutive_forward.
  - apply complement_involutive_reverse.
Qed.

Quick Note on Your Original Lemma #

If you only need to complete the specific lemma you started with, here's the condensed proof using the decidability assumption:

Lemma complement_involutive: forall x, In (Complement (Complement A)) x -> In A x.
Proof.
  intros x H.
  unfold Complement in H.
  firstorder using In_A_dec.
Qed.

内容的提问来源于stack exchange，提问作者larsr