FLC_iso

Stream: condensed mathematics

[Johan Commelin]

Could someone please speed up FLC_iso in src/prop819.lean? It's currently timing out on some peoples hardware

[Kevin Buzzard]

I'll have a look

[Adam Topaz]

I can work on it later too if it's still a problem (since I defined it in the first place... :grimacing:)

[Kevin Buzzard]

I get elaboration of FLC_iso took 30.4s on master but I'm beginning to make progress.

[Adam Topaz]

IIRC the main slowdown is the dsimp [FLC_iso._match_1] in the first line of the proof.

[Kevin Buzzard]

Yes

[Kevin Buzzard]

dsimp only [FLC_iso._match_1] kills one of the two goals really quickly, but doesn't make progress with the other, even though it's what squeeze_dsimp is reporting.

[Adam Topaz]

squeeze_dsimp is rarely helpful, I've found

[Patrick Massot]

Is it faster with change rather than dsimp?

[Kevin Buzzard]

Rather surprisingly, changing your non-terminal tac1; tac2; tac3; dsimp [foo](which changes 1 goal to 4 to 2 to 2 to 1) to a logically equivalent thing with fewer semicolons has immediately pulled the runtime down from 30 seconds to 6 seconds. This is very odd.

[Adam Topaz]

Hmmm... Maybe it's because the single dsimp is looking at lemmas applicable to any of the branches created by the semicolons? I don't really know how dsimp works...

[Kevin Buzzard]

Hmm I think I've misunderstood some output. semicolons are confusing :-/

[Kevin Buzzard]

It's still no faster but I've got rid of the evil dsimp [FLC_iso._match_1]

[Kevin Buzzard]

So there are now two non-terminal dsimps, at least one of which is super-slow. I'll now try Patrick's change idea.

[Kevin Buzzard]

I've pushed the _match_1 removal to branch FLC_iso. I'm still working on it. I can't get change to work, the output of dsimp is super-unwieldy and is not round-tripping from the prettyprinter back into Lean

[Kevin Buzzard]

I've got it down to 11 seconds and I managed to remove one of the two non-terminal dsimps. The other one is just a mystery to me. I don't know how to look at the trace of what it's doing (trace.simplify.rewrite doesn't seem to work) and dsimp only doesn't work. I pushed to the FLC_iso branch.

[Kevin Buzzard]

@Adam Topaz if you take a look at it you might see some tricks I'm missing because you'll know more of the details of the argument.

[Adam Topaz]

I'm looking now...

[Kevin Buzzard]

The branch compiles for me BTW

[Adam Topaz]

Ok, I got it to a somewhat reasonable speed.

[Adam Topaz]

still slow, but not crazy

[Adam Topaz]

Oh, @Kevin Buzzard I noticed you made some changes. Instead of pushing, here's my code:

/--
This is a strict (i.e. norm-preserving) isomorphism between `FLC F M` and
the cochain complex obtained by mapping `FL F M` along the `Completion` functor.
-/
def FLC_iso : strict_iso ((Completion.map_homological_complex _).obj (FL F M)) (FLC F M) :=
{ iso := homological_complex.iso_of_components
    (λ i, nat.rec_on i (eq_to_iso rfl) (λ _ _, eq_to_iso rfl))
    begin
      rintro (_|i) (_|j) (_|⟨i,w⟩); ext,
      { dsimp only [],
        delta FLC FL,
        dsimp only [
          cosimplicial_object.augmented.whiskering,
          cosimplicial_object.augmented.whiskering_obj,
          cosimplicial_object.augmented.to_cocomplex,
          cosimplicial_object.augmented.to_cocomplex_obj,
          cochain_complex.of,
          functor.map_homological_complex ],
        rw dif_pos rfl,
        rw dif_pos rfl,
        erw [category.id_comp, category.comp_id, category.comp_id, category.comp_id],
        dsimp only [cosimplicial_object.augmented.to_cocomplex_d,
          cosimplicial_object.augmented.drop, comma.snd, cosimplicial_object.whiskering,
          whiskering_right, cosimplicial_object.coboundary, functor.const_comp, LCC],
        simp },
      { dsimp only [],
        delta FLC FL,
        dsimp only [
          cosimplicial_object.augmented.whiskering,
          cosimplicial_object.augmented.whiskering_obj,
          cosimplicial_object.augmented.to_cocomplex,
          cosimplicial_object.augmented.to_cocomplex_obj,
          cochain_complex.of,
          functor.map_homological_complex ],
        rw dif_pos rfl,
        rw dif_pos rfl,
        erw [category.id_comp, category.comp_id, category.comp_id, category.comp_id],
        dsimp only [
          cosimplicial_object.augmented.to_cocomplex_d,
          cosimplicial_object.augmented.drop,
          comma.snd,
          cosimplicial_object.whiskering,
          whiskering_right,
          cosimplicial_object.coboundary,
          LCC ],
        rw [Completion.map_sum],
        congr,
        funext k,
        rw [Completion.map_gsmul],
        congr' 1,
        apply FLC_iso_helper }
    end,
  is_strict := λ i, { strict_hom' := λ a, by { cases i; refl } } }.

[Kevin Buzzard]

I pushed to a branch, feel free to push to the same branch, a different branch, or whatever.

[Adam Topaz]

ok, pushed to FLC_iso_2. Someone else should verify whether it's faster on their side before merging to master

[Adam Topaz]

elaboration of FLC_iso took 9.89s

[Adam Topaz]

(on my unplugged underpowered laptop)

[Adam Topaz]

I heard no objections in the last 2.5 hours, so I merged this 9.89 second proof to master

[Johan Commelin]

Thanks a lot for the speedup!