Metamathematics in Coq

Chapter 1: Automated Proof Construction in Type Theory using Resolution. We describe techniques to integrate resolution logic in type theory. Refutation proofs obtained by resolution are translated into lambda-terms, using reflection and an encoding of resolution proofs in minimal logic. Thereby we obtain a verification procedure for resolution proofs, and, more importantly, we add the power of resolution theorem provers to interactive proof construction systems based on type theory. We introduce a novel representation of clauses in minimal logic such that the lambda-representation of resolution steps is linear in the size of the premisses. A clausification algorithm, equipped with a correctness proof, is encoded in Coq. Chapter 2: Proof Reflection in Coq. Natural deduction for first-order logic is formalised in the proof assistant Coq, using de Bruijn indices for variable binding. The main judgement is of the form G |- d [:] p, stating that d is a proof term of formula p under hypotheses G; it can be viewed as a typing relation by the Curry-Howard isomorphism. This relation is proved sound with respect to Coq's native logic and is amenable to the manipulation of formulas and of derivations. As an illustration, I define a reduction relation on proof terms with permutative conversions and prove the property of subject reduction. Chapter 3: Adbmal To make the notion of scope in the lambda-calculus explicit, we extend the syntax of the lambda-calculus with an end-of-scope operator adbmal. The idea is that an adbmal x ends the scope of the matching lambda x above it (in the term tree). Accordingly, beta-reduction is extended to the set of scoped lambda-terms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped $\beta$-reduction. Confluence of beta-reduction for the ordinary lambda-calculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, alpha-equivalence is needed. All our proofs have been verified in Coq