Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proving the pairing axiom

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving the pairing axiom


Chronological Thread 
  • 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==

Many thanks mukesh. I will investigate it more thoroughly.


From: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
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

Hi Richard,

Below is the code. I have slightly modified your code because I was not able to run it locally. To prove pairN, I have used two axioms *prop_degeneracy* (classical logic) and *functional_extentionality*. My intuition is that it cannot be proven in Coq because of this goal (but I am not a type theorist so I could be wrong).  

 object : Type
 eq_dec : ∀ x y : object, {x = y} + {x ≠ y}
 x : object
 f : object → Prop
 y : object
 Hb : x ≠ y
 Ha : (False = True) = (f y = True)
 ============================
  False = f y


From Coq Require Import Utf8.
Require Import Coq.Logic.FunctionalExtensionality.

Section Richard.
  Variable (object : Type).
  Variable (eq_dec : forall (x y : object), {x = y} + {x <> y}).

  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 L (a : object) : N :=
    Caract
      (fun a' : object =>
         match eq_dec a a' with
         | left _ => True
         | right _ => False
         end).

  Axiom prop_degeneracy : forall (P : Prop),
      P = True \/ P = False.


  Lemma false_true_equality : (False = True) = (True = True) -> False.
  Proof.
    intros Ha.
    assert (Hb : True = True) by reflexivity.
    rewrite <- Ha in Hb.
    rewrite Hb.
    exact I.
  Qed.
  

  Lemma pairN : forall (x : object) (A : N),  L x = A <-> set_eq (L x) A.
  Proof.
    intros x A.
    split.
    -
      intro Ha; subst.
      unfold set_eq; intro a.
      apply eq_refl.
    -
      intro Ha.
      unfold set_eq, In in Ha.
      destruct A as [f]. cbn in Ha.
      unfold L.
      f_equal.
      eapply functional_extensionality; intro y.
      specialize (Ha y).
      destruct (eq_dec x y) as [Hb | Hb].
      +
        eapply eq_sym.
        rewrite <-Ha.
        exact eq_refl.
      +
        (* I am committing a sin :-) *)
        destruct (prop_degeneracy (f y)) as [Hc | Hc].
        ++
          rewrite Hc in Ha.
          eapply false_true_equality in Ha.
          inversion Ha.
        ++
          rewrite Hc.
          exact eq_refl.
  Qed.

End Richard.



Best, 
Mukesh 

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





Archive powered by MHonArc 2.6.19+.

Top of Page