The Coq mailing list

["D. Ben Knoble" <ben.knoble AT gmail.com>]

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