The 4-color theorem is very particular because its proof is too big to be described by conventional means (and thus on paper) ; techniques of computational reflection are therefore mandatory. I will describe the formalization attempt undertaken in Coq.
Joint work with Georges Gonthier and Vincent Danos.
Our formalization of graph theory is driven by the following motivations: First of all we want to demonstrate the feasability of computer assisted proofs in an area that is overloaded with pictoral intuition. Second, we want to lay the foundations for some further applications. To this aim we start a comparable small experiment, a formal proof of the five colour theorem, which uses some similar proof principles and graph theoretic background theory as the famous four colour theorem, but it is by far less complicated. In this context we emphasize the advantage of a readable proof format which is facilitated by Markus Wenzel's interface to Isabelle, the Isar proof language.
We present a theory of undirected planar graphs based on an inductive definition of triangulations, which was proposed by Freek Wiedijk. Finally we discuss some details of a readable formal proof of the five colour theorem.
Adequate formal support for abstract mathematical structures (think groups, rings, categories etc.) has been an issue of ongoing research over many years, both in algebraic specification and theorem proving. The present work does *not* aim for all-inclusive answers here. Instead we strive to turn several existing concepts that have emerged from the Isabelle/Isar environment into a viable platform for (intelligible) formal reasoning with mathematical structures. Thus we essentially extend the existing Isar framework for human-readable proof documents towards mathematical applications at a larger scale.
The main ingredients of our structuring concepts are as follows.
We present a formal proof (at the implementation level) of an efficient algorithm proposed by Paul Zimmermann [1] to compute square roots of arbitrary large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library (GMP) is completely proven within the Coq system. Proofs are developed using the Correctness tool to deal with imperative features of the program.
This work can be decomposed into two parts. We first develop a proof of the algorithm in which values are plain integers (Z) and we do not consider any memory management issues. From this "abstract" formalization, we then build a more concrete one. Here, numbers are bounded and encoded in memory segments.
The specification and formal proof of the actual implementation of the algorithm can be decomposed as follows:
The formalization is rather large (more than 13 000 lines). As far as we know, this program is among the largest ones that have been proven using the Correctness tool. Because of the size of this formalization, the present work raises the issues of proof management and proof reuse. Consequently, we propose some ideas to simplify proof development.
[1] Paul Zimmermann, A proof of GMP fast division and square root implementations, Septembre 2000.
We present a constructive formalization of the the Fundamental Theorem of Calculus (FTC), which states that differentiation and integration are inverse processes. This formalization is built upon the library of constructive algebra created in the FTA project, which is extended with results about the real numbers namely about (power) series. Two important issues that arose in this formalization and which will be discussed in more detail are partial functions (different ways of dealing with this concept and the advantages of each different approach) and the high level tactics that were developed in parallel with the formalization (which automate several routine procedures using both Hints and Reflection mechanisms). We will also discuss the differences between formalizing constructive Bishop-style analysis and classical analysis by looking at one simple example.
The While imperative language is extended with a new assignment instruction 'x := random' meaning variable 'x' receives the result of a given random number generator. Dexter Kozen (1981) showed denotation for programs are measure transformations. We show that Hoare's Axiomatic Semantics can be extended in a conservative way, where bounded positive measures replace memory states, provided formulas are built on atomic relations between (measured) functions, such as 'f <= g'. Our framework embeds the classical one ; correctness and completeness issues altogether with w(l)p computations and examples will be presented. This study is formalized as a Coq contribution.
When programming with dependent types, both case analysis of pattern variables and abstraction over intermediate computations affect not only flow of control but also type information. The conventional pattern matching syntax for functional programming was not designed to cope with this additional subtlety and is, we claim, unsuited to it.
We re-analyse the construction of the left-hand sides of functional programs in the pattern matching style, presenting the stepwise analysis of a function's arguments as a `decision tree'. Each node in this tree represents the acquisition of more information in the decision-making process and corresponds directly to the application of a `left rule' in a sequent-style presentation; each leaf explains how to compute the relevant return value, given the information so acquired.
Conventional case analysis becomes one kind of node, suitably generalised to allow admissible notions of pattern matching. The abstraction of intermediate computations (i.e. cut) becomes another kind of node, allowing access to additional information without leaving `the left', and vastly generalising the existing notion of `boolean guard'. Combined, the two provide a powerful basis for programming with dependent types.
Taking as a basis the `decision tree' analysis of `The Left', we show how a dependently typed language readily supports and generalises Wadler's notion of `view'. An admissible notion of matching for a datatype T is given by an inductive family, V : T -> Type, whose constructors give the generators of the view, together with a `covering function', v : (t:T)V t. Matching a given t with respect to this view is just (i) abstracting (v t), then (ii) constructor analysis on the resulting value, crucially exploiting our new freedom to mix `cut' with `case'.
By way of exhibiting the formidable power of this technique, we write a non-constructor view of terms in the simply-typed lambda-calculus---they are `well-typed' or `ill-typed'. Not only is this a quite transparent piece of code, it is, ipso facto, a proof that typechecking is decidable.
Joint work with Andreas Abel.
We introduce a core language for programming with dependent types which evaluates recursion lazily such that conversion and type checking is decidable in any total subtheory.
The aim of this work is to build a type system and a lambda model which characterize completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms.
A theory of observational equivalence for simply typed lambda-calculus is developed. This allows to establish a reduction of the higher-order matching problem to the dual interpolation problem.
(joint work with Andreas Abel)
Two notions of (co-)inductive constructors of rank 2 are compared in the framework of system F_omega. Both come with (co-)iteration but differ in the definition of monotonicity for the underlying operators whose fixed-points are studied. One definition even works uniformly for all finite kinds (a preliminary version has been presented at TYPES 2000), the other (presented at CSL 2001) is only designed for the pure kind of rank 2 but has a more perspicuous reduction behaviour.
It will be shown that both definitions of monotonicity are logically equivalent, that for certain positive rank 2 operators one can even simulate the reduction behaviour and, in a case study, how to program and reason in these two nevertheless very different approaches.
The co-inductive objects in Coq are define by a co-recursion schema. In this schema syntactic restrictions on the acceptable definitions are imposed. As a consequence several natural definitions of co-inductive objects cannot be used and reformulations are necessary.
In this talk we present a general methodology, based on metric spaces, that can be used to overcome the syntactic restrictions.
This is a work in progress in collaboration with Pietro Di Gianantonio
A monadic-style translation of a simply typed lambda calculus with positive inductive and coinductive types is presented which can be used as a generic tool for assigning a semantics to languages with both (co)inductive types and impure features such as control and state.
The implicit universe hierarchy implemented in proof assistants such as Coq and Lego, although really needed, is painful, both for the implementer and the user: it interacts badly with modularity features, errors are difficult to report and to understand. Moreover, type-checking is quite complex.
We address these issues with a new calculus, the Explicit Polymorphic Extended Calculus of Constructions. EPECC is a conservative extension of Luo's ECC with universe variables and explicit universe constraints declarations. EPECC behaves better with respect to error reporting and modularity than implicit universes, and also enjoys good metatheoretical properties, notably strong normalization and Church-Rosser properties. Type-inference and type-checking in EPECC are decidable. A prototype implementation is available.
General recursive algorithms satisfy no syntactic condition that guarantees termination and therefore there is no direct way of formalising such algorithms in type theory. On the other hand, functional programming impose no restrictions on recursive programs, and then writing a general recursive algorithm is straightforward. However, there is no powerful framework that allows us to reason about the correctness of functional programs.
The goal of this talk is to present a method that combines the advantages of both programming styles when formalising general recursive algorithms. In this way, a short algorithm that can be proven correct by using the expressive power of type theory would be obtained.
Part of this work is a joint work with Venanzio Capretta.
Joint work with Antonia Balaa.
Describing recursive functions in inductive type theories has become rather easy when the structure of the recursive functions follows the inductive structure of the data types on which the computation is performed. On the other hand, general recursive functions usually rely on the accessibility predicate and well-founded induction. In this approach difficult concepts, such as dependently typed pattern matching are often unavoidable. This make programming in type theory further remote from the usual practice in functional programming.
We propose and describe a technique to construct general recursive functions that makes a step towards the usual style of programming in languages à la ML. This technique is based on the following steps:
The proof steps in this technique can often be automatized, so that this technique can really be made accessible to a wider community. This technique also has nice properties with respect to extraction, which we will discuss.
Coercive subtyping is a general approach to subtyping, inheritance and abbreviation in dependent type theories. A vital requirement for coercive subtyping is that of coherence - computational uniqueness of coercions between any two types. In this talk, we develop techniques useful in proving coherence and its related result on admissibility of transitivity and substitution. In particular, we consider suitable subtyping rules for Pi-types and Sigma-types and prove its coherence and the admissibility of substitution and transitivity rules at the type level in the coercive subtyping framework.
Previous approaches to subtyping for ML-like languages introduce a subtyping relation with the idea that an object of a subtype can be considered as an object of the supertype. We present a novel approach based on coercions, borrowing ideas that have been successfully applied to proof development in Type Theory. The basic idea behind this is that we extend a language using a set of user-defined and derived coercion functions such that a term can be used in all places where some coercion function applied to this term is valid. The subtyping relation is then a derived notion. Semantic interpretation is given by means of transformation into the original language, which also provides nice properties of the extended language. In addition to the typing rules we give a sound and complete type checking algorithm derived from W. We see this work as a step towards bridging the gap between ML-like functional programming and dependently typed programming.
A basic mechanism to improve the usability of functional programing languages is to enhance their type systems with a subtyping relation on the set of types, enforcing at the same time a subsumption rule stating that a term of type A is also of type B whenever A is a subtype of B.
Constructor subtyping [1] is a basic form of subtyping, in which an inductive type A is viewed as a subtype of another type B if B has more inhabitants than A, or in other words, the set of constructors of A is included in the set of constructors of B. To this end, constructor subtyping combines subtyping between datatypes and overloading of constructors. In order to maintain properties such as subject reduction and confluence of reductions in the resulting system one needs to constrain the overloading of constructors to strict overloading [1], a form of guaranteeing covariance between domain and co-domain of overloaded constructors.
The overloading of constructors becomes also an issue at type inference for these subtyping systems. In the presence of simple subtyping, Mitchell shows in [2] how to find a most general typing judgment to describe the set of possible typings of a term. However with constructor subtyping there is no minimal typing to a term and so, instead of a most general typing judgment, type inference should produce a set of most general typings describing all possible typings to a term.
In this work, we address the problem of finding most general typings to a term and propose a two steps method for solving it. Given a term, at a first step one produces a set of annotated terms, resulting from all possible type annotations to constructors and case-expressions occurring in it. The produced terms can then be taken and typed without constructor overloading and, following Mitchell's subtyping ideas in [2], a most general typing judgment for each of these terms can now be generated. We show that this method is a correct and complete way of generating a set of most general typings to a term.
The main issues raised in the extension of Mitchell's ideas to these subtyping systems are related to the presence of parametric datatypes as a basic type constructor. In extending such ideas, one needs also to take into account the presence of a partial order on datatypes, induced by the constructor subtyping mechanism, as well as the presence of case-expressions built over datatypes.
[1] G. Barthe and M.J. Frade. Constructor subtyping. In D. Swiestra, editor, Proceedings of ESOP'99, volume 1576 of Lecture Notes in Computer Science, pages 109--127. Springer-Verlag, 1999.
[2] John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3):245--286, July 1991.
Joint Work with Gilles Barthe (INRIA-Sophia Antipolis) and Luis Pinto (Dep. Matematica, Univ. Minho).
Focus is a methodology for formal specification and stepwise development of distributed systems. In this paper, an approach is proposed to support Focus using the type theoretical proof assistant Coq. Compared with existing mechanical supports of Focus, this paper works with only finite traces. It shows that finite trace is sufficient for both saftyness and liveliness. The approach is deliberately designed to exploit the computational mechanism intrinsic to type theory so that many cases can be proved automatically by computation. A simplified version of sliding window protocol is used as an illustrating example.
Current type theory based proof assistants are oriented towards helping expert type theorists build proofs efficiently, and they are successful in this goal, but they do not appear suitable for use in less specialist settings. But we believe that users in particular domains can share the benefits of type theory without needing to know much type theory.
This paper presents an approach for verification of properties in some application domain based on a type-theoretic logic framework LF. In our approach, users work on a domain specific interface that is familiar to them, not on a proof assistant directly; the proof assistant is hidden beneath the interface. The interface presents a proof system of the domain through a user-oriented syntax. The domain concepts are formalised in the type-theory UTT which is based on LF. Relevant tools bridge the interface and the LF implementation system Plastic.
We choose verification of properties of concurrency as our domain of interest in this paper. The domain specific specification language and logic are fomalised in Plastic. A relevant proof system is designed for the users of concurrent domain. The corresponding lemmas are proved in Plastic. A prototype of relevant parsers and translators is implemented. We illustrate our approach through a concrete example in a prototype implementation.
Martin Hofmann has introduced a special unit type for making heap operations in a functional language explicit and thus facilitated an affine linear typing which, in the first-order case, provides for in-place update operational semantics.
Aspinall and Hofmann have recently extended the typablity of a first order fragment of this language by distinguishing three modes in which a value of an argument is allowed to be used in the evaluation of a term: read only, read and alias, read and destroy.
We discuss extensions in the same direction that use explicit information about which arguments are allowed to share with each other and which not. We formulate a general typing scheme in which the other ones can be embedded. Thus we can gain more insight about the languages, compare them with respect to their expressivity and translate some of the results from one to another.
We also invstigate how these extensions can be carried over to higher order versions of the language.
The reduction of terms is the key step in the type checking ofcomputing proofs. Generaliy, we represent terms by trees on which a reduction machinery operates. We propose to switch to a linear representation of terms as byte-code produced by a compiler and then strongly normalize terms by using an abstract machine. We will explain the strongly normalizing mechanisme and how modify the Ocaml abstract machine for this purpose. Integration into Coq is underway.
In this talk, we will present the new version of the extraction mechanism in the Coq proof assistant. By extraction, we mean automatic generation of ML code from Coq proofs, in order to produce certified programs. In former versions of Coq, the extraction mechanism suffered several limitations: in particular it could not deal with the entire Coq language, and the generated code was trustworthy only in some particular case. The new version now covers the entire language, and ensures correction of execution with call-by-value strategy. It also includes several optimizations to improve efficiency and readability of generated code. We will discuss difficulties encountered and solutions proposed in our new approach.
Based on a representation of primitive proof objects as lambda terms, which has been built into the theorem prover Isabelle recently, we propose a generic framework for program extraction. We show how this framework can be used to extract functional programs from proofs conducted in a constructive fragment of the object logic Isabelle/HOL. A characteristic feature of our implementation of program extraction is that it produces both a program and a correctness proof. Since the extracted program is available as a function within the logic, its correctness proof can be checked automatically inside Isabelle.
Demo of the new extraction mechanism of Coq.
We demonstrate an experimental implementation of program extraction that can be used to obtain executable functional programs from proofs in Isabelle/HOL.
In Luo's approach to Coercive Subtyping, so-called `coercion rules' extend the range of available coercions by allowing the synthesis of new coercions. Examples include lifting coercions over lists by mapping, or lifting coercions over the first, second, or both components of a Sigma type. Applications include the extension of basic coercions to larger data types, and overloading of notation between simply-typed and dependently-typed structures.
To our knowledge, such forms of coercion have only been implemented in Plastic, a system based on LF, a logical framework. Most cases of synthesising the coercions can be handled by a straightforward, recursive algorithm which uses first-order unification together with the list of existing coercions. However, a complication occurs when `prerequisite' (ie, smaller) coercions appear in the domain or range type of a potential coercion. At first sight, solving such constraints might involve higher order unification, but it appears that a feature of how coercions are used in practice may help in many cases.
This talk will present the current algorithm, as implemented in Plastic, with its use of an extra, very restricted case of unification. It will be demonstrated on examples, including the overloading of `pair' notation between an arbitrary mixture of simple types (A x B) and dependent types (Sigma(A, [x:A]B'(x))). This overloading allows the great convenience of allowing nested pairs to be written down without complex type annotations, then coerced to the precise (possibly dependent) type required
We give an overview of a number of interesting advances in recent versions of Isabelle, notably the new Isabelle2002 release. This includes the following.
Pcoq is a graphical user-interface for coq that runs under Linux and Windows.
The objective is to give examples of advantages of the type system in Mizar versus untyped text. Particularly:
Developing topology over Martin-Loef's type theory, or any foundation which is intuitionistic and also predicative, often requires a new treatment of basic notions, and this can bring to new insight.
I will show this in particular for the notion of closed subset, whose predicative treatment has emerged together with a whole structure which I have called the basic picture. I will also argue that stronger foundations would impede this discovery (as it happened as a matter of facts). I finally speculate about other possible advantages of predicative mathematic and programming.
The talk is meant to be a report of work in progress
A (point-free) compactification technique is developed in the context of (Martin-Löf's) Type Theory, and regarded as describing the predicative content of Stone-Cech compactification (the compact regular co-reflection of frames). It will be shown that, although the full strength of Stone-Cech compactification is to be attained exactly when impredicative definitions become allowed, a very significant part of its features still obtains predicatively.
A peculiarity of the technique we present is that it allows to prove straightforwardly the pointfree analogue of the classical result stating that any space X has a compactification with the same weight of X.
We prove then that compact Hausdorff spaces `form data-types' in Martin Loef's Type Theory, in the sense that the collection of points of any compact regular formal topology (the point-free predicative equivalent of compact Hausdorff spaces) may be identified with a data-type.
A somewhat paradoxical consequence of these results is that any completely regular formal space can be embedded as a dense subspace into (a space forming) a data-type.
A typed functional programming language with (co)inductive datatypes and general recursion is presented where every function is terminating and each infinite object is productive. Termination is not ensured by some static analysis on the program, but by type-checking. To this end, datatypes are indexed by ordinal expressions which represent some notion of size.
The programming language has the good properties of strong normalization. Surprisingly, this can only be shown for continuous result types of recursive functions. A grammar for a suitable class of continuous types is given.
The type-based approach to termination has some advantages over static analysis of the program code. First, it provides more abstraction and thus is less sensitive to syntactical reformulation of the code. Secondly, it can also handle non-strictly positive inductive types. And finally, it is more efficient since termination-checking is done in one pass with type-checking.
This work was inspired by Eduardo Gim'enez (ICALP 1998) and extends the work on sized types by Lars Pareto (POPL 1996; PhD Chalmers, 2000).
From the perspective of formal methods, the representation of OO-languages in a theorem prover is a rewarding target. Unfortunately, type systems and structuring mechanisms of OO-languages are rather different from the typed lambda-calculi underlying many theorem proving systems. In this talk, we will generalize recent experiences with a shallow embedding of UML/OCL to other OO-Languages.
We will demonstrate how to simulate in Java higher types as interfaces and lambda terms as inner classes implementing those interfaces in a direct way.
Generic (or polytypic) programming is about making programs more adaptable by making them more general. We present a framework for generic programming in Martin-Löf Type Theory, allowing to define programs (and proofs) by induction on the structure of user-defined datatypes. In addition to handling algebraic datatypes, we present some ideas for handling dependent types.
In the Coq proof system, some computer algebra structures have already been formalized and automated, such as Abelian rings (automated by the tactic Ring) or commutative fields (automated by the tactic Field). Regarding the tactic Field, equality proofs are automatically built and some side conditions (over the inverses which have been simplified and which must be non equal to zero) are generated (to be proved by the user). However, sometimes in mathematics, we need some extended structures to perform some computations with fewer side conditions. For instance, this is the case for the formal computations carried out in the Riemann sphere (complex numbers + infinite element). It is possible to characterize such sets as a wheel structure, which can be seen as a field extended with an infinite and a bottom elements. In particular, in such structures, the division by zero is allowed. We propose, in the context of Coq, an automation for wheel theories. Some direct applications would be the computations on the Riemann sphere, on some extensions of constructive real numbers or on any commutative ring with (partial) inversion (like rings of real-valued functions).
The design of any programming language encourages us to reconsider basic decisions regarding the primitive types of the language, and the introduction of dependent types no less so. By tradition from Peano, the natural numbers are usually given a linear (unary) representation in type theory, manifestly unsuitable for practical programming. We present an account of sized binary words in terms of two mutually inductive families of (dependent) types, using a dependently-typed (big-end, little-end) constructor. This allows us to specify and implement basic binary arithmetic operations homogeneously at any word size. We may thus identify appropriate types for primitive machine arithmetic operations in such a way as to bootstrap from there to a generic type of big numbers, with certified arithmetic, without further ado. We have partially implemented these ideas in the Coq and Oleg proof assistants as proof of concept. This work has been done jointly with James McKinna and Conor McBride.
I present the Stern-Brocot binary representation for rational numbers and I will define the arithmetical operations on them using lazy algorithms. I will talk about the formalization of this algorithms in Coq. My goal is to prove their properties in Coq, which will result in a rational arithmetic library for Coq.
Let us observe an elementary problem and its solution in plane geometry. We procced like that, concurrently we draw the figure and write the logical properties about the elements of the figure (points, lines, circles...). The parallel with a proof in a conscructive world, as a program, which builds a solution, and its logical justifications can be done, but here the constructors are a ruler and a pair of compasses. A work, which tries to review the Hilbert's axiomatic system following this vision, is now in progress using Coq as support.
We present a dependently typed logical framework, including structures (records) typed by dependent signatures with manifest fields. The framework has typed equality with eta and surjective pairing, and structural subtyping.
This work is in the lineage from Pebble and Cayenne, testing the conjecture that first class records with dependent signatures allowing manifest field definitions can support modularity for programming and proving in the large.
There are currently simple implementations in both ocaml and Haskell, and some checked examples. Extending the framework with Type:Type gives a powerful (if yet inconvenient) programming language.
We hope to also present a realisability semantics for the logical framework, from which normalisation and decidability of type-checking follows.
We introduce a notion of typed parallel process (parallelism with solvable conflicts), of interest of its own, and we use it to interpret the constructive content hidden in (first-order) classical combinatorial proofs
Deduction modulo is an alternative presentation of predicate logic where some axioms are oriented as computation rules. Orienting axioms introduces new cuts and makes cut elimination more difficult to prove, but simplifies the structure of cut free proofs in return. In particular consistency results, constructivity results, and completeness results for proof search methods can be obtained as corollaries of cut elimination for theories expressed in deduction modulo with computation rules only. Many theories (equational theories, simple type theory, several variants of set theory, ...) can be presented in deduction modulo. However arithmetic was an important example of a theory that lacked a presentation in deduction modulo. The goal of this paper is to show that Peano's arithmetic can indeed be presented in deduction modulo and that the standard techniques developed to prove cut elimination in deduction modulo can be used to prove cut elimination in arithmetic.
In this talk, I will present an encoding of Zermelo's set theory into F-omega with universes, a restriction of the Calculus of Constructions with universes in which types are not allowed to depend on proofs.
First, I will describe how sets can be represented as pointed graphs (a representation borrowed to non well-founded set theory) in a large class of impredicative pure type systems, and I will show that in F-omega with universes, this encoding allows all the axioms of intuitionnistic Zermelo's set theory to be derived. By using a double negation translation due to Coquand and Herbelin, I will then extend the encoding to Zermelo's classical set theory.
Finally, I will present two refinements of this encoding. The first one will be the definition of a pure type system with four sorts which captures the proof-theoretic strength of Zermelo's set theory. The second one will be an estimation of the strength of predicative universes in impredicative PTS (without inductive definitions), from which I will deduce that systems such as F-omega plus universes, the Calculus of Constructions with universes and the Extended Calculus of Constructions (ECC) have a proof-theoretic strength which is at least the one of classical Zermelo's set theory extended with infinitely many Zermelo's universes.
Sambin/Valentini's "toolbox" for subsets [Twenty-Five Years of Constructive Type Theory, Sambin and Smith eds, Oxford University Press 1998] turned out not to be general enough when I used it to formalize some algebra. I would like to discuss a slightly generalized theory that seems more natural to me. The equality Id(A,a,b), which plays important roles in the toolbox, is replaced by arbitrary equivalence relations. In particular, we have to define what an equivalence relation on a subset is. The aim of the talk is to propose and discuss proper definitions, rather than to prove theorems.
Joint work with Loïc Pottier and Carlos Simpsons.
Expressiveness of quotient types in the type theory of Coq.
In [HOF95], Martin Hofmann proposes and proves the consistency of an extension of the Calculus of Constructions with categorical quotient types but notices that there are not suffisant to prove the surjectivity of the following morphism theta.
Let E, F be two sets, R an equivalence relation on F, we define the relation S between elements of (E -> F) by fSg iff forall x in f(x)Rg(x). By definition of S, the application rho : (E -> F) -> (E -> F/R) which composes any function f:E->F with [_]R : F -> F/R is compatible with S. Therefore there exists a natural morphism theta from (E->F)/S to (E ->F/R) such that forall f : (E -> F), theta ([f]S)=[_]R o f.
From a classical and mathematical point of view, this morphism is clearly an isomorphism. In the type theory of Coq extended with quotient types, we can define theta (functional extensionality is needed but is consistent with quotient types), prove its injectivity, but we can not show that theta is surjective (in the sense of surjectivity in Prop, we do not talk about constructing an antecedent for each function of E -> (F/R)).
So the question is : can we extend quotient types in a way to make theta surjective? We will show in this talk that we can not : if we suppose the surjectivity of theta, it leads to a contradiction. The inconsistency is established in three steps. First we show that there exists s:(F/R -> F) such that forall x in F/R, [s(x)]R=x. Then, using a particular quotient type, we prove that there exists a function P2b from Prop to bool such that for all proposition P : P <-> ((P2b P)=true), and finally we use the fact that strong excluded middle is inconsistent in Coq (for example [GEU01]) to construct a term of type False.
We'll also show how we can prove, using the same ideas, that
the
following choice axiom in Prop :
AC : (A,B:Type)(R:A-> B-> Prop) ((x:A)(exT [y:B] (R x
y)))-> (ExT
[f:A->B] (R x (f x))))
plus the excluded middle in Prop are inconsistent in the type
theory of
Coq.
References
[GEU01]Herman Geuvers. Inconsistency of classical logic in type theory. http://www.cs.kun.nl/~herman/note.ps.gz
[HOF95]Martin Hofmann. Extensional concepts in intensional type theory. Phd thesis. http://www.lfcs.informatics.ed.ac.uk/reports/95/ ECS-LFCS-95-327
In order to be able to translate HOL proofs to Coq, we have looked for a set of classical axioms that would allow one to encode the HOL logic in Coq. A naive attempt at such an axiomatization turned out to be inconsistent with Coq, because of the impredicativity of Set.
However, we did find a semantics for the constructive part of the HOL Light logic in Coq (without having to put any axioms on top of the Calculus of Inductive Constructions.) In this semantics a HOL type corresponds to a setoid in Type, and in particular the HOL bool type corresponds to the Omega setoid (Prop with logical equivalence.)
The constructive core of HOL Light exactly fits this semantics, apart from the HOL type definition mechanism. We present a different mechanism to define new types, which does fit the semantics, but this turns out to be too weak to construct types like the natural numbers and cartesian products inside the HOL logic.
We analyze the proof of bool=Prop in the Calculus of Constructions + EM + strong sums and show that dependent case analysis does not satisfy subject reduction for classical objects (with call-cc).