Computation-as-deduction in Abella

13 views

Skip to first unread message

Ulysse Gérard

unread,

May 7, 2018, 10:01:37 AM5/7/18

to Abella

Dear all,

In a recent paper , we proposed a small extension to Abella that would allow it to automate some proof search by following the focusing discipline.

In this report we introduce a new tactic compute that repeatedly unfolds a definition and handles the resulting subgoals eagerly as long as they are invertible (asynchronous in focusing terminology).

For example, if we had an assumption

H : plus (s z) (s z) X

then the invocation of compute H would repeatedly unfold the definition of plus and handle the resulting subgoals eagerly if it can, using purely asynchronous steps, eventually removing H and instantiating X with (s (s z)).

But for a predicate that cannot be fully solved like H : nat (s (s X)) one wants more control than just eagerly unfolding to prevent non-terminating search. To solve this problem we also introduce the Suspend declaration that will make Abella stop the asynchronous phase prematurely when certain arguments are variables. For example, Suspend nat X on X.

The compute tactic is allowed to branch and this branching tree can grow quickly. When computing a function all these branches should lead to the same result. Thus we also provide a way to make the computation deterministic in that setting. Given the following definition of singleton :

Define singleton : (A → prop) → prop by singleton P :=

(exists X, P X) ∧

(forall X Y,P X → P Y → X=Y).

Then, if the following theorem holds

Theorem plus_funct: forall X Y, nat X → nat Y → singleton (plus X Y).

the compute tactic applied to plus would eagerly prune the conjunctive branches caused by unfolding the singleton predicate.

You can find more details on our proposal in the draft.

This kind of feature has long been recognized as an important need and we hope that this is a good first step toward the automation of Abella.