dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

Clean up trailing whitespaces and an unused definition.

This commit is contained in:
Dan Frumin 2017-08-09 18:05:58 +02:00
parent 31e08af1d1
commit 33808928db
15 changed files with 137 additions and 152 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
FiniteSets/disjunction.v
View File

@ -12,7 +12,7 @@ Open Scope logic_scope.
Section lor_props.
Context `{Univalence}.
Variable X Y Z : hProp.
Lemma lor_assoc : (X ∨ Y) ∨ Z = X ∨ Y ∨ Z.
Proof.
apply path_iff_hprop ; cbn.
@ -20,15 +20,15 @@ Section lor_props.
intros [xy | z] ; cbn.
+ simple refine (Trunc_ind _ _ xy).
intros [x | y].
++ apply (tr (inl x)).
++ apply (tr (inl x)).
++ apply (tr (inr (tr (inl y)))).
+ apply (tr (inr (tr (inr z)))).
* simple refine (Trunc_ind _ _).
* simple refine (Trunc_ind _ _).
intros [x | yz] ; cbn.
+ apply (tr (inl (tr (inl x)))).
+ simple refine (Trunc_ind _ _ yz).
intros [y | z].
++ apply (tr (inl (tr (inr y)))).
++ apply (tr (inl (tr (inr y)))).
++ apply (tr (inr z)).
Defined.
@ -131,7 +131,7 @@ Section hPropLattice.
- intros [a b] ; apply a.
- intros a ; apply (pair a a).
Defined.
Instance lor_neutrall : NeutralL lor lfalse.
Proof.
unfold NeutralL.
@ -169,7 +169,7 @@ Section hPropLattice.
* assumption.
* apply (tr (inl X)).
Defined.
Global Instance lattice_hprop : Lattice hProp :=
{ commutative_min := _ ;
commutative_max := _ ;
@ -182,5 +182,5 @@ Section hPropLattice.
absorption_min_max := _ ;
absorption_max_min := _
}.
End hPropLattice.

10
FiniteSets/fsets/extensionality.v
View File

@ -6,7 +6,7 @@ Section ext.
Context {A : Type}.
Context `{Univalence}.
Lemma subset_union (X Y : FSet A) :
Lemma subset_union (X Y : FSet A) :
X ⊆ Y -> X ∪ Y = Y.
Proof.
hinduction X ; try (intros; apply path_forall; intro; apply set_path2).
@ -17,7 +17,7 @@ Section ext.
contradiction.
+ intro a0.
simple refine (Trunc_ind _ _).
intro p ; simpl.
intro p ; simpl.
rewrite p; apply idem.
+ intros X1 X2 IH1 IH2.
simple refine (Trunc_ind _ _).
@ -112,8 +112,8 @@ Section ext.
unshelve esplit.
{ intros [H1 H2]. etransitivity. apply H1^.
rewrite comm. apply H2. }
intro; apply path_prod; apply set_path2.
all: intro; apply set_path2.
intro; apply path_prod; apply set_path2.
all: intro; apply set_path2.
Defined.
Lemma eq_subset (X Y : FSet A) :
@ -149,4 +149,4 @@ Section ext.
split ; apply subset_isIn.
Defined.
End ext.
End ext.

8
FiniteSets/fsets/isomorphism.v
View File

@ -14,7 +14,7 @@ Section Iso.
- apply E.
- intros a x.
apply ({|a|} ∪ x).
- intros. cbn.
- intros. cbn.
etransitivity. apply assoc.
apply (ap (∪ x)).
apply idem.
@ -22,7 +22,7 @@ Section Iso.
etransitivity. apply assoc.
etransitivity. refine (ap (∪ x) _ ).
apply FSet.comm.
symmetry.
symmetry.
apply assoc.
Defined.
@ -39,10 +39,10 @@ Section Iso.
- apply singleton_idem.
Defined.
Lemma append_union: forall (x y: FSetC A),
Lemma append_union: forall (x y: FSetC A),
FSetC_to_FSet (x ∪ y) = (FSetC_to_FSet x) ∪ (FSetC_to_FSet y).
Proof.
intros x.
intros x.
hrecursion x; try (intros; apply path_forall; intro; apply set_path2).
- intros. symmetry. apply nl.
- intros a x HR y. unfold union, fsetc_union in *. rewrite HR. apply assoc.

27
FiniteSets/fsets/operations.v
View File

@ -34,7 +34,7 @@ Section operations.
- apply comm.
- apply nl.
- apply nr.
- intros; simpl.
- intros; simpl.
destruct (P x).
+ apply idem.
+ apply nl.
@ -61,7 +61,7 @@ Section operations.
- intros ; apply nr.
- intros ; apply idem.
Defined.
Definition product {A B : Type} : FSet A -> FSet B -> FSet (A * B).
Proof.
intros X Y.
@ -76,7 +76,7 @@ Section operations.
- intros ; apply nr.
- intros ; apply union_idem.
Defined.
Global Instance fset_subset : forall A, hasSubset (FSet A).
Proof.
intros A X Y.
@ -103,21 +103,6 @@ Section operations.
split ; apply p.
Defined.
Definition map (A B : Type) (f : A -> B) : FSet A -> FSet B.
Proof.
hrecursion.
- apply ∅.
- intro a.
apply {|f a|}.
- apply (∪).
- apply assoc.
- apply comm.
- apply nl.
- apply nr.
- intros.
apply idem.
Defined.
Local Ltac remove_transport
:= intros ; apply path_forall ; intro Z ; rewrite transport_arrow
; rewrite transport_const ; simpl.
@ -155,6 +140,6 @@ Section operations.
- remove_transport.
rewrite <- (idem (Z (x; tr 1%path))).
pointwise.
Defined.
End operations.
Defined.
End operations.

18
FiniteSets/fsets/properties.v
View File

@ -10,7 +10,7 @@ Section characterize_isIn.
(** isIn properties *)
Definition empty_isIn (a: A) : a ∈ ∅ -> Empty := idmap.
Definition singleton_isIn (a b: A) : a ∈ {|b|} -> Trunc (-1) (a = b) := idmap.
Definition union_isIn (X Y : FSet A) (a : A)
@ -20,7 +20,7 @@ Section characterize_isIn.
{|X ∪ Y & ϕ|} = {|X & ϕ|} ∪ {|Y & ϕ|}.
Proof.
reflexivity.
Defined.
Defined.
Lemma comprehension_isIn (ϕ : A -> Bool) (a : A) : forall X : FSet A,
a ∈ {|X & ϕ|} = if ϕ a then a ∈ X else False_hp.
@ -37,7 +37,7 @@ Section characterize_isIn.
destruct c ; destruct d ; rewrite Hc, Hd ; try reflexivity
; apply path_iff_hprop ; try contradiction ; intros ; strip_truncations
; apply (false_ne_true).
* apply (Hd^ @ ap ϕ X^ @ Hc).
* apply (Hd^ @ ap ϕ X^ @ Hc).
* apply (Hc^ @ ap ϕ X @ Hd).
}
apply (X (ϕ a) (ϕ b) idpath idpath).
@ -57,7 +57,7 @@ End characterize_isIn.
Section product_isIn.
Context {A B : Type}.
Context `{Univalence}.
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).
Proof.
@ -65,7 +65,7 @@ Section product_isIn.
- apply path_hprop ; symmetry ; apply prod_empty_r.
- intros d.
apply path_iff_hprop.
* intros.
* intros.
strip_truncations.
split ; apply tr ; try (apply (ap fst X)) ; try (apply (ap snd X)).
* intros [Z1 Z2].
@ -93,7 +93,7 @@ Section product_isIn.
** right.
split ; try (apply (tr H1)) ; try (apply Hb2).
Defined.
Definition isIn_product (a : A) (b : B) (X : FSet A) (Y : FSet B) :
(a,b) ∈ (product X Y) = land (a ∈ X) (b ∈ Y).
Proof.
@ -147,7 +147,7 @@ Section properties.
Global Instance joinsemilattice_fset : JoinSemiLattice (FSet A).
Proof.
split ; toHProp.
Defined.
Defined.
(** comprehension properties *)
Lemma comprehension_false : forall (X : FSet A), {|X & fun _ => false|} = ∅.
@ -176,7 +176,7 @@ Section properties.
Proof.
toHProp.
Defined.
Lemma merely_choice : forall X : FSet A, hor (X = ∅) (hexists (fun a => a ∈ X)).
Proof.
hinduction; try (intros; apply equiv_hprop_allpath ; apply _).
@ -295,5 +295,5 @@ Section properties.
repeat f_ap.
apply path_ishprop.
Defined.
End properties.

24
FiniteSets/fsets/properties_cons_repr.v
View File

@ -7,7 +7,7 @@ Section properties.
Context {A : Type}.
Definition append_nl : forall (x: FSetC A), ∅ ∪ x = x
:= fun _ => idpath.
:= fun _ => idpath.
Lemma append_nr : forall (x: FSetC A), x ∪ ∅ = x.
Proof.
@ -15,20 +15,20 @@ Section properties.
- reflexivity.
- intros. apply (ap (fun y => a;;y) X).
Defined.
Lemma append_assoc {H: Funext}:
Lemma append_assoc {H: Funext}:
forall (x y z: FSetC A), x ∪ (y ∪ z) = (x ∪ y) ∪ z.
Proof.
hinduction
; try (intros ; apply path_forall ; intro
; apply path_forall ; intro ; apply set_path2).
- reflexivity.
- intros a x HR y z.
- intros a x HR y z.
specialize (HR y z).
apply (ap (fun y => a;;y) HR).
apply (ap (fun y => a;;y) HR).
Defined.
Lemma append_singleton: forall (a: A) (x: FSetC A),
Lemma append_singleton: forall (a: A) (x: FSetC A),
a ;; x = x ∪ (a ;; ∅).
Proof.
intro a. hinduction; try (intros; apply set_path2).
@ -38,22 +38,22 @@ Section properties.
+ apply (ap (fun y => b ;; y) HR).
Defined.
Lemma append_comm {H: Funext}:
Lemma append_comm {H: Funext}:
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. symmetry. apply append_nr.
- intros a x1 HR x2.
etransitivity.
apply (ap (fun y => a;;y) (HR x2)).
apply (ap (fun y => a;;y) (HR x2)).
transitivity ((x2 ∪ x1) ∪ (a;;∅)).
+ apply append_singleton.
+ apply append_singleton.
+ etransitivity.
* symmetry. apply append_assoc.
* simple refine (ap (x2 ∪) (append_singleton _ _)^).
Defined.
Lemma singleton_idem: forall (a: A),
Lemma singleton_idem: forall (a: A),
{|a|} ∪ {|a|} = {|a|}.
Proof.
unfold singleton.

12
FiniteSets/fsets/properties_decidable.v
View File

@ -60,7 +60,7 @@ Section operations_isIn.
contradiction.
- reflexivity.
Defined.
(* Union and membership *)
Lemma union_isIn_b (X Y : FSet A) (a : A) :
a ∈_d (X ∪ Y) = orb (a ∈_d X) (a ∈_d Y).
@ -111,24 +111,24 @@ Section SetLattice.
intros x y.
apply (x ∪ y).
Defined.
Instance fset_min : minimum (FSet A).
Proof.
intros x y.
apply (x ∩ y).
Defined.
Instance fset_bot : bottom (FSet A).
Proof.
unfold bottom.
apply ∅.
Defined.
Instance lattice_fset : Lattice (FSet A).
Proof.
split; toBool.
Defined.
End SetLattice.
(* With extensionality we can prove decidable equality *)
@ -142,4 +142,4 @@ Section dec_eq.
apply decidable_prod.
Defined.
End dec_eq.
End dec_eq.

10
FiniteSets/implementations/interface.v
View File

@ -87,12 +87,12 @@ Section properties.
Definition well_defined_filter : forall (A : Type) (ϕ : A -> Bool) (X Y : T A),
set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
Proof.
Proof.
intros A ϕ X Y HXY.
simplify.
by rewrite HXY.
Defined.
Lemma union_comm : forall A (X Y : T A),
set_eq A (X ∪ Y) (Y ∪ X).
Proof.
@ -151,7 +151,7 @@ Proof. intros a b c Hab Hbc. apply (Hab @ Hbc). Defined.
Instance View_recursion A : HitRecursion (View A) :=
{
indTy := _; recTy := forall (P : Type) (HP: IsHSet P) (u : T A -> P), (forall x y : T A, set_eq T (@f) A x y -> u x = u y) -> View A -> P;
indTy := _; recTy := forall (P : Type) (HP: IsHSet P) (u : T A -> P), (forall x y : T A, set_eq T (@f) A x y -> u x = u y) -> View A -> P;
H_inductor := quotient_ind (R A); H_recursor := @quotient_rec _ (R A) _
}.
@ -169,7 +169,7 @@ assert (resp1 : forall x y y', set_eq (@f) y y' -> u x y = u x y').
assert (resp2 : forall x x' y, set_eq (@f) x x' -> u x y = u x' y).
{ intros x x' y Hxx'.
apply Hresp. apply Hxx'.
reflexivity. }
reflexivity. }
hrecursion.
- intros a.
hrecursion.
@ -193,7 +193,7 @@ simple refine (View_rec2 _ _ _ _).
apply related_classes_eq.
unfold R in *.
eapply well_defined_union; eauto.
Defined.
Defined.
Ltac reduce :=
intros ;

6
FiniteSets/implementations/lists.v
View File

@ -8,7 +8,7 @@ Section Operations.
Global Instance list_empty A : hasEmpty (list A) := nil.
Global Instance list_single A: hasSingleton (list A) A := fun a => cons a nil.
Global Instance list_union A : hasUnion (list A).
Proof.
intros l1 l2.
@ -58,7 +58,7 @@ Section ListToSet.
* strip_truncations ; apply (tr (inl z1)).
* apply (tr (inr z2)).
Defined.
Definition empty_empty : list_to_set A ∅ = ∅ := idpath.
Lemma filter_comprehension (ϕ : A -> Bool) (l : list A) :
@ -72,7 +72,7 @@ Section ListToSet.
* rewrite nl.
apply IHl.
Defined.
Definition singleton_single (a : A) : list_to_set A (singleton a) = {|a|} :=
nr {|a|}.

20
FiniteSets/lattice.v
View File

@ -4,7 +4,7 @@ Require Import notation.
Section binary_operation.
Variable A : Type.
Class maximum :=
max_L : operation A.
@ -75,7 +75,7 @@ Section BoolLattice.
Ltac solve_bool :=
let x := fresh in
repeat (intro x ; destruct x)
repeat (intro x ; destruct x)
; compute
; auto
; try contradiction.
@ -83,12 +83,12 @@ Section BoolLattice.
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.
@ -116,7 +116,7 @@ Section BoolLattice.
Proof.
solve_bool.
Defined.
End BoolLattice.
Section fun_lattice.
@ -141,7 +141,7 @@ Section fun_lattice.
Proof.
split ; solve_fun.
Defined.
End fun_lattice.
Section sub_lattice.
@ -152,7 +152,7 @@ Section sub_lattice.
Context {Hbot : P empty_L}.
Definition AP : Type := sig P.
Instance botAP : bottom AP := (empty_L ; Hbot).
Instance maxAP : maximum AP :=
@ -174,17 +174,17 @@ Section sub_lattice.
Ltac solve_sub :=
let x := fresh in
repeat (intro x ; destruct x)
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.

44
FiniteSets/representations/T.v
View File

@ -7,7 +7,7 @@ Module Export T.
Private Inductive T (B : Type) : Type :=
| b : T B
| c : T B.
| c : T B.
Axiom p : A -> b A = c A.
Axiom setT : IsHSet (T A).
@ -23,7 +23,7 @@ Module Export T.
Variable (bP : P (b A)).
Variable (cP : P (c A)).
Variable (pP : forall a : A, (p a) # bP = cP).
(* Induction principle *)
Fixpoint T_ind
(x : T A)
@ -31,7 +31,7 @@ Module Export T.
: P x
:= (match x return _ -> _ -> P x with
| b => fun _ _ => bP
| c => fun _ _ => cP
| c => fun _ _ => cP
end) pP H.
Axiom T_ind_beta_p : forall (a : A),
@ -68,7 +68,7 @@ Module Export T.
End T_recursion.
Instance T_recursion A : HitRecursion (T A)
:= {indTy := _; recTy := _;
:= {indTy := _; recTy := _;
H_inductor := T_ind A; H_recursor := T_rec A }.
End T.
@ -119,44 +119,44 @@ Section merely_dec_lem.
Local Ltac f_prop := apply path_forall ; intro ; apply path_ishprop.
Lemma transport_code_b_x (a : A) :
Lemma transport_code_b_x (a : A) :
transport code_b (p a) = fun _ => a.
Proof.
f_prop.
Defined.
Lemma transport_code_c_x (a : A) :
Lemma transport_code_c_x (a : A) :
transport code_c (p a) = fun _ => tt.
Proof.
f_prop.
f_prop.
Defined.
Lemma transport_code_c_x_V (a : A) :
Lemma transport_code_c_x_V (a : A) :
transport code_c (p a)^ = fun _ => a.
Proof.
f_prop.
Proof.
f_prop.
Defined.
Lemma transport_code_x_b (a : A) :
Lemma transport_code_x_b (a : A) :
transport (fun x => code x (b A)) (p a) = fun _ => a.
Proof.
f_prop.
Defined.
Lemma transport_code_x_c (a : A) :
Lemma transport_code_x_c (a : A) :
transport (fun x => code x (c A)) (p a) = fun _ => tt.
Proof.
f_prop.
Defined.
Lemma transport_code_x_c_V (a : A) :
Lemma transport_code_x_c_V (a : A) :
transport (fun x => code x (c A)) (p a)^ = fun _ => a.
Proof.
f_prop.
Defined.
Lemma ap_diag {B : Type} {x y : B} (p : x = y) :
ap (fun x : B => (x, x)) p = path_prod' p p.
ap (fun x : B => (x, x)) p = path_prod' p p.
Proof.
by path_induction.
Defined.
@ -217,7 +217,7 @@ Section merely_dec_lem.
refine (transport_arrow _ _ _ @ _).
refine (transport_paths_FlFr _ _ @ _).
rewrite transport_code_c_x_V.
hott_simpl.
hott_simpl.
Defined.
Lemma transport_paths_FlFr_trunc :
@ -229,7 +229,7 @@ Section merely_dec_lem.
refine (ap tr _).
exact ((concat_1p r)^ @ (concat_p1 (1 @ r))^).
Defined.
Definition decode : forall (x y : T A), code x y -> x = y.
Proof.
simple refine (T_ind _ _ _ _ _ _); simpl.
@ -248,7 +248,7 @@ Section merely_dec_lem.
f_ap.
refine (ap (fun x => (p x)) _).
apply path_ishprop.
+ intro.
+ intro.
rewrite transport_code_x_c_V.
hott_simpl.
+ intro b.
@ -264,7 +264,7 @@ Section merely_dec_lem.
intros p. induction p.
simpl. revert u. simple refine (T_ind _ _ _ _ _ _).
+ simpl. reflexivity.
+ simpl. reflexivity.
+ simpl. reflexivity.
+ intro a.
apply set_path2.
Defined.
@ -278,12 +278,12 @@ Section merely_dec_lem.
+ simpl. intro a. apply path_ishprop.
+ intro a. apply path_forall; intros ?. apply set_path2.
- simple refine (T_ind _ _ _ _ _ _).
+ simpl. intro a. apply path_ishprop.
+ simpl. apply path_ishprop.
+ simpl. intro a. apply path_ishprop.
+ simpl. apply path_ishprop.
+ intro a. apply path_forall; intros ?. apply set_path2.
- intro a. repeat (apply path_forall; intros ?). apply set_path2.
Defined.
Instance T_hprop (a : A) : IsHProp (b A = c A).
Proof.
@ -307,7 +307,7 @@ Section merely_dec_lem.
rewrite ?decode_encode in H1.
apply H1.
Defined.
Lemma equiv_pathspace_T : (b A = c A) = A.
Proof.
apply path_iff_ishprop.

22
FiniteSets/representations/cons_repr.v
View File

@ -3,7 +3,7 @@ Require Import HoTT HitTactics.
Require Export notation.
Module Export FSetC.
Section FSetC.
Private Inductive FSetC (A : Type) : Type :=
| Nil : FSetC A
@ -14,9 +14,9 @@ Module Export FSetC.
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.
a ;; a ;; x = a ;; x.
Axiom comm : forall (a b : A) (x : FSetC A),
a ;; b ;; x = b ;; a ;; x.
@ -41,9 +41,9 @@ Module Export FSetC.
Variable (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).
Variable (commP : forall (a b: A) (x: FSetC A) (px: P x),
comm a b x # cnsP a (b;;x) (cnsP b x px) =
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)
@ -76,18 +76,18 @@ Module Export FSetC.
(* Recursion principle *)
Definition FSetC_rec : FSetC A -> P.
Proof.
simple refine (FSetC_ind _ _ _ _ _ _ _ );
simple refine (FSetC_ind _ _ _ _ _ _ _ );
try (intros; simple refine ((transport_const _ _) @ _ )); cbn.
- apply nil.
- apply (fun a => fun _ => cns a).
- apply (fun a => fun _ => cns a).
- apply duplP.
- apply commP.
- apply commP.
Defined.
Definition FSetC_rec_beta_dupl : forall (a: A) (x : FSetC A),
ap FSetC_rec (dupl a x) = duplP a (FSetC_rec x).
Proof.
intros.
intros.
eapply (cancelL (transport_const (dupl a x) _)).
simple refine ((apD_const _ _)^ @ _).
apply FSetC_ind_beta_dupl.
@ -96,7 +96,7 @@ Module Export FSetC.
Definition FSetC_rec_beta_comm : forall (a b: A) (x : FSetC A),
ap FSetC_rec (comm a b x) = commP a b (FSetC_rec x).
Proof.
intros.
intros.
eapply (cancelL (transport_const (comm a b x) _)).
simple refine ((apD_const _ _)^ @ _).
apply FSetC_ind_beta_comm.
@ -107,7 +107,7 @@ Module Export FSetC.
Instance FSetC_recursion A : HitRecursion (FSetC A) :=
{
indTy := _; recTy := _;
indTy := _; recTy := _;
H_inductor := FSetC_ind A; H_recursor := FSetC_rec A
}.

36
FiniteSets/representations/definition.v
View File

@ -14,7 +14,7 @@ Module Export FSet.
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.
@ -38,7 +38,7 @@ Module Export FSet.
Arguments comm {_} _ _.
Arguments nl {_} _.
Arguments nr {_} _.
Arguments idem {_} _.
Arguments idem {_} _.
Section FSet_induction.
Variable A: Type.
@ -47,22 +47,22 @@ Module Export FSet.
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)
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) 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),
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),
Variable (nrP : forall (x : FSet A) (px: P x),
nr x # uP x ∅ px eP = px).
Variable (idemP : forall (x : A),
Variable (idemP : forall (x : A),
idem x # uP {|x|} {|x|} (lP x) (lP x) = lP x).
(* Induction principle *)
Fixpoint FSet_ind
(x : FSet A)
@ -119,7 +119,7 @@ Module Export FSet.
Defined.
Definition FSet_rec_beta_assoc : forall (x y z : FSet A),
ap FSet_rec (assoc x y z)
ap FSet_rec (assoc x y z)
=
assocP (FSet_rec x) (FSet_rec y) (FSet_rec z).
Proof.
@ -131,7 +131,7 @@ Module Export FSet.
Defined.
Definition FSet_rec_beta_comm : forall (x y : FSet A),
ap FSet_rec (comm x y)
ap FSet_rec (comm x y)
=
commP (FSet_rec x) (FSet_rec y).
Proof.
@ -143,7 +143,7 @@ Module Export FSet.
Defined.
Definition FSet_rec_beta_nl : forall (x : FSet A),
ap FSet_rec (nl x)
ap FSet_rec (nl x)
=
nlP (FSet_rec x).
Proof.
@ -155,7 +155,7 @@ Module Export FSet.
Defined.
Definition FSet_rec_beta_nr : forall (x : FSet A),
ap FSet_rec (nr x)
ap FSet_rec (nr x)
=
nrP (FSet_rec x).
Proof.
@ -167,7 +167,7 @@ Module Export FSet.
Defined.
Definition FSet_rec_beta_idem : forall (a : A),
ap FSet_rec (idem a)
ap FSet_rec (idem a)
=
idemP a.
Proof.
@ -177,12 +177,12 @@ Module Export FSet.
simple refine ((apD_const _ _)^ @ _).
apply FSet_ind_beta_idem.
Defined.
End FSet_recursion.
Instance FSet_recursion A : HitRecursion (FSet A) :=
{
indTy := _; recTy := _;
indTy := _; recTy := _;
H_inductor := FSet_ind A; H_recursor := FSet_rec A
}.
@ -200,5 +200,5 @@ Proof.
rewrite P.
rewrite (comm y x).
rewrite <- (assoc x y y).
f_ap.
Defined.
f_ap.
Defined.

36
FiniteSets/variations/enumerated.v
View File

@ -47,7 +47,7 @@ Proof.
destruct (if P a as b return ((b = true) + (b = false))
then inl 1%path
else inr 1%path) as [Pa' | Pa'].
- rewrite Pa' in Pa. contradiction (true_ne_false Pa).
- rewrite Pa' in Pa. contradiction (true_ne_false Pa).
- reflexivity.
Defined.
@ -104,7 +104,7 @@ Defined.
Lemma enumerated_surj (A B : Type) (f : A -> B) :
IsSurjection f -> enumerated A -> enumerated B.
Proof.
intros Hsurj HeA. strip_truncations; apply tr.
intros Hsurj HeA. strip_truncations; apply tr.
destruct HeA as [eA HeA].
exists (map f eA).
intros x. specialize (Hsurj x).
@ -157,7 +157,7 @@ destruct ys as [|y ys].
Defined.
Fixpoint listProd {A B} (xs : list A) (ys : list B) : list (A * B).
Proof.
Proof.
destruct xs as [|x xs].
- exact nil.
- refine (app _ _).
@ -165,7 +165,7 @@ destruct xs as [|x xs].
+ exact (listProd _ _ xs ys).
Defined.
Lemma listExt_prod_sing {A B} (x : A) (y : B) (ys : list B) :
Lemma listExt_prod_sing {A B} (x : A) (y : B) (ys : list B) :
listExt ys y -> listExt (listProd_sing x ys) (x, y).
Proof.
induction ys; simpl.
@ -193,11 +193,11 @@ induction xs as [| x' xs]; intros x y.
rewrite <- Hyy' in IHxs.
apply listExt_app_l. apply IHxs. assumption.
simpl. apply tr. left. apply tr. reflexivity.
* right.
* right.
apply listExt_app_l.
apply IHxs. assumption.
simpl. apply tr. right. assumption.
Defined.
Defined.
(** Properties of enumerated sets: closed under products *)
Lemma enumerated_prod (A B : Type) `{Funext} :
@ -221,7 +221,7 @@ Section enumerated_fset.
| nil => ∅
| cons x xs => {|x|} ∪ (list_to_fset xs)
end.
Lemma list_to_fset_ext (ls : list A) (a : A):
listExt ls a -> a ∈ (list_to_fset ls).
Proof.
@ -250,8 +250,8 @@ End enumerated_fset.
Section fset_dec_enumerated.
Variable A : Type.
Context `{Univalence}.
Definition Kf_fsetc :
Definition Kf_fsetc :
Kf A -> exists (X : FSetC A), forall (a : A), k_finite.map (FSetC_to_FSet X) a.
Proof.
intros [X HX].
@ -260,7 +260,7 @@ Section fset_dec_enumerated.
by rewrite <- HX.
Defined.
Definition merely_enumeration_FSetC :
Definition merely_enumeration_FSetC :
forall (X : FSetC A),
hexists (fun (ls : list A) => forall a, a ∈ (FSetC_to_FSet X) = listExt ls a).
Proof.
@ -274,13 +274,13 @@ Section fset_dec_enumerated.
- intros. apply path_ishprop.
- intros. apply path_ishprop.
Defined.
Definition Kf_enumerated : Kf A -> enumerated A.
Proof.
intros HKf. apply Kf_fsetc in HKf.
destruct HKf as [X HX].
pose (ls' := (merely_enumeration_FSetC X)).
simple refine (@Trunc_rec _ _ _ _ _ ls'). clear ls'.
pose (ls' := (merely_enumeration_FSetC X)).
simple refine (@Trunc_rec _ _ _ _ _ ls'). clear ls'.
intros [ls Hls].
apply tr. exists ls.
intros a. rewrite <- Hls. apply (HX a).
@ -293,7 +293,7 @@ Section subobjects.
Definition enumeratedS (P : Sub A) : hProp :=
enumerated (sigT P).
Lemma enumeratedS_empty : closedEmpty enumeratedS.
Proof.
unfold enumeratedS.
@ -319,7 +319,7 @@ Section subobjects.
- apply (cons (x; tr (inr Hx))).
apply (weaken_list_r _ _ ls).
Defined.
Lemma listExt_weaken (P Q : Sub A) (ls : list (sigT Q)) (x : A) (Hx : Q x) :
listExt ls (x; Hx) -> listExt (weaken_list_r P Q ls) (x; tr (inr Hx)).
Proof.
@ -333,7 +333,7 @@ Section subobjects.
exists (Hxy..1). apply path_ishprop.
+ right. apply IHls. assumption.
Defined.
Fixpoint concatD {P Q : Sub A}
(ls : list (sigT P)) (ls' : list (sigT Q)) : list (sigT (max_L P Q)).
Proof.
@ -382,9 +382,9 @@ Section subobjects.
Defined.
Opaque enumeratedS.
Definition FSet_to_enumeratedS :
Definition FSet_to_enumeratedS :
forall (X : FSet A), enumeratedS (k_finite.map X).
Proof.
Proof.
hinduction.
- apply enumeratedS_empty.
- intros a. apply enumeratedS_singleton.

2
FiniteSets/variations/k_finite.v
View File

@ -100,7 +100,7 @@ Section structure_k_finite.
exists {|a|}.
cbn.
apply path_forall.
intro z.
intro z.
reflexivity.
Defined.