calc iff

Stream: general

[Patrick Massot]

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]

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]

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]

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]

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]

If you replace →→ with → the trans lemmas are rejected

[Mario Carneiro]

because → is a bit magic for a binary operator

[Patrick Massot]

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

[Patrick Massot]

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]

How do you like that style?

[Kenny Lau]

too long

[Patrick Massot]

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]

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

[Kenny Lau]

what's wrong with the current proof?

[Sebastien Gouezel]

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]

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

[Kenny Lau]

eh, I also think they're irrelevant

[Johan Commelin]

@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]

Kids these days

[Scott Morrison]

... uphill both ways.

[Johan Commelin]

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]

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

[Sebastien Gouezel]

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]

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