如何证明集合的补集是内合集合？
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.
编辑:假设可判定(在A x中)使firstorder能够完全证明引理。
最佳答案
complement_involutive 正是 ~~ A x -> A x ，众所周知，它相当于排除的中间，在本例中为 Type，因此如果不将其假设为公理，则无法在 Coq 中证明。请参阅此答案 https://math.stackexchange.com/questions/1370805/why-cant-you-prove-the-law-of-the-excluded-middle-in-intuitionistic-logic-for
关于set - Coq 证明补体是内卷的，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/49628564/