## Stream: maths

### Topic: Compact-open topology

#### Johannes Hölzl (Sep 24 2018 at 20:29):

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

#### Patrick Massot (Sep 24 2018 at 20:29):

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

#### Johannes Hölzl (Sep 24 2018 at 20:29):

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

#### Patrick Massot (Sep 24 2018 at 20:34):

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 (Sep 24 2018 at 21:28):

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 (Sep 24 2018 at 21:30):

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 (Sep 25 2018 at 11:19):

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 (Sep 25 2018 at 11:22):

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

#### Patrick Massot (Sep 25 2018 at 11:27):

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 (Sep 25 2018 at 11:30):

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 (Sep 25 2018 at 11:31):

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 (Sep 25 2018 at 11:43):

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

#### Reid Barton (Sep 25 2018 at 12:21):

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 (Sep 25 2018 at 12:22):

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 (Sep 25 2018 at 12:22):

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 (Oct 01 2018 at 12:51):

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

Last updated: May 14 2021 at 19:21 UTC