Zulip Chat Archive

lemma fuck (f : equiv α β) (b) : f (f.inv_fun b) = b := f.right_inv b

lemma equiv.image_compl  (f : equiv α β) (s : set α) :
  f '' -s = -(f '' s) :=
begin
  apply subset.antisymm,
  { intros b b_in_image_compl,
    rcases b_in_image_compl with ⟨a, a_compl_s, f_a_b⟩,
    rw (equiv.apply_eq_iff_eq_inverse_apply f a b).1 f_a_b at a_compl_s,
    exact (mt (@mem_image_iff_of_inverse α β f.to_fun f.inv_fun b s f.left_inv f.right_inv).1)
a_compl_s },
  { intros,
    rw subset_def,
    intros b b_in_compl_image,
    apply (@mem_image_iff_of_inverse _ _ _ _ _ _ f.left_inv f.right_inv).2,
    have b_not_in_image := not_mem_of_mem_compl b_in_compl_image,
    rw set.mem_compl_eq,
    by_contra,
    have := mem_image_of_mem f a,
    rw fuck at this,
    finish }
end

Patrick Massot (Apr 01 2018 at 22:20):

But at least Lean was defeated

Mario Carneiro (Apr 01 2018 at 22:45):

Actually, I recommend not using f.right_inv in favor of the coercions

Kevin Buzzard (Apr 01 2018 at 22:57):

Another example of mathematicians getting very frustrated about how sometimes something which is "trivial in maths" can be hard in Lean.

Kevin Buzzard (Apr 01 2018 at 22:57):

In the long term these really need to be fixed somehow

Kevin Buzzard (Apr 01 2018 at 22:57):

if CS people want mathematicians to use the software.

Kevin Buzzard (Apr 01 2018 at 22:58):

And funnily enough, just the same thing happened to me with rw

Simon Hudon (Apr 01 2018 at 22:58):

I don't think it will ever happen that a mathematician using this or another theorem prover and will, 100% of the time, think "this is trivial" and have the prover confirm that (when the statement is true).

Kevin Buzzard (Apr 01 2018 at 22:58):

no, with exact

Kevin Buzzard (Apr 01 2018 at 22:59):

exact (congr_fun H HUigx) failed (type mismatch)

Kevin Buzzard (Apr 01 2018 at 22:59):

but have H2 := congr_fun H HUigx, exact H2 succeeded

Kevin Buzzard (Apr 01 2018 at 23:14):

@Simon Hudon I definitely think that this should happen in the future.

Kevin Buzzard (Apr 01 2018 at 23:14):

I am suggesting we meet you somewhere in the middle.

Kevin Buzzard (Apr 01 2018 at 23:15):

But if it doesn't happen then what hope is there for people to start adopting this computer viewpoint?

Kevin Buzzard (Apr 01 2018 at 23:15):

I think it's a matter of education on our part and adding lemmas on your part

Kevin Buzzard (Apr 01 2018 at 23:16):

We already saw this week how Chris couldn't prove something which was mathematically trivial, and then we found a framework for it and it became straightforward to prove

Simon Hudon (Apr 01 2018 at 23:19):

In that case, I think we're on the same page. In general, we probably need to build packages to better support undergraduate level mathematics and at least the basics of graduate level math.

Simon Hudon (Apr 01 2018 at 23:19):

Improving the automation and the documentation for building your own tactics will probably help you bridge the gap too.

Mario Carneiro (Apr 02 2018 at 01:26):

@Patrick Massot I wrote a proof of this that should appear in mathlib once it finishes checking. It's not nearly as complicated as you made it, and after appropriate sublemmas it's a one-liner:

theorem image_compl_subset {f : α → β} {s : set α} (H : injective f) :
  f '' -s ⊆ -(f '' s) :=
subset_compl_iff_disjoint.2 $ by simp [image_inter H]

theorem subset_image_compl {f : α → β} {s : set α} (H : surjective f) :
  -(f '' s) ⊆ f '' -s :=
compl_subset_iff_union.2 $
by rw ← image_union; simp [image_univ_of_surjective H]

theorem image_compl_eq {f : α → β} {s : set α} (H : bijective f) :
  f '' -s = -(f '' s) :=
subset.antisymm (image_compl_subset H.1) (subset_image_compl H.2)

Patrick Massot (Apr 02 2018 at 08:47):

Thank you very much @Mario Carneiro. I noticed that many support lemmas were missing. I'll use my crappy version in the mean time. But I'm still very much interested in any explanation why I could not avoid having this one lemma in order to rewrite.

Mario Carneiro (Apr 02 2018 at 08:49):

I am not quite sure what you were doing, but I think you wrote things in a non-idiomatic way (which is to say, not the way that mathlib is designed to help with), which made the proof more painful than it should have been

Mario Carneiro (Apr 02 2018 at 08:50):

The idiomatic version of your fuck lemma is f (f.symm x) = x (and it's called apply_inverse_apply)

Kenny Lau (Apr 02 2018 at 08:51):

rw fuck at this

Kenny Lau (Apr 02 2018 at 08:51):

i.e. fuck this

Patrick Massot (Apr 02 2018 at 08:54):

I'll tell you exactly what I was doing. First my brain absolutely refuses to think in this kind of situation, it's only filled with anger. Then I search for all lemmas in mathlib which seem vaguely related and try to apply them. But I got stuck with sorts of coercions issues, and stuff like rw refuses to rewrite etc, so I'm get even more upset. So of course the proof ends up not looking like what I would write on paper (of course in the beginning I would write nothing but then I'm able to write some proof on paper)