Aesop cases

Stream: general

[Bolton Bailey]

Why does Aesop work with the cases call below, but not without it? In the Aesop paper, cases is described as one of the safe rules. Is there something I have to do to get Aesop to look at casing?

import Mathlib.Data.Fin.Basic

set_option trace.aesop.steps true

lemma Fin.zero_false (a : Fin 0) : False := by
  -- cases a
  aesop

[Bolton Bailey]

Does the definition of Fin need to be annotated perhaps?

[Jannis Limperg]

Yes, you have to add cases rules if you want Aesop to perform case analysis on a particular type. This annotation, for example, instructs Aesop to run cases on each hypothesis h : Fin n and to consider this a safe rule (i.e., to do it eagerly without backtracking):

import Mathlib.Data.Fin.Basic

attribute [aesop safe cases] Fin

lemma Fin.zero_false (a : Fin 0) : False := by
  aesop

[Jannis Limperg]

However, this may be a bit too aggressive. A more conservative setup would be this:

import Mathlib.Data.Fin.Basic

@[aesop safe destruct]
lemma Fin.zero_false (a : Fin 0) : False := by
  cases a; aesop

example (h : Fin 0) (_ : True) : False := by
  aesop

[Bolton Bailey]

Cool! Out of curiosity, why do you consider it too aggressive? Is it that it slows down the tactic to add too many of these?

[Eric Rodriguez]

I'd assume you don't really want to case on every Fin

[Bolton Bailey]

But why not? A fin just consists of a Nat and a < - it seems like it would be convenient to always just decompose where possible and then only have to worry about the ability of Aesop to prove things about Nats.

[Bolton Bailey]

Is there an example where the aggressive Fin casing would cause Aesop to fail, where it would succeed without the Fin casing?

[Yakov Pechersky]

It's not just that subtype, it has a different ring structure

[Bolton Bailey]

So I guess you're saying if I wanted to prove something like

lemma (n : Nat) (a b c : fin N) : a * (b * c) = (a * b) * c := sorry

then the decomposition would be inconvenient, I guess that makes sense.

[Scott Morrison]

Fin really should not be a Ring, but anyway... :-)

Blind caseing gets very expensive. tidy used to do more case bashing by default than aesop, and this was the origin of many performance problems.

[Bolton Bailey]

I certainly have often had the experience of a tidycall running forever. On the other hand, I'd prefer a tactic that is unperformant over one that gives up too early.

Is there any way to make safe rules that are applied lazily/with low priority/only if all other options fail?

[Yakov Pechersky]

I used Ring as a shorthand -- whether or not it has modular addition or saturating addition, it's still a different enough structure that breaking it down to the deconstructed subtype tuples might be the "long way around"

[Jannis Limperg]

My intuition (mostly untested) is that the following would be a good process for developing a library with Aesop:

• While developing the API for a type, say Fin, locally add Aesop lemmas that reduce Fin to more primitive notions. Then Aesop can hopefully make progress on the API lemmas. In more complex cases, it may be appropriate to define a rule set for this reduction.
• Once the API is developed, go back and tag likely-useful API lemmas as global rules.

Downstream proofs involving Fin will then hopefully need only the API lemmas. If they need to break the Fin abstraction, corresponding Aesop rules can be added locally again, but this should perhaps be considered a code smell.