From 51bdf670fa8ef46f66c47e08c61dda85de90d079 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Feb 2021 12:42:13 -0800 Subject: [PATCH] chore: add `simp` helper lemmas --- src/Init/SimpLemmas.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 19b741c49d..cf1cdd0473 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -23,6 +23,12 @@ theorem eqFalse (h : ¬ p) : p = False := theorem eqFalse' (h : p → False) : p = False := propext <| Iff.intro (fun h' => absurd h' h) (fun h' => False.elim h') +theorem eqTrueOfDecide {p : Prop} {s : Decidable p} (h : decide p = true) : p = True := + propext <| Iff.intro (fun h => trivial) (fun _ => ofDecideEqTrue h) + +theorem eqFalseOfDecide {p : Prop} {s : Decidable p} (h : decide p = false) : p = False := + propext <| Iff.intro (fun h' => absurd h' (ofDecideEqFalse h)) (fun h => False.elim h) + theorem impCongr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) := h₁ ▸ h₂ ▸ rfl