homeomorph.trans and calc

Stream: general

[Reid Barton]

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]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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

[Reid Barton]

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

[Reid Barton]

/me tests

[Yury G. Kudryashov]

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

[Bhavik Mehta]

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]

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]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Reid Barton]

this does not instill confidence

[Yury G. Kudryashov]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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

[Reid Barton]

Yes, I see

[Mario Carneiro]

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]

5 is for the three things and the two relations

[Yury G. Kudryashov]

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

[Reid Barton]

well, there is a simple solution...

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

hmm, I see

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

So we need to fix calc

[Yury G. Kudryashov]

Added lean#341

[Kevin Buzzard]

Smallest pseudoprime to base 2

[Yury G. Kudryashov]

@Mario Carneiro @Reid Barton Am I right that this is won't fix in Lean 3?

[Yury G. Kudryashov]

Does it work in Lean 4?