Defining interpolants (Section 9)

Note that we can skip much of Subsection 8.2 because we worked already with split tableaux anyway.

NOTE: We may need extra work for uniformity though.

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 8.14 (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 8.14 (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 9.8. 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)

Starting at root, return the list of earliest free (i.e. unloaded nodes). These are the "exits" from a loaded cluster. A repeat has no exit (because to ensure termination we do not rewind here.) Free nodes are their own (only) exit.

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

Helper lemmas for mem_existsOf_of_flip (dependent-type / HEq plumbing)

theorem PathIn_nil_heq {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} (hH : H1 = H2) (hX : X1 = X2) (h : t1 ≍ t2) : PathIn.nil ≍ PathIn.nil

PathIn.nil over heterogeneously-equal tableaux are heterogeneously equal.

theorem mem_existsOf_of_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} (s : PathIn tab.flip) (s_in : s ∈ exitsOf tab.flip) : ⋯ ▸ s.flip ∈ exitsOf tab

This lemma about PathIn.flip is here because it is also about exitsOf.

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.

Cluster Interpolation

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 θ