Defining interpolants (Theorem 8.13)

Here we put together the interpolants for singleton clusters and for proper clusters.

Cluster roots below nodes with a singleton cluster

theorem PathIn.isClusterRoot_of_edge_of_not_proper {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : ¬s ◃⁺ s) (s_t : s ⋖_ t) : t.isClusterRoot

If there is no ◃ cycle at s, then all children of s are cluster roots. This is the analogue of PathIn.isClusterRoot_of_edge_from_free for loaded nodes that form a singleton cluster.

theorem PathIn.proper_of_isLrep {X : Sequent} {tab : Tableau [] X} {s : PathIn tab} (h : s.isLrep) : s ◃⁺ s

A loaded path repeat always is in a proper cluster: it has a ♥ step to its companion and the companion is an ancestor, so it can reach the repeat again.

From Tableau to Interpolant

theorem tabToIntAt {X : Sequent} (h_free : X.isFree) (tab : Tableau [] X) (t_u : tab.isUniform) (s : PathIn tab) : s.isClusterRoot → ∃ (θ : Formula), isPartInterpolant (nodeAt s) θ

In a tableau starting with a free sequent at the root, there exists a PartInterpolant for every cluster root in the tableau.

Note the extra hypothesis s.isClusterRoot: to interpolate at a loaded node we need to know that it is the first node of its cluster along the branch leading to it, because otherwise we cannot make a LoadedCluster. In particular, this hypothesis holds whenever the parent of s is free (see PathIn.isClusterRoot_of_edge_from_free), which is the case for all children of the free nodes we recurse into below. It also holds for the exits of a cluster (see isClusterRoot_of_isExitOf), which need not have a free parent, but which are always the first node of their own cluster.

At the root of the tableau the hypothesis is free of charge: .nil has no parent at all, so PathIn.isClusterRoot_nil holds vacuously and tabToInt below can discharge it. Hence for that we do not even need the additional assumption that the root sequent X is free, but we do want it inside clusterInterpolation later.

Ideally this would be a computable def and not an existential. But currently PathIn.strong_upwards_inductionOn only works with Prop motive.

theorem tabToInt {X : Sequent} (h_free : X.isFree) (tab : Tableau [] X) (t_u : tab.isUniform) : ∃ (θ : Formula), isPartInterpolant X θ