Loaded Clusters (start of Section 9)

Note that we skip much of Subsection 8.2 because we worked already with split tableaux anyway.

This file covers Definitions 9.6 to 9.13 and Lemma 9.14. What comes after it is in separate files: Pdl.Interpolation.QFormula has Definitions 9.15 and 9.16 and Fact 9.17, Pdl.PreInterpolant has Definition 9.18, and Pdl.ClusterInterpolation has Lemma 9.3, i.e. the interpolant for the root of a proper cluster. Counterexamples to Lemma 9.12 (c) and (d) as stated in the paper are in Pdl.ClusterCorrection.

Collecting Cluster Nodes in a Finset

We define the finite sets loadedBelow and loadedAbove of nodes that are reachable from / can reach a given node via ◃ by filtering allPaths: a tableau has only finitely many nodes and PathIn.elem_allPaths says that allPaths tab contains all of them, so we can simply keep those nodes that are ◃-related to p in the desired direction. Then clusterListOf_spec is immediate.

def loadedBelow {X : Sequent} {tab : Tableau [] X} (p : PathIn tab) : Finset (PathIn tab)

Loaded nodes "below" the given one, also allowing ♥ steps. Includes the node itself.

Equations

• loadedBelow p = insert p ({q ∈ allPaths tab | p ◃⁺ q ∧ (nodeAt q).isLoaded})

def loadedAbove {X : Sequent} {tab : Tableau [] X} (p : PathIn tab) : Finset (PathIn tab)

Loaded nodes "above" the given one, also allowing backwards ♥ steps. Includes the node itself.

Equations

• loadedAbove p = insert p ({q ∈ allPaths tab | q ◃⁺ p ∧ (nodeAt q).isLoaded})

@[simp]

theorem mem_loadedBelow {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : q ∈ loadedBelow p ↔ q = p ∨ p ◃⁺ q ∧ (nodeAt q).isLoaded

@[simp]

theorem mem_loadedAbove {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : q ∈ loadedAbove p ↔ q = p ∨ q ◃⁺ p ∧ (nodeAt q).isLoaded

theorem eq_of_cEquiv_of_isFree {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} (p_free : (nodeAt p).isFree) (p_q : p ≡ᶜ q) : q = p

A free node is alone in its cluster (cf. Remark 4.18 in the paper).

def clusterListOf {X : Sequent} {tab : Tableau [] X} (p : PathIn tab) : Finset (PathIn tab)

The set of all other nodes in the same cluster, essentially a constructive version of clusterOf. Computed as the intersection of loadedAbove and loadedBelow.

Equations

• clusterListOf p = loadedBelow p ∩ loadedAbove p

theorem clusterListOf_spec {X : Sequent} {tab : Tableau [] X} {q : PathIn tab} (p : PathIn tab) : q ∈ clusterListOf p ↔ p ≡ᶜ q

Cluster roots

def PathIn.isClusterRoot {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) : Prop

Being a cluster root: there is no ◃ path from s back to a parent of s. As a parent p of s always has a ◃ path to s, this says that no parent of s is ≡ᶜ to s (see PathIn.isClusterRoot_iff), i.e. that s is the first node of its own cluster along the branch leading to s.

Note that this is vacuously true for .nil, the root of the whole tableau, which has no parent at all. This is why we quantify over all parents instead of demanding that a parent exists: the root of a tableau may already be loaded.

Equations

• s.isClusterRoot = ∀ (p : PathIn tab), p ⋖_ s → ¬s ◃* p

theorem PathIn.isClusterRoot_flip {X : Sequent} {tab : Tableau [] X} {p : PathIn tab} (h : p.isClusterRoot) : p.flip.isClusterRoot

theorem PathIn.isClusterRoot_nil {X : Sequent} {tab : Tableau [] X} : nil.isClusterRoot

The root of the whole tableau is a cluster root, because it has no parent.

theorem PathIn.isClusterRoot_iff {X : Sequent} {tab : Tableau [] X} {s : PathIn tab} : s.isClusterRoot ↔ ∀ (p : PathIn tab), p ⋖_ s → ¬p ≡ᶜ s

Equivalent formulation of PathIn.isClusterRoot using ≡ᶜ.

theorem PathIn.isClusterRoot_of_edge_from_free {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (s_free : (nodeAt s).isFree) (s_t : s ⋖_ t) : t.isClusterRoot

If the parent of t is free, then t is a cluster root. This is the case for all children of free nodes in the recursion of tabToIntAt.

theorem PathIn.isClusterRoot_of_parents_free {X : Sequent} {tab : Tableau [] X} {s : PathIn tab} (h : ∀ (p : PathIn tab), p ⋖_ s → (nodeAt p).isFree) : s.isClusterRoot

If all parents of s are free — which for a loaded s says exactly that s is the first loaded node along the branch leading to it — then s is a cluster root.

def isExitOf {X : Sequent} {tab : Tableau [] X} (s e : PathIn tab) : Prop

Def 8.14: e is an exit of the cluster of s, i.e. e ∈ C⁺ \ C where C is the cluster of s: it is not in the cluster of s, but it is a child of a node in it.

Equations

• isExitOf s e = (¬e ≡ᶜ s ∧ ∃ (t : PathIn tab), t ≡ᶜ s ∧ t ⋖_ e)

theorem isExitOf_flip {X : Sequent} {tab : Tableau [] X} {s e : PathIn tab} : isExitOf s.flip e.flip ↔ isExitOf s e

theorem isClusterRoot_of_isExitOf {X : Sequent} {tab : Tableau [] X} {s e : PathIn tab} (h : isExitOf s e) : e.isClusterRoot

Exits of a cluster are cluster roots. This is one of the two things needed to keep the tabToIntAt recursion going.

theorem exists_parent_of_lt {X : Sequent} {tab : Tableau [] X} {u s : PathIn tab} (h : u < s) : ∃ (p : PathIn tab), u ≤ p ∧ p ⋖_ s

If u < s then some parent of s is reachable from u (possibly u itself).

theorem PathIn.le_of_cEquiv_of_isClusterRoot {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (s_cr : s.isClusterRoot) (h : s ≡ᶜ t) : s ≤ t

Lemma 8.15 (a): clusters are subtrees. Here in the form we need it: the root of a cluster is ≤ all nodes of its cluster.

theorem lt_of_isExitOf {X : Sequent} {tab : Tableau [] X} {s e : PathIn tab} (s_cr : s.isClusterRoot) (h : isExitOf s e) : s < e

Exits of the cluster of a cluster root s are proper descendants of s. This is the second thing needed to keep the tabToIntAt recursion going, and it needs that clusters are subtrees, i.e. Lemma 8.15 (a).

Loaded Clusters

structure LoadedCluster {X : Sequent} (tab : Tableau [] X) : Type

A cluster, starting at a right-loaded root which is not ≡ᶜ to any parent of it.

Note that there is no explicit parent field: the root of the whole tableau may itself be loaded and then has no parent. Instead, root_not_to_parent quantifies over all parents of the root — which is exactly the property PathIn.isClusterRoot that tabToIntAt maintains as an invariant.

• root : PathIn tab

  The root of the cluster.

• root_not_to_parent : self.root.isClusterRoot

  There is no ◃ path from the root to any parent of it (so the root is indeed the root).

• proper : self.root ◃⁺ self.root

  There is ◃ path from the root to itself (so we have a proper cluster).

• root_loaded_right : (nodeAt self.root).2.2.isRight

  The root is loaded on the right.

• CL : Finset (PathIn tab)

  The set of all paths in the cluster.

• root_mem_CL : self.root ∈ self.CL

  The root is in the cluster.

• CL_equiv (s : PathIn tab) : s ∈ self.CL → ∀ t ∈ self.CL, s ≡ᶜ t

  All elements of CL are ≡ᶜ and thus can reach each other.

• CL_complete (s : PathIn tab) : s ∈ self.CL → ∀ (t : PathIn tab), s ≡ᶜ t → t ∈ self.CL

  All paths that are ≡ᶜ to something in CL are also in CL.

• root_reaches_all (s : PathIn tab) : s ∈ self.CL → self.root ◃* s

  The root can reach all nodes of the cluster.

def LoadedCluster.ofClusterRoot {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) (s_cr : s.isClusterRoot) (s_proper : s ◃⁺ s) (s_loaded_right : (nodeAt s).2.2.isRight) : LoadedCluster tab

Make the LoadedCluster of a right-loaded node that is the first node of its cluster. This is the way tabToIntAt now gets hold of a LoadedCluster.

Equations

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

def LoadedCluster.exits {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Finset (PathIn tab)

The exits of the cluster, i.e. C⁺ \ C from Def 8.14.

Equations

• C.exits = {e ∈ C.CL.biUnion fun (t : PathIn tab) => Finset.image Subtype.val t.children | e ∉ C.CL}

def LoadedCluster.CL_plus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Finset (PathIn tab)

C⁺, the cluster plus its exits.

Equations

• C.CL_plus = C.CL ∪ C.exits

theorem LoadedCluster.mem_CL_iff {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (p : PathIn tab) : p ∈ C.CL ↔ p ≡ᶜ C.root

The set C.CL contains exactly the exits in the sense of isExitOf.

theorem LoadedCluster.mem_exits_iff {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (e : PathIn tab) : e ∈ C.exits ↔ isExitOf C.root e

The set C.exits contains exactly the exits in the sense of isExitOf.

theorem LoadedCluster.isLoaded_of_between {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {v : PathIn tab} (h1 : C.root ◃* v) (h2 : v ◃* C.root) : (nodeAt v).isLoaded

All nodes that are ◃-between the root of a cluster and itself are loaded.

theorem LoadedCluster.all_right_loaded {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (t : PathIn tab) : t ∈ C.CL → (nodeAt t).2.2.isRight

Lemma 9.4 (a)

theorem LoadedCluster.left_empty_iff_root_left_empty {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (t : PathIn tab) : t ∈ C.CL → ((nodeAt t).1 = ∅ ↔ (nodeAt C.root).1 = ∅)

Lemma 9.4 (b): the left component of a node in the cluster is empty iff the left component of the root of the cluster is empty. Note that here the left component is the free side, because a LoadedCluster is loaded on the right. As Sequent.left ⟨L,R,O⟩ = L ∪ O.L and O.L = ∅ for the nodes in the cluster by LoadedCluster.all_right_loaded, this is the same as Λ₁(t) = ∅ ↔ Λ₁(r) = ∅.

theorem LoadedCluster.children_in_plus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (t : PathIn tab) : t ∈ C.CL → ∀ c ∈ t.children, ↑c ∈ C.CL_plus

Part of Lemma 9.4 (c): All children of t belong to C⁺.

theorem LoadedCluster.nonLpr_some_child_in_C {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (t : PathIn tab) : t ∈ C.CL → ¬t.isLrep → ∃ c ∈ t.children, ↑c ∈ C.CL

Part of Lemma 9.4 (c): If t is not an lpr, then at least one child is in C. This needs that the cluster is proper, i.e. that its root lies on a ◃-cycle.

theorem LoadedCluster.lpr_comp_in_C {X : Sequent} {tab : Tableau [] X} {comp : PathIn tab} (C : LoadedCluster tab) (t : PathIn tab) : t ∈ C.CL → t ♥ comp → comp ∈ C.CL

Part of Lemma 9.4 (c): If t is an lpr, then its companion is in C.

def LoadedCluster.nodesWith {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Finset Formula) : Finset (PathIn tab)

Def 9.6: All nodes in cluster with a certain set of formulas on the right. TODO: .right might not get or not keep track of the loaded formula! Better use Finset WhateverFormula and Sequent.wForms here maybe?

Equations

• C.nodesWith Δ = {p ∈ C.CL | (nodeAt p).right = Δ}

def LoadedCluster.plusNodesWith {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Finset Formula) : Finset (PathIn tab)

Equations

• C.plusNodesWith Δ = {p ∈ C.CL_plus | (nodeAt p).right = Δ}

The cluster at the fine level

The CL field of a LoadedCluster only contains the nodes in the coarse PathIn sense. For Definition 9.8 we also need the intermediate nodes inside the local tableaux, so we now determine which fine nodes belong to the cluster.

An intermediate node v inside the local tableau at a node p of the cluster belongs to the cluster iff some child of p below v is again in the cluster: in that case v lies on a ◃ cycle. Note that the children of p are exactly the nodes p.append (loc Y_in nil) for the end nodes Y of the local tableau at p, and they are labelled with Y.

def LoadedCluster.memFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (f : FinePathIn tab) : Prop

A fine node belongs to the cluster C iff its base node is in C and either it is that base node, or one of the children of the base node below it is in C.

Equations

• C.memFine f = (f.base ∈ C.CL ∧ (f.atBigRoot = true ∨ ∃ q ∈ f.coarseChildrenBelow, q ∈ C.CL))

@[instance_reducible]

noncomputable instance LoadedCluster.instDecidableMemFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (f : FinePathIn tab) : Decidable (C.memFine f)

Equations

• C.instDecidableMemFine f = id inferInstance

theorem LoadedCluster.memFine_toFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {p : PathIn tab} (p_in : p ∈ C.CL) : C.memFine p.toFine

Nodes of the cluster in the coarse sense are also fine nodes of the cluster.

noncomputable def LoadedCluster.fineCL {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : List (FinePathIn tab)

All fine nodes in the cluster C.

Equations

• C.fineCL = List.filter (fun (f : FinePathIn tab) => decide (C.memFine f)) (allFinePaths tab)

theorem LoadedCluster.mem_fineCL {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (f : FinePathIn tab) : f ∈ C.fineCL ↔ C.memFine f

theorem LoadedCluster.root_toFine_mem_fineCL {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : C.root.toFine ∈ C.fineCL

theorem LoadedCluster.exists_child_memFine_aux {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (f_base : f.base ∈ C.CL) {q : PathIn tab} (hq : q ∈ f.coarseChildrenBelow) (q_in : q ∈ C.CL) : ∃ g ∈ f.children, C.memFine g

If a fine node of the cluster has a coarse child of the cluster below it, then it has a fine child in the cluster.

theorem LoadedCluster.exists_child_memFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hf : C.memFine f) (h_not : ¬f.atBigRoot = true) : ∃ g ∈ f.children, C.memFine g

Lemma 9.7 (c) at the fine level, for nodes that are not coarse nodes: if a fine node f inside a local tableau belongs to the cluster, then so does one of its children.

theorem LoadedCluster.exists_child_memFine_of_not_isLrep {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hf : C.memFine f) (h_lrep : ¬f.base.isLrep) : ∃ g ∈ f.children, C.memFine g

Lemma 9.7 (c) at the fine level, in general: any fine node of the cluster that is not a loaded-path repeat has a child in the cluster. For coarse nodes this uses Lemma 9.4 (c), i.e. nonLpr_some_child_in_C, and hence needs that the cluster is proper.

noncomputable def LoadedCluster.fineExits {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Finset (FinePathIn tab)

All fine nodes just outside the cluster C, i.e. C⁺ \ C at the fine level.

Equations

• C.fineExits = {f ∈ C.fineCL.toFinset.sup FinePathIn.children | (decide ¬C.memFine f) = true}

noncomputable def LoadedCluster.fineCLplus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Finset (FinePathIn tab)

The fine version of C⁺.

Equations

• C.fineCLplus = C.fineCL.toFinset ∪ C.fineExits

noncomputable def LoadedCluster.lambdaTwo {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Finset Sequent

Λ₂[C], the right components of the fine nodes of the cluster.

Equations

• C.lambdaTwo = Finset.image (fun (f : FinePathIn tab) => f.label.rightOnly) C.fineCL.toFinset

noncomputable def LoadedCluster.lambdaTwoPlus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Finset Sequent

Λ₂[C⁺], the right components of the fine nodes of the cluster and of its exits.

Equations

• C.lambdaTwoPlus = Finset.image (fun (f : FinePathIn tab) => f.label.rightOnly) C.fineCLplus

noncomputable def LoadedCluster.nodesWithFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : List (FinePathIn tab)

C_Δ from Def 9.6, at the fine level.

Equations

• C.nodesWithFine Δ = List.filter (fun (f : FinePathIn tab) => decide (f.label.rightOnly = Δ)) C.fineCL

noncomputable def LoadedCluster.plusNodesWithFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Finset (FinePathIn tab)

C⁺_Δ from Def 9.6, at the fine level.

Equations

• C.plusNodesWithFine Δ = {f ∈ C.fineCLplus | decide (f.label.rightOnly = Δ) = true}

noncomputable def LoadedCluster.nodesWithFineRight {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : List (FinePathIn tab)

C^R_Δ from Def 9.6: nodes with right component Δ where a right rule is applied.

Equations

• C.nodesWithFineRight Δ = List.filter (fun (f : FinePathIn tab) => f.usesRightRule) (C.nodesWithFine Δ)

noncomputable def LoadedCluster.nodesWithFineLeft {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : List (FinePathIn tab)

C^L_Δ from Def 9.6: nodes with right component Δ where a left rule is applied.

Equations

• C.nodesWithFineLeft Δ = List.filter (fun (f : FinePathIn tab) => f.usesLeftRule) (C.nodesWithFine Δ)

noncomputable def LoadedCluster.nodesWithFineNoRule {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : List (FinePathIn tab)

Nodes with right component Δ where no rule is applied at all. These are the loaded-path repeats and the closing rules, which Lemma 9.7 (a) in the paper does not mention.

Equations

• C.nodesWithFineNoRule Δ = List.filter (fun (f : FinePathIn tab) => !f.usesLeftRule && !f.usesRightRule) (C.nodesWithFine Δ)

theorem LoadedCluster.mem_nodesWithFine_iff {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) (f : FinePathIn tab) : f ∈ C.nodesWithFine Δ ↔ f ∈ C.nodesWithFineLeft Δ ∨ f ∈ C.nodesWithFineRight Δ ∨ f ∈ C.nodesWithFineNoRule Δ

Lemma 9.7 (a), first part: C_Δ is the union of C^L_Δ and C^R_Δ and the nodes where no rule is applied.

theorem LoadedCluster.nodesWithFineLeft_disjoint_right {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) (f : FinePathIn tab) : f ∈ C.nodesWithFineLeft Δ → f ∉ C.nodesWithFineRight Δ

Lemma 9.7 (a), second part: C^L_Δ and C^R_Δ are disjoint.

theorem LoadedCluster.mem_lambdaTwo_iff {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo ↔ C.nodesWithFine Δ ≠ []

Δ ∈ Λ₂[C] iff C_Δ ≠ ∅, the remark after the invariant in Def 9.8.

noncomputable def LoadedCluster.stepOf {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Finset Sequent

The right components of the children of a node in C^R_Δ.

For the quasi-tableau in Def 9.8 we need, given Δ ∈ Λ₂[C], the sequents Π₁, …, Πₙ obtained by applying the right rule to Δ — both for local rules (Lemma 9.7 (f)) and for the modal rule when Δ is basic (Lemma 9.7 (e)). Instead of using uniformity to choose such a rule we here simply look up the first node of C^R_Δ and read off the right components of its children. By uniformity (which we do not prove here) this does not depend on the chosen node. When C^R_Δ is empty — which by Lemma 9.7 (d) only happens when C_Δ is empty, i.e. when Δ ∉ Λ₂[C] — we return the empty list, but note that the construction of Q below never uses stepOf in that case.

Equations

• C.stepOf Δ = match (C.nodesWithFineRight Δ).head? with | some f => Finset.image (fun (g : FinePathIn tab) => g.label.rightOnly) f.children | none => ∅

theorem LoadedCluster.stepOf_ne_nil {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (h : C.nodesWithFineRight Δ ≠ []) : C.stepOf Δ ≠ ∅

If some right rule is applied at a node of the cluster with right component Δ, then stepOf Δ is non-empty: by Lemma 9.7 (c) that node has a child in the cluster, so the rule applied there cannot be a closing rule.

noncomputable def LoadedCluster.stepOfL {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : List Sequent

Equations

• C.stepOfL = Finset.seqSort ∘ C.stepOf

theorem LoadedCluster.stepOfL_ne_nil {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (h : C.nodesWithFineRight Δ ≠ []) : C.stepOfL Δ ≠ []

Uniformity

stepOf reads off the children of the first node of C^R_Δ. Using head? is a legitimate way to implement the "unique local rule R₂ with principal formula ξ" of Lemma 9.7 (f) without making a choice, and it is harmless as long as all nodes of C^R_Δ agree on the right components of their children — which is exactly what uniformity of the tableau (conditions U1 and U2 in the paper) is for. Without uniformity nothing relates stepOf Δ to the nodes of C^R_Δ other than the arbitrarily chosen first one, and the correctness proofs of the pre-interpolants do need the relation for every node of the region R_x = C^R_Δ.

Two remarks. First, uniformity is only needed when Δ is not basic: when Δ is basic, the rule applied at a node of C^R_Δ is the modal rule applied to the unique loaded formula of Δ (Lemma 9.7 (e)), so the right components of the children are determined by Δ alone. Second, stepOf produces an ordered list, so what is needed is agreement of the children lists including their order; since the right components of the children of a node in C^R_Δ are determined by Δ together with the rule and its principal formula, this follows from uniformity in the form of Lemma 9.7 (f).

Uniformity is not available in this development yet, so for now we state the property that is needed as an explicit assumption, and stepOf_spec shows that it suffices to justify the use of head?.

def LoadedCluster.HasUniformSteps {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Prop

The consequence of uniformity that the quasi-tableau construction needs: any two nodes of the cluster with the same right component Δ at which a right rule is applied have the same right components below them, in the same order. Compare Lemma 9.7 (f).

Equations

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

theorem LoadedCluster.stepOf_spec {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hU : C.HasUniformSteps) (Δ : Sequent) {f : FinePathIn tab} (hf : f ∈ C.nodesWithFineRight Δ) : Finset.image (fun (g : FinePathIn tab) => g.label.rightOnly) f.children = C.stepOf Δ

Given HasUniformSteps, the list stepOf Δ really describes the right components of the children of every node in C^R_Δ, and not just of the first one.

theorem LoadedCluster.mem_fineCLplus_of_child {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f g : FinePathIn tab} (hf : f ∈ C.fineCL) (hg : g ∈ f.children) : g ∈ C.fineCLplus

A child of a fine node of the cluster is a fine node of C⁺.

theorem LoadedCluster.mem_lambdaTwoPlus_of_mem_fineCLplus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hf : f ∈ C.fineCLplus) : f.label.rightOnly ∈ C.lambdaTwoPlus

The right component of a fine node of C⁺ is in Λ₂[C⁺].

theorem LoadedCluster.lambdaTwo_subset_lambdaTwoPlus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo → Δ ∈ C.lambdaTwoPlus

Λ₂[C] ⊆ Λ₂[C⁺].

theorem LoadedCluster.stepOf_mem_lambdaTwoPlus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ Pi : Sequent) : Pi ∈ C.stepOf Δ → Pi ∈ C.lambdaTwoPlus

The labels given by stepOf are in Λ₂[C⁺]. This is the invariant needed in Def 9.8: a node of Q is labelled with an element of Λ₂[C⁺], and it is a leaf exactly when it is a repeat or its label is not in Λ₂[C], i.e. when it is an exit.

Interpolants for the exit regions (Def 9.13 and Lemma 9.14)

By the assumption of Lemma 9.3 we have an interpolant θ_t for every exit node t ∈ C⁺ \ C. Here these are given by a map θ on the fine nodes; the assumption that they are interpolants is ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f).

noncomputable def LoadedCluster.exitsWithFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Finset (FinePathIn tab)

C⁺_Δ \ C_Δ, i.e. the exit nodes whose right component is Δ.

Equations

• C.exitsWithFine Δ = {f ∈ C.fineExits | decide (f.label.rightOnly = Δ) = true}

noncomputable def LoadedCluster.thetaOf {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (θ : FinePathIn tab → Formula) (Δ : Sequent) : Formula

Def 9.13: θ_Δ, the disjunction of the interpolants of all exit nodes whose right component is Δ. Note that θ_Δ = ⊥ in case there are no such exit nodes.

Equations

• C.thetaOf θ Δ = (Finset.image θ (C.exitsWithFine Δ)).dis

theorem LoadedCluster.mem_exitsWithFine_iff {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) (f : FinePathIn tab) : f ∈ C.exitsWithFine Δ ↔ f ∈ C.fineExits ∧ f.label.rightOnly = Δ

Membership in C⁺_Δ \ C_Δ means: being an exit node with right component Δ.

theorem LoadedCluster.right_of_mem_exitsWithFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} {f : FinePathIn tab} (hf : f ∈ C.exitsWithFine Δ) : f.label.right = Δ.right

The right component of an exit node with right component Δ is the right component of Δ.

theorem LoadedCluster.thetaOf_left {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (Δ : Sequent) (f : FinePathIn tab) : f ∈ C.exitsWithFine Δ → ¬HasSat.satisfiable ({~C.thetaOf θ Δ} ∪ f.label.left)

Lemma 9.14 (a): Λ₁(t) ⊨ θ_Δ for all t ∈ C⁺_Δ \ C_Δ.

theorem LoadedCluster.thetaOf_right {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (Δ : Sequent) : ¬HasSat.satisfiable ({C.thetaOf θ Δ} ∪ Δ.right)

Lemma 9.14 (b): Δ ⊨ ¬θ_Δ.

theorem LoadedCluster.thetaOf_voc {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (Δ : Sequent) : (C.thetaOf θ Δ).voc ⊆ Vocab.fromFinset (Finset.image (fun (f : FinePathIn tab) => f.label.left.fvoc) (C.exitsWithFine Δ)) ∩ Δ.right.fvoc

Lemma 9.14 (c): the vocabulary of θ_Δ is included in the vocabulary of Δ and in the union of the vocabularies of the left components of the exit nodes with right component Δ.