unfold n and unfold with

[Todd Wilson]

I recently started making use of named specification clauses so that I can debug `search` failures using `unfold`. I have two questions regarding this feature.

1. Is there any reason why we can't use notation like `unfold 5` on a goal like `{G |- of ...}`

to refer to the 5th clause of the of predicate instead of having to name the clauses in the specification?

Note that the witness grammar already includes `unfold(of,5,...)`, although I recognize that clauses are renumbered for the purpose of witnesses when hypotheticals are added dynamically to the beginning of the sequence, which itself creates some confusion. One suggestion here is to use negative clause numbers for dynamic additions to the clause database, so that specification clauses always retain their original numbers.

2. I've been getting some "Unsolvable unification of head of program clause" errors when attempting unfolds that involve higher-order patterns in program clauses. For example, here is the type-application rule from System F:

    %:tapp:

    of (tapp P E) (T P) :- typ P, of E (all T).

Assuming I've diagnosed the problem correctly, it would be nice if I could do something like `unfold tapp with T = ....` to help out with the unification. In the absence of this feature, is there any workaround?

Todd Wilson

California State University, Fresno

[Kaustuv Chaudhuri]

On Tue, May 11, 2021 at 2:45 AM Todd Wilson <lambdaca...@gmail.com> wrote:

1. Is there any reason why we can't use notation like `unfold 5` on a goal like `{G |- of ...}`

to refer to the 5th clause of the of predicate instead of having to name the clauses in the specification?

Note that the witness grammar already includes `unfold(of,5,...)`, although I recognize that clauses are renumbered for the purpose of witnesses when hypotheticals are added dynamically to the beginning of the sequence, which itself creates some confusion. One suggestion here is to use negative clause numbers for dynamic additions to the clause database, so that specification clauses always retain their original numbers.

I think you've already correctly deduced why we don't allow numbering of the clauses because the system doesn't distinguish between program clauses and dynamic clauses when performing a backchaining step.

I'm a bit hesitant to introduce negative numbers for just the unfold tactic into the grammar. It seems easier to just number the clauses from oldest to youngest in declaration order. Note that this order may not be easily predictable from the text because of accumulate, but internally there is a canonical declaration order.

By the way, the more arbitrary numbers you introduce into your proofs, the harder it becomes to maintain them. Named clauses are at least a little more robust to simple changes such as reordering or extending the clauses.

2. I've been getting some "Unsolvable unification of head of program clause" errors when attempting unfolds that involve higher-order patterns in program clauses. For example, here is the type-application rule from System F:

    %:tapp:

    of (tapp P E) (T P) :- typ P, of E (all T).

Assuming I've diagnosed the problem correctly, it would be nice if I could do something like `unfold tapp with T = ....` to help out with the unification. In the absence of this feature, is there any workaround?

I believe 'unfold ... with ...' has been considered before, but its general semantics is unclear because the with parameters can affect clause selection -- e.g., by making a certain clause unselectable because its head doesn't match.

Maybe in this specific case it can make sense because the clause has been selected by its name already.

Tracking this in: https://github.com/abella-prover/abella/issues/135

Kaustuv

[Todd Wilson]

On Monday, May 10, 2021 at 11:34:15 PM UTC-7 Kaustuv Chaudhuri wrote:

I'm a bit hesitant to introduce negative numbers for just the unfold tactic into the grammar. It seems easier to just number the clauses from oldest to youngest in declaration order. Note that this order may not be easily predictable from the text because of accumulate, but internally there is a canonical declaration order.

By the way, the more arbitrary numbers you introduce into your proofs, the harder it becomes to maintain them. Named clauses are at least a little more robust to simple changes such as reordering or extending the clauses.

I also considered suggesting this reverse ordering, but thought that a separate namespace for dynamic clauses would be better. Maybe using a disjoint-union type would make more sense, so the natural program order can be maintained. I agree that `accumulate` complicates matters and that it's better to minimize "magic numbers" in proofs, but I guessed there was enough reason to include them into (non-portable) witnesses that it might make sense here, too. If some kind of disjoint-union type is not feasible, though, then my preference would be for the reverse ordering over shifting clause numbers up as new dynamic clauses are added. Here are a couple other related thoughts:

• If a clause is named, perhaps that name could be used in the witness instead of a number.
• Similarly to the `Show <thm-name>` command, you could have a `List <pred-name>` command that would list the clauses for a given predicate along with their numbers/names so that they could be inspected before an `unfold` application or after a witness is printed out (or indeed just as an alternative to going back to look at the specification to confirm argument ordering, subgoals, etc.).

As a aside, witnesses are one of the features that I have my students turn on for all of their developments (along with instantiations), with the request that they read and check each one, because, in the absence of this, they tend to follow every tactic invocation with a mindless `search` just to see if their subgoal gets proved without actually understanding what's going on. (Just like the way students will recompile their programs again and again after every minor edit when diagnosing compiler errors instead of stepping back and trying to understand the situation.)

 

I believe 'unfold ... with ...' has been considered before, but its general semantics is unclear because the with parameters can affect clause selection -- e.g., by making a certain clause unselectable because its head doesn't match.

Maybe in this specific case it can make sense because the clause has been selected by its name already.

Tracking this in: https://github.com/abella-prover/abella/issues/135

Thanks.