Interpolants for Partitions (big part of Section 7)

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

This is 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 {X : Sequent} {C : List Sequent} (ruleA : LocalRuleApp X C) (Y : Sequent) : Y ∈ C → jvoc Y ⊆ jvoc X

def localInterpolantStep (L R : List Formula) (o : Olf) (C : List Sequent) (ruleA : LocalRuleApp (L, R, o) C) (subθs : (c : Sequent) → c ∈ C → PartInterpolant c) : PartInterpolant (L, R, o)

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

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

W.l.o.g version of clusterInterpolation.

Equations

• clusterInterpolation_right tab exitIPs = sorry

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.

def tabToInt {X : Sequent} (tab : Tableau [] X) : PartInterpolant X

Equations

• tabToInt tab = sorry