The Coq mailing list

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

If *Prop* is replaced with *bool*, pairN can be proved (constructively) in Coq, assuming functional extentionality.

"It seems to me the main issue is the mixing of = (as in `caract s a = True`, `In s1 a = In s2 a`) and Props; normally I would use <-> with Props. Carrying this through, I suppose the best way to make `set_eq A B` a rewritable equality would be by declaring it with the generalized mechanism (https://coq.inria.fr/doc/V8.20.0/refman/addendum/generalized-rewriting.html#)?” 

If I have to formalise something like this I will also use bi-implication for equality. However, it is also painful to make a lot of operations an instance of type classes for rewriting, e.g., see chapter 3 of [2]. I wonder if it is the reason for introducing the *prop_ext* axiom [1]?  The explanation does say, "Propositional extensional is convenient for performing rewriting. It is needed for using Hilbert's epsilon operator in practice and, in particular, to build quotient structures in the general case.” but it would be great if someone who has used *prop_ext* in their formlisation could shed more insights. 

 

Axiom prop_ext : forall (P Q : Prop),
  (P <-> Q) -> P = Q.

Regarding the phrase "I am committing a sin :-)" it was intended as a lighthearted remark for myself because it was the first time I had used a classical axiom to prove a theorem. Unfortunately, I forgot to remove it before posting.

Best, 

Mukesh 

[1] https://github.com/coq/coq/wiki/CoqAndAxioms

[2] https://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf

From Coq Require Import Utf8.

Require Import Coq.Logic.FunctionalExtensionality.

Section Tmp.

  Variable (object : Type).

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

  Inductive N : Type :=

  | Caract : (object -> bool) -> N.

  Definition caract (s : N) (a : object) : bool :=

    let (f) := s in f a.

  Definition In (s : N) (a : object) : bool :=

    caract s a.

  Definition incl (s1 s2 : N) :=

    forall a : object, In s1 a = true -> In s2 a = true.

  Definition set_eq (s1 s2 : N) :=

    forall a : object, In s1 a = true <-> In s2 a = true.

  Definition L (a : object) : N :=

    Caract

      (fun a' : object =>

         match eq_dec a a' with

         | left _ => true

         | right _ => false

         end).

  Lemma pairN : forall (x : object) (A : N),  L x = A <-> set_eq (L x) A.

  Proof using Type.

    intros x A.

    split.

    -

      intro Ha.

      unfold set_eq.

      intro y; split.

      +

        intro Hb.

        rewrite <-Ha.

        exact Hb.

      +

        intro Hb.

        rewrite Ha.

        exact Hb.

    -

      intro Ha.

      unfold set_eq, In in Ha.

      destruct A; cbn in Ha.

      unfold L.

      f_equal.

      eapply functional_extensionality; intro y.

      destruct (eq_dec x y) as [Hb | Hb].

      +

        subst.

        eapply eq_sym.

        eapply Ha.

        destruct (eq_dec y y) eqn:Hc;

          [reflexivity | congruence].

      +

        destruct (b y) eqn:Hc.

        ++

          (* contradiction *)

          specialize (Ha y).

          destruct Ha as (Hal & Har).

          specialize (Har Hc).

          destruct (eq_dec x y); subst;

            try congruence.

        ++

          exact eq_refl.

  Qed.

End Tmp.

On 29 Dec 2024, at 19:47, D. Ben Knoble <ben.knoble AT gmail.com> wrote:

It seems to me the main issue is the mixing of = (as in `caract s a =
True`, `In s1 a = In s2 a`) and Props; normally I would use <-> with
Props.

Carrying this through, I suppose the best way to make `set_eq A B` a
rewritable equality would be by declaring it with the generalized
mechanism (https://coq.inria.fr/doc/V8.20.0/refman/addendum/generalized-rewriting.html#)?

But I'm probably missing some context that makes the original "shape"
more interesting.

RE: "cardinal sin," see
https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html#lab223
for a short statement that "However, the following theorem implies
that it is always safe to assume a decidability axiom (i.e., an
instance of excluded middle) for any particular Prop P" (where the
"following theorem" is
https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html#excluded_middle_irrefutable).

As a last thought, a different alternative might be to use bools
rather than Props if you want to write `= true`. There might be
something about "proof irrelevance" here, too.

On Sat, Dec 28, 2024 at 10:29 AM 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

--
D. Ben Knoble