Interpolants for Partitions (big part of Section 7)

def Olf.toForms : Olf → List Formula

Equations

• Olf.toForms none = []
• Olf.toForms (some (Sum.inl (~'lf))) = [~lf.unload]
• Olf.toForms (some (Sum.inr (~'lf))) = [~lf.unload]

def Sequent.left (X : Sequent) : List Formula

Equations

• X.left = X.L ++ X.O.toForms

def Sequent.right (X : Sequent) : List Formula

Equations

• X.right = X.R ++ X.O.toForms

def jvoc (X : Sequent) : Vocab

Joint vocabulary of all parts of a Sequent.

Equations

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

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)

theorem unfoldBox_voc {x : ℕ ⊕ ℕ} {α : Program} {φ : Formula} {L : List Formula} (L_in : L ∈ unfoldBox α φ) {ψ : Formula} (ψ_in : ψ ∈ L) (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc

theorem unfoldDiamond_voc {x : ℕ ⊕ ℕ} {α : Program} {φ : Formula} {L : List Formula} (L_in : L ∈ unfoldDiamond α φ) {ψ : Formula} (ψ_in : ψ ∈ L) (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc

theorem localRule_does_not_increase_vocab_L {Lcond Rcond : List Formula} {Ocond : Olf} {ress : List Sequent} (rule : LocalRule (Lcond, Rcond, Ocond) ress) (res : Sequent) : res ∈ ress → res.1.fvoc ⊆ Lcond.fvoc

theorem localRule_does_not_increase_vocab_R {Lcond Rcond : List Formula} {Ocond : Olf} {ress : List Sequent} (rule : LocalRule (Lcond, Rcond, Ocond) ress) (res : Sequent) : res ∈ ress → res.2.1.fvoc ⊆ Rcond.fvoc

theorem localRule_does_not_increase_vocab_O {Lcond Rcond : List Formula} {Ocond : Olf} {ress : List Sequent} (rule : LocalRule (Lcond, Rcond, Ocond) ress) (res : Sequent) : res ∈ ress → res.2.2.voc ⊆ Ocond.voc

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 {C : List Sequent} (L R : List Formula) (o : Olf) (ruleA : LocalRuleApp (L, R, o) C) (subθs : (c : Sequent) → c ∈ C → PartInterpolant c) : PartInterpolant (L, R, o)

Maehara's method for local rule applications. This is itpLeaves for singleton clusters in the notes, but not only.

Equations

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

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.rep lpr) = []
• exitsOf (Tableau.loc lt next) = sorry
• exitsOf (Tableau.pdl 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