Compact-open topology

Stream: maths

[Patrick Massot]

I see @Johannes Hölzl merged https://github.com/leanprover/mathlib/pull/368 before Reid answered my comments. Was this done on purpose?

[Johannes Hölzl]

ah, no. I was focusing on the first comment and forgot the other ones...

[Patrick Massot]

I'm not saying they are crucial comments, but I was still suprised

[Johannes Hölzl]

but I think also that ev could be changed to a coe.

[Patrick Massot]

I rather meant that C(α, β) could have a coe to fun, so that the definition of ev becomes def ev : C(α, β) × α → β := λ p, p.1 p.2, or the maybe more readable def ev : C(α, β) × α → β | (f, x) := f x

[Reid Barton]

Patrick, regarding your very last comment, I've had too many bad experiences writing proofs about things defined by matching, and so I never use pattern matching in definitions in simple cases now. I do regret the loss of readability though. That's why I suggested lazy matching (terminology borrowed from Haskell), so you could write | ~(f, x) := f x for := λ p, p.1 p.2.

[Reid Barton]

As for the PR, I'm happy to either pretend it is still open and reply to comments by making a new PR, or just leave it as-is for now, until someone gets annoyed at the name ev

[Patrick Massot]

I don't understand the lazy matching discussion. Both the following definition work:

def f : ℕ × ℕ → ℕ := λ ⟨x, y⟩, x+y

def g : ℕ × ℕ → ℕ | (x, y) := x+y

What would you like that doesn't work?

[Chris Hughes]

I think he wants to use notation similar to that to define f to be λ x, x.1 + x.2

[Patrick Massot]

But this is already this:

def f  : ℕ × ℕ → ℕ := λ ⟨x, y⟩, x + y
def f' : ℕ × ℕ → ℕ := λ x,  x.1 + x.2

example : f = f' :=
begin
  ext x,
  cases x,
  refl
end

[Chris Hughes]

He wants to use nice notation for it, the .1 stuff is better for definitional reduction, but λ ⟨x, y⟩, x + y looks nicer.

[Johannes Hölzl]

The problem happens when you use coercion, e.g. from a subtype. When you use matching:

definition f : subtype p -> A | ⟨a, ha⟩ := ⟨op a, ha...⟩
lemma coe_f : coe (f a) = op (coe a) := by cases a; refl

while using projection gives us a rfl proof:

definition f (x : subtype p) := ⟨op x.1, x.2...⟩
lemma coe_f : coe (f a) = op (coe a) := rfl

[Patrick Massot]

Indeed I was suprised that my f = f' is not rfl

[Reid Barton]

More generally, when you have a function f : S -> T and both S and T are structures, it's better (when possible) to have T.mk ... as the outer structure of f, and do the pattern matching on S inside, rather than having S.rec_on as the outer structure and constructing T inside.

[Reid Barton]

Then if you compose with another such function g : T -> U, and you form g (f s), the places where g pattern matches on its argument will reduce with the T.mk which is the outer structure of f s.

[Reid Barton]

If you do it the other way then g (f s) will look like T.rec_on (S.rec_on s ...) ..., and you won't be able to make any progress unless s is already a constructor.

[Johannes Hölzl]

FYI: I added a proper constant for the type of continuous maps and renamed the theory to continuous_map.