The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

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