Stream: Coq users

Topic: ✔ Ensembles that live in type


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Nov 27 2021 at 13:53):

don't use ensembles

view this post on Zulip Ali Caglayan (Nov 27 2021 at 13:56):

Is there an extensive library of ensembles that use type?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Nov 27 2021 at 14:08):

How can I talk about infinite subsets then?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 14:14):

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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 14:16):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Nov 27 2021 at 14:27):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 14:41):

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

view this post on Zulip 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!)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Nov 28 2021 at 02:00):

Ali Caglayan has marked this topic as resolved.


Last updated: Jan 31 2023 at 13:02 UTC