From c0f5ab1fa51bffaa571d47feb26a97d8b04b7d99 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Feb 2021 14:07:01 -0800 Subject: [PATCH] feat: add congruence lemmas for `simp` --- src/Init/SimpLemmas.lean | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index ea4f88bb24..1a5f1dc6b9 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -34,3 +34,31 @@ theorem impCongrCtx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p theorem forallCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a = q a)) : (∀ a, p a) = (∀ a, q a) := have p = q from funext h this ▸ rfl + +theorem iteCongr {x y u v : α} [s : Decidable b] (h₁ : b = c) (h₂ : x = u) (h₃ : y = v) + : ite b x y = (@ite _ c (Eq.ndrec s h₁) u v) := by + subst b x y; rfl + +theorem iteCongrCtx {x y u v : α} [s : Decidable b] (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) + : ite b x y = (@ite _ c (Eq.ndrec s h₁) u v) := by + subst b + cases Decidable.em c with + | inl h => rw [ifPos h, ifPos h]; exact h₂ h + | inr h => rw [ifNeg h, ifNeg h]; exact h₃ h + +theorem Eq.mprProp {p q : Prop} (h₁ : p = q) (h₂ : q) : p := + h₁ ▸ h₂ + +theorem Eq.mprNot {p q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p := + h₁ ▸ h₂ + +theorem diteCongr [s : Decidable b] + {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} + (h₁ : b = c) + (h₂ : (h : c) → x (Eq.mprProp h₁ h) = u h) + (h₃ : (h : ¬c) → y (Eq.mprNot h₁ h) = v h) + : dite b x y = (@dite _ c (Eq.ndrec s h₁) u v) := by + subst b + cases Decidable.em c with + | inl h => rw [difPos h, difPos h]; exact h₂ h + | inr h => rw [difNeg h, difNeg h]; exact h₃ h