Zulip Chat Archive

Stream: new members

Topic: Redundant lambda


Martin Dvořák (Nov 11 2022 at 17:01):

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 (Nov 11 2022 at 17:05):

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

Patrick Johnson (Nov 11 2022 at 17:05):

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

Martin Dvořák (Nov 11 2022 at 17:08):

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

Riccardo Brasca (Nov 11 2022 at 17:08):

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

Riccardo Brasca (Nov 11 2022 at 17:09):

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

Martin Dvořák (Nov 11 2022 at 17:11):

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 (Nov 11 2022 at 17:12):

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 (Nov 11 2022 at 17:14):

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

Patrick Johnson (Nov 11 2022 at 17:17):

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 (Nov 11 2022 at 17:17):

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 (Nov 11 2022 at 17:18):

Is there no such lemma inside the Lean core?

Riccardo Brasca (Nov 11 2022 at 17:18):

dsimp only is perfectly fine in a proof

Martin Dvořák (Nov 11 2022 at 17:19):

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

Riccardo Brasca (Nov 11 2022 at 17:20):

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

Martin Dvořák (Nov 11 2022 at 17:21):

Yes, it does. Thanks.

Martin Dvořák (Nov 11 2022 at 17:23):

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 (Nov 11 2022 at 17:33):

I don't know

Eric Wieser (Nov 11 2022 at 17:47):

dsimp only is already pretty idiomatic in my opinion

Martin Dvořák (Nov 11 2022 at 20:13):

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

Matt Diamond (Nov 11 2022 at 21:12):

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

Matt Diamond (Nov 11 2022 at 21:13):

no idea how to make clear_except sound normal, though

Kyle Miller (Nov 12 2022 at 13:48):

@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 (Nov 12 2022 at 13:59):

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 (Nov 12 2022 at 14:02):

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 (Nov 12 2022 at 14:04):

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

Martin Dvořák (Nov 12 2022 at 14:12):

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 (Nov 12 2022 at 14:13):

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

Kyle Miller (Nov 12 2022 at 14:14):

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 (Nov 12 2022 at 14:15):

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 (Nov 12 2022 at 14:16):

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 (Nov 12 2022 at 14:18):

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 (Nov 12 2022 at 14:20):

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

Martin Dvořák (Nov 12 2022 at 14:23):

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

Kyle Miller (Nov 12 2022 at 14:24):

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

Martin Dvořák (Nov 12 2022 at 14:24):

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 (Nov 12 2022 at 14:24):

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 (Nov 12 2022 at 14:25):

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

Kyle Miller (Nov 12 2022 at 14:25):

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

Martin Dvořák (Nov 12 2022 at 14:27):

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 (Nov 12 2022 at 14:29):

See this post for more details.

Martin Dvořák (Nov 12 2022 at 14:39):

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 (Nov 12 2022 at 14:42):

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 (Nov 12 2022 at 14:43):

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

Kyle Miller (Nov 12 2022 at 14:44):

Then don't remove it :wink:

Martin Dvořák (Nov 12 2022 at 14:44):

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

Riccardo Brasca (Nov 12 2022 at 14:46):

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

Martin Dvořák (Nov 12 2022 at 14:48):

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 (Nov 12 2022 at 14:49):

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 (Nov 12 2022 at 14:54):

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

Riccardo Brasca (Nov 12 2022 at 14:54):

(but not 24 times at once)

Junyan Xu (Nov 12 2022 at 16:22):

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 (Nov 12 2022 at 17:06):

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 (Nov 12 2022 at 19:04):

squeeze_dsimp is buggy though, right?


Last updated: Dec 20 2023 at 11:08 UTC