A cons-based induction principle for FSets

FiniteSets/fsets/isomorphism.v

@@ -8,6 +8,12 @@ Section Iso.
   Context {A : Type}.
   Context `{Univalence}.
 
+  Definition dupl' (a : A) (X : FSet A) :
+    {|a|} ∪ {|a|} ∪ X = {|a|} ∪ X := assoc _ _ _ @ ap (∪ X) (idem _).
+  Definition comm' (a b : A) (X : FSet A) :
+    {|a|} ∪ {|b|} ∪ X = {|b|} ∪ {|a|} ∪ X :=
+    assoc _ _ _ @ ap (∪ X) (comm _ _) @ (assoc _ _ _)^.
+
   Definition FSetC_to_FSet: FSetC A -> FSet A.
   Proof.
     hrecursion.
@@ -15,15 +21,9 @@ Section Iso.
     - intros a x.
       apply ({|a|} ∪ x).
     - intros. cbn.
-      etransitivity. apply assoc.
+      apply dupl'.
-      apply (ap (∪ x)).
-      apply idem.
     - intros. cbn.
-      etransitivity. apply assoc.
+      apply comm'.
-      etransitivity. refine (ap (∪ x) _ ).
-      apply FSet.comm.
-      symmetry.
-      apply assoc.
   Defined.
 
   Definition FSet_to_FSetC: FSet A -> FSetC A.
@@ -45,7 +45,9 @@ Section Iso.
     intros x.
     hrecursion x; try (intros; apply path_forall; intro; apply set_path2).
     - intros. symmetry. apply nl.
-    - intros a x HR y. unfold union, fsetc_union in *. rewrite HR. apply assoc.
+    - intros a x HR y. unfold union, fsetc_union in *.
+      refine (_ @ assoc _ _ _).
+      apply (ap ({|a|} ∪) (HR _)).
   Defined.
 
   Lemma repr_iso_id_l: forall (x: FSet A), FSetC_to_FSet (FSet_to_FSetC x) = x.
@@ -53,7 +55,10 @@ Section Iso.
     hinduction; try (intros; apply set_path2).
     - reflexivity.
     - intro. apply nr.
-    - intros x y p q. rewrite append_union, p, q. reflexivity.
+    - intros x y p q.
+      refine (append_union _ _ @ _).
+      refine (ap (∪ _) p @ _).
+      apply (ap (_ ∪) q).
   Defined.
 
   Lemma repr_iso_id_r: forall (x: FSetC A), FSet_to_FSetC (FSetC_to_FSet x) = x.
@@ -89,4 +94,66 @@ Section Iso.
     apply (equiv_path _ _)^-1.
     exact repr_iso.
   Defined.
+
+  Theorem FSet_cons_ind (P : FSet A -> Type)
+    (Pset : forall (X : FSet A), IsHSet (P X))
+    (Pempt : P ∅)
+    (Pcons : forall (a : A) (X : FSet A), P X -> P ({|a|} ∪ X))
+    (Pdupl : forall (a : A) (X : FSet A) (px : P X),
+       transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px)
+    (Pcomm : forall (a b : A) (X : FSet A) (px : P X),
+       transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) :
+    forall X, P X.
+  Proof.
+    intros X.
+    refine (transport P (repr_iso_id_l X) _).
+    simple refine (FSetC_ind A (fun Z => P (FSetC_to_FSet Z)) _ _ _ _ _ (FSet_to_FSetC X)); simpl.
+    - apply Pempt.
+    - intros a Y HY. by apply Pcons.
+    - intros a Y PY. cbn.
+      refine (_ @ (Pdupl _ _ _)).
+      etransitivity.
+      { apply (transport_compose _ FSetC_to_FSet (dupl a Y)). }
+      refine (ap (fun z => transport P z _) _).
+      apply FSetC_rec_beta_dupl.
+    - intros a b Y PY. cbn.
+      refine (_ @ (Pcomm _ _ _ _)).
+      etransitivity.
+      { apply (transport_compose _ FSetC_to_FSet (FSetC.comm a b Y)). }
+      refine (ap (fun z => transport P z _) _).
+      apply FSetC_rec_beta_comm.
+  Defined.
+
+  Theorem FSet_cons_ind_beta_empty (P : FSet A -> Type)
+    (Pset : forall (X : FSet A), IsHSet (P X))
+    (Pempt : P ∅)
+    (Pcons : forall (a : A) (X : FSet A), P X -> P ({|a|} ∪ X))
+    (Pdupl : forall (a : A) (X : FSet A) (px : P X),
+       transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px)
+    (Pcomm : forall (a b : A) (X : FSet A) (px : P X),
+       transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) :
+    FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm ∅ = Pempt.
+  Proof. by compute. Defined.
+
+  (* TODO *)
+  (* Theorem FSet_cons_ind_beta_cons (P : FSet A -> Type)  *)
+  (*   (Pset : forall (X : FSet A), IsHSet (P X)) *)
+  (*   (Pempt : P ∅) *)
+  (*   (Pcons : forall (a : A) (X : FSet A), P X -> P ({|a|} ∪ X)) *)
+  (*   (Pdupl : forall (a : A) (X : FSet A) (px : P X), *)
+  (*      transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px) *)
+  (*   (Pcomm : forall (a b : A) (X : FSet A) (px : P X), *)
+  (*      transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) : *)
+  (*   forall a X, FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm ({|a|} ∪ X) = Pcons a X (FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm X). *)
+  (* Proof.     *)
+
+  (* Theorem FSet_cons_ind_beta_dupl (P : FSet A -> Type)  *)
+  (*   (Pset : forall (X : FSet A), IsHSet (P X)) *)
+  (*   (Pempt : P ∅) *)
+  (*   (Pcons : forall (a : A) (X : FSet A), P X -> P ({|a|} ∪ X)) *)
+  (*   (Pdupl : forall (a : A) (X : FSet A) (px : P X), *)
+  (*      transport P (dupl' a X) (Pcons a _ (Pcons a X px)) = Pcons a X px) *)
+  (*   (Pcomm : forall (a b : A) (X : FSet A) (px : P X), *)
+  (*      transport P (comm' a b X) (Pcons a _ (Pcons b X px)) = Pcons b _ (Pcons a X px)) : *)
+  (*   forall a X, apD (FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm) (dupl' a X) = Pdupl a X (FSet_cons_ind P Pset Pempt Pcons Pdupl Pcomm X). *)
 End Iso.

FiniteSets/variations/enumerated.v

@@ -251,35 +251,26 @@ Section fset_dec_enumerated.
   Variable A : Type.
   Context `{Univalence}.
 
-  Definition Kf_fsetc :
+  Definition merely_enumeration_FSet :
-    Kf A -> exists (X : FSetC A), forall (a : A), k_finite.map (FSetC_to_FSet X) a.
+    forall (X : FSet A),
+    hexists (fun (ls : list A) => forall a, a ∈ X = listExt ls a).
   Proof.
-    intros [X HX].
+    simple refine (FSet_cons_ind _ _ _ _ _ _); simpl.
-    exists (FSet_to_FSetC X).
-    rewrite repr_iso_id_l.
-    by rewrite <- HX.
-  Defined.
-
-  Definition merely_enumeration_FSetC :
-    forall (X : FSetC A),
-    hexists (fun (ls : list A) => forall a, a ∈ (FSetC_to_FSet X) = listExt ls a).
-  Proof.
-    hinduction.
     - apply tr. exists nil. simpl. done.
     - intros a X Hls.
       strip_truncations. apply tr.
       destruct Hls as [ls Hls].
       exists (cons a ls). intros b. cbn.
-      f_ap.
+      apply (ap (fun z => _ ∨ z) (Hls b)).
     - intros. apply path_ishprop.
     - intros. apply path_ishprop.
   Defined.
 
   Definition Kf_enumerated : Kf A -> enumerated A.
   Proof.
-    intros HKf. apply Kf_fsetc in HKf.
+    intros HKf. apply Kf_unfold in HKf.
     destruct HKf as [X HX].
-    pose (ls' := (merely_enumeration_FSetC X)).
+    pose (ls' := (merely_enumeration_FSet X)).
     simple refine (@Trunc_rec _ _ _ _ _ ls'). clear ls'.
     intros [ls Hls].
     apply tr. exists ls.