## Stream: general

### Topic: homeomorph.trans and calc

#### 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 ?
-/


#### 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

#### 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?

#### Yury G. Kudryashov (May 29 2020 at 23:54):

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

#### Reid Barton (May 29 2020 at 23:55):

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

/me tests

#### 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.

#### 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

#### 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


#### 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.

#### 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...

#### 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...

#### Mario Carneiro (May 30 2020 at 00:08):

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

#### 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

#### 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);


#### Reid Barton (May 30 2020 at 00:12):

this does not instill confidence

#### Yury G. Kudryashov (May 30 2020 at 00:13):

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

#### Reid Barton (May 30 2020 at 00:14):

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

#### Yury G. Kudryashov (May 30 2020 at 00:14):

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

Yes, I see

#### 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?

#### Reid Barton (May 30 2020 at 00:15):

5 is for the three things and the two relations

#### Yury G. Kudryashov (May 30 2020 at 00:16):

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

#### Reid Barton (May 30 2020 at 00:17):

well, there is a simple solution...

#### 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

#### 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

#### 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

#### Reid Barton (May 30 2020 at 00:40):

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

#### 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

hmm, I see

#### 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)

#### Mario Carneiro (May 30 2020 at 00:43):

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

#### 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

#### Mario Carneiro (May 30 2020 at 00:49):

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

#### 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

#### Scott Morrison (Jun 12 2020 at 09:32):

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

#### 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"?

#### Scott Morrison (Jun 12 2020 at 12:03):

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

#### 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

#### Yury G. Kudryashov (Jun 12 2020 at 15:25):

So we need to fix calc