From 6c86d0c524562622288dd5fb85b645c6876f19b5 Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Thu, 7 Sep 2017 15:44:22 +0200
Subject: [PATCH] Fixes

---
 FiniteSets/FSets.v                           |   7 +-
 FiniteSets/_CoqProject                       |  49 +++----
 FiniteSets/kuratowski/monad.v                |  84 -----------
 FiniteSets/kuratowski/operations_decidable.v |  54 -------
 FiniteSets/kuratowski/properties_decidable.v | 145 -------------------
 FiniteSets/misc/{T.v => dec_lem.v}           |   0
 FiniteSets/{ => misc}/empty_set.v            |   0
 FiniteSets/misc/projective.v                 |   2 +-
 FiniteSets/subobjects/{Sub.v => sub.v}       |   2 +-
 9 files changed, 25 insertions(+), 318 deletions(-)
 delete mode 100644 FiniteSets/kuratowski/monad.v
 delete mode 100644 FiniteSets/kuratowski/operations_decidable.v
 delete mode 100644 FiniteSets/kuratowski/properties_decidable.v
 rename FiniteSets/misc/{T.v => dec_lem.v} (100%)
 rename FiniteSets/{ => misc}/empty_set.v (100%)
 rename FiniteSets/subobjects/{Sub.v => sub.v} (96%)

diff --git a/FiniteSets/FSets.v b/FiniteSets/FSets.v
index 8b1d63c..c7d000a 100644
--- a/FiniteSets/FSets.v
+++ b/FiniteSets/FSets.v
@@ -1,7 +1,2 @@
 Require Export HoTT HitTactics.
-Require Export representations.definition.
-From fsets Require Export
-     monad
-     extensionality
-     properties
-     properties_decidable.
\ No newline at end of file
+Require Export kuratowski_sets kuratowski.operations kuratowski.properties extensionality.
\ No newline at end of file
diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index c862751..69eefc2 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -1,30 +1,25 @@
 -R . "" COQC = hoqc COQDEP = hoqdep
 -R ../prelude ""
-notation.v
-plumbing.v
-lattice.v
-disjunction.v
-representations/bad.v
-representations/definition.v
-representations/cons_repr.v
-fsets/operations_cons_repr.v
-fsets/properties_cons_repr.v
-fsets/isomorphism.v
-fsets/operations.v
-fsets/operations_decidable.v
-fsets/extensionality.v
-fsets/properties.v
-fsets/properties_decidable.v
-fsets/length.v
-fsets/monad.v
+prelude.v
+interfaces/lattice_interface.v
+interfaces/lattice_examples.v
+interfaces/monad_interface.v
+interfaces/set_names.v
+kuratowski/kuratowski_sets.v
+kuratowski/extensionality.v
+list_representation/list_representation.v
+list_representation/operations.v
+list_representation/properties.v
+list_representation/isomorphism.v
+kuratowski/operations.v
+kuratowski/properties.v
 FSets.v
-Sub.v
-representations/T.v
-implementations/interface.v
-implementations/lists.v
-variations/enumerated.v
-variations/k_finite.v
-variations/b_finite.v
-variations/projective.v
-#empty_set.v
-ordered.v
+interfaces/set_interface.v
+subobjects/sub.v
+subobjects/k_finite.v
+subobjects/enumerated.v
+subobjects/b_finite.v
+misc/bad.v
+misc/dec_lem.v
+misc/ordered.v
+misc/projective.v
\ No newline at end of file
diff --git a/FiniteSets/kuratowski/monad.v b/FiniteSets/kuratowski/monad.v
deleted file mode 100644
index c0861a4..0000000
--- a/FiniteSets/kuratowski/monad.v
+++ /dev/null
@@ -1,84 +0,0 @@
-(* [FSet] is a (strong and stable) finite powerset monad *)
-Require Import HoTT HitTactics.
-Require Export representations.definition fsets.properties fsets.operations.
-
-Definition ffmap {A B : Type} : (A -> B) -> FSet A -> FSet B.
-Proof.
-  intro f.
-  hrecursion.
-  - exact ∅.
-  - intro a. exact {| f a |}.
-  - intros X Y. apply (X ∪ Y).
-  - apply assoc.
-  - apply comm.
-  - apply nl.
-  - apply nr.
-  - simpl. intro x. apply idem.
-Defined.
-
-Lemma ffmap_1 `{Funext} {A : Type} : @ffmap A A idmap = idmap.
-Proof.
-  apply path_forall.
-  intro x. hinduction x; try (intros; f_ap);
-             try (intros; apply set_path2).
-Defined.
-
-Global Instance fset_functorish `{Funext}: Functorish FSet
-  := { fmap := @ffmap; fmap_idmap := @ffmap_1 _ }.
-
-Lemma ffmap_compose {A B C : Type} `{Funext} (f : A -> B) (g : B -> C) :
-  fmap FSet (g o f) = fmap _ g o fmap _ f.
-Proof.
-  apply path_forall. intro x.
-  hrecursion x; try (intros; f_ap);
-    try (intros; apply set_path2).
-Defined.
-
-Definition join {A : Type} : FSet (FSet A) -> FSet A.
-Proof.
-hrecursion.
-- exact ∅.
-- exact idmap.
-- intros X Y. apply (X ∪ Y).
-- apply assoc.
-- apply comm.
-- apply nl.
-- apply nr.
-- simpl. apply union_idem.
-Defined.
-
-Lemma join_assoc {A : Type} (X : FSet (FSet (FSet A))) :
-  join (ffmap join X) = join (join X).
-Proof.
-  hrecursion X; try (intros; f_ap);
-    try (intros; apply set_path2).
-Defined.
-
-Lemma join_return_1 {A : Type} (X : FSet A) :
-  join ({| X |}) = X.
-Proof. reflexivity. Defined.
-
-Lemma join_return_fmap {A : Type} (X : FSet A) :
-  join ({| X |}) = join (ffmap (fun x => {|x|}) X).
-Proof.
-  hrecursion X; try (intros; f_ap);
-    try (intros; apply set_path2).
-Defined.
-
-Lemma join_fmap_return_1 {A : Type} (X : FSet A) :
-  join (ffmap (fun x => {|x|}) X) = X.
-Proof. refine ((join_return_fmap _)^ @ join_return_1 _). Defined.
-
-Lemma fmap_isIn `{Univalence} {A B : Type} (f : A -> B) (a : A) (X : FSet A) :
-  a ∈ X -> (f a) ∈ (ffmap 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.
diff --git a/FiniteSets/kuratowski/operations_decidable.v b/FiniteSets/kuratowski/operations_decidable.v
deleted file mode 100644
index dca5b9e..0000000
--- a/FiniteSets/kuratowski/operations_decidable.v
+++ /dev/null
@@ -1,54 +0,0 @@
-(* Operations on [FSet A] when [A] has decidable equality *)
-Require Import HoTT HitTactics.
-Require Export representations.definition fsets.operations.
-
-Section decidable_A.
-  Context {A : Type}.
-  Context {A_deceq : DecidablePaths A}.
-  Context `{Univalence}.
-  
-  Global Instance isIn_decidable : forall (a : A) (X : FSet A),
-      Decidable (a ∈ X).
-  Proof.
-    intros a.
-    hinduction ; try (intros ; apply path_ishprop).
-    - apply _.
-    - intros.
-      unfold Decidable.
-      destruct (dec (a = a0)) as [p | np].
-      * apply (inl (tr p)).
-      * right.
-        intro p.
-        strip_truncations.
-        contradiction.
-    - intros. apply _. 
-  Defined.
-
-  Global Instance fset_member_bool : hasMembership_decidable (FSet A) A.
-  Proof.
-    intros a X.
-    destruct (dec (a ∈ X)).
-    - apply true.
-    - apply false.
-  Defined.
-
-  Global Instance subset_decidable : forall (X Y : FSet A), Decidable (X ⊆ Y).
-  Proof.
-    hinduction ; try (intros ; apply path_ishprop).
-    - intro ; apply _.
-    - intros ; apply _. 
-    - intros. unfold subset in *. apply _.
-  Defined.
-
-  Global Instance fset_subset_bool : hasSubset_decidable (FSet A).
-  Proof.
-    intros X Y.
-    destruct (dec (X ⊆ Y)).
-    - apply true.
-    - apply false.
-  Defined.
-
-  Global Instance fset_intersection : hasIntersection (FSet A)
-    := fun X Y => {|X & (fun a => a ∈_d Y)|}. 
-
-End decidable_A.
\ No newline at end of file
diff --git a/FiniteSets/kuratowski/properties_decidable.v b/FiniteSets/kuratowski/properties_decidable.v
deleted file mode 100644
index e4b3518..0000000
--- a/FiniteSets/kuratowski/properties_decidable.v
+++ /dev/null
@@ -1,145 +0,0 @@
-(* Properties of [FSet A] where [A] has decidable equality *)
-Require Import HoTT HitTactics.
-From fsets Require Export properties extensionality operations_decidable.
-Require Export lattice.
-
-(* Lemmas relating operations to the membership predicate *)
-Section operations_isIn.
-
-  Context {A : Type} `{DecidablePaths A} `{Univalence}.
-
-  Lemma ext : forall (S T : FSet A), (forall a, a ∈_d S = a ∈_d T) -> S = T.
-  Proof.
-    intros X Y H2.
-    apply fset_ext.
-    intro a.
-    specialize (H2 a).
-    unfold member_dec, fset_member_bool, dec in H2.
-    destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y).
-    - apply path_iff_hprop ; intro ; assumption.
-    - contradiction (true_ne_false).
-    - contradiction (true_ne_false) ; apply H2^.
-    - apply path_iff_hprop ; intro ; contradiction.
-  Defined.
-
-  Lemma empty_isIn (a : A) :
-    a ∈_d ∅ = false.
-  Proof.
-    reflexivity.
-  Defined.
-
-  Lemma L_isIn (a b : A) :
-    a ∈ {|b|} -> a = b.
-  Proof.
-    intros. strip_truncations. assumption.
-  Defined.
-
-  Lemma L_isIn_b_true (a b : A) (p : a = b) :
-    a ∈_d {|b|} = true.
-  Proof.
-    unfold member_dec, fset_member_bool, dec.
-    destruct (isIn_decidable a {|b|}) as [n | n] .
-    - reflexivity.
-    - simpl in n.
-      contradiction (n (tr p)).
-  Defined.
-
-  Lemma L_isIn_b_aa (a : A) :
-    a ∈_d {|a|} = true.
-  Proof.
-    apply L_isIn_b_true ; reflexivity.
-  Defined.
-
-  Lemma L_isIn_b_false (a b : A) (p : a <> b) :
-    a ∈_d {|b|} = false.
-  Proof.
-    unfold member_dec, fset_member_bool, dec in *.
-    destruct (isIn_decidable a {|b|}).
-    - simpl in t.
-      strip_truncations.
-      contradiction.
-    - reflexivity.
-  Defined.
-
-  (* Union and membership *)
-  Lemma union_isIn_b (X Y : FSet A) (a : A) :
-    a ∈_d (X ∪ Y) = orb (a ∈_d X) (a ∈_d Y).
-  Proof.
-    unfold member_dec, fset_member_bool, dec.
-    simpl.
-    destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y) ; reflexivity.
-  Defined.
-
-  Lemma comprehension_isIn_b (Y : FSet A) (ϕ : A -> Bool) (a : A) :
-    a ∈_d {|Y & ϕ|} = andb (a ∈_d Y) (ϕ a).
-  Proof.
-    unfold member_dec, fset_member_bool, dec ; simpl.
-    destruct (isIn_decidable a {|Y & ϕ|}) as [t | t]
-    ; destruct (isIn_decidable a Y) as [n | n] ; rewrite comprehension_isIn in t
-    ; destruct (ϕ a) ; try reflexivity ; try contradiction
-    ; try (contradiction (n t)) ; contradiction (t n).
-  Defined.
-
-  Lemma intersection_isIn_b (X Y: FSet A) (a : A) :
-    a ∈_d (intersection X Y) = andb (a ∈_d X) (a ∈_d Y).
-  Proof.
-    apply comprehension_isIn_b.
-  Defined.
-
-End operations_isIn.
-
-(* Some suporting tactics *)
-Ltac simplify_isIn_b :=
-  repeat (rewrite union_isIn_b
-        || rewrite L_isIn_b_aa
-        || rewrite intersection_isIn_b
-        || rewrite comprehension_isIn_b).
-
-Ltac toBool :=
-  repeat intro;
-  apply ext ; intros ;
-  simplify_isIn_b ; eauto with bool_lattice_hints typeclass_instances.
-
-Section SetLattice.
-
-  Context {A : Type}.
-  Context {A_deceq : DecidablePaths A}.
-  Context `{Univalence}.
-
-  Instance fset_max : maximum (FSet A).
-  Proof.
-    intros x y.
-    apply (x ∪ y).
-  Defined.
-
-  Instance fset_min : minimum (FSet A).
-  Proof.
-    intros x y.
-    apply (x ∩ y).
-  Defined.
-
-  Instance fset_bot : bottom (FSet A).
-  Proof.
-    unfold bottom.
-    apply ∅.
-  Defined.
-
-  Instance lattice_fset : Lattice (FSet A).
-  Proof.
-    split; toBool.
-  Defined.
-
-End SetLattice.
-
-(* With extensionality we can prove decidable equality *)
-Section dec_eq.
-  Context (A : Type) `{DecidablePaths A} `{Univalence}.
-
-  Instance fsets_dec_eq : DecidablePaths (FSet A).
-  Proof.
-    intros X Y.
-    apply (decidable_equiv' ((Y ⊆ X) * (X ⊆ Y)) (eq_subset X Y)^-1).
-    apply decidable_prod.
-  Defined.
-
-End dec_eq.
diff --git a/FiniteSets/misc/T.v b/FiniteSets/misc/dec_lem.v
similarity index 100%
rename from FiniteSets/misc/T.v
rename to FiniteSets/misc/dec_lem.v
diff --git a/FiniteSets/empty_set.v b/FiniteSets/misc/empty_set.v
similarity index 100%
rename from FiniteSets/empty_set.v
rename to FiniteSets/misc/empty_set.v
diff --git a/FiniteSets/misc/projective.v b/FiniteSets/misc/projective.v
index 17999d9..5391361 100644
--- a/FiniteSets/misc/projective.v
+++ b/FiniteSets/misc/projective.v
@@ -1,6 +1,6 @@
 Require Import HoTT HitTactics.
 Require Import subobjects.k_finite subobjects.b_finite FSets.
-Require Import misc.T.
+Require Import misc.dec_lem.
 
 Class IsProjective (X : Type) :=
   projective : forall {P Q : Type} (p : P -> Q) (f : X -> Q),
diff --git a/FiniteSets/subobjects/Sub.v b/FiniteSets/subobjects/sub.v
similarity index 96%
rename from FiniteSets/subobjects/Sub.v
rename to FiniteSets/subobjects/sub.v
index c771fd7..3eca93a 100644
--- a/FiniteSets/subobjects/Sub.v
+++ b/FiniteSets/subobjects/sub.v
@@ -1,5 +1,5 @@
 Require Import HoTT.
-Require Import disjunction lattice notation plumbing.
+Require Import set_names lattice_interface lattice_examples prelude.
 
 Section subobjects.
   Variable A : Type.