From 97bc609e77f958c73b6ce71bcf3ea3a134f4b78e Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 14 Jun 2025 16:15:10 -0700 Subject: [PATCH] feat: add `have` forms of `let_*` simp lemmas (#8790) This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on #8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; for now they are duplicates of the `letFun_*` lemmas. --- src/Init/SimpLemmas.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 1bbe56d9b6..c7ac4cf7a1 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -74,6 +74,28 @@ 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 have_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β} + (h : b = b') : (have _ := a; b) = b' := h + +theorem have_unused_dep {α : Sort u} {β : Sort v} (a : α) {b : α → β} {b' : β} + (h : ∀ x, b x = b') : (have x := a; b x) = b' := h a + +theorem have_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β} + (h₁ : a = a') (h₂ : ∀ x, f x = f' x) : (have x := a; f x) = (have x := a'; f' x) := + @congr α β f f' a a' (funext h₂) h₁ + +theorem have_val_congr {α : Sort u} {β : Sort v} {a a' : α} {f : α → β} + (h : a = a') : (have x := a; f x) = (have x := a'; f x) := + @congrArg α β a a' f h + +theorem have_body_congr_dep {α : Sort u} {β : α → Sort v} (a : α) {f f' : (x : α) → β x} + (h : ∀ x, f x = f' x) : (have x := a; f x) = (have x := a; f' x) := + h a + +theorem have_body_congr {α : Sort u} {β : Sort v} (a : α) {f f' : α → β} + (h : ∀ x, f x = f' x) : (have x := a; f x) = (have x := a; f' x) := + h a + theorem letFun_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : @letFun α (fun _ => β) a (fun _ => b) = b' := h