Redundant lambda

Stream: new members

[Martin Dvořák]

This is a really stupid question, but I really don't know (I am not trolling).

example : (λ x : ℕ, x + 1) 2 = 3 :=
begin
  change 2 + 1 = 3,
  refl,
end

How do I change (λ x : ℕ, x + 1) 2 to 2 + 1 using rw instead of change please? Using change is really annoying when the term gets longer.

[Patrick Johnson]

Why do you want to use rw? tactic#dsimp can perform beta reduction.

[Patrick Johnson]

example : (λ x : ℕ, x + 1) 2 = 3 :=
begin
  dsimp only [],
  refl,
end

[Martin Dvořák]

Can you please give me a rw lemma? I usually want to avoid dsimps.

[Riccardo Brasca]

Using dsimp is the right thing to do, but does refl work without anything else?

[Riccardo Brasca]

I think that also something like change _ + _ = _ should work, saving some work

[Martin Dvořák]

Riccardo Brasca said:

Using dsimp is the right thing to do, but does refl work without anything else?

Yes refl works. However, my point was not to prove 2+1 but to provide a MWE. Having stuff like (λ x : ℕ, x + 1) 2 inside real proofs sucks.

[Martin Dvořák]

Riccardo Brasca said:

I think that also something like change _ + _ = _ should work, saving some work

I know it works but it is sometimes too verbose even with those underscores.

[Riccardo Brasca]

Maybe the question is why do you want to avoid dsimp, whose work is exactly this (among other things)

[Patrick Johnson]

Martin Dvořák said:

Can you please give me a rw lemma? I usually want to avoid dsimps.

Why do you want to avoid dsimps in the first place? After you finish the proof, you can delete all redundant dsimps (and most of the time, all of them are redundant).

If you want a rw lemma, you can make it easily:

lemma beta {α β : Type*} {f : α → β} {x : α} :
  (λ (y : α), f y) x = f x := rfl

example : (λ (x : ℕ), x + 1) 2 = 3 :=
begin
  rw beta,
end

But try not to use it in real proofs, because it's an anti-pattern.

[Martin Dvořák]

People usually don't want dsimp to stay inside the proof after the proof is finished. However, it hinders readability if I have to read stuff like (λ x : ℕ, x + 1) 2 later when I refactor my proof. Moreover dsimp sometimes does too much and I don't want to deal with it.

[Martin Dvořák]

Is there no such lemma inside the Lean core?

[Riccardo Brasca]

dsimp only is perfectly fine in a proof

[Martin Dvořák]

Thanks for clarification. Still dsimp only, sounds wrong. I usually expect something to appear after only.

[Riccardo Brasca]

But it does what you want right? I am not in front of a computer

[Martin Dvořák]

Yes, it does. Thanks.

[Martin Dvořák]

If dsimp only is the right thing to write, shouldn't we have an alias for it (which would make it sound idiomatic)?

[Riccardo Brasca]

I don't know

[Eric Wieser]

dsimp only is already pretty idiomatic in my opinion

[Martin Dvořák]

When I write dsimp only, or clear_except, I feel like saying a transitive verb without an object.

[Matt Diamond]

maybe you can think of it like "do you want dsimp with extras?" "no, I just want dsimp only"

[Matt Diamond]

no idea how to make clear_except sound normal, though

[Kyle Miller]

@Martin Dvořák If you find dsimp only to be too linguistically irksome, you can write dsimp only [], which means the same thing as dsimp only.

You can see what kinds of reductions dsimp does in the last section of https://leanprover-community.github.io/extras/simp.html (look for every option for which the dsimp column has a tt).

[Martin Dvořák]

Matt Diamond said:

no idea how to make clear_except sound normal, though

We would have to make an alias like clear_all for clear_except without arguments. However, I don't think it is a good way how to develop a programming language. IMO it falls into the same category as intros and variables.

[Kyle Miller]

I don't think I've ever used clear_except. What is the sort of scenario where you are finding you need to manage your context like this?

[Kyle Miller]

Regarding intros, tactic#rintro is a more powerful replacement. variables has been fixed in Lean 4; it's always variable now.

[Martin Dvořák]

Kyle Miller said:

I don't think I've ever used clear_except. What is the sort of scenario where you are finding you need to manage your context like this?

Maybe I don't use it because the style I use is writing lots of small lemmas that take few steps. I've used clear occasionally in conjuction with induction to make sure my induction hypothesis is correct, though.

In past, I had many proofs by cases in my code where some of the cases were tautological, so I closed them by { clear_except, tauto, }, and continued to the next case. That said, most of these use cases disappeared from my code after I learned about no_confusion on inductive types.

[Martin Dvořák]

I don't use that many small lemmas. Probably because I prefer to clutter my proofs rather than to clutter my namespace.

[Kyle Miller]

Where do you use no_confusion? I think there are usually other approaches than using it directly (like cases h or injection h when h is an equality. There's also tactic#unify_equations, which I occasionally use).

[Kyle Miller]

Martin Dvořák said:

I don't use that many small lemmas. Probably because I prefer to clutter my proofs rather than to clutter my namespace.

I suppose this is where the software engineering part of working with proof assistants comes in. If you find the right way to decompose your arguments into more generally useful sub-lemmas, then it's not cluttering your namespace, and you get to reuse sub-arguments.

[Martin Dvořák]

Kyle Miller said:

Where do you use no_confusion? I think there are usually other approaches than using it directly (like cases h or injection h when h is an equality. There's also tactic#unify_equations, which I occasionally use).

If you want to see how often I use no_confusion, look at these two commits I made the other day:
https://github.com/madvorak/grammars/commit/850c2ab314d3602c0c8acb835f272514b9dd8ee1
https://github.com/madvorak/grammars/commit/decbbe93874769b8e8bd0230813a77b7787538b9

[Martin Dvořák]

Kyle Miller said:

Martin Dvořák said:

I don't use that many small lemmas. Probably because I prefer to clutter my proofs rather than to clutter my namespace.

I suppose this is where the software engineering part of working with proof assistants comes in. If you find the right way to decompose your arguments into more generally useful sub-lemmas, then it's not cluttering your namespace, and you get to reuse sub-arguments.

I usually try to follow the software-engineering best practices, but I am a dumb bitch.

[Kyle Miller]

Re your commits, for example you can do exact option.no_confusion zeroth -> cases zeroth or injection zeroth

[Martin Dvořák]

I didn't know I could use cases on equalities! It works, but what does cases do with equalities in general?

[Kyle Miller]

Think about what docs#eq is, an inductive type with a single constructor rfl

[Martin Dvořák]

Kyle Miller said:

Re your commits, for example you can do exact option.no_confusion zeroth -> cases zeroth or injection zeroth

Still, we probably agree that my old style — discharging these simple situations by tauto — was stupid.

[Kyle Miller]

What cases does is try to solve for the fact that when you have x = y that x and y need to be definitionally the same for it to be rfl : x = x

[Kyle Miller]

but when cases finds a contradiction, it'll automatically close the goal

[Kyle Miller]

it's able to do some amount of no_confusion reasoning for you, basically.

[Martin Dvořák]

Kyle Miller said:

Think about what docs#eq is, an inductive type with a single constructor rfl

I am shaken. I always thought that = was some kind of primitivum, not an inductive type, not a pi type either.

[Riccardo Brasca]

See this post for more details.

[Martin Dvořák]

Back to the topic... Is there a consensus that using dsimp, in non-terminal positions is unacceptable but using dsimp only, in non-terminal positions is all right?

[Kyle Miller]

The consensus is that dsimp is OK everywhere, but that you should check whether you really needed it since sometimes it's removable.

[Martin Dvořák]

It is often removable but doing so makes the proof unreadable for the next time.

[Kyle Miller]

Then don't remove it :wink:

[Martin Dvořák]

Is the consensus that dsimp, is OK when removing it breaks the proof and that dsimp only, is OK always?

[Riccardo Brasca]

dsimp only is surely OK. Usually, even nonterminal dsimp are acceptable, but I personally think dsimp only [...] it's better.

[Martin Dvořák]

Kyle Miller said:

Martin Dvořák If you find dsimp only to be too linguistically irksome, you can write dsimp only [], which means the same thing as dsimp only.

You can see what kinds of reductions dsimp does in the last section of https://leanprover-community.github.io/extras/simp.html (look for every option for which the dsimp column has a tt).

image.png
This is the thing that shouted at my face.

[Martin Dvořák]

Riccardo Brasca said:

dsimp only is surely OK. Usually, even nonterminal dsimp are acceptable, but I personally think dsimp only [...] it's better.

Then I have 24 dsimps to refactor. Which is not that bad. Still, I hope I will use dsimp less often in the future.

[Riccardo Brasca]

Ar you aware of squeeze_dsimp? It will do this for you.

[Riccardo Brasca]

(but not 24 times at once)

[Junyan Xu]

squeeze_dsimp is not robust and is prone to return invalid results; you may use squeeze_simp and remove unnecessary lemmas but that's more work.

Structure projection lemmas like docs#subtype.coe_mk are subsumed by dsimp only, but we still include them in mathlib, so I'd argue it's acceptable/desirable to have this lemma lemma beta {α β : Sort*} {f : α → β} {x : α} : (λ (y : α), f y) x = f x := rfl in mathlib as well to gain more fine control. (However, the LHS ⟨a,h⟩ of docs#subtype.coe_mk is prone to "motive type not correct" errors when rewriting a, so you do need to simplify it to RHS sometimes, and the same doesn't seem to apply to (λ y, f y) x.)

[Kyle Miller]

An issue with beta as a rewrite lemma is that it requires higher order unification to apply (you need to solve for a function f -- you might have y appear multiple times in f y in general beta reduction). This version is closer to congr_fun of eta-reduction.

[Yaël Dillies]

squeeze_dsimp is buggy though, right?