Separation
Section Separation.
Variable X : HF.
Implicit Types x y z a u : X.
Variable p : decPred X.
Lemma sep' x :
Sigma u, forall z, z el u <-> z el x /\ p z.
Proof.
hf_induction x.
- exists 0. hfs.
- intros a x _ (u&IH).
destruct (decPred_dec p a).
+ exists (a@u). hfs.
+ exists u. hfs.
Qed.
Definition sep x := projT1 (sep' x).
Fact sep_el x z :
z el sep x <-> z el x /\ p z.
Proof.
unfold sep. destruct (sep' x) as (u&A). auto.
Qed.
End Separation.
Replacement
Section Replacement.
Variable X : HF.
Implicit Types x y z a u : X.
Variable f : X -> X.
Lemma rep' x :
Sigma u, forall z, z el u <-> exists a, a el x /\ f a = z.
Proof.
hf_induction x.
- exists 0. hfs.
- intros a x _ (u&IH). exists (f a @ u). hfs.
Qed.
Definition rep x := projT1 (rep' x).
Fact rep_el x z :
z el rep x <-> exists a, a el x /\ f a = z.
Proof.
unfold rep. destruct (rep' x) as (u&A). auto.
Qed.
End Replacement.
Binary union
Section BinaryUnion.
Variable X : HF.
Implicit Types x y z a u : X.
Lemma bun' x y :
Sigma u, forall z, z el u <-> z el x \/ z el y.
Proof.
hf_induction x.
- exists y. hfs.
- intros a x _ (u&IH). exists (a@u). hfs.
Qed.
Definition bun x y := projT1 (bun' x y).
Fact bun_el x y z :
z el bun x y <-> z el x \/ z el y.
Proof.
unfold bun. destruct (bun' x y) as (u&A); cbn. auto.
Qed.
End BinaryUnion.
Big union
Section BigUnion.
Variable X : HF.
Implicit Types x y z a u : X.
Lemma union' x :
Sigma u, forall z, z el u <-> exists z', z el z' /\ z' el x.
Proof.
hf_induction x.
- exists 0. hfs.
- intros a x _ (u&IH). exists (bun a u).
intros z. rewrite bun_el. hfs.
Qed.
Definition union x := projT1 (union' x).
Fact union_el x z :
z el union x <-> exists y, y el x /\ z el y.
Proof.
unfold union. destruct (union' x) as (u&A); cbn. hfs.
Qed.
Fact unionE_eq :
union 0 = 0.
Proof.
extensio as z. rewrite union_el. hfs.
Qed.
Fact union_el_incl x y :
y el x -> y <<= union x.
Proof.
intros A z B. apply union_el. eauto.
Qed.
Fact union_incl x v :
(forall z, z el x -> z <<= v) -> union x <<= v.
Proof.
intros A z. rewrite union_el. hfs.
Qed.
Fact union_lub u x :
union x = u <->
(forall z, z el x -> z <<= u) /\
(forall v, (forall z, z el x -> z <<= v) -> u <<= v).
Proof.
split.
- intros A. subst u. split.
+ apply union_el_incl.
+ apply union_incl.
- intros [A B]. extensio as z. split.
+ rewrite union_el. hfs.
+ intros C. apply B. apply union_el_incl. exact C.
Qed.
Fact union_sing_eq a :
union (a@0) = a.
Proof.
extensio as z. rewrite union_el. hfs.
Qed.
Fact unionA_incl_eq a x :
union x <<= a -> union (a@x) = a.
Proof.
intros A. apply union_lub. split.
- intros z [-> |B] % adj_el. hfs.
intros y C. apply A. revert y C. now apply union_el_incl.
- intros v B. apply B. hfs.
Qed.
Fact unionA_incl_eq' a x :
a <<= union x -> union (a@x) = union x.
Proof.
intros B. extensio as z.
rewrite !union_el. split; intros (y&C&D).
- apply adj_el in C as [-> |C].
+ apply union_el. hfs.
+ eauto.
- exists y. hfs.
Qed.
Fact succ_inv x :
trans x -> union (x@x) = x.
Proof.
unfold trans. intros A. extensio as z. rewrite union_el. hfs.
Qed.
End BigUnion.
Big intersection
Section BigIntersection.
Variable X : HF.
Implicit Types x y z : X.
Definition inter x :=
sep (DecPred (fun z => forall y, y el x -> z el y)) (union x).
Fact inter_el x z (A : inhab x) :
z el inter x <-> forall y, y el x -> z el y.
Proof.
unfold inter. rewrite sep_el, union_el. hfs.
Qed.
Fact inter_el_incl x y :
y el x -> inter x <<= y.
Proof.
intros A z. rewrite inter_el; hfs.
Qed.
Lemma inter_incl u x (A : inhab x) :
u <<= inter x <-> forall y, y el x -> u <<= y.
Proof.
split.
- intros B y C z D % B. rewrite inter_el in D; hfs.
- intros B z C. apply inter_el; hfs.
Qed.
Lemma inter_glb x (A : inhab x) u :
inter x = u <->
(forall z, z el x -> u <<= z) /\
(forall v, (forall z, z el x -> v <<= z) -> v <<= u).
Proof.
split.
- intros B. subst u. split.
+ intros y. apply inter_el_incl.
+ intros v. now apply inter_incl.
- intros [B C]. extensio as z. split.
+ apply C. intros y. apply inter_el_incl.
+ intros D. apply inter_el; hfs.
Qed.
Fact inter_sing_eq a :
inter (a@0) = a.
Proof.
apply inter_glb.
- hfs.
- split. hfs. intros x A. apply A. hfs.
Qed.
Fact interA_incl_eq a x :
a <<= inter x -> inter (a@x) = a.
Proof.
intros A. apply inter_glb. hfs. split.
- intros z [-> |B] % adj_el. hfs.
apply (@inter_incl a x); hfs.
- intros v B. apply B. hfs.
Qed.
Fact interA_incl_eq' a x :
inhab x -> inter x <<= a -> inter (a@x) = inter x.
Proof.
intros A B. extensio as z.
rewrite !inter_el; [|hfs| hfs].
split; intros C y D.
- apply C; hfs.
- apply adj_el in D as [-> |D]; [|now auto].
apply B. apply inter_el. exact A. exact C.
Qed.
End BigIntersection.
Chains
Section Chain.
Variable X : HF.
Implicit Types x y z a u : X.
Definition chain u := forall x y, x el u -> y el u -> x <<= y \/ y <<= x.
Fact chainA a x :
chain (a@x) -> chain x.
Proof.
intros A y z B C. apply A; hfs.
Qed.
Fact chain_union x :
inhab x -> chain x -> union x el x.
Proof.
hf_induction x.
- hfs.
- intros a x _ IH A B.
decide (x=0) as [-> |C].
+ rewrite union_sing_eq. hfs.
+ assert (D: union x el x).
{ apply IH. hfs. eapply chainA, B. }
assert (a <<= union x \/ union x <<= a) as [E|E].
* apply B; hfs.
* rewrite unionA_incl_eq'; hfs.
* rewrite unionA_incl_eq; hfs.
Qed.
Fact chain_inter x :
inhab x -> chain x -> inter x el x.
Proof.
hf_induction x.
- hfs.
- intros a x _ IH A B.
decide (x=0) as [->|C].
+ rewrite inter_sing_eq. hfs.
+ assert (D: inter x el x).
{ apply IH. hfs. eapply chainA, B. }
assert (a <<= inter x \/ inter x <<= a) as [E|E].
* apply B; hfs.
* rewrite interA_incl_eq; hfs.
* rewrite interA_incl_eq'; hfs.
Qed.
End Chain.
Power
Section Power.
Variable X : HF.
Implicit Types x y z a u : X.
Lemma power' x :
Sigma u, forall z, z el u <-> z <<= x.
Proof.
hf_induction x.
- exists (0@0). hfs.
- intros a x _ (u&IH).
exists (bun u (rep (adj a) u)).
intros z. rewrite bun_el, rep_el. split.
+ hfs.
+ intros A.
decide (a el x) as [B|B]. hfs.
decide (a el z) as [C|C]; [|hfs].
right. apply part in C as (v&->&C). exists v. hfs.
Qed.
Definition power x := projT1 (power' x).
Fact power_el x z :
z el power x <-> z <<= x.
Proof.
unfold power. destruct (power' x) as (u&A). hfs.
Qed.
End Power.
Singletons and unordered pairs
Section SingUnorderedPair.
Variable X : HF.
Implicit Types x y z : X.
Fact sing_el z x :
z el x@0 <-> z = x.
Proof.
hfs.
Qed.
Fact sing_injective x y :
x@0 = y@0 -> x=y.
Proof.
intros A. apply sing_el. rewrite <- A. hfs.
Qed.
Fact upair_el x y z :
z el x@y@0 <-> z = x \/ z = y.
Proof.
hfs.
Qed.
Fact upair_injective x y a b :
x@y@0 = a@b@0 -> x=a /\ y=b \/ x=b /\ y=a.
Proof.
intros A.
assert (B: x=a \/ x=b).
{ apply upair_el. rewrite <- A; hfs. }
assert (C: y=a \/ y=b).
{ apply upair_el. rewrite <- A. hfs. }
assert (D: a=x \/ a=y).
{ apply upair_el. rewrite A; hfs. }
assert (E: b=x \/ b=y).
{ apply upair_el. rewrite A; hfs. }
hfs.
Qed.
Lemma upair_sing x y z :
x@y@0 = z@0 -> x = y /\ x = z.
Proof.
rewrite <- (cancel z).
intros A % upair_injective. hfs.
Qed.
End SingUnorderedPair.
Ordered pairs
Section Pairs.
Variable X : HF.
Implicit Types x y z : X.
Definition pair x y := (x @ 0) @ (x @ y @ 0) @ 0.
Definition pi1 x := union (inter x).
Definition pi2 x := union (sep (DecPred (fun z => pair (pi1 x) z = x)) (union x)).
Fact pair_injective x y a b :
pair x y = pair a b -> x = a /\ y = b.
Proof.
intros [(A&B)|(A&B)] % upair_injective.
- apply sing_injective in A as <-.
apply upair_injective in B. hfs.
- symmetry in A. apply upair_sing in A; apply upair_sing in B. hfs.
Qed.
Lemma union_pair_eq x y :
union (pair x y) = x@y@0.
Proof.
unfold pair. apply union_lub. split.
- hfs.
- intros u A. apply A. hfs.
Qed.
Lemma inter_pair_eq x y :
inter (pair x y) = x@0.
Proof.
unfold pair. apply inter_glb.
- exists (x@0). hfs.
- split.
+ hfs.
+ intros u A. apply A. hfs.
Qed.
Fact pi1_eq x y :
pi1 (pair x y) = x.
Proof.
unfold pi1. rewrite inter_pair_eq. apply union_sing_eq.
Qed.
Fact pi2_eq x y :
pi2 (pair x y) = y.
Proof.
unfold pi2. rewrite union_pair_eq, pi1_eq.
rewrite union_lub. split.
- intros z (_&B) % sep_el.
apply pair_injective in B as [_ B]. hfs.
- intros v B. apply B, sep_el. hfs.
Qed.
Definition product x y := union (rep (fun a => (rep (pair a) y)) x).
Fact product_el x y z :
z el product x y <-> exists a, a el x /\ exists b, b el y /\ z = pair a b.
Proof.
unfold product. rewrite union_el. split.
- intros (z' & (a&A&<-)%rep_el &B).
apply rep_el in B as (b&B&<-). hfs.
- intros (a&A&b&B&->). exists (rep (pair a) y).
rewrite !rep_el. hfs.
Qed.
End Pairs.