How does lambda work?

Stream: new members

[Boldizsar Mann]

Hey, I have been trying to use a basic lambda expression in Lean. If I have something like (λx : N, x) m and m : N, then how can I simplify this expression to just m?

[Kalle Kytölä]

In tactic mode dsimp should work.

[Boldizsar Mann]

Oh thanks!

[Kalle Kytölä]

Also simp should do this, I believe, but it might also do other things. As far as I understand, dsimp is meant to do only the type of things that you asked for.

[Kevin Buzzard]

Note that they are definitionally equal, so you should be able to use them interchangeably in a term mode proof.

[Boldizsar Mann]

The simp tactic looks for applicable facts to apply the replace tactic with. In this case, what fact is applied here?

[Patrick Johnson]

Simp also performs beta and eta reduction (and a few other reductions).
The expression (λ (x : N), x) m beta-reduces to m.

[Floris van Doorn]

Kalle Kytölä said:

Also simp should do this, I believe, but it might also do other things. As far as I understand, dsimp is meant to do only the type of things that you asked for.

dsimp will rewrite with all @[simp] lemmas that are proven by reflexivity. dsimp only will not do this, and can be used to just do reduction/computation that are built into the type theory. This doesn't involve applying any lemmas, just computing. The list of computations Lean can perform without applying any lemmas is here: https://leanprover.github.io/reference/expressions.html#computation

[Floris van Doorn]

Boldizsar Mann said:

The simp tactic looks for applicable facts to apply the replace tactic with. In this case, what fact is applied here?

simp, simp only, dsimp, dsimp only will all do computation (and some of them will also rewrite with lemmas), see my previous message.

[Eric Wieser]

This doesn't involve applying any lemmas, just computing

You could probably argue that dsimp doesn't "apply" any lemmas: it uses lemmas to inform what the new goal should be, but then ultimately lets the kernel compute that the result and original are the same by definition, and doesn't attempt to build up a proof one lemma at a time.