From 344117a9b3750335e8b4d6007bb18af212a2ae45 Mon Sep 17 00:00:00 2001 From: Niels van der Weide Date: Thu, 21 Sep 2017 23:33:20 +0200 Subject: [PATCH] Length of product --- FiniteSets/kuratowski/length.v | 82 +++++++++++++++++++++++++++++- FiniteSets/kuratowski/properties.v | 55 ++++++++++++++++++-- FiniteSets/prelude.v | 27 +++++++++- 3 files changed, 157 insertions(+), 7 deletions(-) diff --git a/FiniteSets/kuratowski/length.v b/FiniteSets/kuratowski/length.v index 1e15494..9eaa6e4 100644 --- a/FiniteSets/kuratowski/length.v +++ b/FiniteSets/kuratowski/length.v @@ -1,7 +1,7 @@ Require Import HoTT HitTactics prelude interfaces.lattice_interface interfaces.lattice_examples. Require Import kuratowski.operations kuratowski.properties kuratowski.kuratowski_sets isomorphism. -Section Length. +Section length. Context {A : Type} `{MerelyDecidablePaths A} `{Univalence}. Definition length : FSet A -> nat. @@ -148,5 +148,83 @@ Section Length. rewrite plus_assoc. reflexivity. Defined. +End length. + +Section length_product. + Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B} `{Univalence}. -End Length. \ No newline at end of file + Theorem length_singleproduct (a : A) (X : FSet B) + : length (single_product a X) = length X. + Proof. + simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _ X) + ; try (intros ; apply path_ishprop) ; simpl. + - reflexivity. + - intros b X1 HX1. + rewrite ?length_compute, ?HX1. + enough(b ∈_d X1 = (a, b) ∈_d (single_product a X1)) as HE. + { rewrite HE ; reflexivity. } + rewrite singleproduct_isIn_d_aa ; try reflexivity. + Defined. + + Open Scope nat. + + Lemma single_product_disjoint (a : A) (X1 : FSet A) (Y : FSet B) + : sum (prod (a ∈_d X1 = true) + ((single_product a Y) ∪ (product X1 Y) = (product X1 Y))) + (prod (a ∈_d X1 = false) + (disjoint (single_product a Y) (product X1 Y))). + Proof. + pose (b := a ∈_d X1). + assert (a ∈_d X1 = b) as HaX1. + { reflexivity. } + destruct b. + * refine (inl(HaX1,_)). + apply ext. + intros [a1 b1]. + rewrite ?union_isIn_d. + unfold member_dec, fset_member_bool in *. + destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t] + ; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p] + ; try reflexivity. + rewrite singleproduct_isIn in t. + destruct t as [t1 t2]. + rewrite product_isIn in p. + strip_truncations. + rewrite <- t1 in HaX1. + destruct (dec (a1 ∈ X1)) ; try (contradiction false_ne_true). + contradiction (p(t,t2)). + * refine (inr(HaX1,_)). + apply ext. + intros [a1 b1]. + rewrite intersection_isIn_d, empty_isIn_d. + unfold member_dec, fset_member_bool in *. + destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t] + ; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p] + ; try reflexivity. + rewrite singleproduct_isIn in t ; destruct t as [t1 t2]. + rewrite product_isIn in p ; destruct p as [p1 p2]. + strip_truncations. + rewrite t1 in p1. + destruct (dec (a ∈ X1)). + ** contradiction true_ne_false. + ** contradiction (n p1). + Defined. + + Theorem length_product (X : FSet A) (Y : FSet B) + : length (product X Y) = length X * length Y. + Proof. + simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _ X) + ; try (intros ; apply path_ishprop) ; simpl. + - reflexivity. + - intros a X1 HX1. + rewrite length_compute. + destruct (single_product_disjoint a X1 Y) as [[p1 p2] | [p1 p2]]. + * rewrite p2. + destruct (a ∈_d X1). + ** apply HX1. + ** contradiction false_ne_true. + * rewrite p1, length_disjoint, HX1 ; try assumption. + rewrite length_singleproduct. + reflexivity. + Defined. +End length_product. diff --git a/FiniteSets/kuratowski/properties.v b/FiniteSets/kuratowski/properties.v index f81b11d..d6e4b9b 100644 --- a/FiniteSets/kuratowski/properties.v +++ b/FiniteSets/kuratowski/properties.v @@ -52,7 +52,7 @@ Section properties_membership. Context {B : Type}. - Lemma isIn_singleproduct (a : A) (b : B) (c : A) : forall (Y : FSet B), + Lemma singleproduct_isIn (a : A) (b : B) (c : A) : forall (Y : FSet B), (a, b) ∈ (single_product c Y) = land (BuildhProp (Trunc (-1) (a = c))) (b ∈ Y). Proof. hinduction ; try (intros ; apply path_ishprop). @@ -91,13 +91,13 @@ Section properties_membership. split ; try (apply (tr H1)) ; try (apply Hb2). Defined. - Definition isIn_product (a : A) (b : B) (X : FSet A) (Y : FSet B) : + Definition product_isIn (a : A) (b : B) (X : FSet A) (Y : FSet B) : (a,b) ∈ (product X Y) = land (a ∈ X) (b ∈ Y). Proof. hinduction X ; try (intros ; apply path_ishprop). - apply path_hprop ; symmetry ; apply prod_empty_l. - intros. - apply isIn_singleproduct. + apply singleproduct_isIn. - intros X1 X2 HX1 HX2. cbn. rewrite HX1, HX2. @@ -324,7 +324,7 @@ Section properties_membership_decidable. a ∈_d (difference X Y) = andb (a ∈_d X) (negb (a ∈_d Y)). Proof. apply comprehension_isIn_d. - Defined. + Defined. Lemma singleton_isIn_d `{IsHSet A} (a b : A) : a ∈ {|b|} -> a = b. @@ -335,6 +335,53 @@ Section properties_membership_decidable. Defined. End properties_membership_decidable. +Section product_membership. + Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B} `{Univalence}. + + Lemma singleproduct_isIn_d_aa (a : A) (b : B) (c : A) (p : c = a) (Y : FSet B) : + (a, b) ∈_d (single_product c Y) = b ∈_d Y. + Proof. + unfold member_dec, fset_member_bool, dec ; simpl. + destruct (isIn_decidable (a, b) (single_product c Y)) as [t | t] + ; destruct (isIn_decidable b Y) as [n | n] + ; try reflexivity. + * rewrite singleproduct_isIn in t. + destruct t as [t1 t2]. + contradiction (n t2). + * rewrite singleproduct_isIn in t. + contradiction (t (tr(p^),n)). + Defined. + + Lemma singleproduct_isIn_d_false (a : A) (b : B) (c : A) (p : c = a -> Empty) (Y : FSet B) : + (a, b) ∈_d (single_product c Y) = false. + Proof. + unfold member_dec, fset_member_bool, dec ; simpl. + destruct (isIn_decidable (a, b) (single_product c Y)) as [t | t] + ; destruct (isIn_decidable b Y) as [n | n] + ; try reflexivity. + * rewrite singleproduct_isIn in t. + destruct t as [t1 t2]. + strip_truncations. + contradiction (p t1^). + * rewrite singleproduct_isIn in t. + contradiction (n (snd t)). + Defined. + + Lemma product_isIn_d (a : A) (b : B) (X : FSet A) (Y : FSet B) : + (a, b) ∈_d (product X Y) = andb (a ∈_d X) (b ∈_d Y). + Proof. + unfold member_dec, fset_member_bool, dec ; simpl. + destruct (isIn_decidable (a, b) (product X Y)) as [t | t] + ; destruct (isIn_decidable a X) as [n1 | n1] + ; destruct (isIn_decidable b Y) as [n2 | n2] + ; try reflexivity + ; rewrite ?product_isIn in t + ; try (destruct t as [t1 t2] + ; contradiction (n1 t1) || contradiction (n2 t2)). + contradiction (t (n1, n2)). + Defined. +End product_membership. + (* Some suporting tactics *) Ltac simplify_isIn_d := repeat (rewrite union_isIn_d diff --git a/FiniteSets/prelude.v b/FiniteSets/prelude.v index 28089b9..5fcbd39 100644 --- a/FiniteSets/prelude.v +++ b/FiniteSets/prelude.v @@ -35,4 +35,29 @@ Proof. - refine (inr(fun p => _)). strip_truncations. apply (n p). -Defined. \ No newline at end of file +Defined. + +Global Instance merely_decidable_paths_prod (A B : Type) + `{MerelyDecidablePaths A} `{MerelyDecidablePaths B} + : MerelyDecidablePaths(A * B). +Proof. + intros x y. + destruct (m_dec_path (fst x) (fst y)) as [p1 | n1], + (m_dec_path (snd x) (snd y)) as [p2 | n2]. + - apply inl. + strip_truncations. + apply tr. + apply path_prod ; assumption. + - apply inr. + intros pp. + strip_truncations. + apply (n2 (tr (ap snd pp))). + - apply inr. + intros pp. + strip_truncations. + apply (n1 (tr (ap fst pp))). + - apply inr. + intros pp. + strip_truncations. + apply (n1 (tr (ap fst pp))). +Defined.