Uses merely decidable equality, added length.

FiniteSets/kuratowski/extensionality.v

@@ -2,6 +2,10 @@
 Require Import HoTT HitTactics.
 Require Import kuratowski.kuratowski_sets.
 
+(** We prove extensionality via a chain of equivalences.
+    We end with proving that equality can be defined with the subset relation.
+    From that we can conclude that [FSet A] has decidable equality if [A] has.
+*)
 Section ext.
   Context {A : Type}.
   Context `{Univalence}.

FiniteSets/kuratowski/kuratowski_sets.v

@@ -1,4 +1,6 @@
-(** Definitions of the Kuratowski-finite sets via a HIT *)
+(** Definitions of the Kuratowski-finite sets via a HIT.
+    We do not need the computation rules in the development, so they are not present here.
+*)
 Require Import HoTT HitTactics.
 Require Export set_names lattice_examples.
 

FiniteSets/kuratowski/length.v

@@ -0,0 +1,26 @@
+Require Import HoTT HitTactics.
+Require Import kuratowski.operations kuratowski.properties kuratowski.kuratowski_sets.
+
+Section Length.
+  Context {A : Type} `{DecidablePaths A} `{Univalence}.
+  
+  Definition length : FSet A -> nat.
+    simple refine (FSet_cons_rec _ _ _ _ _ _).
+    - apply 0.
+    - intros a X n.
+      apply (if a ∈_d X then n else (S n)).
+    - intros X a n.
+      simpl.
+      simplify_isIn_d.
+      destruct (dec (a ∈ X)) ; reflexivity.
+    - intros X a b n.
+      simpl.
+      simplify_isIn_d.
+      destruct (dec (a = b)) as [Hab | Hab].
+      + rewrite Hab. simplify_isIn_d. reflexivity.
+      + rewrite ?singleton_isIn_d_false; auto.
+        ++ simpl. 
+           destruct (a ∈_d X), (b ∈_d X) ; reflexivity.
+        ++ intro p. contradiction (Hab p^).
+  Defined.
+End Length.

FiniteSets/kuratowski/operations.v

@@ -1,6 +1,7 @@
 (** Operations on the [FSet A] for an arbitrary [A] *)
-Require Import HoTT HitTactics.
-Require Import kuratowski_sets monad_interface extensionality.
+Require Import HoTT HitTactics prelude.
+Require Import kuratowski_sets monad_interface extensionality
+        list_representation.isomorphism list_representation.list_representation.
 
 Section operations.
   (** Monad operations. *)
@@ -167,7 +168,7 @@ End operations.
 
 Section operations_decidable.
   Context {A : Type}.
-  Context {A_deceq : DecidablePaths A}.
+  Context `{MerelyDecidablePaths A}.
   Context `{Univalence}.
 
   Global Instance isIn_decidable (a : A) : forall (X : FSet A),
@@ -175,12 +176,7 @@ Section operations_decidable.
   Proof.
     hinduction ; try (intros ; apply path_ishprop).
     - apply _.
-    - intros b.
-      destruct (dec (a = b)) as [p | np].
-      * apply (inl (tr p)).
-      * refine (inr(fun p => _)).
-        strip_truncations.
-        contradiction.
+    - apply (m_dec_path _).
     - apply _. 
   Defined.
 
@@ -207,4 +203,35 @@ Section operations_decidable.
 
   Global Instance fset_intersection : hasIntersection (FSet A)
     := fun X Y => {|X & (fun a => a ∈_d Y)|}.
-End operations_decidable.
+End operations_decidable.
+
+Section FSet_cons_rec.
+  Context `{A : Type}.
+  
+  Variable (P : Type)
+           (Pset : IsHSet P)
+           (Pe : P)
+           (Pcons : A -> FSet A -> P -> P)
+           (Pdupl : forall X a p, Pcons a ({|a|} ∪ X) (Pcons a X p) = Pcons a X p)
+           (Pcomm : forall X a b p, Pcons a ({|b|} ∪ X) (Pcons b X p)
+                                           = Pcons b ({|a|} ∪ X) (Pcons a X p)).
+  
+  Definition FSet_cons_rec (X : FSet A) : P.
+  Proof.
+    simple refine (FSetC_ind A (fun _ => P) _ Pe _ _ _ (FSet_to_FSetC X)) ; simpl.
+    - intros a Y p.
+      apply (Pcons a (FSetC_to_FSet Y) p).
+    - intros.
+      refine (transport_const _ _ @ _).
+      apply Pdupl.
+    - intros.
+      refine (transport_const _ _ @ _).
+      apply Pcomm.
+  Defined.
+
+  Definition FSet_cons_beta_empty : FSet_cons_rec ∅ = Pe := idpath.
+  
+  Definition FSet_cons_beta_cons (a : A) (X : FSet A)
+    : FSet_cons_rec ({|a|} ∪ X) = Pcons a X (FSet_cons_rec X)
+    := ap (fun z => Pcons a z _) (repr_iso_id_l _).
+End FSet_cons_rec.

FiniteSets/kuratowski/properties.v

@@ -1,4 +1,4 @@
-Require Import HoTT HitTactics.
+Require Import HoTT HitTactics prelude.
 Require Import kuratowski.extensionality kuratowski.operations kuratowski_sets.
 Require Import lattice_interface lattice_examples monad_interface.
 
@@ -251,7 +251,7 @@ End fset_join_semilattice.
 
 (* Lemmas relating operations to the membership predicate *)
 Section properties_membership_decidable.
-  Context {A : Type} `{DecidablePaths A} `{Univalence}.
+  Context {A : Type} `{MerelyDecidablePaths A} `{Univalence}.
 
   Lemma ext : forall (S T : FSet A), (forall a, a ∈_d S = a ∈_d T) -> S = T.
   Proof.
@@ -267,17 +267,7 @@ Section properties_membership_decidable.
     - apply path_iff_hprop ; intro ; contradiction.
   Defined.
 
-  Lemma empty_isIn_d (a : A) :
-    a ∈_d ∅ = false.
-  Proof.
-    reflexivity.
-  Defined.
-
-  Lemma singleton_isIn_d (a b : A) :
-    a ∈ {|b|} -> a = b.
-  Proof.
-    intros. strip_truncations. assumption.
-  Defined.
+  Definition empty_isIn_d (a : A) : a ∈_d ∅ = false := idpath.
 
   Lemma singleton_isIn_d_true (a b : A) (p : a = b) :
     a ∈_d {|b|} = true.
@@ -329,6 +319,14 @@ Section properties_membership_decidable.
   Proof.
     apply comprehension_isIn_d.
   Defined.
+  
+  Lemma singleton_isIn_d `{DecidablePaths A} (a b : A) :
+    a ∈ {|b|} -> a = b.
+  Proof.
+    intros.
+    strip_truncations.
+    assumption.
+  Defined.
 End properties_membership_decidable.
 
 (* Some suporting tactics *)
@@ -346,7 +344,7 @@ Ltac toBool :=
 (** If `A` has decidable equality, then `FSet A` is a lattice *) 
 Section set_lattice.
   Context {A : Type}.
-  Context {A_deceq : DecidablePaths A}.
+  Context `{MerelyDecidablePaths A}.
   Context `{Univalence}.
 
   Instance fset_max : maximum (FSet A).