feat(library): minor cleanup, replace 'refl _' with 'rfl', define equivalence relation for sets

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/data/bool.lean

@@ -25,10 +25,10 @@ theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
 cases_on b (or_inl (refl ff)) (or_inr (refl tt))
 
 theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
-refl (cond ff t e)
+rfl
 
 theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
-refl (cond tt t e)
+rfl
 
 theorem ff_ne_tt : ¬ ff = tt :=
 assume H : ff = tt, absurd
@@ -47,7 +47,7 @@ definition bor (a b : bool) :=
 bool_rec (bool_rec ff tt b) tt a
 
 theorem bor_tt_left (a : bool) : bor tt a = tt :=
-refl (bor tt a)
+rfl
 
 infixl `||` := bor
 
@@ -90,7 +90,7 @@ bool_rec ff (bool_rec ff tt b) a
 infixl `&&` := band
 
 theorem band_ff_left (a : bool) : ff && a = ff :=
-refl (ff && a)
+rfl
 
 theorem band_tt_left (a : bool) : tt && a = a :=
 cases_on a (refl (tt && ff)) (refl (tt && tt))
@@ -137,8 +137,10 @@ notation `!` x:max := bnot x
 theorem bnot_bnot (a : bool) : !!a = a :=
 cases_on a (refl (!!ff)) (refl (!!tt))
 
-theorem bnot_false : !ff = tt := refl _
+theorem bnot_false : !ff = tt :=
+rfl
 
-theorem bnot_true  : !tt = ff := refl _
+theorem bnot_true  : !tt = ff :=
+rfl
 
 end bool

library/data/option.lean

@@ -42,11 +42,11 @@ inhabited_mk none
 theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)}
     (o₁ o₂ : option A) : decidable (o₁ = o₂) :=
 rec_on o₁
-  (rec_on o₂ (inl (refl _)) (take a₂, (inr (none_ne_some a₂))))
+  (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
   (take a₁ : A, rec_on o₂
     (inr (ne_symm (none_ne_some a₁)))
     (take a₂ : A, decidable.rec_on (H a₁ a₂)
-      (assume Heq : a₁ = a₂, inl (Heq ▸ refl _))
+      (assume Heq : a₁ = a₂, inl (Heq ▸ rfl))
       (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne))))
 
 end option

library/data/prod.lean

@@ -28,8 +28,11 @@ section
   abbreviation pr1 (p : prod A B) := prod_rec (λ x y, x) p
   abbreviation pr2 (p : prod A B) := prod_rec (λ x y, y) p
 
-  theorem pr1_pair (a : A) (b : B) : pr1 (a, b) = a := refl a
-  theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b := refl b
+  theorem pr1_pair (a : A) (b : B) : pr1 (a, b) = a :=
+  rfl
+
+  theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b :=
+  rfl
 
   -- TODO: remove prefix when we can protect it
   theorem pair_destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
@@ -39,25 +42,22 @@ section
   pair_destruct p (λx y, refl (x, y))
 
   theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
-  subst H1 (subst H2 (refl _))
+  subst H1 (subst H2 rfl)
 
   theorem prod_eq {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
   pair_destruct p1 (take a1 b1, pair_destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
 
-  theorem prod_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
+  theorem prod_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b)))
 
-  theorem prod_eq_decidable (u v : A × B) (H1 : decidable (pr1 u = pr1 v))
+  theorem prod_eq_decidable [instance] (u v : A × B) (H1 : decidable (pr1 u = pr1 v))
       (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) :=
     have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
       iff_intro
-        (assume H, subst H (and_intro (refl _) (refl _)))
+        (assume H, subst H (and_intro rfl rfl))
         (assume H, and_elim H (assume H4 H5, prod_eq H4 H5)),
     decidable_iff_equiv _ (iff_symm H3)
 
 end
 
-instance prod_inhabited
-instance prod_eq_decidable
-
 end prod

library/data/set.lean

@@ -3,32 +3,47 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad, Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
-
-import logic.axioms.funext data.bool
+import data.bool
 using eq_ops bool
 
 namespace set
-definition set (T : Type) := T → bool
-definition mem {T : Type} (x : T) (s : set T) := (s x) = tt
+definition set (T : Type) :=
+T → bool
+definition mem {T : Type} (x : T) (s : set T) :=
+(s x) = tt
 infix `∈` := mem
 
-section
-parameter {T : Type}
+definition eqv {T : Type} (A B : set T) : Prop :=
+∀x, x ∈ A ↔ x ∈ B
+infixl `∼`:50 := eqv
 
-definition empty : set T := λx, ff
+theorem eqv_refl {T : Type} (A : set T) : A ∼ A :=
+take x, iff_rfl
+
+theorem eqv_symm {T : Type} {A B : set T} (H : A ∼ B) : B ∼ A :=
+take x, iff_symm (H x)
+
+theorem eqv_trans {T : Type} {A B C : set T} (H1 : A ∼ B) (H2 : B ∼ C) : A ∼ C :=
+take x, iff_trans (H1 x) (H2 x)
+
+definition empty {T : Type} : set T :=
+λx, ff
 notation `∅` := empty
 
-theorem mem_empty (x : T) : ¬ (x ∈ ∅) :=
+theorem mem_empty {T : Type} (x : T) : ¬ (x ∈ ∅) :=
 assume H : x ∈ ∅, absurd H ff_ne_tt
 
-definition univ : set T := λx, tt
+definition univ {T : Type} : set T :=
+λx, tt
 
-theorem mem_univ (x : T) : x ∈ univ := refl _
+theorem mem_univ {T : Type} (x : T) : x ∈ univ :=
+rfl
 
-definition inter (A B : set T) : set T := λx, A x && B x
+definition inter {T : Type} (A B : set T) : set T :=
+λx, A x && B x
 infixl `∩` := inter
 
-theorem mem_inter (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) :=
+theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) :=
 iff_intro
   (assume H, and_intro (band_eq_tt_elim_left H) (band_eq_tt_elim_right H))
   (assume H,
@@ -36,16 +51,26 @@ iff_intro
     have e2 : B x = tt, from and_elim_right H,
     show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ band_tt_left tt)
 
-theorem inter_comm (A B : set T) : A ∩ B = B ∩ A :=
-funext (λx, band_comm (A x) (B x))
+theorem inter_id {T : Type} (A : set T) : A ∩ A ∼ A :=
+take x, band_id (A x) ▸ iff_rfl
 
-theorem inter_assoc (A B C : set T) : (A ∩ B) ∩ C = A ∩ (B ∩ C) :=
-funext (λx, band_assoc (A x) (B x) (C x))
+theorem inter_empty_right {T : Type} (A : set T) : A ∩ ∅ ∼ ∅ :=
+take x, band_ff_right (A x) ▸ iff_rfl
 
-definition union (A B : set T) : set T := λx, A x || B x
+theorem inter_empty_left {T : Type} (A : set T) : ∅ ∩ A ∼ ∅ :=
+take x, band_ff_left (A x) ▸ iff_rfl
+
+theorem inter_comm {T : Type} (A B : set T) : A ∩ B ∼ B ∩ A :=
+take x, band_comm (A x) (B x) ▸ iff_rfl
+
+theorem inter_assoc {T : Type} (A B C : set T) : (A ∩ B) ∩ C ∼ A ∩ (B ∩ C) :=
+take x, band_assoc (A x) (B x) (C x) ▸ iff_rfl
+
+definition union {T : Type} (A B : set T) : set T :=
+λx, A x || B x
 infixl `∪` := union
 
-theorem mem_union (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) :=
+theorem mem_union {T : Type} (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) :=
 iff_intro
   (assume H, bor_to_or H)
   (assume H, or_elim H
@@ -54,12 +79,19 @@ iff_intro
     (assume Hb : B x = tt,
       show A x || B x = tt, from Hb⁻¹ ▸ bor_tt_right (A x)))
 
-theorem union_comm (A B : set T) : A ∪ B = B ∪ A :=
-funext (λx, bor_comm (A x) (B x))
+theorem union_id {T : Type} (A : set T) : A ∪ A ∼ A :=
+take x, bor_id (A x) ▸ iff_rfl
 
-theorem union_assoc (A B C : set T) : (A ∪ B) ∪ C = A ∪ (B ∪ C) :=
-funext (λx, bor_assoc (A x) (B x) (C x))
+theorem union_empty_right {T : Type} (A : set T) : A ∪ ∅ ∼ A :=
+take x, bor_ff_right (A x) ▸ iff_rfl
 
-end
+theorem union_empty_left {T : Type} (A : set T) : ∅ ∪ A ∼ A :=
+take x, bor_ff_left (A x) ▸ iff_rfl
+
+theorem union_comm {T : Type} (A B : set T) : A ∪ B ∼ B ∪ A :=
+take x, bor_comm (A x) (B x) ▸ iff_rfl
+
+theorem union_assoc {T : Type} (A B C : set T) : (A ∪ B) ∪ C ∼ A ∪ (B ∪ C) :=
+take x, bor_assoc (A x) (B x) (C x) ▸ iff_rfl
 
 end set

library/logic/connectives/basic.lean

@@ -169,6 +169,9 @@ iff_intro
 theorem iff_refl (a : Prop) : a ↔ a :=
 iff_intro (assume H, H) (assume H, H)
 
+theorem iff_rfl {a : Prop} : a ↔ a :=
+iff_refl a
+
 theorem iff_trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c :=
 iff_intro
   (assume Ha, iff_elim_left H2 (iff_elim_left H1 Ha))