From 8a1405a1d8b5b98f252fa329ee27a3de98bcd093 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Sat, 19 Aug 2017 18:55:47 +0200 Subject: [PATCH] A cons-based induction principle for FSets --- FiniteSets/fsets/isomorphism.v | 87 ++++++++++++++++++++++++++---- FiniteSets/variations/enumerated.v | 23 +++----- 2 files changed, 84 insertions(+), 26 deletions(-) diff --git a/FiniteSets/fsets/isomorphism.v b/FiniteSets/fsets/isomorphism.v index a4fa178..10d88fc 100644 --- a/FiniteSets/fsets/isomorphism.v +++ b/FiniteSets/fsets/isomorphism.v @@ -8,6 +8,12 @@ Section Iso. Context {A : Type}. Context `{Univalence}. + Definition dupl' (a : A) (X : FSet A) : + {|a|} ∪ {|a|} ∪ X = {|a|} ∪ X := assoc _ _ _ @ ap (∪ X) (idem _). + Definition comm' (a b : A) (X : FSet A) : + {|a|} ∪ {|b|} ∪ X = {|b|} ∪ {|a|} ∪ X := + assoc _ _ _ @ ap (∪ X) (comm _ _) @ (assoc _ _ _)^. + Definition FSetC_to_FSet: FSetC A -> FSet A. Proof. hrecursion. @@ -15,15 +21,9 @@ Section Iso. - intros a x. apply ({|a|} ∪ x). - intros. cbn. - etransitivity. apply assoc. - apply (ap (∪ x)). - apply idem. + apply dupl'. - intros. cbn. - etransitivity. apply assoc. - etransitivity. refine (ap (∪ x) _ ). - apply FSet.comm. - symmetry. - apply assoc. + apply comm'. Defined. Definition FSet_to_FSetC: FSet A -> FSetC A. @@ -45,7 +45,9 @@ Section Iso. 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 *. rewrite HR. apply assoc. + - intros a x HR y. unfold union, fsetc_union in *. + refine (_ @ assoc _ _ _). + apply (ap ({|a|} ∪) (HR _)). Defined. Lemma repr_iso_id_l: forall (x: FSet A), FSetC_to_FSet (FSet_to_FSetC x) = x. @@ -53,7 +55,10 @@ Section Iso. hinduction; try (intros; apply set_path2). - reflexivity. - intro. apply nr. - - intros x y p q. rewrite append_union, p, q. reflexivity. + - intros x y p q. + refine (append_union _ _ @ _). + refine (ap (∪ _) p @ _). + apply (ap (_ ∪) q). Defined. Lemma repr_iso_id_r: forall (x: FSetC A), FSet_to_FSetC (FSetC_to_FSet x) = x. @@ -89,4 +94,66 @@ Section Iso. apply (equiv_path _ _)^-1. exact repr_iso. Defined. + + Theorem FSet_cons_ind (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 X, 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. + - apply Pempt. + - intros a Y HY. by apply Pcons. + - intros a Y PY. cbn. + refine (_ @ (Pdupl _ _ _)). + etransitivity. + { apply (transport_compose _ FSetC_to_FSet (dupl a Y)). } + refine (ap (fun z => transport P z _) _). + apply FSetC_rec_beta_dupl. + - intros a b Y PY. cbn. + refine (_ @ (Pcomm _ _ _ _)). + etransitivity. + { apply (transport_compose _ FSetC_to_FSet (FSetC.comm a b Y)). } + refine (ap (fun z => transport P z _) _). + apply FSetC_rec_beta_comm. + Defined. + + Theorem FSet_cons_ind_beta_empty (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)) : + FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm ∅ = Pempt. + Proof. 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). *) End Iso. diff --git a/FiniteSets/variations/enumerated.v b/FiniteSets/variations/enumerated.v index 8b73de8..8663d5d 100644 --- a/FiniteSets/variations/enumerated.v +++ b/FiniteSets/variations/enumerated.v @@ -251,35 +251,26 @@ Section fset_dec_enumerated. Variable A : Type. Context `{Univalence}. - Definition Kf_fsetc : - Kf A -> exists (X : FSetC A), forall (a : A), k_finite.map (FSetC_to_FSet X) a. + Definition merely_enumeration_FSet : + forall (X : FSet A), + hexists (fun (ls : list A) => forall a, a ∈ X = listExt ls a). Proof. - intros [X HX]. - exists (FSet_to_FSetC X). - rewrite repr_iso_id_l. - by rewrite <- HX. - Defined. - - Definition merely_enumeration_FSetC : - forall (X : FSetC A), - hexists (fun (ls : list A) => forall a, a ∈ (FSetC_to_FSet X) = listExt ls a). - Proof. - hinduction. + simple refine (FSet_cons_ind _ _ _ _ _ _); simpl. - 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. - f_ap. + apply (ap (fun z => _ ∨ z) (Hls b)). - intros. apply path_ishprop. - intros. apply path_ishprop. Defined. Definition Kf_enumerated : Kf A -> enumerated A. Proof. - intros HKf. apply Kf_fsetc in HKf. + intros HKf. apply Kf_unfold in HKf. destruct HKf as [X HX]. - pose (ls' := (merely_enumeration_FSetC X)). + pose (ls' := (merely_enumeration_FSet X)). simple refine (@Trunc_rec _ _ _ _ _ ls'). clear ls'. intros [ls Hls]. apply tr. exists ls.