Schematic polymorphism

Schematic polymorphism lets terms, definitions, theorems, and specifications be parameterized by type variables. A schematic entity represents all of its monomorphic instances, obtained by replacing the type variables with ground types. Proofs are schematic in the same sense: a schematic proof works uniformly for every instance, and Abella ensures this by treating type variables as opaque during unification.

The feature is described in the paper Schematic Polymorphism in the Abella Proof Assistant. The examples on this page are drawn from examples/schm-poly/schm_poly_tst.thm.

Schematic terms and definitions

Kind introduces type constructors. The built-in list type constructor is declared as if by

Kind list type -> type.

The type expression list (list A) -> list B represents functions from lists of lists of A to lists of B.

Type introduces constants. A free type variable in the type of a constant makes the constant schematic. The built-in list constants are declared as if by

Type nil list A.
Type ::  A -> list A -> list A.

Abella provides list, nil, and ::, so these declarations must not be repeated. The type argument is inferred at each use, so X :: nil is a list whose element type is the type of X.

A definition may be schematic in the same way:

Define append : list A -> list A -> list A -> prop by
  append nil L L ;
  append (X :: L1) L2 (X :: L3) := append L1 L2 L3.

The predicate append is schematic in A. Every occurrence of append in the definition must use its most general type list A -> list A -> list A. After the definition, append may be used at any instance of A.

Schematic theorems and proofs

A theorem is schematic when it lists its type variables in brackets after the name:

Theorem append_det[A] : forall (L1 : list A) L2 L3 L3',
  append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.

The annotation on L1 fixes the type of the list and lets inference determine the rest. The proof proceeds as for the monomorphic version:

induction on 1. intros. case H1.
  case H2. search.
  case H2. apply IH to H3 H4. search.

The proof is schematic because case analysis does not inspect the structure of A. Abella's unification treats generic type variables as black boxes. If a tactic would have to choose a particular instantiation of A, it fails instead of producing a non-schematic proof.

Instantiating schematic theorems

A schematic theorem may be used at a specific type by writing the instance after its name:

Theorem oappend_det : forall (L1 : list o) L2 L3 L3',
  append L1 L2 L3 -> append L1 L2 L3' -> L3 = L3'.
intros. apply append_det[o] to H1 H2. search.

The instance may be partially specified with _, or omitted entirely when inference determines it:

apply append_det[_] to H1 H2.
apply append_det to H1 H2.

The same notation applies to any schematic lemma. For example, member_prune[o,o] fixes the two type parameters of the theorem below.

Schematic reasoning with higher-order syntax

Schematic polymorphism is especially useful with higher-order abstract syntax. The membership predicate is schematic:

Theorem member_prune[A,B] : forall M (L : list A), nabla (x : B),
  member (M x) L -> exists M', M = y\ M'.

Because L is quantified outside the nabla, it cannot contain x. The theorem says that any dependence of M x on x is vacuous. It has a schematic proof:

induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

Specific instances use the same bracket syntax, and backchain accepts it too:

apply member_prune[o,o] to H1.
backchain member_prune[o,o].

Polymorphic specifications

Schematic polymorphism also applies to specifications. A signature may declare a predicate whose type contains free type variables, and its clauses may use the predicate at its most general type. For example, a signature may declare

append.sig

sig append.

type app list A -> list A -> list A -> o.

with module

append.mod

module append.

app nil L L.
app (X :: L1) L2 (X :: L3) :- app L1 L2 L3.

Each clause is schematic in A. A development can then prove properties of app at a schematic type:

Specification "append".

Theorem app_search[A] : forall (X : A) L,
  {app (X :: nil) L (X :: L)}.
search.

Theorem app_det[A] : forall (L1 : list A) L2 L3 L3',
  {app L1 L2 L3} -> {app L1 L2 L3'} -> L3 = L3'.
induction on 1. intros. case H1 (keep).
  case H2. search.
  case H2. apply IH to H3 H4. search.

For case analysis on a specification judgment to be schematic, every program clause must either have no type instance unifiable with the judgment, or have a unique type-generic instance built using only the type variables of the theorem. No new type variables may be introduced by the case analysis.

Limitations

Some statements have no schematic proof because their truth depends on the type instance. For example:

Type p A -> o.

Define eq : A -> A -> prop by
  eq M M.

Theorem tst[A,B] : forall (X : A) (Y : B),
  eq (p X) (p Y) -> false.
intros. case H1.

This fails with a unification error: case analysis would have to inspect whether A and B are the same type. When they are different, the two occurrences of p cannot be unified, so the assumption is unprovable; when they are the same, it can be proved for suitable X and Y. No uniform proof exists.

A similar limitation applies to object-level case analysis. Consider a signature with a polymorphic constant used at its most general type:

pred.sig

sig pred.

kind i type.
type cst A -> i.
type pred i -> o.

pred.mod

module pred.

pred (cst X).

The type of X is not fixed by the conclusion pred M, where M : i. Case analysis therefore fails:

Theorem ty_not_fdet_left : forall M,
  {pred M} -> false.
intros. case H1.

Abella reports that it cannot fully infer the type of the program clause. Similarly, search cannot prove

Theorem ty_not_fdet_right : forall M, {pred M}.
search.

because it cannot determine the type of X from the goal.

Further reading

• The paper Schematic Polymorphism in the Abella Proof Assistant.
• examples/schm-poly/schm_poly_tst.thm in the distribution.