case_bash and automation

Stream: mathlib4

[Joël Riou]

In CategoryTheory.Category.Pairwise, there are goals which require doing cases on variables before aesop_cat can handle them. In mathlib, this was taken care of by doing attribute [local tidy] tactic.case_bash. Is there an analogue of this in mathlib4? (See https://github.com/leanprover-community/mathlib4/pull/2534/files#diff-dbac9e254ec82565831843ba6c9b622e4a210161ec9c7f4ce6d99d8e04d8571aR90-R109 for the actual example where I have manually fill the assoc/comp_id/id_comp fields.)

[Matthew Ballard]

Local attributes in aesop will be supported soon !4#2484. case_bash hasn't been ported yet but theoretically tagging appropriate types as cases rules for aesop should replace that. I couldn't get that work currently. There appears to be a bug https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Goal.20state.20not.20updating.2C.20bugs.2C.20etc.2E/near/338368889

[Adam Topaz]

Just to expand on what I think Matt is saying...

One possibility is to make a small tactic like discrete_cases
https://github.com/leanprover-community/mathlib4/blob/35dd23d0c6eb5921c1629ffb476573dc8d73b95d/Mathlib/CategoryTheory/DiscreteCategory.lean#L117
and activate it locally with aesop_cat as Matt mentioned.

[Adam Topaz]

in my experience in mathlib3, allowing tidy to case bash makes it waaaaaayyyyy too slow. I hope this approach via aesop would be better.

[Matthew Ballard]

Can you get aesop to case on morphisms in Discrete C by just tagging things?

[Adam Topaz]

yeah there is some way to do it, I think, but in the discrete case one also has to case on morphisms and unification is a bit tricky there.

[Adam Topaz]

I think the situation is similar for Pairwise and the other finite categories we have around.

[Adam Topaz]

Namely, morphisms in Discrete X are defined as ULift (PLift (a = b)), but lean would have a hard time understanding that a \hom b is indeed this ulift of a plift.

[Adam Topaz]

Similarly for Pairwise, the homs are defined as an inductive type called Pairwise.Hom or something, so lean still needs some hints because the usual spelling is a \hom b and not Pairwise.Hom a b.

[Adam Topaz]

another approach is to redefine the induction principle for homs with the right spelling, and train aesop to apply this induction principle.

[Matthew Ballard]

Can we make some basic api like

theorem DiscreteMorphism.toULiftOfPLift (f : a \hom b) : ULift (PLift (a = b)) := f

and then feed it to aesop_cat as a simp rule

[Matthew Ballard]

I’ve tried custom automation and no automation and neither are great for me

[Adam Topaz]

I think the lemma docs4#CategoryTheory.Discrete.eqToHom is essentially what we want here

[Adam Topaz]

but this wouldn't work on a hypothesis, only a goal.

[Matthew Ballard]

So the only rule type in aesop that operates on hypotheses is cases?

[Adam Topaz]

We would have to ask @Jannis Limperg ;)

[Adam Topaz]

I would assume that aesop can also simplify hypotheses but I don't think that would be helpful in this case.

[Adam Topaz]

Maybe there is a way to tell aesop to apply custom induction principles? That would apply in this case

[Jannis Limperg]

Aesop rules that operate on hypotheses are forward, destruct and simp/unfold (and tactic obvs). See here. Do any of these work for you?

[Jannis Limperg]

Adam Topaz said:

Maybe there is a way to tell aesop to apply custom induction principles? That would apply in this case

Not at the moment. I thought this could always be done with destruct, but in the presence of dependencies, that's not true. I'll look into it.

[Matthew Ballard]

Thanks. It takes some time for things to penetrate my skull and take root. This helps.