new writing technique

Stream: general

[Patrick Massot]

I've found a nice new trick to write obfuscated^W concise code:

lemma chart_chart_inv {φ : chart X} {x : φ.target} : x ∈ φ.range → φ (φ.inv x) = x
| ⟨y, ⟨y_in, φ_y⟩⟩ := inv_fun_on_eq ⟨y, ⟨y_in, φ_y⟩⟩

[Patrick Massot]

Why not writing assume H, inv_fun_on_eq H? Well, the sequences of pointy brackets in the pattern matching and body don't represent the same (anonymized) constructor.

[Simon Hudon]

Would it make you happy if Lean gave you a warning about using the anonymous constructors in disjoint expressions to build expressions of different types?

[Patrick Massot]

I don't know.

[Patrick Massot]

I'm not complaining about anything.

[Patrick Massot]

I do think that if I read this code later than a few days away from now, I'll be thinking WTF?

[Simon Hudon]

Sorry, I'm highjacking your conversation. I've been saying for a while that we need a linter tool to find dubious code

[Simon Hudon]

And I'm wondering how to define "dubious code"

[Chris Hughes]

Maybe the type of the two ⟨y, ⟨y_in, φ_y⟩⟩s is different.

[Simon Hudon]

Yes, that's what Patrick was pointing out

[Patrick Massot]

Here is a minimized example for the curious readers:

import data.set.basic
open set

example (α β : Type) (s : set α) (f : α → β) (b) (h : ∃a∈s, f a = b) : b ∈ f '' s  :=
begin
  -- rw mem_image, exact h,
  -- rw mem_image_eq, exact h,
  rw mem_image,
  rcases h with ⟨a, ⟨b, c⟩⟩,
  exact ⟨a, ⟨b, c⟩⟩
end

The two commented out lines are nice tries that don't work.

[Patrick Massot]

And it's in tactic mode so you can see everything

[Patrick Massot]

@Mario Carneiro Is there a variation on mem_image that I'm missing here?

[Mario Carneiro]

I see nothing wrong with chart_inv_inv

[Mario Carneiro]

example (α β : Type) (s : set α) (f : α → β) (b) (h : ∃a∈s, f a = b) : b ∈ f '' s  :=
by simpa using h

[Patrick Massot]

How does this work? What is simpa magically doing here? I know mem_image is a simp lemma. And then?

[Chris Hughes]

∃ (H : a ∈ s), f a = b ==> a ∈ s ∧ f a = b exists_prop