Interpolants preserved by local tableau rules

Partition Interpolants

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

The vocabulary and two inconsistency conditions defining a partial interpolant.

Equations

• PDL.isPartInterpolant X θ = (θ.voc ⊆ PDL.jvoc X ∧ ¬PDL.HasSat.satisfiable ({θ.neg} ∪ X.left) ∧ ¬PDL.HasSat.satisfiable ({θ} ∪ X.right))

def PDL.PartInterpolant (N : Sequent) : Type

A formula equipped with the partial-interpolant conditions for a sequent.

Equations

• PDL.PartInterpolant N = Subtype (PDL.isPartInterpolant N)

Interpolants for local rules

theorem PDL.LoadRule.voc {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lr : LoadRule (NegLoadFormula.neg χ) ress) : lfovocFin ress ⊆ χ.voc

theorem PDL.localRule_does_not_increase_vocab_L {Cond : Sequent} {B : Finset Sequent} (rule : LocalRule Cond B) (res : Sequent) : res ∈ B → res.left.pdlFvoc ⊆ Cond.left.pdlFvoc

theorem PDL.localRule_does_not_increase_vocab_R {B : Finset Sequent} {Cond : Sequent} (rule : LocalRule Cond B) (res : Sequent) : res ∈ B → res.right.pdlFvoc ⊆ Cond.right.pdlFvoc

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

theorem PDL.localInterpolantStep_oneSidedL (L R : Finset Formula) (o : Olf) (Lcond : Finset Formula) (ress_1 C : Finset Sequent) {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule Lcond ress) (rule : LocalRule (Lcond, ∅, none) ress_1) (hC : C = applyLocalRule rule (L, R, o)) (precondProof : Lcond ⊆ L ∧ ∅ ⊆ R ∧ none ⊆ o) (subθs : (c : Sequent) → c ∈ C → PartInterpolant c) (YS_def : ress_1 = Finset.image (fun (res : Finset Formula) => (res, ∅, none)) ress) (def_rule : rule = LocalRule.oneSidedL orule YS_def) : have interSet := Finset.image (fun (c : ↥C) => ↑(subθs ↑c ⋯)) C.attach; isPartInterpolant { L := L, R := R, O := o, Lcond := Lcond, ress := ress_1, lr := LocalRule.oneSidedL orule YS_def, C := C, hC := hC, preconditionProof := precondProof }.X (dis interSet.pdlSort)

Maehara interpolation for a oneSidedL local rule.

theorem PDL.localInterpolantStep_oneSidedR (L R : Finset Formula) (o : Olf) (Rcond : Finset Formula) (ress_1 C : Finset Sequent) {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule Rcond ress) (rule : LocalRule (∅, Rcond, none) ress_1) (hC : C = applyLocalRule rule (L, R, o)) (precondProof : ∅ ⊆ L ∧ Rcond ⊆ R ∧ none ⊆ o) (subθs : (c : Sequent) → c ∈ C → PartInterpolant c) (YS_def : ress_1 = Finset.image (fun (res : Finset Formula) => (∅, res, none)) ress) (def_rule : rule = LocalRule.oneSidedR orule YS_def) : have interSet := Finset.image (fun (c : ↥C) => ↑(subθs ↑c ⋯)) C.attach; isPartInterpolant { L := L, R := R, O := o, Rcond := Rcond, ress := ress_1, lr := LocalRule.oneSidedR orule YS_def, C := C, hC := hC, preconditionProof := precondProof }.X (con interSet.pdlSort)

Maehara interpolation for a oneSidedR local rule.

theorem PDL.localInterpolantStep_loadedL (L R : Finset Formula) (o : Olf) (ress_1 C : Finset Sequent) {ress : Finset (Finset Formula × Option NegLoadFormula)} (χ : LoadFormula) (lrule : LoadRule (NegLoadFormula.neg χ) ress) (rule : LocalRule (∅, ∅, some (Sum.inl (NegLoadFormula.neg χ))) ress_1) (hC : C = applyLocalRule rule (L, R, o)) (precondProof : ∅ ⊆ L ∧ ∅ ⊆ R ∧ some (Sum.inl (NegLoadFormula.neg χ)) ⊆ o) (subθs : (c : Sequent) → c ∈ C → PartInterpolant c) (YS_def : ress_1 = Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) ress) (def_rule : rule = LocalRule.loadedL χ lrule YS_def) : have interSet := Finset.image (fun (c : ↥C) => ↑(subθs ↑c ⋯)) C.attach; Sequent.O (L, R, o) = some (Sum.inl (NegLoadFormula.neg χ)) → isPartInterpolant { L := L, R := R, O := o, Ocond := some (Sum.inl (NegLoadFormula.neg χ)), ress := ress_1, lr := LocalRule.loadedL χ lrule YS_def, C := C, hC := hC, preconditionProof := precondProof }.X (dis interSet.pdlSort)

Maehara interpolation for a loadedL local rule.

theorem PDL.localInterpolantStep_loadedR (L R : Finset Formula) (o : Olf) (ress_1 C : Finset Sequent) {ress : Finset (Finset Formula × Option NegLoadFormula)} (χ : LoadFormula) (lrule : LoadRule (NegLoadFormula.neg χ) ress) (rule : LocalRule (∅, ∅, some (Sum.inr (NegLoadFormula.neg χ))) ress_1) (hC : C = applyLocalRule rule (L, R, o)) (precondProof : ∅ ⊆ L ∧ ∅ ⊆ R ∧ some (Sum.inr (NegLoadFormula.neg χ)) ⊆ o) (subθs : (c : Sequent) → c ∈ C → PartInterpolant c) (YS_def : ress_1 = Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) ress) (def_rule : rule = LocalRule.loadedR χ lrule YS_def) : have interSet := Finset.image (fun (c : ↥C) => ↑(subθs ↑c ⋯)) C.attach; Sequent.O (L, R, o) = some (Sum.inr (NegLoadFormula.neg χ)) → isPartInterpolant { L := L, R := R, O := o, Ocond := some (Sum.inr (NegLoadFormula.neg χ)), ress := ress_1, lr := LocalRule.loadedR χ lrule YS_def, C := C, hC := hC, preconditionProof := precondProof }.X (con interSet.pdlSort)

Maehara interpolation for a loadedR local rule.

def PDL.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 PDL.LocalTableau.interpolant {X : Sequent} (ltX : LocalTableau X) (endθs : (Y : Sequent) → Y ∈ endNodesOf ltX → PartInterpolant Y) : PartInterpolant X

Propagate interpolants from the end nodes through a local tableau.

Equations

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