diff --git a/library/data/equiv.lean b/library/data/equiv.lean
index 586934352..2ba065902 100644
--- a/library/data/equiv.lean
+++ b/library/data/equiv.lean
@@ -40,7 +40,7 @@ protected theorem trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A ≃ C
 lemma false_equiv_empty : empty ≃ false :=
 mk (λ e, empty.rec _ e) (λ h, false.rec _ h) (λ e, empty.rec _ e) (λ h, false.rec _ h)
 
-lemma arrow_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
+lemma arrow_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
 | (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
   mk
    (λ (h : A₁ → B₁) (a : A₂), f₂ (h (g₁ a)))
@@ -70,7 +70,7 @@ calc (false → A) ≃ (empty → A) : arrow_congr false_equiv_empty !equiv.refl
              ... ≃ unit        : empty_arrow_equiv_unit
 end
 
-lemma prod_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ × B₁) ≃ (A₂ × B₂)
+lemma prod_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ × B₁) ≃ (A₂ × B₂)
 | (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
   mk
     (λ p, match p with (a₁, b₁) := (f₁ a₁, f₂ b₁) end)
@@ -112,7 +112,7 @@ end
 
 section
 open sum
-lemma sum_congr {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ + B₁) ≃ (A₂ + B₂)
+lemma sum_congr [congr] {A₁ B₁ A₂ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ + B₁) ≃ (A₂ + B₂)
 | (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
   mk
    (λ s, match s with inl a₁ := inl (f₁ a₁) | inr b₁ := inr (f₂ b₁) end)
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index dcc7421f2..7b3a15476 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -25,7 +25,7 @@ lemma map_append (f : A → B) : ∀ l₁ l₂, map f (l₁++l₂) = (map f l₁
 
 lemma map_singleton (f : A → B) (a : A) : map f [a] = [f a] := rfl
 
-theorem map_id : ∀ l : list A, map id l = l
+theorem map_id [simp] : ∀ l : list A, map id l = l
 | []      := rfl
 | (x::xs) := begin rewrite [map_cons, map_id] end
 
@@ -33,13 +33,13 @@ theorem map_id' {f : A → A} (H : ∀x, f x = x) : ∀ l : list A, map f l = l
 | []      := rfl
 | (x::xs) := begin rewrite [map_cons, H, map_id'] end
 
-theorem map_map (g : B → C) (f : A → B) : ∀ l, map g (map f l) = map (g ∘ f) l
+theorem map_map [simp] (g : B → C) (f : A → B) : ∀ l, map g (map f l) = map (g ∘ f) l
 | []       := rfl
 | (a :: l) :=
   show (g ∘ f) a :: map g (map f l) = map (g ∘ f) (a :: l),
   by rewrite (map_map l)
 
-theorem length_map (f : A → B) : ∀ l : list A, length (map f l) = length l
+theorem length_map [simp] (f : A → B) : ∀ l : list A, length (map f l) = length l
 | []       := by esimp
 | (a :: l) :=
   show length (map f l) + 1 = length l + 1,
@@ -78,12 +78,12 @@ definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
 | []     := []
 | (a::l) := if p a then a :: filter l else filter l
 
-theorem filter_nil (p : A → Prop) [h : decidable_pred p] : filter p [] = []
+theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = []
 
-theorem filter_cons_of_pos {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, p a → filter p (a::l) = a :: filter p l :=
+theorem filter_cons_of_pos [simp] {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, p a → filter p (a::l) = a :: filter p l :=
 λ l pa, if_pos pa
 
-theorem filter_cons_of_neg {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, ¬ p a → filter p (a::l) = filter p l :=
+theorem filter_cons_of_neg [simp] {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, ¬ p a → filter p (a::l) = filter p l :=
 λ l pa, if_neg pa
 
 theorem of_mem_filter {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ {l}, a ∈ filter p l → p a
@@ -116,7 +116,7 @@ theorem mem_filter_of_mem {p : A → Prop} [h : decidable_pred p] {a : A} : ∀
     (λ aeqb : a = b, absurd (eq.rec_on aeqb pa) npb)
     (λ ainl : a ∈ l, by rewrite [filter_cons_of_neg _ npb]; exact (mem_filter_of_mem ainl pa)))
 
-theorem filter_sub {p : A → Prop} [h : decidable_pred p] (l : list A) : filter p l ⊆ l :=
+theorem filter_sub [simp] {p : A → Prop} [h : decidable_pred p] (l : list A) : filter p l ⊆ l :=
 λ a ain, mem_of_mem_filter ain
 
 theorem filter_append {p : A → Prop} [h : decidable_pred p] : ∀ (l₁ l₂ : list A), filter p (l₁++l₂) = filter p l₁ ++ filter p l₂
@@ -130,17 +130,17 @@ definition foldl (f : A → B → A) : A → list B → A
 | a []       := a
 | a (b :: l) := foldl (f a b) l
 
-theorem foldl_nil (f : A → B → A) (a : A) : foldl f a [] = a
+theorem foldl_nil [simp] (f : A → B → A) (a : A) : foldl f a [] = a
 
-theorem foldl_cons (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l
+theorem foldl_cons [simp] (f : A → B → A) (a : A) (b : B) (l : list B) : foldl f a (b::l) = foldl f (f a b) l
 
 definition foldr (f : A → B → B) : B → list A → B
 | b []       := b
 | b (a :: l) := f a (foldr b l)
 
-theorem foldr_nil (f : A → B → B) (b : B) : foldr f b [] = b
+theorem foldr_nil [simp] (f : A → B → B) (b : B) : foldr f b [] = b
 
-theorem foldr_cons (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l)
+theorem foldr_cons [simp] (f : A → B → B) (b : B) (a : A) (l : list A) : foldr f b (a::l) = f a (foldr f b l)
 
 section foldl_eq_foldr
   -- foldl and foldr coincide when f is commutative and associative
@@ -171,11 +171,11 @@ section foldl_eq_foldr
     end
 end foldl_eq_foldr
 
-theorem foldl_append (f : B → A → B) : ∀ (b : B) (l₁ l₂ : list A), foldl f b (l₁++l₂) = foldl f (foldl f b l₁) l₂
+theorem foldl_append [simp] (f : B → A → B) : ∀ (b : B) (l₁ l₂ : list A), foldl f b (l₁++l₂) = foldl f (foldl f b l₁) l₂
 | b []      l₂ := rfl
 | b (a::l₁) l₂ := by rewrite [append_cons, *foldl_cons, foldl_append]
 
-theorem foldr_append (f : A → B → B) : ∀ (b : B) (l₁ l₂ : list A), foldr f b (l₁++l₂) = foldr f (foldr f b l₂) l₁
+theorem foldr_append [simp] (f : A → B → B) : ∀ (b : B) (l₁ l₂ : list A), foldr f b (l₁++l₂) = foldr f (foldr f b l₂) l₁
 | b []      l₂ := rfl
 | b (a::l₁) l₂ := by rewrite [append_cons, *foldr_cons, foldr_append]
 
@@ -186,7 +186,7 @@ foldr (λ a r, p a ∧ r) true l
 definition any (l : list A) (p : A → Prop) : Prop :=
 foldr (λ a r, p a ∨ r) false l
 
-theorem all_nil_eq (p : A → Prop) : all [] p = true
+theorem all_nil_eq [simp] (p : A → Prop) : all [] p = true
 
 theorem all_nil (p : A → Prop) : all [] p := trivial
 
@@ -226,9 +226,9 @@ theorem all_of_forall {p : A → Prop} : ∀ {l}, (∀a, a ∈ l → p a) → al
 | (a::l) H := all_cons (H a !mem_cons)
                        (all_of_forall (λ a' H', H a' (mem_cons_of_mem _ H')))
 
-theorem any_nil (p : A → Prop) : any [] p = false
+theorem any_nil [simp] (p : A → Prop) : any [] p = false
 
-theorem any_cons (p : A → Prop) (a : A) (l : list A) : any (a::l) p = (p a ∨ any l p)
+theorem any_cons [simp] (p : A → Prop) (a : A) (l : list A) : any (a::l) p = (p a ∨ any l p)
 
 theorem any_of_mem {p : A → Prop} {a : A} : ∀ {l}, a ∈ l → p a → any l p
 | []     i h := absurd i !not_mem_nil
@@ -282,9 +282,9 @@ definition unzip : list (A × B) → list A × list B
   | (la, lb) := (a :: la, b :: lb)
   end
 
-theorem unzip_nil : unzip (@nil (A × B)) = ([], [])
+theorem unzip_nil [simp] : unzip (@nil (A × B)) = ([], [])
 
-theorem unzip_cons (a : A) (b : B) (l : list (A × B)) :
+theorem unzip_cons [simp] (a : A) (b : B) (l : list (A × B)) :
    unzip ((a, b) :: l) = match unzip l with (la, lb) := (a :: la, b :: lb) end :=
 rfl
 
diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean
index 49910a2d4..c823f1b8d 100644
--- a/library/data/list/perm.lean
+++ b/library/data/list/perm.lean
@@ -88,7 +88,7 @@ list.induction_on l
   (λ p, p)
   (λ x xs r p, skip x (r p))
 
-theorem perm_app {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (l₁++t₁) ~ (l₂++t₂) :=
+theorem perm_app [congr] {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (l₁++t₁) ~ (l₂++t₂) :=
 assume p₁ p₂, trans (perm_app_left t₁ p₁) (perm_app_right l₂ p₂)
 
 theorem perm_app_cons (a : A) {h₁ h₂ t₁ t₂ : list A} : h₁ ~ h₂ → t₁ ~ t₂ → (h₁ ++ (a::t₁)) ~ (h₂ ++ (a::t₂)) :=
@@ -100,7 +100,10 @@ theorem perm_cons_app (a : A) : ∀ (l : list A), (a::l) ~ (l ++ [a])
   a::x::xs ~ x::a::xs     : swap x a xs
        ... ~ x::(xs++[a]) : skip x (perm_cons_app xs)
 
-theorem perm_app_comm {l₁ l₂ : list A} : (l₁++l₂) ~ (l₂++l₁) :=
+theorem perm_cons_app_simp [simp] (a : A) : ∀ (l : list A), (l ++ [a]) ~ (a::l) :=
+take l, perm.symm !perm_cons_app
+
+theorem perm_app_comm [simp] {l₁ l₂ : list A} : (l₁++l₂) ~ (l₂++l₁) :=
 list.induction_on l₁
   (by rewrite [append_nil_right, append_nil_left])
   (λ a t r, calc
@@ -145,6 +148,9 @@ theorem perm_rev : ∀ (l : list A), l ~ (reverse l)
     ... ~ reverse xs ++ [x] : perm_app_left [x] (perm_rev xs)
     ... = reverse (x::xs)   : by rewrite [reverse_cons, concat_eq_append]
 
+theorem perm_rev_simp [simp] : ∀ (l : list A), (reverse l) ~ l :=
+take l, perm.symm (perm_rev l)
+
 theorem perm_middle (a : A) (l₁ l₂ : list A) : (a::l₁)++l₂ ~ l₁++(a::l₂) :=
 calc
   (a::l₁) ++ l₂ = a::(l₁++l₂)   : rfl
@@ -152,6 +158,9 @@ calc
            ...  = l₁++(l₂++[a]) : append.assoc
            ...  ~ l₁++(a::l₂)   : perm_app_right l₁ (perm.symm (perm_cons_app a l₂))
 
+theorem perm_middle_simp [simp] (a : A) (l₁ l₂ : list A) : l₁++(a::l₂) ~ (a::l₁)++l₂ :=
+perm.symm !perm_middle
+
 theorem perm_cons_app_cons {l l₁ l₂ : list A} (a : A) : l ~ l₁++l₂ → a::l ~ l₁++(a::l₂) :=
 assume p, calc
   a::l ~ l++[a]        : perm_cons_app
@@ -172,7 +181,7 @@ theorem perm_erase [H : decidable_eq A] {a : A} : ∀ {l : list A}, a ∈ l →
             ... ~ a::x::(erase a t)   : swap
             ... = a::(erase a (x::t)) : by rewrite [!erase_cons_tail naeqx])
 
-theorem erase_perm_erase_of_perm [H : decidable_eq A] (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → erase a l₁ ~ erase a l₂ :=
+theorem erase_perm_erase_of_perm [congr] [H : decidable_eq A] (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → erase a l₁ ~ erase a l₂ :=
 assume p, perm.induction_on p
   nil
   (λ x t₁ t₂ p r,
@@ -208,7 +217,7 @@ assume p, calc
   x::y::l₁  ~  y::x::l₁  : swap
         ... ~  y::x::l₂  : skip y (skip x p)
 
-theorem perm_map (f : A → B) {l₁ l₂ : list A} : l₁ ~ l₂ → map f l₁ ~ map f l₂ :=
+theorem perm_map [congr] (f : A → B) {l₁ l₂ : list A} : l₁ ~ l₂ → map f l₁ ~ map f l₂ :=
 assume p, perm_induction_on p
   nil
   (λ x l₁ l₂ p r, skip (f x) r)
@@ -492,7 +501,7 @@ section foldr
   variable lcomm : left_commutative f
   include  lcomm
 
-  theorem foldr_eq_of_perm : l₁ ~ l₂ → ∀ b, foldr f b l₁ = foldr f b l₂ :=
+  theorem foldr_eq_of_perm [congr] : l₁ ~ l₂ → ∀ b, foldr f b l₁ = foldr f b l₂ :=
   assume p, perm_induction_on p
     (λ b, by rewrite *foldl_nil)
     (λ x t₁ t₂ p r b, calc
@@ -507,7 +516,7 @@ section foldr
     (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ a, eq.trans (r₁ a) (r₂ a))
 end foldr
 
-theorem perm_erase_dup_of_perm [H : decidable_eq A] {l₁ l₂ : list A} : l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
+theorem perm_erase_dup_of_perm [congr] [H : decidable_eq A] {l₁ l₂ : list A} : l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
 assume p, perm_induction_on p
   nil
   (λ x t₁ t₂ p r, by_cases
@@ -621,7 +630,7 @@ list.induction_on l
       assert nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
       by rewrite [union_cons_of_not_mem _ nxint₁, union_cons_of_not_mem _ nxint₂]; exact (skip _ (r p))))
 
-theorem perm_union {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (union l₁ t₁) ~ (union l₂ t₂) :=
+theorem perm_union [congr] {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (union l₁ t₁) ~ (union l₂ t₂) :=
 assume p₁ p₂, trans (perm_union_left t₁ p₁) (perm_union_right l₂ p₂)
 end perm_union
 
@@ -629,7 +638,7 @@ section perm_insert
 variable [H : decidable_eq A]
 include H
 
-theorem perm_insert (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → (insert a l₁) ~ (insert a l₂) :=
+theorem perm_insert [congr] (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → (insert a l₁) ~ (insert a l₂) :=
 assume p, by_cases
  (λ ainl₁  : a ∈ l₁,
    assert ainl₂ : a ∈ l₂, from mem_perm p ainl₁,
@@ -675,7 +684,7 @@ list.induction_on l
       assert nxint₂ : x ∉ t₂, from not_mem_perm p nxint₁,
       by rewrite [inter_cons_of_not_mem _ nxint₁, inter_cons_of_not_mem _ nxint₂]; exact (r p)))
 
-theorem perm_inter {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (inter l₁ t₁) ~ (inter l₂ t₂) :=
+theorem perm_inter [congr] {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (inter l₁ t₁) ~ (inter l₂ t₂) :=
 assume p₁ p₂, trans (perm_inter_left t₁ p₁) (perm_inter_right l₂ p₂)
 end perm_inter
 
@@ -751,12 +760,12 @@ list.induction_on l
   (λ a t r p,
     perm_app (perm_map _ p) (r p))
 
-theorem perm_product {l₁ l₂ : list A} {t₁ t₂ : list B} : l₁ ~ l₂ → t₁ ~ t₂ → (product l₁ t₁) ~ (product l₂ t₂) :=
+theorem perm_product [congr] {l₁ l₂ : list A} {t₁ t₂ : list B} : l₁ ~ l₂ → t₁ ~ t₂ → (product l₁ t₁) ~ (product l₂ t₂) :=
 assume p₁ p₂, trans (perm_product_left t₁ p₁) (perm_product_right l₂ p₂)
 end product
 
 /- filter -/
-theorem perm_filter {l₁ l₂ : list A} {p : A → Prop} [decp : decidable_pred p] :
+theorem perm_filter [congr] {l₁ l₂ : list A} {p : A → Prop} [decp : decidable_pred p] :
   l₁ ~ l₂ → (filter p l₁) ~ (filter p l₂) :=
 assume u, perm.induction_on u
   perm.nil
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 9cad30380..3a9851636 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -569,15 +569,15 @@ theorem if_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidabl
         (if b then x else y) = (if c then u else v) :=
 @if_ctx_congr A b c dec_b dec_c x y u v h_c (λ h, h_t) (λ h, h_e)
 
-theorem if_ctx_rw_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A}
+theorem if_ctx_simp_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A}
                         (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) :
         (if b then x else y) = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
 @if_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x y u v h_c h_t h_e
 
-theorem if_rw_congr {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A}
+theorem if_simp_congr [congr] {A : Type} {b c : Prop} [dec_b : decidable b] {x y u v : A}
                  (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
         (if b then x else y) = (@ite c (decidable_of_decidable_of_iff dec_b h_c) A u v) :=
-@if_ctx_rw_congr A b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
+@if_ctx_simp_congr A b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
 
 theorem if_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
                       (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) :
@@ -594,11 +594,16 @@ decidable.rec_on dec_b
       ...  ↔ v                    : h_e (iff.mp (not_iff_not_of_iff h_c) hn)
       ...  ↔ (if c then u else v) : iff.of_eq (if_neg (iff.mp (not_iff_not_of_iff h_c) hn)))
 
-theorem if_rw_congr_prop {b c x y u v : Prop} [dec_b : decidable b]
-                         (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) :
+theorem if_ctx_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b]
+                               (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) :
         if b then x else y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) :=
 @if_congr_prop b c x y u v dec_b (decidable_of_decidable_of_iff dec_b h_c) h_c h_t h_e
 
+theorem if_simp_congr_prop [congr] {b c x y u v : Prop} [dec_b : decidable b]
+                           (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) :
+        if b then x else y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Prop u v) :=
+@if_ctx_simp_congr_prop b c x y u v dec_b h_c (λ h, h_t) (λ h, h_e)
+
 -- We use "dependent" if-then-else to be able to communicate the if-then-else condition
 -- to the branches
 definition dite (c : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
@@ -638,7 +643,7 @@ decidable.rec_on dec_b
       ...  = v (iff.mp h_nc hn)                : h_e
       ...  = (if h : c then u h else v h)      : dif_neg (iff.mp h_nc hn))
 
-theorem dif_ctx_rw_congr {A : Type} {b c : Prop} [dec_b : decidable b]
+theorem dif_ctx_simp_congr {A : Type} {b c : Prop} [dec_b : decidable b]
                          {x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A}
                          (h_c : b ↔ c)
                          (h_t : ∀ (h : c),    x (iff.mpr h_c h)                      = u h)
@@ -669,3 +674,10 @@ decidable.rec_on H₁ (λ Hc, !false.rec (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
 
 theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c :=
 decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, absurd true.intro (if_neg Hnc ▸ H₂))
+
+-- namespace used to collect congruence rules for "contextual simplification"
+namespace contextual
+  attribute if_ctx_simp_congr      [congr]
+  attribute if_ctx_simp_congr_prop [congr]
+  attribute dif_ctx_simp_congr     [congr]
+end contextual
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index 4c5a35beb..7bf7fceb0 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -93,10 +93,10 @@ and.elim H₁ (assume Ha : a, assume Hc : c, and.intro (H Ha) Hc)
 theorem and_of_and_of_imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b :=
 and.elim H₁ (assume Hc : c, assume Ha : a, and.intro Hc (H Ha))
 
-theorem and.comm : a ∧ b ↔ b ∧ a :=
+theorem and.comm [simp] : a ∧ b ↔ b ∧ a :=
 iff.intro (λH, and.swap H) (λH, and.swap H)
 
-theorem and.assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
+theorem and.assoc [simp] : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
 iff.intro
   (assume H,
    obtain [Ha Hb] Hc, from H,
@@ -174,10 +174,10 @@ or.elim H₁ (assume Ha, Ha) (assume Hb, absurd Hb H₂)
 theorem or.swap (H : a ∨ b) : b ∨ a :=
 or.elim H (assume Ha, or.inr Ha) (assume Hb, or.inl Hb)
 
-theorem or.comm : a ∨ b ↔ b ∨ a :=
+theorem or.comm [simp] : a ∨ b ↔ b ∨ a :=
 iff.intro (λH, or.swap H) (λH, or.swap H)
 
-theorem or.assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
+theorem or.assoc [simp] : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
 iff.intro
   (assume H, or.elim H
     (assume H₁, or.elim H₁
@@ -309,23 +309,15 @@ section
   variables {a₁ b₁ a₂ b₂ : Prop}
   variables (H₁ : a₁ ↔ b₁) (H₂ : a₂ ↔ b₂)
 
-  theorem congr_and : a₁ ∧ a₂ ↔ b₁ ∧ b₂ :=
-  iff.intro
-    (assume H₃ : a₁ ∧ a₂, and_of_and_of_imp_of_imp H₃ (iff.elim_left H₁) (iff.elim_left H₂))
-    (assume H₃ : b₁ ∧ b₂, and_of_and_of_imp_of_imp H₃ (iff.elim_right H₁) (iff.elim_right H₂))
+  theorem congr_and [congr] : a₁ ∧ a₂ ↔ b₁ ∧ b₂ :=
+  and_iff_and H₁ H₂
 
-  theorem congr_or : a₁ ∨ a₂ ↔ b₁ ∨ b₂ :=
-  iff.intro
-    (assume H₃ : a₁ ∨ a₂, or_of_or_of_imp_of_imp H₃ (iff.elim_left H₁) (iff.elim_left H₂))
-    (assume H₃ : b₁ ∨ b₂, or_of_or_of_imp_of_imp H₃ (iff.elim_right H₁) (iff.elim_right H₂))
+  theorem congr_or [congr] : a₁ ∨ a₂ ↔ b₁ ∨ b₂ :=
+  or_iff_or H₁ H₂
 
-  theorem congr_imp : (a₁ → a₂) ↔ (b₁ → b₂) :=
-  iff.intro
-    (assume H₃ : a₁ → a₂, assume Hb₁ : b₁, iff.elim_left H₂ (H₃ ((iff.elim_right H₁) Hb₁)))
-    (assume H₃ : b₁ → b₂, assume Ha₁ : a₁, iff.elim_right H₂ (H₃ ((iff.elim_left H₁) Ha₁)))
+  theorem congr_imp [congr] : (a₁ → a₂) ↔ (b₁ → b₂) :=
+  imp_iff_imp H₁ H₂
 
-  theorem congr_iff : (a₁ ↔ a₂) ↔ (b₁ ↔ b₂) :=
-  iff.intro
-    (assume H₃ : a₁ ↔ a₂, iff.trans (iff.symm H₁) (iff.trans H₃ H₂))
-    (assume H₃ : b₁ ↔ b₂, iff.trans H₁ (iff.trans H₃ (iff.symm H₂)))
+  theorem congr_iff [congr] : (a₁ ↔ a₂) ↔ (b₁ ↔ b₂) :=
+  iff_iff_iff H₁ H₂
 end
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index f1fde36bf..1696516ea 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -15,7 +15,7 @@ calc
     ... ↔ a ∨ (c ∨ b)       : {or.comm}
      ... ↔ (a ∨ c) ∨ b      : iff.symm or.assoc
 
-theorem or.left_comm (a b c : Prop) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
+theorem or.left_comm [simp] (a b c : Prop) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
 calc
   a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc
     ... ↔ (b ∨ a) ∨ c       : {or.comm}
@@ -27,7 +27,7 @@ calc
     ... ↔ a ∧ (c ∧ b)       : {and.comm}
      ... ↔ (a ∧ c) ∧ b      : iff.symm and.assoc
 
-theorem and.left_comm (a b c : Prop) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
+theorem and.left_comm [simp] (a b c : Prop) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
 calc
   a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc
     ... ↔ (b ∧ a) ∧ c       : {and.comm}
@@ -42,10 +42,10 @@ iff.intro
 theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a :=
 iff.mp not_not_iff H
 
-theorem not_true_iff_false : ¬true ↔ false :=
+theorem not_true_iff_false [simp] : ¬true ↔ false :=
 iff.intro (assume H, H trivial) false.elim
 
-theorem not_false_iff_true : ¬false ↔ true :=
+theorem not_false_iff_true [simp] : ¬false ↔ true :=
 iff.intro (assume H, trivial) (assume H H', H')
 
 theorem not_or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
@@ -124,27 +124,27 @@ iff.intro
   (assume H, false.of_ne H)
   (assume H, false.elim H)
 
-theorem eq_self_iff_true {A : Type} (a : A) : (a = a) ↔ true :=
+theorem eq_self_iff_true [simp] {A : Type} (a : A) : (a = a) ↔ true :=
 iff_true_intro rfl
 
-theorem heq_self_iff_true {A : Type} (a : A) : (a == a) ↔ true :=
+theorem heq_self_iff_true [simp] {A : Type} (a : A) : (a == a) ↔ true :=
 iff_true_intro (heq.refl a)
 
-theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
+theorem iff_not_self [simp] (a : Prop) : (a ↔ ¬a) ↔ false :=
 iff.intro
   (assume H,
     have H' : ¬a, from assume Ha, (H ▸ Ha) Ha,
     H' (H⁻¹ ▸ H'))
   (assume H, false.elim H)
 
-theorem true_iff_false : (true ↔ false) ↔ false :=
+theorem true_iff_false [simp] : (true ↔ false) ↔ false :=
 not_true_iff_false ▸ (iff_not_self true)
 
-theorem false_iff_true : (false ↔ true) ↔ false :=
+theorem false_iff_true [simp] : (false ↔ true) ↔ false :=
 not_false_iff_true ▸ (iff_not_self false)
 
-theorem iff_true_iff (a : Prop) : (a ↔ true) ↔ a :=
+theorem iff_true_iff [simp] (a : Prop) : (a ↔ true) ↔ a :=
 iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H)
 
-theorem iff_false_iff_not (a : Prop) : (a ↔ false) ↔ ¬a :=
+theorem iff_false_iff_not [simp] (a : Prop) : (a ↔ false) ↔ ¬a :=
 iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H)
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 7ece059e5..fea7697aa 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -123,7 +123,7 @@
                "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]"
                "\[whnf\]" "\[multiple-instances\]" "\[none\]"
                "\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]"
-               "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[simp\]"
+               "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[simp\]" "\[congr\]"
                "\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]"
                "\[reduce-hints\]" "\[unfold-hints\]" "\[aliases\]" "\[eqv\]" "\[localrefinfo\]"))
       . 'font-lock-doc-face)
diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index 8752e342b..b408488af 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -40,6 +40,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
     m_subst                  = false;
     m_recursor               = false;
     m_simp                   = false;
+    m_congr                  = false;
 }
 
 void decl_attributes::parse(buffer<name> const & ns, parser & p) {
@@ -138,6 +139,9 @@ void decl_attributes::parse(buffer<name> const & ns, parser & p) {
         } else if (p.curr_is_token(get_simp_attr_tk())) {
             p.next();
             m_simp = true;
+        } else if (p.curr_is_token(get_congr_attr_tk())) {
+            p.next();
+            m_congr = true;
         } else if (p.curr_is_token(get_recursor_tk())) {
             p.next();
             if (!p.curr_is_token(get_rbracket_tk())) {
@@ -219,6 +223,8 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
         env = add_class(env, d, m_persistent);
     if (m_simp)
         env = add_simp_rule(env, d, m_persistent);
+    if (m_congr)
+        env = add_congr_rule(env, d, m_persistent);
     if (m_has_multiple_instances)
         env = mark_multiple_instances(env, d, m_persistent);
     return env;
@@ -229,7 +235,7 @@ void decl_attributes::write(serializer & s) const {
       << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible
       << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_full_hint
       << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor
-      << m_simp << m_recursor_major_pos << m_priority;
+      << m_simp << m_congr << m_recursor_major_pos << m_priority;
     write_list(s, m_unfold_hint);
 }
 
@@ -238,7 +244,7 @@ void decl_attributes::read(deserializer & d) {
       >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible
       >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_full_hint
       >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor
-      >> m_simp >> m_recursor_major_pos >> m_priority;
+      >> m_simp >> m_congr >> m_recursor_major_pos >> m_priority;
     m_unfold_hint = read_list<unsigned>(d);
 }
 }
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index f469920f8..507c43b62 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -30,6 +30,7 @@ class decl_attributes {
     bool               m_subst;
     bool               m_recursor;
     bool               m_simp;
+    bool               m_congr;
     optional<unsigned> m_recursor_major_pos;
     optional<unsigned> m_priority;
     list<unsigned>     m_unfold_hint;
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 26ec1741d..b83b5713e 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -108,7 +108,7 @@ void init_token_table(token_table & t) {
          "definition", "example", "coercion", "abbreviation",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans-instance]",
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
-         "[simp]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
+         "[simp]", "[congr]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
          "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-full]", "[unfold-hints]",
          "[constructor]", "[unfold", "print",
          "end", "namespace", "section", "prelude", "help",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index b743291bb..55691fb05 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -115,6 +115,7 @@ static name const * g_trans_tk = nullptr;
 static name const * g_refl_tk = nullptr;
 static name const * g_subst_tk = nullptr;
 static name const * g_simp_attr_tk = nullptr;
+static name const * g_congr_attr_tk = nullptr;
 static name const * g_recursor_tk = nullptr;
 static name const * g_attribute_tk = nullptr;
 static name const * g_with_tk = nullptr;
@@ -262,6 +263,7 @@ void initialize_tokens() {
     g_refl_tk = new name{"[refl]"};
     g_subst_tk = new name{"[subst]"};
     g_simp_attr_tk = new name{"[simp]"};
+    g_congr_attr_tk = new name{"[congr]"};
     g_recursor_tk = new name{"[recursor"};
     g_attribute_tk = new name{"attribute"};
     g_with_tk = new name{"with"};
@@ -410,6 +412,7 @@ void finalize_tokens() {
     delete g_refl_tk;
     delete g_subst_tk;
     delete g_simp_attr_tk;
+    delete g_congr_attr_tk;
     delete g_recursor_tk;
     delete g_attribute_tk;
     delete g_with_tk;
@@ -557,6 +560,7 @@ name const & get_trans_tk() { return *g_trans_tk; }
 name const & get_refl_tk() { return *g_refl_tk; }
 name const & get_subst_tk() { return *g_subst_tk; }
 name const & get_simp_attr_tk() { return *g_simp_attr_tk; }
+name const & get_congr_attr_tk() { return *g_congr_attr_tk; }
 name const & get_recursor_tk() { return *g_recursor_tk; }
 name const & get_attribute_tk() { return *g_attribute_tk; }
 name const & get_with_tk() { return *g_with_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 612f9a3fe..b748a552c 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -117,6 +117,7 @@ name const & get_trans_tk();
 name const & get_refl_tk();
 name const & get_subst_tk();
 name const & get_simp_attr_tk();
+name const & get_congr_attr_tk();
 name const & get_recursor_tk();
 name const & get_attribute_tk();
 name const & get_with_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index c289a8784..f21d3eee4 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -110,6 +110,7 @@ trans        [trans]
 refl         [refl]
 subst        [subst]
 simp_attr    [simp]
+congr_attr   [congr]
 recursor     [recursor
 attribute    attribute
 with         with
diff --git a/src/library/simplifier/simp_rule_set.cpp b/src/library/simplifier/simp_rule_set.cpp
index 735f47f30..c73ee9eae 100644
--- a/src/library/simplifier/simp_rule_set.cpp
+++ b/src/library/simplifier/simp_rule_set.cpp
@@ -191,6 +191,11 @@ environment add_simp_rule(environment const & env, name const & n, bool persiste
     return rrs_ext::add_entry(env, get_dummy_ios(), n, persistent);
 }
 
+environment add_congr_rule(environment const & env, name const & n, bool persistent) {
+    // TODO(Leo):
+    return env;
+}
+
 bool is_simp_rule(environment const & env, name const & n) {
     return rrs_ext::get_state(env).m_rnames.contains(n);
 }
diff --git a/src/library/simplifier/simp_rule_set.h b/src/library/simplifier/simp_rule_set.h
index d2899d338..0ecce41d9 100644
--- a/src/library/simplifier/simp_rule_set.h
+++ b/src/library/simplifier/simp_rule_set.h
@@ -69,6 +69,8 @@ simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id,
 simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2);
 
 environment add_simp_rule(environment const & env, name const & n, bool persistent = true);
+environment add_congr_rule(environment const & env, name const & n, bool persistent = true);
+
 /** \brief Return true if \c n is an active rewrite rule in \c env */
 bool is_simp_rule(environment const & env, name const & n);
 /** \brief Get current rewrite rule sets */