From 16e0e6f63dd753ad2ac3470bf5f435ce691070da Mon Sep 17 00:00:00 2001 From: Niels van der Weide Date: Wed, 4 Oct 2017 23:00:14 +0200 Subject: [PATCH] Shortenings in b_finite --- FiniteSets/subobjects/b_finite.v | 273 ++++++++++++++----------------- 1 file changed, 125 insertions(+), 148 deletions(-) diff --git a/FiniteSets/subobjects/b_finite.v b/FiniteSets/subobjects/b_finite.v index 4ab9573..12b0f3a 100644 --- a/FiniteSets/subobjects/b_finite.v +++ b/FiniteSets/subobjects/b_finite.v @@ -15,7 +15,7 @@ Section finite_hott. exists (a; tr idpath). intros [b p]. simple refine (Trunc_ind (fun p => (a; tr 1%path) = (b; p)) _ p). - clear p; intro p. simpl. + clear p; intro p ; simpl. apply path_sigma_hprop; simpl. apply p^. Defined. @@ -32,7 +32,7 @@ Section finite_hott. Proof. intros a. simple refine (Build_Finite _ 1 _). - apply tr. + apply tr. symmetry. refine (BuildEquiv _ _ (singleton_fin_equiv' a) _). Defined. @@ -47,8 +47,7 @@ Section finite_hott. Definition decidable_empty_finite : hasDecidableEmpty Bfin. Proof. - intros X Y. - destruct Y as [n f]. + intros X [n f]. strip_truncations. destruct n. - refine (tr(inl _)). @@ -62,83 +61,66 @@ Section finite_hott. Defined. Lemma no_union `{IsHSet A} - (f : forall (X Y : Sub A), + (U : forall (X Y : Sub A), Bfin X -> Bfin Y -> Bfin (X ∪ Y)) : DecidablePaths A. Proof. intros a b. - specialize (f {|a|} {|b|} (singleton a) (singleton b)). - unfold Bfin in f. - destruct f as [n pn]. + destruct (U {|a|} {|b|} (singleton a) (singleton b)) as [n pn]. strip_truncations. - destruct pn as [f [g fg gf _]]. - destruct n as [|n]. unfold Sect in *. + destruct pn as [f [g fg gf _]], n as [ | [ | n]]. - contradiction f. - exists a. apply (tr(inl(tr idpath))). - - destruct n as [|n]. - + (* If the size of the union is 1, then (a = b) *) - refine (inl _). - pose (s1 := (a;tr(inl(tr idpath))) - : {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}). - pose (s2 := (b;tr(inr(tr idpath))) - : {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}). - refine (ap (fun x => x.1) (gf s1)^ @ _ @ (ap (fun x => x.1) (gf s2))). - assert (fs_eq : f s1 = f s2). - { by apply path_ishprop. } - refine (ap (fun x => (g x).1) fs_eq). - + (* Otherwise, ¬(a = b) *) - refine (inr (fun p => _)). - pose (s1 := inl (inr tt) : Fin n + Unit + Unit). - pose (s2 := inr tt : Fin n + Unit + Unit). - pose (gs1 := g s1). - pose (c := g s1). - pose (gs2 := g s2). - pose (d := g s2). - assert (Hgs1 : gs1 = c) by reflexivity. - assert (Hgs2 : gs2 = d) by reflexivity. - destruct c as [x px']. - destruct d as [y py']. - simple refine (Trunc_ind _ _ px') ; intros px - ; simple refine (Trunc_ind _ _ py') ; intros py ; simpl. - cut (x = y). - { - enough (s1 = s2) as X. - { - unfold s1, s2 in X. - contradiction (inl_ne_inr _ _ X). - } - unfold gs1, gs2 in *. - refine ((fg s1)^ @ _ @ fg s2). - rewrite Hgs1, Hgs2. - f_ap. - simple refine (path_sigma _ _ _ _ _); [ | apply path_ishprop ]; simpl. - destruct px as [px | px] ; destruct py as [py | py] - ; refine (Trunc_rec _ px) ; clear px ; intro px - ; refine (Trunc_rec _ py) ; clear py ; intro py. - * apply (px @ py^). - * refine (px @ _ @ py^). auto. - * refine (px @ _^ @ py^). auto. - * apply (px @ py^). - } - destruct px as [px | px] ; destruct py as [py | py] - ; refine (Trunc_rec _ px) ; clear px ; intro px - ; refine (Trunc_rec _ py) ; clear py ; intro py. - ** apply (px @ py^). - ** refine (px @ _ @ py^). auto. - ** refine (px @ _^ @ py^). auto. - ** apply (px @ py^). - Defined. + exists a. + apply (tr(inl(tr idpath))). + - refine (inl _). + pose (s1 := (a;tr(inl(tr idpath))) + : {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}). + pose (s2 := (b;tr(inr(tr idpath))) + : {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}). + refine (ap (fun x => x.1) (gf s1)^ @ _ @ (ap (fun x => x.1) (gf s2))). + assert (fs_eq : f s1 = f s2). + { by apply path_ishprop. } + refine (ap (fun x => (g x).1) fs_eq). + - (* Otherwise, ¬(a = b) *) + refine (inr (fun p => _)). + pose (s1 := inl (inr tt) : Fin n + Unit + Unit). + pose (s2 := inr tt : Fin n + Unit + Unit). + pose (gs1 := g s1). + pose (c := gs1). + pose (gs2 := g s2). + pose (d := gs2). + assert (Hgs1 : gs1 = c) by reflexivity. + assert (Hgs2 : gs2 = d) by reflexivity. + destruct c as [x px'], d as [y py']. + simple refine (Trunc_ind _ _ px') ; intros px + ; simple refine (Trunc_ind _ _ py') ; intros py ; simpl. + enough (s1 = s2) as X. + { + unfold s1, s2 in X. + contradiction (inl_ne_inr _ _ X). + } + refine ((fg s1)^ @ ap f (Hgs1 @ _ @ Hgs2^) @ fg s2). + simple refine (path_sigma _ _ _ _ _); [ | apply path_ishprop ]; simpl. + destruct px as [px | px] ; destruct py as [py | py] + ; refine (Trunc_rec _ px) ; clear px ; intro px + ; refine (Trunc_rec _ py) ; clear py ; intro py. + * apply (px @ py^). + * refine (px @ p @ py^). + * refine (px @ p^ @ py^). + * apply (px @ py^). + Defined. End finite_hott. Section singleton_set. Variable (A : Type). Context `{Univalence}. + Variable (HA : forall a, {b : A & b ∈ {|a|}} <~> Fin 1). + Definition el x : {b : A & b ∈ {|x|}} := (x;tr idpath). - Theorem single_bfin_set (HA : forall a, {b : A & b ∈ {|a|}} <~> Fin 1) - : forall (x : A) (p : x = x), p = idpath. + Theorem single_bfin_set : forall (x : A) (p : x = x), p = idpath. Proof. intros x p. specialize (HA x). @@ -172,6 +154,13 @@ Section singleton_set. } apply path_ishprop. Defined. + + Global Instance set_singleton : IsHSet A. + Proof. + refine hset_axiomK. + unfold axiomK. + apply single_bfin_set. + Defined. End singleton_set. Section empty. @@ -179,6 +168,7 @@ Section empty. Variable (X : A -> hProp) (Xequiv : {a : A & a ∈ X} <~> Fin 0). Context `{Univalence}. + Lemma X_empty : X = ∅. Proof. apply path_forall. @@ -217,8 +207,7 @@ Section split. apply path_sigma_hprop. apply p. - rewrite transport_paths_FlFr. hott_simpl; cbn. - rewrite ap_compose. - rewrite (ap_compose inl f^-1). + rewrite ap_compose, (ap_compose inl f^-1). rewrite ap_inl_path_sum_inl. repeat (rewrite transport_paths_FlFr; hott_simpl). rewrite !ap_pp. @@ -233,7 +222,8 @@ Section split. rewrite concat_Vp. rewrite (concat_p_pp (ap pr1 (eissect f (f^-1 (inl x))))^). rewrite concat_Vp. - hott_simpl. } + hott_simpl. + } exists (fun a => BuildhProp (P' a)). exists (f^-1 (inr tt)).1. split. @@ -245,8 +235,9 @@ Section split. - intros [a [y p]]; cbn. eapply path_sigma with p^. apply path_ishprop. - - intros x; cbn. - reflexivity. } + - intros x. + reflexivity. + } { intros a. unfold P'. apply path_iff_hprop. @@ -279,9 +270,8 @@ Section Bfin_no_singletons. Definition S1toSig (x : S1) : {x : S1 & merely(x = base)}. Proof. exists x. - simple refine (S1_ind (fun z => merely(z = base)) _ _ x) ; simpl. - - apply (tr idpath). - - apply path_ishprop. + simple refine (S1_ind (fun z => merely(z = base)) (tr idpath) _ x). + apply path_ishprop. Defined. Instance S1toSig_equiv : IsEquiv S1toSig. @@ -289,10 +279,9 @@ Section Bfin_no_singletons. apply isequiv_biinv. split. - exists (fun x => x.1). - simple refine (S1_ind _ _ _) ; simpl. - * reflexivity. - * rewrite transport_paths_FlFr. - hott_simpl. + simple refine (S1_ind _ idpath _) ; simpl. + rewrite transport_paths_FlFr. + hott_simpl. - exists (fun x => x.1). intros [z x]. simple refine (path_sigma _ _ _ _ _) ; simpl. @@ -322,7 +311,8 @@ End Bfin_no_singletons. (* If A has decidable equality, then every Bfin subobject has decidable membership *) Section dec_membership. Variable (A : Type). - Context `{DecidablePaths A} `{Univalence}. + Context `{MerelyDecidablePaths A} `{Univalence}. + Global Instance DecidableMembership (P : Sub A) (Hfin : Bfin P) (a : A) : Decidable (a ∈ P). Proof. @@ -341,20 +331,23 @@ Section dec_membership. unfold member, sub_membership. rewrite (HP a). destruct (IHn P' HP') as [IH | IH]. - + left. apply (tr (inl IH)). - + destruct (dec (a = b)) as [Hab | Hab]. - left. apply (tr (inr (tr Hab))). - right. intros α. strip_truncations. - destruct α as [? | ?]; [ | strip_truncations]; contradiction. + * apply (inl (tr (inl IH))). + * destruct (m_dec_path a b) as [Hab | Hab]. + + apply (inl (tr (inr Hab))). + + refine (inr(fun a => _)). + strip_truncations. + destruct a as [? | t] ; [ | strip_truncations] ; try contradiction. + contradiction (Hab (tr t)). Defined. End dec_membership. Section bfin_kfin. Context `{Univalence}. + Lemma bfin_to_kfin : forall (B : Type), Finite B -> Kf B. Proof. apply finite_ind_hprop. - - intros. apply _. + - apply _. - apply Kf_unfold. exists ∅. intros []. - intros B [n f] IH. @@ -393,56 +386,43 @@ Section kfin_bfin. Proof. intros HYb. unshelve eapply BuildEquiv. - { intros [a Ha]. cbn in Ha. + - intros [a Ha]. cbn in Ha. destruct (dec (BuildhProp (a = b))) as [Hab | Hab]. - - right. apply tt. - - left. exists a. + + apply (inr tt). + + refine (inl(a;_)). strip_truncations. destruct Ha as [HXa | HYa]. - + refine (Empty_rec _). + * refine (Empty_rec _). strip_truncations. by apply Hab. - + apply HYa. } - { apply isequiv_biinv. - unshelve esplit; cbn. - - unshelve eexists. - + intros [[a Ha] | []]. - * exists a. - apply tr. - right. apply Ha. - * exists b. - apply (tr (inl (tr idpath))). - + intros [a Ha]; cbn. - strip_truncations. - simple refine (path_sigma' _ _ _); [ | apply path_ishprop ]. - destruct (H a b); cbn. - * apply p^. - * reflexivity. - - unshelve eexists. (* TODO ACHTUNG CODE DUPLICATION *) - + intros [[a Ha] | []]. - * exists a. - apply tr. - right. apply Ha. - * exists b. - apply (tr (inl (tr idpath))). - + intros [[a Ha] | []]; cbn. - destruct (dec (_ = b)) as [Hb | Hb]; cbn. - { refine (Empty_rec _). - rewrite Hb in Ha. - contradiction. } - { reflexivity. } - destruct (dec (b = b)); [ reflexivity | contradiction ]. } + * apply HYa. + - apply isequiv_biinv. + unshelve esplit ; (unshelve eexists + ; [intros [[a Ha] | []] + ; [apply (a;(tr(inr Ha))) | apply (b;(tr(inl (tr idpath))))] + | ]). + + intros [a Ha]; cbn. + strip_truncations. + simple refine (path_sigma' _ _ _); [ | apply path_ishprop ]. + destruct (H a b); cbn. + * apply p^. + * reflexivity. + + intros [[a Ha] | []]; cbn. + destruct (dec (a = b)) as [Hb | Hb]; cbn. + * refine (Empty_rec _). + rewrite Hb in Ha. + contradiction. + * reflexivity. + * destruct (dec (b = b)); [ reflexivity | contradiction ]. Defined. Theorem bfin_union : @closedUnion A Bfin. Proof. - intros X Y HX HY. - destruct HX as [n fX]. + intros X Y [n fX] HY. strip_truncations. revert fX. revert X. induction n; intros X fX. - - rewrite (X_empty _ X fX). - rewrite (neutralL_max (Sub A)). + - rewrite (X_empty _ X fX), (neutralL_max (Sub A)). apply HY. - destruct (split X n fX) as (X' & b & HX' & HX). @@ -469,48 +449,45 @@ Section kfin_bfin. exists (n'.+1). apply tr. transitivity ({a : A & a ∈ (fun a => merely (a = b)) ∪ (X' ∪ Y)}). - { apply equiv_functor_sigma_id. + * apply equiv_functor_sigma_id. intro a. rewrite <- (associative_max (Sub A)). assert (X = X' ∪ (fun a => merely (a = b))) as HX_. - { apply path_forall. intros ?. - unfold union, sub_union, max_fun. - apply HX. } - rewrite HX_. - rewrite <- (commutative_max (Sub A) X'). - reflexivity. } - cbn[Fin]. - etransitivity. apply (notIn_ext_union_singleton b _ HX'Yb). - by rewrite ((equiv_path _ _)^-1 fw). + ** apply path_forall. intros ?. + unfold union, sub_union, max_fun. + apply HX. + ** rewrite HX_, <- (commutative_max (Sub A) X'). + reflexivity. + * etransitivity. + { apply (notIn_ext_union_singleton b _ HX'Yb). } + by rewrite ((equiv_path _ _)^-1 fw). Defined. Definition FSet_to_Bfin : forall (X : FSet A), Bfin (map X). Proof. hinduction; try (intros; apply path_ishprop). - - exists 0. apply tr. simpl. + - exists 0. + apply tr. simple refine (BuildEquiv _ _ _ _). destruct 1 as [? []]. - - intros a. - apply _. - - intros Y1 Y2 HY1 HY2. - apply bfin_union; auto. + - apply _. + - intros. + apply bfin_union ; assumption. Defined. End kfin_bfin. -Instance Kf_to_Bf (X : Type) `{Univalence} `{DecidablePaths X} (Hfin : Kf X) : Finite X. +Global Instance Kf_to_Bf (X : Type) `{Univalence} `{DecidablePaths X} (Hfin : Kf X) : Finite X. Proof. - apply Kf_unfold in Hfin. - destruct Hfin as [Y HY]. - pose (X' := FSet_to_Bfin _ Y). - unfold Bfin in X'. - simple refine (finite_equiv' _ _ X'). + destruct (Kf_unfold _ Hfin) as [Y HY]. + simple refine (finite_equiv' _ _ (FSet_to_Bfin _ Y)). unshelve esplit. - - intros [a ?]. apply a. - - apply isequiv_biinv. split. + - apply (fun z => z.1). + - apply isequiv_biinv. + split. * exists (fun a => (a;HY a)). intros [b Hb]. apply path_sigma' with idpath. apply path_ishprop. - * exists (fun a => (a;HY a)). - intros b. reflexivity. + * refine (fun a => (a;HY a);fun _ => _). + reflexivity. Defined. \ No newline at end of file