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} {X : Sequent} (tab : Tableau Hist X) : List (PathIn tab)

Helper for exitsOf. Or replace it fully with this?

Equations

• One or more equations did not get rendered due to their size.
• exitsOf (Tableau.lrep lpr) = if X.isLoaded = true then [] else [PathIn.nil]
• exitsOf (Tableau.pdl nrep bas r next) = if X.isLoaded = true then List.map PathIn.pdl (exitsOf next) else [PathIn.nil]

theorem loaded_iff_exitsOf_non_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} : X.isLoaded = true ↔ ∀ q ∈ exitsOf tab, q ≠ PathIn.nil

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

Equations

• PathIn.children = sorry

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. This may need additional hypotheses to say that we start at the root of the cluster.

Equations

• clusterInterpolation_right tab exitIPs = sorry

theorem PathIn.loc_flip {L R : List Formula} {nlf : NegLoadFormula} {Hist : List Sequent} {nrep' : ¬rep Hist (L, R, some (Sum.inl nlf))} {nbas' : ¬Sequent.basic (L, R, some (Sum.inl nlf))} (nrep : ¬rep (List.map Sequent.flip Hist) (Sequent.flip (L, R, some (Sum.inl nlf)))) (nbas : ¬(Sequent.flip (L, R, some (Sum.inl nlf))).basic) (lt : LocalTableau (L, R, some (Sum.inl nlf))) (next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau ((L, R, some (Sum.inl nlf)) :: Hist) Y) (next' : (Yf : Sequent) → Yf ∈ endNodesOf lt.flip → Tableau (List.map Sequent.flip ((L, R, some (Sum.inl nlf)) :: Hist)) Yf) (Y : Sequent) (Y_in : Y ∈ endNodesOf lt) (p : PathIn (next Y Y_in)) (Yf_in : Y.flip ∈ endNodesOf lt.flip) (h_next : (next Y Y_in).flip = next' Y.flip Yf_in) (h : Tableau.loc nrep nbas lt.flip next' = (Tableau.loc nrep' nbas' lt next).flip) : (loc Y_in nil).flip = h ▸ loc Yf_in nil

TODO messy helper for mem_existsOf_of_flip

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

@[irreducible]

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

def exitsOf_flip {Hist : History} {L R : List Formula} {nlf : NegLoadFormula ⊕ NegLoadFormula} {tab : Tableau Hist (L, R, some nlf)} (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.strong_upwards_inductionOn only works with Prop motive.

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