exact/assumption timeout

Stream: new members

[Tsvi Benson-Tilsen]

In the middle of the attempted proof of full_faith_surj_equiv below, I get to this goal state:

filter: no filter
▶ 1 goal

C : cat
D : cat
F : Funct C D
fullF : full F
faithfulF : faithful F
surjF : essentially_surjective F
Ftransport : Π (c c' : C.obj), iso D (F.o c) (F.o c') → iso C c c' := full_faith_transport_iso F fullF faithfulF
a b : C.obj
f : C.hom a b
xx : D.seq (F.m f) (D.Id (F.o b)) = F.m f
⊢ D.seq (F.m f) (D.Id (F.o b)) = F.m f

Looks good. But then, using assumption or exact xx or similar gives a deterministic timeout. I'm confused by this. My impression is that the way to help with timeouts is to break things out into lemmas, which I'll try. Is there something easier that might work? Also, I'm surprised and confused that it's possible to have a term in the context with type equal to the goal Prop, and yet assumption and similar don't work easily. What's going on? Is it similar/related to "motive is not type correct" errors with rw? Is there some eq.rec kind of stuff going on in the background or something? Are definitions being unfolded for some reason? (I would guess not since there aren't any defined things in the goal... but maybe they're being hidden somehow, or maybe xx is being unfolded for some reason...?) How is it even possible for exact sorry to not succeed immediately? Does that mean Lean somehow doesn't know what type is supposed to go there, or something? (Replacing the whole term being worked on with sorry works fine, see comment.) Sorry for the long example, I don't get what's going on so I don't know how to make a smaller one.

(Note: the below is not the version I posted originally, it's changed to reflect changes I've made to my code at Alex B.'s suggestion.)

import tactic.ext
import data.finset
universes v v1 v2 u u1 u2 w

def reverse_compose {A B C : Type _} (f : A → B) (g : B → C) : A → C := λ x, g (f x)
infix `  ⨟ `:50 := reverse_compose

---- Categories and Functors

structure cat :=
(obj : Type u )
(hom : obj → obj → Type v)
(seq {a b c : obj} : hom a b → hom b c → hom a c)
(Id : Π (a : obj), hom a a)
(id_before : ∀ (a b : obj) (f : hom a b), seq (Id a) f = f)
(id_after : ∀ (a b : obj) (f : hom a b), seq f (Id b) = f)
(assoc {a b c d : obj}: ∀  (f : hom a b) (g : hom b c) (h : hom c d), seq (seq f g) h = seq f (seq g h))


@[ext] structure Funct (C : cat.{v1 u1}) (D : cat.{v2 u2}) :=
(o : C.obj → D.obj)
(m {a b : C.obj} : C.hom a b → D.hom (o a) (o b))
(comm : ∀ {a b c : C.obj} (f : C.hom a b) (g : C.hom b c), m (C.seq f g) = D.seq (m f) (m g))
(id : ∀ (c : C.obj), m (C.Id c) = D.Id (o c))

def Fseq {C D E : cat} (F : Funct C D) (G : Funct D E) : Funct C E := Funct.mk
(F.o ⨟ G.o)
(λ {a b} f, G.m (F.m f))
(λ {a b c} f g, by simp [F.comm f g, G.comm (F.m f) (F.m g)])
(λ c, begin delta reverse_compose, rw [F.id, G.id], end)

def CatId (C : cat) : Funct C C := Funct.mk
(id)
(λ a b, id)
(λ a b c f g, rfl)
(λ c, rfl)

def cat_id_before (C D : cat) (F : Funct C D) : Fseq (CatId C) F = F :=
begin ext, exact rfl, exact rfl, intro, delta Fseq CatId, simp, end

def cat_id_after (C D : cat) (F : Funct C D) : Fseq F (CatId D) = F :=
begin ext, exact rfl, exact rfl, intro, delta Fseq CatId, simp, end

structure iso (C : cat) (a b : C.obj) :=
(f : C.hom a b)
(inv : C.hom b a)
(finv:  C.seq f inv = C.Id a)
(invf:  C.seq inv f = C.Id b)

---- Natural transformations
@[ext] structure NT {C D : cat } (F G : Funct C D) :=
(η : Π (x : C.obj), D.hom (F.o x) (G.o x))
(comm : ∀ {a b : C.obj} (f : C.hom a b), D.seq (F.m f) (η b) = D.seq (η a) (G.m f))

def NTId {C D : cat} (F : Funct C D) := NT.mk
(λ x, D.Id (F.o x))
(λ f, by simp [D.id_before, D.id_after])

def NTseq {C D : cat} {F G H : Funct C D} (N : NT F G) (M : NT G H) : NT F H := NT.mk
(λ x, D.seq (N.η x) (M.η x))
(λ {a b : C.obj} f : C.hom a b, by rw [←D.assoc, N.comm, D.assoc, M.comm, D.assoc])

theorem NT_component_eq {C D : cat} (F G : Funct C D) (N M : NT F G) (ee : N.η = M.η) : N = M :=
by {ext, exact congr_fun ee x}

theorem NT_idbefore {C D : cat} (F G : Funct C D) (N : NT F G) : NTseq (NTId F) N = N :=
begin delta NTId NTseq, simp, ext, simp, rw [D.id_before] end

theorem NT_idafter {C D : cat} (F G : Funct C D) (N : NT F G) : NTseq N (NTId G) = N :=
begin delta NTId NTseq, simp, ext, simp, rw [D.id_after] end

def FunctCat (C : cat) (D : cat) : cat := cat.mk
(Funct C D)
(NT)
(@NTseq C D)
(NTId)
(NT_idbefore)
(NT_idafter)
(begin intros, delta NTseq, simp, ext, rw [D.assoc] end)

def Types : cat := cat.mk
(Type _)
(λ A B, (A → B))
(λ a b c f g, f ⨟ g)
(λ a, id)
(begin tidy, end)
(begin tidy, end)
(begin tidy, end)

-- isomorphic objects -> isomorphic homsets
theorem iso_objects_iso_hom (C : cat) (a a' b b' : C.obj) (isoaa' : iso C a a') (isobb' : iso C b b') : iso Types (C.hom a b) (C.hom a' b') := iso.mk
(λ f, C.seq isoaa'.inv (C.seq f isobb'.f))
(λ f, C.seq isoaa'.f (C.seq f isobb'.inv))
(begin ext, delta Types, simp, delta reverse_compose, simp, rw C.assoc, rw C.assoc, rw isobb'.finv, rw C.id_after, rw ←C.assoc, rw isoaa'.finv, rw C.id_before, end)
(begin ext, delta Types, simp, delta reverse_compose, simp, rw C.assoc, rw C.assoc, rw isobb'.invf, rw C.id_after, rw ←C.assoc, rw isoaa'.invf, rw C.id_before, end)

theorem iso_objects_iso_hom_pres_id (C : cat) (a b : C.obj) (isoab : iso C a b) : (iso_objects_iso_hom C a b a b isoab isoab).f (C.Id a) = C.Id b := begin
delta iso_objects_iso_hom, simp, rw [C.id_before, isoab.invf ], end


structure cat_equivalence (C D : cat) :=
(F : Funct C D)
(Inv : Funct D C)
(FInv : iso (FunctCat C C) (Fseq F Inv) (CatId C) )
(InvF : iso (FunctCat D D) (Fseq Inv F) (CatId D) )


variables {C D : cat}
structure full (F : Funct C D)  :=
(pre : Π {c c' : C.obj} (df : D.hom (F.o c) (F.o c')), C.hom c c')
(preimage : Π {c c' : C.obj} (df : D.hom (F.o c) (F.o c')), F.m (pre df) = df)

def faithful (F : Funct C D) := ∀ {c c' : C.obj} {cf cf' : C.hom c c'} (Fcf : F.m cf = F.m cf'),  (cf = cf')

def essentially_surjective (F : Funct C D) := Π (d : D.obj), Σ (c : C.obj), iso D d (F.o c)

-- set_option pp.all true

theorem full_faith_transport_iso (F : Funct C D) (fullF : full F) (faithfulF : faithful F) (c c' : C.obj) (isoFcFc' : iso D (F.o c) (F.o c')) : iso C c c' := iso.mk
(fullF.pre isoFcFc'.f)
(fullF.pre isoFcFc'.inv)
(faithfulF (begin rw F.comm, rw F.id, rw (fullF.preimage isoFcFc'.f), rw (fullF.preimage isoFcFc'.inv), rw isoFcFc'.finv, end))
(faithfulF (begin rw F.comm, rw F.id, rw (fullF.preimage isoFcFc'.f), rw (fullF.preimage isoFcFc'.inv), rw isoFcFc'.invf, end))

theorem full_faith_surj_equiv (F : Funct C D) (fullF : full F) (faithfulF : faithful F) (surjF : essentially_surjective F) : cat_equivalence C D := cat_equivalence.mk
F
(Funct.mk
   (λ d, (surjF d).1)
   (λ d d' df, (fullF.pre ((iso_objects_iso_hom D d (F.o (surjF d).1) d' (F.o (surjF d').1) (surjF d).2 (surjF d').2 ).f df)))
   (begin intros a b c f g,
      exact faithfulF (begin
         rw F.comm,
         simp only [fullF.preimage],
         delta iso_objects_iso_hom, simp only,
         rw D.assoc, rw D.assoc, rw D.assoc, rw ←D.assoc (surjF b).snd.f, rw (surjF b).snd.finv, rw D.id_before,
      end) end)
   (begin
      intro d,
      rw iso_objects_iso_hom_pres_id,
      exact faithfulF (begin
         simp only [fullF.preimage],
         rw F.id,
      end)
      end))
(iso.mk
(let Ftransport := (full_faith_transport_iso F (@fullF) (@faithfulF)) in NT.mk
   (λ c, (Ftransport c (surjF (F.o c)).fst (surjF (F.o c)).snd).inv)

-- sorry
-- start of term /-
   (begin intros a b f,
   delta Fseq,
simp only [id.def, eq_mpr_eq_cast, cast_eq],
   delta CatId, simp only [id.def],
   exact (faithfulF (begin
      simp only [F.comm],
      simp only [fullF.preimage],
      delta iso_objects_iso_hom,
      simp only [Ftransport],
      delta full_faith_transport_iso,
      simp only [fullF.preimage],
      simp only [D.assoc],
      exact congr_arg (D.seq (surjF (F.o a)).snd.inv)
      (begin
         simp only [(surjF (F.o b)).snd.finv],
         have xx, from D.id_after (F.o a) (F.o b) (F.m f),
dsimp,
-- these give: (deterministic) timeout
-- exact xx,
-- convert xx,
-- assumption,
         end)
   end)),
   end)

-- end of term  -/
   )
sorry
sorry
sorry)
sorry

[Alex J. Best]

If you set set_option pp.all true before the lemma can you find any differences between xx and the goal in that spot. It might be quite long and difficult to see but this is probably a case where there is some difference that isn't shown in the prettty printed representation of the terms

[Alex J. Best]

dsimp,
exact xx,

works for me, but still takes a while

[Tsvi Benson-Tilsen]

Thanks. Well, xx and the goal definitely aren't identical when fully printed.

[Tsvi Benson-Tilsen]

Hm, I still get a deterministic timeout with
dsimp, exact xx,

[Alex J. Best]

I did use squeeze_simp to find out that most of the simps in your proof were really simp only [something] this is good practice to do anyway and helps speed up long proofs

[Tsvi Benson-Tilsen]

Ok I'll try that.

[Alex J. Best]

It also looks like you might be using tactic mode to produce data (def-like things rather than theorem-like things) this often produces terms that are very hard to handle as tactics often generate a lot of extra things in the term

[Tsvi Benson-Tilsen]

Yeah, I use tactic mode for the first argument to NT.mk, which is data.

[Tsvi Benson-Tilsen]

I'm still getting a timeout. That term now looks like:

-- start of term /-
   (begin intros a b f,
   delta Fseq,
simp only [id.def, eq_mpr_eq_cast, cast_eq],
   delta CatId, simp only [id.def],
   exact (faithfulF (begin
      simp only [F.comm],
      simp only [fullF.preimage],
      delta iso_objects_iso_hom,
      simp only [Ftransport],
      delta full_faith_transport_iso,
-- squeeze_simp,
--       simp,
      simp only [fullF.preimage],
      simp only [D.assoc],
      exact congr_arg (D.seq (surjF (F.o a)).snd.inv)
      (begin
         simp only [(surjF (F.o b)).snd.finv],
         have xx, from D.id_after (F.o a) (F.o b) (F.m f),
dsimp,
  exact xx,

--          gives: (deterministic) timeout
--            assumption,
--
--          gives: (deterministic) timeout
--           convert xx,
--
--          gives: (deterministic) timeout
--          exact xx,
--
--          gives: (deterministic) timeout
--          rw xx,
--
--          gives: (deterministic) timeout
--           exact sorry
         end)
   end)),
   end)

-- end of term  -/

[Tsvi Benson-Tilsen]

I'll try rewriting the data term.

[Tsvi Benson-Tilsen]

(Alex, are you sure it succeeded for you? The error message appears at the first line of the theorem statement.)

[Tsvi Benson-Tilsen]

The data term (the previous argument)

(λ c, begin delta Fseq,delta  reverse_compose, delta CatId,  simp only [id.def],
exact (Ftransport c (surjF (F.o c)).fst (surjF (F.o c)).snd).inv, end)

can be replaced with

   (λ c, (Ftransport c (surjF (F.o c)).fst (surjF (F.o c)).snd).inv)

but I still get a timeout.

[Tsvi Benson-Tilsen]

I've rewritten all the simps to simp only, and now xx and the goal are identical with set_option pp.all true:

xx : @eq.{u_3+1} (D.hom (@Funct.o.{u_1 u_3 u_2 u_4} C D F a) (@Funct.o.{u_1 u_3 u_2 u_4} C D F b)) (@cat.seq.{u_3 u_4} D (@Funct.o.{u_1 u_3 u_2 u_4} C D F a) (@Funct.o.{u_1 u_3 u_2 u_4} C D F b) (@Funct.o.{u_1 u_3 u_2 u_4} C D F b) (@Funct.m.{u_1 u_3 u_2 u_4} C D F a b f) (D.Id (@Funct.o.{u_1 u_3 u_2 u_4} C D F b))) (@Funct.m.{u_1 u_3 u_2 u_4} C D F a b f)
⊢ @eq.{u_3+1} (D.hom (@Funct.o.{u_1 u_3 u_2 u_4} C D F a) (@Funct.o.{u_1 u_3 u_2 u_4} C D F b)) (@cat.seq.{u_3 u_4} D (@Funct.o.{u_1 u_3 u_2 u_4} C D F a) (@Funct.o.{u_1 u_3 u_2 u_4} C D F b) (@Funct.o.{u_1 u_3 u_2 u_4} C D F b) (@Funct.m.{u_1 u_3 u_2 u_4} C D F a b f) (D.Id (@Funct.o.{u_1 u_3 u_2 u_4} C D F b))) (@Funct.m.{u_1 u_3 u_2 u_4} C D F a b f)

But I still get a timeout! Here's the current text of the theorem:

theorem full_faith_surj_equiv (F : Funct C D) (fullF : full F) (faithfulF : faithful F) (surjF : essentially_surjective F) : cat_equivalence C D := cat_equivalence.mk
F
(Funct.mk
   (λ d, (surjF d).1)
   (λ d d' df, (fullF.pre ((iso_objects_iso_hom D d (F.o (surjF d).1) d' (F.o (surjF d').1) (surjF d).2 (surjF d').2 ).f df)))
   (begin intros a b c f g,
      exact faithfulF (begin
         rw F.comm,
         simp only [fullF.preimage],
         delta iso_objects_iso_hom, simp only,
         rw D.assoc, rw D.assoc, rw D.assoc, rw ←D.assoc (surjF b).snd.f, rw (surjF b).snd.finv, rw D.id_before,
      end) end)
   (begin
      intro d,
      rw iso_objects_iso_hom_pres_id,
      exact faithfulF (begin
         simp only [fullF.preimage],
         rw F.id,
      end)
      end))
(iso.mk
(let Ftransport := (full_faith_transport_iso F (@fullF) (@faithfulF)) in NT.mk
   (λ c, (Ftransport c (surjF (F.o c)).fst (surjF (F.o c)).snd).inv)

-- sorry
-- start of term /-
   (begin intros a b f,
   delta Fseq,
simp only [id.def, eq_mpr_eq_cast, cast_eq],
   delta CatId, simp only [id.def],
   exact (faithfulF (begin
      simp only [F.comm],
      simp only [fullF.preimage],
      delta iso_objects_iso_hom,
      simp only [Ftransport],
      delta full_faith_transport_iso,
      simp only [fullF.preimage],
      simp only [D.assoc],
      exact congr_arg (D.seq (surjF (F.o a)).snd.inv)
      (begin
         simp only [(surjF (F.o b)).snd.finv],
         have xx, from D.id_after (F.o a) (F.o b) (F.m f),
dsimp,
-- these give: (deterministic) timeout
-- exact xx,
-- convert xx,
assumption,
         end)
   end)),
   end)

-- end of term  -/
   )
sorry
sorry
sorry)
sorry

[Alex J. Best]

Yeah it does eventually work for me, maybe I just have a higher timeout setting, but changing your settings is not a solution :smile: we shouldn't have to wait several seconds to check theorems ideally.

[Alex J. Best]

One other thing that might help is avoiding nested tactic blocks

[Alex J. Best]

E.g.

import tactic.ext
import data.finset
universes v v1 v2 u u1 u2 w

def reverse_compose {A B C : Type _} (f : A → B) (g : B → C) : A → C := λ x, g (f x)
infix `  ⨟ `:50 := reverse_compose

---- Categories and Functors

structure cat :=
(obj : Type u )
(hom : obj → obj → Type v)
(seq {a b c : obj} : hom a b → hom b c → hom a c)
(Id : Π (a : obj), hom a a)
(id_before : ∀ (a b : obj) (f : hom a b), seq (Id a) f = f)
(id_after : ∀ (a b : obj) (f : hom a b), seq f (Id b) = f)
(assoc {a b c d : obj}: ∀  (f : hom a b) (g : hom b c) (h : hom c d), seq (seq f g) h = seq f (seq g h))
#print cat.id_before

@[ext] structure Funct (C : cat.{v1 u1}) (D : cat.{v2 u2}) :=
(o : C.obj → D.obj)
(m {a b : C.obj} : C.hom a b → D.hom (o a) (o b))
(comm : ∀ {a b c : C.obj} (f : C.hom a b) (g : C.hom b c), m (C.seq f g) = D.seq (m f) (m g))
(id : ∀ (c : C.obj), m (C.Id c) = D.Id (o c))

def Fseq {C D E : cat} (F : Funct C D) (G : Funct D E) : Funct C E := Funct.mk
(F.o ⨟ G.o)
(λ {a b} f, G.m (F.m f))
(λ {a b c} f g, by simp [F.comm f g, G.comm (F.m f) (F.m g)])
(λ c, begin delta reverse_compose, rw [F.id, G.id], end)

def CatId (C : cat) : Funct C C := Funct.mk
(id)
(λ a b, id)
(λ a b c f g, rfl)
(λ c, rfl)

def cat_id_before (C D : cat) (F : Funct C D) : Fseq (CatId C) F = F :=
begin ext, exact rfl, exact rfl, intro, delta Fseq CatId, simp, end

def cat_id_after (C D : cat) (F : Funct C D) : Fseq F (CatId D) = F :=
begin ext, exact rfl, exact rfl, intro, delta Fseq CatId, simp, end

structure iso (C : cat) (a b : C.obj) :=
(f : C.hom a b)
(inv : C.hom b a)
(finv:  C.seq f inv = C.Id a)
(invf:  C.seq inv f = C.Id b)

---- Natural transformations
@[ext] structure NT {C D : cat } (F G : Funct C D) :=
(η : Π (x : C.obj), D.hom (F.o x) (G.o x))
(comm : ∀ {a b : C.obj} (f : C.hom a b), D.seq (F.m f) (η b) = D.seq (η a) (G.m f))

def NTId {C D : cat} (F : Funct C D) := NT.mk
(λ x, D.Id (F.o x))
(λ f, by simp [D.id_before, D.id_after])

def NTseq {C D : cat} {F G H : Funct C D} (N : NT F G) (M : NT G H) : NT F H := NT.mk
(λ x, D.seq (N.η x) (M.η x))
(λ {a b : C.obj} f : C.hom a b, by rw [←D.assoc, N.comm, D.assoc, M.comm, D.assoc])

theorem NT_component_eq {C D : cat} (F G : Funct C D) (N M : NT F G) (ee : N.η = M.η) : N = M :=
by {ext, exact congr_fun ee x}

theorem NT_idbefore {C D : cat} (F G : Funct C D) (N : NT F G) : NTseq (NTId F) N = N :=
begin delta NTId NTseq, simp, ext, simp, rw [D.id_before] end

theorem NT_idafter {C D : cat} (F G : Funct C D) (N : NT F G) : NTseq N (NTId G) = N :=
begin delta NTId NTseq, simp, ext, simp, rw [D.id_after] end

def FunctCat (C : cat) (D : cat) : cat := cat.mk
(Funct C D)
(NT)
(@NTseq C D)
(NTId)
(NT_idbefore)
(NT_idafter)
(begin intros, delta NTseq, simp, ext, rw [D.assoc] end)

def Types : cat := cat.mk
(Type _)
(λ A B, (A → B))
(λ a b c f g, f ⨟ g)
(λ a, id)
(begin tidy, end)
(begin tidy, end)
(begin tidy, end)

-- isomorphic objects -> isomorphic homsets
theorem iso_objects_iso_hom (C : cat) (a a' b b' : C.obj) (isoaa' : iso C a a') (isobb' : iso C b b') : iso Types (C.hom a b) (C.hom a' b') := iso.mk
(λ f, C.seq isoaa'.inv (C.seq f isobb'.f))
(λ f, C.seq isoaa'.f (C.seq f isobb'.inv))
(begin ext, delta Types, simp, delta reverse_compose, simp, rw C.assoc, rw C.assoc, rw isobb'.finv, rw C.id_after, rw ←C.assoc, rw isoaa'.finv, rw C.id_before, end)
(begin ext, delta Types, simp, delta reverse_compose, simp, rw C.assoc, rw C.assoc, rw isobb'.invf, rw C.id_after, rw ←C.assoc, rw isoaa'.invf, rw C.id_before, end)

theorem iso_objects_iso_hom_pres_id (C : cat) (a b : C.obj) (isoab : iso C a b) : (iso_objects_iso_hom C a b a b isoab isoab).f (C.Id a) = C.Id b := begin
delta iso_objects_iso_hom, simp, rw [C.id_before, isoab.invf ], end


structure cat_equivalence (C D : cat) :=
(F : Funct C D)
(Inv : Funct D C)
(FInv : iso (FunctCat C C) (Fseq F Inv) (CatId C) )
(InvF : iso (FunctCat D D) (Fseq Inv F) (CatId D) )


variables {C D : cat}
structure full (F : Funct C D)  :=
(pre : Π {c c' : C.obj} (df : D.hom (F.o c) (F.o c')), C.hom c c')
(preimage : Π {c c' : C.obj} (df : D.hom (F.o c) (F.o c')), F.m (pre df) = df)

def faithful (F : Funct C D) := ∀ {c c' : C.obj} {cf cf' : C.hom c c'} (Fcf : F.m cf = F.m cf'),  (cf = cf')

def essentially_surjective (F : Funct C D) := Π (d : D.obj), Σ (c : C.obj), iso D d (F.o c)

theorem full_faith_transport_iso (F : Funct C D) (fullF : full F) (faithfulF : faithful F) (c c' : C.obj) (isoFcFc' : iso D (F.o c) (F.o c')) : iso C c c' := iso.mk
(fullF.pre isoFcFc'.f)
(fullF.pre isoFcFc'.inv)
(faithfulF (begin rw F.comm, rw F.id, rw (fullF.preimage isoFcFc'.f), rw (fullF.preimage isoFcFc'.inv), rw isoFcFc'.finv, end))
(faithfulF (begin rw F.comm, rw F.id, rw (fullF.preimage isoFcFc'.f), rw (fullF.preimage isoFcFc'.inv), rw isoFcFc'.invf, end))

-- set_option pp.all true
theorem full_faith_surj_equiv (F : Funct C D) (fullF : full F) (faithfulF : faithful F) (surjF : essentially_surjective F) : cat_equivalence C D := cat_equivalence.mk
F
(Funct.mk
   (λ d, (surjF d).1)
   (λ d d' df, (fullF.pre ((iso_objects_iso_hom D d (F.o (surjF d).1) d' (F.o (surjF d').1) (surjF d).2 (surjF d').2 ).f df)))
   (begin intros a b c f g,
      refine faithfulF _,
         rw F.comm,
         simp only [fullF.preimage],
         delta iso_objects_iso_hom, simp only,
         rw D.assoc, rw D.assoc, rw D.assoc, rw ←D.assoc (surjF b).snd.f, rw (surjF b).snd.finv, rw D.id_before,
     end)
   (begin
      intro d,
      rw iso_objects_iso_hom_pres_id,
      refine faithfulF _,
         simp only [fullF.preimage],
         rw F.id,
      end))
(iso.mk
(let Ftransport := (full_faith_transport_iso F (@fullF) (@faithfulF)) in NT.mk
   (λ c,
(Ftransport c (surjF (F.o c)).fst (surjF (F.o c)).snd).inv)
-- sorry
-- start of term /-
   (begin intros a b f,
   delta Fseq,
   delta CatId, simp only [id.def],
   refine (faithfulF _),
      simp_rw [F.comm],
      simp only [fullF.preimage],
      delta iso_objects_iso_hom,
      simp only [Ftransport],
      delta full_faith_transport_iso,
      simp only [fullF.preimage],
      simp_rw D.assoc,
      refine congr_arg (D.seq (surjF (F.o a)).snd.inv) _,
         simp_rw (surjF (F.o b)).snd.finv,
         dsimp,
        exact D.id_after (F.o a) (F.o b) (F.m f),
        --  exact xx,
--          gives: (deterministic) timeout
--            assumption,
--
--          gives: (deterministic) timeout
--           convert xx,
--
--          gives: (deterministic) timeout
--          exact xx,
--
--          gives: (deterministic) timeout
--          rw xx,
--
--          gives: (deterministic) timeout
--           exact sorry
   end)

-- end of term  -/
   )
sorry
sorry
sorry)
sorry

[Alex J. Best]

But it is still slow even with this

[Tsvi Benson-Tilsen]

Thanks. I've rewritten it like that. But now... I can't figure out how to set timeout :(. I've run "lean --timeout=100000"; and I've changed some line in /lean.nvim/lua/lean/_util.lua from timeout = timeout or 10000 to timeout = timeout or 100000; and I've tried the tactic try_for 1000000 { exact xx }; and I've tried set_option timeout 100000 before the theorem; still, it fails with a timeout after apparently the same amount of time (about 10 seconds or so).

I'm in neovim; Lean version 3.38.0.

[Alex J. Best]

Timeout isn't a literal time for lean, rather a maximum number of memory allocations mine is set to 3000000, so maybe you just need to try bigger values ?

[Alex J. Best]

It should be set on the command line when initiating the server, but hopefully the lean.nvim plugin will have a configurable option

[Julian Berman]

That's the wrong place (lsp/_util), but sorry that the docs don't make this example clear. Right now you do this by:

require('lean').setup{
  -- whatever other options you set
  lsp3 = {
    cmd = { 'lean-language-server', '--stdio', '--', '-M', '4096', '-T', '3000000' },
    -- on_attach = on_attach or whatever else you set here
  },
}

[Julian Berman]

An issue asking for better docs on how to modify the timeout is definitely welcome, as of course is a PR adding that example, or feel free to add it in the wiki here: https://github.com/Julian/lean.nvim/wiki/Configuring-&-Extending

[Julian Berman]

(Also welcome would be if sufficient folks think the default timeout should be higher we could change it, but I think I copied the VSCode default)

[Tsvi Benson-Tilsen]

Ha, I was just writing an email to you! (Yeah I'd figured that was probably the wrong place, on reflection.) Ok great I'll try that out.

[Julian Berman]

Well hello there then :) yeah let me know how it goes!

[Tsvi Benson-Tilsen]

Success! The timeout is longer, and the proof goes through! Thanks both. I'll add an entry to that wiki page.

[Tsvi Benson-Tilsen]

So, I bumped into another instance of this sort of very slow proof. Can someone point me to stuff to look at (exposition about how Lean works, or parts of the source code maybe) to understand enough of what's going on under the hood that I can make educated guesses about why proofs take a really long time to be checked? I'm confused how a proof that basically looks like delta simp only delta simp only.... , and then ends with exact, takes so long. Like, I run these tactics, and in the background Lean is setting up some function from [the rest of the proof] to [the final actual proof term], and somehow that can lead to explosively large proof terms, but, like, how can just unfolding definitions and doing seemingly simple (e.g., seemingly linear or linear-ish) beta reductions and similar lead to huge terms? Is there in general something wrong with writing lots of nested definitions?

Here's another example of the sort of proof I mean; this takes over a minute to check, for me. (This is NOT a MWE, there's a MWE above; this is just to illustrate more what I mean by this sort of proof.)

theorem cone_to_FtoX_full {J C : cat} (F : Funct J C) : full (conecat_to_FtoXcat F) := full.mk
(λ c c' f, ⟨f.sourcef,begin
have fcomm, from f.comm,
delta conecat_to_FtoXcat at fcomm,
delta Diagonal at fcomm,
delta objFunct at fcomm,
dsimp at fcomm,
delta comm_square at fcomm,
delta FunctCat at fcomm,
dsimp at fcomm,
delta NTseq at fcomm,
dsimp at fcomm,
delta NTId at fcomm,
dsimp at fcomm,
simp_rw C.id_after at fcomm,
have xx, from (λ j, congr_fun fcomm j),
dsimp only at xx,
exact xx,
end
⟩)
(begin
sorry
end)

[Tsvi Benson-Tilsen]

One naive guess I can make is that there's some stuff hidden by the pretty printer; then, when I do delta X, there's some Xs in the hidden stuff, and those get invisibly unfolded in the background; and that expands out. Is that a likely scenario? Is there some way to unfold definitions more conservatively (like "only in the term I'm looking at in the pretty printer" or something)?

[Tsvi Benson-Tilsen]

Am I supposed to make more things irreducible?

[Tsvi Benson-Tilsen]

Ok apparently using dunfold instead of delta is WAY faster (in the above example, that replacement makes the checking go from >1 min to ~1 sec for me).

[Alex J. Best]

Whoa nice find! That's news to me. This definitely seems like something worth getting to the bottom of and writing about on the community documentation pages, as it could definitely be catching a lot of people out without them realizing

[Alex J. Best]

By the way, have you tried using the mathlib linters? You just type #lint at the bottom of the file (assuming you have tactic.lint imported somehow) and it inspects your work for common mistakes, some of them can be ignored if you aren't worried about PRing stuff to mathlib.
It highlights a couple of potential problems in the code you posted before, some defs that should be lemmas and also some universe issues. These might be contributing to the bad performance you are seeing

[Tsvi Benson-Tilsen]

Not sure how to get to the bottom of things. Maybe someone who knows how Lean works can take a look? Here's a working example; see the two versions of the theorem at the end.

import tactic.ext
import data.finset
universes v v1 v2 u u1 u2 w

def reverse_compose {A B C : Type _} (f : A → B) (g : B → C) : A → C := λ x, g (f x)
infix `  ⨟ `:50 := reverse_compose

---- categories, functors, natural transformations
---- Categories and Functors
structure cat :=
(obj : Type u )
(hom : obj → obj → Type v)
(seq {a b c : obj} : hom a b → hom b c → hom a c)
(Id : Π (a : obj), hom a a)
(id_before : ∀ (a b : obj) (f : hom a b), seq (Id a) f = f)
(id_after : ∀ (a b : obj) (f : hom a b), seq f (Id b) = f)
(assoc {a b c d : obj}: ∀  (f : hom a b) (g : hom b c) (h : hom c d), seq (seq f g) h = seq f (seq g h))


@[ext] structure Funct (C : cat.{v1 u1}) (D : cat.{v2 u2}) :=
(o : C.obj → D.obj)
(m {a b : C.obj} : C.hom a b → D.hom (o a) (o b))
(comm : ∀ {a b c : C.obj} (f : C.hom a b) (g : C.hom b c), m (C.seq f g) = D.seq (m f) (m g))
(id : ∀ (c : C.obj), m (C.Id c) = D.Id (o c))

def Fseq {C D E : cat} (F : Funct C D) (G : Funct D E) : Funct C E := Funct.mk
(F.o ⨟ G.o)
(λ {a b} f, G.m (F.m f))
(λ {a b c} f g, by simp [F.comm f g, G.comm (F.m f) (F.m g)])
(λ c, begin delta reverse_compose, rw [F.id, G.id], end)

def CatId (C : cat) : Funct C C := Funct.mk
(id)
(λ a b, id)
(λ a b c f g, rfl)
(λ c, rfl)

def cat_id_before (C D : cat) (F : Funct C D) : Fseq (CatId C) F = F :=
begin ext, exact rfl, exact rfl, intro, delta Fseq CatId, simp, end

def cat_id_after (C D : cat) (F : Funct C D) : Fseq F (CatId D) = F :=
begin ext, exact rfl, exact rfl, intro, delta Fseq CatId, simp, end

def Cat : cat := cat.mk
(cat)
(λ (C D : cat), Funct C D)
(λ C D E, Fseq)
(CatId)
(cat_id_before)
(cat_id_after)
(begin delta Fseq, simp, delta reverse_compose, simp, intros, trivial end)

structure iso (C : cat) (a b : C.obj) :=
(f : C.hom a b)
(inv : C.hom b a)
(finv:  C.seq f inv = C.Id a)
(invf:  C.seq inv f = C.Id b)

---- Natural transformations
def preNT {C D : cat } (F G : Funct C D) := Π (x : C.obj), D.hom (F.o x) (G.o x)

@[ext] structure NT {C D : cat } (F G : Funct C D) :=
(η : preNT F G)
(comm : ∀ {a b : C.obj} (f : C.hom a b), D.seq (F.m f) (η b) = D.seq (η a) (G.m f))

def NTId {C D : cat} (F : Funct C D) := NT.mk
(λ x, D.Id (F.o x))
(λ f, by simp [D.id_before, D.id_after])

def NTseq {C D : cat} {F G H : Funct C D} (N : NT F G) (M : NT G H) : NT F H := NT.mk
(λ x, D.seq (N.η x) (M.η x))
(λ {a b : C.obj} f : C.hom a b, by rw [←D.assoc, N.comm, D.assoc, M.comm, D.assoc])

theorem NT_idbefore {C D : cat} (F G : Funct C D) (N : NT F G) : NTseq (NTId F) N = N :=
begin delta NTId NTseq, simp, ext, simp, rw [D.id_before] end

theorem NT_idafter {C D : cat} (F G : Funct C D) (N : NT F G) : NTseq N (NTId G) = N :=
begin delta NTId NTseq, simp, ext, simp, rw [D.id_after] end

def FunctCat (C : cat) (D : cat) : cat := cat.mk
(Funct C D)
(NT)
(@NTseq C D)
(NTId)
(NT_idbefore)
(NT_idafter)
(begin intros, delta NTseq, simp, ext, rw [D.assoc] end)

def isSingleton (T : Type _) : Prop := ∃ x : T, ∀ y : T, x = y
def isInitial  {C: cat} (c : C.obj) : Prop := ∀ (d : C.obj), isSingleton (C.hom c d)
def isTerminal {C: cat} (c : C.obj) : Prop := ∀ (d : C.obj), isSingleton (C.hom d c)

def Terminal (C : cat) := { c : C.obj  // isTerminal c }
def Initial (C : cat) := { c : C.obj  // isInitial c }

def Nonempty (C : cat) := inhabited C.obj

def Types : cat := cat.mk
(Type _)
(λ A B, (A → B))
(λ a b c f g, f ⨟ g)
(λ a, id)
(begin tidy, end)
(begin tidy, end)
(begin tidy, end)

---- Comma categories
def comm_square {C : cat} { a b c d : C.obj} (ab : C.hom a b) (bd : C.hom b d) (ac : C.hom a c) (cd : C.hom c d) : Prop :=
C.seq ab bd = C.seq ac cd

theorem comp_comm_square {C : cat} { a b c d e f: C.obj} {ab : C.hom a b} {bd : C.hom b d} {ac : C.hom a c} {cd : C.hom c d} {df : C.hom d f} {ce : C.hom c e} {ef : C.hom e f}
(abcd : comm_square ab bd ac cd) (cdef : comm_square cd df ce ef) : comm_square ab (C.seq bd df) (C.seq ac ce) ef :=
begin
unfold comm_square,
unfold comm_square at abcd,
unfold comm_square at cdef,
rw [C.assoc, ←cdef, ←C.assoc, abcd, C.assoc],
end

theorem funct_id {C D : cat} (F : Funct C D) : ∀ (c : C.obj), F.m (C.Id c) = D.Id (F.o c) :=
begin
intro c,
rw [F.id c],
end


variables {A B : cat} (C : cat) (S : Funct A C) (T : Funct B C)

def CommaObj := Σ (a : A.obj) (b : B.obj), C.hom (S.o a) (T.o b)

@[ext]
structure CommaHom (ar1 ar2 : CommaObj C S T) :=
(sourcef : A.hom ar1.1 ar2.1)
(targetf : B.hom ar1.2.1 ar2.2.1)
(comm : comm_square ar1.2.2 (T.m targetf) (S.m sourcef) ar2.2.2 )

def Comma : cat := cat.mk
(CommaObj C S T)
(λ ar1 ar2, CommaHom C S T ar1 ar2)
(λ ar1 ar2 ar3 m12 m23, CommaHom.mk (A.seq m12.sourcef m23.sourcef) (B.seq m12.targetf m23.targetf) (begin
   rw [T.comm,S.comm], exact comp_comm_square m12.comm m23.comm, end))
(λ ar, CommaHom.mk (A.Id ar.1) (B.Id ar.2.1) (begin rw [funct_id, funct_id], unfold comm_square, rw [C.id_before, C.id_after], end))
(begin intros, dsimp only, simp only [A.id_before, B.id_before], ext, dsimp only, refl, dsimp only, refl, end)
(begin intros, dsimp only, simp only [A.id_after, B.id_after], ext, dsimp only, refl, dsimp only, refl, end)
(begin intros, simp only, split, apply A.assoc, apply B.assoc, end)

---- Discrete
inductive Star : Type _
| star : Star

def One : cat := cat.mk
Star
(λ _ _, Star)
(λ _ _ _ _, id)
(λ _, Star.star)
(begin intros, refl end)
(begin intros, simp, induction f, refl end)
(begin intros, refl end)

---- Universal morphism

def constFunct {C : cat} (J : cat) (c : C.obj) : Funct J C := Funct.mk
(λ _, c)
(λ _ _ _, C.Id c)
(by {rw [C.id_before], intros, refl})
(λ _, rfl)

def objFunct {C : cat} (x : C.obj) : Funct One C := Funct.mk
(λ _, x)
(λ _ _ _, C.Id x)
(λ _ _ _ _ _, eq.symm (C.id_before x x (C.Id x)))
(λ _, rfl)

def FtoXCat {J C : cat} (F : Funct J C) (x : C.obj) : cat := (Comma C F (objFunct x))
def FfromXCat {J C : cat} (F : Funct J C) (x : C.obj) : cat := (Comma C (objFunct x) F)

def universal_FtoX {J C : cat} (F : Funct J C) (x : C.obj) : Type _ := Terminal (FtoXCat F x)
def universal_FfromX {J C : cat} (F : Funct J C) (x : C.obj) : Type _ := Initial (FfromXCat F x)

---- Limits
def Diagonal (C J : cat ) : Funct C (FunctCat J C) := Funct.mk
(λ c, constFunct J c)
(λ a b f, NT.mk
   (λ _, f)
   (begin intros, delta constFunct, simp, rw C.id_before a b f, rw C.id_after a b f, end))
(begin intros, delta FunctCat, simp, ext, simp, delta NTseq, simp, end)
(begin intros,  delta FunctCat, simp, delta NTId, ext, simp, delta constFunct,simp, end)

def limit_univ_morphism {J C : cat} (F : Funct J C) := universal_FtoX (Diagonal C J) F
def colimit_univ_morphism {J C : cat} (F : Funct J C) := universal_FfromX (Diagonal C J) F

structure Cone {J C : cat} (D : Funct J C) :=
(c : C.obj)
(proj : Π (j : J.obj), C.hom c (D.o j))
(comm : ∀ {a b : J.obj} (m : J.hom a b), C.seq (proj a) (D.m m) = proj b)

structure ConeHom {J C : cat} (D : Funct J C) (c1 c2 : Cone D) :=
(map : C.hom c1.c c2.c)
(comm : ∀ (j : J.obj), c1.proj j = C.seq map (c2.proj j))

def ConeCat {J C : cat} (D : Funct J C) : cat := cat.mk
(Cone D)
(λ c1 c2, ConeHom D c1 c2)
(λ a b c f g, ⟨C.seq f.1 g.1, begin intros j, cases g, cases f, dsimp at *, rw [f_comm j, g_comm j, C.assoc], end⟩)
(λ c, ⟨C.Id c.1,begin intros j, rw [C.id_before], end⟩)
(begin intros a b f, cases f, dsimp at *, simp at *, rw [C.id_before], end)
(begin intros a b f, cases f, dsimp at *, simp at *, rw [C.id_after], end)
(begin intros a b c d f g h, cases h, cases g, cases f, dsimp at *, simp at *, rw [C.assoc], end)

def limit_cone {J C : cat} (F : Funct J C) := Terminal (ConeCat F)

def conecat_to_FtoXcat {J C : cat} (F : Funct J C) : Funct (ConeCat F) (FtoXCat (Diagonal C J) F) := Funct.mk
(λ cone, ⟨cone.c,⟨Star.star, NT.mk
   (λ j, cone.proj j)
   (begin intros a b f, dunfold Diagonal, dsimp only, dunfold constFunct, dsimp only, rw C.id_before, dunfold objFunct, dsimp only, rw (cone.comm f), end) ⟩⟩)
(λ a b f, CommaHom.mk f.map Star.star (begin
cases f, dsimp at *, ext1, ext1,
dunfold FunctCat, dunfold objFunct, dunfold Diagonal, dsimp only [NTseq, NTId], rw C.id_after, rw (f_comm x),
end))
(begin intros a b c f g, refl, end)
(begin intro c, refl, end)

#check 1

structure full {C D : cat} (F : Funct C D)  :=
(pre : Π {c c' : C.obj} (df : D.hom (F.o c) (F.o c')), C.hom c c')
(preimage : Π {c c' : C.obj} (df : D.hom (F.o c) (F.o c')), F.m (pre df) = df)

--- fast version
-- /-
theorem cone_to_FtoX_full {J C : cat} (F : Funct J C) : full (conecat_to_FtoXcat F) := full.mk
(λ c c' f, ⟨f.sourcef,begin
have fcomm, from f.comm,
dunfold conecat_to_FtoXcat at fcomm,
dunfold Diagonal at fcomm,
dunfold objFunct at fcomm,
dsimp at fcomm,
dunfold comm_square at fcomm,
dunfold FunctCat at fcomm,
dsimp at fcomm,
dunfold NTseq at fcomm,
dsimp at fcomm,
dunfold NTId at fcomm,
dsimp at fcomm,
simp_rw C.id_after at fcomm,
have xx, from (λ j, congr_fun fcomm j),
dsimp only at xx,
exact xx,
end⟩)
sorry
-- -/

--- super slow version (same as above, but s/dunfold/delta)
/-
theorem cone_to_FtoX_full {J C : cat} (F : Funct J C) : full (conecat_to_FtoXcat F) := full.mk
(λ c c' f, ⟨f.sourcef,begin
have fcomm, from f.comm,
delta conecat_to_FtoXcat at fcomm,
delta Diagonal at fcomm,
delta objFunct at fcomm,
dsimp at fcomm,
delta comm_square at fcomm,
delta FunctCat at fcomm,
dsimp at fcomm,
delta NTseq at fcomm,
dsimp at fcomm,
delta NTId at fcomm,
dsimp at fcomm,
simp_rw C.id_after at fcomm,
have xx, from (λ j, congr_fun fcomm j),
dsimp only at xx,
exact xx,
end⟩)
sorry
-/

[Tsvi Benson-Tilsen]

Not sure how to boil this down to a small example.

[Tsvi Benson-Tilsen]

No I didn't know about #lint, thanks, I'll try that out!

[Kevin Buzzard]

These multiple dunfolds in proofs indicate to me that you are missing some API.

[Tsvi Benson-Tilsen]

API? Do you mean something like, if I define bar in terms of foo, and then baz in terms of bar, I should also define baz in an elementary way, and then prove that the definitions are equivalent, so that I don't have to unpack all the way to foo when dealing with baz?

[Tsvi Benson-Tilsen]

And like prove lemmas about baz?

[Kevin Buzzard]

I have not looked at your code in detail, but my gut feeling is that

dunfold conecat_to_FtoXcat at fcomm,
dunfold Diagonal at fcomm,
dunfold objFunct at fcomm,
dsimp at fcomm,

should be replaced with rw how_it_started_eq_how_it_ends at fcomm where how_it_started_eq_how_it_ends is an independent lemma proved beforehand with refl.