Solving simple goals with aesop

[suhr]

I have the following definition:

def spec (w : Nat → State) : Prop :=
  (init $ w 0) ∧ (∀t : Nat, w t = w (t+1) ∨ next (w t) (w $ t+1))

And want to use Aesop to solve something very simple:

theorem aesop_proj1 (w : Nat → State) (sp : spec w) : (init $ w 0) :=
by aesop (safe [sp, spec])

theorem aesop_proj2 (w : Nat → State) (sp : spec w) :
  (∀t : Nat, w t = w (t+1) ∨ next (w t) (w $ t+1)) :=
by aesop (safe [sp, spec])

Unfortunately, this does not work:

aesop: failed to prove the goal

I know that Aesop is WIP, but proving anything about distributed systems without any kind of logical automation is not great. So I'm trying to use it.

[JLimperg]

Very happy to have someone try out the tactic! Could you provide a working example? Then I can check what prevents Aesop from solving your goals.

In general, Aesop's default rules are quite haphazard right now, so you're likely to run into many simple goals that it can't solve. Reports about these are very welcome.

[suhr]

Sure, there it is: https://gist.github.com/suhr/aec6bcb760191c18ee07c729fbf3458e. It's pretty much a formalization of OneBit mutex from Lamport's Hyperbook.

[suhr]

Now aesop (add norm unfold spec) solves this.