From 6a21e83b6cde088d7520dbcd559425ccfd0cdafb Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Fri, 22 Sep 2017 16:16:12 +0200
Subject: [PATCH] Added length of disjoint sum

---
 FiniteSets/kuratowski/length.v     |  62 +++++++++++
 FiniteSets/kuratowski/operations.v |  11 +-
 FiniteSets/kuratowski/properties.v | 165 ++++++++++++++++++-----------
 FiniteSets/prelude.v               |  94 +++++++++++-----
 4 files changed, 240 insertions(+), 92 deletions(-)

diff --git a/FiniteSets/kuratowski/length.v b/FiniteSets/kuratowski/length.v
index 9eaa6e4..df9061d 100644
--- a/FiniteSets/kuratowski/length.v
+++ b/FiniteSets/kuratowski/length.v
@@ -228,3 +228,65 @@ Section length_product.
         reflexivity.
   Defined.
 End length_product.
+
+Section length_sum.
+  Context `{Univalence}.
+  Lemma length_fmap_inj
+        {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}
+        (X : FSet A) (f : A -> B) `{IsEmbedding f}
+    : length (fset_fmap f X) = length X.
+  Proof.
+    simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _ X)
+    ; try (intros ; apply path_ishprop) ; simpl.
+    - reflexivity.
+    - intros a Y HX.
+      rewrite ?length_compute, HX, (fmap_isIn_d_inj _ f)
+      ; auto.
+  Defined.
+
+  Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}.
+
+  Lemma fmap_inl X a : (inl a) ∈_d (fset_fmap (@inr A B) X) = false.
+  Proof.
+    hinduction X ; try (intros ; apply path_ishprop).
+    - reflexivity.
+    - intros b.
+      rewrite singleton_isIn_d_false.
+      * reflexivity.
+      * apply inl_ne_inr.
+    - intros X1 X2 HX1 HX2.
+      rewrite union_isIn_d, HX1, HX2.
+      reflexivity.
+  Defined.
+  
+  Lemma fmap_inr X a : (inr a) ∈_d (fset_fmap (@inl A B) X) = false.
+  Proof.
+    hinduction X ; try (intros ; apply path_ishprop).
+    - reflexivity.
+    - intros b.
+      rewrite singleton_isIn_d_false.
+      * reflexivity.
+      * apply inr_ne_inl.
+    - intros X1 X2 HX1 HX2.
+      rewrite union_isIn_d, HX1, HX2.
+      reflexivity.
+  Defined.
+  
+  Lemma disjoint_summants X Y : disjoint (fset_fmap (@inl A B) X) (fset_fmap inr Y).
+  Proof.
+    apply ext.
+    intros [x1 | x2] ; rewrite empty_isIn_d, intersection_isIn_d, ?fmap_inl, ?fmap_inr
+    ; simpl ; try reflexivity.
+    destruct ((inl x1) ∈_d (fset_fmap inl X)) ; reflexivity.
+  Defined.
+
+  Open Scope nat.
+  
+  Theorem length_disjoint_sum (X : FSet A) (Y : FSet B)
+    : length (disjoint_sum X Y) = length X + length Y.
+  Proof.
+    rewrite (length_disjoint _ _ (disjoint_summants _ _)).
+    rewrite ?(length_fmap_inj _ _).
+    reflexivity.
+  Defined.
+End length_sum.
\ No newline at end of file
diff --git a/FiniteSets/kuratowski/operations.v b/FiniteSets/kuratowski/operations.v
index 7f4ced7..7361e29 100644
--- a/FiniteSets/kuratowski/operations.v
+++ b/FiniteSets/kuratowski/operations.v
@@ -180,11 +180,12 @@ Section operations_decidable.
     - apply _. 
   Defined.
 
-  Global Instance fset_member_bool : hasMembership_decidable (FSet A) A.
-  Proof.
-    intros a X.
-    refine (if (dec a ∈ X) then true else false).
-  Defined.
+  Global Instance fset_member_bool : hasMembership_decidable (FSet A) A :=
+    fun a X =>
+      match (dec a ∈ X) with
+      | inl _ => true
+      | inr _ => false
+      end.
 
   Global Instance subset_decidable : forall (X Y : FSet A), Decidable (X ⊆ Y).
   Proof.
diff --git a/FiniteSets/kuratowski/properties.v b/FiniteSets/kuratowski/properties.v
index d6e4b9b..878382e 100644
--- a/FiniteSets/kuratowski/properties.v
+++ b/FiniteSets/kuratowski/properties.v
@@ -2,6 +2,69 @@ Require Import HoTT HitTactics prelude.
 Require Import kuratowski.extensionality kuratowski.operations kuratowski_sets.
 Require Import lattice_interface lattice_examples monad_interface.
 
+(** [FSet] is a (strong and stable) finite powerset monad *)
+Section monad_fset.
+  Context `{Funext}.
+
+  Global Instance fset_functorish : Functorish FSet.
+  Proof.
+    simple refine (Build_Functorish _ _ _).
+    - intros ? ? f.
+      apply (fset_fmap f).
+    - intros A.
+      apply path_forall.
+      intro x.
+      hinduction x
+      ; try (intros ; f_ap)
+      ; try (intros ; apply path_ishprop).
+  Defined.
+
+  Global Instance fset_functor : Functor FSet.
+  Proof.
+    split.
+    intros.
+    apply path_forall.
+    intro x.
+    hrecursion x
+    ; try (intros ; f_ap)
+    ; try (intros ; apply path_ishprop).
+  Defined.
+
+  Global Instance fset_monad : Monad FSet.
+  Proof.
+    split.
+    - intros.
+      apply path_forall.
+      intro X.
+      hrecursion X ; try (intros; f_ap) ;
+        try (intros; apply path_ishprop).
+    - intros.
+      apply path_forall.
+      intro X.
+      hrecursion X ; try (intros; f_ap) ;
+        try (intros; apply path_ishprop).
+    - intros.
+      apply path_forall.
+      intro X.
+      hrecursion X ; try (intros; f_ap) ;
+        try (intros; apply path_ishprop).
+  Defined.
+
+  Lemma fmap_isIn `{Univalence} {A B : Type} (f : A -> B) (a : A) (X : FSet A) :
+    a ∈ X -> (f a) ∈ (fmap FSet f X).
+  Proof.
+    hinduction X; try (intros; apply path_ishprop).
+    - apply idmap.
+    - intros b Hab; strip_truncations.
+      apply (tr (ap f Hab)).
+    - intros X0 X1 HX0 HX1 Ha.
+      strip_truncations. apply tr.
+      destruct Ha as [Ha | Ha].
+      + left. by apply HX0.
+      + right. by apply HX1.
+  Defined.
+End monad_fset.
+
 (** Lemmas relating operations to the membership predicate *)
 Section properties_membership.
   Context {A : Type} `{Univalence}.
@@ -206,6 +269,31 @@ Section properties_membership.
            repeat f_ap.
            apply path_ishprop.
   Defined.
+
+  Lemma fmap_isIn_inj (f : A -> B) (a : A) (X : FSet A) {f_inj : IsEmbedding f} :
+    a ∈ X = (f a) ∈ (fmap FSet f X).
+  Proof.
+    hinduction X; try (intros; apply path_ishprop).
+    - reflexivity.
+    - intros b.
+      apply path_iff_hprop.
+      * intros Ha.
+        strip_truncations.
+        apply (tr (ap f Ha)).
+      * intros Hfa.
+        strip_truncations.
+        apply tr.
+        unfold IsEmbedding, hfiber in *.
+        specialize (f_inj (f a)).
+        pose ((a;idpath (f a)) : {x : A & f x = f a}) as p1.
+        pose ((b;Hfa^) : {x : A & f x = f a}) as p2.
+        assert (p1 = p2) as Hp1p2.
+        { apply f_inj. }
+        apply (ap (fun x => x.1) Hp1p2).
+    - intros X0 X1 HX0 HX1.
+      rewrite ?union_isIn, HX0, HX1.
+      reflexivity.
+  Defined.
 End properties_membership.
 
 Ltac simplify_isIn :=
@@ -325,6 +413,20 @@ Section properties_membership_decidable.
   Proof.
     apply comprehension_isIn_d.
   Defined.  
+
+  Context (B : Type) `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}.
+
+  Lemma fmap_isIn_d_inj (f : A -> B) (a : A) (X : FSet A) {f_inj : IsEmbedding f} :
+    a ∈_d X = (f a) ∈_d (fmap FSet f X).
+  Proof.
+    unfold member_dec, fset_member_bool, dec.
+    destruct (isIn_decidable a X) as [t | t], (isIn_decidable (f a) (fmap FSet f X)) as [n | n]
+    ; try reflexivity.
+    - rewrite <- fmap_isIn_inj in n ; try (apply _).
+      contradiction (n t).
+    - rewrite <- fmap_isIn_inj in n ; try (apply _).
+      contradiction (t n).
+  Defined.
   
   Lemma singleton_isIn_d `{IsHSet A} (a b : A) :
     a ∈ {|b|} -> a = b.
@@ -436,69 +538,6 @@ Section dec_eq.
   Defined.
 End dec_eq.
 
-(** [FSet] is a (strong and stable) finite powerset monad *)
-Section monad_fset.
-  Context `{Funext}.
-
-  Global Instance fset_functorish : Functorish FSet.
-  Proof.
-    simple refine (Build_Functorish _ _ _).
-    - intros ? ? f.
-      apply (fset_fmap f).
-    - intros A.
-      apply path_forall.
-      intro x.
-      hinduction x
-      ; try (intros ; f_ap)
-      ; try (intros ; apply path_ishprop).
-  Defined.
-
-  Global Instance fset_functor : Functor FSet.
-  Proof.
-    split.
-    intros.
-    apply path_forall.
-    intro x.
-    hrecursion x
-    ; try (intros ; f_ap)
-    ; try (intros ; apply path_ishprop).
-  Defined.
-
-  Global Instance fset_monad : Monad FSet.
-  Proof.
-    split.
-    - intros.
-      apply path_forall.
-      intro X.
-      hrecursion X ; try (intros; f_ap) ;
-        try (intros; apply path_ishprop).
-    - intros.
-      apply path_forall.
-      intro X.
-      hrecursion X ; try (intros; f_ap) ;
-        try (intros; apply path_ishprop).
-    - intros.
-      apply path_forall.
-      intro X.
-      hrecursion X ; try (intros; f_ap) ;
-        try (intros; apply path_ishprop).
-  Defined.
-
-  Lemma fmap_isIn `{Univalence} {A B : Type} (f : A -> B) (a : A) (X : FSet A) :
-    a ∈ X -> (f a) ∈ (fmap FSet f X).
-  Proof.
-    hinduction X; try (intros; apply path_ishprop).
-    - apply idmap.
-    - intros b Hab; strip_truncations.
-      apply (tr (ap f Hab)).
-    - intros X0 X1 HX0 HX1 Ha.
-      strip_truncations. apply tr.
-      destruct Ha as [Ha | Ha].
-      + left. by apply HX0.
-      + right. by apply HX1.
-  Defined.
-End monad_fset.
-
 (** comprehension properties *)
 Section comprehension_properties.
   Context {A : Type} `{Univalence}.
diff --git a/FiniteSets/prelude.v b/FiniteSets/prelude.v
index 5fcbd39..6ec4b46 100644
--- a/FiniteSets/prelude.v
+++ b/FiniteSets/prelude.v
@@ -24,6 +24,22 @@ Proof.
   - apply equiv_hprop_allpath. apply _.
 Defined.
 
+Global Instance inl_embedding (A B : Type) : IsEmbedding (@inl A B).
+Proof.
+  - intros [x1 | x2].
+    * apply ishprop_hfiber_inl.
+    * intros [z p].
+      contradiction (inl_ne_inr _ _ p).
+Defined.
+
+Global Instance inr_embedding (A B : Type) : IsEmbedding (@inr A B).
+Proof.
+  - intros [x1 | x2].
+    * intros [z p].
+      contradiction (inr_ne_inl _ _ p).
+    * apply ishprop_hfiber_inr.
+Defined.
+
 Class MerelyDecidablePaths A :=
   m_dec_path : forall (a b : A), Decidable(Trunc (-1) (a = b)).
 
@@ -37,27 +53,57 @@ Proof.
     apply (n p).
 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.  
+Section merely_decidable_operations.
+  Variable (A B : Type).
+  Context `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}.
+  
+  Global Instance merely_decidable_paths_prod : 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.  
+
+  Global Instance merely_decidable_sum : MerelyDecidablePaths (A + B).
+  Proof.
+    intros [x1 | x2] [y1 | y2].
+    - destruct (m_dec_path x1 y1) as [t | n].
+      * apply inl.
+        strip_truncations.
+        apply (tr(ap inl t)).
+      * refine (inr(fun p => _)).
+        strip_truncations.
+        refine (n(tr _)).
+        refine (path_sum_inl _ p).
+    - refine (inr(fun p => _)).
+      strip_truncations.
+      refine (inl_ne_inr x1 y2 p).
+    - refine (inr(fun p => _)).
+      strip_truncations.
+      refine (inr_ne_inl x2 y1 p).
+    - destruct (m_dec_path x2 y2) as [t | n].
+      * apply inl.
+        strip_truncations.
+        apply (tr(ap inr t)).
+      * refine (inr(fun p => _)).
+        strip_truncations.
+        refine (n(tr _)).
+        refine (path_sum_inr _ p).
+  Defined.
+End merely_decidable_operations.
\ No newline at end of file