Automation in cslib

Stream: CSLib

[David Wegmann]

I am currently trying to understand the approaches to automation in cslib.

I am familiar with auto and eauto and the respective databases from coq, but I haven't used aesop or grind very much and I couldn't find any best practices guide or something like that.

[David Wegmann]

I tried playing around with aesop:

@[aesop safe [constructors]]
inductive ReflTransClosure {α : Type} (R : α → α → Prop) : α → α → Prop
| refl {a : α} : ReflTransClosure R a a
| step {a b c : α} : ReflTransClosure R a b → R b c → ReflTransClosure R a c

def ReflTransClosure.rel {α : Type} {R : α → α → Prop} {a b : α}
  (h : R a b) : ReflTransClosure R a b := by aesop -- aesop does not work

The code snipped above does not work.

In this next snipped it works:

@[aesop safe]
inductive ReflTransClosure {α : Type} (R : α → α → Prop) : α → α → Prop
| refl {a : α} : ReflTransClosure R a a
| step {a b c : α} : ReflTransClosure R a b → R b c → ReflTransClosure R a c

@[aesop safe]
def ReflTransClosure.refl1 {α : Type} {R : α → α → Prop} {a : α} :
  ReflTransClosure R a a := by
    apply ReflTransClosure.refl

def ReflTransClosure.rel {α : Type} {R : α → α → Prop} {a b : α}
  (h : R a b) : ReflTransClosure R a b := by aesop

Why is that? How do I correctly flag the constructors for aesop?

[Chris Henson]

In CSLib we have been primarily using grind for automation. Some things that might help:

• the locally nameless modules very closely follow a Rocq development that used auto/eauto, so it can be useful to compare. This is linked at the top of the documentation.
• There is a chapter of the reference manual about grind

It's actually been a bit since I've used aesop, so I can't answer your question off the top of my head. I will note that a grind attribute on that inductive succeeds in producing the rules you probably expect for each constructor. (And docs#Relation.ReflTransGen does so in Mathlib)

[David Wegmann]

I know, this code is not intended to go into any proof for the stlc strong norm stuff, I am just trying to replicate some stuff that I did with coq to learn aesop/grind/ other automation.

[David Wegmann]

is there a variant of grind that uses existential variables?

like auto vs eauto from coq if you know that.

[Chris Henson]

There is some subtlety about what cases are currently supported, but grind will close certain existential goals.

[Snir Broshi]

Is it only simple existentials that lia can solve? AFAIK grind refuses to solve existentials and this is on purpose

[Snir Broshi]

To kinda simulate eauto you can use ?_, and then simp I think (grind isn't really an auto, but simp is)
though it won't handle any other existentials nested inside