Aczel_sets.v

From Coq.Classes Require Import RelationClasses Morphisms.
From Coq.Setoids Require Import Setoid.

Inductive Ens : Type :=
  ens_intro : forall A : Type, (A -> Ens) -> Ens.

Definition idx (A : Ens) : Type := match A with ens_intro T _ => T end.

Definition elem (A : Ens) (i : idx A) : Ens :=
  match A as u return idx u -> Ens with ens_intro B f => fun j => f j end i.

Inductive equiv : Ens -> Ens -> Prop :=
  equiv_intro A B :
    (forall i, exists j, equiv (elem A i) (elem B j)) ->
    (forall j, exists i, equiv (elem B j) (elem A i)) ->
    equiv A B.

Infix "≡" := equiv (at level 70, no associativity).

Global Instance equiv_refl : Reflexive equiv.
Proof. intros A; induction A; constructor; eauto. Qed.

Global Instance equiv_sym : Symmetric equiv.
Proof. inversion 1; subst; constructor; auto. Qed.

Global Instance equiv_trans : Transitive equiv.
Proof.
  intros A; induction A as [TA f IHf]; intros B C.
  inversion 1 as [? ? HAB HBA]; subst; inversion 1 as [? ? HBC HCB]; subst.
  constructor.
  - intros i.
    destruct (HAB i) as [j Hj].
    destruct (HBC j) as [k Hk].
    eauto.
  - intros k.
    destruct (HCB k) as [j Hj].
    destruct (HBA j) as [i Hi].
    exists i; apply equiv_sym; eapply IHf; apply equiv_sym; eauto.
Qed.

Global Instance equiv_rewrite_relation : RewriteRelation equiv | 150 := {}.

Definition elem_of (x A : Ens) := exists a, (elem A a) ≡ x.

Infix "∈" := elem_of (at level 70).

Lemma elem_elem_of A i : (elem A i) ∈ A.
Proof. exists i; reflexivity. Qed.

Lemma extensionality A B : A ≡ B <-> forall x, x ∈ A <-> x ∈ B.
Proof.
  split.
  - inversion 1 as [? ? HAB HBA]; subst.
    intros x; split; intros [i Hi].

    + destruct (HAB i) as [j Hj].
      exists j; rewrite <- Hj; assumption.
    + destruct (HBA i) as [j Hj].
      exists j; rewrite <- Hj; assumption.
  - intros HAB.
    constructor.
    + intros i.
      destruct (HAB (elem A i)) as [HAB' _].
      destruct HAB' as [j Hj]; [eexists; reflexivity|].
      exists j; symmetry; assumption.
    + intros j.
      destruct (HAB (elem B j)) as [_ HBA].
      destruct HBA as [i Hi]; [eexists; reflexivity|].
      exists i; symmetry; assumption.
Qed.

Global Instance elem_of_resp : Proper (equiv ==> equiv ==> iff) elem_of.
Proof.
  intros a b Hab A B HAB.
  split.
  - intros [i Hi].
    destruct HAB as [? ? HAB HBA].
    destruct (HAB i) as [j Hj].
    exists j; rewrite <- Hab, <- Hj; assumption.
  - intros [i Hi].
    destruct HAB as [? ? HAB HBA].
    destruct (HBA i) as [j Hj].
    exists j; rewrite Hab, <- Hj; assumption.
Qed.

Lemma elem_of_wf : well_founded elem_of.
Proof.
  intros A.
  induction A as [TA f IHf].
  constructor; intros B [i Hi]; simpl in *.
  constructor; intros b Hb.
  destruct (IHf i) as [Hfi].
  apply Hfi.
  rewrite Hi; assumption.
Qed.

Lemma set_induction (P : Ens -> Prop) :
  (forall A, (forall a, a ∈ A -> P a) -> P A) -> forall A, P A.
Proof.
  intros IH A.
  induction (elem_of_wf A) as [B HBacc HB].
  apply IH; assumption.
Qed.

Definition empty : Ens := ens_intro False (False_rect Ens).

Lemma elem_of_empty a : ~ a ∈ empty.
Proof.
  intros [? ?]; assumption.
Qed.

Definition Union {T} (f : T -> Ens) :=
  ens_intro {x : T & idx (f x)} (fun u => elem (f (projT1 u)) (projT2 u)).

Lemma elem_of_union {T} (f : T -> Ens) A : A ∈ (Union f) <-> exists t, A ∈ (f t).
Proof.
  split.
  - intros [[z idx] Hzidx]; exists z, idx; assumption.
  - intros [z [idx Hzidx]]; exists (existT _ z idx); assumption.
Qed.

Definition pairing (a b : Ens) : Ens := ens_intro bool (fun x => if x then a else b).

Lemma elem_of_pairing a b c : c ∈ (pairing a b) <-> c ≡ a \/ c ≡ b.
Proof.
  split.
  - intros [[] <-]; [left|right]; reflexivity.
  - intros [->| ->]; [exists true|exists false]; reflexivity.
Qed.

Definition subset (A B : Ens) : Prop := forall x, x ∈ A -> x ∈ B.

Definition carve_subset (A : Ens) (f : idx A -> Prop) :=
  ens_intro {i : idx A | f i} (fun x => elem A (proj1_sig x)).

Lemma elem_of_carve_subset A f a :
  a ∈ (carve_subset A f) <-> a ∈ A /\ exists j, f j /\ elem A j ≡ a.
Proof.
  split.
  - intros [[i ?] Hi]; split; [eexists i; assumption|eauto].
  - intros [[i ?] [j [Hfj <-]]]; exists (exist _ j Hfj); reflexivity.
Qed.

Lemma carve_subset_subset A P : subset (carve_subset A P) A.
Proof. intros x Hx; apply elem_of_carve_subset in Hx as []; assumption. Qed.

Definition comprehension (A : Ens) (P : Ens -> Prop) := carve_subset A (fun i => P (elem A i)).

Lemma elem_of_comprehension A (P : Ens -> Prop) x :
  (forall a b, a ≡ b -> P a -> P b) -> x ∈ (comprehension A P) <-> x ∈ A /\ P x.
Proof.
  intros HP.
  unfold comprehension.
  split.
  - intros Hx.
    apply elem_of_carve_subset in Hx as [? [? [? ?]]].
    split; [assumption|].
    eapply HP; eauto.
  - intros [HxA HPx]; apply elem_of_carve_subset; split; [assumption|].
    destruct HxA as [i ?]; exists i; split; [|assumption].
    eapply HP; [symmetry|]; eauto.
Qed.

Lemma comprehension_subset A P : subset (comprehension A P) A.
Proof. apply carve_subset_subset. Qed.

Definition power_set (A : Ens) : Ens := ens_intro (idx A -> Prop) (fun f => carve_subset A f).

Lemma elem_of_powerset (A B : Ens) : B ∈ (power_set A) <-> subset B A.
Proof.
  split.
  - intros [i Hi] x Hx. rewrite <- Hi in Hx. apply carve_subset_subset in Hx; assumption.
  - intros Hsb.
    exists (fun i => elem_of (elem A i) B).
    apply extensionality; intros x.
    split.
    + intros Hx.
      apply elem_of_carve_subset in Hx as [Hx [j [Hj1 Hj2]]].
      rewrite <- Hj2; assumption.
    + intros Hx.
      apply elem_of_carve_subset.
      split; [apply Hsb; assumption|].
      destruct (Hsb _ Hx) as [j Hj].
      exists j; split; [|assumption].
      rewrite Hj; assumption.
Qed.

(* A functional relation with domain A. *)
Class functional_relation (f : Ens -> Ens -> Prop) (A : Ens) :=
  { funrel_exist : forall a, a ∈ A -> { b | f a b}; (* Each element of A is related to something. *)
    funrel_unique : (forall a b b', f a b -> f a b' -> b ≡ b'); (* Each element is mapped to at most one element. *)
    funrel_resp :> Proper (equiv ==> equiv ==> iff) f (* The relation f respects equivalence of sets. *)
  }.

Arguments funrel_exist {_ _} _.

Definition replacement {f : Ens -> Ens -> Prop} {A : Ens} (f_func : functional_relation f A) :=
  ens_intro (idx A) (fun i => proj1_sig (funrel_exist f_func (elem A i) (elem_elem_of A i))).

Lemma elem_of_replacement f A (f_func : functional_relation f A) b :
  b ∈ replacement f_func <-> exists a, a ∈ A /\ f a b.
Proof.
  split.
  - intros [i Hi]; simpl in *.
    exists (elem A i); split; [apply elem_elem_of|].
    rewrite <- Hi.
    apply (proj2_sig (funrel_exist f_func _ _)).
  - intros [a [[i <-] Hab]].
    exists i; simpl.
    eapply funrel_unique; [|eassumption].
    apply (proj2_sig (funrel_exist f_func _ _)).
Qed.