From 0c6056aaa9b593cdc694c814b9593d6b2a6c8c5b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Nov 2024 14:52:41 -0800 Subject: [PATCH] chore: add `letFun` helper simp theorems --- src/Init/SimpLemmas.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 3cab2e7cac6f..beb1b18bcb9e 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -72,6 +72,21 @@ theorem let_body_congr {α : Sort u} {β : α → Sort v} {b b' : (a : α) → (a : α) (h : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a; b' x) := (funext h : b = b') ▸ rfl +theorem letFun_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : @letFun α (fun _ => β) a (fun _ => b) = b' := + h + +theorem letFun_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β} (h₁ : a = a') (h₂ : ∀ x, f x = f' x) + : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f' := by + rw [h₁, funext h₂] + +theorem letFun_body_congr {α : Sort u} {β : Sort v} (a : α) {f f' : α → β} (h : ∀ x, f x = f' x) + : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a f' := by + rw [funext h] + +theorem letFun_val_congr {α : Sort u} {β : Sort v} {a a' : α} {f : α → β} (h : a = a') + : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f := by + rw [h] + @[congr] theorem ite_congr {x y u v : α} {s : Decidable b} [Decidable c] (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : ite b x y = ite c u v := by