From 39e2ce1c05f087abfeab84919ead6e818fbeb15c Mon Sep 17 00:00:00 2001 From: Niels van der Weide Date: Thu, 21 Sep 2017 14:12:51 +0200 Subject: [PATCH] Uses merely decidable equality, added length. --- FiniteSets/_CoqProject | 1 + FiniteSets/interfaces/lattice_interface.v | 4 + FiniteSets/interfaces/set_names.v | 1 + FiniteSets/kuratowski/extensionality.v | 4 + FiniteSets/kuratowski/kuratowski_sets.v | 4 +- FiniteSets/kuratowski/length.v | 26 ++++ FiniteSets/kuratowski/operations.v | 47 ++++++-- FiniteSets/kuratowski/properties.v | 26 ++-- FiniteSets/list_representation/isomorphism.v | 112 ++++++++++-------- .../list_representation/list_representation.v | 6 +- FiniteSets/list_representation/operations.v | 2 +- FiniteSets/list_representation/properties.v | 24 ++-- FiniteSets/misc/dec_kuratowski.v | 25 ++-- FiniteSets/prelude.v | 13 ++ FiniteSets/subobjects/enumerated.v | 4 +- 15 files changed, 193 insertions(+), 106 deletions(-) create mode 100644 FiniteSets/kuratowski/length.v diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject index e7ec07e..bbebf44 100644 --- a/FiniteSets/_CoqProject +++ b/FiniteSets/_CoqProject @@ -13,6 +13,7 @@ list_representation/properties.v list_representation/isomorphism.v kuratowski/operations.v kuratowski/properties.v +kuratowski/length.v FSets.v interfaces/set_interface.v implementations/lists.v diff --git a/FiniteSets/interfaces/lattice_interface.v b/FiniteSets/interfaces/lattice_interface.v index 965aa2d..2084d1c 100644 --- a/FiniteSets/interfaces/lattice_interface.v +++ b/FiniteSets/interfaces/lattice_interface.v @@ -1,6 +1,7 @@ (** Interface for lattices and join semilattices. *) Require Import HoTT. +(** Some preliminary notions to define lattices. *) Section binary_operation. Definition operation (A : Type) := A -> A -> A. @@ -43,6 +44,7 @@ Arguments neutralityL {_} {_} {_} {_} _. Arguments neutralityR {_} {_} {_} {_} _. Arguments absorb {_} {_} {_} {_} _ _. +(** The operations in a lattice. *) Section lattice_operations. Variable (A : Type). @@ -60,6 +62,7 @@ Arguments max_L {_} {_} _. Arguments min_L {_} {_} _. Arguments empty {_}. +(** Join semilattices as a typeclass. They only have a join operator. *) Section JoinSemiLattice. Variable A : Type. Context {max_L : maximum A} {empty_L : bottom A}. @@ -84,6 +87,7 @@ Hint Resolve idempotency : joinsemilattice_hints. Hint Resolve neutralityL : joinsemilattice_hints. Hint Resolve neutralityR : joinsemilattice_hints. +(** Lattices as a typeclass which have both a join and a meet. *) Section Lattice. Variable A : Type. Context {max_L : maximum A} {min_L : minimum A} {empty_L : bottom A}. diff --git a/FiniteSets/interfaces/set_names.v b/FiniteSets/interfaces/set_names.v index e740141..5f9c480 100644 --- a/FiniteSets/interfaces/set_names.v +++ b/FiniteSets/interfaces/set_names.v @@ -1,6 +1,7 @@ (** Classes for set operations, so they can be overloaded. *) Require Import HoTT. +(** The operations on sets for which we add names. *) Section structure. Variable (T A : Type). diff --git a/FiniteSets/kuratowski/extensionality.v b/FiniteSets/kuratowski/extensionality.v index a430676..200c0e9 100644 --- a/FiniteSets/kuratowski/extensionality.v +++ b/FiniteSets/kuratowski/extensionality.v @@ -2,6 +2,10 @@ Require Import HoTT HitTactics. Require Import kuratowski.kuratowski_sets. +(** We prove extensionality via a chain of equivalences. + We end with proving that equality can be defined with the subset relation. + From that we can conclude that [FSet A] has decidable equality if [A] has. +*) Section ext. Context {A : Type}. Context `{Univalence}. diff --git a/FiniteSets/kuratowski/kuratowski_sets.v b/FiniteSets/kuratowski/kuratowski_sets.v index 2c313e9..32aa2da 100644 --- a/FiniteSets/kuratowski/kuratowski_sets.v +++ b/FiniteSets/kuratowski/kuratowski_sets.v @@ -1,4 +1,6 @@ -(** Definitions of the Kuratowski-finite sets via a HIT *) +(** Definitions of the Kuratowski-finite sets via a HIT. + We do not need the computation rules in the development, so they are not present here. +*) Require Import HoTT HitTactics. Require Export set_names lattice_examples. diff --git a/FiniteSets/kuratowski/length.v b/FiniteSets/kuratowski/length.v new file mode 100644 index 0000000..72ab83b --- /dev/null +++ b/FiniteSets/kuratowski/length.v @@ -0,0 +1,26 @@ +Require Import HoTT HitTactics. +Require Import kuratowski.operations kuratowski.properties kuratowski.kuratowski_sets. + +Section Length. + Context {A : Type} `{DecidablePaths A} `{Univalence}. + + Definition length : FSet A -> nat. + simple refine (FSet_cons_rec _ _ _ _ _ _). + - apply 0. + - intros a X n. + apply (if a ∈_d X then n else (S n)). + - intros X a n. + simpl. + simplify_isIn_d. + destruct (dec (a ∈ X)) ; reflexivity. + - intros X a b n. + simpl. + simplify_isIn_d. + destruct (dec (a = b)) as [Hab | Hab]. + + rewrite Hab. simplify_isIn_d. reflexivity. + + rewrite ?singleton_isIn_d_false; auto. + ++ simpl. + destruct (a ∈_d X), (b ∈_d X) ; reflexivity. + ++ intro p. contradiction (Hab p^). + Defined. +End Length. \ No newline at end of file diff --git a/FiniteSets/kuratowski/operations.v b/FiniteSets/kuratowski/operations.v index 66b58f2..e65fad9 100644 --- a/FiniteSets/kuratowski/operations.v +++ b/FiniteSets/kuratowski/operations.v @@ -1,6 +1,7 @@ (** Operations on the [FSet A] for an arbitrary [A] *) -Require Import HoTT HitTactics. -Require Import kuratowski_sets monad_interface extensionality. +Require Import HoTT HitTactics prelude. +Require Import kuratowski_sets monad_interface extensionality + list_representation.isomorphism list_representation.list_representation. Section operations. (** Monad operations. *) @@ -167,7 +168,7 @@ End operations. Section operations_decidable. Context {A : Type}. - Context {A_deceq : DecidablePaths A}. + Context `{MerelyDecidablePaths A}. Context `{Univalence}. Global Instance isIn_decidable (a : A) : forall (X : FSet A), @@ -175,12 +176,7 @@ Section operations_decidable. Proof. hinduction ; try (intros ; apply path_ishprop). - apply _. - - intros b. - destruct (dec (a = b)) as [p | np]. - * apply (inl (tr p)). - * refine (inr(fun p => _)). - strip_truncations. - contradiction. + - apply (m_dec_path _). - apply _. Defined. @@ -207,4 +203,35 @@ Section operations_decidable. Global Instance fset_intersection : hasIntersection (FSet A) := fun X Y => {|X & (fun a => a ∈_d Y)|}. -End operations_decidable. \ No newline at end of file +End operations_decidable. + +Section FSet_cons_rec. + Context `{A : Type}. + + Variable (P : Type) + (Pset : IsHSet P) + (Pe : P) + (Pcons : A -> FSet A -> P -> P) + (Pdupl : forall X a p, Pcons a ({|a|} ∪ X) (Pcons a X p) = Pcons a X p) + (Pcomm : forall X a b p, Pcons a ({|b|} ∪ X) (Pcons b X p) + = Pcons b ({|a|} ∪ X) (Pcons a X p)). + + Definition FSet_cons_rec (X : FSet A) : P. + Proof. + simple refine (FSetC_ind A (fun _ => P) _ Pe _ _ _ (FSet_to_FSetC X)) ; simpl. + - intros a Y p. + apply (Pcons a (FSetC_to_FSet Y) p). + - intros. + refine (transport_const _ _ @ _). + apply Pdupl. + - intros. + refine (transport_const _ _ @ _). + apply Pcomm. + Defined. + + Definition FSet_cons_beta_empty : FSet_cons_rec ∅ = Pe := idpath. + + Definition FSet_cons_beta_cons (a : A) (X : FSet A) + : FSet_cons_rec ({|a|} ∪ X) = Pcons a X (FSet_cons_rec X) + := ap (fun z => Pcons a z _) (repr_iso_id_l _). +End FSet_cons_rec. \ No newline at end of file diff --git a/FiniteSets/kuratowski/properties.v b/FiniteSets/kuratowski/properties.v index aaba4cf..958fb29 100644 --- a/FiniteSets/kuratowski/properties.v +++ b/FiniteSets/kuratowski/properties.v @@ -1,4 +1,4 @@ -Require Import HoTT HitTactics. +Require Import HoTT HitTactics prelude. Require Import kuratowski.extensionality kuratowski.operations kuratowski_sets. Require Import lattice_interface lattice_examples monad_interface. @@ -251,7 +251,7 @@ End fset_join_semilattice. (* Lemmas relating operations to the membership predicate *) Section properties_membership_decidable. - Context {A : Type} `{DecidablePaths A} `{Univalence}. + Context {A : Type} `{MerelyDecidablePaths A} `{Univalence}. Lemma ext : forall (S T : FSet A), (forall a, a ∈_d S = a ∈_d T) -> S = T. Proof. @@ -267,17 +267,7 @@ Section properties_membership_decidable. - apply path_iff_hprop ; intro ; contradiction. Defined. - Lemma empty_isIn_d (a : A) : - a ∈_d ∅ = false. - Proof. - reflexivity. - Defined. - - Lemma singleton_isIn_d (a b : A) : - a ∈ {|b|} -> a = b. - Proof. - intros. strip_truncations. assumption. - Defined. + Definition empty_isIn_d (a : A) : a ∈_d ∅ = false := idpath. Lemma singleton_isIn_d_true (a b : A) (p : a = b) : a ∈_d {|b|} = true. @@ -329,6 +319,14 @@ Section properties_membership_decidable. Proof. apply comprehension_isIn_d. Defined. + + Lemma singleton_isIn_d `{DecidablePaths A} (a b : A) : + a ∈ {|b|} -> a = b. + Proof. + intros. + strip_truncations. + assumption. + Defined. End properties_membership_decidable. (* Some suporting tactics *) @@ -346,7 +344,7 @@ Ltac toBool := (** If `A` has decidable equality, then `FSet A` is a lattice *) Section set_lattice. Context {A : Type}. - Context {A_deceq : DecidablePaths A}. + Context `{MerelyDecidablePaths A}. Context `{Univalence}. Instance fset_max : maximum (FSet A). diff --git a/FiniteSets/list_representation/isomorphism.v b/FiniteSets/list_representation/isomorphism.v index e835ef9..2cfb63d 100644 --- a/FiniteSets/list_representation/isomorphism.v +++ b/FiniteSets/list_representation/isomorphism.v @@ -1,16 +1,16 @@ -(* The representations [FSet A] and [FSetC A] are isomorphic for every A *) +(** The representations [FSet A] and [FSetC A] are isomorphic for every A *) Require Import HoTT HitTactics. Require Import list_representation list_representation.operations list_representation.properties. Require Import kuratowski.kuratowski_sets. Section Iso. - Context {A : Type} `{Univalence}. + Context {A : Type}. Definition FSetC_to_FSet: FSetC A -> FSet A. Proof. hrecursion. - - apply E. + - apply ∅. - intros a x. apply ({|a|} ∪ x). - intros a X. @@ -23,8 +23,8 @@ Section Iso. Proof. hrecursion. - apply ∅. - - intro a. apply {|a|}. - - intros X Y. apply (X ∪ Y). + - apply (fun a => {|a|}). + - apply (∪). - apply append_assoc. - apply append_comm. - apply append_nl. @@ -35,19 +35,20 @@ Section Iso. Lemma append_union: forall (x y: FSetC A), FSetC_to_FSet (x ∪ y) = (FSetC_to_FSet x) ∪ (FSetC_to_FSet y). Proof. - intros x. - hrecursion x; try (intros; apply path_forall; intro; apply set_path2). - - intros. symmetry. apply nl. - - intros a x HR y. unfold union, fsetc_union in *. - refine (_ @ assoc _ _ _). - apply (ap ({|a|} ∪) (HR _)). + intros x y. + hrecursion x ; try (intros ; apply path_ishprop). + - intros. + apply (nl _)^. + - intros a x HR. + refine (ap ({|a|} ∪) HR @ assoc _ _ _). Defined. Lemma repr_iso_id_l: forall (x: FSet A), FSetC_to_FSet (FSet_to_FSetC x) = x. Proof. - hinduction; try (intros; apply set_path2). + hinduction ; try (intros ; apply path_ishprop). - reflexivity. - - intro. apply nr. + - intro. + apply nr. - intros x y p q. refine (append_union _ _ @ _). refine (ap (∪ _) p @ _). @@ -56,15 +57,16 @@ Section Iso. Lemma repr_iso_id_r: forall (x: FSetC A), FSet_to_FSetC (FSetC_to_FSet x) = x. Proof. - hinduction; try (intros; apply set_path2). + hinduction ; try (intros ; apply path_ishprop). - reflexivity. - - intros a x HR. rewrite HR. reflexivity. + - intros a x HR. + refine (ap ({|a|} ∪) HR). Defined. Global Instance: IsEquiv FSet_to_FSetC. Proof. apply isequiv_biinv. - unfold BiInv. split. + split. exists FSetC_to_FSet. unfold Sect. apply repr_iso_id_l. exists FSetC_to_FSet. @@ -82,12 +84,18 @@ Section Iso. simple refine (@BuildEquiv (FSet A) (FSetC A) FSet_to_FSetC _ ). Defined. - Theorem fset_fsetc : FSet A = FSetC A. + Theorem fset_fsetc `{Univalence} : FSet A = FSetC A. Proof. apply (equiv_path _ _)^-1. exact repr_iso. Defined. + Definition dupl' (a : A) (X : FSet A) : {|a|} ∪ {|a|} ∪ X = {|a|} ∪ X + := assoc _ _ _ @ ap (∪ X) (idem a). + + Definition comm' (a b : A) (X : FSet A) : {|a|} ∪ {|b|} ∪ X = {|b|} ∪ {|a|} ∪ X + := assoc _ _ _ @ ap (∪ X) (comm _ _) @ (assoc _ _ _)^. + Theorem FSet_cons_ind (P : FSet A -> Type) (Pset : forall (X : FSet A), IsHSet (P X)) (Pempt : P ∅) @@ -95,28 +103,28 @@ Section Iso. (Pdupl : forall (a : A) (X : FSet A) (px : P X), transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px) (Pcomm : forall (a b : A) (X : FSet A) (px : P X), - transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) : - forall X, P X. + transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) + (X : FSet A) + : P X. Proof. - intros X. refine (transport P (repr_iso_id_l X) _). - simple refine (FSetC_ind A (fun Z => P (FSetC_to_FSet Z)) _ _ _ _ _ (FSet_to_FSetC X)); simpl. + simple refine (FSetC_ind A (fun Z => P (FSetC_to_FSet Z)) _ _ _ _ _ (FSet_to_FSetC X)) + ; simpl. - apply Pempt. - - intros a Y HY. by apply Pcons. + - intros a Y HY. + apply (Pcons a _ HY). - intros a Y PY. refine (_ @ (Pdupl _ _ _)). - etransitivity. - { apply (transport_compose _ FSetC_to_FSet (dupl a Y)). } + refine (transport_compose _ FSetC_to_FSet (dupl a Y) _ @ _). refine (ap (fun z => transport P z _) _). apply path_ishprop. - - intros a b Y PY. cbn. - refine (_ @ (Pcomm _ _ _ _)). - etransitivity. - { apply (transport_compose _ FSetC_to_FSet (FSetC.comm a b Y)). } + - intros a b Y PY. + refine (transport_compose _ FSetC_to_FSet (comm_s a b Y) _ @ _ @ (Pcomm _ _ _ _)). refine (ap (fun z => transport P z _) _). apply path_ishprop. Defined. + (* Theorem FSet_cons_ind_beta_empty (P : FSet A -> Type) (Pset : forall (X : FSet A), IsHSet (P X)) (Pempt : P ∅) @@ -130,25 +138,31 @@ Section Iso. by compute. Defined. - (* TODO *) - (* Theorem FSet_cons_ind_beta_cons (P : FSet A -> Type) *) - (* (Pset : forall (X : FSet A), IsHSet (P X)) *) - (* (Pempt : P ∅) *) - (* (Pcons : forall (a : A) (X : FSet A), P X -> P ({|a|} ∪ X)) *) - (* (Pdupl : forall (a : A) (X : FSet A) (px : P X), *) - (* transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px) *) - (* (Pcomm : forall (a b : A) (X : FSet A) (px : P X), *) - (* transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) : *) - (* forall a X, FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm ({|a|} ∪ X) = Pcons a X (FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm X). *) - (* Proof. *) - - (* Theorem FSet_cons_ind_beta_dupl (P : FSet A -> Type) *) - (* (Pset : forall (X : FSet A), IsHSet (P X)) *) - (* (Pempt : P ∅) *) - (* (Pcons : forall (a : A) (X : FSet A), P X -> P ({|a|} ∪ X)) *) - (* (Pdupl : forall (a : A) (X : FSet A) (px : P X), *) - (* transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px) *) - (* (Pcomm : forall (a b : A) (X : FSet A) (px : P X), *) - (* transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) : *) - (* forall a X, apD (FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm) (dupl' a X) = Pdupl a X (FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm X). *) + + Theorem FSet_cons_ind_beta_cons (P : FSet A -> Type) + (Pset : forall (X : FSet A), IsHSet (P X)) + (Pempt : P ∅) + (Pcons : forall (a : A) (X : FSet A), P X -> P ({|a|} ∪ X)) + (Pdupl : forall (a : A) (X : FSet A) (px : P X), + transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px) + (Pcomm : forall (a b : A) (X : FSet A) (px : P X), + transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) : + forall a X, FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm ({|a|} ∪ X) + = Pcons a X (FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm X). + Proof. + intros. + unfold FSet_cons_ind. + simpl. + rewrite ?transport_pp. + hinduction X ; try(intros ; apply path_ishprop) ; simpl. + - admit. + - intro b. + unfold FSet_cons_ind. + simpl. + admit. + - intros. + unfold FSet_cons_ind. + simpl. + rewrite X. + *) End Iso. diff --git a/FiniteSets/list_representation/list_representation.v b/FiniteSets/list_representation/list_representation.v index f3d5f95..3dd6659 100644 --- a/FiniteSets/list_representation/list_representation.v +++ b/FiniteSets/list_representation/list_representation.v @@ -18,7 +18,7 @@ Module Export FSetC. Axiom dupl : forall (a : A) (x : FSetC A), a ;; a ;; x = a ;; x. - Axiom comm : forall (a b : A) (x : FSetC A), + Axiom comm_s : forall (a b : A) (x : FSetC A), a ;; b ;; x = b ;; a ;; x. Axiom trunc : IsHSet (FSetC A). @@ -26,7 +26,7 @@ Module Export FSetC. Arguments Cns {_} _ _. Arguments dupl {_} _ _. - Arguments comm {_} _ _ _. + Arguments comm_s {_} _ _ _. Infix ";;" := Cns (at level 8, right associativity). @@ -39,7 +39,7 @@ Module Export FSetC. (duplP : forall (a: A) (x: FSetC A) (px : P x), dupl a x # cnsP a (a;;x) (cnsP a x px) = cnsP a x px) (commP : forall (a b: A) (x: FSetC A) (px: P x), - comm a b x # cnsP a (b;;x) (cnsP b x px) = + comm_s a b x # cnsP a (b;;x) (cnsP b x px) = cnsP b (a;;x) (cnsP a x px)). (* Induction principle *) diff --git a/FiniteSets/list_representation/operations.v b/FiniteSets/list_representation/operations.v index d6b87a8..630c88a 100644 --- a/FiniteSets/list_representation/operations.v +++ b/FiniteSets/list_representation/operations.v @@ -10,7 +10,7 @@ Section operations. - apply y. - apply Cns. - apply dupl. - - apply comm. + - apply comm_s. Defined. Global Instance fsetc_singleton : forall A, hasSingleton (FSetC A) A := fun A a => a;;∅. diff --git a/FiniteSets/list_representation/properties.v b/FiniteSets/list_representation/properties.v index ab654f4..7ac7fc0 100644 --- a/FiniteSets/list_representation/properties.v +++ b/FiniteSets/list_representation/properties.v @@ -1,4 +1,5 @@ -(** Properties of the operations on [FSetC A] *) +(** Properties of the operations on [FSetC A]. These are needed to prove that the + representations are isomorphic. *) Require Import HoTT HitTactics. Require Import list_representation list_representation.operations. @@ -10,7 +11,7 @@ Section properties. Lemma append_nr : forall (x: FSetC A), x ∪ ∅ = x. Proof. - hinduction; try (intros; apply set_path2). + hinduction; try (intros; apply path_ishprop). - reflexivity. - intros. apply (ap (fun y => a;;y) X). Defined. @@ -20,8 +21,7 @@ Section properties. Proof. intros x y z. hinduction x ; try (intros ; apply path_ishprop). - - cbn. - reflexivity. + - reflexivity. - intros. cbn. f_ap. @@ -30,21 +30,21 @@ Section properties. Lemma append_singleton: forall (a: A) (x: FSetC A), a ;; x = x ∪ (a ;; ∅). Proof. - intro a. hinduction; try (intros; apply set_path2). + intro a. hinduction; try (intros; apply path_ishprop). - reflexivity. - - intros b x HR. refine (_ @ _). - + apply comm. - + apply (ap (fun y => b ;; y) HR). + - intros b x HR. + refine (comm_s _ _ _ @ ap (fun y => b ;; y) HR). Defined. - Lemma append_comm {H: Funext}: + Lemma append_comm : forall (x1 x2: FSetC A), x1 ∪ x2 = x2 ∪ x1. Proof. - hinduction ; try (intros ; apply path_forall ; intro ; apply set_path2). + intros x1 x2. + hinduction x1 ; try (intros ; apply path_ishprop). - intros. apply (append_nr _)^. - - intros a x1 HR x2. - refine (ap (fun y => a;;y) (HR x2) @ _). + - intros a x HR. + refine (ap (fun y => a;;y) HR @ _). refine (append_singleton _ _ @ _). refine ((append_assoc _ _ _)^ @ _). refine (ap (x2 ∪) (append_singleton _ _)^). diff --git a/FiniteSets/misc/dec_kuratowski.v b/FiniteSets/misc/dec_kuratowski.v index 8097fab..49b5bc4 100644 --- a/FiniteSets/misc/dec_kuratowski.v +++ b/FiniteSets/misc/dec_kuratowski.v @@ -7,9 +7,8 @@ Section membership. Definition dec_membership (H1 : forall (a : A) (X : FSet A), Decidable(a ∈ X)) - (a b : A) - : Decidable(merely(a = b)) - := H1 a {|b|}. + : MerelyDecidablePaths A + := fun a b => H1 a {|b|}. End membership. Section intersection. @@ -19,8 +18,9 @@ Section intersection. (int_member : forall (a : A) (X Y : FSet A), a ∈ (int X Y) = BuildhProp(a ∈ X * a ∈ Y)). - Theorem dec_intersection (a b : A) : Decidable(merely(a = b)). + Theorem dec_intersection : MerelyDecidablePaths A. Proof. + intros a b. destruct (merely_choice (int {|a|} {|b|})) as [p | p]. - refine (inr(fun X => _)). strip_truncations. @@ -42,24 +42,23 @@ Section subset. Definition dec_subset (H1 : forall (X Y : FSet A), Decidable(X ⊆ Y)) - (a b : A) - : Decidable(merely(a = b)) - := H1 {|a|} {|b|}. + : MerelyDecidablePaths A + := fun a b => H1 {|a|} {|b|}. End subset. Section decidable_equality. Context {A : Type} `{Univalence}. - Definition dec_decidable_equality (H1 : DecidablePaths(FSet A)) (a b : A) - : Decidable(merely(a = b)). + Definition dec_decidable_equality (H1 : DecidablePaths(FSet A)) + : MerelyDecidablePaths A. Proof. - destruct (H1 {|a|} {|b|}) as [p | p]. + intros a b. + destruct (H1 {|a|} {|b|}) as [p | n]. - pose (transport (fun z => a ∈ z) p) as t. apply (inl (t (tr idpath))). - - refine (inr (fun n => _)). + - refine (inr (fun p => _)). strip_truncations. - pose (transport (fun z => {|a|} = {|z|}) n) as t. - apply (p (t idpath)). + apply (n (transport (fun z => {|z|} = {|b|}) p^ idpath)). Defined. End decidable_equality. diff --git a/FiniteSets/prelude.v b/FiniteSets/prelude.v index 45df745..28089b9 100644 --- a/FiniteSets/prelude.v +++ b/FiniteSets/prelude.v @@ -22,4 +22,17 @@ Proof. apply (equiv_hprop_allpath _)^-1. intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction. - apply equiv_hprop_allpath. apply _. +Defined. + +Class MerelyDecidablePaths A := + m_dec_path : forall (a b : A), Decidable(Trunc (-1) (a = b)). + +Global Instance DecidableToMerely A (H : DecidablePaths A) : MerelyDecidablePaths A. +Proof. + intros x y. + destruct (dec (x = y)). + - apply (inl(tr p)). + - refine (inr(fun p => _)). + strip_truncations. + apply (n p). Defined. \ No newline at end of file diff --git a/FiniteSets/subobjects/enumerated.v b/FiniteSets/subobjects/enumerated.v index a336e0e..6cf45bd 100644 --- a/FiniteSets/subobjects/enumerated.v +++ b/FiniteSets/subobjects/enumerated.v @@ -254,15 +254,13 @@ Section fset_dec_enumerated. forall (X : FSet A), hexists (fun (ls : list A) => forall a, a ∈ X = listExt ls a). Proof. - simple refine (FSet_cons_ind _ _ _ _ _ _); simpl. + simple refine (FSet_cons_ind _ _ _ _ _ _) ; try (intros ; apply path_ishprop). - apply tr. exists nil. simpl. done. - intros a X Hls. strip_truncations. apply tr. destruct Hls as [ls Hls]. exists (cons a ls). intros b. cbn. apply (ap (fun z => _ ∨ z) (Hls b)). - - intros. apply path_ishprop. - - intros. apply path_ishprop. Defined. Definition Kf_enumerated : Kf A -> enumerated A.