requesting help on mathlib4#674

Stream: mathlib4

[Arien Malec]

I've got mathlib4#674 to the point where the obvious failures are addressed, and have cleaned up docu, etc. Now on the hard stuff.

In particular:

The failures in theorem option_subtype are those where more experienced eyes would solve the failures much faster than I.

1. Lean 4 seems confused by the Subtype typing
2. We have a Lean 3 coe in the house

[Arien Malec]

@Eric Wieser -- looks like you were the original author?

[Moritz Doll]

You might want to turn off autoimplicits, they can be a huge pain when dealing with coe.
The first error you get is annoying, there seems to be an issue with EquivLike

[Arien Malec]

Thanks for the point fix!

[Kevin Buzzard]

So the first error in the file right now is this: in Lean 3 this works:

import logic.equiv.defs

example (α β : Type) (p : (α ≃ β) → Prop) (s : {e : α ≃ β // p e}) (a : α) : β := s a -- works

because we have docs#equiv.has_coe_to_fun in mathlib and docs#coe_subtype, docs#coe_fn_trans in core Lean 3, so s has a coercion to function. I am still a bit lost about how coercions work in Lean 4, but what I do know is that right now this doesn't work in Lean 4:

import Mathlib.Logic.Equiv.Defs

example (α β : Type) (p : (α ≃ β) → Prop) (s : {e : α ≃ β // p e}) (a : α) : β := s a -- function expected

How am I supposed to fix it?

[Arien Malec]

Thanks @Kevin Buzzard --

I think that's a more #mwe than this:

import Mathlib.Data.Subtype
import Mathlib.Logic.Equiv.Defs

variable {α β : Type _}

def option_subtype [DecidableEq β] (x : β) :
    { e : Option α ≃ β // e none = x } ≃ (α ≃ { y : β // y ≠ x }) where
  toFun e :=
    { toFun :=
        fun a => ⟨e a, sorry⟩, --function expected at e term has type{ e // Equiv.toFun e none = x }
      invFun := sorry,
      left_inv := sorry,
      right_inv := sorry}
  invFun e := sorry
  left_inv e := sorry
  right_inv e := sorry

[Kevin Buzzard]

What I'm unclear about is whether we're supposed to be just copying how it worked in Lean 3, or using these things like coeHead and coeTail which I don't understand properly, or just writing out the coercions explicitly, or...

[Scott Morrison]

Oh! logic.equiv.defs is horribly broken, and gets fixed in mathlib4#631. So unless you're basing off that expect everything about coercions and equivs to be wrong.

[Kevin Buzzard]

OK I'll try merging! By the way I just reviewed the logic.equiv.defs PR.

[Scott Morrison]

(It's actually porting logic.equiv.basic; logic.equiv.defs was done earlier, but with some mistakes handling coercions)

[Kevin Buzzard]

OK I've merged the current state of logic_equiv_basic (the mathlib4#631 branch) into mathlib4#674 and I still have

import Mathlib.Logic.Equiv.Defs

example (α β : Type) (p : (α ≃ β) → Prop) (s : {e : α ≃ β // p e}) (a : α) : β := s a
-- error
-- function expected

[Scott Morrison]

Oh, didn't Gabriel say something about this yesterday? What happens with (s : \a \equiv \b) a?

[Kevin Buzzard]

This fixes the problem in mathlib4#674 -- what I don't understand is whether this is what I'm supposed to be doing. Mathlib3 is doing one coercion to function here, and this fix is not syntactically the same because it's doing two coercions.

[Kevin Buzzard]

However if that transitive coercion is literally going to be unfolded in Lean 4 into the two coercions then I guess it will be syntactically the same in Lean 4, so maybe this solution is fine?

[Kevin Buzzard]

Ok I'm currently working on this branch, assuming that this is the fix we want

[Scott Morrison]

Sorry, I wasn't able to find the message I half-remembered. @Gabriel Ebner, do you have a moment to advise Kevin here?

[Kevin Buzzard]

OK so the good news is that mathlib4#674 is compiling (it depends on mathlib4#631 ; the actual diff is just Mathlib.Logic.Equiv.Option). The bad news is

set_option maxHeartbeats 600000 -- next def times out with default heartbeats (200000)

on line 165 of Mathlib.Logic.Equiv.Option, just before option_subtype. In Lean 3 the entire file compiles very quickly; in Lean 4 this one declaration takes about 8 seconds on my machine (I don't understand how to work the profiler in Lean 4). Could this be because the coercion from {e : alpha \equiv beta // p e} to alpha -> beta is packaged up in Lean 3 and is unpackaged into two coercions in Lean 4 with my current approach?

[Kevin Buzzard]

Even if I squeeze all the simps it still takes several seconds:

set_option maxHeartbeats 600000 -- next def times out with default heartbeats (200000)
set_option profiler true
/-- Equivalences between `Option α` and `β` that send `none` to `x` are equivalent to
equivalences between `α` and `{y : β // y ≠ x}`. -/
def option_subtype [DecidableEq β] (x : β) :
    { e : Option α ≃ β // e none = x } ≃ (α ≃ { y : β // y ≠ x }) where
  toFun e :=
    { toFun :=
        fun a => ⟨(e : Option α ≃ β) a, ((EquivLike.injective _).ne_iff' e.property).2 (some_ne_none _)⟩,
      invFun := fun b =>
        get _
          (ne_none_iff_isSome.1
            (((EquivLike.injective _).ne_iff'
              ((apply_eq_iff_eq_symm_apply _).1 e.property).symm).2 b.property)),
      left_inv := fun a => by
        rw [← some_inj, some_get]
        exact symm_apply_apply (e : Option α ≃ β) a,
      right_inv := fun b => by
        ext
        simp only [ne_eq, some_get, apply_symm_apply] }
  invFun e :=
    ⟨{  toFun := fun a => casesOn' a x (Subtype.val ∘ e),
        invFun := fun b => if h : b = x then none else e.symm ⟨b, h⟩,
        left_inv := fun a => by
          cases a with
          | none => simp only [ne_eq, casesOn'_none, dite_true]
          | some a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property,
        right_inv := fun b => by
          by_cases h : b = x;
          { simp only [h, ne_eq, dite_true, casesOn'_none] }
          { simp only [h, ne_eq, dite_false, casesOn'_some, Function.comp_apply, apply_symm_apply]
          } },
      rfl⟩
  left_inv e := by
    ext a
    cases a
    · simp only [ne_eq, coe_fn_mk, coe_fn_symm_mk, some_get, dite_eq_ite, casesOn'_none]
      exact e.property.symm
    · simp only [ne_eq, coe_fn_mk, coe_fn_symm_mk, some_get, dite_eq_ite, casesOn'_some,
        Function.comp_apply]

  right_inv e := by
    ext a
    rfl
#align equiv.option_subtype Equiv.option_subtype

[Gabriel Ebner]

I'll look at this once mathlib4#631 is merged.

[Scott Morrison]

@Gabriel Ebner, merged. :-)

[Scott Morrison]

It's the second simp in left_inv which is mysteriously slow. However rfl closes that goal instantly, so I've just replaced it with that.

[Sebastien Gouezel]

It would still be good to understand why this simp is slow, because unless we diagnose what is going on this is bound to repeat many times during the porting. But of course, replacing it with a faster proof is an excellent short term solution.

[Arien Malec]

Do we have a test case collection of simp issues encountered during porting?

[Arien Malec]

or a TODO/FIXME tag that can be applied in source?