# Zulip Chat Archive

## Stream: general

### Topic: calc iff

#### 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?

#### 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...

#### 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

#### 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

#### 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

#### Mario Carneiro (Dec 20 2018 at 09:53):

If you replace `→→`

with `→`

the trans lemmas are rejected

#### Mario Carneiro (Dec 20 2018 at 09:54):

because `→`

is a bit magic for a binary operator

#### Patrick Massot (Dec 20 2018 at 09:54):

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

#### 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

#### Patrick Massot (Dec 20 2018 at 09:56):

How do you like that style?

#### Kenny Lau (Dec 20 2018 at 10:02):

too long

#### 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

#### Patrick Massot (Dec 20 2018 at 10:07):

It's really a pain that `le_refl`

isn't inserted automatically

#### Kenny Lau (Dec 20 2018 at 10:09):

what's wrong with the current proof?

#### 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.

#### Patrick Massot (Dec 20 2018 at 10:16):

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

#### Kenny Lau (Dec 20 2018 at 10:17):

eh, I also think they're irrelevant

#### 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.

#### Kevin Buzzard (Dec 20 2018 at 10:36):

Kids these days

#### Scott Morrison (Dec 20 2018 at 10:37):

... uphill both ways.

#### 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.

#### Kenny Lau (Dec 20 2018 at 11:02):

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

#### 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 :)

#### 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