The lab has done a number of set theory related formalizations in Coq including constructions of models of set theory and constructions of models of type theory using set theory.
We present a formal constructive theory of regular languages in Coq+Ssreflect. The development includes Kleene's Theorem, the Myhill-Nerode Theorem and a number of other constructions.
We formalize a higher-order logic with Church style typing. We also formalize an M-set model where the monoid M is a type of substitutions and a base type is interpreted as untyped lambda terms. This M-set model justifies representing untyped lambda terms using higher-order abstract syntax in the higher-order logic. The Autosubst package is used to support reasoning about substitutions and terms.
We formalize two well-known semantics for intuitionistic propositional logic: Heyting algebras and Kripke models. We prove both semantics are sound for an intuitionistic propositional logic with only implication and false. We use Heyting algebras to prove undefinability results. We also prove a Kripke model can be converted into a Heyting algebra. Assuming excluded middle, we can convert a Heyting algebra into a Kripke model. In some ways our task is made easier by the fact that the logic does not have disjunction.
We develop a library for finite sets using Ssreflect. In contrast to the "finset" library in Ssreflect, which only allows finite base types, we allow countable types as base types. Finite sets are implemented as a quotient on lists using some canonical duplicate free list as representative. We provide most of the basic theory as well as constructions for least and greatest fixpoints and maximal extensions.
Tue Apr 11 15:03:27 2017