calc with `≃*`

Stream: general

[Joachim Breitner]

I’d really like to do something like this:

example (a b c : Type*) [group a] [group b] [group c] : a ≃* c :=
begin
  calc a ≃* b : sorry
     ... ≃* c : sorry
end

but I get

type mismatch at application
  mul_equiv.trans
term
  a
has type
  Type ? : Type (?+1)
but is expected to have type
  has_mul ?m_1 : Type ?
state:
a : Type ?,
b : Type ?,
c : Type ?,
_inst_1 : group a,
_inst_2 : group b,
_inst_3 : group c
⊢ a ≃* c

Is there a way to have calculations with ≃*?

[Yaël Dillies]

Have a look through the docs#mul_equiv API to see whether the relevant definitions have been marked @[trans], although it looks like the error is elsewhere

[Yaël Dillies]

Indeed, docs#mul_equiv.trans is marked @[trans] (although it's not written in the docs, cc @Bryan Gin-ge Chen), so I suspect it's a bug in calc or in trans that turn instance arguments into explicit ones, or something of this vein.

[Reid Barton]

There is a known issue with calc not working when the "relation" (here ≃*) has more arguments than = would have--here those pesky has_mul arguments.

[Reid Barton]

e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/calc.20for.20linear.20equivs/near/240337990

[Reid Barton]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/homeomorph.2Etrans.20and.20calc/near/199225731

[Bryan Gin-ge Chen]

Yaël Dillies said:

Indeed, docs#mul_equiv.trans is marked @[trans] (although it's not written in the docs, cc Bryan Gin-ge Chen), ...

Regarding trans not showing up in the docs, doc-gen only includes attributes from a hard-coded list. I'm not sure what the criteria are for inclusion, but maybe a PR adding more would be accepted? cc: @Rob Lewis

[Heather Macbeth]

Reid Barton said:

There is a known issue with calc not working when the "relation" (here ≃*) has more arguments than = would have--here those pesky has_mul arguments.

That's interesting, because I've definitely got calc to work with the relation docs#int.modeq. Eg here

[Gabriel Ebner]

It's not so much the number of arguments, but what the last five arguments are. For calc, these need to be a, b, c, h₁ : a ≃ b, h₂ : b ≼ c, in that order.

[Reid Barton]

Ah... but that's not very workable when there are type class constraints on a b c

[Eric Rodriguez]

is that the behaviour in Lean4?

[Yaël Dillies]

Oooh, so that's why trans sometimes outputs "not enough arguments".

[Eric Rodriguez]

@Gabriel Ebner is this similarly the case for @[symm] and @[refl]? I'm currently preparing a PR to make the most of what's possible, and I'm wondering if I should fix those at the same time anyways

[Gabriel Ebner]

calc only uses trans, so this specific problem won't happen with symm or refl.

[Eric Rodriguez]

#12860

[Yaël Dillies]

Could we make calc more robust instead?

[Eric Rodriguez]

for sure, that's the ideal solution, but this is a nice stop-gap

[Joachim Breitner]

What would be ways to fix that? An (optional) attribute to trans that indicates which argument positions correspond to the expected 5 arguments maybe? (Blunt, I agree)

Or make the command ignore type class arguments?

Or is calc too low level to cater for such specific whims?

[Eric Rodriguez]

I would hope that ignoring type-class arguments would work, but who knows...

[Yaël Dillies]

Why can't calc infer a, b, c from a ≃ b, b ≼ c?

[Sebastian Ullrich]

Eric Rodriguez said:

is that the behaviour in Lean4?

Lean 4 uses a typeclass Trans instead of an attribute, so this issue should not apply

[Eric Wieser]

Elaborating on @Yael's comment, I'd hope calc could work it out from lemmas of the shape... (hab : type_one ... a b) (hbc : type_two ... b c) : type_three ... a c, and unify to work out a, b, and c.

[Yaël Dillies]

I suspect the answer is that some trans lemmas are rather ... (hab : type_one ... a b ...) (hbc : type_two ... b c ...) : type_three ... a c ...

[Eric Wieser]

Do we actually have any of those that can't be reordered, and are currently supported by calc today?

[Eric Wieser]

My guess would be that there are far fewer of those than the type that we're asking for in this thread.

[Eric Rodriguez]

there's a lottt of different forms, some of the ones I rememeber were ≪ᵥ, some of the model ones, and equality_mod_filters

[Eric Rodriguez]

ok, now I'm confused: why doesn't this work on the branch above?

import analysis.asymptotics.asymptotic_equivalent

variables {α β γ δ : Type*}

section is_equivalent

open_locale asymptotics

#check @asymptotics.is_equivalent.trans

example {l : filter α} {u v w : α → β} [normed_group β]
  (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w :=
calc u ~[l] v : huv
   ... ~[l] w : hvw

end is_equivalent

[Kyle Miller]

Joachim Breitner said:

An (optional) attribute to trans that indicates which argument positions correspond to the expected 5 arguments maybe?

I wonder if we can get away with giving trans a single optional numeric argument corresponding to the position of "b". Example:

#check @mul_equiv.trans
-- Π {M : Type u_2} {N : Type u_3} {P : Type u_4}
--   [_inst_1 : has_mul M] [_inst_2 : has_mul N] [_inst_3 : has_mul P],
--   M ≃* N → N ≃* P → M ≃* P

set_attribute [trans 2] mul_equiv.trans

I haven't looked at the actual underlying code to see if this would work though.

[Joachim Breitner]

I'm curious: why would just b be needed?

[Yaël Dillies]

That's because a appears in the first hypothesis where b appears in the second, and c appears in the second hypothesis where b appears in the first.

[Yaël Dillies]

Oh wait, I am completely off.

[Joachim Breitner]

Why does calc when have to instantiate these arguments (a, b, c) explicitly? Doesn't it always have the type of h1 and h2 explicitly given in the calc syntax, and can pass that as a type annotation?

[Yaël Dillies]

But how do you figure out a, b, c from the hypotheses? In simple cases, it's straightforward. In others, I don't really know.

[Eric Rodriguez]

Joachim Breitner said:

Why does calc when have to instantiate these arguments (a, b, c) explicitly? Doesn't it always have the type of h1 and h2 explicitly given in the calc syntax, and can pass that as a type annotation?

This was my thought, too; the current pproach doesn't even work for some interesting types /cf my mwe)

[Eric Wieser]

Yaël Dillies said:

But how do you figure out a, b, c from the hypotheses? In simple cases, it's straightforward. In others, I don't really know.

Can't we require that the type of hab : a ~ b end in the arguments a b (eg be some_rel _ _ _ a b)? Are there any examples where this isn't possible?

[Yaël Dillies]

I agree that this sounds like a reasonable restriction but I'm sure people can come up with counterexamples.

[Eric Rodriguez]

ring_equivs

[Eric Wieser]

Oh, whoops

[Jannis Limperg]

I haven't read through this thread in detail, but if the problem is that calc can't reliably figure out the relation, perhaps users could just give it explicitly: calc[R] x R y : p ....

[Eric Rodriguez]

but the whole point of calc is that you can mix relations, for example if you wanted x ∈ A ∪ B you can currently write:

import field_theory.abel_ruffini

example {α} (A B : set α) (a : α) (h : a ∈ A) : a ∈ A ∪ B :=
calc a ∈ A : h
   ... ⊆ A ∪ B : by simp

[Kyle Miller]

Joachim Breitner said:

I'm curious: why would just b be needed?

I'd made a wrong guess about how it worked based on the existence of tactic#transitivity

Here's actually how the transitivity foo tactic works:

1. Look at the target, get the head of the application (e.g., for eq a b that'd be eq), require that it be a constant.
2. Look for a trans lemma in the environment for that constant.
3. Basically apply that lemma using the new_goals.non_dep_only strategy.
4. Use docs#environment.relation_info to get the arity of the relation and the indices into the arguments list for the "lhs" and "rhs" of the relation.
5. For the first goal produced by applying the trans lemma, unify the "rhs" of it with foo.

The docstring for relation_info says something about things being "marked as relations." Haven't dug into that yet.

[Kyle Miller]

It looks like the "lhs" and "rhs" of a relation are always the last two explicit arguments, and the last two arguments to a trans lemma must be relation-like (they don't seem to be involved in the relation registration system -- not sure if that's a bug). relation_manager.cpp

Side question: what is a subst lemma? It doesn't seem like it has any use -- was this meant to be a way to implement relation-based rewriting?

[Kyle Miller]

Here's where how @Gabriel Ebner said calc works actually happens.

It takes the two relations being chained together and looks in the trans database for that pair to find a relevant trans lemma (note: there are two ways this database is queried: transitivity uses the relation constructed by the trans lemma, but calc uses the last two arguments to the trans lemma). If there is such a lemma, then trans_it in the linked code is truthy. Then the last five arguments to the trans lemma are filled in exactly as @Gabriel Ebner said: a, b, c, proof of first relation involving a and b, proof of second relation involving b and c.

[Kyle Miller]

Joachim Breitner said:

Why does calc when have to instantiate these arguments (a, b, c) explicitly? Doesn't it always have the type of h1 and h2 explicitly given in the calc syntax, and can pass that as a type annotation?

Given that the relation manager knows what the "lhs" and "rhs" of each relation involved is, it seems plausible to me that a, b, and c can be set indirectly through the types of h1 and h2.

(I haven't looked at @Eric Rodriguez's MWE yet, or what it's an MWE of -- is it that you'd expect calc to work given that it seemingly meets the constraints?)

[Eric Rodriguez]

yeah, pretty much, but it errops out. I assume because it's a relation of the sort a =[f] b

[Jannis Limperg]

Eric Rodriguez said:

but the whole point of calc is that you can mix relations

Then the annotation could be used as a hint:

calc[R] x R y : ...
      ... S z : ...

Lean could look at the R in square brackets to figure out which arguments are considered the left and right element, while using the current heuristic for S. Not sure whether this is a good idea, but it seems possible to me.

[Yaël Dillies]

Btw, how does calc handle ≥? Does it literally use docs#ge_trans or is there special support?

[Eric Rodriguez]

I would imagine it uses that, yes

[Kevin Buzzard]

Heather Macbeth said:

Reid Barton said:

There is a known issue with calc not working when the "relation" (here ≃*) has more arguments than = would have--here those pesky has_mul arguments.

That's interesting, because I've definitely got calc to work with the relation docs#int.modeq. Eg here

but but but... https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/calc.20ZMOD.20bug/near/272408274 I think you got lucky because you never used consecutive ZMODs ?

[Kyle Miller]

Yaël Dillies said:

Btw, how does calc handle ≥? Does it literally use docs#ge_trans or is there special support?

The only special support for anything that calc seems to have is for eq (saving us from having to write a bunch of silly trans lemmas).

The way calc appears to work is that it takes pairs of consecutive relations in the calc (say ≥ and ≥, or ≥ and >, or what have you) then looks for a trans lemma that takes that pair of relations. Whichever trans lemma matches then determines what the resulting composite relation is -- for example docs#ge_trans results in the ≥ relation.

[Kyle Miller]

@Eric Rodriguez It looks like the problem with your example is that the relation isn't following the correct specification. The related terms have to be the last two explicit arguments, but the filter is coming last: https://github.com/leanprover-community/mathlib/blob/d586195418d55d8d56c2d412c35bffd9a516a3c5/src/analysis/asymptotics/asymptotic_equivalent.lean#L63

[Kyle Miller]

ZMOD seems to work fine because the underlying relation is modeq n a b, that is, a and b come last.

lemma foo (a b c d n : ℤ)
  (h1 : a ≡ b [ZMOD n]) (h2 : b ≡ c [ZMOD n]) (h3 : c ≡ d [ZMOD n]) :
  a ≡ d [ZMOD n] :=
calc a ≡ b [ZMOD n] : h1
   ... ≡ c [ZMOD n] : h2
   ... ≡ d [ZMOD n] : h3

(Not sure what's going on with the metavariable problem in @Kevin Buzzard's examples.)

[Kyle Miller]

I'm going to hazard a guess that calc just isn't unifying anything but the last two arguments of the relation.

[Kyle Miller]

Oh, yep, that's it:

lemma foo (a b c d n : ℤ)
  (h1 : a ≡ b [ZMOD n]) (h2 : b ≡ c [ZMOD n]) (h3 : c ≡ d [ZMOD n]) :
  a ≡ d [ZMOD n] :=
calc a ≡ b [ZMOD 37] : h1
   ... ≡ c [ZMOD 22] : h2
   ... ≡ d [ZMOD 482] : h3

[Eric Rodriguez]

Kyle Miller said:

Eric Rodriguez It looks like the problem with your example is that the relation isn't following the correct specification. The related terms have to be the last two explicit arguments, but the filter is coming last: https://github.com/leanprover-community/mathlib/blob/d586195418d55d8d56c2d412c35bffd9a516a3c5/src/analysis/asymptotics/asymptotic_equivalent.lean#L63

On my branch it does

[Kyle Miller]

@Eric Rodriguez I don't have a very good Lean environment on the computer I have with me -- what's the specific error you're seeing?

[Kyle Miller]

(My guess is "failed to synthesize type class instance for normed_group ?m_1")

[Eric Rodriguez]

Kyle Miller said:

(My guess is "failed to synthesize type class instance for normed_group ?m_1")

nope:

image.png

[Eric Rodriguez]

i'll push that to the branch so everyone can see

[Eric Rodriguez]

OK, so I changed things to fully work properly. There are some @[trans] tagged relations that don't follow the rules and I didn't want to change for argument order - if anyone has strong opinions on these, let me know:

• docs#turing.evals_to_in_time - the spelling is really nice, but I don't know the TM side of mathlib at all. I left a note to those who do do it there.
• docs#set.eq_on (this one I kind of wanted to change, as s.eq_on seems like a reasonable spelling to me! but I feel like the nicest spelling would be f.eq g on s, and that's not possible (I don't think?)
• docs#continuous_map.homotopic_with, docs#continuous_map.homotopic_rel: I'm torn on these.

[Joachim Breitner]

To avoid confusion: what works fully now? calc with ≃*?

[Eric Rodriguez]

nope, that's still prevented by the issue with needing []s. there's currently two requirements on calc:

• the relation type's two last _explicit_ arguments must be the two things being related (that's what I'm talking about above): for example, the issue I had above is that a =[f] b used to be a type of the form @filter_eq a b f or whatever.
• the last 5 arguments (not only explicit) of the @[trans] method must be equal to a, b, c, R a b, R b c. This is what's holding up ≃*, and requires a change to core.

[Kyle Miller]

That "last two explicit argument" rule for relations seems to be shared by everything that uses the relation manager, so refl, symm, trans, the corresponding tactics, and calc. So, Eric's work on hammering out argument order for relations at least improves all these tactics.

calc needs to be fixed (as this example shows). There's a subtle issue that, for applications such as mul_equiv, we want to make sure a, b, and c get unified soon enough that typeclass inference involving them is able to succeed. Maybe all it needs to do is fill in the last three explicit arguments before the last two arguments, rather than the last three such.

[Eric Rodriguez]

is this true? this example compiles, and it's one of the examples above that explicitly haven't had their arg order changed:

import computability.tm_computable

example : turing.evals_to_in_time (@some ℕ) 0 ↑0 0 :=
begin
  refl
end

[Eric Rodriguez]

symmetry does fail, though

[Eric Rodriguez]

oh wait, that's not a symmetric relation :face_palm:

[Eric Rodriguez]

import topology.homotopy.basic

example {X : Type} {Y : Type} [topological_space X] [topological_space Y] (f₀ f₁ : C(X, Y))
        (P : C(X, Y) → Prop) : f₀.homotopic_with f₁ P :=
begin
  symmetry,
end

[Eric Rodriguez]

this one does work, though