From 4ade6e60cc60e9306d0190556037f4e53064a27b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 8 Aug 2017 13:18:45 +0200
Subject: [PATCH] Clean up the interface.v proofs

---
 FiniteSets/implementations/interface.v | 65 ++++++++++++--------------
 1 file changed, 30 insertions(+), 35 deletions(-)

diff --git a/FiniteSets/implementations/interface.v b/FiniteSets/implementations/interface.v
index 5dd806d..54f2a8d 100644
--- a/FiniteSets/implementations/interface.v
+++ b/FiniteSets/implementations/interface.v
@@ -53,77 +53,72 @@ Section properties.
   Definition set_subset : forall A, T A -> T A -> hProp :=
     fun A X Y => (f A X) ⊆ (f A Y).
 
-  Ltac reduce := intros ; repeat (rewrite ?(f_empty _ _) ; rewrite ?(f_singleton _ _) ;
-                         rewrite ?(f_union _ _) ; rewrite ?(f_filter _ _) ;
-                         rewrite ?(f_member _ _)).
+  Ltac reduce :=
+    intros ;
+    repeat (rewrite (f_empty _ _)
+         || rewrite ?(f_singleton _ _)
+         || rewrite ?(f_union _ _)
+         || rewrite ?(f_filter _ _)
+         || rewrite ?(f_member _ _)).
 
-  Definition empty_isIn : forall (A : Type) (a : A), member a empty = False_hp.
+  Definition empty_isIn : forall (A : Type) (a : A),
+    member a empty = False_hp.
   Proof.
-    reduce.
-    reflexivity.
+    by reduce.
   Defined.
 
   Definition singleton_isIn : forall (A : Type) (a b : A),
-      member a (singleton b) = BuildhProp (Trunc (-1) (a = b)).
+    member a (singleton b) = merely (a = b).
   Proof.
-    reduce.
-    reflexivity.
+    by reduce.
   Defined.
 
   Definition union_isIn : forall (A : Type) (a : A) (X Y : T A),
-      member a (union X Y) = lor (member a X) (member a Y).
+    member a (union X Y) = lor (member a X) (member a Y).
   Proof.
-    reduce.
-    reflexivity.
+    by reduce.
   Defined.
 
   Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A),
-      member a (filter ϕ X) = if ϕ a then member a X else False_hp.
+    member a (filter ϕ X) = if ϕ a then member a X else False_hp.
   Proof.
     reduce.
     apply properties.comprehension_isIn.
   Defined.
 
   Definition reflect_eq : forall (A : Type) (X Y : T A),
-      f A X = f A Y -> set_eq A X Y.
-  Proof.
-    auto.
-  Defined.
+    f A X = f A Y -> set_eq A X Y.
+  Proof. done. Defined.
 
   Definition reflect_subset : forall (A : Type) (X Y : T A),
-      subset (f A X) (f A Y) -> set_subset A X Y.
-  Proof.
-    auto.
-  Defined.
+    subset (f A X) (f A Y) -> set_subset A X Y.
+  Proof. done. Defined.
 
   Hint Unfold set_eq set_subset.
 
   Ltac simplify := intros ; autounfold in * ; apply reflect_eq ; reduce.
 
   Definition well_defined_union : forall (A : Type) (X1 X2 Y1 Y2 : T A),
-      set_eq A X1 Y1 -> set_eq A X2 Y2 -> set_eq A (union X1 X2) (union Y1 Y2).
+    set_eq A X1 Y1 -> set_eq A X2 Y2 -> set_eq A (union X1 X2) (union Y1 Y2).
   Proof.
+    intros A X1 X2 Y1 Y2 HXY1 HXY2.
     simplify.
-    rewrite X, X0.
-    reflexivity.
+    by rewrite HXY1, HXY2.
   Defined.
 
   Definition well_defined_filter : forall (A : Type) (ϕ : A -> Bool) (X Y : T A),
-      set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
-  Proof.
+    set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
+  Proof.    
+    intros A ϕ X Y HXY.
     simplify.
-    rewrite X0.
-    reflexivity.
+    by rewrite HXY.
   Defined.
   
-  Variable (A : Type).
-  Context `{DecidablePaths A}.
-  
-  Lemma union_comm : forall (X Y : T A),
-      set_eq A (union X Y) (union Y X).
+  Lemma union_comm : forall A (X Y : T A),
+    set_eq A (union X Y) (union Y X).
   Proof.
     simplify.
-    apply lattice_fset.
+    apply comm.
   Defined.
 
-End properties.
\ No newline at end of file
+End properties.