Adding user command to explore higher-order unification

[ThatDaleMiller]

There are lots of formulas that are theorems of G but which are not provable in Abella since Abella doesn't implement full higher-order unification (which is actually a requirement of the inference rules for G). For a simple example of a non-Abella provable theorem (similar to those mentioned before):

Kind i   type.
Type f   i -> i.

Theorem prune: forall (A : i -> i -> i),
   nabla x y, A x (f x) = A x y -> exists A', A = (x\y\ A' x).

I propose that we should add user-level commands that allow higher-order unification to be explored by the user directly. For example, we should consider adding three new commands to Abella: match, simplify (using Huet's terminology), and prune. These would take one hypothesis label as an argument. (Prune is based on the improper factors described in section 11 of my mixed prefix unification paper).

People will always want to move beyond the pattern fragment, especially since G is based on the richer notion of higher-order unification. Providing such tacticals would be good for that. Actually, the simplication tactic might always be operated automatically. The match tactic might cause multiple cases to be explored (since different factors of unifiers are suggested by the project/imitation search steps in Huet's paper). A fourth command might also be useful for terminating a proof when the equation being processed satisfies the "rigid-path" check (generalized occur checking).

[ThatDaleMiller]

Follow on email discussion raised the point that Abella will already allow exploring higher-order unification for non-pattern unification problems. The case statement can explore the match substitutions directly. Thus, the following works in Abella now.

Kind i  type.
Type g i -> i -> i.
Type e i.

Theorem test : forall (F : i -> i),
                       F e = (g e e) -> (F = x\ g e e) \/(F = x\ g x e) \/
                                        (F = x\ g e x) \/(F = x\ g x x).
intros.
  case H1. % imitation
    case H2. % imitation and projection
      case H3. % ditto
         search. % imitation on H3 and H2
         search. % imitation on H2, proj on H3
      case H3.
         search. % proj on H2, imit on H3
     search. % proj on H2 and H3     

The following example illustrates how unification can encode operations on lists built using function composition (this goes back at least to Huet's proof of undecidability of 3-order unification). Most of the case commands are used to explore Huet's match tree.

Type u, v    i -> i.

Define answer1 : (i -> i) -> (i -> i) -> prop by
  answer1 (w\ w) (w\ u (v w)) ;
  answer1 (w\ u w) (w\ v w) ;
  answer1 (w\ u (v w)) (w\w).

Theorem test2 : forall X (Y : i -> i), (nabla w, (X (Y w)) = (u (v w))) -> answer1 X Y.
  intros eq. eq : case eq. eq : case eq.eq : case eq.eq : case eq. search. search. search.

Thus, from my original issue post, the only thing missing is a means to compute and apply some forms of pruning.