Proof by Higher-order unification

Higher-order unification

Calculate a unifier (replacement for schematic variables) for two higher-order terms, e.g.

Rule: ?P => ?Q => ?P /\ ?Q

Goal: (a > b) /\ (b > c)

Unifier: ?P = a > b, ?Q = b > c

New goal: a > b and b > c

Backward Proof

Intuition for backward proof:

$$\frac{A\Rightarrow B(H\Rightarrow B^{\prime })\Rightarrow C{B}^{\prime }\theta =B\theta }{(H\Rightarrow A)\Rightarrow C}$$

Full rule:

$$\frac{A\Rightarrow B\left(\forall \vec{x}.\vec{H}\vec{x}\Rightarrow B^{\prime }\right)\Rightarrow C\left(\lambda \vec{x}.B\vec{x}\right)\theta =B^{\prime }\theta }{\left(\forall \vec{x}.\vec{H}\vec{x}\Rightarrow A\vec{x}\right)\theta \Rightarrow C\theta }$$

Forward Proof

Isabelle itself does not support forward proof by solely using higher-order unification.

The of / OF methods can instantiate schematic variables in a term / a proven theorem.

$$\frac{A=\left(H\Rightarrow B^{\prime }\Rightarrow C\right)B^{\prime }\theta =B\theta }{A\text{OF}B=\left(H\Rightarrow C\right)\theta }$$

With Hoare Logic?

Enhanced sequence rule:

$$\frac{\{P\}{C}_1\{Q\}\{Q^{\prime }\}{C}_2\{R\}Q\theta =R\theta }{\{P\theta \}{C}_1;C_2\{R\theta \}}$$