From 9cdfc671dcdd24bf283ce141f01251dd6853791d Mon Sep 17 00:00:00 2001 From: Niels Date: Thu, 3 Aug 2017 15:07:53 +0200 Subject: [PATCH] Added structure to k_finite sts --- FiniteSets/Sub.v | 99 +++++++++++++++++++++++++++++++- FiniteSets/fsets/properties.v | 30 ++++++++++ FiniteSets/variations/k_finite.v | 64 ++++++++++++++++++--- 3 files changed, 182 insertions(+), 11 deletions(-) diff --git a/FiniteSets/Sub.v b/FiniteSets/Sub.v index faecf02..97a3778 100644 --- a/FiniteSets/Sub.v +++ b/FiniteSets/Sub.v @@ -5,10 +5,17 @@ Section subobjects. Variable A : Type. Definition Sub := A -> hProp. + + Definition empty_sub : Sub := fun _ => False_hp. + + Definition singleton (a : A) : Sub := fun b => BuildhProp (Trunc (-1) (b = a)). End subobjects. -Section blah. - Variable A : Type. +Arguments empty_sub {_}. +Arguments singleton {_} _. + +Section sub_classes. + Context {A : Type}. Variable C : (A -> hProp) -> hProp. Context `{Univalence}. @@ -20,4 +27,90 @@ Section blah. Definition hasUnion := forall X Y, C X -> C Y -> C (max_fun X Y). Definition hasIntersection := forall X Y, C X -> C Y -> C (min_fun X Y). -End blah. + Definition hasEmpty := C empty_sub. + Definition hasSingleton := forall a, C (singleton a). + Definition hasDecidableEmpty := forall X, C X -> hor (X = empty_sub) (hexists (fun a => X a)). +End sub_classes. + +Section isIn. + Variable A : Type. + Variable C : (A -> hProp) -> hProp. + + Context `{Univalence}. + Context {HS : hasSingleton C} {HIn : forall X, C X -> forall a, Decidable (X a)}. + + Theorem decidable_A_isIn : forall a b : A, Decidable (Trunc (-1) (b = a)). + Proof. + intros. + unfold Decidable, hasSingleton in *. + pose (HIn (singleton a) (HS a) b). + destruct s. + - unfold singleton in t. + left. + apply t. + - right. + intro p. + unfold singleton in n. + strip_truncations. + contradiction (n (tr p)). + Defined. + +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}. + Context + {HI :hasIntersection C} {HE : hasEmpty C} + {HS : hasSingleton C} {HDE : hasDecidableEmpty C}. + + Theorem decidable_A_intersect : forall a b : A, Decidable (Trunc (-1) (b = a)). + Proof. + intros. + 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. + assert (BuildhProp (Trunc (-1) (b = b)) = Unit_hp). + { + apply path_iff_hprop. + - apply (fun _ => tt). + - apply (fun _ => tr idpath). + } + rewrite X in pb. + unfold Unit_hp in pb. + assert (forall P : hProp, land P Unit_hp = P). + { + intro P. + apply path_iff_hprop. + - intros [x _] ; assumption. + - apply (fun x => (x, tt)). + } + rewrite (X0 (BuildhProp (Trunc (-1) (b = a)))) in pb. + intro q. + assert (BuildhProp (Trunc (-1) (b = a))). + { + apply q. + } + apply (pb # X1). + - strip_truncations. + destruct p as [a0 [t1 t2]]. + strip_truncations. + apply (inl (tr (t2^ @ t1))). + Defined. +End intersect. \ No newline at end of file diff --git a/FiniteSets/fsets/properties.v b/FiniteSets/fsets/properties.v index c3c1c6c..59fd57d 100644 --- a/FiniteSets/fsets/properties.v +++ b/FiniteSets/fsets/properties.v @@ -150,5 +150,35 @@ Section properties. rewrite Q. reflexivity. Defined. + + Lemma merely_choice : forall X : FSet A, hor (X = E) (hexists (fun a => isIn a X)). + Proof. + hinduction; try (intros; apply equiv_hprop_allpath ; apply _). + - apply (tr (inl idpath)). + - intro a. + refine (tr (inr (tr (a ; tr idpath)))). + - intros X Y TX TY. + strip_truncations. + destruct TX as [XE | HX] ; destruct TY as [YE | HY] ; try(strip_truncations ; apply tr). + * apply tr ; left. + rewrite XE, YE. + apply (union_idem E). + * right. + destruct HY as [a Ya]. + apply tr. + exists a. + apply (tr (inr Ya)). + * right. + destruct HX as [a Xa]. + apply tr. + exists a. + apply (tr (inl Xa)). + * right. + destruct HX as [a Xa]. + destruct HY as [b Yb]. + apply tr. + exists a. + apply (tr (inl Xa)). + Defined. End properties. diff --git a/FiniteSets/variations/k_finite.v b/FiniteSets/variations/k_finite.v index 7ff00c5..dc35129 100644 --- a/FiniteSets/variations/k_finite.v +++ b/FiniteSets/variations/k_finite.v @@ -1,18 +1,11 @@ Require Import HoTT HitTactics. -Require Import lattice representations.definition fsets.operations extensionality. - -Definition Sub A := A -> hProp. +Require Import lattice representations.definition fsets.operations extensionality Sub fsets.properties. Section k_finite. Context {A : Type}. Context `{Univalence}. - Instance subA_set : IsHSet (Sub A). - Proof. - apply _. - Defined. - Definition map (X : FSet A) : Sub A := fun a => isIn a X. Instance map_injective : IsEmbedding map. @@ -52,3 +45,58 @@ Section k_finite. Defined. End k_finite. + +Section structure_k_finite. + Context {A : Type}. + Context `{Univalence}. + + Lemma map_union : forall X Y : FSet A, map (U X Y) = max_fun (map X) (map Y). + Proof. + intros. + unfold map, max_fun. + reflexivity. + Defined. + + Lemma k_finite_union : @hasUnion A Kf_sub. + Proof. + unfold hasUnion, Kf_sub, Kf_sub_intern. + intros. + destruct X0 as [SX XP]. + destruct X1 as [SY YP]. + exists (U SX SY). + rewrite map_union. + rewrite XP, YP. + reflexivity. + Defined. + + Lemma k_finite_empty : @hasEmpty A Kf_sub. + Proof. + unfold hasEmpty, Kf_sub, Kf_sub_intern, map, empty_sub. + exists E. + reflexivity. + Defined. + + Lemma k_finite_singleton : @hasSingleton A Kf_sub. + Proof. + unfold hasSingleton, Kf_sub, Kf_sub_intern, map, singleton. + intro. + exists (L a). + cbn. + apply path_forall. + intro z. + reflexivity. + Defined. + + Lemma k_finite_hasDecidableEmpty : @hasDecidableEmpty A Kf_sub. + Proof. + unfold hasDecidableEmpty, hasEmpty, Kf_sub, Kf_sub_intern, map. + intros. + destruct X0 as [SX EX]. + rewrite EX. + simple refine (Trunc_ind _ _ (merely_choice SX)). + intros [SXE | H1]. + - rewrite SXE. + apply (tr (inl idpath)). + - apply (tr (inr H1)). + Defined. +End structure_k_finite.