I have a problem. I have a nice inductive set A, and I have been carving out subsets by defining Ensembles using inductive types. Now I want to eliminate from this subset to another type, but this is impossible since Ensemble is based on Prop. What should I do instead?

don't use ensembles

Is there an extensive library of ensembles that use type?

The reason I am asking is that I have a lot of stuff like, Included, Union etc. lying around. Will I have to write these from scratch using `A -> Type`

instead?

I could be wrong, but I think what Gaëtan means is to not use the predicate/function approach to sets in Coq at all

How can I talk about infinite subsets then?

I mean my original example doesn't show this, but pretend A a type with infinitely many terms

I want to talk about arbitrary subsets of A, the only way I know how to do this is with a predicate (or type family)

For example, Stdpp has a form of sets that should allow infinite subsets (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/sets.v) but we may want to ping @Paolo Giarrusso to confirm

Ali Caglayan said:

The reason I am asking is that I have a lot of stuff like, Included, Union etc. lying around. Will I have to write these from scratch using

`A -> Type`

instead?

possibly yes

@Karl Palmskog yes, the 3 implementations that has are propset (basically ensembles), coPset and coGset

so essentially, by switching to Stdpp sets one switches to just reasoning at the "interface level" instead, right?

I don’t think the interface has enough introduction forms?

you can certainly do _some_ reasoning at the abstract level, but I don't think you can convert an arbitrary predicate with infinite support into a generic `TopSet`

or a `coPset`

— they're not representable.

for instance, `coPset`

has strong restrictions (https://gitlab.mpi-sws.org/iris/stdpp/blob/3c1f58a9a08353c7f78d04bc547819abffe4b438/theories/coPset.v).

@Ali Caglayan OTOH, is your "inductive" a representation of infinite sets? Making that an instance of one of stdpp's abstractions could work?

I don't know what you mean by a representation, but basically I need something like this:

```
From Coq Require Import Ensembles.
Inductive IsEven : Ensemble nat :=
| iseven_zero : IsEven 0
| iseven_SS n : IsEven n -> IsEven (S (S n))
.
Definition div_by_2 n (H : IsEven n) : nat.
Proof.
Fail destruct H.
Abort.
```

The datatype I have in mind is a lot more complicated than this but it demonstrates the point that I can't really eliminate from ensembles.

Would stdpp's representation of sets allow handling of something like this?

Gaëtan's suggestion works fine like this:

```
Inductive IsEven : nat -> Set :=
| iseven_zero : IsEven 0
| iseven_SS n : IsEven n -> IsEven (S (S n))
.
Definition div_by_2 n (H : IsEven n) : nat.
Proof.
destruct H.
1: exact 0.
exact n.
Defined.
```

But now I have a lot stuff using definitions/typeclasses about Ensembles that I have to set up again.

Honestly, `s/Prop/Type/`

across your code _and_ ensembles might be the quickest way to get things done, if you really want to go this way...

The datatype I have in mind is a lot more complicated than this but it demonstrates the point that I can't really eliminate from ensembles.

This example _can_ be written ensembles, tho, and I don't know if it's an accident.

here, of course, you can `destruct n`

(and ignore `H`

), and in general you can destruct Props when proving other `Prop`

s. I assume your point is that even this isn't enough...

and in general, splitting things into `Prop`

and `Type`

correctly can be tricky for everybody.

(whether there's an alternative like https://coq.zulipchat.com/#narrow/stream/237659-Equations-devs.20.26.20users/topic/Derive.20NoConfusion.20failing/near/262871609, dunno!)

alternatively, what about using the pointwise lifting of `inhabited`

to inject `A -> Set`

into `A -> Prop`

? (EDIT: fixed name)

```
Definition to_ensemble {A} (x : A -> Set) : A -> Prop :=
fun a => inhabited (x a).
```

then you can keep using `A -> Set`

where needed, and lift them into ensembles via `to_ensemble`

.

Ali Caglayan said:

I don't know what you mean by a representation, but basically I need something like this:

In this case you can actually can destruct IsEven, but you need to show the lemma by hand:

```
Lemma IsEven_rect : forall (P : nat -> Type),
P 0 -> (forall n : nat, IsEven n -> P n -> P (S (S n))) ->
forall n : nat, IsEven n -> P n.
Proof.
intros P v0 vSS.
assert (forall n, (IsEven n -> P n) * (IsEven (S n) -> P (S n))).
2:firstorder.
intros n;induction n as [|n IHn];split;intros H.
- exact v0.
- exfalso; inversion H.
- apply IHn;assumption.
- assert (IsEven n) by (inversion H;auto).
apply vSS,IHn;assumption.
Defined.
Definition div_by_2 n (H : IsEven n) : nat.
Proof.
induction H using IsEven_rect.
```

Ali Caglayan has marked this topic as resolved.

Last updated: Jun 18 2024 at 21:01 UTC