Zulip Chat Archive

Stream: general

Topic: homeomorph.trans and calc


view this post on Zulip Reid Barton (May 29 2020 at 23:50):

Is there some way to make calc work with homeomorph? MWE:

import topology.homeomorph

local attribute [trans] homeomorph.trans

def sq {α : Type} [topological_space α] (h : α ≃ₜ α) : α ≃ₜ α :=
calc α ≃ₜ α : h
  ...  ≃ₜ α : h
/-
type mismatch at application
  homeomorph.trans
term
  α
has type
  Type : Type 1
but is expected to have type
  topological_space ?m_1 : Type ?
-/

view this post on Zulip Bhavik Mehta (May 29 2020 at 23:54):

I wanted something analogous with equiv today as well, would be great if something like this worked

view this post on Zulip Reid Barton (May 29 2020 at 23:54):

With equiv it does work though (just tested). Something about calc not supplying the right number of arguments to trans?

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 23:54):

It seems that @[trans] doesn't work with non-explicit after explicit ones.

view this post on Zulip Reid Barton (May 29 2020 at 23:55):

That doesn't occur in homeomorph.trans though. Are the [] arguments confusing it?

view this post on Zulip Reid Barton (May 29 2020 at 23:55):

/me tests

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 23:56):

I mean that homeomorph α β is actually @homeomorph α β [topological_space α] [topological_space β], and probably trans can't deal with this.

view this post on Zulip Bhavik Mehta (May 29 2020 at 23:56):

Reid Barton said:

With equiv it does work though (just tested). Something about calc not supplying the right number of arguments to trans?

Oh! Good to know, I should've actually tried

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 23:56):

Here is the error with pp.all:

9:3: type mismatch at application
  @homeomorph.trans.{?l_1 ?l_2 ?l_3} ?m_4 ?m_5 ?m_6 α
term
  α
has type
  Type : Type 1
but is expected to have type
  topological_space.{?l_1} ?m_2 : Type ?l_1

view this post on Zulip Reid Barton (May 29 2020 at 23:57):

I tried making a copy of homeomorph.trans with all the [] arguments turned to {} and it didn't help.

view this post on Zulip Reid Barton (May 29 2020 at 23:59):

I've used calc successfully with a pretty complicated [trans] lemma type before and it worked, so not sure what is going on, or how calc decides how to build the application...

view this post on Zulip Reid Barton (May 30 2020 at 00:05):

I feel like I must be doing something very dumb, but I can't figure out what...

view this post on Zulip Mario Carneiro (May 30 2020 at 00:08):

That bad application looks like something that has to be fixed in C++

view this post on Zulip Reid Barton (May 30 2020 at 00:09):

What confuses me is that this [trans] lemma works fine: https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/data/bij_on.lean#L67

view this post on Zulip Reid Barton (May 30 2020 at 00:11):

        expr trans    = mk_op_fn(p, trans_it->m_name, trans_it->m_num_args-5, pos);

view this post on Zulip Reid Barton (May 30 2020 at 00:12):

this does not instill confidence

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 00:13):

Bij_on.trans has three arguments "objects that are related" right before the explicit arguments.

view this post on Zulip Reid Barton (May 30 2020 at 00:14):

Now I'm wondering if the issue is actually with the type of homeomorph

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 00:14):

While homeomorph.trans has three arguments [topological_space ...] between types and explicit args.

view this post on Zulip Reid Barton (May 30 2020 at 00:15):

Yes, I see

view this post on Zulip Mario Carneiro (May 30 2020 at 00:15):

I'm reading the source of calc now. Did you know that when you write a -> b as an expression in a calc proof, it gets turned into implies a b?

view this post on Zulip Reid Barton (May 30 2020 at 00:15):

5 is for the three things and the two relations

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 00:16):

But for homeomorph we have extra args between three and two.

view this post on Zulip Reid Barton (May 30 2020 at 00:17):

well, there is a simple solution...

view this post on Zulip Mario Carneiro (May 30 2020 at 00:35):

I think what this should do is unify the trans lemma against op _ a b -> op' _ b c -> op'' _ a c where the op's are specified by the trans lemma and there are op.n_args-2 _ for each op

view this post on Zulip Reid Barton (May 30 2020 at 00:38):

Even this won't actually work here because in this case op also has extra implicit arguments that come after a b

view this post on Zulip Mario Carneiro (May 30 2020 at 00:40):

in that case you will have to elaborate the pre-expression op a b or use mk_app to build those parts

view this post on Zulip Reid Barton (May 30 2020 at 00:40):

What if we just apply the trans lemma to the two proofs as a pexpr?

view this post on Zulip Mario Carneiro (May 30 2020 at 00:41):

because the typing part of the calc also provides some information, about the form of the subgoals that needs to be used both outside the calc block and to type the proofs

view this post on Zulip Reid Barton (May 30 2020 at 00:42):

hmm, I see

view this post on Zulip Mario Carneiro (May 30 2020 at 00:42):

that is, it is like (trans_lemma (proof1 : op a b) (proof2 : op b c) : op a c)

view this post on Zulip Mario Carneiro (May 30 2020 at 00:43):

I'm not sure if those are ascriptions or actual identity functions

view this post on Zulip Mario Carneiro (May 30 2020 at 00:48):

oh weird. There is an actual identity function inserted if it is a 1-step calc, i.e. calc a = b : proof is the same as show a = b, from proof, but not if there are two or more steps. I guess because the transitivity lemma is invoked with a and b as arguments it is considered unnecessary to add an extra show

view this post on Zulip Mario Carneiro (May 30 2020 at 00:49):

maybe I should start using calc a = b: rfl for golfing :P

view this post on Zulip Mario Carneiro (May 30 2020 at 00:55):

calc should really be a tactic. I'm sure Sebastian would do a better job of it, but I should look into something like user_notation for being able to call tactics without by and allowing metavariables to escape the by block, so that you can implement calc as a tactic. I also think it would enable more elaborate notations for tactics in term mode

view this post on Zulip Scott Morrison (Jun 12 2020 at 09:32):

Hrm, I just encountered wanting calc for ≃+, and it not working. :-(

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 10:36):

As in "nobody tagged the transitivity result with trans, or as in "I tagged it with trans and it still didn't work"?

view this post on Zulip Scott Morrison (Jun 12 2020 at 12:03):

Good point. It had @[trans] all along, but chokes on the typeclass arguments.

view this post on Zulip Yury G. Kudryashov (Jun 12 2020 at 15:25):

As in trans makes some assumptions about arguments of trans lemmas and we can't make homeomorph.trans satisfy these assumptions

view this post on Zulip Yury G. Kudryashov (Jun 12 2020 at 15:25):

So we need to fix calc

view this post on Zulip Yury G. Kudryashov (Jun 16 2020 at 17:23):

Added lean#341

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 17:36):

Smallest pseudoprime to base 2


Last updated: May 15 2021 at 00:39 UTC