coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Richard Dapoigny <richard.dapoigny AT univ-smb.fr>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Proving the pairing axiom
- Date: Sun, 29 Dec 2024 18:43:36 +0100 (CET)
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout02-ext4.partage.renater.fr
- Dkim-filter: OpenDKIM Filter v2.10.3 zmtaout04.partage.renater.fr 705C6140247
- Ironport-sdr: 67718a4a_qUQOlKvDnF6ULc4HXTnnYEQjNHvIfTypEli2QImhoxCf6YR GXTzeCHz+5z1qfXXN4Ou8TDqTmdqRW9NZJH+5Xw==
To: "coq-club" <coq-club AT inria.fr>
Sent: Saturday, December 28, 2024 8:17:57 PM
Subject: Re: [Coq-Club] Proving the pairing axiom
On 28 Dec 2024, at 14:41, richard <richard.dapoigny AT univ-smb.fr> wrote:Dear Coq user,
I am working on sets with characteristic functions and a datatype called object for wich equality is decidable.
Singletons called ι are also defined in this context. An excerpt of the code is given below.
Definition object: Type := t.
Definition eqobject_dec := eq_dec.
Inductive N : Type :=
| Caract : (object -> Prop) -> N.
Definition caract (s :N)(a:object) : Prop := let (f) := s in f a.
Definition In (s :N)(a:object) : Prop := caract s a = True.
Definition incl (s1 s2 :N) := forall a:object, In s1 a -> In s2 a.
Definition set_eq (s1 s2 :N) := forall a:object, In s1 a = In s2 a.Definition ι (a:object) :=
Caract
(fun a':object =>
match eqobject_dec a a' with
| left h => True
| right h => False
end).My question is the following : is there a possibility to prove the pairing axiom with these assumptions, i.e. to prove that
Lemma pairN : forall (x:object)(A:N), set_eq (ι x) A <-> ι x = A.
In addition we assume classical logic.
Thanks in advance,
Richard
- [Coq-Club] Proving the pairing axiom, richard, 12/28/2024
- Re: [Coq-Club] Proving the pairing axiom, mukesh tiwari, 12/28/2024
- Re: [Coq-Club] Proving the pairing axiom, Richard Dapoigny, 12/29/2024
- Re: [Coq-Club] Proving the pairing axiom, Jason Hu, 12/29/2024
- Re: [Coq-Club] Proving the pairing axiom, Richard Dapoigny, 12/29/2024
- Re: [Coq-Club] Proving the pairing axiom, mukesh tiwari, 12/28/2024
Archive powered by MHonArc 2.6.19+.