From 1aebb3879e143623f6b65a7710fc4ed6b4f55b46 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 11 Oct 2017 10:03:28 +0200 Subject: [PATCH] Add the CPP paper overview --- FiniteSets/CPP.v | 137 +++++++++++++++++++++++++++++++++++++++++ FiniteSets/_CoqProject | 3 +- 2 files changed, 139 insertions(+), 1 deletion(-) create mode 100644 FiniteSets/CPP.v diff --git a/FiniteSets/CPP.v b/FiniteSets/CPP.v new file mode 100644 index 0000000..adbbda4 --- /dev/null +++ b/FiniteSets/CPP.v @@ -0,0 +1,137 @@ +Require Import FSets list_representation. +Require Import kuratowski.length misc.dec_kuratowski. +From interfaces Require Import lattice_interface. +From subobjects Require Import sub b_finite enumerated k_finite. +(* we need so many imports :( *) + +(** * Definitions *) +Definition definition_2_1 := FSet. +Definition definition_2_2 := FSet_ind. +Definition lemma_2_3 {A : Type} : forall x: FSet A, x ∪ x = x := union_idem. + +(** ** Extensionality *) +Definition definition_2_4 `{Univalence} := fset_member. +Definition theorem_2_5 `{Univalence} {A} (X Y : FSet A) : + X = Y <~> forall (a : A), a ∈ X = a ∈ Y := fset_ext X Y. +Definition lemma_2_6 `{Univalence} (A : Type) (X Y : FSet A) := equiv_subset1_r X Y. + +(** ** L(A) definition *) +Definition definition_2_7 := list_representation.FSetC.FSetC. +Definition theorem_2_8 {A} : FSet A <~> FSetC A := isomorphism.repr_iso. +Definition proposition_2_9 {A : Type} : + forall P : Type, + IsHSet P -> + P -> + forall Pcons : A -> FSet A -> P -> P, + (forall (X : FSet A) (a : A) (p : P), + Pcons a {|a|} ∪ X (Pcons a X p) = Pcons a X p) -> + (forall (X : FSet A) (a b : A) (p : P), + Pcons a {|b|} ∪ X (Pcons b X p) = Pcons b {|a|} ∪ X (Pcons a X p)) -> + FSet A -> P + := FSet_cons_rec. + + +(** * Decidability *) +Require Import misc.dec_lem. +Definition theorem_3_1 `{Univalence} := merely_dec. + +(** ** Decidable membership *) +Definition proposition_3_2 `{Univalence} {A} + `{MerelyDecidablePaths A} + (x : FSet A) (a : A) : + Decidable (a ∈ x) + := isIn_decidable a x. +Definition definition_3_3 `{Univalence} {A}`{MerelyDecidablePaths A} + := fset_member_bool. +Definition proposition_3_4 `{H: Univalence} {A : Type} := @dec_membership A H. + +(** ** Size *) +Definition proposition_3_5 `{Univalence} (A: Type) `{MerelyDecidablePaths A} + (X : FSet A) : nat := length X. +Definition proposition_3_6 `{H : Univalence} (A : Type) := @dec_length A H. + +(** ** Lattice structure *) +Definition definition_3_7 := fset_comprehension. +Definition definition_3_8 `{H : Univalence} {A : Type} + `{M : MerelyDecidablePaths A} := @fset_intersection A M H. +Definition proposition_3_9 `{H : Univalence} {A : Type} + `{M : MerelyDecidablePaths A} (X Y : FSet A) := intersection_isIn X Y. +Definition theorem_3_10 {H : Univalence} {A : Type} + `{M : MerelyDecidablePaths A} := @lattice_fset A M H. +Definition proposition_3_11 `{H : Univalence} (A : Type) := @merely_choice A H. +Definition proposition_3_12 `{H: Univalence} (A : Type) := @dec_intersection A H. + + +(** * Finite types *) +(** ** Subobjects *) +Definition definition_4_1 := Sub. +Definition lemma_4_2 := notIn_ext_union_singleton. +(** ** Bishop-finite *) +Definition definition_4_3 := Fin. +Definition definition_4_4 := Finite. +Definition definition_4_5 (A: Type) (X : Sub A) := Bfin X. +Definition lemma_4_6 := Finite_ind. +Definition proposition_4_7 := singleton. +Definition proposition_4_8 := set_singleton. + +Definition lemma_4_9 `{Univalence} (A : Type) (P : Sub A) := split P. +Definition lemma_4_10 `{Univalence} := DecidableMembership. +Definition proposition_4_11 := bfin_union. +Definition proposition_4_12 := no_union. + +(** ** Finite by enumeration *) +Definition definition_4_13 := enumerated. +Definition definition_4_14 := Kf. (* We define it slightly differently in Coq, see also lemma [Kf_unfold] *) +Definition proposition_4_15 := Kf_sub_hprop. +Definition proposition_4_16 := enumerated_Kf. +Definition proposition_4_17 `{Univalence} := Kf_enumerated. +Definition proposition_4_18 := map_injective. +Definition definition_4_19 := Kf_sub. +Definition example_4_20 `{Univalence} := S1_Kfinite. +Definition theorem_4_21 `{Univalence} (X Y : Type) : + (forall (f : X -> Y), IsSurjection f -> Kf X -> Kf Y) + /\ (Kf X -> Kf Y -> Kf (X * Y)) + /\ (Kf X -> Kf Y -> Kf (X + Y)) + /\ (closedSingleton (Kf_sub X)) + /\ (closedUnion (Kf_sub X)). +Proof. + repeat split. + - apply Kf_surjection. + - apply Kf_prod. + - apply Kf_sum. + - apply k_finite_singleton. + - apply k_finite_union. +Qed. +Definition proposition_4_22 `{Univalence} := bfin_to_kfin. +Definition theorem_4_23 `{Univalence} (X : Type) `{DecidablePaths X} := Kf_to_Bf X. + +(** * Interface for finite sets *) +From interfaces Require Import set_interface. +(** ** Method *) +Definition definition_5_1 := tt. (* not actually present; bundled in the next definition *) +Definition definition_5_2 `{Univalence} := sets. +Definition proposition_5_3 `{Univalence} := f_surjective. +Definition proposition_5_4 `{Univalence} (T : Type -> Type) + (f : forall A, T A -> FSet A) `{sets T f} (A : Type) := quotient_iso (f A). +(* TODO: Definition proposition_5_5 *) +Definition theorem_5_6 := transfer. +Definition corollary_5_7 := refinement. +(** ** Application *) +Require Import misc.dec_fset. +Definition definition_5_8 `{Univalence} {A : Type} (P : A -> hProp) := all P. +Definition proposition_5_9 `{Univalence} {A : Type} (P : A -> hProp) : + (forall (x : FSet A), (forall (a : A), a ∈ x -> P a) -> all P x) +/\ (forall (x : FSet A) (a : A), all P x -> (a ∈ x) -> P a). +Proof. + split. + - apply all_intro. + - apply all_elim. +Qed. + +(** * Related work *) +(** This is not stated separately in the paper, but we can handle examples from e.g. "Denis Firsov and Tarmo Uustalu. 2015. Dependently Typed Program- +ming with Finite Sets" *) +(** The Pauli group example *) +Definition misc_1 `{Univalence} := Pauli_mult_comm. +(** Decidility of prediates on finite sets is preserved by quantifiers *) +Definition misc_2 `{Univalence} {A : Type} (P : A -> hProp) `{forall a, Decidable (P a)} := all_decidable P. diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject index e0a1976..1c8a3bc 100644 --- a/FiniteSets/_CoqProject +++ b/FiniteSets/_CoqProject @@ -26,4 +26,5 @@ misc/ordered.v misc/projective.v misc/dec_kuratowski.v misc/dec_fset.v -implementations/lists.v \ No newline at end of file +implementations/lists.v +CPP.v