The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-smb.fr>]

Hi,

It can be proved semi-automatically with CoqHammer (only the prop_degeneracy definition is involved) :

Lemma pairN : forall (x:object)(A:N), set_eq (ι x) A <-> ι x = A.
Proof.
intros;split.
- intro Ha;unfold set_eq, In in Ha;destruct A as [f];cbn in Ha;unfold ι;f_equal;eapply functional_extensionality;intro y;specialize (Ha y); destruct (eqobject_dec x y) as [Hb | Hb].
-- assert (True = True);[ sfirstorder | rewrite Ha in H;sfirstorder ].
-- assert ((False = True) -> False);[ sauto lq: on | rewrite Ha in H;sfirstorder use: PropExtensionalityFacts.PropExt_imp_RefutPropExt,
  in_singleton, propositional_extensionality unfold: In, ι, prop_degeneracy ].
- intro Ha;subst;sfirstorder.
Qed.

---

From: "Jason Hu" <fdhzs2010 AT hotmail.com>
To: "coq-club" <coq-club AT inria.fr>
Sent: Sunday, December 29, 2024 11:17:13 PM
Subject: Re: [Coq-Club] Proving the pairing axiom

That some Prop equals to True is a bit bizarre. I would imagine directing using the Prop itself would simplify some proofs. Also, using equality between Prop's sounds a bit inconvenient, if propositional extensionality is not assumed. I think the targeted formalization is just too set theoretic. 

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
Sent: Saturday, December 28, 2024 11:17 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
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