From 73e87b6b1ded49dd9b08819b75d87f6ad2181982 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 21 Jan 2019 18:15:33 +0100
Subject: [PATCH] Make set_eq and instance direclty

---
 czf.v | 91 +++++++++++++++++++----------------------------------------
 1 file changed, 29 insertions(+), 62 deletions(-)

diff --git a/czf.v b/czf.v
index 6f13d95..f8ecd03 100644
--- a/czf.v
+++ b/czf.v
@@ -15,21 +15,21 @@ Definition branch (a : V) : ind a -> V :=
   end.
 
 (** * Equality *)
-Fixpoint set_eq (a : V) (b : V) : Prop :=
-  match (a, b) with
-      (sup A f, sup B g) =>
-      (forall (x:A), exists (y: B), (set_eq (f x) (g y)))
-      /\ (forall (y:B), exists (x: A), (set_eq (f x) (g y)))
+Instance set_eq : Equiv V :=
+  fix go a b : Prop :=
+  let _ : Equiv V := @go in
+  match a, b with
+  | sup A f, sup B g =>
+     (∀ x:A, ∃ y: B, f x ≡ g y) ∧ (∀ y:B, ∃ x: A, f x ≡ g y)
   end.
-Instance equiv_V : Equiv V := set_eq.
 
-Lemma eq1 : forall x, x ≡ x.
+Lemma eq1 : forall (x : V), x ≡ x.
 Proof.
   intros. induction x.
   split; intros; [exists x | exists y]; apply H.
 Qed.
 
-Lemma eq2 : forall x y, x ≡ y -> y ≡ x.
+Lemma eq2 : forall (x y : V), x ≡ y -> y ≡ x.
 Proof.
   intro x. induction x as [A f IHx].
   intro y. destruct y as [B g].
@@ -43,7 +43,7 @@ Proof.
     exists y0. apply (IHx y (g y0)). assumption.
 Qed.
 
-Lemma eq3 : forall x y z,  x≡y -> y≡z -> x≡z.
+Lemma eq3 : forall (x y z : V),  x≡y -> y≡z -> x≡z.
 Proof.
   intro. induction x as [A f X].
   intro. destruct y as [B g].
@@ -60,10 +60,10 @@ Proof.
     exists z. apply (X z (g y0) (h y)); assumption.
 Qed.
 
-Instance set_eq_refl : Reflexive equiv_V := eq1.
-Instance set_eq_sym : Symmetric equiv_V := eq2.
-Instance set_eq_trans : Transitive equiv_V := eq3.
-Instance set_eq_equivalence : Equivalence equiv_V.
+Instance set_eq_refl : Reflexive set_eq := eq1.
+Instance set_eq_sym : Symmetric set_eq := eq2.
+Instance set_eq_trans : Transitive set_eq := eq3.
+Instance set_eq_equivalence : Equivalence set_eq.
 Proof. split; apply _. Qed.
 
 Lemma set_eq_unfold a b :
@@ -75,56 +75,24 @@ Proof.
 Qed.
 
 (** * Membership *)
-
-Lemma test1 (a b c : V) :
-  a ≡ b →
-  b ≡ c →
-  a ≡ c.
-Proof.
-  intros ? H2.
-  rewrite <-H2.
-  apply H.
-Qed.
-
-Lemma test2 (a b c : V) :
-  equiv_V a b →
-  equiv_V b c →
-  equiv_V a c.
-Proof.
-  intros ? H2.
-  Fail rewrite <-H2.
-Abort.
-
 Instance elem_of_V : ElemOf V V := λ (a b : V),
     exists (y : ind b), a ≡ (branch b y).
 
-Instance elem_of_V_proper : Proper ((≡) ==> (≡) ==> (=)) elem_of_V.
-Proof. Admitted.
+Instance elem_of_V_proper : Proper ((≡) ==> (≡) ==> (impl)) elem_of_V.
+Proof.
+  intros a a' Ha b b' Hb.
+  intros [y Hy].
+  destruct b as [B g].
+  destruct b' as [B' g'].
+  simpl in *.
+  destruct Hb as [i1 i2].
+  destruct (i1 y) as [y' Hy'].
+  exists y'. simpl. rewrite <- Hy'.
+  rewrite <- Ha. apply Hy.
+Qed.
 
-(* Instance elem_of_V_proper : Proper ((=) ==> (≡) ==> (impl)) elem_of_V. *)
-(* Proof. *)
-(*   intros a a' Ha b b' Hb. *)
-(*   apply propositional_extensionality. split. *)
-(*   rewrite <-Ha. *)
-(*   { intros [y Hy]. *)
-(*     destruct b as [B g]. *)
-(*     destruct b' as [B' g']. *)
-(*     simpl in *. *)
-(*     destruct Hb as [i1 i2]. *)
-(*     destruct (i1 y) as [y' Hy']. *)
-(*     exists y'. simpl. unfold equiv. admit. } *)
-(*   { intros [y' Hy']. *)
-(*     destruct b as [B g]. *)
-(*     destruct b' as [B' g']. *)
-(*     simpl in *. *)
-(*     destruct Hb as [i1 i2]. *)
-(*     destruct (i2 y') as [y Hy]. *)
-(*     exists y. simpl. symmetry. *)
-(*     unfold equiv. *)
-(* admit. } *)
-(* Admitted. *)
-
-Instance Acc_elem_of_proper : Proper ((≡) ==> (impl)) (Acc elem_of_V).
+(* Here we have to use `elem_of` instead of `elem_of_V` *)
+Instance Acc_elem_of_proper : Proper ((≡) ==> (impl)) (Acc (elem_of : V -> V -> Prop)).
 Proof.
   intros a a' Ha.
   intros acc.
@@ -135,9 +103,8 @@ Proof.
   destruct Ha as [i1 i2].
   constructor. intros x' [y' Hx'].
   eapply IH. 2:{ reflexivity. }
-  (* TODO: does not work *)
-  (* rewrite Hx'. *)
-  erewrite (elem_of_V_proper x' (branch a' y')); eauto.
+  rewrite Hx'.
+  (* erewrite (elem_of_V_proper x' (branch a' y')); eauto. *)
   destruct (i2 y') as [y Hy].
   exists y. symmetry. apply Hy.
 Qed.