Operations


Require Export HFS.Extensionality.

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.