Interpolants for Partitions (big part of Section 7)

Note that we can skip much of subsection 7.3 because we worked already with split tableaux anyway.

Joint vocabulary

def jvoc (X : Sequent) : Vocab

The joint vocabulary occurring on both the left and the right side.

Equations

• jvoc X = X.left.fvoc ∩ X.right.fvoc

theorem jvoc_sub_of_voc_sub {Y X : Sequent} (hl : Y.left.fvoc ⊆ X.left.fvoc) (hr : Y.right.fvoc ⊆ X.right.fvoc) : jvoc Y ⊆ jvoc X

Partition Interpolants

def isPartInterpolant (X : Sequent) (θ : Formula) : Prop

Equations

• isPartInterpolant X θ = (θ.voc ⊆ jvoc X ∧ ¬HasSat.satisfiable (~θ :: X.left) ∧ ¬HasSat.satisfiable (θ :: X.right))

def PartInterpolant (N : Sequent) : Type

Equations

• PartInterpolant N = Subtype (isPartInterpolant N)

def onlfvoc : Option NegLoadFormula → Vocab

Like Olf.voc but without the ⊕ inside.

Equations

• onlfvoc none = ∅
• onlfvoc (some nlf) = nlf.voc

def lfovoc (L : List (List Formula × Option NegLoadFormula)) : Vocab

Equations

• lfovoc L = L.toFinset.sup fun (x : List Formula × Option NegLoadFormula) => match x with | (fs, o) => fs.fvoc ∪ onlfvoc o

Interpolants for local rules

theorem LoadRule_voc {χ : LoadFormula} {ress : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) ress) : lfovoc ress ⊆ χ.voc

theorem localRule_does_not_increase_vocab_L {Cond : Sequent} {B : List Sequent} (rule : LocalRule Cond B) (res : Sequent) : res ∈ B → res.left.fvoc ⊆ Cond.left.fvoc

theorem localRule_does_not_increase_vocab_R {Cond : Sequent} {B : List Sequent} (rule : LocalRule Cond B) (res : Sequent) : res ∈ B → res.right.fvoc ⊆ Cond.right.fvoc

theorem localRuleApp_does_not_increase_jvoc (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → jvoc Y ⊆ jvoc lra.X

def localInterpolantStep (lra : LocalRuleApp) (subθs : (c : Sequent) → c ∈ lra.C → PartInterpolant c) : PartInterpolant lra.X

Maehara's method for single-step local rule applications. This covers easy cases without any loaded path repeats. We do not use localRuleTruth to prove this, but the more specific lemmas oneSidedL_sat_down and oneSidedL_sat_down.

Equations

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

Interpolants for Local Tableau

def LocalTableau.interpolant {X : Sequent} (ltX : LocalTableau X) (endθs : (Y : Sequent) → Y ∈ endNodesOf ltX → PartInterpolant Y) : PartInterpolant X

Equations

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

Interpolants for PdlRules applied to free nodes

The only rule treated here is (L+), i.e. loadL and loadR.

def freePdlRuleInterpolant {X Y : Sequent} (r : PdlRule X Y) (Xfree : X.isFree = true) (θY : PartInterpolant Y) : PartInterpolant X

Equations

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

Cluster tools

def repeatsOf {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) : List (PathIn tab)

Equations

• repeatsOf s = sorry

def all_cEdge {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) : List (PathIn tab)

Equations

• all_cEdge s = sorry

theorem all_cEdge_spec {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : t ∈ all_cEdge s ↔ s ⋖_ t ∨ s ♥ t

def all_cEdge_rev {X : Sequent} {tab : Tableau [] X} (t : PathIn tab) : List (PathIn tab)

Equations

• all_cEdge_rev t = sorry

theorem all_cEdge_rev_spec {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : s ∈ all_cEdge_rev t ↔ s ⋖_ t ∨ s ♥ t

def loadedBelow {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : PathIn tab → List (PathIn tab)

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

Equations

• loadedBelow = sorry

def loadedAbove {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : PathIn tab → List (PathIn tab)

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

Equations

• loadedAbove = sorry

def clusterListOf {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) : List (PathIn tab)

List 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 ∩ loadedBelow p

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

def rootOf {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : List (PathIn tab) → PathIn tab

Equations

• rootOf = sorry

theorem cluster_all_left_loaded {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {p : PathIn tab} (h : (nodeAt p).2.2.isLeft) (q : PathIn tab) : q ∈ clusterListOf p → (nodeAt q).2.2.isLeft

Lemma 7.22 (b) for left side

theorem cluster_all_right_loaded {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {p : PathIn tab} (h : (nodeAt p).2.2.isRight) (q : PathIn tab) : q ∈ clusterListOf p → (nodeAt q).2.2.isRight

Lemma 7.22 (b) for right side

def isExitIn : Sequent → List Sequent → Prop

Equations

• isExitIn = sorry

instance instDecidableIsExitIn {X : Sequent} {C : List Sequent} : Decidable (isExitIn X C)

Equations

• instDecidableIsExitIn = sorry

Quasi-Tableaux

inductive Typ : Type

• one : Typ
• two : Typ
• three : Typ

inductive QuasiTab : Type

Simple tree data type for Q in Def. 7.31.

• QNode (k : Typ) (Δ : Sequent) (next : List QuasiTab) : QuasiTab

@[irreducible]

def Qchildren (C : List Sequent) (k : Typ) (Hist : List Sequent) (X : Sequent) : List QuasiTab

Equations

• Qchildren C Typ.one x✝¹ x✝ = if x✝ ∈ x✝¹ ∨ isExitIn x✝ C then [] else [QuasiTab.QNode Typ.two x✝ (Qchildren C Typ.two (x✝ :: x✝¹) x✝)]
• Qchildren C Typ.two x✝¹ x✝ = [QuasiTab.QNode Typ.three x✝ (Qchildren C Typ.three (x✝ :: x✝¹) x✝)]
• Qchildren C Typ.three x✝¹ x✝ = if x✝.basic then sorry else sorry

def Q {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {r : PathIn tab} : QuasiTab

Quasi-Tableau from Def 7.31. Here we "start the construction", then use Qchildren. No names for the nodes as we use an inductive type, so we just write X for Δₓ

Equations

• Q = QuasiTab.QNode Typ.one (nodeAt r) (Qchildren (List.map nodeAt (clusterListOf r)) Typ.one [] (nodeAt r))

Interpolants for proper clusters

def exitsOf {Hist : History} {L R : List Formula} {nlf : NegLoadFormula ⊕ NegLoadFormula} (tab : Tableau Hist (L, R, some nlf)) : List (PathIn tab)

The exits of a cluster: (C \ C+).

Equations

• exitsOf (Tableau.lrep lpr) = []
• exitsOf (Tableau.loc nrep nbas lt next) = sorry
• exitsOf (Tableau.pdl nrep bas r next) = sorry

def PathIn.children {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) : List (PathIn tab)

Equations

• PathIn.children = sorry

def plus_exits {X : Sequent} {tab : Tableau [] X} (C : List (PathIn tab)) : List (PathIn tab)

Exits from a given list of nodes. Something like this should get us from C to C+.

Equations

• plus_exits C = C ++ (List.map (fun (p : PathIn tab) => p.children) C).flatten

def clusterInterpolation_right {Hist : History} {L R : List Formula} {nlf : NegLoadFormula} (tab : Tableau Hist (L, R, some (Sum.inr nlf))) (exitIPs : (e : PathIn tab) → e ∈ exitsOf tab → PartInterpolant (nodeAt e)) : PartInterpolant (L, R, some (Sum.inr nlf))

Specific version of clusterInterpolation where loaded formula is on the right side.

Equations

• clusterInterpolation_right tab exitIPs = sorry

The following lemma about PathIn.flip is here because it is also about exitsOf.

theorem mem_existsOf_of_flip {Hist : History} {L R : List Formula} {nlf : NegLoadFormula ⊕ NegLoadFormula} {tab : Tableau Hist (L, R, some nlf)} {s : PathIn tab.flip} (s_in : s ∈ exitsOf tab.flip) : ⋯ ▸ s.flip ∈ exitsOf tab

def exitsOf_flip {a✝ : History} {fst✝ fst✝¹ : List Formula} {val✝ : NegLoadFormula ⊕ NegLoadFormula} {tab : Tableau a✝ (fst✝, fst✝¹, some val✝)} (exitIPs : (e : PathIn tab) → e ∈ exitsOf tab → PartInterpolant (nodeAt e)) (e : PathIn tab.flip) : e ∈ exitsOf tab.flip → PartInterpolant (nodeAt e)

Equations

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

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 clusterInterpolation {Hist : History} {L R : List Formula} {snlf : NegLoadFormula ⊕ NegLoadFormula} (tab : Tableau Hist (L, R, some snlf)) (exitIPs : (e : PathIn tab) → e ∈ exitsOf tab → PartInterpolant (nodeAt e)) : PartInterpolant (L, R, some snlf)

Given a tableau where the root is loaded, and exit interpolants, interpolate the root.

Equations

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

theorem tabToIntAt {X : Sequent} (tab : Tableau [] X) (s : PathIn tab) : ∃ (θ : Formula), isPartInterpolant (nodeAt s) θ

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

theorem tabToInt {X : Sequent} (tab : Tableau [] X) : ∃ (θ : Formula), isPartInterpolant X θ