From 0fe561d063da40b862b181bd92ec9685133e33bd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 19 Dec 2017 14:14:38 +0100 Subject: [PATCH] feat(init/function): `comp_app` simp lemma --- library/init/data/list/lemmas.lean | 3 +-- library/init/function.lean | 2 ++ 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index efd4130f91..ad642c786e 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -192,8 +192,7 @@ theorem length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length @[simp] lemma partition_eq_filter_filter (p : α → Prop) [decidable_pred p] : ∀ (l : list α), partition p l = (filter p l, filter (not ∘ p) l) | [] := rfl -| (a::l) := by { by_cases pa : p a; simp [partition, filter, pa, partition_eq_filter_filter l], - rw [if_neg (not_not_intro pa)], rw [if_pos pa] } +| (a::l) := by { by_cases pa : p a; simp [partition, filter, pa, partition_eq_filter_filter l] } /- sublists -/ diff --git a/library/init/function.lean b/library/init/function.lean index abcd06a6c2..648a6ea1ef 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -51,6 +51,8 @@ lemma left_id (f : α → β) : id ∘ f = f := rfl lemma right_id (f : α → β) : f ∘ id = f := rfl +@[simp] lemma comp_app (f : β → φ) (g : α → β) (a : α) : (f ∘ g) a = f (g a) := rfl + lemma comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl lemma comp.left_id (f : α → β) : id ∘ f = f := rfl