From c7e12d6d25a09917754abee43d76f2d7b7b8d5a5 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Thu, 3 Aug 2017 15:10:01 +0200 Subject: [PATCH] Enumerated implies Kurarowski-finite --- FiniteSets/Sub.v | 23 ++++++-------- FiniteSets/variations/enumerated.v | 51 +++++++++++++++++++++++++++--- FiniteSets/variations/k_finite.v | 35 +++++++++++++++----- 3 files changed, 83 insertions(+), 26 deletions(-) diff --git a/FiniteSets/Sub.v b/FiniteSets/Sub.v index 97a3778..8c99993 100644 --- a/FiniteSets/Sub.v +++ b/FiniteSets/Sub.v @@ -57,21 +57,19 @@ Section isIn. End isIn. -Context `{Univalence}. - -Instance koe : forall (T : Type) (Ttrunc : IsHProp T), IsTrunc (-1) (T + ~T). -Proof. - intros. - apply (equiv_hprop_allpath _)^-1. - intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction. - - apply equiv_hprop_allpath. apply _. -Defined. - Section intersect. Variable A : Type. Variable C : (Sub A) -> hProp. - Context `{Univalence}. + + Instance hprop_lem : forall (T : Type) (Ttrunc : IsHProp T), IsHProp (T + ~T). + Proof. + intros. + apply (equiv_hprop_allpath _)^-1. + intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction. + - apply equiv_hprop_allpath. apply _. + Defined. + Context {HI :hasIntersection C} {HE : hasEmpty C} {HS : hasSingleton C} {HDE : hasDecidableEmpty C}. @@ -82,7 +80,6 @@ Section intersect. unfold Decidable, hasEmpty, hasIntersection, hasSingleton, hasDecidableEmpty in *. pose (HI (singleton a) (singleton b) (HS a) (HS b)) as IntAB. pose (HDE (min_fun (singleton a) (singleton b)) IntAB) as IntE. - Print Trunc_rec. refine (@Trunc_rec _ _ _ _ _ IntE) ; intros [p | p] ; unfold min_fun, singleton in p. - right. pose (apD10 p b) as pb ; unfold empty_sub in pb ; cbn in pb. @@ -113,4 +110,4 @@ Section intersect. strip_truncations. apply (inl (tr (t2^ @ t1))). Defined. -End intersect. \ No newline at end of file +End intersect. diff --git a/FiniteSets/variations/enumerated.v b/FiniteSets/variations/enumerated.v index cb351f6..01d2e6c 100644 --- a/FiniteSets/variations/enumerated.v +++ b/FiniteSets/variations/enumerated.v @@ -1,6 +1,8 @@ (* Enumerated finite sets *) -Require Import HoTT HoTT.Types.Bool. +Require Import HoTT. Require Import disjunction. +Require Import representations.cons_repr representations.definition variations.k_finite. +From fsets Require Import operations isomorphism. Definition Sub A := A -> hProp. @@ -73,9 +75,11 @@ induction ls as [| a ls]. * apply IHls. apply HIH. Defined. +(** Definition of finite sets in an enumerated sense *) Definition enumerated (A : Type) : Type := exists ls, forall (a : A), listExt ls a. +(** Properties of enumerated sets: closed under decidable subsets *) Lemma enumerated_comprehension (A : Type) (P : A -> Bool) : enumerated A -> enumerated { x : A | P x = true }. Proof. @@ -96,6 +100,7 @@ induction ls. + right. apply IHls. apply HIH. Defined. +(** Properties of enumerated sets: closed under surjections *) Lemma enumerated_surj (A B : Type) (f : A -> B) : IsSurjection f -> enumerated A -> enumerated B. Proof. @@ -129,6 +134,7 @@ induction ls'; simpl. right. apply IHls'. apply Hls. Defined. +(** Properties of enumerated sets: closed under sums *) Lemma enumerated_sum (A B : Type) : enumerated A -> enumerated B -> enumerated (A + B). Proof. @@ -190,11 +196,46 @@ induction xs as [| x' xs]; intros x y. simpl. apply tr. right. assumption. Defined. +(** Properties of enumerated sets: closed under products *) Lemma enumerated_prod (A B : Type) `{Funext} : enumerated A -> enumerated B -> enumerated (A * B). Proof. -intros [eA HeA] [eB HeB]. -exists (listProd eA eB). -intros [x y]. -apply listExt_prod; [ apply HeA | apply HeB ]. + intros [eA HeA] [eB HeB]. + exists (listProd eA eB). + intros [x y]. + apply listExt_prod; [ apply HeA | apply HeB ]. Defined. + +(** If a set is enumerated is it Kuratowski-finite *) +Section enumerated_fset. + Variable A : Type. + Context `{Univalence}. + + Fixpoint list_to_fset (ls : list A) : FSet A := + match ls with + | nil => ∅ + | cons x xs => {|x|} ∪ (list_to_fset xs) + end. + + Lemma list_to_fset_ext (ls : list A) (a : A): + listExt ls a -> isIn a (list_to_fset ls). + Proof. + induction ls as [|x xs]; simpl. + - apply idmap. + - intros Hin. + strip_truncations. apply tr. + destruct Hin as [Hax | Hin]. + + left. exact Hax. + + right. by apply IHxs. + Defined. + + Lemma enumerated_Kf : enumerated A -> Kf A. + Proof. + intros [ls Hls]. + exists (list_to_fset ls). + apply path_forall. intro a. + symmetry. apply path_hprop. + apply if_hprop_then_equiv_Unit. apply _. + by apply list_to_fset_ext. + Defined. +End enumerated_fset. diff --git a/FiniteSets/variations/k_finite.v b/FiniteSets/variations/k_finite.v index dc35129..982aba6 100644 --- a/FiniteSets/variations/k_finite.v +++ b/FiniteSets/variations/k_finite.v @@ -3,7 +3,7 @@ Require Import lattice representations.definition fsets.operations extensionalit Section k_finite. - Context {A : Type}. + Context (A : Type). Context `{Univalence}. Definition map (X : FSet A) : Sub A := fun a => isIn a X. @@ -33,8 +33,25 @@ Section k_finite. Definition Kf : hProp := Kf_sub (fun x => True). - Lemma Kf_unfold : Kf <-> (exists (X : FSet A), forall (a : A), map X a). + Instance: IsHProp {X : FSet A & forall a : A, map X a}. Proof. + apply hprop_allpath. + intros [X PX] [Y PY]. + assert (X = Y) as HXY. + { apply fset_ext. intros a. + unfold map in *. + apply path_hprop. + apply equiv_iff_hprop; intros. + + apply PY. + + apply PX. } + apply path_sigma with HXY. simpl. + apply path_forall. intro. + apply path_ishprop. + Defined. + + Lemma Kf_unfold : Kf <~> (exists (X : FSet A), forall (a : A), map X a). + Proof. + apply equiv_equiv_iff_hprop. apply _. apply _. split. - intros [X PX]. exists X. intro a. rewrite <- PX. done. @@ -46,8 +63,10 @@ Section k_finite. End k_finite. +Arguments map {_} {_} _. + Section structure_k_finite. - Context {A : Type}. + Context (A : Type). Context `{Univalence}. Lemma map_union : forall X Y : FSet A, map (U X Y) = max_fun (map X) (map Y). @@ -56,8 +75,8 @@ Section structure_k_finite. unfold map, max_fun. reflexivity. Defined. - - Lemma k_finite_union : @hasUnion A Kf_sub. + + Lemma k_finite_union : hasUnion (Kf_sub A). Proof. unfold hasUnion, Kf_sub, Kf_sub_intern. intros. @@ -69,14 +88,14 @@ Section structure_k_finite. reflexivity. Defined. - Lemma k_finite_empty : @hasEmpty A Kf_sub. + Lemma k_finite_empty : hasEmpty (Kf_sub A). Proof. unfold hasEmpty, Kf_sub, Kf_sub_intern, map, empty_sub. exists E. reflexivity. Defined. - Lemma k_finite_singleton : @hasSingleton A Kf_sub. + Lemma k_finite_singleton : hasSingleton (Kf_sub A). Proof. unfold hasSingleton, Kf_sub, Kf_sub_intern, map, singleton. intro. @@ -87,7 +106,7 @@ Section structure_k_finite. reflexivity. Defined. - Lemma k_finite_hasDecidableEmpty : @hasDecidableEmpty A Kf_sub. + Lemma k_finite_hasDecidableEmpty : hasDecidableEmpty (Kf_sub A). Proof. unfold hasDecidableEmpty, hasEmpty, Kf_sub, Kf_sub_intern, map. intros.