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

Get rid of cow induction for the proof of `closedUnion Bfin`

This commit is contained in:
Dan Frumin 2017-08-24 11:35:58 +02:00 committed by Dan Frumin
parent e1a8220ba0
commit eef533e345
1 changed files with 113 additions and 103 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

216
FiniteSets/variations/b_finite.v
View File

@ -156,7 +156,7 @@ Section finite_hott.
(Xequiv : {a : A & P a } <~> Fin n + Unit). (Xequiv : {a : A & P a } <~> Fin n + Unit).
Definition split : exists P' : Sub A, exists b : A, Definition split : exists P' : Sub A, exists b : A,
({a : A & P' a} <~> Fin n) * (forall x, P x = P' x ∨ merely (x = b)). ({a : A & P' a} <~> Fin n) * (forall x, P x = (P' x ∨ merely (x = b))).
Proof. Proof.
destruct Xequiv as [f [g fg gf adj]]. destruct Xequiv as [f [g fg gf adj]].
unfold Sect in *. unfold Sect in *.
@ -369,109 +369,119 @@ Section cowd.
Lemma kfin_is_bfin : @closedUnion A Bfin. Lemma kfin_is_bfin : @closedUnion A Bfin.
Proof. Proof.
intros X Y HX HY. intros X Y HX HY.
pose (Xcow := (X; HX) : cow). destruct HX as [n fX].
pose (Ycow := (Y; HY) : cow). strip_truncations.
simple refine (cowy (fun C => Bfin (C.1 ∪ Y)) _ _ Xcow); simpl. revert fX. revert X.
- assert ((fun a => Trunc (-1) (Empty + Y a)) = (fun a => Y a)) as Help. induction n; intros X fX.
{ apply path_forall. intros z; simpl. - destruct HY as [m fY]. strip_truncations.
apply path_iff_ishprop. exists m. apply tr.
+ intros; strip_truncations; auto. transitivity {a : A & a ∈ Y}; [ | assumption ].
destruct X0; auto. destruct e. apply equiv_functor_sigma_id.
+ intros ?. apply tr. right; assumption. intros a.
(* TODO FIX THIS with sum_empty_l *) apply equiv_iff_hprop.
} * intros Ha. strip_truncations.
rewrite Help. apply HY. destruct Ha as [Ha | Ha]; [ | apply Ha ].
- intros a [X' HX'] [n FX'Y]. strip_truncations. contradiction (fX (a;Ha)).
destruct (dec(a ∈ X')) as [HaX' | HaX']. * intros Ha. apply tr. by right.
* exists n. apply tr. - destruct (split _ X n fX) as
transitivity ({a : A & Trunc (-1) (X' a + Y a)}); [| assumption ]. (X' & b & HX' & HX).
apply equiv_functor_sigma_id. intro a'. assert (Bfin X') by (eexists; apply (tr HX')).
apply equiv_iff_hprop. destruct (dec (b ∈ X')) as [HX'b | HX'b].
{ intros Q. strip_truncations. + cut (X ∪ Y = X' ∪ Y).
destruct Q as [Q | Q]. { intros HXY. rewrite HXY.
- strip_truncations. by apply IHn. }
apply tr. left. apply path_forall. intro a.
destruct Q ; auto. unfold union, sub_union, lattice.max_fun.
strip_truncations. rewrite t; assumption. apply path_iff_hprop.
- apply (tr (inr Q)). } * intros Ha.
{ intros Q. strip_truncations. strip_truncations.
destruct Q as [Q | Q]; apply tr. destruct Ha as [HXa | HYa]; [ | apply tr; by right ].
- left. apply tr. left. done. rewrite HX in HXa.
- right. done. } strip_truncations.
* destruct (dec (a ∈ Y)) as [HaY | HaY ]. destruct HXa as [HX'a | Hab];
** exists n. apply tr. [ | strip_truncations ]; apply tr; left.
transitivity ({a : A & Trunc (-1) (X' a + Y a)}); [| assumption ]. ** done.
apply equiv_functor_sigma_id. intro a'. ** rewrite Hab. apply HX'b.
apply equiv_iff_hprop. * intros Ha.
{ intros Q. strip_truncations. strip_truncations. apply tr.
destruct Q as [Q | Q]. destruct Ha as [HXa | HYa]; [ left | by right ].
- strip_truncations. rewrite HX. apply (tr (inl HXa)).
apply tr. + (* b ∉ X' *)
destruct Q. destruct (IHn X' HX') as [n' fw].
left. auto. strip_truncations.
right. strip_truncations. rewrite t; assumption. destruct (dec (b ∈ Y)) as [HYb | HYb].
- apply (tr (inr Q)). } { exists n'. apply tr.
{ intros Q. strip_truncations. transitivity {a : A & a ∈ X' ∪ Y}; [ | apply fw ].
destruct Q as [Q | Q]; apply tr. apply equiv_functor_sigma_id. intro a.
- left. apply tr. left. done. apply equiv_iff_hprop; cbn; simple refine (Trunc_rec _).
- right. done. } { intros [HXa | HYa].
** exists (n.+1). apply tr. - rewrite HX in HXa.
destruct FX'Y as [f [g Hfg Hgf adj]].
unshelve esplit.
{ intros [a' Ha']. cbn in Ha'.
destruct (dec (BuildhProp (a' = a))) as [Ha'a | Ha'a].
- right. apply tt.
- left. refine (f (a';_)).
strip_truncations. strip_truncations.
destruct Ha' as [Ha' | Ha']. destruct HXa as [HX'a | Hab]; apply tr.
+ strip_truncations. * by left.
destruct Ha' as [Ha' | Ha']. * right. strip_truncations.
* apply (tr (inl Ha')). rewrite Hab. apply HYb.
* strip_truncations. contradiction. - apply tr. by right. }
+ apply (tr (inr Ha')). } { intros [HX'a | HYa]; apply tr.
{ apply isequiv_biinv; simpl. * left. rewrite HX.
unshelve esplit; simpl. apply (tr (inl HX'a)).
- unfold Sect; simpl. * by right. } }
simple refine (_;_). { exists (n'.+1).
{ destruct 1 as [M | ?]. apply tr.
- destruct (g M) as [a' Ha']. unshelve eapply BuildEquiv.
exists a'. { intros [a Ha]. cbn in Ha.
strip_truncations; apply tr. destruct (dec (BuildhProp (a = b))) as [Hab | Hab].
destruct Ha' as [Ha' | Ha']. - right. apply tt.
+ left. apply (tr (inl Ha')). - left. refine (fw (a;_)).
+ right. done. strip_truncations. apply tr.
- exists a. apply (tr (inl (tr (inr (tr idpath))))). } destruct Ha as [HXa | HYa].
{ intros [a' Ha']; simpl. + left. rewrite HX in HXa.
strip_truncations. strip_truncations.
destruct Ha' as [HXa' | Haa']; simpl; destruct HXa as [HX'a | Hab']; [apply HX'a |].
destruct (dec (a' = a)); simpl. strip_truncations. contradiction.
** apply path_sigma' with p^. apply path_ishprop. + right. apply HYa. }
** rewrite Hgf; cbn. apply path_sigma' with idpath. apply path_ishprop. { apply isequiv_biinv.
** apply path_sigma' with p^. apply path_ishprop. unshelve esplit; cbn.
** rewrite Hgf; cbn. done. } - unshelve eexists.
- unfold Sect; simpl. + intros [m | []].
simple refine (_;_). * destruct (fw^-1 m) as [a Ha].
{ destruct 1 as [M | ?]. exists a.
- (* destruct (g M) as [a' Ha']. *) strip_truncations. apply tr.
exists (g M).1. destruct Ha as [HX'a | HYa]; [ left | by right ].
simple refine (Trunc_rec _ (g M).2). rewrite HX.
intros Ha'. apply (tr (inl HX'a)).
apply tr. * exists b.
(* strip_truncations; apply tr. *) rewrite HX.
destruct Ha' as [Ha' | Ha']. apply (tr (inl (tr (inr (tr idpath))))).
+ left. apply (tr (inl Ha')). + intros [a Ha]; cbn.
+ right. done. strip_truncations.
- exists a. apply (tr (inl (tr (inr (tr idpath))))). } simple refine (path_sigma' _ _ _); [ | apply path_ishprop ].
simpl. intros [M | [] ]. destruct (H a b); cbn.
** destruct (dec (_ = a)) as [Haa' | Haa']; simpl. * apply p^.
{ destruct (g M) as [a' Ha']. simpl in Haa'. * rewrite eissect; cbn.
strip_truncations. reflexivity.
rewrite Haa' in Ha'. destruct Ha'; by contradiction. } - unshelve eexists. (* TODO: Duplication!! *)
{ f_ap. transitivity (f (g M)); [ | apply Hfg]. + intros [m | []].
f_ap. apply path_sigma' with idpath. * exists (fw^-1 m).1.
apply path_ishprop. } simple refine (Trunc_rec _ (fw^-1 m).2).
** destruct (dec (a = a)); try by contradiction. intros [HX'a | HYa]; apply tr; [ left | by right ].
reflexivity. } 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.
End cowd. End cowd.