Interpolants for proper clusters (Lemma 9.3)

This file contains the interpolation step for proper clusters: given interpolants for all exit nodes of a cluster, we build an interpolant for the root of the cluster.

The three conditions on the interpolant θ_r := C.itp θ of Definition 9.20 are exactly

• LoadedCluster.itp_voc (Lemma 10.1),
• LoadedCluster.left_unsat_neg_itp (Lemma 10.3), and
• LoadedCluster.right_unsat_itp (Lemma 10.8).

What this file adds is the interface: the interpolants θ used by those three results are indexed by the fine exit nodes of the cluster, i.e. also by nodes inside a local tableau, while clusterInterpolation_right is only given interpolants for the exits in the coarse PathIn sense. The first half of the file bridges that gap, by pushing the interpolants of the coarse exits upwards through the local tableaux with LocalTableau.interpolant.

Flipping Interpolants

theorem IsPartInterpolant.flip {X : Sequent} {θ : Formula} : isPartInterpolant X θ → isPartInterpolant X.flip (~θ)

When X is an interpolant for X, then ~θ is an interpolant for X.flip.

def PartInterpolant.flipPath {X : Sequent} {tab : Tableau [] X} {p : PathIn tab} (ip : PartInterpolant (nodeAt p)) : PartInterpolant (nodeAt p.flip)

Transport an interpolant to the flipped tableau.

Equations

• ip.flipPath = ⟨~↑ip, ⋯⟩

def PartInterpolant.unflipPath {X : Sequent} {tab : Tableau [] X} {p : PathIn tab} (ip : PartInterpolant (nodeAt p.flip)) : PartInterpolant (nodeAt p)

Transport an interpolant back from the flipped tableau.

Equations

• ip.unflipPath = ⟨~↑ip, ⋯⟩

From the coarse exits to the fine exits

A fine exit of the cluster is either a coarse node — then it is an exit in the coarse sense and we are given an interpolant for it — or a node inside a local tableau from which the cluster is never re-entered. In the latter case all end nodes of the local tableau below it are coarse exits, and we obtain an interpolant by local interpolation.

theorem LocalPathIn.exists_mem_endNodesBelow {Y Z : Sequent} {lt : LocalTableau Z} (lp : LocalPathIn lt) : Y ∈ endNodesOf lp.ltAt → ∃ (hY : Y ∈ endNodesOf lt), ⟨Y, hY⟩ ∈ lp.endNodesBelow

Every end node of the local tableau at a local path is an end node of the whole local tableau that is below that path.

theorem FinePathIn.edge_of_mem_coarseChildrenBelow {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (q : PathIn tab') : q ∈ f.coarseChildrenBelow → f.base ⋖_ q

A coarse child below a fine node really is a child of the base of that fine node.

theorem FinePathIn.base_of_mem_children' {H : History} {Z : Sequent} {tab' : Tableau H Z} (f g : FinePathIn tab') : g ∈ f.children → g.base = f.base ∨ f.base ⋖_ g.base ∧ g.atBigRoot = true

A sharpening of FinePathIn.base_of_mem_children: a fine child that lies at a different coarse node is a coarse node itself.

theorem FinePathIn.exists_interpolant_of_coarse {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : ¬f.atBigRoot = true → (∀ q ∈ f.coarseChildrenBelow, ∃ (θ : Formula), isPartInterpolant (nodeAt q) θ) → ∃ (θ : Formula), isPartInterpolant f.label θ

Local interpolation at fine nodes. If a fine node is not a coarse node, i.e. it lies properly inside a local tableau, and we have interpolants for all coarse children below it — these are the end nodes of that local tableau that are reachable from it — then we have an interpolant for the fine node itself. This is LocalTableau.interpolant applied to the part of the local tableau below the node.

noncomputable def FinePathIn.itp {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : Formula

An interpolant for the label of a fine node, whenever one exists. This is the map θ on the fine exit nodes that Definitions 9.13 and 9.18 need.

Equations

• f.itp = if h : ∃ (θ : Formula), isPartInterpolant f.label θ then h.choose else ⊤

theorem FinePathIn.itp_spec {H : History} {Z : Sequent} {tab' : Tableau H Z} {f : FinePathIn tab'} (h : ∃ (θ : Formula), isPartInterpolant f.label θ) : isPartInterpolant f.label f.itp

theorem LoadedCluster.mem_exits_of_mem_coarseChildrenBelow {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hbase : f.base ∈ C.CL) (hf : ¬C.memFine f) (q : PathIn tab) : q ∈ f.coarseChildrenBelow → q ∈ C.exits

Every coarse child below a fine exit of the cluster is a coarse exit of the cluster.

theorem LoadedCluster.mem_exits_base_of_mem_fineExits {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hf : f ∈ C.fineExits) (hbr : f.atBigRoot = true) : f.base ∈ C.exits

A fine exit of the cluster that is a coarse node is a coarse exit of the cluster.

theorem LoadedCluster.exists_itp_of_mem_fineExits {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (exitIPs : ∀ e ∈ C.exits, ∃ (θ : Formula), isPartInterpolant (nodeAt e) θ) (f : FinePathIn tab) : f ∈ C.fineExits → ∃ (θ : Formula), isPartInterpolant f.label θ

Interpolants for the coarse exits of the cluster give interpolants for all fine exits.

theorem LoadedCluster.fineExits_itp_spec {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (exitIPs : ∀ e ∈ C.exits, ∃ (θ : Formula), isPartInterpolant (nodeAt e) θ) (f : FinePathIn tab) : f ∈ C.fineExits → isPartInterpolant f.label f.itp

The interpolants of the fine exit nodes of the cluster, given interpolants for the coarse exits. This is the map θ of Definitions 9.13, 9.18 and 9.20.

Where uniformity is needed

The facts about a proper cluster that the proofs of Lemmas 10.1, 10.3 and 10.7 use are proved in Pdl.ClusterFacts and Pdl.ClusterSatDownFacts. All of them follow from properness of the cluster, which is part of LoadedCluster, except for LoadedCluster.rightRuleChildren_of_uniform, which also needs uniformity of the tableau (conditions U1/U2, formalised as LoadedCluster.HasUniformSteps with LoadedCluster.stepOf_spec, and obtained from tab.isUniform by LoadedCluster.uniformOfUniTab).

The reason is that C.stepOf Δ reads the right components of the children of the first node of C^R_Δ, while the facts quantify over all nodes of C^R_Δ:

• LoadedCluster.rightRuleChildren_of_uniform (used at non-basic type-3 nodes in the proof of Lemma 10.3) says that for every t ∈ C^R_Δ and every Π ∈ stepOf Δ there is a node of C⁺_Π with the same left component as t. Its proof takes the children of t, so it needs the right components of those children to be the list stepOf Δ — which for a non-basic Δ is precisely stepOf_spec, i.e. uniformity.
• LoadedCluster.modalStep_of and LoadedCluster.basicStep_of also quantify over t ∈ C^R_Δ, but only for basic Δ. There the rule applied is the modal rule for the unique loaded formula of Δ (Lemma 9.7 (e)), so the right components of the children are determined by Δ alone; this is what LoadedCluster.basicModalStepAt shows, and it is why modalStep_of needs no uniformity.
• The remaining facts (LoadedCluster.nonBasicStep_of, LoadedCluster.stepOf_lt_Sequent, LoadedCluster.leftPropagation_of_proper, LoadedCluster.exists_right_of_proper, the vocabulary facts) speak about Δ and stepOf Δ only, or about local invertibility at a single node, and are independent of uniformity.

Interpolants for proper clusters

noncomputable def clusterInterpolation_right {X : Sequent} {tab : Tableau [] X} (Xfree : X.isFree) (t_u : tab.isUniform) (C : LoadedCluster tab) (exitIPs : (e : PathIn tab) → e ∈ C.exits → PartInterpolant (nodeAt e)) : PartInterpolant (nodeAt C.root)

Lemma 9.3 for the case where the loaded formula is on the right side: given interpolants for all exits of the cluster C, interpolate the root of C.

The interpolant is C.itp θ from Definition 9.20, where θ gives the interpolants of the fine exit nodes, obtained from the given interpolants of the coarse exits by LoadedCluster.fineExits_itp_spec. Its three defining properties are Lemma 10.1 (itp_voc), Lemma 10.3 (left_unsat_neg_itp) and Lemma 10.8 (right_unsat_itp).

Equations

• clusterInterpolation_right Xfree t_u C exitIPs = ⟨C.itp FinePathIn.itp, ⋯⟩

noncomputable def clusterInterpolation {X : Sequent} {tab : Tableau [] X} (Xfree : X.isFree) (t_u : tab.isUniform) (s : PathIn tab) (s_cr : s.isClusterRoot) (s_proper : s ◃⁺ s) (s_loaded : (nodeAt s).isLoaded) (exitIPs : (e : PathIn tab) → isExitOf s e → PartInterpolant (nodeAt e)) : PartInterpolant (nodeAt s)

Lemma 9.3: Given a loaded node s that is the first node of its cluster, and given interpolants for all exits of that cluster, we get an interpolant for s. Note how s_cr is exactly what is needed to make a LoadedCluster here.

Equations

• One or more equations did not get rendered due to their size.