Lemmas for functions

Stream: lean4

[Julien Marquet]

I couldn't find these lemmas in lean4, are there somewhere ?

∀ {α β} (f : α → β) {a b : α}, a = b → f a = f b
∀ {α β} {f g : α → β}, f = g → ∀ a, f a = g a

[Sebastian Ullrich]

congrArg/congrFun

[Julien Marquet]

(Oh, I understand why I didn't find them, I was expecting a f a = f b notation but they are written with Eq. Thanks !)

[Kevin Buzzard]

A lot of lean 4 core stuff is written without notation. Is there a reason for this?

[Daniel Selsam]

I presume it is a staging issue -- defining the notations (e.g. in Init/Notation.Lean) depends on many things from Init/Prelude.lean. AFAICT only Prelude.lean cannot use the notations defined in Notation.lean.

[Julien Marquet]

By the way, is there a theorem for beta reduction ?
(I noticed that simp only [] already does beta reductions)

[Julien Marquet]

(I sometimes want to rewrite in expressions like (fun x => a * x) y, but I have to beta-reduce first)

[Daniel Selsam]

beta reduction is builtin to the logic of Lean, and simp beta-reduces automatically without needing justification (since the result is def-eq to the original term).

[Daniel Selsam]

you can disable this though, if you don't want simp to beta-reduce

[Daniel Selsam]

These are the simp flags: https://github.com/leanprover/lean4/blob/master/src/Init/Meta.lean#L870-L880

[Julien Marquet]

By looking further where you pointed I also found more useful features of simp so thanks ! :)

[Sebastian Ullrich]

There is also a brief, non-exhaustive list of simp features at https://raw.githubusercontent.com/IPDSnelting/tba-2021/master/slides/lecture4.pdf?page=12, pages 12 ff

[Mario Carneiro]

Daniel Selsam said:

I presume it is a staging issue -- defining the notations (e.g. in Init/Notation.Lean) depends on many things from Init/Prelude.lean. AFAICT only Prelude.lean cannot use the notations defined in Notation.lean.

I thought it was a remnant of earlier versions of lean 4 without the stage0 stuff. With it, I don't see why notations can't be introduced immediately after the definition itself, similar to how it is done in lean 3

[Sebastian Ullrich]

These notations are not built-in, so they are taken from the current stage, so they can be defined only after ParserDescr/Macro.

[Mario Carneiro]

Does writing infixl "foo" => bar require ParserDescr to exist in the current stage? It doesn't directly reference this constant and doesn't require import Lean so I'm not sure how that happens

[Sebastian Ullrich]

It does elaborate to a ParserDescr (which is defined in Prelude)