Ignat Insarov (Jun 19 2021 at 15:54): 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}"
*)
you define the appropriate Instances
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?
Ignat Insarov (Jun 19 2021 at 16:12):I do not understand what decide_rel x y :> Decision (R x y) means…
Ignat Insarov (Jun 19 2021 at 16:22):This works:
Instance countableOnEvenℕ: Countable ({n: ℕ | even n}). Admitted.
EqDecision arises automagically.
Ignat Insarov (Jun 19 2021 at 16:22):Can I somehow make it work for any property, not only even?
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.
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
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…
Gaëtan Gilbert (Jun 19 2021 at 16:43): Ignat Insarov (Jun 20 2021 at 08:29):Wow, they really thought of everything!
Last updated: Oct 13 2024 at 01:02 UTC