Zulip Chat Archive

Stream: maths

Topic: Compact-open topology


view this post on Zulip Patrick Massot (Sep 24 2018 at 20:28):

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

view this post on Zulip Johannes Hölzl (Sep 24 2018 at 20:29):

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

view this post on Zulip Patrick Massot (Sep 24 2018 at 20:29):

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

view this post on Zulip Johannes Hölzl (Sep 24 2018 at 20:29):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 25 2018 at 11:27):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 25 2018 at 11:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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