From f60fc5183a7f769a7c746ac1e2a9e410da9c4d78 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Mar 2015 17:56:50 -0800 Subject: [PATCH] feat(library/data/bool): add auxiliary theorems --- library/data/bool.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/library/data/bool.lean b/library/data/bool.lean index 1088d3266..df54e6287 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -29,6 +29,17 @@ namespace bool ... = false : cond.ff) true_ne_false + theorem eq_tt_of_ne_ff : ∀ {a : bool}, a ≠ ff → a = tt + | @eq_tt_of_ne_ff tt H := rfl + | @eq_tt_of_ne_ff ff H := absurd rfl H + + theorem eq_ff_of_ne_tt : ∀ {a : bool}, a ≠ tt → a = ff + | @eq_ff_of_ne_tt tt H := absurd rfl H + | @eq_ff_of_ne_tt ff H := rfl + + theorem absurd_of_eq_ff_of_eq_tt {B : Prop} {a : bool} (H₁ : a = ff) (H₂ : a = tt) : B := + absurd (H₁⁻¹ ⬝ H₂) ff_ne_tt + theorem bor.tt_left (a : bool) : bor tt a = tt := rfl