diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v deleted file mode 100644 index 0475146..0000000 --- a/FiniteSets/disjunction.v +++ /dev/null @@ -1,163 +0,0 @@ -(* Logical disjunction in HoTT (see ch. 3 of the book) *) -Require Import HoTT. -Require Import lattice notation. - -Instance lor : maximum hProp := fun X Y => BuildhProp (Trunc (-1) (sum X Y)). - -Delimit Scope logic_scope with L. -Notation "A ∨ B" := (lor A B) (at level 20, right associativity) : logic_scope. -Arguments lor _%L _%L. -Open Scope logic_scope. - -Section lor_props. - Context `{Univalence}. - Variable X Y Z : hProp. - - Local Ltac lor_intros := - let x := fresh in intro x - ; repeat (strip_truncations ; destruct x as [x | x]). - - - Lemma lor_assoc : (X ∨ Y) ∨ Z = X ∨ Y ∨ Z. - Proof. - apply path_iff_hprop ; lor_intros - ; apply tr ; auto - ; try (left ; apply tr) - ; try (right ; apply tr) ; auto. - Defined. - - Lemma lor_comm : X ∨ Y = Y ∨ X. - Proof. - apply path_iff_hprop ; lor_intros - ; apply tr ; auto. - Defined. - - Lemma lor_nl : False_hp ∨ X = X. - Proof. - apply path_iff_hprop ; lor_intros ; try contradiction - ; try (refine (tr(inr _))) ; auto. - Defined. - - Lemma lor_nr : X ∨ False_hp = X. - Proof. - apply path_iff_hprop ; lor_intros ; try contradiction - ; try (refine (tr(inl _))) ; auto. - Defined. - - Lemma lor_idem : X ∨ X = X. - Proof. - apply path_iff_hprop ; lor_intros - ; try(refine (tr(inl _))) ; auto. - Defined. - -End lor_props. - -Instance land : minimum hProp := fun X Y => BuildhProp (prod X Y). -Instance lfalse : bottom hProp := False_hp. - -Notation "A ∧ B" := (land A B) (at level 20, right associativity) : logic_scope. -Arguments land _%L _%L. -Open Scope logic_scope. - -Section hPropLattice. - Context `{Univalence}. - - Instance lor_commutative : Commutative lor. - Proof. - unfold Commutative. - intros. - apply lor_comm. - Defined. - - Instance land_commutative : Commutative land. - Proof. - unfold Commutative, land. - intros. - apply path_hprop. - apply equiv_prod_symm. - Defined. - - Instance lor_associative : Associative lor. - Proof. - unfold Associative. - intros. - apply lor_assoc. - Defined. - - Instance land_associative : Associative land. - Proof. - unfold Associative, land. - intros. - symmetry. - apply path_hprop. - apply equiv_prod_assoc. - Defined. - - Instance lor_idempotent : Idempotent lor. - Proof. - unfold Idempotent. - intros. - apply lor_idem. - Defined. - - Instance land_idempotent : Idempotent land. - Proof. - unfold Idempotent, land. - intros. - apply path_iff_hprop ; cbn. - - intros [a b] ; apply a. - - intros a ; apply (pair a a). - Defined. - - Instance lor_neutrall : NeutralL lor lfalse. - Proof. - unfold NeutralL. - intros. - apply lor_nl. - Defined. - - Instance lor_neutralr : NeutralR lor lfalse. - Proof. - unfold NeutralR. - intros. - apply lor_nr. - Defined. - - Instance absorption_orb_andb : Absorption lor land. - Proof. - unfold Absorption. - intros. - apply path_iff_hprop ; cbn. - - intros X ; strip_truncations. - destruct X as [Xx | [Xy1 Xy2]] ; assumption. - - intros X. - apply (tr (inl X)). - Defined. - - Instance absorption_andb_orb : Absorption land lor. - Proof. - unfold Absorption. - intros. - apply path_iff_hprop ; cbn. - - intros [X Y] ; strip_truncations. - assumption. - - intros X. - split. - * assumption. - * apply (tr (inl X)). - Defined. - - Global Instance lattice_hprop : Lattice hProp := - { commutative_min := _ ; - commutative_max := _ ; - associative_min := _ ; - associative_max := _ ; - idempotent_min := _ ; - idempotent_max := _ ; - neutralL_max := _ ; - neutralR_max := _ ; - absorption_min_max := _ ; - absorption_max_min := _ - }. - -End hPropLattice. diff --git a/FiniteSets/implementations/lists.v b/FiniteSets/implementations/lists.v index 05cdbc0..f577a3a 100644 --- a/FiniteSets/implementations/lists.v +++ b/FiniteSets/implementations/lists.v @@ -1,6 +1,6 @@ (* Implementation of [FSet A] using lists *) Require Import HoTT HitTactics. -Require Import FSets implementations.interface. +Require Import FSets set_interface. Section Operations. Context `{Univalence}. diff --git a/FiniteSets/interfaces/lattice_examples.v b/FiniteSets/interfaces/lattice_examples.v new file mode 100644 index 0000000..1eb26db --- /dev/null +++ b/FiniteSets/interfaces/lattice_examples.v @@ -0,0 +1,250 @@ +(** Some examples of lattices. *) +Require Import HoTT lattice_interface. + +(** [Bool] is a lattice. *) +Section BoolLattice. + Ltac solve_bool := + let x := fresh in + repeat (intro x ; destruct x) + ; compute + ; auto + ; try contradiction. + + Instance maximum_bool : maximum Bool := orb. + Instance minimum_bool : minimum Bool := andb. + Instance bottom_bool : bottom Bool := false. + + Global Instance lattice_bool : Lattice Bool. + Proof. + split ; solve_bool. + Defined. + + Definition and_true : forall b, andb b true = b. + Proof. + solve_bool. + Defined. + + Definition and_false : forall b, andb b false = false. + Proof. + solve_bool. + Defined. + + Definition dist₁ : forall b₁ b₂ b₃, + andb b₁ (orb b₂ b₃) = orb (andb b₁ b₂) (andb b₁ b₃). + Proof. + solve_bool. + Defined. + + Definition dist₂ : forall b₁ b₂ b₃, + orb b₁ (andb b₂ b₃) = andb (orb b₁ b₂) (orb b₁ b₃). + Proof. + solve_bool. + Defined. + + Definition max_min : forall b₁ b₂, + orb (andb b₁ b₂) b₁ = b₁. + Proof. + solve_bool. + Defined. +End BoolLattice. + +Create HintDb bool_lattice_hints. +Hint Resolve associativity : bool_lattice_hints. +Hint Resolve (associativity _ _ _)^ : bool_lattice_hints. +Hint Resolve commutative : bool_lattice_hints. +Hint Resolve absorb : bool_lattice_hints. +Hint Resolve idempotency : bool_lattice_hints. +Hint Resolve neutralityL : bool_lattice_hints. +Hint Resolve neutralityR : bool_lattice_hints. + +Hint Resolve + associativity + and_true and_false + dist₁ dist₂ max_min + : bool_lattice_hints. + +(** If [B] is a lattice, then [A -> B] is a lattice. *) +Section fun_lattice. + Context {A B : Type}. + Context `{Lattice B}. + Context `{Funext}. + + Global Instance max_fun : maximum (A -> B) := + fun (f g : A -> B) (a : A) => max_L0 (f a) (g a). + + Global Instance min_fun : minimum (A -> B) := + fun (f g : A -> B) (a : A) => min_L0 (f a) (g a). + + Global Instance bot_fun : bottom (A -> B) + := fun _ => empty_L. + + Ltac solve_fun := + compute ; intros ; apply path_forall ; intro ; + eauto with lattice_hints typeclass_instances. + + Global Instance lattice_fun : Lattice (A -> B). + Proof. + split ; solve_fun. + Defined. +End fun_lattice. + +(** If [A] is a lattice and [P] is closed under the lattice operations, then [Σ(x:A), P x] is a lattice. *) +Section sub_lattice. + Context {A : Type} {P : A -> hProp}. + Context `{Lattice A}. + Context {Hmax : forall x y, P x -> P y -> P (max_L0 x y)}. + Context {Hmin : forall x y, P x -> P y -> P (min_L0 x y)}. + Context {Hbot : P empty_L}. + + Definition AP : Type := sig P. + + Instance botAP : bottom AP := (empty_L ; Hbot). + + Instance maxAP : maximum AP := + fun x y => + match x, y with + | (a ; pa), (b ; pb) => (max_L0 a b ; Hmax a b pa pb) + end. + + Instance minAP : minimum AP := + fun x y => + match x, y with + | (a ; pa), (b ; pb) => (min_L0 a b ; Hmin a b pa pb) + end. + + Instance hprop_sub : forall c, IsHProp (P c). + Proof. + apply _. + Defined. + + Ltac solve_sub := + let x := fresh in + repeat (intro x ; destruct x) + ; simple refine (path_sigma _ _ _ _ _) + ; simpl + ; try (apply hprop_sub) + ; eauto 3 with lattice_hints typeclass_instances. + + Global Instance lattice_sub : Lattice AP. + Proof. + split ; solve_sub. + Defined. +End sub_lattice. + +Instance lor : maximum hProp := fun X Y => BuildhProp (Trunc (-1) (sum X Y)). + +Delimit Scope logic_scope with L. +Notation "A ∨ B" := (lor A B) (at level 20, right associativity) : logic_scope. +Arguments lor _%L _%L. +Open Scope logic_scope. + +Instance land : minimum hProp := fun X Y => BuildhProp (prod X Y). +Instance lfalse : bottom hProp := False_hp. + +Notation "A ∧ B" := (land A B) (at level 20, right associativity) : logic_scope. +Arguments land _%L _%L. +Open Scope logic_scope. + +(** [hProp] is a lattice. *) +Section hPropLattice. + Context `{Univalence}. + + Local Ltac lor_intros := + let x := fresh in intro x + ; repeat (strip_truncations ; destruct x as [x | x]). + + Instance lor_commutative : Commutative lor. + Proof. + intros X Y. + apply path_iff_hprop ; lor_intros + ; apply tr ; auto. + Defined. + + Instance land_commutative : Commutative land. + Proof. + intros X Y. + apply path_hprop. + apply equiv_prod_symm. + Defined. + + Instance lor_associative : Associative lor. + Proof. + intros X Y Z. + apply path_iff_hprop ; lor_intros + ; apply tr ; auto + ; try (left ; apply tr) + ; try (right ; apply tr) ; auto. + Defined. + + Instance land_associative : Associative land. + Proof. + intros X Y Z. + symmetry. + apply path_hprop. + apply equiv_prod_assoc. + Defined. + + Instance lor_idempotent : Idempotent lor. + Proof. + intros X. + apply path_iff_hprop ; lor_intros + ; try(refine (tr(inl _))) ; auto. + Defined. + + Instance land_idempotent : Idempotent land. + Proof. + intros X. + apply path_iff_hprop ; cbn. + - intros [a b] ; apply a. + - intros a ; apply (pair a a). + Defined. + + Instance lor_neutrall : NeutralL lor lfalse. + Proof. + intros X. + apply path_iff_hprop ; lor_intros ; try contradiction + ; try (refine (tr(inr _))) ; auto. + Defined. + + Instance lor_neutralr : NeutralR lor lfalse. + Proof. + intros X. + apply path_iff_hprop ; lor_intros ; try contradiction + ; try (refine (tr(inl _))) ; auto. + Defined. + + Instance absorption_orb_andb : Absorption lor land. + Proof. + intros Z1 Z2. + apply path_iff_hprop ; cbn. + - intros X ; strip_truncations. + destruct X as [Xx | [Xy1 Xy2]] ; assumption. + - intros X. + apply (tr (inl X)). + Defined. + + Instance absorption_andb_orb : Absorption land lor. + Proof. + intros Z1 Z2. + apply path_iff_hprop ; cbn. + - intros [X Y] ; strip_truncations. + assumption. + - intros X. + split. + * assumption. + * apply (tr (inl X)). + Defined. + + Global Instance lattice_hprop : Lattice hProp := + { commutative_min := _ ; + commutative_max := _ ; + associative_min := _ ; + associative_max := _ ; + idempotent_min := _ ; + idempotent_max := _ ; + neutralL_max := _ ; + neutralR_max := _ ; + absorption_min_max := _ ; + absorption_max_min := _ + }. +End hPropLattice. \ No newline at end of file diff --git a/FiniteSets/interfaces/lattice_interface.v b/FiniteSets/interfaces/lattice_interface.v new file mode 100644 index 0000000..103daea --- /dev/null +++ b/FiniteSets/interfaces/lattice_interface.v @@ -0,0 +1,115 @@ +(** Interface for lattices and join semilattices. *) +Require Import HoTT. + +Section binary_operation. + Definition operation (A : Type) := A -> A -> A. + + Variable (A : Type) + (f : operation A). + + Class Commutative := + commutative : forall x y, f x y = f y x. + + Class Associative := + associativity : forall x y z, f (f x y) z = f x (f y z). + + Class Idempotent := + idempotency : forall x, f x x = x. + + Variable g : operation A. + + Class Absorption := + absorb : forall x y, f x (g x y) = x. + + Variable (n : A). + + Class NeutralL := + neutralityL : forall x, f n x = x. + + Class NeutralR := + neutralityR : forall x, f x n = x. +End binary_operation. + +Arguments Commutative {_} _. +Arguments Associative {_} _. +Arguments Idempotent {_} _. +Arguments NeutralL {_} _ _. +Arguments NeutralR {_} _ _. +Arguments Absorption {_} _ _. +Arguments commutative {_} {_} {_} _ _. +Arguments associativity {_} {_} {_} _ _ _. +Arguments idempotency {_} {_} {_} _. +Arguments neutralityL {_} {_} {_} {_} _. +Arguments neutralityR {_} {_} {_} {_} _. +Arguments absorb {_} {_} {_} {_} _ _. + +Section lattice_operations. + Variable (A : Type). + + Class maximum := + max_L : operation A. + + Class minimum := + min_L : operation A. + + Class bottom := + empty : A. +End lattice_operations. + +Arguments max_L {_} {_} _. +Arguments min_L {_} {_} _. +Arguments empty {_}. + +Section JoinSemiLattice. + Variable A : Type. + Context {max_L : maximum A} {empty_L : bottom A}. + + Class JoinSemiLattice := + { + commutative_max_js :> Commutative max_L ; + associative_max_js :> Associative max_L ; + idempotent_max_js :> Idempotent max_L ; + neutralL_max_js :> NeutralL max_L empty_L ; + neutralR_max_js :> NeutralR max_L empty_L ; + }. +End JoinSemiLattice. + +Arguments JoinSemiLattice _ {_} {_}. + +Create HintDb joinsemilattice_hints. +Hint Resolve associativity : joinsemilattice_hints. +Hint Resolve (associativity _ _ _)^ : joinsemilattice_hints. +Hint Resolve commutative : joinsemilattice_hints. +Hint Resolve idempotency : joinsemilattice_hints. +Hint Resolve neutralityL : joinsemilattice_hints. +Hint Resolve neutralityR : joinsemilattice_hints. + +Section Lattice. + Variable A : Type. + Context {max_L : maximum A} {min_L : minimum A} {empty_L : bottom A}. + + Class Lattice := + { + commutative_min :> Commutative min_L ; + commutative_max :> Commutative max_L ; + associative_min :> Associative min_L ; + associative_max :> Associative max_L ; + idempotent_min :> Idempotent min_L ; + idempotent_max :> Idempotent max_L ; + neutralL_max :> NeutralL max_L empty_L ; + neutralR_max :> NeutralR max_L empty_L ; + absorption_min_max :> Absorption min_L max_L ; + absorption_max_min :> Absorption max_L min_L + }. +End Lattice. + +Arguments Lattice _ {_} {_} {_}. + +Create HintDb lattice_hints. +Hint Resolve associativity : lattice_hints. +Hint Resolve (associativity _ _ _)^ : lattice_hints. +Hint Resolve commutative : lattice_hints. +Hint Resolve absorb : lattice_hints. +Hint Resolve idempotency : lattice_hints. +Hint Resolve neutralityL : lattice_hints. +Hint Resolve neutralityR : lattice_hints. \ No newline at end of file diff --git a/FiniteSets/interfaces/monad_interface.v b/FiniteSets/interfaces/monad_interface.v new file mode 100644 index 0000000..7d748e1 --- /dev/null +++ b/FiniteSets/interfaces/monad_interface.v @@ -0,0 +1,45 @@ +(** The structure of a monad. *) +Require Import HoTT. + +Section functor. + Variable (F : Type -> Type). + Context `{Functorish F}. + + Class Functor := + { + fmap_compose {A B C : Type} (f : A -> B) (g : B -> C) : + fmap F (g o f) = fmap F g o fmap F f + }. +End functor. + +Section monad_operations. + Variable (F : Type -> Type). + + Class hasPure := + { + pure : forall (A : Type), A -> F A + }. + + Class hasBind := + { + bind : forall (A : Type), F(F A) -> F A + }. +End monad_operations. + +Arguments pure {_} {_} _ _. +Arguments bind {_} {_} _ _. + +Section monad. + Variable (F : Type -> Type). + Context `{Functor F} `{hasPure F} `{hasBind F}. + + Class Monad := + { + bind_assoc : forall {A : Type}, + bind A o bind (F A) = bind A o fmap F (bind A) ; + bind_neutral_l : forall {A : Type}, + bind A o pure (F A) = idmap ; + bind_neutral_r : forall {A : Type}, + bind A o fmap F (pure A) = idmap + }. +End monad. \ No newline at end of file diff --git a/FiniteSets/interfaces/set_interface.v b/FiniteSets/interfaces/set_interface.v new file mode 100644 index 0000000..2c56e66 --- /dev/null +++ b/FiniteSets/interfaces/set_interface.v @@ -0,0 +1,331 @@ +Require Import HoTT. +Require Import FSets lattice_interface. + +Section interface. + Context `{Univalence}. + Variable (T : Type -> Type) + (f : forall A, T A -> FSet A). + Context `{forall A, hasMembership (T A) A + , forall A, hasEmpty (T A) + , forall A, hasSingleton (T A) A + , forall A, hasUnion (T A) + , forall A, hasComprehension (T A) A}. + + Class sets := + { + f_empty : forall A, f A ∅ = ∅ ; + f_singleton : forall A a, f A (singleton a) = {|a|}; + f_union : forall A X Y, f A (union X Y) = (f A X) ∪ (f A Y); + f_filter : forall A φ X, f A (filter φ X) = {| f A X & φ |}; + f_member : forall A a X, member a X = a ∈ (f A X) + }. + + Global Instance f_surjective A `{sets} : IsSurjection (f A). + Proof. + unfold IsSurjection. + hinduction ; try (intros ; apply path_ishprop). + - simple refine (BuildContr _ _ _). + * refine (tr(∅;_)). + apply f_empty. + * intros ; apply path_ishprop. + - intro a. + simple refine (BuildContr _ _ _). + * refine (tr({|a|};_)). + apply f_singleton. + * intros ; apply path_ishprop. + - intros Y1 Y2 [X1' ?] [X2' ?]. + simple refine (BuildContr _ _ _). + * simple refine (Trunc_rec _ X1') ; intros [X1 fX1]. + simple refine (Trunc_rec _ X2') ; intros [X2 fX2]. + refine (tr(X1 ∪ X2;_)). + rewrite f_union, fX1, fX2. + reflexivity. + * intros ; apply path_ishprop. + Defined. + +End interface. + +Section quotient_surjection. + Variable (A B : Type) + (f : A -> B) + (H : IsSurjection f). + Context `{IsHSet B} `{Univalence}. + + Definition f_eq : relation A := fun a1 a2 => f a1 = f a2. + Definition quotientB : Type := quotient f_eq. + + Global Instance quotientB_recursion : HitRecursion quotientB := + { + indTy := _; + recTy := + forall (P : Type) (HP: IsHSet P) (u : A -> P), + (forall x y : A, f_eq x y -> u x = u y) -> quotientB -> P; + H_inductor := quotient_ind f_eq ; + H_recursor := @quotient_rec _ f_eq _ + }. + + Global Instance R_refl : Reflexive f_eq. + Proof. + intro. + reflexivity. + Defined. + + Global Instance R_sym : Symmetric f_eq. + Proof. + intros a b Hab. + apply (Hab^). + Defined. + + Global Instance R_trans : Transitive f_eq. + Proof. + intros a b c Hab Hbc. + apply (Hab @ Hbc). + Defined. + + Definition quotientB_to_B : quotientB -> B. + Proof. + hrecursion. + - apply f. + - done. + Defined. + + Instance quotientB_emb : IsEmbedding (quotientB_to_B). + Proof. + apply isembedding_isinj_hset. + unfold isinj. + hrecursion ; [ | intros; apply path_ishprop ]. + intro. + hrecursion ; [ | intros; apply path_ishprop ]. + intros. + by apply related_classes_eq. + Defined. + + Instance quotientB_surj : IsSurjection (quotientB_to_B). + Proof. + apply BuildIsSurjection. + intros Y. + destruct (H Y). + simple refine (Trunc_rec _ center) ; intros [a fa]. + apply (tr(class_of _ a;fa)). + Defined. + + Definition quotient_iso : quotientB <~> B. + Proof. + refine (BuildEquiv _ _ quotientB_to_B _). + apply isequiv_surj_emb ; apply _. + Defined. + + Definition reflect_eq : forall (X Y : A), + f X = f Y -> f_eq X Y. + Proof. + done. + Defined. + + Lemma same_class : forall (X Y : A), + class_of f_eq X = class_of f_eq Y -> f_eq X Y. + Proof. + intros. + simple refine (classes_eq_related _ _ _ _) ; assumption. + Defined. + +End quotient_surjection. + +Arguments quotient_iso {_} {_} _ {_} {_} {_}. + +Ltac reduce T := + intros ; + repeat (rewrite (f_empty T _) + || rewrite (f_singleton T _) + || rewrite (f_union T _) + || rewrite (f_filter T _) + || rewrite (f_member T _)). + +Section quotient_properties. + Variable (T : Type -> Type). + Variable (f : forall {A : Type}, T A -> FSet A). + Context `{sets T f}. + + Definition set_eq A := f_eq (T A) (FSet A) (f A). + Definition View A : Type := quotientB (T A) (FSet A) (f A). + + Instance f_is_surjective A : IsSurjection (f A). + Proof. + apply (f_surjective T f A). + Defined. + + Global Instance view_union (A : Type) : hasUnion (View A). + Proof. + intros X Y. + apply (quotient_iso _)^-1. + simple refine (union _ _). + - simple refine (quotient_iso (f A) X). + - simple refine (quotient_iso (f A) Y). + Defined. + + Definition well_defined_union (A : Type) (X Y : T A) : + (class_of _ X) ∪ (class_of _ Y) = class_of _ (X ∪ Y). + Proof. + rewrite <- (eissect (quotient_iso _)). + simpl. + rewrite (f_union T _). + reflexivity. + Defined. + + Global Instance view_comprehension (A : Type) : hasComprehension (View A) A. + Proof. + intros ϕ X. + apply (quotient_iso _)^-1. + simple refine ({|_ & ϕ|}). + apply (quotient_iso (f A) X). + Defined. + + Definition well_defined_filter (A : Type) (ϕ : A -> Bool) (X : T A) : + {|class_of _ X & ϕ|} = class_of _ {|X & ϕ|}. + Proof. + rewrite <- (eissect (quotient_iso _)). + simpl. + rewrite (f_filter T _). + reflexivity. + Defined. + + Global Instance View_empty A : hasEmpty (View A). + Proof. + apply ((quotient_iso _)^-1 ∅). + Defined. + + Definition well_defined_empty A : ∅ = class_of (set_eq A) ∅. + Proof. + rewrite <- (eissect (quotient_iso _)). + simpl. + rewrite (f_empty T _). + reflexivity. + Defined. + + Global Instance View_singleton A: hasSingleton (View A) A. + Proof. + intro a ; apply ((quotient_iso _)^-1 {|a|}). + Defined. + + Definition well_defined_sungleton A (a : A) : {|a|} = class_of _ {|a|}. + Proof. + rewrite <- (eissect (quotient_iso _)). + simpl. + rewrite (f_singleton T _). + reflexivity. + Defined. + + Global Instance View_member A : hasMembership (View A) A. + Proof. + intros a ; unfold View. + hrecursion. + - apply (member a). + - intros X Y HXY. + reduce T. + apply (ap _ HXY). + Defined. + + Instance View_max A : maximum (View A). + Proof. + apply view_union. + Defined. + + Hint Unfold Commutative Associative Idempotent NeutralL NeutralR View_max view_union. + + Instance bottom_view A : bottom (View A). + Proof. + apply View_empty. + Defined. + + Ltac sq1 := autounfold ; intros ; try f_ap + ; rewrite ?(eisretr (quotient_iso _)) + ; eauto with lattice_hints typeclass_instances. + + Ltac sq2 := autounfold ; intros + ; rewrite <- (eissect (quotient_iso _)), ?(eisretr (quotient_iso _)) + ; f_ap ; simpl + ; reduce T ; eauto with lattice_hints typeclass_instances. + + Global Instance view_lattice A : JoinSemiLattice (View A). + Proof. + split ; try sq1 ; try sq2. + Defined. + +End quotient_properties. + +Arguments set_eq {_} _ {_} _ _. + +Section properties. + Context `{Univalence}. + Variable (T : Type -> Type) (f : forall A, T A -> FSet A). + Context `{sets T f}. + + Definition set_subset : forall A, T A -> T A -> hProp := + fun A X Y => (f A X) ⊆ (f A Y). + + Definition empty_isIn : forall (A : Type) (a : A), + a ∈ ∅ = False_hp. + Proof. + by (reduce T). + Defined. + + Definition singleton_isIn : forall (A : Type) (a b : A), + a ∈ {|b|} = merely (a = b). + Proof. + by (reduce T). + Defined. + + Definition union_isIn : forall (A : Type) (a : A) (X Y : T A), + a ∈ (X ∪ Y) = lor (a ∈ X) (a ∈ Y). + Proof. + by (reduce T). + Defined. + + Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A), + member a (filter ϕ X) = if ϕ a then member a X else False_hp. + Proof. + reduce T. + apply properties.comprehension_isIn. + Defined. + + Definition reflect_f_eq : forall (A : Type) (X Y : T A), + class_of (set_eq f) X = class_of (set_eq f) Y -> set_eq f X Y. + Proof. + intros. + refine (same_class _ _ _ _ _ _) ; assumption. + Defined. + + Ltac via_quotient := intros ; apply reflect_f_eq ; simpl + ; rewrite <- ?(well_defined_union T _), <- ?(well_defined_empty T _) + ; eauto with lattice_hints typeclass_instances. + + Lemma union_comm : forall A (X Y : T A), + set_eq f (X ∪ Y) (Y ∪ X). + Proof. + via_quotient. + Defined. + + Lemma union_assoc : forall A (X Y Z : T A), + set_eq f ((X ∪ Y) ∪ Z) (X ∪ (Y ∪ Z)). + Proof. + via_quotient. + Defined. + + Lemma union_idem : forall A (X : T A), + set_eq f (X ∪ X) X. + Proof. + via_quotient. + Defined. + + Lemma union_neutralL : forall A (X : T A), + set_eq f (∅ ∪ X) X. + Proof. + via_quotient. + Defined. + + Lemma union_neutralR : forall A (X : T A), + set_eq f (X ∪ ∅) X. + Proof. + via_quotient. + Defined. + +End properties. \ No newline at end of file diff --git a/FiniteSets/notation.v b/FiniteSets/interfaces/set_names.v similarity index 62% rename from FiniteSets/notation.v rename to FiniteSets/interfaces/set_names.v index cd3c53f..e740141 100644 --- a/FiniteSets/notation.v +++ b/FiniteSets/interfaces/set_names.v @@ -1,52 +1,6 @@ +(** Classes for set operations, so they can be overloaded. *) Require Import HoTT. -Section binary_operation. - Variable A : Type. - - Definition operation := A -> A -> A. -End binary_operation. - -Section Defs. - Variable A : Type. - Variable f : A -> A -> A. - - Class Commutative := - commutative : forall x y, f x y = f y x. - - Class Associative := - associativity : forall x y z, f (f x y) z = f x (f y z). - - Class Idempotent := - idempotency : forall x, f x x = x. - - Variable g : operation A. - - Class Absorption := - absorb : forall x y, f x (g x y) = x. - - Variable n : A. - - Class NeutralL := - neutralityL : forall x, f n x = x. - - Class NeutralR := - neutralityR : forall x, f x n = x. - -End Defs. - -Arguments Commutative {_} _. -Arguments Associative {_} _. -Arguments Idempotent {_} _. -Arguments NeutralL {_} _ _. -Arguments NeutralR {_} _ _. -Arguments Absorption {_} _ _. -Arguments commutative {_} {_} {_} _ _. -Arguments associativity {_} {_} {_} _ _ _. -Arguments idempotency {_} {_} {_} _. -Arguments neutralityL {_} {_} {_} {_} _. -Arguments neutralityR {_} {_} {_} {_} _. -Arguments absorb {_} {_} {_} {_} _ _. - Section structure. Variable (T A : Type). diff --git a/FiniteSets/fsets/extensionality.v b/FiniteSets/kuratowski/extensionality.v similarity index 98% rename from FiniteSets/fsets/extensionality.v rename to FiniteSets/kuratowski/extensionality.v index e8a517e..a430676 100644 --- a/FiniteSets/fsets/extensionality.v +++ b/FiniteSets/kuratowski/extensionality.v @@ -1,6 +1,6 @@ (** Extensionality of the FSets *) Require Import HoTT HitTactics. -Require Import representations.definition fsets.operations. +Require Import kuratowski.kuratowski_sets. Section ext. Context {A : Type}. diff --git a/FiniteSets/kuratowski/kuratowski_sets.v b/FiniteSets/kuratowski/kuratowski_sets.v new file mode 100644 index 0000000..2c313e9 --- /dev/null +++ b/FiniteSets/kuratowski/kuratowski_sets.v @@ -0,0 +1,165 @@ +(** Definitions of the Kuratowski-finite sets via a HIT *) +Require Import HoTT HitTactics. +Require Export set_names lattice_examples. + +Module Export FSet. + Section FSet. + Private Inductive FSet (A : Type) : Type := + | E : FSet A + | L : A -> FSet A + | U : FSet A -> FSet A -> FSet A. + + Global Instance fset_empty : forall A, hasEmpty (FSet A) := E. + Global Instance fset_singleton : forall A, hasSingleton (FSet A) A := L. + Global Instance fset_union : forall A, hasUnion (FSet A) := U. + + Variable A : Type. + + Axiom assoc : forall (x y z : FSet A), + x ∪ (y ∪ z) = (x ∪ y) ∪ z. + + Axiom comm : forall (x y : FSet A), + x ∪ y = y ∪ x. + + Axiom nl : forall (x : FSet A), + ∅ ∪ x = x. + + Axiom nr : forall (x : FSet A), + x ∪ ∅ = x. + + Axiom idem : forall (x : A), + {|x|} ∪ {|x|} = {|x|}. + + Axiom trunc : IsHSet (FSet A). + + End FSet. + + Arguments assoc {_} _ _ _. + Arguments comm {_} _ _. + Arguments nl {_} _. + Arguments nr {_} _. + Arguments idem {_} _. + + Section FSet_induction. + Variable (A : Type) + (P : FSet A -> Type) + (H : forall X : FSet A, IsHSet (P X)) + (eP : P ∅) + (lP : forall a: A, P {|a|}) + (uP : forall (x y: FSet A), P x -> P y -> P (x ∪ y)) + (assocP : forall (x y z : FSet A) + (px: P x) (py: P y) (pz: P z), + assoc x y z # + (uP x (y ∪ z) px (uP y z py pz)) + = + (uP (x ∪ y) z (uP x y px py) pz)) + (commP : forall (x y: FSet A) (px: P x) (py: P y), + comm x y # + uP x y px py = uP y x py px) + (nlP : forall (x : FSet A) (px: P x), + nl x # uP ∅ x eP px = px) + (nrP : forall (x : FSet A) (px: P x), + nr x # uP x ∅ px eP = px) + (idemP : forall (x : A), + idem x # uP {|x|} {|x|} (lP x) (lP x) = lP x). + + (* Induction principle *) + Fixpoint FSet_ind + (x : FSet A) + {struct x} + : P x + := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with + | E => fun _ _ _ _ _ _ => eP + | L a => fun _ _ _ _ _ _ => lP a + | U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z) + end) H assocP commP nlP nrP idemP. + End FSet_induction. + + Section FSet_recursion. + Variable (A : Type) + (P : Type) + (H: IsHSet P) + (e : P) + (l : A -> P) + (u : P -> P -> P) + (assocP : forall (x y z : P), u x (u y z) = u (u x y) z) + (commP : forall (x y : P), u x y = u y x) + (nlP : forall (x : P), u e x = x) + (nrP : forall (x : P), u x e = x) + (idemP : forall (x : A), u (l x) (l x) = l x). + + (* Recursion princople *) + Definition FSet_rec : FSet A -> P. + Proof. + simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) + ; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn. + - apply e. + - apply l. + - intros x y ; apply u. + - apply assocP. + - apply commP. + - apply nlP. + - apply nrP. + - apply idemP. + Defined. + End FSet_recursion. + + Instance FSet_recursion A : HitRecursion (FSet A) := + { + indTy := _; recTy := _; + H_inductor := FSet_ind A; H_recursor := FSet_rec A + }. +End FSet. + +Lemma union_idem {A : Type} : forall x: FSet A, x ∪ x = x. +Proof. + hinduction ; try (intros ; apply set_path2). + - apply nl. + - apply idem. + - intros x y P Q. + rewrite assoc. + rewrite (comm x y). + rewrite <- (assoc y x x). + rewrite P. + rewrite (comm y x). + rewrite <- (assoc x y y). + apply (ap (x ∪) Q). +Defined. + +Section relations. + Context `{Univalence}. + + (** Membership of finite sets. *) + Global Instance fset_member : forall A, hasMembership (FSet A) A. + Proof. + intros A a. + hrecursion. + - apply False_hp. + - apply (fun a' => merely(a = a')). + - apply lor. + - eauto with lattice_hints typeclass_instances. + - eauto with lattice_hints typeclass_instances. + - eauto with lattice_hints typeclass_instances. + - eauto with lattice_hints typeclass_instances. + - eauto with lattice_hints typeclass_instances. + Defined. + + (** Subset relation of finite sets. *) + Global Instance fset_subset : forall A, hasSubset (FSet A). + Proof. + intros A X Y. + hrecursion X. + - apply Unit_hp. + - apply (fun a => a ∈ Y). + - intros X1 X2. + exists (prod X1 X2). + exact _. + - eauto with lattice_hints typeclass_instances. + - eauto with lattice_hints typeclass_instances. + - intros. + apply path_trunctype ; apply prod_unit_l. + - intros. + apply path_trunctype ; apply prod_unit_r. + - eauto with lattice_hints typeclass_instances. + Defined. +End relations. \ No newline at end of file diff --git a/FiniteSets/fsets/monad.v b/FiniteSets/kuratowski/monad.v similarity index 100% rename from FiniteSets/fsets/monad.v rename to FiniteSets/kuratowski/monad.v diff --git a/FiniteSets/fsets/operations.v b/FiniteSets/kuratowski/operations.v similarity index 51% rename from FiniteSets/fsets/operations.v rename to FiniteSets/kuratowski/operations.v index 034fe0d..4cfe74d 100644 --- a/FiniteSets/fsets/operations.v +++ b/FiniteSets/kuratowski/operations.v @@ -1,27 +1,45 @@ -(* Operations on the [FSet A] for an arbitrary [A] *) +(** Operations on the [FSet A] for an arbitrary [A] *) Require Import HoTT HitTactics. -Require Import representations.definition disjunction lattice. +Require Import kuratowski_sets monad_interface. Section operations. - Context `{Univalence}. - - Global Instance fset_member : forall A, hasMembership (FSet A) A. + (** Monad operations. *) + Definition fset_fmap {A B : Type} : (A -> B) -> FSet A -> FSet B. Proof. - intros A a. + intro f. hrecursion. - - exists Empty. - exact _. - - intro a'. - exists (Trunc (-1) (a = a')). - exact _. - - apply lor. - - intros ; symmetry ; apply lor_assoc. - - apply lor_commutative. - - apply lor_nl. - - apply lor_nr. - - intros ; apply lor_idem. + - exact ∅. + - apply (fun a => {|f a|}). + - apply (∪). + - apply assoc. + - apply comm. + - apply nl. + - apply nr. + - apply (idem o f). Defined. + Global Instance fset_pure : hasPure FSet. + Proof. + split. + apply (fun _ a => {|a|}). + Defined. + + Global Instance fset_bind : hasBind FSet. + Proof. + split. + intros A. + hrecursion. + - exact ∅. + - exact idmap. + - apply (∪). + - apply assoc. + - apply comm. + - apply nl. + - apply nr. + - apply union_idem. + Defined. + + (** Set-theoretical operations. *) Global Instance fset_comprehension : forall A, hasComprehension (FSet A) A. Proof. intros A P. @@ -54,11 +72,12 @@ Section operations. - intro b. apply {|(a, b)|}. - apply (∪). - - intros X Y Z ; apply assoc. - - intros X Y ; apply comm. - - intros ; apply nl. - - intros ; apply nr. - - intros ; apply idem. + - apply assoc. + - apply comm. + - apply nl. + - apply nr. + - intros. + apply idem. Defined. Definition product {A B : Type} : FSet A -> FSet B -> FSet (A * B). @@ -69,39 +88,13 @@ Section operations. - intro a. apply (single_product a Y). - apply (∪). - - intros ; apply assoc. - - intros ; apply comm. - - intros ; apply nl. - - intros ; apply nr. + - apply assoc. + - apply comm. + - apply nl. + - apply nr. - intros ; apply union_idem. Defined. - Global Instance fset_subset : forall A, hasSubset (FSet A). - Proof. - intros A X Y. - hrecursion X. - - exists Unit. - exact _. - - intros a. - apply (a ∈ Y). - - intros X1 X2. - exists (prod X1 X2). - exact _. - - intros. - apply path_trunctype ; apply equiv_prod_assoc. - - intros. - apply path_trunctype ; apply equiv_prod_symm. - - intros. - apply path_trunctype ; apply prod_unit_l. - - intros. - apply path_trunctype ; apply prod_unit_r. - - intros a'. - apply path_iff_hprop ; cbn. - * intros [p1 p2]. apply p1. - * intros p. - split ; apply p. - Defined. - Local Ltac remove_transport := intros ; apply path_forall ; intro Z ; rewrite transport_arrow ; rewrite transport_const ; simpl. @@ -111,7 +104,10 @@ Section operations. ; f_ap ; hott_simpl ; simple refine (path_sigma _ _ _ _ _) ; try (apply transport_const) ; try (apply path_ishprop). - Lemma separation (A B : Type) : forall (X : FSet A) (f : {a | a ∈ X} -> B), FSet B. + Context `{Univalence}. + + (** Separation axiom for finite sets. *) + Definition separation (A B : Type) : forall (X : FSet A) (f : {a | a ∈ X} -> B), FSet B. Proof. hinduction. - intros f. @@ -140,5 +136,48 @@ Section operations. rewrite <- (idem (Z (x; tr 1%path))). pointwise. Defined. - End operations. + +Section operations_decidable. + Context {A : Type}. + Context {A_deceq : DecidablePaths A}. + Context `{Univalence}. + + Global Instance isIn_decidable (a : A) : forall (X : FSet A), + Decidable (a ∈ X). + 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 _. + 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 subset_decidable : forall (X Y : FSet A), Decidable (X ⊆ Y). + Proof. + hinduction ; try (intros ; apply path_ishprop). + - apply _. + - apply _. + - unfold subset in *. + apply _. + Defined. + + Global Instance fset_subset_bool : hasSubset_decidable (FSet A). + Proof. + intros X Y. + apply (if (dec (X ⊆ Y)) then true else false). + Defined. + + Global Instance fset_intersection : hasIntersection (FSet A) + := fun X Y => {|X & (fun a => a ∈_d Y)|}. +End operations_decidable. \ No newline at end of file diff --git a/FiniteSets/fsets/operations_decidable.v b/FiniteSets/kuratowski/operations_decidable.v similarity index 100% rename from FiniteSets/fsets/operations_decidable.v rename to FiniteSets/kuratowski/operations_decidable.v diff --git a/FiniteSets/fsets/properties.v b/FiniteSets/kuratowski/properties.v similarity index 57% rename from FiniteSets/fsets/properties.v rename to FiniteSets/kuratowski/properties.v index 594561d..aaba4cf 100644 --- a/FiniteSets/fsets/properties.v +++ b/FiniteSets/kuratowski/properties.v @@ -1,14 +1,11 @@ Require Import HoTT HitTactics. -From fsets Require Import operations extensionality. -Require Export representations.definition disjunction. -Require Import lattice. +Require Import kuratowski.extensionality kuratowski.operations kuratowski_sets. +Require Import lattice_interface lattice_examples monad_interface. -(* Lemmas relating operations to the membership predicate *) -Section characterize_isIn. - Context {A : Type}. - Context `{Univalence}. +(** Lemmas relating operations to the membership predicate *) +Section properties_membership. + Context {A : Type} `{Univalence}. - (** isIn properties *) Definition empty_isIn (a: A) : a ∈ ∅ -> Empty := idmap. Definition singleton_isIn (a b: A) : a ∈ {|b|} -> Trunc (-1) (a = b) := idmap. @@ -52,11 +49,8 @@ Section characterize_isIn. destruct Z ; assumption. ** intros ; apply tr ; right ; assumption. Defined. -End characterize_isIn. -Section product_isIn. - Context {A B : Type}. - Context `{Univalence}. + Context {B : Type}. Lemma isIn_singleproduct (a : A) (b : B) (c : A) : forall (Y : FSet B), (a, b) ∈ (single_product c Y) = land (BuildhProp (Trunc (-1) (a = c))) (b ∈ Y). @@ -75,8 +69,10 @@ Section product_isIn. - intros X1 X2 HX1 HX2. apply path_iff_hprop ; rewrite ?union_isIn. * intros X. + cbn in *. strip_truncations. - destruct X as [H1 | H1] ; rewrite ?HX1, ?HX2 in H1 ; destruct H1 as [H1 H2]. + destruct X as [H1 | H1] ; rewrite ?HX1, ?HX2 in H1 + ; destruct H1 as [H1 H2]. ** split. *** apply H1. *** apply (tr(inl H2)). @@ -84,6 +80,7 @@ Section product_isIn. *** apply H1. *** apply (tr(inr H2)). * intros [H1 H2]. + cbn in *. strip_truncations. apply tr. rewrite HX1, HX2. @@ -102,7 +99,7 @@ Section product_isIn. - intros. apply isIn_singleproduct. - intros X1 X2 HX1 HX2. - rewrite (union_isIn (product X1 Y)). + cbn. rewrite HX1, HX2. apply path_iff_hprop ; rewrite ?union_isIn. * intros X. @@ -116,7 +113,100 @@ Section product_isIn. ** left ; split ; assumption. ** right ; split ; assumption. Defined. -End product_isIn. + + Lemma separation_isIn : forall (X : FSet A) (f : {a | a ∈ X} -> B) (b : B), + b ∈ (separation A B X f) = hexists (fun a : A => hexists (fun (p : a ∈ X) => f (a;p) = b)). + Proof. + hinduction ; try (intros ; apply path_forall ; intro ; apply path_ishprop). + - intros ; simpl. + apply path_iff_hprop ; try contradiction. + intros X. + strip_truncations. + destruct X as [a X]. + strip_truncations. + destruct X as [p X]. + assumption. + - intros. + apply path_iff_hprop ; simpl. + * intros ; strip_truncations. + apply tr. + exists a. + apply tr. + exists (tr idpath). + apply X^. + * intros X ; strip_truncations. + destruct X as [a0 X]. + strip_truncations. + destruct X as [X q]. + simple refine (Trunc_ind _ _ X). + intros p. + apply tr. + rewrite <- q. + f_ap. + simple refine (path_sigma _ _ _ _ _). + ** apply p. + ** apply path_ishprop. + - intros X1 X2 HX1 HX2 f b. + pose (fX1 := fun Z : {a : A & a ∈ X1} => f (pr1 Z;tr (inl (pr2 Z)))). + pose (fX2 := fun Z : {a : A & a ∈ X2} => f (pr1 Z;tr (inr (pr2 Z)))). + specialize (HX1 fX1 b). + specialize (HX2 fX2 b). + apply path_iff_hprop. + * intros X. + cbn in *. + strip_truncations. + destruct X as [X | X]. + ** rewrite HX1 in X. + strip_truncations. + destruct X as [a Ha]. + apply tr. + exists a. + strip_truncations. + destruct Ha as [p pa]. + apply tr. + exists (tr(inl p)). + rewrite <- pa. + reflexivity. + ** rewrite HX2 in X. + strip_truncations. + destruct X as [a Ha]. + apply tr. + exists a. + strip_truncations. + destruct Ha as [p pa]. + apply tr. + exists (tr(inr p)). + rewrite <- pa. + reflexivity. + * intros. + strip_truncations. + destruct X as [a X]. + strip_truncations. + destruct X as [Ha p]. + cbn. + simple refine (Trunc_ind _ _ Ha) ; intros [Ha1 | Ha2]. + ** refine (tr(inl _)). + rewrite HX1. + apply tr. + exists a. + apply tr. + exists Ha1. + rewrite <- p. + unfold fX1. + repeat f_ap. + apply path_ishprop. + ** refine (tr(inr _)). + rewrite HX2. + apply tr. + exists a. + apply tr. + exists Ha2. + rewrite <- p. + unfold fX2. + repeat f_ap. + apply path_ishprop. + Defined. +End properties_membership. Ltac simplify_isIn := repeat (rewrite union_isIn @@ -127,10 +217,9 @@ Ltac toHProp := apply fset_ext ; intros ; simplify_isIn ; eauto with lattice_hints typeclass_instances. -(* Other properties *) -Section properties. +(** [FSet A] is a join semilattice. *) +Section fset_join_semilattice. Context {A : Type}. - Context `{Univalence}. Instance: bottom(FSet A). Proof. @@ -146,10 +235,223 @@ Section properties. Global Instance joinsemilattice_fset : JoinSemiLattice (FSet A). Proof. - split ; toHProp. + split. + - intros ? ?. + apply comm. + - intros ? ? ?. + apply (assoc _ _ _)^. + - intros ?. + apply union_idem. + - intros x. + apply nl. + - intros ?. + apply nr. + Defined. +End fset_join_semilattice. + +(* Lemmas relating operations to the membership predicate *) +Section properties_membership_decidable. + 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. - (** comprehension properties *) + 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. + + Lemma singleton_isIn_d_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 singleton_isIn_d_aa (a : A) : + a ∈_d {|a|} = true. + Proof. + apply singleton_isIn_d_true ; reflexivity. + Defined. + + Lemma singleton_isIn_d_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. + + Lemma union_isIn_d (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_d (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_d (X Y: FSet A) (a : A) : + a ∈_d (intersection X Y) = andb (a ∈_d X) (a ∈_d Y). + Proof. + apply comprehension_isIn_d. + Defined. +End properties_membership_decidable. + +(* Some suporting tactics *) +Ltac simplify_isIn_d := + repeat (rewrite union_isIn_d + || rewrite singleton_isIn_d_aa + || rewrite intersection_isIn_d + || rewrite comprehension_isIn_d). + +Ltac toBool := + repeat intro; + apply ext ; intros ; + simplify_isIn_d ; eauto with bool_lattice_hints typeclass_instances. + +(** If `A` has decidable equality, then `FSet A` is a lattice *) +Section set_lattice. + 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 set_lattice. + +(** If `A` has decidable equality, then so has `FSet A`. *) +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. + +(** [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}. + Lemma comprehension_false : forall (X : FSet A), {|X & fun _ => false|} = ∅. Proof. toHProp. @@ -176,6 +478,11 @@ Section properties. Proof. toHProp. Defined. +End comprehension_properties. + +(** For [FSet A] we have mere choice. *) +Section mere_choice. + Context {A : Type} `{Univalence}. Local Ltac solve_mc := repeat (let x := fresh in intro x ; try(destruct x)) @@ -219,98 +526,4 @@ Section properties. - solve_mc. - solve_mc. Defined. - - Lemma separation_isIn (B : Type) : forall (X : FSet A) (f : {a | a ∈ X} -> B) (b : B), - b ∈ (separation A B X f) = hexists (fun a : A => hexists (fun (p : a ∈ X) => f (a;p) = b)). - Proof. - hinduction ; try (intros ; apply path_forall ; intro ; apply path_ishprop). - - intros ; simpl. - apply path_iff_hprop ; try contradiction. - intros X. - strip_truncations. - destruct X as [a X]. - strip_truncations. - destruct X as [p X]. - assumption. - - intros. - apply path_iff_hprop ; simpl. - * intros ; strip_truncations. - apply tr. - exists a. - apply tr. - exists (tr idpath). - apply X^. - * intros X ; strip_truncations. - destruct X as [a0 X]. - strip_truncations. - destruct X as [X q]. - simple refine (Trunc_ind _ _ X). - intros p. - apply tr. - rewrite <- q. - f_ap. - simple refine (path_sigma _ _ _ _ _). - ** apply p. - ** apply path_ishprop. - - intros X1 X2 HX1 HX2 f b. - pose (fX1 := fun Z : {a : A & a ∈ X1} => f (pr1 Z;tr (inl (pr2 Z)))). - pose (fX2 := fun Z : {a : A & a ∈ X2} => f (pr1 Z;tr (inr (pr2 Z)))). - specialize (HX1 fX1 b). - specialize (HX2 fX2 b). - apply path_iff_hprop. - * intros X. - rewrite union_isIn in X. - strip_truncations. - destruct X as [X | X]. - ** rewrite HX1 in X. - strip_truncations. - destruct X as [a Ha]. - apply tr. - exists a. - strip_truncations. - destruct Ha as [p pa]. - apply tr. - exists (tr(inl p)). - rewrite <- pa. - reflexivity. - ** rewrite HX2 in X. - strip_truncations. - destruct X as [a Ha]. - apply tr. - exists a. - strip_truncations. - destruct Ha as [p pa]. - apply tr. - exists (tr(inr p)). - rewrite <- pa. - reflexivity. - * intros. - strip_truncations. - destruct X as [a X]. - strip_truncations. - destruct X as [Ha p]. - rewrite union_isIn. - simple refine (Trunc_ind _ _ Ha) ; intros [Ha1 | Ha2]. - ** refine (tr(inl _)). - rewrite HX1. - apply tr. - exists a. - apply tr. - exists Ha1. - rewrite <- p. - unfold fX1. - repeat f_ap. - apply path_ishprop. - ** refine (tr(inr _)). - rewrite HX2. - apply tr. - exists a. - apply tr. - exists Ha2. - rewrite <- p. - unfold fX2. - repeat f_ap. - apply path_ishprop. - Defined. - -End properties. +End mere_choice. diff --git a/FiniteSets/fsets/properties_decidable.v b/FiniteSets/kuratowski/properties_decidable.v similarity index 100% rename from FiniteSets/fsets/properties_decidable.v rename to FiniteSets/kuratowski/properties_decidable.v diff --git a/FiniteSets/lattice.v b/FiniteSets/lattice.v deleted file mode 100644 index 97358eb..0000000 --- a/FiniteSets/lattice.v +++ /dev/null @@ -1,205 +0,0 @@ -(* Typeclass for lattices *) -Require Import HoTT. -Require Import notation. - -Section binary_operation. - Variable A : Type. - - Class maximum := - max_L : operation A. - - Class minimum := - min_L : operation A. - - Class bottom := - empty : A. -End binary_operation. - -Arguments max_L {_} {_} _. -Arguments min_L {_} {_} _. -Arguments empty {_}. - -Section JoinSemiLattice. - Variable A : Type. - Context {max_L : maximum A} {empty_L : bottom A}. - - Class JoinSemiLattice := - { - commutative_max_js :> Commutative max_L ; - associative_max_js :> Associative max_L ; - idempotent_max_js :> Idempotent max_L ; - neutralL_max_js :> NeutralL max_L empty_L ; - neutralR_max_js :> NeutralR max_L empty_L ; - }. -End JoinSemiLattice. - -Arguments JoinSemiLattice _ {_} {_}. - -Create HintDb joinsemilattice_hints. -Hint Resolve associativity : joinsemilattice_hints. -Hint Resolve (associativity _ _ _)^ : joinsemilattice_hints. -Hint Resolve commutative : joinsemilattice_hints. -Hint Resolve idempotency : joinsemilattice_hints. -Hint Resolve neutralityL : joinsemilattice_hints. -Hint Resolve neutralityR : joinsemilattice_hints. - -Section Lattice. - Variable A : Type. - Context {max_L : maximum A} {min_L : minimum A} {empty_L : bottom A}. - - Class Lattice := - { - commutative_min :> Commutative min_L ; - commutative_max :> Commutative max_L ; - associative_min :> Associative min_L ; - associative_max :> Associative max_L ; - idempotent_min :> Idempotent min_L ; - idempotent_max :> Idempotent max_L ; - neutralL_max :> NeutralL max_L empty_L ; - neutralR_max :> NeutralR max_L empty_L ; - absorption_min_max :> Absorption min_L max_L ; - absorption_max_min :> Absorption max_L min_L - }. -End Lattice. - -Arguments Lattice _ {_} {_} {_}. - -Create HintDb lattice_hints. -Hint Resolve associativity : lattice_hints. -Hint Resolve (associativity _ _ _)^ : lattice_hints. -Hint Resolve commutative : lattice_hints. -Hint Resolve absorb : lattice_hints. -Hint Resolve idempotency : lattice_hints. -Hint Resolve neutralityL : lattice_hints. -Hint Resolve neutralityR : lattice_hints. - -Section BoolLattice. - - Ltac solve_bool := - let x := fresh in - repeat (intro x ; destruct x) - ; compute - ; auto - ; try contradiction. - - Instance maximum_bool : maximum Bool := orb. - Instance minimum_bool : minimum Bool := andb. - Instance bottom_bool : bottom Bool := false. - - Global Instance lattice_bool : Lattice Bool. - Proof. - split ; solve_bool. - Defined. - - Definition and_true : forall b, andb b true = b. - Proof. - solve_bool. - Defined. - - Definition and_false : forall b, andb b false = false. - Proof. - solve_bool. - Defined. - - Definition dist₁ : forall b₁ b₂ b₃, - andb b₁ (orb b₂ b₃) = orb (andb b₁ b₂) (andb b₁ b₃). - Proof. - solve_bool. - Defined. - - Definition dist₂ : forall b₁ b₂ b₃, - orb b₁ (andb b₂ b₃) = andb (orb b₁ b₂) (orb b₁ b₃). - Proof. - solve_bool. - Defined. - - Definition max_min : forall b₁ b₂, - orb (andb b₁ b₂) b₁ = b₁. - Proof. - solve_bool. - Defined. - -End BoolLattice. - -Section fun_lattice. - Context {A B : Type}. - Context `{Lattice B}. - Context `{Funext}. - - Global Instance max_fun : maximum (A -> B) := - fun (f g : A -> B) (a : A) => max_L0 (f a) (g a). - - Global Instance min_fun : minimum (A -> B) := - fun (f g : A -> B) (a : A) => min_L0 (f a) (g a). - - Global Instance bot_fun : bottom (A -> B) - := fun _ => empty_L. - - Ltac solve_fun := - compute ; intros ; apply path_forall ; intro ; - eauto with lattice_hints typeclass_instances. - - Global Instance lattice_fun : Lattice (A -> B). - Proof. - split ; solve_fun. - Defined. - -End fun_lattice. - -Section sub_lattice. - Context {A : Type} {P : A -> hProp}. - Context `{Lattice A}. - Context {Hmax : forall x y, P x -> P y -> P (max_L0 x y)}. - Context {Hmin : forall x y, P x -> P y -> P (min_L0 x y)}. - Context {Hbot : P empty_L}. - - Definition AP : Type := sig P. - - Instance botAP : bottom AP := (empty_L ; Hbot). - - Instance maxAP : maximum AP := - fun x y => - match x, y with - | (a ; pa), (b ; pb) => (max_L0 a b ; Hmax a b pa pb) - end. - - Instance minAP : minimum AP := - fun x y => - match x, y with - | (a ; pa), (b ; pb) => (min_L0 a b ; Hmin a b pa pb) - end. - - Instance hprop_sub : forall c, IsHProp (P c). - Proof. - apply _. - Defined. - - Ltac solve_sub := - let x := fresh in - repeat (intro x ; destruct x) - ; simple refine (path_sigma _ _ _ _ _) - ; simpl - ; try (apply hprop_sub) - ; eauto 3 with lattice_hints typeclass_instances. - - Global Instance lattice_sub : Lattice AP. - Proof. - split ; solve_sub. - Defined. - -End sub_lattice. - -Create HintDb bool_lattice_hints. -Hint Resolve associativity : bool_lattice_hints. -Hint Resolve (associativity _ _ _)^ : bool_lattice_hints. -Hint Resolve commutative : bool_lattice_hints. -Hint Resolve absorb : bool_lattice_hints. -Hint Resolve idempotency : bool_lattice_hints. -Hint Resolve neutralityL : bool_lattice_hints. -Hint Resolve neutralityR : bool_lattice_hints. - -Hint Resolve - associativity - and_true and_false - dist₁ dist₂ max_min - : bool_lattice_hints. diff --git a/FiniteSets/fsets/isomorphism.v b/FiniteSets/list_representation/isomorphism.v similarity index 95% rename from FiniteSets/fsets/isomorphism.v rename to FiniteSets/list_representation/isomorphism.v index 10d88fc..5a16b63 100644 --- a/FiniteSets/fsets/isomorphism.v +++ b/FiniteSets/list_representation/isomorphism.v @@ -1,15 +1,16 @@ (* The representations [FSet A] and [FSetC A] are isomorphic for every A *) Require Import HoTT HitTactics. -From representations Require Import cons_repr definition. -From fsets Require Import operations_cons_repr properties_cons_repr. +Require Import list_representation list_representation.operations + list_representation.properties. +Require Import kuratowski.kuratowski_sets. 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 _ _ _)^. @@ -110,18 +111,18 @@ Section Iso. 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. + - intros a Y PY. refine (_ @ (Pdupl _ _ _)). etransitivity. { apply (transport_compose _ FSetC_to_FSet (dupl a Y)). } refine (ap (fun z => transport P z _) _). - apply FSetC_rec_beta_dupl. + apply path_ishprop. - 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. + apply path_ishprop. Defined. Theorem FSet_cons_ind_beta_empty (P : FSet A -> Type) @@ -133,7 +134,9 @@ Section Iso. (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. + Proof. + by compute. + Defined. (* TODO *) (* Theorem FSet_cons_ind_beta_cons (P : FSet A -> Type) *) diff --git a/FiniteSets/list_representation/list_representation.v b/FiniteSets/list_representation/list_representation.v new file mode 100644 index 0000000..f3d5f95 --- /dev/null +++ b/FiniteSets/list_representation/list_representation.v @@ -0,0 +1,84 @@ +(** Definition of Finite Sets as via lists. *) +Require Import HoTT HitTactics. +Require Export set_names. + +Module Export FSetC. + + Section FSetC. + Private Inductive FSetC (A : Type) : Type := + | Nil : FSetC A + | Cns : A -> FSetC A -> FSetC A. + + Global Instance fset_empty : forall A,hasEmpty (FSetC A) := Nil. + + Variable A : Type. + Arguments Cns {_} _ _. + Infix ";;" := Cns (at level 8, right associativity). + + Axiom dupl : forall (a : A) (x : FSetC A), + a ;; a ;; x = a ;; x. + + Axiom comm : forall (a b : A) (x : FSetC A), + a ;; b ;; x = b ;; a ;; x. + + Axiom trunc : IsHSet (FSetC A). + End FSetC. + + Arguments Cns {_} _ _. + Arguments dupl {_} _ _. + Arguments comm {_} _ _ _. + + Infix ";;" := Cns (at level 8, right associativity). + + Section FSetC_induction. + Variable (A : Type) + (P : FSetC A -> Type) + (H : forall x : FSetC A, IsHSet (P x)) + (eP : P ∅) + (cnsP : forall (a:A) (x: FSetC A), P x -> P (a ;; x)) + (duplP : forall (a: A) (x: FSetC A) (px : P x), + dupl a x # cnsP a (a;;x) (cnsP a x px) = cnsP a x px) + (commP : forall (a b: A) (x: FSetC A) (px: P x), + comm a b x # cnsP a (b;;x) (cnsP b x px) = + cnsP b (a;;x) (cnsP a x px)). + + (* Induction principle *) + Fixpoint FSetC_ind + (x : FSetC A) + {struct x} + : P x + := (match x return _ -> _ -> _ -> P x with + | Nil => fun _ => fun _ => fun _ => eP + | a ;; y => fun _ => fun _ => fun _ => cnsP a y (FSetC_ind y) + end) H duplP commP. + End FSetC_induction. + + Section FSetC_recursion. + Variable (A : Type) + (P : Type) + (H : IsHSet P) + (nil : P) + (cns : A -> P -> P) + (duplP : forall (a: A) (x: P), cns a (cns a x) = (cns a x)) + (commP : forall (a b: A) (x: P), cns a (cns b x) = cns b (cns a x)). + + (* Recursion principle *) + Definition FSetC_rec : FSetC A -> P. + Proof. + simple refine (FSetC_ind _ _ _ _ _ _ _ ); + try (intros; simple refine ((transport_const _ _) @ _ )); cbn. + - apply nil. + - apply (fun a => fun _ => cns a). + - apply duplP. + - apply commP. + Defined. + End FSetC_recursion. + + Instance FSetC_recursion A : HitRecursion (FSetC A) := + { + indTy := _; recTy := _; + H_inductor := FSetC_ind A; H_recursor := FSetC_rec A + }. +End FSetC. + +Infix ";;" := Cns (at level 8, right associativity). diff --git a/FiniteSets/fsets/operations_cons_repr.v b/FiniteSets/list_representation/operations.v similarity index 79% rename from FiniteSets/fsets/operations_cons_repr.v rename to FiniteSets/list_representation/operations.v index 57850cc..d6b87a8 100644 --- a/FiniteSets/fsets/operations_cons_repr.v +++ b/FiniteSets/list_representation/operations.v @@ -1,6 +1,6 @@ -(* Operations on [FSetC A] *) +(** Operations on [FSetC A] *) Require Import HoTT HitTactics. -Require Import representations.cons_repr. +Require Import list_representation. Section operations. Global Instance fsetc_union : forall A, hasUnion (FSetC A). diff --git a/FiniteSets/fsets/properties_cons_repr.v b/FiniteSets/list_representation/properties.v similarity index 70% rename from FiniteSets/fsets/properties_cons_repr.v rename to FiniteSets/list_representation/properties.v index dbb02be..a09187f 100644 --- a/FiniteSets/fsets/properties_cons_repr.v +++ b/FiniteSets/list_representation/properties.v @@ -1,7 +1,6 @@ -(* Properties of the operations on [FSetC A] *) +(** Properties of the operations on [FSetC A] *) Require Import HoTT HitTactics. -Require Import representations.cons_repr. -From fsets Require Import operations_cons_repr. +Require Import list_representation list_representation.operations. Section properties. Context {A : Type}. @@ -12,8 +11,8 @@ Section properties. Lemma append_nr : forall (x: FSetC A), x ∪ ∅ = x. Proof. hinduction; try (intros; apply set_path2). - - reflexivity. - - intros. apply (ap (fun y => a;;y) X). + - reflexivity. + - intros. apply (ap (fun y => a;;y) X). Defined. Lemma append_assoc {H: Funext}: @@ -42,21 +41,18 @@ Section properties. forall (x1 x2: FSetC A), x1 ∪ x2 = x2 ∪ x1. Proof. hinduction ; try (intros ; apply path_forall ; intro ; apply set_path2). - - intros. symmetry. apply append_nr. + - intros. + apply (append_nr _)^. - intros a x1 HR x2. - etransitivity. - apply (ap (fun y => a;;y) (HR x2)). - transitivity ((x2 ∪ x1) ∪ (a;;∅)). - + apply append_singleton. - + etransitivity. - * symmetry. apply append_assoc. - * simple refine (ap (x2 ∪) (append_singleton _ _)^). + refine (ap (fun y => a;;y) (HR x2) @ _). + refine (append_singleton _ _ @ _). + refine ((append_assoc _ _ _)^ @ _). + refine (ap (x2 ∪) (append_singleton _ _)^). Defined. Lemma singleton_idem: forall (a: A), {|a|} ∪ {|a|} = {|a|}. Proof. - unfold singleton. intro. apply dupl. Defined. diff --git a/FiniteSets/misc/T.v b/FiniteSets/misc/T.v new file mode 100644 index 0000000..348d6d1 --- /dev/null +++ b/FiniteSets/misc/T.v @@ -0,0 +1,62 @@ +(** Merely decidable equality implies LEM *) +Require Import HoTT HitTactics prelude. + +Section TR. + Context `{Univalence}. + Variable A : hProp. + + Definition T := Unit + Unit. + + Definition R (x y : T) : hProp := + match x, y with + | inl tt, inl tt => Unit_hp + | inl tt, inr tt => A + | inr tt, inl tt => A + | inr tt, inr tt => Unit_hp + end. + + Global Instance R_refl : Reflexive R. + Proof. + intro x ; destruct x as [[ ] | [ ]] ; apply tt. + Defined. + + Global Instance R_sym : Symmetric R. + Proof. + repeat (let x := fresh in intro x ; destruct x as [[ ] | [ ]]) + ; auto ; apply tt. + Defined. + + Global Instance R_trans : Transitive R. + Proof. + repeat (let x := fresh in intro x ; destruct x as [[ ] | [ ]]) ; intros + ; auto ; apply tt. + Defined. + + Definition TR : Type := quotient R. + Definition TR_zero : TR := class_of R (inl tt). + Definition TR_one : TR := class_of R (inr tt). + + Definition equiv_pathspace_T : (TR_zero = TR_one) = (R (inl tt) (inr tt)) + := path_universe (sets_exact R (inl tt) (inr tt)). + + Global Instance quotientB_recursion : HitRecursion TR := + { + indTy := _; + recTy := + forall (P : Type) (HP: IsHSet P) (u : T -> P), + (forall x y : T, R x y -> u x = u y) -> TR -> P; + H_inductor := quotient_ind R ; + H_recursor := @quotient_rec _ R _ + }. +End TR. + +Theorem merely_dec `{Univalence} : (forall (A : Type) (a b : A), hor (a = b) (~a = b)) + -> + forall (A : hProp), A + (~A). +Proof. + intros X A. + specialize (X (TR A) (TR_zero A) (TR_one A)). + rewrite equiv_pathspace_T in X. + strip_truncations. + apply X. +Defined. \ No newline at end of file diff --git a/FiniteSets/misc/bad.v b/FiniteSets/misc/bad.v new file mode 100644 index 0000000..2821de2 --- /dev/null +++ b/FiniteSets/misc/bad.v @@ -0,0 +1,288 @@ +(* This is a /bad/ definition of FSets, without the 0-truncation. + Here we show that the resulting type is not an h-set. *) +Require Import HoTT HitTactics. +Require Import set_names. + +Module Export FSet. + + Section FSet. + Private Inductive FSet (A : Type): Type := + | E : FSet A + | L : A -> FSet A + | U : FSet A -> FSet A -> FSet A. + + Global Instance fset_empty : forall A, hasEmpty (FSet A) := E. + Global Instance fset_singleton : forall A, hasSingleton (FSet A) A := L. + Global Instance fset_union : forall A, hasUnion (FSet A) := U. + + Variable A : Type. + + Axiom assoc : forall (x y z : FSet A), + x ∪ (y ∪ z) = (x ∪ y) ∪ z. + + Axiom comm : forall (x y : FSet A), + x ∪ y = y ∪ x. + + Axiom nl : forall (x : FSet A), + ∅ ∪ x = x. + + Axiom nr : forall (x : FSet A), + x ∪ ∅ = x. + + Axiom idem : forall (x : A), + {|x|} ∪ {|x|} = {|x|}. + + End FSet. + + Arguments assoc {_} _ _ _. + Arguments comm {_} _ _. + Arguments nl {_} _. + Arguments nr {_} _. + Arguments idem {_} _. + + Section FSet_induction. + Variable A: Type. + Variable (P : FSet A -> Type). + Variable (eP : P ∅). + Variable (lP : forall a: A, P {|a |}). + Variable (uP : forall (x y: FSet A), P x -> P y -> P (x ∪ y)). + Variable (assocP : forall (x y z : FSet A) + (px: P x) (py: P y) (pz: P z), + assoc x y z # + (uP x (y ∪ z) px (uP y z py pz)) + = + (uP (x ∪ y) z (uP x y px py) pz)). + Variable (commP : forall (x y: FSet A) (px: P x) (py: P y), + comm x y # + uP x y px py = uP y x py px). + Variable (nlP : forall (x : FSet A) (px: P x), + nl x # uP ∅ x eP px = px). + Variable (nrP : forall (x : FSet A) (px: P x), + nr x # uP x ∅ px eP = px). + Variable (idemP : forall (x : A), + idem x # uP {|x|} {|x|} (lP x) (lP x) = lP x). + + (* Induction principle *) + Fixpoint FSet_ind + (x : FSet A) + {struct x} + : P x + := (match x return _ -> _ -> _ -> _ -> _ -> P x with + | E => fun _ _ _ _ _ => eP + | L a => fun _ _ _ _ _ => lP a + | U y z => fun _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z) + end) assocP commP nlP nrP idemP. + + Axiom FSet_ind_beta_assoc : forall (x y z : FSet A), + apD FSet_ind (assoc x y z) = + (assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)). + + Axiom FSet_ind_beta_comm : forall (x y : FSet A), + apD FSet_ind (comm x y) = commP x y (FSet_ind x) (FSet_ind y). + + Axiom FSet_ind_beta_nl : forall (x : FSet A), + apD FSet_ind (nl x) = nlP x (FSet_ind x). + + Axiom FSet_ind_beta_nr : forall (x : FSet A), + apD FSet_ind (nr x) = nrP x (FSet_ind x). + + Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x. + End FSet_induction. + + Section FSet_recursion. + + Variable A : Type. + Variable P : Type. + Variable e : P. + Variable l : A -> P. + Variable u : P -> P -> P. + Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z. + Variable commP : forall (x y : P), u x y = u y x. + Variable nlP : forall (x : P), u e x = x. + Variable nrP : forall (x : P), u x e = x. + Variable idemP : forall (x : A), u (l x) (l x) = l x. + + Definition FSet_rec : FSet A -> P. + Proof. + simple refine (FSet_ind A _ _ _ _ _ _ _ _ _) ; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn. + - apply e. + - apply l. + - intros x y ; apply u. + - apply assocP. + - apply commP. + - apply nlP. + - apply nrP. + - apply idemP. + Defined. + + Definition FSet_rec_beta_assoc : forall (x y z : FSet A), + ap FSet_rec (assoc x y z) + = + assocP (FSet_rec x) (FSet_rec y) (FSet_rec z). + Proof. + intros. + unfold FSet_rec. + eapply (cancelL (transport_const (assoc x y z) _)). + simple refine ((apD_const _ _)^ @ _). + apply FSet_ind_beta_assoc. + Defined. + + Definition FSet_rec_beta_comm : forall (x y : FSet A), + ap FSet_rec (comm x y) + = + commP (FSet_rec x) (FSet_rec y). + Proof. + intros. + unfold FSet_rec. + eapply (cancelL (transport_const (comm x y) _)). + simple refine ((apD_const _ _)^ @ _). + apply FSet_ind_beta_comm. + Defined. + + Definition FSet_rec_beta_nl : forall (x : FSet A), + ap FSet_rec (nl x) + = + nlP (FSet_rec x). + Proof. + intros. + unfold FSet_rec. + eapply (cancelL (transport_const (nl x) _)). + simple refine ((apD_const _ _)^ @ _). + apply FSet_ind_beta_nl. + Defined. + + Definition FSet_rec_beta_nr : forall (x : FSet A), + ap FSet_rec (nr x) + = + nrP (FSet_rec x). + Proof. + intros. + unfold FSet_rec. + eapply (cancelL (transport_const (nr x) _)). + simple refine ((apD_const _ _)^ @ _). + apply FSet_ind_beta_nr. + Defined. + + Definition FSet_rec_beta_idem : forall (a : A), + ap FSet_rec (idem a) + = + idemP a. + Proof. + intros. + unfold FSet_rec. + eapply (cancelL (transport_const (idem a) _)). + simple refine ((apD_const _ _)^ @ _). + apply FSet_ind_beta_idem. + Defined. + + End FSet_recursion. + + Instance FSet_recursion A : HitRecursion (FSet A) := + { + indTy := _; recTy := _; + H_inductor := FSet_ind A; H_recursor := FSet_rec A + }. + +End FSet. + +Section set_sphere. + From HoTT.HIT Require Import Circle. + Context `{Univalence}. + Instance S1_recursion : HitRecursion S1 := + { + indTy := _; recTy := _; + H_inductor := S1_ind; H_recursor := S1_rec + }. + + Variable A : Type. + + Definition f (x : S1) : x = x. + Proof. + hrecursion x. + - exact loop. + - refine (transport_paths_FlFr _ _ @ _). + hott_simpl. + Defined. + + Definition S1op (x y : S1) : S1. + Proof. + hrecursion y. + - exact x. (* x + base = x *) + - apply f. + Defined. + + Lemma S1op_nr (x : S1) : S1op x base = x. + Proof. reflexivity. Defined. + + Lemma S1op_nl (x : S1) : S1op base x = x. + Proof. + hrecursion x. + - exact loop. + - refine (transport_paths_FlFr loop _ @ _). + hott_simpl. + apply moveR_pM. apply moveR_pM. hott_simpl. + refine (ap_V _ _ @ _). + f_ap. apply S1_rec_beta_loop. + Defined. + + Lemma S1op_assoc (x y z : S1) : S1op x (S1op y z) = S1op (S1op x y) z. + Proof. + hrecursion z. + - reflexivity. + - refine (transport_paths_FlFr loop _ @ _). + hott_simpl. + apply moveR_Mp. hott_simpl. + rewrite S1_rec_beta_loop. + rewrite ap_compose. + rewrite S1_rec_beta_loop. + hrecursion y. + + symmetry. apply S1_rec_beta_loop. + + apply is1type_S1. + Qed. + + Lemma S1op_comm (x y : S1) : S1op x y = S1op y x. + Proof. + hrecursion x. + - apply S1op_nl. + - hrecursion y. + + rewrite transport_paths_FlFr. hott_simpl. + rewrite S1_rec_beta_loop. reflexivity. + + apply is1type_S1. + Defined. + + Definition FSet_to_S : FSet A -> S1. + Proof. + hrecursion. + - exact base. + - intro a. exact base. + - exact S1op. + - apply S1op_assoc. + - apply S1op_comm. + - apply S1op_nl. + - apply S1op_nr. + - simpl. reflexivity. + Defined. + + Lemma FSet_S_ap : (nl (E A)) = (nr ∅) -> idpath = loop. + Proof. + intros H1. + enough (ap FSet_to_S (nl ∅) = ap FSet_to_S (nr ∅)) as H'. + - rewrite FSet_rec_beta_nl in H'. + rewrite FSet_rec_beta_nr in H'. + simpl in H'. unfold S1op_nr in H'. + exact H'^. + - f_ap. + Defined. + + Lemma FSet_not_hset : IsHSet (FSet A) -> False. + Proof. + intros H1. + enough (idpath = loop). + - assert (S1_encode _ idpath = S1_encode _ (loopexp loop (pos Int.one))) as H' by f_ap. + rewrite S1_encode_loopexp in H'. simpl in H'. symmetry in H'. + apply (pos_neq_zero H'). + - apply FSet_S_ap. + apply set_path2. + Qed. + +End set_sphere. diff --git a/FiniteSets/misc/ordered.v b/FiniteSets/misc/ordered.v new file mode 100644 index 0000000..7dde386 --- /dev/null +++ b/FiniteSets/misc/ordered.v @@ -0,0 +1,274 @@ +(** If [A] has a total order, then we can pick the minimum of finite sets. *) +Require Import HoTT HitTactics. +Require Import kuratowski.kuratowski_sets kuratowski.operations kuratowski.properties. + +Definition relation A := A -> A -> Type. + +Section TotalOrder. + Class IsTop (A : Type) (R : relation A) (a : A) := + top_max : forall x, R x a. + + Class LessThan (A : Type) := + leq : relation A. + + Class Antisymmetric {A} (R : relation A) := + antisymmetry : forall x y, R x y -> R y x -> x = y. + + Class Total {A} (R : relation A) := + total : forall x y, x = y \/ R x y \/ R y x. + + Class TotalOrder (A : Type) {R : LessThan A} := + { TotalOrder_Reflexive :> Reflexive R | 2 ; + TotalOrder_Antisymmetric :> Antisymmetric R | 2; + TotalOrder_Transitive :> Transitive R | 2; + TotalOrder_Total :> Total R | 2; }. +End TotalOrder. + +Section minimum. + Context {A : Type}. + Context `{TotalOrder A}. + + Definition min (x y : A) : A. + Proof. + destruct (@total _ R _ x y). + - apply x. + - destruct s as [s | s]. + * apply x. + * apply y. + Defined. + + Lemma min_spec1 x y : R (min x y) x. + Proof. + unfold min. + destruct (total x y) ; simpl. + - reflexivity. + - destruct s as [ | t]. + * reflexivity. + * apply t. + Defined. + + Lemma min_spec2 x y z : R z x -> R z y -> R z (min x y). + Proof. + intros. + unfold min. + destruct (total x y) as [ | s]. + * assumption. + * try (destruct s) ; assumption. + Defined. + + Lemma min_comm x y : min x y = min y x. + Proof. + unfold min. + destruct (total x y) ; destruct (total y x) ; simpl. + - assumption. + - destruct s as [s | s] ; auto. + - destruct s as [s | s] ; symmetry ; auto. + - destruct s as [s | s] ; destruct s0 as [s0 | s0] ; try reflexivity. + * apply (@antisymmetry _ R _ _) ; assumption. + * apply (@antisymmetry _ R _ _) ; assumption. + Defined. + + Lemma min_idem x : min x x = x. + Proof. + unfold min. + destruct (total x x) ; simpl. + - reflexivity. + - destruct s ; reflexivity. + Defined. + + Lemma min_assoc x y z : min (min x y) z = min x (min y z). + Proof. + apply (@antisymmetry _ R _ _). + - apply min_spec2. + * etransitivity ; apply min_spec1. + * apply min_spec2. + ** etransitivity ; try (apply min_spec1). + simpl. + rewrite min_comm ; apply min_spec1. + ** rewrite min_comm ; apply min_spec1. + - apply min_spec2. + * apply min_spec2. + ** apply min_spec1. + ** etransitivity. + { rewrite min_comm ; apply min_spec1. } + apply min_spec1. + * transitivity (min y z); simpl + ; rewrite min_comm ; apply min_spec1. + Defined. + + Variable (top : A). + Context `{IsTop A R top}. + + Lemma min_nr x : min x top = x. + Proof. + intros. + unfold min. + destruct (total x top). + - reflexivity. + - destruct s. + * reflexivity. + * apply (@antisymmetry _ R _ _). + ** assumption. + ** refine (top_max _). apply _. + Defined. + + Lemma min_nl x : min top x = x. + Proof. + rewrite min_comm. + apply min_nr. + Defined. + + Lemma min_top_l x y : min x y = top -> x = top. + Proof. + unfold min. + destruct (total x y). + - apply idmap. + - destruct s as [s | s]. + * apply idmap. + * intros X. + rewrite X in s. + apply (@antisymmetry _ R _ _). + ** apply top_max. + ** assumption. + Defined. + + Lemma min_top_r x y : min x y = top -> y = top. + Proof. + rewrite min_comm. + apply min_top_l. + Defined. + +End minimum. + +Section add_top. + Variable (A : Type). + Context `{TotalOrder A}. + + Definition Top := A + Unit. + Definition top : Top := inr tt. + + Global Instance RTop : LessThan Top. + Proof. + unfold relation. + induction 1 as [a1 | ] ; induction 1 as [a2 | ]. + - apply (R a1 a2). + - apply Unit_hp. + - apply False_hp. + - apply Unit_hp. + Defined. + + Global Instance rtop_hprop : + is_mere_relation A R -> is_mere_relation Top RTop. + Proof. + intros P a b. + destruct a ; destruct b ; apply _. + Defined. + + Global Instance RTopOrder : TotalOrder Top. + Proof. + split. + - intros x ; induction x ; unfold RTop ; simpl. + * reflexivity. + * apply tt. + - intros x y ; induction x as [a1 | ] ; induction y as [a2 | ] ; unfold RTop ; simpl + ; try contradiction. + * intros ; f_ap. + apply (@antisymmetry _ R _ _) ; assumption. + * intros ; induction b ; induction b0. + reflexivity. + - intros x y z ; induction x as [a1 | b1] ; induction y as [a2 | b2] + ; induction z as [a3 | b3] ; unfold RTop ; simpl + ; try contradiction ; intros ; try (apply tt). + transitivity a2 ; assumption. + - intros x y. + unfold RTop ; simpl. + induction x as [a1 | b1] ; induction y as [a2 | b2] ; try (apply (inl idpath)). + * destruct (TotalOrder_Total a1 a2). + ** left ; f_ap ; assumption. + ** right ; assumption. + * apply (inr(inl tt)). + * apply (inr(inr tt)). + * left ; induction b1 ; induction b2 ; reflexivity. + Defined. + + Global Instance top_a_top : IsTop Top RTop top. + Proof. + intro x ; destruct x ; apply tt. + Defined. +End add_top. + +(** If [A] has a total order, then a nonempty finite set has a minimum element. *) +Section min_set. + Variable (A : Type). + Context `{TotalOrder A}. + Context `{is_mere_relation A R}. + Context `{Univalence} `{IsHSet A}. + + Definition min_set : FSet A -> Top A. + Proof. + hrecursion. + - apply (top A). + - apply inl. + - apply min. + - intros ; symmetry ; apply min_assoc. + - apply min_comm. + - apply min_nl. apply _. + - apply min_nr. apply _. + - intros ; apply min_idem. + Defined. + + Definition empty_min : forall (X : FSet A), min_set X = top A -> X = ∅. + Proof. + simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _) + ; try (intros ; apply path_forall ; intro q ; apply set_path2) + ; simpl. + - intros ; reflexivity. + - intros. + unfold top in X. + enough Empty. + { contradiction. } + refine (not_is_inl_and_inr' (inl a) _ _). + * apply tt. + * rewrite X ; apply tt. + - intros. + assert (min_set x = top A). + { + simple refine (min_top_l _ _ (min_set y) _) ; assumption. + } + rewrite (X X2). + rewrite nl. + assert (min_set y = top A). + { simple refine (min_top_r _ (min_set x) _ _) ; assumption. } + rewrite (X0 X3). + reflexivity. + Defined. + + Definition min_set_spec (a : A) : forall (X : FSet A), + a ∈ X -> RTop A (min_set X) (inl a). + Proof. + simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _) + ; try (intros ; apply path_ishprop) + ; simpl. + - contradiction. + - intros. + strip_truncations. + rewrite X. + reflexivity. + - intros. + strip_truncations. + unfold member in X, X0. + destruct X1. + * specialize (X t). + assert (RTop A (min (min_set x) (min_set y)) (min_set x)) as X1. + { apply min_spec1. } + etransitivity. + { apply X1. } + assumption. + * specialize (X0 t). + assert (RTop A (min (min_set x) (min_set y)) (min_set y)) as X1. + { rewrite min_comm ; apply min_spec1. } + etransitivity. + { apply X1. } + assumption. + Defined. +End min_set. \ No newline at end of file diff --git a/FiniteSets/variations/projective.v b/FiniteSets/misc/projective.v similarity index 97% rename from FiniteSets/variations/projective.v rename to FiniteSets/misc/projective.v index 100acbe..17999d9 100644 --- a/FiniteSets/variations/projective.v +++ b/FiniteSets/misc/projective.v @@ -1,7 +1,6 @@ Require Import HoTT HitTactics. -Require Import variations.k_finite variations.b_finite. -Require Import FSets. -Require Import representations.T. +Require Import subobjects.k_finite subobjects.b_finite FSets. +Require Import misc.T. Class IsProjective (X : Type) := projective : forall {P Q : Type} (p : P -> Q) (f : X -> Q), diff --git a/FiniteSets/ordered.v b/FiniteSets/ordered.v deleted file mode 100644 index f10ae97..0000000 --- a/FiniteSets/ordered.v +++ /dev/null @@ -1,826 +0,0 @@ -Require Import HoTT. -Require Import HitTactics. -Require Import definition. -Require Import operations. -Require Import properties. - -Definition relation A := A -> A -> Type. - -Section TotalOrder. - Class IsTop (A : Type) (R : relation A) (a : A) := - top_max : forall x, R x a. - - Class LessThan (A : Type) := - leq : relation A. - - Class Antisymmetric {A} (R : relation A) := - antisymmetry : forall x y, R x y -> R y x -> x = y. - - Class Total {A} (R : relation A) := - total : forall x y, x = y \/ R x y \/ R y x. - - Class TotalOrder (A : Type) {R : LessThan A} := - { TotalOrder_Reflexive :> Reflexive R | 2 ; - TotalOrder_Antisymmetric :> Antisymmetric R | 2; - TotalOrder_Transitive :> Transitive R | 2; - TotalOrder_Total :> Total R | 2; }. -End TotalOrder. - -Section minimum. - Context {A : Type}. - Context `{TotalOrder A}. - - Definition min (x y : A) : A. - Proof. - destruct (@total _ R _ x y). - - apply x. - - destruct s as [s | s]. - * apply x. - * apply y. - Defined. - - Lemma min_spec1 x y : R (min x y) x. - Proof. - unfold min. - destruct (total x y) ; simpl. - - reflexivity. - - destruct s as [ | t]. - * reflexivity. - * apply t. - Defined. - - Lemma min_spec2 x y z : R z x -> R z y -> R z (min x y). - Proof. - intros. - unfold min. - destruct (total x y) as [ | s]. - * assumption. - * try (destruct s) ; assumption. - Defined. - - Lemma min_comm x y : min x y = min y x. - Proof. - unfold min. - destruct (total x y) ; destruct (total y x) ; simpl. - - assumption. - - destruct s as [s | s] ; auto. - - destruct s as [s | s] ; symmetry ; auto. - - destruct s as [s | s] ; destruct s0 as [s0 | s0] ; try reflexivity. - * apply (@antisymmetry _ R _ _) ; assumption. - * apply (@antisymmetry _ R _ _) ; assumption. - Defined. - - Lemma min_idem x : min x x = x. - Proof. - unfold min. - destruct (total x x) ; simpl. - - reflexivity. - - destruct s ; reflexivity. - Defined. - - Lemma min_assoc x y z : min (min x y) z = min x (min y z). - Proof. - apply (@antisymmetry _ R _ _). - - apply min_spec2. - * etransitivity ; apply min_spec1. - * apply min_spec2. - ** etransitivity ; try (apply min_spec1). - simpl. - rewrite min_comm ; apply min_spec1. - ** rewrite min_comm ; apply min_spec1. - - apply min_spec2. - * apply min_spec2. - ** apply min_spec1. - ** etransitivity. - { rewrite min_comm ; apply min_spec1. } - apply min_spec1. - * transitivity (min y z); simpl - ; rewrite min_comm ; apply min_spec1. - Defined. - - Variable (top : A). - Context `{IsTop A R top}. - - Lemma min_nr x : min x top = x. - Proof. - intros. - unfold min. - destruct (total x top). - - reflexivity. - - destruct s. - * reflexivity. - * apply (@antisymmetry _ R _ _). - ** assumption. - ** refine (top_max _). apply _. - Defined. - - Lemma min_nl x : min top x = x. - Proof. - rewrite min_comm. - apply min_nr. - Defined. - - Lemma min_top_l x y : min x y = top -> x = top. - Proof. - unfold min. - destruct (total x y). - - apply idmap. - - destruct s as [s | s]. - * apply idmap. - * intros X. - rewrite X in s. - apply (@antisymmetry _ R _ _). - ** apply top_max. - ** assumption. - Defined. - - Lemma min_top_r x y : min x y = top -> y = top. - Proof. - rewrite min_comm. - apply min_top_l. - Defined. - -End minimum. - -Section add_top. - Variable (A : Type). - Context `{TotalOrder A}. - - Definition Top := A + Unit. - Definition top : Top := inr tt. - - Global Instance RTop : LessThan Top. - Proof. - unfold relation. - induction 1 as [a1 | ] ; induction 1 as [a2 | ]. - - apply (R a1 a2). - - apply Unit_hp. - - apply False_hp. - - apply Unit_hp. - Defined. - - Global Instance rtop_hprop : - is_mere_relation A R -> is_mere_relation Top RTop. - Proof. - intros P a b. - destruct a ; destruct b ; apply _. - Defined. - - Global Instance RTopOrder : TotalOrder Top. - Proof. - split. - - intros x ; induction x ; unfold RTop ; simpl. - * reflexivity. - * apply tt. - - intros x y ; induction x as [a1 | ] ; induction y as [a2 | ] ; unfold RTop ; simpl - ; try contradiction. - * intros ; f_ap. - apply (@antisymmetry _ R _ _) ; assumption. - * intros ; induction b ; induction b0. - reflexivity. - - intros x y z ; induction x as [a1 | b1] ; induction y as [a2 | b2] - ; induction z as [a3 | b3] ; unfold RTop ; simpl - ; try contradiction ; intros ; try (apply tt). - transitivity a2 ; assumption. - - intros x y. - unfold RTop ; simpl. - induction x as [a1 | b1] ; induction y as [a2 | b2] ; try (apply (inl idpath)). - * destruct (TotalOrder_Total a1 a2). - ** left ; f_ap ; assumption. - ** right ; assumption. - * apply (inr(inl tt)). - * apply (inr(inr tt)). - * left ; induction b1 ; induction b2 ; reflexivity. - Defined. - - Global Instance top_a_top : IsTop Top RTop top. - Proof. - intro x ; destruct x ; apply tt. - Defined. -End add_top. - -Section min_set. - Variable (A : Type). - Context `{TotalOrder A}. - Context `{is_mere_relation A R}. - Context `{Univalence} `{IsHSet A}. - - Definition min_set : FSet A -> Top A. - Proof. - hrecursion. - - apply (top A). - - apply inl. - - apply min. - - intros ; symmetry ; apply min_assoc. - - apply min_comm. - - apply min_nl. apply _. - - apply min_nr. apply _. - - intros ; apply min_idem. - Defined. - - Definition empty_min : forall (X : FSet A), min_set X = top A -> X = ∅. - Proof. - simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _) - ; try (intros ; apply path_forall ; intro q ; apply set_path2) - ; simpl. - - intros ; reflexivity. - - intros. - unfold top in X. - enough Empty. - { contradiction. } - refine (not_is_inl_and_inr' (inl a) _ _). - * apply tt. - * rewrite X ; apply tt. - - intros. - assert (min_set x = top A). - { - simple refine (min_top_l _ _ (min_set y) _) ; assumption. - } - rewrite (X X2). - rewrite nl. - assert (min_set y = top A). - { simple refine (min_top_r _ (min_set x) _ _) ; assumption. } - rewrite (X0 X3). - reflexivity. - Defined. - - Definition min_set_spec (a : A) : forall (X : FSet A), - a ∈ X -> RTop A (min_set X) (inl a). - Proof. - simple refine (FSet_ind _ _ _ _ _ _ _ _ _ _ _) - ; try (intros ; apply path_ishprop) - ; simpl. - - contradiction. - - intros. - strip_truncations. - rewrite X. - reflexivity. - - intros. - strip_truncations. - unfold member in X, X0. - destruct X1. - * specialize (X t). - assert (RTop A (min (min_set x) (min_set y)) (min_set x)) as X1. - { apply min_spec1. } - etransitivity. - { apply X1. } - assumption. - * specialize (X0 t). - assert (RTop A (min (min_set x) (min_set y)) (min_set y)) as X1. - { rewrite min_comm ; apply min_spec1. } - etransitivity. - { apply X1. } - assumption. - Defined. - -End min_set. - - -(* -Ltac eq_neq_tac := -match goal with - | [ H: ?x <> E, H': ?x = E |- _ ] => destruct H; assumption -end. - - -Ltac destruct_match_1 := - repeat match goal with - | [|- match ?X with | _ => _ end ] => destruct X - | [|- ?X = ?Y ] => apply path_ishprop - | [ H: ?x <> E |- Empty ] => destruct H - | [ H1: ?x = E, H2: ?y = E, H3: ?w ∪ ?q = E |- ?r = E] - => rewrite H1, H2 in H3; rewrite nl in H3; rewrite nl in H3 - end. - - -Lemma transport_dom_eq (D1 D2 C: Type) (P: D1 = D2) (f: D1 -> C) : -transport (fun T: Type => T -> C) P f = fun y => f (transport (fun X => X) P^ y). -Proof. -induction P. -hott_simpl. -Defined. - -Lemma transport_dom_eq_gen (Ty: Type) (D1 D2: Ty) (C: Type) (P: D1 = D2) - (Q : Ty -> Type) (f: Q D1 -> C) : -transport (fun X: Ty => Q X -> C) P f = fun y => f (transport Q P^ y). -Proof. -induction P. -hott_simpl. -Defined. - -(* Lemma min {HFun: Funext} (x: FSet A): x <> ∅ -> A. *) -(* Proof. *) -(* hrecursion x. *) -(* - intro H. destruct H. reflexivity. *) -(* - intros. exact a. *) -(* - intros x y rx ry H. *) -(* apply union_non_empty' in H. *) -(* destruct H. *) -(* + destruct p. specialize (rx fst). exact rx. *) -(* + destruct s. *) -(* * destruct p. specialize (ry snd). exact ry. *) -(* * destruct p. specialize (rx fst). specialize (ry snd). *) -(* destruct (TotalOrder_Total rx ry) as [Heq | [ Hx | Hy ]]. *) -(* ** exact rx. *) -(* ** exact rx. *) -(* ** exact ry. *) -(* - intros. rewrite transport_dom_eq_gen. *) -(* apply path_forall. intro y0. *) -(* destruct ( union_non_empty' x y ∪ z *) -(* (transport (fun X : FSet A => X <> ∅) (assoc x y z)^ y0)) *) -(* as [[ G1 G2] | [[ G3 G4] | [G5 G6]]]. *) -(* + pose (G2' := G2). apply eset_union_lr in G2'; destruct G2'. cbn. *) -(* destruct (union_non_empty' x ∪ y z y0) as *) -(* [[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; try eq_neq_tac. *) -(* destruct (union_non_empty' x y H'x). *) -(* ** destruct p. assert (G1 = fst0). apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. reflexivity. *) -(* ** destruct s; destruct p; eq_neq_tac. *) -(* + destruct (union_non_empty' y z G4) as *) -(* [[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; try eq_neq_tac. *) -(* destruct (union_non_empty' x ∪ y z y0). *) -(* ** destruct p. cbn. destruct (union_non_empty' x y fst). *) -(* *** destruct p; eq_neq_tac. *) -(* *** destruct s. destruct p. *) -(* **** assert (H'x = snd0). apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. reflexivity. *) -(* **** destruct p. eq_neq_tac. *) -(* ** destruct s; destruct p; try eq_neq_tac. *) -(* ** destruct (union_non_empty' x ∪ y z y0). *) -(* *** destruct p. eq_neq_tac. *) -(* *** destruct s. destruct p. *) -(* **** assert (H'b = snd). apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. reflexivity. *) -(* **** destruct p. assert (x ∪ y = E). *) -(* rewrite H'a, G3. apply union_idem. eq_neq_tac. *) -(* ** cbn. destruct (TotalOrder_Total (py H'c) (pz H'd)). *) -(* *** destruct (union_non_empty' x ∪ y z y0). *) -(* **** destruct p0. eq_neq_tac. *) -(* **** destruct s. *) -(* ***** destruct p0. rewrite G3, nl in fst. eq_neq_tac. *) -(* ***** destruct p0. destruct (union_non_empty' x y fst). *) -(* ****** destruct p0. eq_neq_tac. *) -(* ****** destruct s. *) -(* ******* destruct p0. *) -(* destruct (TotalOrder_Total (py snd0) (pz snd)). *) -(* f_ap. apply path_forall. intro. *) -(* apply path_ishprop. *) -(* destruct s. f_ap. apply path_forall. intro. *) -(* apply path_ishprop. *) -(* rewrite p. f_ap. apply path_forall. intro. *) -(* apply path_ishprop. *) -(* ******* destruct p0. eq_neq_tac. *) -(* *** destruct (union_non_empty' x ∪ y z y0). *) -(* **** destruct p. eq_neq_tac. *) -(* **** destruct s0. destruct p. rewrite comm in fst. *) -(* apply eset_union_l in fst. eq_neq_tac. *) -(* destruct p. *) -(* destruct (union_non_empty' x y fst). *) -(* ***** destruct p; eq_neq_tac. *) -(* ***** destruct s0. destruct p. *) -(* destruct (TotalOrder_Total (py snd0) (pz snd)); *) -(* destruct s; try (f_ap; apply path_forall; intro; *) -(* apply path_ishprop). *) -(* rewrite p. f_ap; apply path_forall; intro; *) -(* apply path_ishprop. *) -(* destruct s0. f_ap; apply path_forall; intro; *) -(* apply path_ishprop. *) -(* assert (snd0 = H'c). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* assert (snd = H'd). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* rewrite <- X0 in r. rewrite X in r0. *) -(* apply TotalOrder_Antisymmetric; assumption. *) -(* destruct s0. *) -(* assert (snd0 = H'c). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* assert (snd = H'd). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* rewrite <- X in r. rewrite X0 in r0. *) -(* apply TotalOrder_Antisymmetric; assumption. *) -(* f_ap; apply path_forall; intro; *) -(* apply path_ishprop. *) -(* destruct p; eq_neq_tac. *) -(* + cbn. destruct (union_non_empty' y z G6). *) -(* ** destruct p. destruct ( union_non_empty' x ∪ y z y0). *) -(* *** destruct p. destruct (union_non_empty' x y fst0). *) -(* **** destruct p; eq_neq_tac. *) -(* **** destruct s; destruct p. eq_neq_tac. *) -(* assert (fst1 = G5). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* assert (fst = snd1). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* rewrite X, X0. *) -(* destruct (TotalOrder_Total (px G5) (py snd1)). *) -(* reflexivity. *) -(* destruct s; reflexivity. *) -(* *** destruct s; destruct p; eq_neq_tac. *) -(* ** destruct (union_non_empty' x ∪ y z y0). *) -(* *** destruct p. destruct s; destruct p; eq_neq_tac. *) -(* *** destruct s. destruct p. destruct s0. destruct p. *) -(* apply eset_union_l in fst0. eq_neq_tac. *) -(* **** destruct p. *) -(* assert (snd = snd0). apply path_forall; intro; *) -(* apply path_ishprop. *) - -(* destruct (union_non_empty' x y fst0). *) -(* destruct p. *) -(* assert (fst1 = G5). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* assert (fst = snd1). apply set_path2. *) -(* ***** rewrite X0. rewrite <- X. reflexivity. *) -(* ***** destruct s; destruct p; eq_neq_tac. *) -(* **** destruct s0. destruct p0. destruct p. *) -(* ***** apply eset_union_l in fst. eq_neq_tac. *) -(* ***** destruct p, p0. *) -(* assert (snd0 = snd). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* rewrite X. *) -(* destruct (union_non_empty' x y fst0). *) -(* destruct p; eq_neq_tac. *) -(* destruct s. destruct p; eq_neq_tac. *) -(* destruct p. *) -(* assert (fst = snd1). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* assert (fst1 = G5). apply path_forall; intro; *) -(* apply path_ishprop. *) -(* rewrite <- X0. rewrite X1. *) -(* destruct (TotalOrder_Total (py fst) (pz snd)). *) -(* ****** rewrite <- p. *) -(* destruct (TotalOrder_Total (px G5) (py fst)). *) -(* rewrite <- p0. *) -(* destruct (TotalOrder_Total (px G5) (px G5)). *) -(* reflexivity. *) -(* destruct s; reflexivity. *) -(* destruct s. destruct (TotalOrder_Total (px G5) (py fst)). *) -(* reflexivity. *) -(* destruct s. *) -(* reflexivity. *) -(* apply TotalOrder_Antisymmetric; assumption. *) -(* destruct (TotalOrder_Total (py fst) (py fst)). *) -(* reflexivity. *) -(* destruct s; *) -(* reflexivity. *) -(* ****** destruct s. *) -(* destruct (TotalOrder_Total (px G5) (py fst)). *) -(* destruct (TotalOrder_Total (px G5) (pz snd)). *) -(* reflexivity. *) -(* destruct s. *) -(* reflexivity. rewrite <- p in r. *) -(* apply TotalOrder_Antisymmetric; assumption. *) -(* destruct s. *) -(* destruct ( TotalOrder_Total (px G5) (pz snd)). *) -(* reflexivity. *) -(* destruct s. reflexivity. *) -(* apply (TotalOrder_Transitive (px G5)) in r. *) -(* apply TotalOrder_Antisymmetric; assumption. *) -(* assumption. *) -(* destruct (TotalOrder_Total (py fst) (pz snd)). reflexivity. *) -(* destruct s. reflexivity. *) -(* apply TotalOrder_Antisymmetric; assumption. *) -(* ******* *) -(* destruct ( TotalOrder_Total (px G5) (py fst)). *) -(* reflexivity. *) -(* destruct s. destruct (TotalOrder_Total (px G5) (pz snd)). *) -(* reflexivity. destruct s; reflexivity. *) -(* destruct ( TotalOrder_Total (px G5) (pz snd)). *) -(* rewrite <- p. *) -(* destruct (TotalOrder_Total (py fst) (px G5)). *) -(* apply symmetry; assumption. *) -(* destruct s. rewrite <- p in r. *) -(* apply TotalOrder_Antisymmetric; assumption. *) -(* reflexivity. destruct s. *) -(* assert ((py fst) = (pz snd)). apply TotalOrder_Antisymmetric. *) -(* apply (TotalOrder_Transitive (py fst) (px G5)); assumption. *) -(* assumption. rewrite X2. assert (px G5 = pz snd). *) -(* apply TotalOrder_Antisymmetric. assumption. *) -(* apply (TotalOrder_Transitive (pz snd) (py fst)); assumption. *) -(* rewrite X3. *) -(* destruct ( TotalOrder_Total (pz snd) (pz snd)). *) -(* reflexivity. destruct s; reflexivity. *) -(* destruct (TotalOrder_Total (py fst) (pz snd)). *) -(* apply TotalOrder_Antisymmetric. assumption. rewrite p. *) -(* apply (TotalOrder_Reflexive). destruct s. *) -(* apply TotalOrder_Antisymmetric; assumption. reflexivity. *) -(* - intros. rewrite transport_dom_eq_gen. *) -(* apply path_forall. intro y0. cbn. *) -(* destruct *) -(* (union_non_empty' x y *) -(* (transport (fun X : FSet A => X <> ∅) (comm x y)^ y0)) as *) -(* [[Hx Hy] | [ [Ha Hb] | [Hc Hd]]]; *) -(* destruct (union_non_empty' y x y0) as *) -(* [[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; *) -(* try (eq_neq_tac). *) -(* assert (Hx = H'b). apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. reflexivity. *) -(* assert (Hb = H'x). apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. reflexivity. *) -(* assert (Hd = H'c). apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. *) -(* assert (H'd = Hc). apply path_forall. intro. *) -(* apply path_ishprop. *) -(* rewrite X0. rewrite <- X. *) -(* destruct *) -(* (TotalOrder_Total (px Hc) (py Hd)) as [G1 | [G2 | G3]]; *) -(* destruct *) -(* (TotalOrder_Total (py Hd) (px Hc)) as [T1 | [T2 | T3]]; *) -(* try (assumption); *) -(* try (reflexivity); *) -(* try (apply symmetry; assumption); *) -(* try (apply TotalOrder_Antisymmetric; assumption). *) - -(* - intros. rewrite transport_dom_eq_gen. *) -(* apply path_forall. intro y. *) -(* destruct (union_non_empty' ∅ x (transport (fun X : FSet A => X <> ∅) (nl x)^ y)). *) -(* destruct p. eq_neq_tac. *) -(* destruct s. *) -(* destruct p. *) -(* assert (y = snd). *) -(* apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. reflexivity. *) -(* destruct p. destruct fst. *) -(* - intros. rewrite transport_dom_eq_gen. *) -(* apply path_forall. intro y. *) -(* destruct (union_non_empty' x ∅ (transport (fun X : FSet A => X <> ∅) (nr x)^ y)). *) -(* destruct p. assert (y = fst). apply path_forall. intro. *) -(* apply path_ishprop. rewrite X. reflexivity. *) -(* destruct s. *) -(* destruct p. *) -(* eq_neq_tac. *) -(* destruct p. *) -(* destruct snd. *) -(* - intros. rewrite transport_dom_eq_gen. *) -(* apply path_forall. intro y. *) -(* destruct ( union_non_empty' {|x|} {|x|} (transport (fun X : FSet A => X <> ∅) (idem x)^ y)). *) -(* reflexivity. *) -(* destruct s. *) -(* reflexivity. *) -(* destruct p. *) -(* cbn. destruct (TotalOrder_Total x x). reflexivity. *) -(* destruct s; reflexivity. *) -(* Defined. *) - - -Definition minfset {HFun: Funext} : - FSet A -> { Y: (FSet A) & (Y = E) + { a: A & Y = L a } }. -intro X. -hinduction X. -- exists E. left. reflexivity. -- intro a. exists (L a). right. exists a. reflexivity. -- intros IH1 IH2. - destruct IH1 as [R1 HR1]. - destruct IH2 as [R2 HR2]. - destruct HR1. - destruct HR2. - exists E; left. reflexivity. - destruct s as [a Ha]. exists (L a). right. - exists a. reflexivity. - destruct HR2. - destruct s as [a Ha]. - exists (L a). right. exists a. reflexivity. - destruct s as [a1 Ha1]. - destruct s0 as [a2 Ha2]. - assert (a1 = a2 \/ R a1 a2 \/ R a2 a1). - apply TotalOrder_Total. - destruct X. - exists (L a1). right. exists a1. reflexivity. - destruct s. - exists (L a1). right. exists a1. reflexivity. - exists (L a2). right. exists a2. reflexivity. - - cbn. intros R1 R2 R3. - destruct R1 as [Res1 HR1]. - destruct HR1 as [HR1E | HR1S]. - destruct R2 as [Res2 HR2]. - destruct HR2 as [HR2E | HR2S]. - destruct R3 as [Res3 HR3]. - destruct HR3 as [HR3E | HR3S]. - + cbn. reflexivity. - + cbn. reflexivity. - + cbn. destruct R3 as [Res3 HR3]. - destruct HR3 as [HR3E | HR3S]. - * cbn. reflexivity. - * destruct HR2S as [a2 Ha2]. - destruct HR3S as [a3 Ha3]. - destruct (TotalOrder_Total a2 a3). - ** cbn. reflexivity. - ** destruct s. cbn. reflexivity. - cbn. reflexivity. - + destruct HR1S as [a1 Ha1]. - destruct R2 as [Res2 HR2]. - destruct HR2 as [HR2E | HR2S]. - destruct R3 as [Res3 HR3]. - destruct HR3 as [HR3E | HR3S]. - * cbn. reflexivity. - * destruct HR3S as [a3 Ha3]. - destruct (TotalOrder_Total a1 a3). - reflexivity. - destruct s; reflexivity. - * destruct HR2S as [a2 Ha2]. - destruct R3 as [Res3 HR3]. - destruct HR3 as [HR3E | HR3S]. - cbn. destruct (TotalOrder_Total a1 a2). - cbn. reflexivity. - destruct s. - cbn. reflexivity. - cbn. reflexivity. - destruct HR3S as [a3 Ha3]. - destruct (TotalOrder_Total a2 a3). - ** rewrite p. - destruct (TotalOrder_Total a1 a3). - rewrite p0. - destruct ( TotalOrder_Total a3 a3). - reflexivity. - destruct s; reflexivity. - destruct s. cbn. - destruct (TotalOrder_Total a1 a3). - reflexivity. - destruct s. reflexivity. - assert (a1 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. - cbn. destruct (TotalOrder_Total a3 a3). - reflexivity. - destruct s; reflexivity. - ** destruct s. - *** cbn. destruct (TotalOrder_Total a1 a2). - cbn. destruct (TotalOrder_Total a1 a3). - reflexivity. - destruct s. reflexivity. - rewrite <- p in r. - assert (a1 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. - destruct s. cbn. - destruct (TotalOrder_Total a1 a3). - reflexivity. - destruct s. reflexivity. - assert (R a1 a3). - apply (TotalOrder_Transitive a1 a2); assumption. - assert (a1 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X0. reflexivity. - cbn. destruct (TotalOrder_Total a2 a3). - reflexivity. - destruct s. - reflexivity. - assert (a2 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. - *** cbn. destruct (TotalOrder_Total a1 a3). - rewrite p. destruct (TotalOrder_Total a3 a2). - cbn. destruct (TotalOrder_Total a3 a3). - reflexivity. destruct s; reflexivity. - destruct s. cbn. - destruct (TotalOrder_Total a3 a3). - reflexivity. destruct s; reflexivity. - cbn. destruct (TotalOrder_Total a2 a3). - rewrite p0. - reflexivity. - destruct s. - assert (a2 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. reflexivity. - destruct s. - cbn. - destruct (TotalOrder_Total a1 a2). - cbn. - destruct (TotalOrder_Total a1 a3). - reflexivity. - assert (a1 = a3). - apply TotalOrder_Antisymmetric. assumption. - rewrite <- p in r. assumption. - destruct s. reflexivity. rewrite X. reflexivity. - destruct s. cbn. - destruct (TotalOrder_Total a1 a3). reflexivity. - destruct s. reflexivity. - assert (a1 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. - cbn. destruct (TotalOrder_Total a2 a3). - rewrite p in r1. - assert (a2 = a1). - transitivity a3. - assumption. - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. - destruct s. - assert (a1 = a2). - apply TotalOrder_Antisymmetric. - apply (TotalOrder_Transitive a1 a3); assumption. - assumption. - rewrite X. reflexivity. - assert (a1 = a3). - apply TotalOrder_Antisymmetric. - assumption. - apply (TotalOrder_Transitive a3 a2); assumption. - rewrite X. reflexivity. - destruct ( TotalOrder_Total a1 a2). - cbn. - destruct (TotalOrder_Total a1 a3). - rewrite p0. - reflexivity. - destruct s. - assert (a1 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. reflexivity. - destruct s. - cbn. - destruct (TotalOrder_Total a1 a3 ). - rewrite p. - reflexivity. - destruct s. - assert (a1 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. reflexivity. - cbn. - destruct (TotalOrder_Total a1 a3 ). - assert (a2 = a3). - rewrite p in r1. - apply TotalOrder_Antisymmetric; assumption. - rewrite X. destruct (TotalOrder_Total a3 a3). reflexivity. - destruct s; reflexivity. - destruct s. - destruct (TotalOrder_Total a2 a3). - rewrite p. - reflexivity. - destruct s. - assert (a2 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. - reflexivity. - cbn. destruct (TotalOrder_Total a2 a3). - rewrite p. - reflexivity. - destruct s. - assert (a2 = a3). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. reflexivity. reflexivity. - - cbn. intros R1 R2. - destruct R1 as [La1 HR1]. - destruct HR1 as [HR1E | HR1S]. - destruct R2 as [La2 HR2]. - destruct HR2 as [HR2E | HR2S]. - reflexivity. - reflexivity. - destruct R2 as [La2 HR2]. - destruct HR2 as [HR2E | HR2S]. - reflexivity. - destruct HR1S as [a1 Ha1]. - destruct HR2S as [a2 Ha2]. - destruct (TotalOrder_Total a1 a2). - rewrite p. - destruct (TotalOrder_Total a2 a2). - reflexivity. - destruct s; reflexivity. - destruct s. - destruct (TotalOrder_Total a2 a1). - rewrite p. - reflexivity. - destruct s. - assert (a1 = a2). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. - reflexivity. - reflexivity. - destruct (TotalOrder_Total a2 a1). - rewrite p. - reflexivity. - destruct s. - reflexivity. - assert (a1 = a2). - apply TotalOrder_Antisymmetric; assumption. - rewrite X. - reflexivity. - - cbn. intro R. destruct R as [La HR]. - destruct HR. rewrite <- p. reflexivity. - destruct s as [a1 H]. - apply (path_sigma' _ H^). - rewrite transport_sum. - f_ap. - rewrite transport_sigma. - simpl. - simple refine (path_sigma' _ _ _ ). - apply transport_const. - apply set_path2. - - - intros R. cbn. - destruct R as [ R HR]. - destruct HR as [HE | Ha ]. - rewrite <- HE. reflexivity. - destruct Ha as [a Ha]. - apply (path_sigma' _ Ha^). - rewrite transport_sum. - f_ap. - rewrite transport_sigma. - simpl. - simple refine (path_sigma' _ _ _ ). - apply transport_const. - apply set_path2. - - cbn. intro. - destruct (TotalOrder_Total x x). - reflexivity. - destruct s. - reflexivity. - reflexivity. -Defined. -*) \ No newline at end of file diff --git a/FiniteSets/plumbing.v b/FiniteSets/prelude.v similarity index 59% rename from FiniteSets/plumbing.v rename to FiniteSets/prelude.v index 1bb52b7..45df745 100644 --- a/FiniteSets/plumbing.v +++ b/FiniteSets/prelude.v @@ -1,8 +1,6 @@ +(** Some general prerequisities in homotopy type theory. *) Require Import HoTT. -(* Lemmas from this file do not belong in this project. *) -(* Some of them should probably be in the HoTT library? *) - Lemma ap_inl_path_sum_inl {A B} (x y : A) (p : inl x = inl y) : ap inl (path_sum_inl B p) = p. Proof. @@ -11,13 +9,17 @@ Proof. destruct (path_sum_inl B p). reflexivity. Defined. + Lemma ap_equiv {A B} (f : A <~> B) {x y : A} (p : x = y) : ap (f^-1 o f) p = eissect f x @ p @ (eissect f y)^. -Proof. destruct p. hott_simpl. Defined. +Proof. + destruct p. + hott_simpl. +Defined. Global Instance hprop_lem `{Univalence} (T : Type) (Ttrunc : IsHProp T) : IsHProp (T + ~T). - Proof. - apply (equiv_hprop_allpath _)^-1. - intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction. - - apply equiv_hprop_allpath. apply _. - Defined. +Proof. + apply (equiv_hprop_allpath _)^-1. + intros [x | nx] [y | ny] ; try f_ap ; try (apply Ttrunc) ; try contradiction. + - apply equiv_hprop_allpath. apply _. +Defined. \ No newline at end of file diff --git a/FiniteSets/Sub.v b/FiniteSets/subobjects/Sub.v similarity index 100% rename from FiniteSets/Sub.v rename to FiniteSets/subobjects/Sub.v diff --git a/FiniteSets/variations/b_finite.v b/FiniteSets/subobjects/b_finite.v similarity index 98% rename from FiniteSets/variations/b_finite.v rename to FiniteSets/subobjects/b_finite.v index 811aa64..c51324e 100644 --- a/FiniteSets/variations/b_finite.v +++ b/FiniteSets/subobjects/b_finite.v @@ -1,7 +1,6 @@ (* Bishop-finiteness is that "default" notion of finiteness in the HoTT library *) -Require Import HoTT HitTactics plumbing. -Require Import Sub notation variations.k_finite. -Require Import fsets.properties fsets.monad. +Require Import HoTT HitTactics. +Require Import sub subobjects.k_finite FSets prelude. Section finite_hott. Variable (A : Type). @@ -322,7 +321,7 @@ Section bfin_kfin. apply Kf_unfold in IH. destruct IH as [X HX]. apply Kf_unfold. - exists ((ffmap inl X) ∪ {|inr tt|}); simpl. + exists ((fmap FSet inl X) ∪ {|inr tt|}); simpl. intros [a | []]; apply tr. + left. apply fmap_isIn. @@ -380,7 +379,6 @@ Section kfin_bfin. { intros HXY. rewrite HXY. by apply IHn. } apply path_forall. intro a. - unfold union, sub_union, lattice.max_fun. apply path_iff_hprop. * intros Ha. strip_truncations. diff --git a/FiniteSets/variations/enumerated.v b/FiniteSets/subobjects/enumerated.v similarity index 98% rename from FiniteSets/variations/enumerated.v rename to FiniteSets/subobjects/enumerated.v index 8663d5d..a336e0e 100644 --- a/FiniteSets/variations/enumerated.v +++ b/FiniteSets/subobjects/enumerated.v @@ -1,9 +1,8 @@ (* Enumerated finite sets *) Require Import HoTT HitTactics. -Require Import disjunction Sub. -Require Import representations.cons_repr representations.definition. -Require Import variations.k_finite. -From fsets Require Import operations isomorphism properties_decidable operations_decidable. +Require Import sub prelude FSets list_representation subobjects.k_finite + list_representation.isomorphism + lattice_interface lattice_examples. Fixpoint listExt {A} (ls : list A) : Sub A := fun x => match ls with diff --git a/FiniteSets/variations/k_finite.v b/FiniteSets/subobjects/k_finite.v similarity index 96% rename from FiniteSets/variations/k_finite.v rename to FiniteSets/subobjects/k_finite.v index d0e17a0..b3778b0 100644 --- a/FiniteSets/variations/k_finite.v +++ b/FiniteSets/subobjects/k_finite.v @@ -1,5 +1,5 @@ Require Import HoTT HitTactics. -Require Import lattice representations.definition fsets.operations extensionality Sub fsets.properties fsets.monad. +Require Import sub lattice_interface lattice_examples FSets. Section k_finite. @@ -125,7 +125,7 @@ Section k_properties. Proof. intros HX. apply Kf_unfold. apply Kf_unfold in HX. destruct HX as [Xf HXf]. - exists (ffmap f Xf). + exists (fmap FSet f Xf). intro y. pose (x' := center (merely (hfiber f y))). simple refine (@Trunc_rec (-1) (hfiber f y) _ _ _ x'). clear x'; intro x. @@ -168,7 +168,7 @@ Section alternative_definition. Local Ltac help_solve := repeat (let x := fresh in intro x ; destruct x) ; intros ; try (simple refine (path_sigma _ _ _ _ _)) ; try (apply path_ishprop) ; simpl - ; unfold union, Sub.sub_union, max_fun + ; unfold union, sub_union, max_fun ; apply path_forall ; intro z ; eauto with lattice_hints typeclass_instances.