From 1bab2206a30f69bdebec176fde9a4e0d09194565 Mon Sep 17 00:00:00 2001 From: Niels Date: Mon, 7 Aug 2017 16:22:55 +0200 Subject: [PATCH] Some cleaning --- FiniteSets/fsets/properties.v | 121 ++++++++++++++----------------- FiniteSets/representations/bad.v | 62 ++++++++-------- 2 files changed, 86 insertions(+), 97 deletions(-) diff --git a/FiniteSets/fsets/properties.v b/FiniteSets/fsets/properties.v index ade2872..cc20a78 100644 --- a/FiniteSets/fsets/properties.v +++ b/FiniteSets/fsets/properties.v @@ -9,8 +9,7 @@ Section operations_isIn. Lemma union_idem : forall x: FSet A, U x x = x. Proof. - hinduction; - try (intros ; apply set_path2). + hinduction ; try (intros ; apply set_path2). - apply nl. - apply idem. - intros x y P Q. @@ -21,16 +20,16 @@ Section operations_isIn. rewrite (comm y x). rewrite <- (assoc x y y). f_ap. - Qed. + Defined. (** ** Properties about subset relation. *) Lemma subset_union (X Y : FSet A) : subset X Y -> U X Y = Y. Proof. - hinduction X; try (intros; apply path_forall; intro; apply set_path2). + hinduction X ; try (intros; apply path_forall; intro; apply set_path2). - intros. apply nl. - - intros a. hinduction Y; - try (intros; apply path_forall; intro; apply set_path2). + - intros a. + hinduction Y ; try (intros; apply path_forall; intro; apply set_path2). + intro. contradiction. + intro a0. @@ -53,34 +52,28 @@ Section operations_isIn. rewrite (IH2 G2). apply (IH1 G1). Defined. - + Lemma subset_union_l (X : FSet A) : forall Y, subset X (U X Y). Proof. - hinduction X ; - try (repeat (intro; intros; apply path_forall); intro; apply equiv_hprop_allpath ; apply _). + hinduction X ; try (repeat (intro; intros; apply path_forall); + intro ; apply equiv_hprop_allpath ; apply _). - apply (fun _ => tt). - intros a Y. - apply tr ; left ; apply tr ; reflexivity. + apply (tr(inl(tr idpath))). - intros X1 X2 HX1 HX2 Y. split. * rewrite <- assoc. apply HX1. * rewrite (comm X1 X2). rewrite <- assoc. apply HX2. Defined. - (* Union and membership *) - Lemma union_isIn (X Y : FSet A) (a : A) : - isIn a (U X Y) = isIn a X ∨ isIn a Y. - Proof. - reflexivity. - Defined. - + (* simplify it using extensionality *) Lemma comprehension_or : forall ϕ ψ (x: FSet A), comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) (comprehension ψ x). Proof. intros ϕ ψ. - hinduction; try (intros; apply set_path2). + hinduction ; try (intros; apply set_path2). - apply (union_idem _)^. - intros. destruct (ϕ a) ; destruct (ψ a) ; symmetry. @@ -108,16 +101,43 @@ Section properties. Context `{Univalence}. (** isIn properties *) - Lemma singleton_isIn (a b: A) : isIn a (L b) -> Trunc (-1) (a = b). + Definition empty_isIn (a: A) : isIn a E -> Empty := idmap. + + Definition singleton_isIn (a b: A) : isIn a (L b) -> Trunc (-1) (a = b) := idmap. + + Definition union_isIn (X Y : FSet A) (a : A) + : isIn a (U X Y) = isIn a X ∨ isIn a Y := idpath. + + Lemma comprehension_isIn (ϕ : A -> Bool) (a : A) : forall X : FSet A, + isIn a (comprehension ϕ X) = if ϕ a then isIn a X else False_hp. Proof. - apply idmap. - Defined. - - Lemma empty_isIn (a: A) : isIn a E -> Empty. - Proof. - apply idmap. + hinduction ; try (intros ; apply set_path2) ; cbn. + - destruct (ϕ a) ; reflexivity. + - intros b. + assert (forall c d, ϕ a = c -> ϕ b = d -> + a ∈ (if ϕ b then {|b|} else ∅) + = + (if ϕ a then BuildhProp (Trunc (-1) (a = b)) else False_hp)) as X. + { + intros c d Hc Hd. + destruct c ; destruct d ; rewrite Hc, Hd ; try reflexivity + ; apply path_iff_hprop ; try contradiction ; intros ; strip_truncations + ; apply (false_ne_true). + * apply (Hd^ @ ap ϕ X^ @ Hc). + * apply (Hc^ @ ap ϕ X @ Hd). + } + apply (X (ϕ a) (ϕ b) idpath idpath). + - intros X Y H1 H2. + rewrite H1, H2. + destruct (ϕ a). + * reflexivity. + * apply path_iff_hprop. + ** intros Z ; strip_truncations. + destruct Z ; assumption. + ** intros ; apply tr ; right ; assumption. Defined. + (* The proof can be simplified using extensionality *) (** comprehension properties *) Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = E. Proof. @@ -125,11 +145,11 @@ Section properties. - reflexivity. - reflexivity. - intros x y IHa IHb. - rewrite IHa. - rewrite IHb. + rewrite IHa, IHb. apply union_idem. Defined. + (* Can be simplified using extensionality *) Lemma comprehension_subset : forall ϕ (X : FSet A), U (comprehension ϕ X) X = X. Proof. @@ -160,54 +180,21 @@ Section properties. - 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. + * refine (tr (inl _)). rewrite XE, YE. apply (union_idem E). - * right. - destruct HY as [a Ya]. - apply tr. + * destruct HY as [a Ya]. + refine (inr (tr _)). exists a. apply (tr (inr Ya)). - * right. - destruct HX as [a Xa]. - apply tr. + * destruct HX as [a Xa]. + refine (inr (tr _)). exists a. apply (tr (inl Xa)). - * right. - destruct HX as [a Xa]. - destruct HY as [b Yb]. - apply tr. + * destruct (HX, HY) as [[a Xa] [b Yb]]. + refine (inr (tr _)). exists a. apply (tr (inl Xa)). Defined. - - Lemma comprehension_isIn (ϕ : A -> Bool) (a : A) : forall X : FSet A, - isIn a (comprehension ϕ X) = if ϕ a then isIn a X else False_hp. - Proof. - hinduction ; try (intros ; apply set_path2) ; cbn. - - destruct (ϕ a) ; reflexivity. - - intros b. - assert (forall c d, ϕ a = c -> ϕ b = d -> - a ∈ (if ϕ b then {|b|} else ∅) - = - (if ϕ a then BuildhProp (Trunc (-1) (a = b)) else False_hp)) as X. - { - intros c d Hc Hd. - destruct c ; destruct d ; rewrite Hc, Hd ; try reflexivity - ; apply path_iff_hprop ; try contradiction ; intros ; strip_truncations - ; apply (false_ne_true). - * apply (Hd^ @ ap ϕ X^ @ Hc). - * apply (Hc^ @ ap ϕ X @ Hd). - } - apply (X (ϕ a) (ϕ b) idpath idpath). - - intros X Y H1 H2. - rewrite H1, H2. - destruct (ϕ a). - * reflexivity. - * apply path_iff_hprop. - ** intros Z ; strip_truncations. - destruct Z ; assumption. - ** intros ; apply tr ; right ; assumption. - Defined. End properties. diff --git a/FiniteSets/representations/bad.v b/FiniteSets/representations/bad.v index e0abc6c..b884ae8 100644 --- a/FiniteSets/representations/bad.v +++ b/FiniteSets/representations/bad.v @@ -42,19 +42,22 @@ Module Export FSet. Arguments nl {_} _. Arguments nr {_} _. Arguments idem {_} _. + Notation "{| x |}" := (L x). + Infix "∪" := U (at level 8, right associativity). + Notation "∅" := E. Section FSet_induction. Variable A: Type. Variable (P : FSet A -> Type). - Variable (eP : P E). - Variable (lP : forall a: A, P (L a)). - Variable (uP : forall (x y: FSet A), P x -> P y -> P (U x y)). + Variable (eP : P ∅). + Variable (lP : forall a: A, P {|a |}). + Variable (uP : forall (x y: FSet A), P x -> P y -> P (x ∪ y)). Variable (assocP : forall (x y z : FSet A) (px: P x) (py: P y) (pz: P z), assoc x y z # - (uP x (U y z) px (uP y z py pz)) + (uP x (y ∪ z) px (uP y z py pz)) = - (uP (U x y) z (uP x y px py) pz)). + (uP (x ∪ y) z (uP x y px py) pz)). Variable (commP : forall (x y: FSet A) (px: P x) (py: P y), comm x y # uP x y px py = uP y x py px). @@ -71,26 +74,24 @@ Module Export FSet. {struct x} : P x := (match x return _ -> _ -> _ -> _ -> _ -> P x with - | E => fun _ => fun _ => fun _ => fun _ => fun _ => eP - | L a => fun _ => fun _ => fun _ => fun _ => fun _ => lP a - | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z - (FSet_ind y) - (FSet_ind z) + | ∅ => fun _ _ _ _ _ => eP + | {|a|} => fun _ _ _ _ _ => lP a + | y ∪ z => fun _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z) end) assocP commP nlP nrP idemP. Axiom FSet_ind_beta_assoc : forall (x y z : FSet A), apD FSet_ind (assoc x y z) = - (assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)). + (assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)). Axiom FSet_ind_beta_comm : forall (x y : FSet A), - apD FSet_ind (comm x y) = (commP x y (FSet_ind x) (FSet_ind y)). + apD FSet_ind (comm x y) = commP x y (FSet_ind x) (FSet_ind y). Axiom FSet_ind_beta_nl : forall (x : FSet A), - apD FSet_ind (nl x) = (nlP x (FSet_ind x)). + apD FSet_ind (nl x) = nlP x (FSet_ind x). Axiom FSet_ind_beta_nr : forall (x : FSet A), - apD FSet_ind (nr x) = (nrP x (FSet_ind x)). + apD FSet_ind (nr x) = nrP x (FSet_ind x). Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x. End FSet_induction. @@ -183,9 +184,11 @@ Module Export FSet. End FSet_recursion. - Instance FSet_recursion A : HitRecursion (FSet A) := { - indTy := _; recTy := _; - H_inductor := FSet_ind A; H_recursor := FSet_rec A }. + Instance FSet_recursion A : HitRecursion (FSet A) := + { + indTy := _; recTy := _; + H_inductor := FSet_ind A; H_recursor := FSet_rec A + }. End FSet. @@ -195,10 +198,12 @@ Notation "∅" := E. Section set_sphere. From HoTT.HIT Require Import Circle. - From HoTT Require Import UnivalenceAxiom. - Instance S1_recursion : HitRecursion S1 := { - indTy := _; recTy := _; - H_inductor := S1_ind; H_recursor := S1_rec }. + Context `{Univalence}. + Instance S1_recursion : HitRecursion S1 := + { + indTy := _; recTy := _; + H_inductor := S1_ind; H_recursor := S1_rec + }. Variable A : Type. @@ -206,8 +211,7 @@ Section set_sphere. Proof. hrecursion x. - exact loop. - - etransitivity. - eapply (@transport_paths_FlFr S1 S1 idmap idmap). + - refine (transport_paths_FlFr _ _ @ _). hott_simpl. Defined. @@ -225,11 +229,10 @@ Section set_sphere. Proof. hrecursion x. - exact loop. - - etransitivity. - apply (@transport_paths_FlFr _ _ (fun x => S1op base x) idmap _ _ loop loop). + - refine (transport_paths_FlFr loop _ @ _). hott_simpl. apply moveR_pM. apply moveR_pM. hott_simpl. - etransitivity. apply (ap_V (S1op base) loop). + refine (ap_V _ _ @ _). f_ap. apply S1_rec_beta_loop. Defined. @@ -237,8 +240,7 @@ Section set_sphere. Proof. hrecursion z. - reflexivity. - - etransitivity. - apply (@transport_paths_FlFr _ _ (fun z => S1op x (S1op y z)) (S1op (S1op x y)) _ _ loop idpath). + - refine (transport_paths_FlFr loop _ @ _). hott_simpl. apply moveR_Mp. hott_simpl. rewrite S1_rec_beta_loop. @@ -274,7 +276,7 @@ Section set_sphere. Lemma FSet_S_ap : (nl (@E A)) = (nr E) -> idpath = loop. Proof. - intros H. + intros H1. enough (ap FSet_to_S (nl E) = ap FSet_to_S (nr E)) as H'. - rewrite FSet_rec_beta_nl in H'. rewrite FSet_rec_beta_nr in H'. @@ -285,7 +287,7 @@ Section set_sphere. Lemma FSet_not_hset : IsHSet (FSet A) -> False. Proof. - intros H. + intros H1. enough (idpath = loop). - assert (S1_encode _ idpath = S1_encode _ (loopexp loop (pos Int.one))) as H' by f_ap. rewrite S1_encode_loopexp in H'. simpl in H'. symmetry in H'.