From 5296275c41d2db058a45a1bdd6a1c0dfd8d522da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Jul 2014 12:29:23 -0700 Subject: [PATCH] feat(library/standard/logic): add imp_or theorems Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index bb8e43e2b8..4bd0c37eab 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -99,6 +99,21 @@ theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) (assume Ha, absurd_elim _ Ha Hna) (assume Hb, absurd_elim _ Hb Hnb) +theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d +:= or_elim H1 + (assume Ha : a, or_intro_left _ (H2 Ha)) + (assume Hb : b, or_intro_right _ (H3 Hb)) + +theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c +:= or_elim H1 + (assume H2 : a, or_intro_left _ (H H2)) + (assume H2 : c, or_intro_right _ H2) + +theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b +:= or_elim H1 + (assume H2 : c, or_intro_left _ H2) + (assume H2 : a, or_intro_right _ (H H2)) + inductive eq {A : Type} (a : A) : A → Prop := | refl : eq a a