-- Formalisation of subtyping for recursive types
-- Nils Anders Danielsson

-- This formalisation is explained in "Subtyping, Declaratively—An
-- Exercise in Mixed Induction and Coinduction" (coauthored with
-- Thorsten Altenkirch). The code is partly based on "Coinductive
-- Axiomatization of Recursive Type Equality and Subtyping" by Michael
-- Brandt and Fritz Henglein.

module RecursiveTypes where

-- Recursive types and potentially infinite trees.

import RecursiveTypes.Syntax

-- Substitutions.

import RecursiveTypes.Substitution

-- The semantics of recursive types, defined in terms of the trees
-- that you get when unfolding them.

import RecursiveTypes.Semantics

-- The definition of subtyping which, in my eyes, is the most obvious.
-- Some people may dislike coinductive definitions, though.

import RecursiveTypes.Subtyping.Semantic.Coinductive

-- An example.

import RecursiveTypes.Subtyping.Example

-- Another definition of subtyping, this time in terms of finite
-- approximations. According to Brandt and Henglein this definition is
-- due to Amadio and Cardelli.

import RecursiveTypes.Subtyping.Semantic.Inductive

-- The two semantical definitions of subtyping above can easily be
-- proved equivalent.

import RecursiveTypes.Subtyping.Semantic.Equivalence

-- An axiomatisation of subtyping which is inspired by Brandt and
-- Henglein's. The main difference is that their axiomatisation is
-- inductive, using explicit hypotheses to get a coinductive flavour,
-- whereas mine is mixed inductive/coinductive, using no explicit
-- hypotheses. The axiomatisation is proved equivalent to the
-- coinductive semantic definition of subtyping. The proof is a lot
-- simpler than Brandt and Henglein's, but their proof includes a
-- decision procedure for subtyping.

import RecursiveTypes.Subtyping.Axiomatic.Coinductive

-- Brandt and Henglein's axiomatisation, plus some proofs:
-- • A proof showing that the axiomatisation is sound with respect to
--   the ones above. The soundness proof is different from the one
--   given by Brandt and Henglein: it is cyclic (but productive).
-- • Proofs of decidability and completeness, based on Brandt and
--   Henglein's algorithm.

import RecursiveTypes.Subtyping.Axiomatic.Inductive

-- Some modules containing supporting code for the proof of
-- decidability, including Brandt and Henglein's subterm relation.

import RecursiveTypes.Subterm
import RecursiveTypes.Subterm.RestrictedHypothesis
import RecursiveTypes.Syntax.UnfoldedOrFixpoint

-- An incorrect "subtyping" relation which illustrates the fact that
-- taking the transitive closure of a coinductively defined relation
-- is not in general equivalent to adding an inductive transitivity
-- constructor to it.

import RecursiveTypes.Subtyping.Axiomatic.Incorrect

-- Finally some code which is not directly related to subtyping or
-- recursive types: an example which shows that, in a coinductive
-- setting, it is not always sound to postulate admissible rules
-- (inductively).

import AdmissibleButNotPostulable