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 LoadedCluster.basicModalStepAt — 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 LocalRuleApp.SameRuleAs.map_rightOnly_C_eq.

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 this component 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 a uniform tableau we do not try to repair a given tableau, but instead 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.

theorem LocalRuleApp.SameRuleAs.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.

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 local tableau

We now define uniLocalTab, a tableau 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).

Later the this uniform local tableau is used in Move and gameP_general.

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_rightOnly_X {lra : LocalRuleApp} {X : Sequent} (hX : lra.X = X) (hr : lra.isRightRule = true) : (lra.toContext X.rightOnly).X = X.rightOnly

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 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

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.