problems with aesop

Stream: homology

[Joël Riou]

Adam Topaz said:

Unfortunately Indexed C is a little "evil"... ext for its Homs would involve HEq or eqToHoms

In order to prove the map_id and map_comp fields of the functor cechSimplicial, I did not use an ext lemma (which would indeed involve eqToHom), because congr worked (because the maps on indices were defeq!)

[Adam Topaz]

Yes, I see that. But unfortunately that means that aesop_cat won't be too useful in this context.

[Joël Riou]

aesop_cat does a great job in general, but it cannot prove everything!

[Adam Topaz]

I know, but this is concrete enough that I feel like it should be able to do a lot.

[Joël Riou]

With a suitable hom_ext lemma, aesop_cat fails, but ext <;> simp works!

[Kim Morrison]

Do you know what it tries instead? Something is going wrong if aesop_cat is missing ext <;> simp proofs!

[Joël Riou]

I have tried this:

noncomputable def cechSimplicial {I : Type w} (U : I → C) [HasFiniteProducts C] :
    SimplicialObject (FormalCoproduct C) where
  obj := fun Δ ↦
    { I := Fin (Δ.unop.len + 1) → I
      obj := fun a ↦ ∏ᶜ (fun x ↦ U (a x)) }
  map {Δ Δ'} f :=
    { f := fun a x ↦ a (f.unop.toOrderHom x)
      φ := fun a ↦ Pi.map' (fun x ↦ f.unop.toOrderHom x) (fun x ↦ 𝟙 _) }
  map_id _ := by ext <;> simp
  map_comp _ _ := by
    aesop (config := { warnOnNonterminal := false })
            (rule_sets := [CategoryTheory])
    simp

It seems aesop has mostly applied ext, which creates two goals, and solved the first (which is rfl), but it fails to see that the second goal can be proved by simp.

[Kim Morrison]

Joël Riou said:

I have tried this:

noncomputable def cechSimplicial {I : Type w} (U : I → C) [HasFiniteProducts C] :
    SimplicialObject (FormalCoproduct C) where
  obj := fun Δ ↦
    { I := Fin (Δ.unop.len + 1) → I
      obj := fun a ↦ ∏ᶜ (fun x ↦ U (a x)) }
  map {Δ Δ'} f :=
    { f := fun a x ↦ a (f.unop.toOrderHom x)
      φ := fun a ↦ Pi.map' (fun x ↦ f.unop.toOrderHom x) (fun x ↦ 𝟙 _) }
  map_id _ := by ext <;> simp
  map_comp _ _ := by
    aesop (config := { warnOnNonterminal := false })
            (rule_sets := [CategoryTheory])
    simp

It seems aesop has mostly applied ext, which creates two goals, and solved the first (which is rfl), but it fails to see that the second goal can be proved by simp.

@Joël Riou, is there a branch/commit you can point me to where I can take a look at this issue?

[Joël Riou]

Yes, this is the branch https://github.com/leanprover-community/mathlib4/tree/cech-experiment

[Kim Morrison]

@Jannis Limperg, I think I've identified the problem. I'm not sure if it is a bug in aesop or just suprising behaviour.

In the proof of map_id and map_comp above,

ext <;> aesop

works, as does

aesop (add safe apply hom_ext)

(hom_ext is the lemma that ext is applying), however

aesop (add safe tactic Std.Tactic.Ext.extCore')

fails, apparently because aesop doesn't continue working on both goals generated after applying the ext lemma.

If you'd like to take a look at this, please use branch#cech-experiment-aesop, and see the file Mathlib/CategoryTheory/Sites/Cech.lean, in the declaration cechSimplicial.

[Kim Morrison]

More generally, now that ext is a core lean tactic, I wonder if you would consider turning it on by default, or otherwise providing an easier hook than having to define extCore'.

[Kevin Buzzard]

Thanks for the debugging Kim!

[Jannis Limperg]

Yeah, thanks. I'm quite ill atm, so I'll take a closer look once I'm on my feet again. However, I can already say that ext is on by default in Aesop these days, so this should just work.

[Kim Morrison]

Ah! I will try to remove extCore from aesop_cat and report back.

I hope you're feeling better soon. :-(

[Kim Morrison]

Preliminary cleanup at #14843

[Kim Morrison]

And #14845, removing all the apparently unused configuration options for aesop_cat.

[Jannis Limperg]

All right, back from the dead. :) Did removing extCore fix the original issue?

[Kim Morrison]

Thanks for the reminder, I will look again in the next few days (or someone else can :-)

[Kim Morrison]

@Jannis Limperg this is still failing, after I'm merged master into cech-experiment.

The map_id field of cechSimplicial work by ext <;> simp, but does not work by aesop, despite it working (with a nonterminal warning) with

aesop
ext <;> simp

Here aesop? suggests

rename_i inst inst_1 inst_2 inst_3 inst_4 x
simp_all only [unop_id, SimplexCategory.id_toOrderHom, OrderHom.id_coe, id_eq]
sorry

which is reasonable, and again

rename_i inst inst_1 inst_2 inst_3 inst_4 x
simp_all only [unop_id, SimplexCategory.id_toOrderHom, OrderHom.id_coe, id_eq]
ext <;> simp

closes the goal.

So I think it is a bug in aesop!

[Jannis Limperg]

So this turns out to be quite a deep issue. Essentially, what happens is this:

• Aesop runs simp_all and ext. This produces two goals ?g1 and ?g2 such that ?g1 appears as a metavariable in ?g2.
• Aesop therefore doesn't treat ?g1 as a goal in its own right and only works on ?g2.
• Aesop runs simp_all on ?g2, which solves it but doesn't solve ?g1. This is forbidden, so Aesop discards the result of simp_all.
• No other rules apply to ?g2, so Aesop gives up.

I believe it would be possible to change Aesop's behaviour in step 3 such that it adds ?g1 as an additional goal to be solved. However, doing this cleanly would be a major operation and since anything metavariable-related is hell on earth, I'm inclined to leave this as a known limitation.