A formal approach to some usually informal techniques used in mathematical reasoning

Abstract

One of the striking characteristics of mathematical reasoning is the contrast between the formal aspects of mathematical truth and the informal character of the ways to that truth. Among the many important and usually informal mathematical activities we are interested by proof analogy (i.e. common pattern between proofs of different theorems) in the context of interactive theorem proving. In some sense we propose a partial contribution of one of the Polya's wishes [Polya 73]: "Analogy pervades all our thinking, our everyday speech and our trivial conclusions as well as artistic way of expression and the highest scientific achievements..but analogy may reach the level of mathematical precision.." It is a work in philosophy of mathematics [Resnik 75], in which mathematics is viewed as studying patterns or structures, which encouraged us to pursue our aim of partially formalizing analogy. We naturally arrived at the need of considering other activities strongly tied to the notion of analogy and very well known of the working mathematician: generalization, abstraction and analysis of proofs. We propose a method to deal with proof analogy in interactive theorem proving where the paradigm of "proposition as types" is adopted, proofs are represented as terms and a higher-order language L is available to the user. Let us assume that the user has to prove a conjecture C. Given a proof P for a known theorem T, he describes in the language L a scheme of P. Then he expresses the syntactic analogy he views as relevant between the scheme of P and what "should be" a proof scheme for C, as a transformation rule. This process needs analysis of proofs, generalization and abstraction. A second order pattern matching algorithm constructs matchers of P and its scheme, and applies them to the intended proof scheme of the conjecture C. In the best case one obtains a potential proof of C, but in general one obtains a more instantiated proof-scheme with some "holes" to be filled by a theorem prover. In both cases a proof-checking process is necessary (analogy is in general a heuristic way of thinking). A question arises naturally: "What to do when the assumed analogy fails?". We study in this paper one of the possible answers: "Information may be extracted from the failure in order to suggest lemmas that try to semantically restore analogy". Of course these lemmas can also serve for detecting wrong analogies (for example, if required lemmas clearly cannot be theorems). Two kinds of failure are possible:i)The given proof P and its proposed scheme are not matchable.ii)A type error is detected in the instantiated proof scheme for C. We give in the following a method to suggest lemmas in the first case, and sketch some ideas of how to use such a possibility in the second case.