mirror of https://github.com/nmvdw/HITs-Examples
Simplify the `bfin_union` proof.
This commit is contained in:
parent
28a9e95fea
commit
c2babb9422
|
|
@ -1,6 +1,7 @@
|
||||||
(* Bishop-finiteness is that "default" notion of finiteness in the HoTT library *)
|
(* Bishop-finiteness is that "default" notion of finiteness in the HoTT library *)
|
||||||
Require Import HoTT HitTactics.
|
Require Import HoTT HitTactics.
|
||||||
Require Import sub subobjects.k_finite FSets prelude.
|
Require Import FSets interfaces.lattice_interface.
|
||||||
|
From subobjects Require Import sub k_finite.
|
||||||
|
|
||||||
Section finite_hott.
|
Section finite_hott.
|
||||||
Variable (A : Type).
|
Variable (A : Type).
|
||||||
|
|
@ -354,7 +355,54 @@ Section kfin_bfin.
|
||||||
Variable (A : Type).
|
Variable (A : Type).
|
||||||
Context `{DecidablePaths A} `{Univalence}.
|
Context `{DecidablePaths A} `{Univalence}.
|
||||||
|
|
||||||
Lemma bfin_union : @closedUnion A Bfin.
|
Lemma notIn_ext_union_singleton (b : A) (Y : Sub A) :
|
||||||
|
~ (b ∈ Y) ->
|
||||||
|
{a : A & a ∈ ({|b|} ∪ Y)} <~> {a : A & a ∈ Y} + Unit.
|
||||||
|
Proof.
|
||||||
|
intros HYb.
|
||||||
|
unshelve eapply BuildEquiv.
|
||||||
|
{ intros [a Ha]. cbn in Ha.
|
||||||
|
destruct (dec (BuildhProp (a = b))) as [Hab | Hab].
|
||||||
|
- right. apply tt.
|
||||||
|
- left. exists a.
|
||||||
|
strip_truncations.
|
||||||
|
destruct Ha as [HXa | HYa].
|
||||||
|
+ refine (Empty_rec _).
|
||||||
|
strip_truncations.
|
||||||
|
by apply Hab.
|
||||||
|
+ apply HYa. }
|
||||||
|
{ apply isequiv_biinv.
|
||||||
|
unshelve esplit; cbn.
|
||||||
|
- unshelve eexists.
|
||||||
|
+ intros [[a Ha] | []].
|
||||||
|
* exists a.
|
||||||
|
apply tr.
|
||||||
|
right. apply Ha.
|
||||||
|
* exists b.
|
||||||
|
apply (tr (inl (tr idpath))).
|
||||||
|
+ intros [a Ha]; cbn.
|
||||||
|
strip_truncations.
|
||||||
|
simple refine (path_sigma' _ _ _); [ | apply path_ishprop ].
|
||||||
|
destruct (H a b); cbn.
|
||||||
|
* apply p^.
|
||||||
|
* reflexivity.
|
||||||
|
- unshelve eexists. (* TODO ACHTUNG CODE DUPLICATION *)
|
||||||
|
+ intros [[a Ha] | []].
|
||||||
|
* exists a.
|
||||||
|
apply tr.
|
||||||
|
right. apply Ha.
|
||||||
|
* exists b.
|
||||||
|
apply (tr (inl (tr idpath))).
|
||||||
|
+ intros [[a Ha] | []]; cbn.
|
||||||
|
destruct (dec (_ = b)) as [Hb | Hb]; cbn.
|
||||||
|
{ refine (Empty_rec _).
|
||||||
|
rewrite Hb in Ha.
|
||||||
|
contradiction. }
|
||||||
|
{ reflexivity. }
|
||||||
|
destruct (dec (b = b)); [ reflexivity | contradiction ]. }
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Theorem bfin_union : @closedUnion A Bfin.
|
||||||
Proof.
|
Proof.
|
||||||
intros X Y HX HY.
|
intros X Y HX HY.
|
||||||
destruct HX as [n fX].
|
destruct HX as [n fX].
|
||||||
|
|
@ -373,102 +421,46 @@ Section kfin_bfin.
|
||||||
* intros Ha. apply tr. by right.
|
* intros Ha. apply tr. by right.
|
||||||
- destruct (split X n fX) as
|
- destruct (split X n fX) as
|
||||||
(X' & b & HX' & HX).
|
(X' & b & HX' & HX).
|
||||||
assert (Bfin X') by (eexists; apply (tr HX')).
|
assert (Bfin (X'∪ Y)) by (by apply IHn).
|
||||||
destruct (dec (b ∈ X')) as [HX'b | HX'b].
|
destruct (dec (b ∈ (X' ∪ Y))) as [HX'Yb | HX'Yb].
|
||||||
+ cut (X ∪ Y = X' ∪ Y).
|
+ cut (X ∪ Y = X' ∪ Y).
|
||||||
{ intros HXY. rewrite HXY.
|
{ intros HXY. rewrite HXY. assumption. }
|
||||||
by apply IHn. }
|
|
||||||
apply path_forall. intro a.
|
apply path_forall. intro a.
|
||||||
|
unfold union, sub_union, max_fun.
|
||||||
|
rewrite HX.
|
||||||
|
rewrite (commutative (X' a)).
|
||||||
|
rewrite (associativity _ (X' a)).
|
||||||
apply path_iff_hprop.
|
apply path_iff_hprop.
|
||||||
* intros Ha.
|
* intros Ha.
|
||||||
strip_truncations.
|
strip_truncations.
|
||||||
destruct Ha as [HXa | HYa]; [ | apply tr; by right ].
|
destruct Ha as [HXa | HYa]; [ | assumption ].
|
||||||
rewrite HX in HXa.
|
|
||||||
strip_truncations.
|
strip_truncations.
|
||||||
destruct HXa as [HX'a | Hab];
|
rewrite HXa.
|
||||||
[ | strip_truncations ]; apply tr; left.
|
by apply tr.
|
||||||
** done.
|
|
||||||
** rewrite Hab. apply HX'b.
|
|
||||||
* intros Ha.
|
* intros Ha.
|
||||||
strip_truncations. apply tr.
|
apply (tr (inr Ha)).
|
||||||
destruct Ha as [HXa | HYa]; [ left | by right ].
|
+ destruct (IHn X' HX') as [n' fw].
|
||||||
rewrite HX. apply (tr (inl HXa)).
|
|
||||||
+ (* b ∉ X' *)
|
|
||||||
destruct (IHn X' HX') as [n' fw].
|
|
||||||
strip_truncations.
|
strip_truncations.
|
||||||
destruct (dec (b ∈ Y)) as [HYb | HYb].
|
exists (n'.+1).
|
||||||
{ exists n'. apply tr.
|
|
||||||
transitivity {a : A & a ∈ X' ∪ Y}; [ | apply fw ].
|
|
||||||
apply equiv_functor_sigma_id. intro a.
|
|
||||||
apply equiv_iff_hprop; cbn; simple refine (Trunc_rec _).
|
|
||||||
{ intros [HXa | HYa].
|
|
||||||
- rewrite HX in HXa.
|
|
||||||
strip_truncations.
|
|
||||||
destruct HXa as [HX'a | Hab]; apply tr.
|
|
||||||
* by left.
|
|
||||||
* right. strip_truncations.
|
|
||||||
rewrite Hab. apply HYb.
|
|
||||||
- apply tr. by right. }
|
|
||||||
{ intros [HX'a | HYa]; apply tr.
|
|
||||||
* left. rewrite HX.
|
|
||||||
apply (tr (inl HX'a)).
|
|
||||||
* by right. } }
|
|
||||||
{ exists (n'.+1).
|
|
||||||
apply tr.
|
apply tr.
|
||||||
unshelve eapply BuildEquiv.
|
transitivity ({a : A & a ∈ (fun a => merely (a = b)) ∪ (X' ∪ Y)}).
|
||||||
{ intros [a Ha]. cbn in Ha.
|
{ apply equiv_functor_sigma_id.
|
||||||
destruct (dec (BuildhProp (a = b))) as [Hab | Hab].
|
intro a.
|
||||||
- right. apply tt.
|
rewrite <- (associative_max (Sub A)).
|
||||||
- left. refine (fw (a;_)).
|
assert (X = X' ∪ (fun a => merely (a = b))) as HX_.
|
||||||
strip_truncations. apply tr.
|
{ apply path_forall. intros ?.
|
||||||
destruct Ha as [HXa | HYa].
|
unfold union, sub_union, max_fun.
|
||||||
+ left. rewrite HX in HXa.
|
apply HX. }
|
||||||
strip_truncations.
|
rewrite HX_.
|
||||||
destruct HXa as [HX'a | Hab']; [apply HX'a |].
|
rewrite <- (commutative_max (Sub A) X').
|
||||||
strip_truncations. contradiction.
|
reflexivity. }
|
||||||
+ right. apply HYa. }
|
cbn[Fin].
|
||||||
{ apply isequiv_biinv.
|
etransitivity. apply (notIn_ext_union_singleton b _ HX'Yb).
|
||||||
unshelve esplit; cbn.
|
(* TODO: rewrite fw does not work *)
|
||||||
- unshelve eexists.
|
apply equiv_path.
|
||||||
+ intros [m | []].
|
f_ap.
|
||||||
* destruct (fw^-1 m) as [a Ha].
|
apply (equiv_path _ _)^-1.
|
||||||
exists a.
|
apply fw.
|
||||||
strip_truncations. apply tr.
|
|
||||||
destruct Ha as [HX'a | HYa]; [ left | by right ].
|
|
||||||
rewrite HX.
|
|
||||||
apply (tr (inl HX'a)).
|
|
||||||
* exists b.
|
|
||||||
rewrite HX.
|
|
||||||
apply (tr (inl (tr (inr (tr idpath))))).
|
|
||||||
+ intros [a Ha]; cbn.
|
|
||||||
strip_truncations.
|
|
||||||
simple refine (path_sigma' _ _ _); [ | apply path_ishprop ].
|
|
||||||
destruct (H a b); cbn.
|
|
||||||
* apply p^.
|
|
||||||
* rewrite eissect; cbn.
|
|
||||||
reflexivity.
|
|
||||||
- unshelve eexists. (* TODO: Duplication!! *)
|
|
||||||
+ intros [m | []].
|
|
||||||
* exists (fw^-1 m).1.
|
|
||||||
simple refine (Trunc_rec _ (fw^-1 m).2).
|
|
||||||
intros [HX'a | HYa]; apply tr; [ left | by right ].
|
|
||||||
rewrite HX.
|
|
||||||
apply (tr (inl HX'a)).
|
|
||||||
* exists b.
|
|
||||||
rewrite HX.
|
|
||||||
apply (tr (inl (tr (inr (tr idpath))))).
|
|
||||||
+ intros [m | []]; cbn.
|
|
||||||
destruct (dec (_ = b)) as [Hb | Hb]; cbn.
|
|
||||||
{ destruct (fw^-1 m) as [a Ha]. simpl in Hb.
|
|
||||||
simple refine (Trunc_rec _ Ha). clear Ha.
|
|
||||||
rewrite Hb.
|
|
||||||
intros [HX'b2 | HYb2]; contradiction. }
|
|
||||||
{ f_ap. transitivity (fw (fw^-1 m)).
|
|
||||||
- f_ap.
|
|
||||||
apply path_sigma' with idpath.
|
|
||||||
apply path_ishprop.
|
|
||||||
- apply eisretr. }
|
|
||||||
destruct (dec (b = b)); [ reflexivity | contradiction ]. } }
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition FSet_to_Bfin : forall (X : FSet A), Bfin (map X).
|
Definition FSet_to_Bfin : forall (X : FSet A), Bfin (map X).
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue