Stream: Coq users

Topic: Decidable equality and countability on Σ types?


view this post on Zulip Ignat Insarov (Jun 19 2021 at 15:54):

I have some sigma types {ℕ | ℕ → ℙ} and I want to put them in a gset. How can I explain to Coq that numbers decorated with proofs are still countable and have decidable equality? _(I assume that this holds due to proof irrelevance.)_

Here is my code so far.

From stdpp Require Import
  base
  fin_sets
  gmap
  .

Notation  := nat.
Notation  := Prop.

Definition completeSet
  (item: Type)
  (hasHallmark: item  )
  `{ EqDecision item
   , Countable item
   } := { s: gset item
        | anItem, hasHallmark anItem  anItem = anItem }.

Example exampleOfCompleteSet: completeSet  even.
Proof.
  unfold completeSet.
  exists {[2]}.
  intros. reflexivity. Qed.

Definition completeSet₂
  (item: Type)
  (hasHallmark: item  )
  `{ EqDecision {anItem: item | hasHallmark anItem}
   , Countable {anItem: item | hasHallmark anItem}
   } := { s: gset {anItem: item | hasHallmark anItem}
        | anItem, hasHallmark anItem  anItem = anItem }.

Example anotherExampleOfCompleteSet: completeSet₂  even.
(*
    Error:
    Unable to satisfy the following constraints:

    ?EqDecision1 : "EqDecision {anItem : ℕ | (λ n : ℕ, Nat.even n) anItem}"

    ?H : "Countable {anItem : ℕ | (λ n : ℕ, Nat.even n) anItem}"
 *)

view this post on Zulip Gaëtan Gilbert (Jun 19 2021 at 16:07):

you define the appropriate Instances

view this post on Zulip Ignat Insarov (Jun 19 2021 at 16:10):

Class RelDecision {A B} (R : A  B  Prop) :=
  decide_rel x y :> Decision (R x y).

Notation EqDecision A := (RelDecision (=@{A})).

So I must define Coq.Init.Logic.eq for my Σ type? Is it even legal?

view this post on Zulip Ignat Insarov (Jun 19 2021 at 16:12):

I do not understand what decide_rel x y :> Decision (R x y) means…

view this post on Zulip Ignat Insarov (Jun 19 2021 at 16:22):

This works:

Instance countableOnEvenℕ: Countable ({n:  | even n}). Admitted.

EqDecision arises automagically.

view this post on Zulip Ignat Insarov (Jun 19 2021 at 16:22):

Can I somehow make it work for any property, not only even?

view this post on Zulip Gaëtan Gilbert (Jun 19 2021 at 16:28):

Class RelDecision {A B} (R : A  B  Prop) :=
  decide_rel x y :> Decision (R x y).

is equivalent to

Definition RelDecision {A B} (R : A  B  Prop) := forall x y, Decision (R x y).
Instance decide_rel {A B} (R : A  B  Prop) (H:RelDecision R)  : forall x y, Decision (R x y) := H.

view this post on Zulip Gaëtan Gilbert (Jun 19 2021 at 16:34):

Ignat Insarov said:

Can I somehow make it work for any property, not only even?

You could try proving it, I think you need the property to be decidable in order to get a countable sigma type though

view this post on Zulip Ignat Insarov (Jun 19 2021 at 16:39):

Maybe I can make a class for decidable properties and instantiate the properties I want to wield into that class…

view this post on Zulip Gaëtan Gilbert (Jun 19 2021 at 16:43):

https://gitlab.mpi-sws.org/iris/stdpp/-/blob/0a38be458cbfd571889b888fb27c8e4432fcaae9/theories/base.v#L315

view this post on Zulip Ignat Insarov (Jun 20 2021 at 08:29):

Wow, they really thought of everything!


Last updated: Feb 06 2023 at 12:04 UTC