From 2b5a1fd4f37230eb967561c327ab1b0de82050ad Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 21 Jan 2019 18:47:18 +0100
Subject: [PATCH] Subset relation and extensionality

---
 czf.v | 72 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)

diff --git a/czf.v b/czf.v
index f8ecd03..3eb2e4a 100644
--- a/czf.v
+++ b/czf.v
@@ -74,6 +74,9 @@ Proof.
   destruct a, b; reflexivity.
 Qed.
 
+Instance sup_proper A : Proper (((=) ==> (≡)) ==> (≡)) (sup A).
+Proof. intros f f' Hf. split; eauto. Qed.
+
 (** * Membership *)
 Instance elem_of_V : ElemOf V V := λ (a b : V),
     exists (y : ind b), a ≡ (branch b y).
@@ -120,7 +123,76 @@ Proof.
 Qed.
 
 (** * Set formers *)
+
+(** *** Empty set *)
 Instance empty_V : Empty V :=
   sup Empty_set (Empty_set_rect _).
 
+(** *** Singleton *)
+Instance singleton_V : Singleton V V := λ x,
+  sup unit (λ _, x).
 
+Instance singleton_proper : Proper ((≡) ==> (≡)) (singleton : V → V).
+Proof.
+  intros x x' Hx.
+  unfold singleton, singleton_V. f_equiv.
+  intros ??. eauto.
+Qed.
+
+(** *** Union *)
+Instance union_V : Union V := λ a b,
+    match (a, b) with
+    | (sup A f, sup B g) =>
+      sup (A + B) (λ x, match x with
+                        | inl a => f a
+                        | inr b => g b
+                        end)
+    end.
+
+Instance union_proper : Proper ((≡) ==> (≡) ==> (≡)) (union : V → V → V).
+Proof.
+  intros [A f] [A' f'] [i1 i2] [B g] [B' g'] [j1 j2].
+  cbn. split.
+  - intros [a|b].
+    + destruct (i1 a) as [a' Ha].
+      exists (inl a'). assumption.
+    + destruct (j1 b) as [b' Hb].
+      exists (inr b'). assumption.
+  - intros [a|b].
+    + destruct (i2 a) as [a' Ha].
+      exists (inl a'). assumption.
+    + destruct (j2 b) as [b' Hb].
+      exists (inr b'). assumption.
+Qed.
+
+(** *** Natural numbers *)
+Fixpoint delta (n:nat) : V :=
+  match n with
+    | O => ∅
+    | S x => (delta x) ∪ {[ delta x ]}
+  end.
+Definition NN : V := sup nat delta.
+
+(** * Extensionality *)
+Instance subseteq_V : SubsetEq V := λ a b,
+  forall x, x ∈ a → x ∈ b.
+
+Instance subseteq_proper : Proper ((≡) ==> (≡) ==> impl) (subseteq : relation V).
+Proof.
+  intros a a' Ha b b' Hb.
+  unfold subseteq, subseteq_V. intros Hs x.
+  rewrite <- Ha. rewrite <- Hb. apply Hs.
+Qed.
+
+Lemma V_ext (a b : V) :
+  a ⊆ b → b ⊆ a → a ≡ b.
+Proof.
+  destruct a as [A f]. destruct b as [B g].
+  intros HAB HBA. split.
+  - intros x. apply HAB.
+    exists x. reflexivity.
+  - intros y.
+    assert (g y ∈ sup B g) as Hgy. { exists y. reflexivity. }
+    destruct (HBA (g y) Hgy) as [x Hx].
+    exists x. symmetry. apply Hx.
+Qed.