Uniformity of split tableaux (Section 8.1)

This file defines when a tableau is uniform, by the two conditions U1 and U2 of the paper, and shows that in a uniform tableau every loaded cluster has the property LoadedCluster.HasUniformSteps that the construction of the quasi-tableau needs.

Recall the two conditions from the paper, where Λ₁(s) and Λ₂(s) are the left and the right component of the sequent at the node s, and where i ∈ {1,2}:

• U1. If Λᵢ(s) is loaded then a local rule is applied to a formula in the unloaded component of s, unless that component is basic.
• U2. If Λᵢ(s) = Λᵢ(t) is loaded and not basic, and the unloaded components of both s and t are basic, then at s and at t the same rule is applied, to the same formula in the loaded component of the node.

Both conditions speak about the nodes of the tableau in the sense of the paper, i.e. also about the nodes inside the local tableaux. Hence we state them for FinePathIn tab. Note that in U2 the loaded component is not basic, so the rule applied at s and at t must be a local rule; we therefore phrase U2 using FinePathIn.lra?, and "the same rule applied to the same formula" becomes LocalRuleApp.SameRuleAs: the two rule applications have the same principal formulas (Lcond, Rcond and Ocond) and the same results (ress), and indeed use the same rule (lr).

The main result is LoadedCluster.uniformOfUniTab. Its proof splits into two cases, and only the second one uses uniformity:

• If Δ is basic then by Lemma 9.7 (e) — here Uniformity.basicModalStep — the rule applied at a node of C^R_Δ is the modal rule (M) for the loaded formula of Δ, and hence the right component of the unique child only depends on Δ.
• If Δ is not basic then the rule applied at a node of C^R_Δ is a local rule acting on the right. By U1 the left component of such a node is basic, so U2 applies and says that the same rule with the same principal formula is used at all these nodes. Since a local rule application only changes the right component by deleting its principal formulas and adding the results, the right components of the children agree — this is Uniformity.map_rightOnly_C_eq.

Duplicated helper lemmas

The file Pdl.ClusterInterpolation imports this file (it uses Tableau.isUniform and LoadedCluster.uniformOfUniTab), so we cannot use the lemmas about right rules that are proved there. The section Uniformity below therefore repeats those that are needed here, under different names.

The components of a sequent

def Sequent.leftOnly (X : Sequent) : Sequent

The left component of a sequent, together with the loaded formula, again as a sequent. This is Λ₁ from the paper; compare Sequent.rightOnly, which is Λ₂.

Equations

• X.leftOnly = (X.1, ∅, X.2.2)

def Sequent.leftFree (X : Sequent) : Sequent

The left component of a sequent, without any loaded formula. When the loaded formula is on the right, i.e. in the situation of a LoadedCluster, this is the unloaded component Λ₁ of the node, and Sequent.leftFree X |>.basic says that no local rule is applicable to it.

Equations

• X.leftFree = (X.1, ∅, none)

def Sequent.rightFree (X : Sequent) : Sequent

The right component of a sequent, without any loaded formula. When the loaded formula is on the left this is the unloaded component Λ₂ of the node.

Equations

• X.rightFree = (∅, X.2.1, none)

def LocalRuleApp.SameRuleAs (lra₁ lra₂ : LocalRuleApp) : Prop

Two local rule applications use the same rule with the same principal formulas. The fields Lcond, Rcond and Ocond are the principal formulas and ress is the list of results of the rule, so this says that the same rule instance is applied at two nodes, which may still have different sequents.

Equations

• lra₁.SameRuleAs lra₂ = (lra₁.Lcond = lra₂.Lcond ∧ lra₁.Rcond = lra₂.Rcond ∧ lra₁.Ocond = lra₂.Ocond ∧ lra₁.ress = lra₂.ress ∧ lra₁.lr ≍ lra₂.lr)

Uniformity

def Tableau.U1 {H : History} {X : Sequent} (tab : Tableau H X) : Prop

Condition U1: at a node with a loaded component, a rule is applied to the unloaded component unless the latter is basic. Since every rule is a left rule or a right rule but not both (FinePathIn.not_left_and_right), we state this as: a rule on the unloaded side is applied.

The condition is only about nodes at which a rule is applied at all, i.e. we exclude the leaves given by a loaded-path repeat, which is what ¬ f.base.isLrep says. Note that this exclusion is needed: at a loaded-path repeat the tableau stops, so no rule at all — and in particular no rule on the unloaded component — is applied there, while the sequent of a loaded-path repeat may well have a non-basic unloaded component. (For example, the sequent reached again after a loop may contain a conjunction on the unloaded side; the tableau is then forced to stop, because Tableau.loc and Tableau.pdl both require ¬ flprep.) Without the exclusion no tableau with such a repeat would be uniform, and Tableau.toUniform would fail.

Equations

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

def Tableau.U2 {H : History} {X : Sequent} (tab : Tableau H X) : Prop

Condition U2: two nodes whose loaded component is the same and not basic, and whose unloaded components are both basic, apply the same rule to the same formula of the loaded component. As the loaded component is not basic the rule must be a local one, so we may state this for the local rule applications f.lra? and g.lra?.

Equations

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

def Tableau.UniCore {H : History} {X : Sequent} (tab : Tableau H X) : Prop

The conditions U1 and U2 together.

Equations

• tab.UniCore = (tab.U1 ∧ tab.U2)

theorem Tableau.uniCore_of_all_free {H : History} {X : Sequent} {tab : Tableau H X} (h : ∀ (f : FinePathIn tab), f.label.2.2 = none) : tab.UniCore

A sanity check that U1 and U2 are not contradictory: both conditions only constrain nodes with a loaded component, so a tableau in which no node is loaded satisfies them.

def Tableau.isUniform {H : History} {X : Sequent} (tab : Tableau H X) : Prop

A tableau is uniform if it satisfies the conditions U1 and U2.

We also demand U1 and U2 for the flipped tableau tab.flip, in which the left and the right components of all sequents are swapped. This is not an extra demand: U1 and U2 are symmetric in the two components, so tab.UniCore and tab.flip.UniCore say the same thing. Asking for both here only spares us the purely technical work of transporting U1 and U2 along Tableau.flip, which would need a flip operation on FinePathIn. What it buys us is Tableau.isUniform.flip below, which is needed because the interpolation proof flips the tableau when the loaded formula is on the left.

Equations

• tab.isUniform = (tab.UniCore ∧ tab.flip.UniCore)

theorem Tableau.UniCore.heq_transfer {H₁ : History} {X₁ : Sequent} {H₂ : History} {X₂ : Sequent} {t₁ : Tableau H₁ X₁} {t₂ : Tableau H₂ X₂} (hH : H₁ = H₂) (hX : X₁ = X₂) (h : t₁ ≍ t₂) (h₁ : t₁.UniCore) : t₂.UniCore

Transporting Tableau.UniCore along an equality of tableaux.

theorem Tableau.isUniform.flip {H : History} {X : Sequent} {tab : Tableau H X} (h : tab.isUniform) : tab.flip.isUniform

Uniformity is preserved by flipping the tableau.

Uniform tableaux by construction

To obtain uniform tableaux we follow approach (B): instead of repairing a given tableau we describe how a uniform one is built, by fixing which local rule is applied at each node. The conditions U1 and U2 only speak about the local rules applied at the nodes, and both are conditions that can be read off a single rule application together with the sequent it is applied to. This is what LocalRuleApp.IsUniChoice below says:

• the rule is applied to the unloaded component, unless that component is basic (U1); and
• if it is applied to the loaded component (the unloaded one then being basic) then it is the canonical rule for that component, given by uniRightChoice resp. uniLeftChoice.

Since the canonical rule only depends on the loaded component Λᵢ(s), any two nodes with the same loaded component use the same rule, which is U2. A tableau all of whose rule applications are IsUniChoice is called Tableau.IsUni, and Tableau.IsUni.uniCore shows that such a tableau indeed satisfies U1 and U2. The construction is symmetric under flipping (Tableau.IsUni.flip), which gives the second half of Tableau.isUniform.

Flipping components, rules and rule applications

@[simp]

theorem LocalRuleApp.flip_O (lra : LocalRuleApp) : lra.flip.O = lra.O.flip

@[simp]

theorem LocalRuleApp.flip_X (lra : LocalRuleApp) : lra.flip.X = lra.X.flip

@[simp]

theorem LocalRuleApp.flip_isRightRule (lra : LocalRuleApp) : lra.flip.isRightRule = lra.isLeftRule

@[simp]

theorem LocalRuleApp.flip_isLeftRule (lra : LocalRuleApp) : lra.flip.isLeftRule = lra.isRightRule

@[simp]

theorem Sequent.flip_leftFree {X : Sequent} : X.flip.leftFree = X.rightFree.flip

@[simp]

theorem Sequent.flip_rightFree {X : Sequent} : X.flip.rightFree = X.leftFree.flip

@[simp]

theorem Sequent.flip_rightOnly {X : Sequent} : X.flip.rightOnly = X.leftOnly.flip

@[simp]

theorem Sequent.flip_leftOnly {X : Sequent} : X.flip.leftOnly = X.rightOnly.flip

theorem LocalRuleApp.SameRuleAs.flip {lra₁ lra₂ : LocalRuleApp} (h : lra₁.SameRuleAs lra₂) : lra₁.flip.SameRuleAs lra₂.flip

Being the same rule is preserved by flipping.

theorem LocalRuleApp.SameRuleAs.refl (lra : LocalRuleApp) : lra.SameRuleAs lra

Being the same rule is reflexive.

theorem LocalRuleApp.SameRuleAs.symm {lra₁ lra₂ : LocalRuleApp} (h : lra₁.SameRuleAs lra₂) : lra₂.SameRuleAs lra₁

Being the same rule is symmetric.

theorem LocalRuleApp.SameRuleAs.trans {lra₁ lra₂ lra₃ : LocalRuleApp} (h : lra₁.SameRuleAs lra₂) (h' : lra₂.SameRuleAs lra₃) : lra₁.SameRuleAs lra₃

Being the same rule is transitive.

The canonical rule for a component

def uniRightChoice (Y : Sequent) : Option LocalRuleApp

The canonical local rule to be applied to the right component of a sequent. We use the first right rule in the list LocalRuleApp.all of all applicable rules. Which rule exactly is picked does not matter for uniformity; all that matters is that this is a function of the sequent — and that it is applied to sequents of the form X.rightOnly, so that it only depends on the right component.

Equations

• uniRightChoice Y = List.find? (fun (lra : LocalRuleApp) => lra.isRightRule) (LocalRuleApp.all Y)

def uniLeftChoice (Y : Sequent) : Option LocalRuleApp

The canonical local rule to be applied to the left component of a sequent. Defined as the flip of uniRightChoice, which makes the whole construction symmetric.

Equations

• uniLeftChoice Y = Option.map LocalRuleApp.flip (uniRightChoice Y.flip)

theorem uniLeftChoice_flip (Y : Sequent) : uniLeftChoice Y.flip = Option.map LocalRuleApp.flip (uniRightChoice Y)

theorem uniRightChoice_flip (Y : Sequent) : uniRightChoice Y.flip = Option.map LocalRuleApp.flip (uniLeftChoice Y)

Uniform rule applications

structure LocalRuleApp.IsUniChoice (lra : LocalRuleApp) : Prop

The conditions on a single local rule application in a uniform tableau: the first two fields are the local form of U1 and the last two are the local form of U2.

• leftFirst : lra.X.2.2.isRight → ¬lra.X.leftFree.basic → lra.isLeftRule = true

  If loaded on the right and the left component is not basic, a left rule is applied.

• rightFirst : lra.X.2.2.isLeft → ¬lra.X.rightFree.basic → lra.isRightRule = true

  If loaded on the left and the right component is not basic, a right rule is applied.

• rightCanon : lra.isRightRule = true → lra.X.2.2.isRight → lra.X.leftFree.basic → ∃ (lrb : LocalRuleApp), uniRightChoice lra.X.rightOnly = some lrb ∧ lra.SameRuleAs lrb

  A right rule applied at a node loaded on the right whose left component is basic is the canonical rule for the right component.

• leftCanon : lra.isLeftRule = true → lra.X.2.2.isLeft → lra.X.rightFree.basic → ∃ (lrb : LocalRuleApp), uniLeftChoice lra.X.leftOnly = some lrb ∧ lra.SameRuleAs lrb

  A left rule applied at a node loaded on the left whose right component is basic is the canonical rule for the left component.

theorem LocalRuleApp.IsUniChoice.flip {lra : LocalRuleApp} (h : lra.IsUniChoice) : lra.flip.IsUniChoice

The conditions on rule applications are symmetric under flipping.

Basic sequents have basic components

theorem Sequent.leftFree_basic_of_basic {X : Sequent} (h : X.basic) : X.leftFree.basic

theorem Sequent.rightFree_basic_of_basic {X : Sequent} (h : X.basic) : X.rightFree.basic

def LocalTableau.IsUni {X : Sequent} : LocalTableau X → Prop

All local rule applications inside a local tableau are uniform choices.

Equations

• (LocalTableau.sim a).IsUni = True
• (LocalTableau.byLocalRule lra X_def next).IsUni = (lra.IsUniChoice ∧ ∀ (Y : Sequent) (h : Y ∈ lra.C), (next Y h).IsUni)

def Tableau.IsUni {H : History} {X : Sequent} : Tableau H X → Prop

All local rule applications inside a tableau are uniform choices.

Equations

• (Tableau.loc nflprep nbas lt next).IsUni = (lt.IsUni ∧ ∀ (Y : Sequent) (h : Y ∈ endNodesOf lt), (next Y h).IsUni)
• (Tableau.pdl nflprep bas r next).IsUni = next.IsUni
• (Tableau.lrep lpr).IsUni = True

theorem LocalTableau.IsUni.ltAt {X : Sequent} {lt : LocalTableau X} (h : lt.IsUni) (lp : LocalPathIn lt) : lp.ltAt.IsUni

theorem Tableau.IsUni.lra?_isUniChoice {H : History} {X : Sequent} {tab : Tableau H X} (h : tab.IsUni) {f : FinePathIn tab} {lra : LocalRuleApp} (hf : f.lra? = some lra) : lra.IsUniChoice

theorem FinePathIn.usesLeftRule_eq_of_lra? {H : History} {X : Sequent} {tab : Tableau H X} {f : FinePathIn tab} {lra : LocalRuleApp} (hf : f.lra? = some lra) : f.usesLeftRule = lra.isLeftRule

theorem FinePathIn.usesRightRule_eq_of_lra? {H : History} {X : Sequent} {tab : Tableau H X} {f : FinePathIn tab} {lra : LocalRuleApp} (hf : f.lra? = some lra) : f.usesRightRule = lra.isRightRule

theorem FinePathIn.isLrep_or_basic_of_lra?_eq_none {H : History} {X : Sequent} {tab : Tableau H X} {f : FinePathIn tab} (hf : f.lra? = none) : f.base.isLrep ∨ f.label.basic

theorem Tableau.IsUni.uniCore {H : History} {X : Sequent} {tab : Tableau H X} (h : tab.IsUni) : tab.UniCore

theorem LocalTableau.IsUni_cast {A B : Sequent} (h : A = B) (t : LocalTableau A) : (h ▸ t).IsUni ↔ t.IsUni

theorem Tableau.IsUni_cast {H : History} {A B : Sequent} (h : A = B) (t : Tableau H A) : (h ▸ t).IsUni ↔ t.IsUni

theorem LocalTableau.IsUni.flip {X : Sequent} {lt : LocalTableau X} (h : lt.IsUni) : lt.flip.IsUni

theorem Tableau.IsUni.flip {H : History} {X : Sequent} {tab : Tableau H X} (h : tab.IsUni) : tab.flip.IsUni

theorem Tableau.IsUni.isUniform {X : Sequent} {tab : Tableau [] X} (h : tab.IsUni) : tab.isUniform

A tableau all of whose local rule applications are uniform choices is uniform.

Building a uniform tableau

We now show Tableau.exists_isUni: for every tableau there is one that applies the rules in the canonical order. The construction is deterministic: uniChoiceAt picks, at each sequent, the canonical rule application (first a rule for the unloaded component, and once that is basic the canonical rule for the loaded component), and uniLocalTab iterates this to a local tableau all of whose rule applications are uniform choices (uniLocalTab_isUni).

Given an arbitrary tableau we then re-build it, replacing the local tableau at each loc step by the canonical one. Because the end nodes of the canonical local tableau need not be literally the same lists as the end nodes of the original one, we prove the statement in the more flexible form Tableau.exists_isUni_of_msEq, allowing the sequent and the history to change up to Sequent.multisetEqTo, i.e. up to permutation of the two lists in a sequent. That the calculus does not care about such permutations is PdlRule.exists_of_multisetEqTo and lpr_of_multisetEqTo.

The only step that is left open is uniLocalTab_endNode_dominated.

def LocalRuleApp.inContext (lra : LocalRuleApp) (L R : Finset Formula) (O : Olf) (hL : lra.Lcond ⊆ L) (hR : lra.Rcond ⊆ R) (hO : lra.Ocond ⊆ O) : LocalRuleApp

Put a local rule application into a different context, keeping the rule itself.

Equations

• lra.inContext L R O hL hR hO = { L := L, R := R, O := O, Lcond := lra.Lcond, Rcond := lra.Rcond, Ocond := lra.Ocond, ress := lra.ress, lr := lra.lr, hC := ⋯, preconditionProof := ⋯ }

def LocalRuleApp.toContext (lra : LocalRuleApp) (X : Sequent) : LocalRuleApp

Put a local rule application into the context of the sequent X, if possible.

Equations

• lra.toContext X = if h : lra.Lcond ⊆ X.1 ∧ lra.Rcond ⊆ X.2.1 ∧ lra.Ocond ⊆ X.2.2 then lra.inContext X.1 X.2.1 X.2.2 ⋯ ⋯ ⋯ else lra

theorem LocalRuleApp.toContext_sameRuleAs (lra : LocalRuleApp) (X : Sequent) : (lra.toContext X).SameRuleAs lra

@[simp]

theorem LocalRuleApp.toContext_isLeftRule (lra : LocalRuleApp) (X : Sequent) : (lra.toContext X).isLeftRule = lra.isLeftRule

@[simp]

theorem LocalRuleApp.toContext_isRightRule (lra : LocalRuleApp) (X : Sequent) : (lra.toContext X).isRightRule = lra.isRightRule

theorem LocalRuleApp.toContext_X (lra : LocalRuleApp) (X : Sequent) (h : lra.Lcond ⊆ X.1 ∧ lra.Rcond ⊆ X.2.1 ∧ lra.Ocond ⊆ X.2.2) : (lra.toContext X).X = X

theorem uniRightChoice_spec {Y : Sequent} {lra : LocalRuleApp} (h : uniRightChoice Y = some lra) : lra.X = Y ∧ lra.isRightRule = true

theorem uniRightChoice_isSome {Y : Sequent} {lra : LocalRuleApp} (hX : lra.X = Y) (hr : lra.isRightRule = true) : (uniRightChoice Y).isSome = true

theorem uniLeftChoice_spec {Y : Sequent} {lra : LocalRuleApp} (h : uniLeftChoice Y = some lra) : lra.X = Y ∧ lra.isLeftRule = true

theorem uniLeftChoice_isSome {Y : Sequent} {lra : LocalRuleApp} (hX : lra.X = Y) (hl : lra.isLeftRule = true) : (uniLeftChoice Y).isSome = true

Shapes of left and right rules

theorem LocalRuleApp.isLeftRule_shape {lra : LocalRuleApp} (h : lra.isLeftRule = true) : lra.Rcond = ∅ ∧ (lra.Ocond = none ∨ lra.Ocond.isLeft)

theorem LocalRuleApp.isRightRule_shape {lra : LocalRuleApp} (h : lra.isRightRule = true) : lra.Lcond = ∅ ∧ (lra.Ocond = none ∨ lra.Ocond.isRight)

theorem LocalRuleApp.isLeftRule_of_X_eq {lra : LocalRuleApp} {L : Finset Formula} (h : lra.X = (L, ∅, none)) : lra.isLeftRule = true

Any local rule applicable to a sequent of the shape (L, ∅, none) is a left rule.

Moving rules between a sequent and its components

theorem LocalRuleApp.toContext_X_of_leftOnly {lra : LocalRuleApp} {X : Sequent} (h : lra.X = X.leftOnly) : (lra.toContext X).X = X

theorem LocalRuleApp.toContext_X_of_rightOnly {lra : LocalRuleApp} {X : Sequent} (h : lra.X = X.rightOnly) : (lra.toContext X).X = X

theorem LocalRuleApp.toContext_leftOnly_X {lra : LocalRuleApp} {X : Sequent} (hX : lra.X = X) (hl : lra.isLeftRule = true) : (lra.toContext X.leftOnly).X = X.leftOnly

theorem LocalRuleApp.toContext_rightOnly_X {lra : LocalRuleApp} {X : Sequent} (hX : lra.X = X) (hr : lra.isRightRule = true) : (lra.toContext X.rightOnly).X = X.rightOnly

theorem LocalRuleApp.toContext_leftFree_X {lra : LocalRuleApp} {X : Sequent} (hX : lra.X = X) (hl : lra.isLeftRule = true) (hO : lra.Ocond = none) : (lra.toContext X.leftFree).X = X.leftFree

When is the canonical choice available?

theorem exists_localRuleApp_of_not_basic {Y : Sequent} (h : ¬Y.basic) : ∃ (lra : LocalRuleApp), lra.X = Y

theorem uniLeftChoice_leftOnly_isSome {X : Sequent} (h : ¬X.leftFree.basic) : (uniLeftChoice X.leftOnly).isSome = true

theorem uniLeftChoice_leftOnly_eq_none {X : Sequent} (hb : X.leftFree.basic) (hO : ¬X.2.2.isLeft) : uniLeftChoice X.leftOnly = none

theorem uniRightChoice_rightOnly_isSome {X : Sequent} {lra : LocalRuleApp} (hX : lra.X = X) (hr : lra.isRightRule = true) : (uniRightChoice X.rightOnly).isSome = true

The canonical rule choice

def uniChoiceRL (X : Sequent) : Option LocalRuleApp

The canonical rule application for a sequent that is free or loaded on the right: first reduce the left component, then use the canonical rule for the right component.

Equations

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

theorem uniChoiceRL_X {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceRL X = some lra) : lra.X = X

theorem uniChoiceRL_isSome {X : Sequent} (h : ¬X.basic) : (uniChoiceRL X).isSome = true

theorem uniChoiceRL_isUniChoice {X : Sequent} {lra : LocalRuleApp} (hnl : ¬X.2.2.isLeft) (h : uniChoiceRL X = some lra) : lra.IsUniChoice

def uniChoiceAt (X : Sequent) : Option LocalRuleApp

The canonical local rule application at a sequent: when the sequent is loaded on the left we flip, use uniChoiceRL and flip back.

Equations

• uniChoiceAt X = if X.2.2.isLeft then Option.map LocalRuleApp.flip (uniChoiceRL X.flip) else uniChoiceRL X

theorem uniChoiceAt_X {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) : lra.X = X

theorem uniChoiceAt_isSome {X : Sequent} (h : ¬X.basic) : (uniChoiceAt X).isSome = true

theorem uniChoiceAt_isUniChoice {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) : lra.IsUniChoice

theorem uniChoiceAt_C_lt {X : Sequent} {lra : LocalRuleApp} (h : uniChoiceAt X = some lra) {Y : Sequent} (hY : Y ∈ lra.C) : lt_Sequent Y X

@[irreducible]

def uniLocalTab (X : Sequent) : LocalTableau X

The canonical local tableau: always apply the canonical rule uniChoiceAt.

Equations

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

theorem uniLocalTab_isUni (X : Sequent) : (uniLocalTab X).IsUni

Refutable sequents

To show that the local development of a sequent does not depend on the order in which the rules are applied we have to deal with clashes: one local tableau may close a branch with a closure rule while another one first decomposes the two clashing formulas. So we need to know that a clash cannot get lost, i.e. that after applying any local rule to a closed sequent the resulting sequents can still be closed.

We call a sequent Refutable if it has a local tableau without any end nodes. Note that we only ask for the existence of such a local tableau; this is all that is needed below, and it can be shown by purely syntactic means: the interesting case is when the rule applied is the box or the diamond unfolding for the two clashing formulas ⌈α⌉ψ and ~⌈α⌉ψ. There the branches of unfoldBox and of unfoldDiamond clash pairwise, either on a test or on a formula ⌈⌈δ⌉⌉ψ, which is Dset_mem_P_of_tests below.

theorem Dset_mem_P_of_tests (α : Program) (ℓ : TP α) (Fs : List Formula) (δ : List Program) (h : (Fs, δ) ∈ Dset α) (hF : ∀ τ ∈ Fs, ~τ ∉ F α ℓ) : δ ∈ P α ℓ

Refutable and dominated sequents

def Sequent.DominatedBy (W : Sequent) (Ys : Finset Sequent) : Prop

The sequent W is dominated by the finite set Ys if it has a local tableau all of whose end nodes occur in Ys.

Equations

• W.DominatedBy Ys = ∃ (lt : LocalTableau W), ∀ Y ∈ endNodesOf lt, Y ∈ Ys

def Sequent.Refutable (X : Sequent) : Prop

A sequent is refutable if it has a local tableau without any end nodes.

Equations

• X.Refutable = X.DominatedBy ∅

theorem Sequent.refutable_iff {X : Sequent} : X.Refutable ↔ ∃ (lt : LocalTableau X), endNodesOf lt = ∅

theorem Sequent.DominatedBy.mono {W : Sequent} {Ys Zs : Finset Sequent} (h : W.DominatedBy Ys) (hsub : Ys ⊆ Zs) : W.DominatedBy Zs

theorem Sequent.Refutable.dominatedBy {W : Sequent} (h : W.Refutable) (Ys : Finset Sequent) : W.DominatedBy Ys

theorem Sequent.DominatedBy.byRule {W : Sequent} {Ys : Finset Sequent} {lra : LocalRuleApp} (hX : lra.X = W) (h : ∀ V ∈ lra.C, V.DominatedBy Ys) : W.DominatedBy Ys

If all children of a rule application are dominated by Ys then so is the sequent.

theorem Sequent.Refutable.of_closed {X : Sequent} (h : X.closed) : X.Refutable

A closed sequent is refutable: a closure rule can be applied to it.

Clashes survive the application of a rule

The next lemmas say that a clash in a sequent cannot be lost by applying a local rule: the results are again refutable. The interesting cases are those where the rule is applied to one of the two clashing formulas.

theorem Sequent.Refutable.byOneSided {X : Sequent} {p : Formula} {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule {p} ress) (hp : p ∈ X) (h : ∀ res ∈ ress, ∀ (W : Sequent), (∀ f ∈ X, f ≠ p → f ∈ W) → (∀ φ ∈ res, φ ∈ W) → W.Refutable) : X.Refutable

To show that X is refutable it suffices to apply a one-sided rule to a formula p of X and to refute all the results. The resulting sequents are only described by two properties, so that we do not have to care about which of the two components p is in: all formulas of X other than p are still present, and the result of the rule was added.

theorem Formula.ne_of_length_lt {φ ψ : Formula} (h : lengthOfFormula φ < lengthOfFormula ψ) : φ ≠ ψ

Two formulas of different length are different.

theorem Formula.ne_of_length_ne {φ ψ : Formula} (h : lengthOfFormula φ ≠ lengthOfFormula ψ) : φ ≠ ψ

Two formulas of different length are different.

theorem Sequent.closed.append {L R Ln Rn : Finset Formula} {O O' : Olf} (hX : closed (L, R, O)) : closed (L ∪ Ln, R ∪ Rn, O')

Adding formulas to a closed sequent keeps it closed.

theorem OneSidedLocalRule.singleton_precond {pre : Finset Formula} {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule pre ress) (h : ress ≠ ∅) : ∃ (p : Formula), pre = {p}

A one-sided rule that is not a closure rule has exactly one principal formula.

theorem lengthOfFormula_lt_of_mem_testsOfProgram {α : Program} {τ : Formula} : τ ∈ testsOfProgram α → lengthOfFormula τ < lengthOfProgram α

Tests are shorter than the program they occur in.

theorem boxes_ne_neg {δ : List Program} {ψ χ : Formula} (h : lengthOfFormula ψ ≤ lengthOfFormula χ) : (⌈⌈δ⌉⌉ψ) ≠ ~χ

A list of boxes in front of a short formula is not the negation of a longer one.

theorem ne_neg_box_of_mem_Bset {α : Program} {ψ : Formula} {ℓ : TP α} {f : Formula} (hf : f ∈ Bset α ℓ ψ) : f ≠ ~⌈α⌉ψ

A formula in the unfolding of ⌈α⌉ψ is not ~⌈α⌉ψ.

theorem ne_box_of_mem_Yset {α : Program} {ψ : Formula} {Fs : List Formula} {δ : List Program} (hFδ : (Fs, δ) ∈ Dset α) {f : Formula} (hf : f ∈ Yset (Fs, δ) ψ) : (f ≠ ⌈α⌉ψ) ∧ f ≠ ~~⌈α⌉ψ

A formula in the unfolding of ~⌈α⌉ψ is neither ⌈α⌉ψ nor ~~⌈α⌉ψ.

theorem Bset_Yset_clash {α : Program} {ψ : Formula} (ℓ : TP α) {Fs : List Formula} {δ : List Program} (hFδ : (Fs, δ) ∈ Dset α) : ∃ (f : Formula), f ∈ Bset α ℓ ψ ∧ ~f ∈ Yset (Fs, δ) ψ ∨ ~f ∈ Bset α ℓ ψ ∧ f ∈ Yset (Fs, δ) ψ

The branches of the box unfolding and of the diamond unfolding clash. Given a test profile ℓ and a pair (Fs, δ) ∈ Dset α, the two lists Bset α ℓ ψ and Yset (Fs, δ) ψ contain a formula and its negation: either the two disagree about a test, or δ ∈ P α ℓ and then ⌈⌈δ⌉⌉ψ is in the first and ~⌈⌈δ⌉⌉ψ is in the second list.

theorem refutable_of_negneg {X : Sequent} {χ : Formula} (h1 : χ ∈ X) (h2 : ~ ~~χ ∈ X) : X.Refutable

theorem refutable_of_con_nCo {X : Sequent} {χ ρ : Formula} (h1 : χ ∈ X) (h2 : ρ ∈ X) (h3 : ~(χ ⋀ ρ) ∈ X) : X.Refutable

theorem refutable_of_nCo_con {X : Sequent} {χ ρ : Formula} (h1 : ~χ ∈ X ∨ ~ρ ∈ X) (h2 : χ ⋀ ρ ∈ X) : X.Refutable

theorem refutable_of_nCo_negneg {X : Sequent} {χ ρ : Formula} (h1 : ~χ ∈ X ∨ ~ρ ∈ X) (h2 : ~~(χ ⋀ ρ) ∈ X) : X.Refutable

theorem refutable_of_box_dia {X : Sequent} {α : Program} {ψ : Formula} {ℓ : TP α} (hna : ¬α.isAtomic) (hB : ∀ φ ∈ Bset α ℓ ψ, φ ∈ X) (hd : (~⌈α⌉ψ) ∈ X) : X.Refutable

theorem refutable_of_dia_box {X : Sequent} {α : Program} {ψ : Formula} {Fs : List Formula} {δ : List Program} (hna : ¬α.isAtomic) (hFδ : (Fs, δ) ∈ Dset α) (hY : ∀ φ ∈ Yset (Fs, δ) ψ, φ ∈ X) (hb : (⌈α⌉ψ) ∈ X) : X.Refutable

theorem refutable_of_dia_negneg {X : Sequent} {α : Program} {ψ : Formula} {Fs : List Formula} {δ : List Program} (hna : ¬α.isAtomic) (hFδ : (Fs, δ) ∈ Dset α) (hY : ∀ φ ∈ Yset (Fs, δ) ψ, φ ∈ X) (hb : (~~⌈α⌉ψ) ∈ X) : X.Refutable

theorem Sequent.Refutable.of_oneSided_step {X W : Sequent} (hX : X.closed) {p : Formula} {pre : Finset Formula} {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule pre ress) (hpre : pre = {p}) {res : Finset Formula} (hres : res ∈ ress) (hsurv : ∀ f ∈ X, f ≠ p → f ∈ W) (hmem : ∀ φ ∈ res, φ ∈ W) : W.Refutable

A clash survives a one-sided rule. If X is closed and W is obtained from X by removing the principal formula p of a one-sided rule and adding one of its results, then W is refutable.

theorem Sequent.Refutable.child_of_closed {X W : Sequent} (hX : X.closed) {lra : LocalRuleApp} (hXl : lra.X = X) (hW : W ∈ lra.C) : W.Refutable

A clash survives any local rule: every child of a rule application to a closed sequent is refutable.

Closure rules

A local rule has no results if and only if it is one of the closure rules. For the direction we need here we must know that the box and diamond unfoldings are never empty.

theorem unfoldBox_ne_nil (a : Program) (phi : Formula) : unfoldBox a phi ≠ []

The box unfolding is never empty.

theorem Dset_ne_nil (a : Program) : Dset a ≠ []

The program unfolding used for diamonds is never empty.

theorem LocalRuleApp.closed_of_ress_nil {lra : LocalRuleApp} (h : lra.ress = ∅) : lra.X.closed

A rule without results is a closure rule, so the sequent it is applied to is closed.

theorem LocalRuleApp.shape_of_ress_ne_nil {lra : LocalRuleApp} (h : lra.ress ≠ ∅) : (∃ (p : Formula), lra.Lcond = {p} ∧ lra.Rcond = ∅ ∧ lra.Ocond = none ∧ ∀ Y ∈ lra.ress, Y.2.2 = none) ∨ (∃ (p : Formula), lra.Lcond = ∅ ∧ lra.Rcond = {p} ∧ lra.Ocond = none ∧ ∀ Y ∈ lra.ress, Y.2.2 = none) ∨ lra.Lcond = ∅ ∧ lra.Rcond = ∅ ∧ lra.Ocond ≠ none

The shape of a rule application that is not a closure rule: it has exactly one principal formula, in the left component, in the right component, or the loaded formula.

theorem LocalRuleApp.Ocond_eq_O {lra : LocalRuleApp} (h : lra.Ocond ≠ none) : lra.Ocond = lra.O

A loaded rule can only be applied when its condition is the loaded formula present.

theorem LocalRuleApp.C_eq (lra : LocalRuleApp) : lra.C = Finset.image (fun (Z : Sequent) => (lra.L \ lra.Lcond ∪ Z.1, lra.R \ lra.Rcond ∪ Z.2.1, lra.O.change lra.Ocond Z.2.2)) lra.ress

The children of a rule application, written out.

theorem LocalRuleApp.exists_at (lra : LocalRuleApp) (Y : Sequent) (hL : lra.Lcond ⊆ Y.1) (hR : lra.Rcond ⊆ Y.2.1) (hO : lra.Ocond ⊆ Y.2.2) : ∃ (lra' : LocalRuleApp), lra'.X = Y ∧ lra'.C = Finset.image (fun (Z : Sequent) => (Y.1 \ lra.Lcond ∪ Z.1, Y.2.1 \ lra.Rcond ∪ Z.2.1, Y.2.2.change lra.Ocond Z.2.2)) lra.ress

A rule can be applied at any sequent that satisfies its precondition.

theorem endNodesOf_of_basic {X : Sequent} (bas : X.basic) (lt : LocalTableau X) : endNodesOf lt = {X}

A local tableau for a basic sequent has that sequent as its only end node.

Helpers

These are copies of results in Pdl.ClusterInterpolation, which are not available here because that file imports this one.

theorem Uniformity.basic_rightOnly {X : Sequent} (h : X.basic) : X.rightOnly.basic

The right component of a basic sequent is basic. Same as Sequent.basic_rightOnly in Pdl.ClusterInterpolation.

theorem Uniformity.not_rightOnly_basic_of_isRightRule (lra : LocalRuleApp) (h : lra.isRightRule = true) : ¬lra.X.rightOnly.basic

A right local rule cannot be applied when the right component of the sequent is basic. Same as LocalRuleApp.not_rightOnly_basic_of_isRightRule in Pdl.ClusterInterpolation.

theorem Uniformity.lra_or_basic_of_usesRightRule {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : f.usesRightRule = true → (∃ (lra : LocalRuleApp), f.lra? = some lra ∧ lra.isRightRule = true) ∨ f.label.basic

Where a right rule is applied, it is either a local rule or the node is basic. Same as FinePathIn.lra_or_basic_of_usesRightRule in Pdl.ClusterInterpolation.

def Uniformity.modRChildRight (A : ℕ) (ξ : AnyFormula) (R : Finset Formula) : Sequent

The right component of the child obtained by applying the modal rule (M) to a sequent whose loaded formula ~⌊·A⌋ξ is on the right. Same as modRChildRightOnly in Pdl.ClusterInterpolation.

Equations

• Uniformity.modRChildRight A (AnyFormula.normal φ) R = (∅, {~φ} ∪ Finset.projection A R, none)
• Uniformity.modRChildRight A (AnyFormula.loaded χ) R = (∅, Finset.projection A R, some (Sum.inr (~'χ)))

theorem Uniformity.basicRightStep {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.usesRightRule = true) (hb : f.label.rightOnly.basic) : f.atBigRoot = true ∧ f.label.2.2 = none ∨ (∃ (g : FinePathIn tab'), f.children = {g} ∧ g.atBigRoot = true ∧ g.label.2.2 = none) ∨ ∃ (A : ℕ) (ξ : AnyFormula), f.label.2.2 = some (Sum.inr (~'⌊·A⌋ξ)) ∧ ∃ (g : FinePathIn tab'), f.children = {g} ∧ g.atBigRoot = true ∧ g.label.left = Finset.projection A f.label.left ∧ g.label.rightOnly = modRChildRight A ξ f.label.2.1

At a fine node with a basic right component where a right rule is applied, that rule is one of the three PdlRules acting on the right. Same as FinePathIn.basicRightStep in Pdl.ClusterInterpolation.

theorem Uniformity.label_eq_nodeAt_base {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') (h : f.atBigRoot = true) : f.label = nodeAt f.base

A fine node that is a node in the coarse sense has the label of that coarse node. Same as FinePathIn.label_eq_nodeAt_base in Pdl.ClusterInterpolation.

theorem Uniformity.isRight_of_mem_C (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → Y.2.2.isRight → lra.X.2.2.isRight

If a child of a local rule application is loaded on the right, then so is its premise. Same as LocalRuleApp.isRight_of_mem_C in Pdl.ClusterInterpolation.

theorem Uniformity.isRight_of_mem_endNodesOf {Z : Sequent} (lt : LocalTableau Z) (Y : Sequent) : Y ∈ endNodesOf lt → Y.2.2.isRight → Z.2.2.isRight

If some end node of a local tableau is loaded on the right, then so is its root. Same as LocalTableau.isRight_of_mem_endNodesOf in Pdl.ClusterInterpolation.

theorem Uniformity.mem_endNodesOf_ltAt {Z : Sequent} {lt : LocalTableau Z} (lp : LocalPathIn lt) (Yh : ↥(endNodesOf lt)) : Yh ∈ lp.endNodesBelow → ↑Yh ∈ endNodesOf lp.ltAt

The end nodes below a local path are end nodes of the local tableau at that path. Same as LocalPathIn.mem_endNodesOf_ltAt in Pdl.ClusterInterpolation.

theorem Uniformity.isRight_of_mem_coarseChildrenBelow {H : History} {Z : Sequent} {tab' : Tableau H Z} (f : FinePathIn tab') : ¬f.atBigRoot = true → ∀ q ∈ f.coarseChildrenBelow, (nodeAt q).2.2.isRight → f.label.2.2.isRight

A fine node that is not a coarse node and has a coarse child loaded on the right is itself loaded on the right. Same as FinePathIn.isRight_of_mem_coarseChildrenBelow in Pdl.ClusterInterpolation.

theorem Uniformity.isRight_of_memFine {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {f : FinePathIn tab} (hf : C.memFine f) : f.label.2.2.isRight

Lemma 9.4 (a) at the fine level: every fine node of a loaded cluster is loaded on the right. For a coarse node this is LoadedCluster.all_right_loaded, and for a node inside a local tableau it follows because that node has a coarse child in the cluster.

theorem Uniformity.basicModalStep {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (hb : Δ.basic) {t : FinePathIn tab} (ht : t ∈ C.nodesWithFineRight Δ) : ∃ (A : ℕ) (ξ : AnyFormula), Δ.2.2 = some (Sum.inr (~'⌊·A⌋ξ)) ∧ ∃ (g : FinePathIn tab), t.children = {g} ∧ g.label.rightOnly = modRChildRight A ξ Δ.2.1

Lemma 9.7 (e): at a node t of C^R_Δ with Δ basic the rule applied is the modal rule (M) for the loaded formula ~⌊·A⌋ξ of Δ, so that the right component of the unique child of t only depends on Δ. Same as LoadedCluster.basicModalStepAt in Pdl.ClusterInterpolation.

theorem Uniformity.map_rightOnly_C_eq {lra₁ lra₂ : LocalRuleApp} (hsame : lra₁.SameRuleAs lra₂) (hX : lra₁.X.rightOnly = lra₂.X.rightOnly) : Finset.image Sequent.rightOnly lra₁.C = Finset.image Sequent.rightOnly lra₂.C

The key computation for condition U2: if the same local rule with the same principal formulas is applied at two nodes with the same right component, then the right components of the children agree, including their order. This holds because a local rule application deletes the principal formulas from, and adds the results to, the given sequent.

theorem LoadedCluster.uniformOfUniTab {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (uni_tab : tab.isUniform) : C.HasUniformSteps

In a uniform tableau any loaded cluster has the property HasUniformSteps needed for the construction of the quasi-tableau: 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.

The case where Δ is basic does not use uniformity: there the rule applied is the modal rule for the loaded formula of Δ (Lemma 9.7 (e)). The case where Δ is not basic is Lemma 9.7 (f), and uses both U1 and U2.