Stream: Coq users

Topic: ✔ Ensembles that live in type

Ali Caglayan (Nov 27 2021 at 13:51):

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?

Gaëtan Gilbert (Nov 27 2021 at 13:53):

don't use ensembles

Ali Caglayan (Nov 27 2021 at 13:56):

Is there an extensive library of ensembles that use type?

Ali Caglayan (Nov 27 2021 at 14:05):

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?

Karl Palmskog (Nov 27 2021 at 14:07):

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

Ali Caglayan (Nov 27 2021 at 14:08):

How can I talk about infinite subsets then?

Ali Caglayan (Nov 27 2021 at 14:09):

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

Ali Caglayan (Nov 27 2021 at 14:09):

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)

Karl Palmskog (Nov 27 2021 at 14:09):

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

Gaëtan Gilbert (Nov 27 2021 at 14:12):

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

Paolo Giarrusso (Nov 27 2021 at 14:14):

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

Karl Palmskog (Nov 27 2021 at 14:15):

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

Paolo Giarrusso (Nov 27 2021 at 14:16):

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

Paolo Giarrusso (Nov 27 2021 at 14:19):

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.

Paolo Giarrusso (Nov 27 2021 at 14:21):

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

Paolo Giarrusso (Nov 27 2021 at 14:22):

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

Ali Caglayan (Nov 27 2021 at 14:26):

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.

Ali Caglayan (Nov 27 2021 at 14:27):

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.

Ali Caglayan (Nov 27 2021 at 14:27):

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

Ali Caglayan (Nov 27 2021 at 14:30):

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.

Paolo Giarrusso (Nov 27 2021 at 14:37):

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...

Paolo Giarrusso (Nov 27 2021 at 14:37):

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.

Paolo Giarrusso (Nov 27 2021 at 14:40):

here, of course, you can destruct n (and ignore H), and in general you can destruct Props when proving other Props. I assume your point is that even this isn't enough...

Paolo Giarrusso (Nov 27 2021 at 14:41):

and in general, splitting things into Prop and Type correctly can be tricky for everybody.

Paolo Giarrusso (Nov 27 2021 at 14:43):

(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!)

Paolo Giarrusso (Nov 27 2021 at 14:47):

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).

Paolo Giarrusso (Nov 27 2021 at 14:48):

then you can keep using A -> Set where needed, and lift them into ensembles via to_ensemble.

Gaëtan Gilbert (Nov 27 2021 at 14:57):

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.

Notification Bot (Nov 28 2021 at 02:00):

Ali Caglayan has marked this topic as resolved.

Last updated: Apr 16 2024 at 21:01 UTC