Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts

Coinduction is a proof rule, it is the dual of induction. It allows reasoni ng about non-well-founded structures such as lazy lists or streams and is o f particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called a b isimulation). We present an automation of coinductive theorem proving. This automation is based on the idea of proof planning [7]. Proof planning constructs the hig her level steps in a proof. using knowledge of the general structure of a f amily of proofs and exploiting this knowledge to control the proof search. Part of proof planning involves the use of failure information to modify th e plan by the use of a proof critic [23] which exploits the information gai ned from the failed proof attempt. Our approach to the problem was to develop a strategy that makes an initial simple guess at a bisimulation and then uses generalisation techniques, mo tivated by a critic, to refine this guess, so that a larger class of coindu ctive problems can be automatically verified. The implementation of this strategy has focused on the use of coinduction t o prove the equivalence of programs in a small lazy functional language whi ch is similar to Haskell [22]. We have developed a proof plan for coinduction acid a critic associated wit h this proof plan. These have been implemented in (CoCLM)-M-A, an extended version of (CLM)-M-A [9], with encouraging results. The planner has been su ccessfully tested on a number of theorems.