Code smell?

Stream: new members

[Martin Dvořák]

Is it a code smell if I often write apply congr_arg, in my proofs?

[Eric Wieser]

Sometimes you might want congr' 1, instead. refine congr_arg _ _ can also sometimes be more predictable

[Martin Dvořák]

Is it a code smell if I write change immediately followed by convert_to in some places (not many) of my proofs?

[Damiano Testa]

My experience with change is that often you are better off proving a rfl lemma doing the change for you. In some cases this simple trick has spectacular proof-shortening effects. I wish I had an example at hand, but I don't at the moment.

[Martin Dvořák]

You mean a lemma that "restates" the definition?

[Damiano Testa]

Yes, just a lemma whose proof is rfl, guiding lean through the definition.

[Martin Dvořák]

Is there no better way how to tell Lean to apply / unapply definition without creating this boilerplate? Unfortunately unfold does not always do what I want.

[Eric Wieser]

Can you give an example of a definition where unfold does the wrong thing?

[Martin Dvořák]

Yes, I can. However, making MWE out of it will probably be hard.

[Eric Wieser]

What's the non-mwe version? Can you link to a gist or something?

[Martin Dvořák]

On this line:
https://github.com/madvorak/grammars/blob/75c5d5db4be45957bafd1d651086821af4373472/src/context_free/closure_properties/binary/CF_union_CF.lean#L326

I am unpacking this definition:
https://github.com/madvorak/grammars/blob/75c5d5db4be45957bafd1d651086821af4373472/src/context_free/cfg.lean#L29

Unfotunately unfold CF_generates, does not work.

[Martin Dvořák]

It gives me: simplify tactic failed to simplify

[Eric Wieser]

What's the goal state at that point

[Martin Dvořák]

I would like to obtain CF_generates_str (union_grammar g₁ g₂) (list.map symbol.terminal w), without stating it explicitly. My change only does what I supposed that unfold would do.

[Kevin Buzzard]

I would say that unfold is a code smell indicating that there is missing boilerplate.

[Martin Dvořák]

Is there really no better way than repeating the definition again as a lemma? I hate how it looks.

[Yaël Dillies]

Does rw CF_generates do what you want?

[Martin Dvořák]

It gives me: failed

[Eric Wieser]

Martin Dvořák said:

I would like to obtain CF_generates_str (union_grammar g₁ g₂) (list.map symbol.terminal w), without stating it explicitly. My change only does what I supposed that unfold would do.

Yes, but what was the goal state before that?

[Martin Dvořák]

Oh sorry. It was: w ∈ CF_generates (union_grammar g₁ g₂)

[Eric Wieser]

That goal is nonsense

[Eric Wieser]

CF_generates isn't a set

[Eric Wieser]

How did you get there?

[Eric Wieser]

Is language docs#language?

[Eric Wieser]

If so, these lines are wrong
https://github.com/madvorak/grammars/blob/75c5d5db4be45957bafd1d651086821af4373472/src/context_free/cfg.lean#L33-L34

[Eric Wieser]

That should be

def CF_language : language T :=
set_of (CF_generates g)

[Martin Dvořák]

Oh, thanks a lot!!

So I cannot use set t as t → Prop hoping that it is definitionally equivalent?

[Eric Wieser]

You'll find you have to fight with change all the time if you do that

[Martin Dvořák]

Thank you very much!!! This change will eliminate change in so many places!!!

[Eric Wieser]

They're definitionally equivalent, but to keep things in a state where lean will help you, you use ∈ to convert a set into a function, and docs#set_of (aka {x | p x}) to convert a function into a set

[Martin Dvořák]

I don't know whether it is related but... When I have a goal in the form of list.mem a L existing lemmata about lists don't work. I have to change it to a ∈ L and only then they can be applied. Is there a similar trick for that?

[Yaël Dillies]

Same question. How did you get there?

[Martin Dvořák]

I had: r_in : r ∈ (head :: tail)
https://github.com/madvorak/grammars/blob/75c5d5db4be45957bafd1d651086821af4373472/src/context_free/closure_properties/binary/CF_union_CF.lean#L151
I called: cases r_in,
The first case was great: r = head
The second case was: list.mem r tail
What could I have done instead to obtain r ∈ tail please?

[Eric Wieser]

You should have looked for a lemma that matches the form of the hypothesis

[Eric Wieser]

#naming suggests it would be called docs#list.mem_cons

[Eric Wieser]

Clicking that link reveals it's called docs#list.mem_cons_iff

[Eric Wieser]

Either way, if you type list.mem_cons in vs-code, autocomplete should do the rest

[Martin Dvořák]

Thanks a lot!!!

[Martin Dvořák]

Is there a general methodical mistake that I make?

[Eric Wieser]

In fact, cases list.eq_or_mem_of_mem_cons r_in is probably what you want, where that lemma is just below the one I linked to

[Eric Wieser]

Martin Dvořák said:

Is there a general methodical mistake that I make?

Always search for a lemma before unfolding. To some extent, cases does unfolding too. Use your judgement on the output of cases to decide if you might have unfolded too far

[Eric Wieser]

An easy way to search for useful lemmas is just simp?

[Martin Dvořák]

I learnt to use squeeze_simp only recently.

[Eric Wieser]

Which might not get you to where you want to be, but will usually take you to a place where it's easier to find matching lemmas

[Eric Wieser]

Martin Dvořák said:

I learnt to use squeeze_simp only recently.

That's better than simp? but a bit slower

[Martin Dvořák]

Is it a code smell when I have the following pair of lines in my code?

rw some_lemma,
rw some_lemma at some_assumption,

[Rémy Degenne]

You can write instead the shorter

rw some_lemma at some_assumption ⊢,

That last sign means the goal.

[Rémy Degenne]

Writing such a line is not uncommon and not a code smell in itself

[Martin Dvořák]

Is it idiomatic to use variable instead of variables when adding a single (implicit) argument?

[Yaël Dillies]

I tend not to because my brain always bugs when I then add another variable to it and get a weird error.

[Eric Wieser]

Yeah, I agree; the very marginal readability benefit is totally outweighed by the awkwardness to edit

[Eric Wieser]

It would be like having [1, 2, and 3] as list notation

[Martin Dvořák]

It smells like a slightly bad design decision that both variable and variables exist.

[Yaël Dillies]

I think it would be fine if they were functionally the same.

[Martin Dvořák]

However, I am pretty fine with both intro and intros because I almost never edit them.

[Mario Carneiro]

Note that in lean 4 variable has been deleted and variables has been renamed to variable

[Mario Carneiro]

I think intro is just as bad TBH. rintro is just silently identical to rintros

[Yaël Dillies]

Yeah, I always use rintro instead of intro and intros for the same reasons.

[Mario Carneiro]

Plurals were a mistake :trademark:

[Mario Carneiro]

Although, a variation on this same "one looks different from more than one" issue is rw e vs rw [e1, e2]

[Mario Carneiro]

lean 4 also removed the first version, possibly for this reason

[Martin Dvořák]

I really like rw e as it works in lean 3.

[Martin Dvořák]

BTW, is it a bad style if I declare variables which are then used only in small portion of the stuff in the given scope?

[Patrick Massot]

We do it all the time in mathlib

[Martin Dvořák]

Is it OK even if they occupy "expensive" identifiers (i.e., one-letter names)?

[Eric Wieser]

You can always "shadow" expensive variable names in lemma statements

[Eric Wieser]

The two main problems you face when having too many variables are usually:

• Having a type R that has too many typeclasses in the variables list, and not being able to easily exclude those without declaring a brand new R
• Not remembering whether the variables line 100 lines up the file uses () or {} to declare the variables, and getting your argument implicitness wrong as a result

[Martin Dvořák]

Am I the only one who finds it confusing to use variables for explicit arguments (a : T) shared by multiple items? I have a natural tendency to expect, when I look at a declaration of a function, to see all arguments that I need to pass when calling the function.

The code intellisense "quick info" in VSCode shows all arguments (including those written using variables anywhere above) but I like to look at my definition in the code. There I easily get confused by an "invisible" required argument.

[Violeta Hernández]

I agree that it's confusing. Gets particularly annoying when you add a few extra theorems and suddenly the argument a can be made implicit in them

[Martin Dvořák]

So, should I use variables only for {stuff} and [stuff] for the sake of code readability?

[Violeta Hernández]

I mean, if you have 15 theorems in a code block and all of them need an explicit argument, I'd say using variables (stuff) is fine

[Violeta Hernández]

But if it's just a handful, then it's not a great idea

[Martin Dvořák]

I'd like to hear more opinions about this issue. It has been bugging me recently a lot.

[Yaël Dillies]

I have the same stance as Violeta. Unless all your lemmas are gonna need the same explicit arguments, restrict variables declarations to implicit or instance arguments.

[Martin Dvořák]

And if they do, does it justify the loss of readability?

[Violeta Hernández]

I think that in some cases, you gain a lot of readability. Writing down (a : T) (b : U) (c : V) over and over, particularly when the types have much longer names, and particularly when they're clear from context, is quite a chore

[Eric Wieser]

I think my view lies closer to Martin's here. One other case to consider; if one of your explicit arguments is a Type, it's a chore to repeat all its typeclasses on a lemma. Usually this is handled with variables (R) the_lemma variables {R}

[Eric Wieser]

Which is still fairly readable because the explicit argument is adjacent

[Martin Dvořák]

Is there a shortcut for the following two lines?

  rw set.mem_set_of_eq at ⊢ h,
  rw set.mem_set_of_eq at ⊢,

I want to apply set.mem_set_of_eq twice to the goal and once to h.

[Riccardo Brasca]

Does

simp only [set.mem_set_of_eq] at ⊢ h

work?

[Yaël Dillies]

dsimp at ⊢ h,?

[Damiano Testa]

Or even not doing anything? :upside_down:

[Riccardo Brasca]

Ah yes, I didn't even had a look of what the lemma was.
To clarify, the lemma is useful for a human being, but the LHS is defined to be the RHS, so it's possible the Lean doesn't need it at all.

[Martin Dvořák]

Riccardo Brasca said:

Does

simp only [set.mem_set_of_eq] at ⊢ h

work?

Yes, it does. However, I don't like calling simp for something that I know precisely how to do.

[Martin Dvořák]

I tried rw set.mem_set_of_eq at ⊢ h ⊢, but was disappointed.

[Martin Dvořák]

I don't mind that much that I have to write two nearly-identical lines. I hate that the "three operations" are grouped into "two commands" in a counter-intuitive way.

[Damiano Testa]

Maybe you could try repeat { rw set.mem_set_of_eq, try { rw set.mem_set_of_eq at h } }?

[Damiano Testa]

I'm not sure what we are aiming for here, though...

[Martin Dvořák]

Damiano Testa said:

I'm not sure what we are aiming for here, though...

I am aiming for something less awkward. If it cannot be done, I will put up with it.

[Martin Dvořák]

Damiano Testa said:

Maybe you could try repeat { rw set.mem_set_of_eq, try { rw set.mem_set_of_eq at h } }?

I'd rather write three lines than this.

[Damiano Testa]

But have you tried just skipping the rw?

[Damiano Testa]

What is the next line in your proof?

[Martin Dvořák]

I know I can skip this rw. However, according to some advice I obtained here previously, I decided to define stuff with set_of in order to avoid the command change. So now, I want to take advantage of that. I am aware that set.mem_set_of_eq does only a definitional equality; however, it has impact on the effect of some other tactics. And I don't feel like going to change again.

[Kyle Miller]

Martin Dvořák said:

Yes, it does. However, I don't like calling simp for something that I know precisely how to do.

I'm curious what the motivation is for this preference -- simp is designed for repeatedly doing rewrites like this.

But if this preference is strong, you can refactor it as

  repeat { rw set.mem_set_of_eq },
  rw set.mem_set_of_eq at h,

[Martin Dvořák]

Calling simp performs some kind of state-space search. Why would I tell the computer to perform the search every time it rebuilds my project if I can explicitly say what three substitutions lead to the desired state?

[Martin Dvořák]

BTW, I don't like calling repeat for something that I want to do exactly twice. What is your preference?

[Damiano Testa]

Regarding your state-space search, it would be interesting to measure the time difference. After all, rw also looks around the expression to find locations to perform the rewrite. I wonder which one is faster. It might depend on the expression itself...

[Damiano Testa]

I have certainly observed simp producing shorter proof terms than the corresponding chain of rewrites, but not always.

[Martin Dvořák]

I like to use simp together with have or convert but not in the middle of my proof.

[Martin Dvořák]

I know that simp only is pretty safe to use, but I still don't like it in non-terminal positions.

[Damiano Testa]

I'm also wary of non-terminal simps, so I understand your concern.

[Martin Dvořák]

In general, I prefer to use simp less often. Also my friends make fun of me: "Look, Martin is simping for math again!"

[Kyle Miller]

Martin Dvořák said:

Calling simp performs some kind of state-space search.

How much work do you think it's doing here? It might be called "simp" but that doesn't mean it's looking for the simplest representation (unless the simp lemmas you provide cause it to enter rewrite cycles, like with add_assoc and add_comm together)

[Yakov Pechersky]

simp only is not calling any lemmas other than the ones you provide. It still does things that rw doesn't, like beta reduction

[Kyle Miller]

If you don't like repeat, then try tactic#iterate or

  rw [set.mem_set_of_eq, set.mem_set_of_eq],
  rw set.mem_set_of_eq at h,

[Stuart Presnell]

If you’re doing something to be PRed to mathlib then the preference is (other things being equal) for shorter solutions. So if simp only does the job, your personal preference for a more verbose spelling likely won’t make it through review. Of course, this isn’t an issue if you’re just writing for your own projects.

[Martin Dvořák]

Yes, it is a project that only I write.

[Martin Dvořák]

Is there a more idiomatic way how to write clear_except, to delete everything but the goal?

[Martin Dvořák]

Is there a shortcut for the following construction?

have sublemma : ∃ x, (...),
{
  (...)
},
cases sublemma with x hx,

I repeat lines like the above very often.

[Julian Berman]

I think obtain is meant to be the shortcut for have + cases -- i.e. obtain \<x, hx\> := stuffinyourproof, with or without the explicit type if necessary

[Eric Rodriguez]

I can't remember whether obtain suuports the , syntax instead of := { ... } specifically, but otherwise yes

[Mario Carneiro]

it does

[Mario Carneiro]

you have to give the type if you want to pattern match though, obtain \<x, y\>, doesn't work

[Bart Michels]

Mario Carneiro said:

you have to give the type if you want to pattern match though, obtain \<x, y\>, doesn't work

I assume that's because the notation is ambiguous when you have nested constructors?

[Bart Michels]

Like if you want to obtain \<x, y, z\> of type (p \and q) \and (r \and s).

[Mario Carneiro]

No, it's always right associative in that sense. It's because it is ambiguous what we are destructing: it could be Exists.rec or and.rec or nat.rec

[Mario Carneiro]

you can't pattern match on something of unknown type: obtain <x, y> := _ is an error

[Bart Michels]

I'm not sure if I don't get it or if I am thinking the same. Say I have something of type (∃ n : ℕ, p n) ∧ (∃ n : ℕ, q n). How is this different from ((p ∧ q) ∧ r) ∧ ((s ∧ t) ∧ u) (except for the fact that the ns can be further destructed) ?

[Mario Carneiro]

you can't use exists.rec to destruct an element of the second type

[Bart Michels]

I mean, I agree that it's ambiguous, I am just surprised that you (seem to) say that it's not for something like (p ∧ q) ∧ (s ∧ t)

[Mario Carneiro]

the tactic has to decide what theorem to apply, and it needs the type to do that

[Mario Carneiro]

the brackets can be nested in different ways if you want to destruct stuff like (p ∧ q) ∧ (s ∧ t)

[Mario Carneiro]

you would need to use <<hp, hq>, <hs, ht>> to match that

[Mario Carneiro]

obtain doesn't try to be smart about associativity if you don't write the brackets correctly

[Mario Carneiro]

you can also use <<hp, hq>, hs, ht> in that case but that's just because the angle brackets are always interpreted as right associative

[Mario Carneiro]

<hp, hq, <hs, ht>> would not work

[Bart Michels]

But then I don't see why lean wouldn't know what to destruct. Can it not just look at the top-most symbol?

[Bart Michels]

When you say "It's because it is ambiguous what we are destructing:"

[Mario Carneiro]

because the top most symbol is ?m_1

[Mario Carneiro]

if the type is not known

[Mario Carneiro]

if you write obtain <x, y>, with literally no other information, how can it tell what you want to destruct?

[Mario Carneiro]

you can use obtain <x, y> : \exists n, P n, or obtain <x, y> := h, both of which provide a way to get the type

[Bart Michels]

Right, thanks. I was assuming that lean would derive the type from the {} block that follows.

[Mario Carneiro]

it can't use types from the future because after the , the tactic runs and it has to transition the tactic state to something such that the {} block will do something useful

[Bart Michels]

Got it, makes a lot of sense.

[Bart Michels]

Thanks!

[Martin Dvořák]

Martin Dvořák said:

Is there a more idiomatic way how to write clear_except, to delete everything but the goal?

I encountered it again. Is there any idiomatic way to write it? I kinda wanna signpost that I will show that the goal is tautological.

[Martin Dvořák]

What should I do instead of the following two lines?

have my_inequality_ := my_inequality,
tauto,

I want to "load" an existing private lemma into a local context in order to discharge the goal by tauto with its help?

[Alex J. Best]

Seems fine to me

[Martin Dvořák]

I'd rather do something like tauto [my_inequality] or perform tauto with library_search at the same time.
Or, is there a way to do what I did without needing to name the proposition again?

[Ruben Van de Velde]

You can use have := xxx which will call the local assumption this

[Martin Dvořák]

Is it idiomatic in Lean? I guess it is OK when I write have := my_inequality, on the penultimate line of the block (followed by a tactic that does not obtain this as an explicit argument).

[Alex J. Best]

Using this is fairly idiomatic, and some tactics like simpa using have special support for it even

[Martin Dvořák]

In my proofs, my block often ends with something like:

have almost_there := some_lemma some_parameter,
rw [some_transformation, other_transformation] at almost_there,
exact almost_there,

Is there a better way to write it?

[Eric Rodriguez]

rwa :)

[Martin Dvořák]

The line have almost_there := some_lemma some_parameter, has to stay, I guess.

[Yaël Dillies]

simpa only [some_transformation, other_transformation] using some_lemma some_parameter might or might not work in your situation.

[Yaël Dillies]

Is there any reason rwa [] using _ is not supported syntax?

[Martin Dvořák]

Eric Rodriguez said:

rwa :)

Isn't it a bit slower? I'd rather have it call exact [right side of rwa] than to walk through the local context.

[Yaël Dillies]

It's almost no difference, given that you will typically have less < 50 assumptions in context. And note that this is also (slightly) cheaper in tactic parsing.

[Eric Rodriguez]

Yaël Dillies said:

Is there any reason rwa [] using _ is not supported syntax?

Ooh this would be really nice

[Martin Dvořák]

Is it bad practice to reuse argument names between different functions / lemmata and have x of different type in different parts of your code?

[Johan Commelin]

Not necessarily. But having multiple xs` at the same time will be confusing.

[Martin Dvořák]

What about dsimp only [], in the middle of a proof?

[Kyle Miller]

Those are fine according to mathlib standards.

A small golf: dsimp only does the same thing as dsimp only []

[Kyle Miller]

One of the reasons dsimp only appears is that it's able to do a number of reductions that are necessary for further rewrites.

[Kyle Miller]

Even dsimp is allowed, because theoretically it transforms something into something definitionally equivalent, so it's not so bad fixing things if the simp set changes. (I usually still go for dsimp only [whatever the lemmas] when possible)

[Kyle Miller]

But, once you're done with a proof, it's worth checking if there are any dsimps (or unfolds) that you can remove. It can be surprising what's not necessary.

[Martin Dvořák]

I usually realize that dsimp and unfold cannot be removed.

[Martin Dvořák]

Is there a way how to replace the following two lines by a single command?

have is_it_in := congr_arg (λ l, 42 ∈ l) hyp,
dsimp only at is_it_in,

I wish there was a way to write the congr_arg expression in a way that will not require the beta reduction immediately after it.

[Ruben Van de Velde]

You could use have is_it_in : 42 \in a = 42 \in b := congr_arg .. (if I remembered congr_arg correctly)

[Martin Dvořák]

That's a bit too verbose but thanks.

[Ruben Van de Velde]

Oh, or maybe even have is_it_in : _ \in _ = _ \in _ := ...

[Alex J. Best]

You could use tactic#dsimp_result, for this example its still a bit verbose but it might be helpful in other cases

import data.set.basic
example (a b : set ℕ) (hyp : a = b) : false :=
begin
  have is_it_in, { dsimp_result { exact congr_arg (λ l, 42 ∈ l) hyp} },
end

[Kyle Miller]

Ext lemmas are good for these too

example (α : Type*) (s t : set α) (h : s = t) (x : α) : x ∈ s ↔ x ∈ t :=
begin
  have := set.ext_iff.mp h x,
  exact this
end

[Kyle Miller]

For submodules you can for example use docs#set_like.ext_iff since they tend to use the set_like interface

[Martin Dvořák]

I have the following block, which totally looks like a code smell, on six places in my code.

exfalso,
(...)
apply false_of_true_eq_false,
convert my_hyp.symm,
{
  rw [eq_iff_iff, true_iff],
  (...)
},
{
  rw [eq_iff_iff, false_iff],
  (...)
}

Is there a better way to write the same thing without significantly changing the decomposition?

[Anne Baanen]

If I read this right, the situation is that my_hyp : p = q, and you have a proof of p and a proof of ¬ q? I'd probably structure this as:

have : ¬ q :=
{ ... },
refine (this _).elim,
rw my_hyp,
-- Now prove `p`
{ ... }

[Anne Baanen]

Another option might be:

have hp : p,
{ ... },
have hnq : ¬ p,
{ rw my_hyp,
  -- Now prove `¬ q`
  ... },
contradiction

[Martin Dvořák]

Oh yes, thanks!
Is there also a way that doesn't require me to restate p and/or q?

[Martin Dvořák]

Motivation: I often work with propositions that take more than 100 characters to state. And I don't like boilerplate in my code.

[Anne Baanen]

The best I can figure out is the rather cryptic (mt (eq.mp my_hyp) _ _).elim

[Anne Baanen]

Or I guess absurd (eq.mp my_hyp _) _?

[Reid Barton]

Martin Dvořák said:

Motivation: I often work with propositions that take more than 100 characters to state

Some people would claim that this is the code smell

[Junyan Xu]

A bit late but this directly gives what you wanted:

import data.set.basic
example (a b : set ℕ) (hyp : a = b) : false :=
begin
  have := congr_arg ((∈) 42) hyp, /- this: 42 ∈ a = (42 ∈ b) -/
end