Zulip Chat Archive

Stream: general

Topic: calc iff


view this post on Zulip Patrick Massot (Dec 20 2018 at 09:30):

Is there anything we can do to get something like

example (p q r s : Prop) (h : p  q) (h' : q  r) (h'' : r  s) : p  s :=
λ hp, (calc p  q : h
...  r : h'
...  s : h'') hp

to work?

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:33):

I'm trying to please Johannes who doesn't like

example (p q r s : Prop) (h : p  q) (h' : q  r) (h'' : r  s) : p  s :=
begin
  rw h,
  rwa h'' at h',
end

which I admit is less transparent...

view this post on Zulip Johan Commelin (Dec 20 2018 at 09:36):

If only Prop were a category... then you could write

example (p q r s : Prop) (h : p  q) (h' : q  r) (h'' : r  s) : p  s :=
h.mp  h'  h''.mp

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:38):

Maybe I should say that the actual proof would rather look like

example (p q r s : Prop) (h : ...) (h' : ...) (h'' : ...) : p  s :=
λ hp, (calc p  q : by rw h
...  r : by h'
...  s : by rw h'') hp

view this post on Zulip Mario Carneiro (Dec 20 2018 at 09:52):

unfortunately no. Here's the best we can do:

abbreviation imp (p q : Prop) := p  q
infixr `→→`:25 := imp
@[trans] theorem imp_of_iff_of_imp {p q r : Prop}
  (h₁ : p  q) (h₂ : q →→ r) : p →→ r := h₂  h₁.1

@[trans] theorem iff_of_imp_of_imp {p q r : Prop}
  (h₁ : p →→ q) (h₂ : q  r) : p →→ r := h₂.1  h₁

example (p q r s : Prop) (h : p  q) (h' : q  r) (h'' : r  s) : p  s :=
λ hp, (calc p  q : h
... →→ r : h'
...  s : h'') hp

view this post on Zulip Mario Carneiro (Dec 20 2018 at 09:53):

If you replace →→ with the trans lemmas are rejected

view this post on Zulip Mario Carneiro (Dec 20 2018 at 09:54):

because is a bit magic for a binary operator

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:54):

This magic obstruction is what I suspected when I tried to define those trans lemmas

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:55):

Here is the best I could do in order to rewrite my continuity proof so that it looks like what I see on paper:

lemma uniform_continuous.continuous [uniform_space β] {f : α  β}
  (hf : uniform_continuous f) : continuous f :=
let ff := (λ p : α×α, (f p.1, f p.2)) in
continuous_iff_tendsto.mpr $ λ a,
have key : prod.mk (f a)  f = ff  prod.mk a, by ext x ; simp,
have map ff uniformity  uniformity, from hf,
have uniformity  comap ff uniformity, from map_le_iff_le_comap.1 this,
have comap (prod.mk a) (@uniformity α _)  (comap (prod.mk a) (comap ff uniformity)), from comap_mono this,
have nhds a  comap (ff  prod.mk a) uniformity, by rwa [comap_comap_comp, nhds_eq_comap_uniformity] at this,
have nhds a  comap (prod.mk (f a)  f) uniformity, by rwa key at this,
have nhds a  comap f (comap (prod.mk (f a)) uniformity), by rwa comap_comap_comp at this,
have nhds a  comap f (nhds (f a)), by rwa nhds_eq_comap_uniformity at this,
tendsto_iff_comap.2 this

view this post on Zulip Patrick Massot (Dec 20 2018 at 09:56):

How do you like that style?

view this post on Zulip Kenny Lau (Dec 20 2018 at 10:02):

too long

view this post on Zulip Patrick Massot (Dec 20 2018 at 10:07):

Variation:

lemma uniform_continuous.continuous [uniform_space β] {f : α  β}
  (hf : uniform_continuous f) : continuous f :=
let ff := (λ p : α×α, (f p.1, f p.2)) in
continuous_iff_tendsto.mpr $ λ a,
have key : prod.mk (f a)  f = ff  prod.mk a, by ext x ; simp,
have map ff uniformity  uniformity, from hf,
have uniformity  comap ff uniformity, from map_le_iff_le_comap.1 this,
have comap (prod.mk a) (@uniformity α _)  (comap (prod.mk a) (comap ff uniformity)), from comap_mono this,
let this := calc
nhds a  comap (ff  prod.mk a) uniformity : by rwa [comap_comap_comp, nhds_eq_comap_uniformity] at this
   ...  comap (prod.mk (f a)  f) uniformity : by simp[key, le_refl]
   ...  comap f (comap (prod.mk (f a)) uniformity) : by rw comap_comap_comp ; exact le_refl _
   ...  comap f (nhds (f a)) : by rw nhds_eq_comap_uniformity ; exact le_refl _  in
tendsto_iff_comap.2 this

view this post on Zulip Patrick Massot (Dec 20 2018 at 10:07):

It's really a pain that le_refl isn't inserted automatically

view this post on Zulip Kenny Lau (Dec 20 2018 at 10:09):

what's wrong with the current proof?

view this post on Zulip Sebastien Gouezel (Dec 20 2018 at 10:15):

I have added le_refl to the simp set in my mathlib. I will probably PR it one day, together with a lot of other stuff (but cut into atomic pieces, if this is the way we should do PRs), once (or if?) my two topology PRs are merged.

view this post on Zulip Patrick Massot (Dec 20 2018 at 10:16):

Kenny, the current proof is inelegant. Remember that only Lean thinks proofs are irrelevant

view this post on Zulip Kenny Lau (Dec 20 2018 at 10:17):

eh, I also think they're irrelevant

view this post on Zulip Johan Commelin (Dec 20 2018 at 10:20):

@Kevin Buzzard You've created little monsters :scream:. Clearly they need to be brought up in the ways of the old masters, who value the esthetics of a good proof, and whose proofs illuminate and inspire understanding.

view this post on Zulip Kevin Buzzard (Dec 20 2018 at 10:36):

Kids these days

view this post on Zulip Scott Morrison (Dec 20 2018 at 10:37):

... uphill both ways.

view this post on Zulip Johan Commelin (Dec 20 2018 at 11:00):

I will probably PR it one day, ... once (or if?) my two topology PRs are merged.

O.o... that doesn't sound good.

view this post on Zulip Kenny Lau (Dec 20 2018 at 11:02):

looks like he will PR it after Lean 4 has been released

view this post on Zulip Sebastien Gouezel (Dec 20 2018 at 11:04):

It's just that all my constructions build on these two PRs, so there is no way I can PR anything before those two are merged. But this does not prevent me of working steadily on my own branch, I have almost proved now that the Gromov-Hausdorff distance is a distance, which involves a lot of material (several thousands of line, I would say :)

view this post on Zulip Mario Carneiro (Dec 20 2018 at 11:19):

yeah okay. I've been putting it off because it's a big PR and I had to check it out and fiddle with stuff, but I will work on that now


Last updated: May 10 2021 at 00:31 UTC