Generating all Local Tableaux

We show that for any X the type LocalTableau is finite.

This is needed to define BuildTree as a finite tree.

Helpers about Finset.pdlSort

theorem PDL.Finset.pdlSort_toFinset (X : Finset Formula) : X.pdlSort.toFinset = X

@[simp]

theorem PDL.Finset.pdlSort_singleton (a : Formula) : {a}.pdlSort = [a]

theorem PDL.Finset.length_pdlSort (X : Finset Formula) : X.pdlSort.length = X.card

theorem PDL.Finset.pdlSort_nodup (X : Finset Formula) : X.pdlSort.Nodup

theorem PDL.pdlSort_eq_singleton {X : Finset Formula} {a : Formula} (h : X.pdlSort = [a]) : X = {a}

theorem PDL.pdlSort_eq_pair {X : Finset Formula} {a b : Formula} (h : X.pdlSort = [a, b]) : X = {a, b}

theorem PDL.sublist_pdlSort_toFinset_subset {L : Finset Formula} {l : List Formula} (h : l.Sublist L.pdlSort) : l.toFinset ⊆ L

A sublist of the sorted version of L gives a subset of L.

theorem PDL.exists_sublist_pdlSort_of_subset {L Lcond : Finset Formula} (h : Lcond ⊆ L) : ∃ l ∈ L.pdlSort.sublists, l.toFinset = Lcond

Any subset of L arises from a sublist of the sorted version of L.

theorem PDL.Olf.subset_self (o : Olf) : o ⊆ o

theorem PDL.Olf.none_subset (o : Olf) : none ⊆ o

theorem PDL.Formula.ne_neg (φ : Formula) : φ ≠ φ.neg

theorem PDL.Formula.ne_neg_neg (φ : Formula) : φ ≠ φ.neg.neg

theorem PDL.pair_neg_cases {φ a b : Formula} (h : {φ, φ.neg} = {a, b}) (hab : a ≠ b) : a = φ ∧ b = φ.neg ∨ a = φ.neg ∧ b = φ

If {φ, ~φ} = {a, b} with a ≠ b then the pair is one of the two obvious ones.

All one-sided local rules

def PDL.osrCast {L L' : Finset Formula} {B : Finset (Finset Formula)} (h : L = L') (r : OneSidedLocalRule L' B) : OneSidedLocalRule L B

Transport a OneSidedLocalRule along an equality of preconditions.

Equations

• PDL.osrCast h r = ⋯.mpr r

@[simp]

theorem PDL.osrCast_self {L : Finset Formula} {B : Finset (Finset Formula)} (h : L = L) (r : OneSidedLocalRule L B) : osrCast h r = r

def PDL.OneSidedLocalRule.ofSorted (L : Finset Formula) (l : List Formula) : L.pdlSort = l → Option ((B : Finset (Finset Formula)) × OneSidedLocalRule L B)

Given the sorted list of the formulas in L, is there a OneSidedLocalRule for L? The pair case comes first so that the equations below hold by rfl.

Equations

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

theorem PDL.OneSidedLocalRule.ofSorted_pair {L : Finset Formula} {a b : Formula} (h : L.pdlSort = [a, b]) : ofSorted L [a, b] h = if hb : b = a.neg then some ⟨∅, osrCast ⋯ (not a)⟩ else if ha : a = b.neg then some ⟨∅, osrCast ⋯ (not b)⟩ else none

theorem PDL.OneSidedLocalRule.ofSorted_bot {L : Finset Formula} (h : L.pdlSort = [⊥]) : ofSorted L [⊥] h = some ⟨∅, osrCast ⋯ bot⟩

theorem PDL.OneSidedLocalRule.ofSorted_neg {L : Finset Formula} {φ : Formula} (h : L.pdlSort = [φ.neg.neg]) : ofSorted L [φ.neg.neg] h = some ⟨{{φ}}, osrCast ⋯ (neg φ)⟩

theorem PDL.OneSidedLocalRule.ofSorted_con {L : Finset Formula} {φ ψ : Formula} (h : L.pdlSort = [φ.and ψ]) : ofSorted L [φ.and ψ] h = some ⟨{{φ, ψ}}, osrCast ⋯ (con φ ψ)⟩

theorem PDL.OneSidedLocalRule.ofSorted_nCo {L : Finset Formula} {φ ψ : Formula} (h : L.pdlSort = [(φ.and ψ).neg]) : ofSorted L [(φ.and ψ).neg] h = some ⟨{{φ.neg}, {ψ.neg}}, osrCast ⋯ (nCo φ ψ)⟩

theorem PDL.OneSidedLocalRule.ofSorted_box {L : Finset Formula} {α : Program} {φ : Formula} (h : L.pdlSort = [Formula.box α φ]) : ofSorted L [Formula.box α φ] h = if notAtm : ¬α.isAtomic then some ⟨(unfoldBox α φ).pdlToFinFin, osrCast ⋯ (box α φ notAtm)⟩ else none

theorem PDL.OneSidedLocalRule.ofSorted_dia {L : Finset Formula} {α : Program} {φ : Formula} (h : L.pdlSort = [(Formula.box α φ).neg]) : ofSorted L [(Formula.box α φ).neg] h = if notAtm : ¬α.isAtomic then some ⟨(unfoldDiamond α φ).pdlToFinFin, osrCast ⋯ (dia α φ notAtm)⟩ else none

def PDL.OneSidedLocalRule.all (L : Finset Formula) : Option ((B : Finset (Finset Formula)) × OneSidedLocalRule L B)

Is there a OneSidedLocalRule applicable to L?

Equations

• PDL.OneSidedLocalRule.all L = PDL.OneSidedLocalRule.ofSorted L L.pdlSort ⋯

theorem PDL.OneSidedLocalRule.all_eq_ofSorted {L : Finset Formula} {l : List Formula} (h : L.pdlSort = l) : all L = ofSorted L l h

theorem PDL.OneSidedLocalRule.all_spec {L : Finset Formula} {B : Finset (Finset Formula)} (osr : OneSidedLocalRule L B) : all L = some ⟨B, osr⟩

@[instance_reducible]

instance PDL.OneSidedLocalRule.fintype {L : Finset Formula} {B : Finset (Finset Formula)} : Fintype (OneSidedLocalRule L B)

Equations

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

All load rules

def PDL.LoadRule.the (nχ : NegLoadFormula) : Option ((ress : Finset (Finset Formula × Option NegLoadFormula)) × LoadRule nχ ress)

Given a negated loaded formula, is there a LoadRule applicable to it?

Equations

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

theorem PDL.LoadRule.the_spec {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lor : LoadRule (NegLoadFormula.neg χ) ress) : some ⟨ress, lor⟩ = the (NegLoadFormula.neg χ)

@[instance_reducible]

instance PDL.LoadRule.fintype {nχ : NegLoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} : Fintype (LoadRule nχ ress)

Equations

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

All local rules

def PDL.lrCast {c c' : Sequent} {ress : Finset Sequent} (h : c = c') (r : LocalRule c' ress) : LocalRule c ress

Transport a LocalRule along an equality of the conditions.

Equations

• PDL.lrCast h r = ⋯.mpr r

@[simp]

theorem PDL.lrCast_self {c : Sequent} {ress : Finset Sequent} (h : c = c) (r : LocalRule c ress) : lrCast h r = r

def PDL.LocalRule.negPairOf (L R : Finset Formula) (lL lR : List Formula) : L.pdlSort = lL → R.pdlSort = lR → Option ((ress : Finset Sequent) × LocalRule (L, R, none) ress)

Helper for LocalRule.all, dealing with the two closing rules LRnegL and LRnegR.

Equations

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

theorem PDL.LocalRule.negPairOf_singletons {L R : Finset Formula} {φ1 φ2 : Formula} (hL : L.pdlSort = [φ1]) (hR : R.pdlSort = [φ2]) : negPairOf L R [φ1] [φ2] hL hR = if h : φ2 = φ1.neg then some ⟨∅, lrCast ⋯ (LRnegL φ1)⟩ else if h : φ1 = φ2.neg then some ⟨∅, lrCast ⋯ (LRnegR φ2)⟩ else none

def PDL.LocalRule.all (cond : Sequent) : Option ((ress : Finset Sequent) × LocalRule cond ress)

Given a subsequent cond to be replaced, is there an applicable local rule? Note that cond are only the principal formulas, not the whole sequent.

Equations

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

theorem PDL.LocalRule.all_none (L R : Finset Formula) : all (L, R, none) = if hR : R = ∅ then Option.map (fun (x : (B : Finset (Finset Formula)) × OneSidedLocalRule L B) => match x with | ⟨fst, orule⟩ => ⟨Finset.image (fun (res : Finset Formula) => (res, ∅, none)) fst, lrCast ⋯ (oneSidedL orule ⋯)⟩) (OneSidedLocalRule.all L) else if hL : L = ∅ then Option.map (fun (x : (B : Finset (Finset Formula)) × OneSidedLocalRule R B) => match x with | ⟨fst, orule⟩ => ⟨Finset.image (fun (res : Finset Formula) => (∅, res, none)) fst, lrCast ⋯ (oneSidedR orule ⋯)⟩) (OneSidedLocalRule.all R) else negPairOf L R L.pdlSort R.pdlSort ⋯ ⋯

theorem PDL.LocalRule.all_inl_loaded (L R : Finset Formula) (α : Program) (χ : LoadFormula) : all (L, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.box α (AnyFormula.loaded χ))))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) (unfoldDiamondLoaded α χ).pdlToFinFinOpt, lrCast ⋯ (loadedL (LoadFormula.box α (AnyFormula.loaded χ)) (LoadRule.dia notAtm) ⋯)⟩ else none else none else none

theorem PDL.LocalRule.all_inl_normal (L R : Finset Formula) (α : Program) (φ : Formula) : all (L, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.box α (AnyFormula.normal φ))))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) (unfoldDiamondLoaded' α φ).pdlToFinFinOpt, lrCast ⋯ (loadedL (LoadFormula.box α (AnyFormula.normal φ)) (LoadRule.dia' notAtm) ⋯)⟩ else none else none else none

theorem PDL.LocalRule.all_inr_loaded (L R : Finset Formula) (α : Program) (χ : LoadFormula) : all (L, R, some (Sum.inr (NegLoadFormula.neg (LoadFormula.box α (AnyFormula.loaded χ))))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) (unfoldDiamondLoaded α χ).pdlToFinFinOpt, lrCast ⋯ (loadedR (LoadFormula.box α (AnyFormula.loaded χ)) (LoadRule.dia notAtm) ⋯)⟩ else none else none else none

theorem PDL.LocalRule.all_inr_normal (L R : Finset Formula) (α : Program) (φ : Formula) : all (L, R, some (Sum.inr (NegLoadFormula.neg (LoadFormula.box α (AnyFormula.normal φ))))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) (unfoldDiamondLoaded' α φ).pdlToFinFinOpt, lrCast ⋯ (loadedR (LoadFormula.box α (AnyFormula.normal φ)) (LoadRule.dia' notAtm) ⋯)⟩ else none else none else none

theorem PDL.OneSidedLocalRule.precond_ne_empty {P : Finset Formula} {B : Finset (Finset Formula)} (osr : OneSidedLocalRule P B) : P ≠ ∅

theorem PDL.LocalRule.negPairOf_eq {L R : Finset Formula} {lL lR : List Formula} (hL : L.pdlSort = lL) (hR : R.pdlSort = lR) : negPairOf L R L.pdlSort R.pdlSort ⋯ ⋯ = negPairOf L R lL lR hL hR

theorem PDL.LocalRule.all_spec {L : Sequent} {B : Finset Sequent} (lr : LocalRule L B) : ⟨B, lr⟩ ∈ all L

@[instance_reducible]

instance PDL.LocalRule.fintype {X : Sequent} {ress : Finset Sequent} : Fintype (LocalRule X ress)

Equations

• PDL.LocalRule.fintype = match h_the : PDL.LocalRule.all X with | some ⟨ress', lr⟩ => { elems := if h : ress = ress' then {⋯ ▸ lr} else ∅, complete := ⋯ } | none => { elems := ∅, complete := ⋯ }

All local rule applications

def PDL.LocalRuleApp.all (X : Sequent) : List LocalRuleApp

Given a sequent, return a list of all possible local rule applications.

Equations

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

theorem PDL.LocalRuleApp.all_X (X : Sequent) (lra : LocalRuleApp) : lra ∈ all X → lra.X = X

theorem PDL.LocalRuleApp.all_spec (lrA : LocalRuleApp) : lrA ∈ all lrA.X

theorem PDL.LocalRuleApp.all_nonempty_of_nonbasic {X : Sequent} (X_nonbas : ¬X.basic) : all X ≠ []

Termination measure for local tableaux

def PDL.lmOfOlf : Olf → ℕ

The formula-length measure of the optional loading.

Equations

• PDL.lmOfOlf none = 0
• PDL.lmOfOlf (some (Sum.inl nlf)) = PDL.lmOfFormula (PDL.negUnload nlf)
• PDL.lmOfOlf (some (Sum.inr nlf)) = PDL.lmOfFormula (PDL.negUnload nlf)

def PDL.lmOfSequent (X : Sequent) : ℕ

Local measure of a sequent: the sum of lmOfFormula over all three components.

Equations

• PDL.lmOfSequent X = ∑ φ ∈ X.1, PDL.lmOfFormula φ + ∑ φ ∈ X.2.1, PDL.lmOfFormula φ + PDL.lmOfOlf X.2.2

def PDL.lmOfONlf : Option NegLoadFormula → ℕ

Local measure of an optional negated loaded formula.

Equations

• PDL.lmOfONlf none = 0
• PDL.lmOfONlf (some nlf) = PDL.lmOfFormula (PDL.negUnload nlf)

Helpers to show that local rules decrease the measure

theorem PDL.lm_sum_union_le (A B : Finset Formula) : ∑ φ ∈ A ∪ B, lmOfFormula φ ≤ ∑ φ ∈ A, lmOfFormula φ + ∑ φ ∈ B, lmOfFormula φ

The measure sum over a union is at most the sum of the measure sums.

theorem PDL.lm_sum_Dset_le_tests {α : Program} {F : List Formula} {δ : List Program} (in_D : (F, δ) ∈ Dset α) : ∑ ψ ∈ F.toFinset, lmOfFormula ψ ≤ (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula ↑τ) (testsOfProgram α).attach).sum

For (F,δ) ∈ Dset α the measure sum over F is at most the test measure of α.

theorem PDL.lm_dia_eq {α : Program} {φ : Formula} (h : ¬α.isAtomic) : lmOfFormula (Formula.box α φ).neg = 1 + lmOfFormula φ.neg + (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula ↑τ) (testsOfProgram α).attach).sum

Unfolding the measure of a diamond with a non-atomic program.

theorem PDL.OneSidedLocalRule.decreases_lm {precond : Finset Formula} {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule precond ress) (res : Finset Formula) : res ∈ ress → ∑ φ ∈ res, lmOfFormula φ < ∑ φ ∈ precond, lmOfFormula φ

One-sided local rules strictly decrease the measure sum.

theorem PDL.LoadRule.decreases_lm {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lrule : LoadRule (NegLoadFormula.neg χ) ress) (Fo : Finset Formula × Option NegLoadFormula) : Fo ∈ ress → ∑ ψ ∈ Fo.1, lmOfFormula ψ + lmOfONlf Fo.2 < lmOfFormula χ.unload.neg

Loaded rules strictly decrease the measure: the new formulas together with the new loaded formula have a smaller measure than the old loaded formula.

theorem PDL.localRuleApp.decreases_lm (lra : LocalRuleApp) (Y : Sequent) (h : Y ∈ lra.C) : lmOfSequent Y < lmOfSequent lra.X

Generating all local tableaux

def PDL.combo {α : Type} [DecidableEq α] {q : α → Type} {L : List α} (f : (x : α) → x ∈ L → List (q x)) : List ((x : α) → x ∈ L → q x)

Convert a function returning lists into a list of functions. Helper for LocalTableau.all.

Equations

• One or more equations did not get rendered due to their size.
• PDL.combo x_2 = [fun (x : α) (x_in : x ∈ []) => ⋯.elim]

theorem PDL.combo_mem_of_forall_in {α : Type} [DecidableEq α] {q : α → Type} {L : List α} (f : (x : α) → x ∈ L → List (q x)) (g : (x : α) → x ∈ L → q x) : (∀ (x : α) (x_in : x ∈ L), g x x_in ∈ f x x_in) → g ∈ combo f

Characterization of members of combo result. Could be strengthened to ↔ later.

def PDL.comboF {q : Sequent → Type} (s : Finset Sequent) (f : (x : Sequent) → x ∈ s → List (q x)) : List ((x : Sequent) → x ∈ s → q x)

Version of combo for Finsets.

Equations

• PDL.comboF s f = List.map (fun (g : (x : PDL.Sequent) → x ∈ s.pdlSeqSort → q x) (x : PDL.Sequent) (hx : x ∈ s) => g x ⋯) (PDL.combo fun (x : PDL.Sequent) (hx : x ∈ s.pdlSeqSort) => f x ⋯)

theorem PDL.comboF_mem_of_forall_in {q : Sequent → Type} {s : Finset Sequent} (f : (x : Sequent) → x ∈ s → List (q x)) (g : (x : Sequent) → x ∈ s → q x) (h : ∀ (x : Sequent) (x_in : x ∈ s), g x x_in ∈ f x x_in) : g ∈ comboF s f

@[irreducible]

def PDL.LocalTableau.all (X : Sequent) : List (LocalTableau X)

Enumerate all local tableaux rooted at a sequent.

Equations

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

theorem PDL.LocalTableau.all_nonempty (X : Sequent) : all X ≠ []

theorem PDL.LocalTableau.all_spec {X : Sequent} {ltX : LocalTableau X} : ltX ∈ all X

@[instance_reducible]

instance PDL.LocalTableau.fintype {X : Sequent} : Fintype (LocalTableau X)

Equations

• PDL.LocalTableau.fintype = { elems := (PDL.LocalTableau.all X).toFinset, complete := ⋯ }

Generating all Open Local Tableaux

def PDL.OpenLocalTableau.all (X : Sequent) : List (OpenLocalTableau X)

Enumerate all local tableaux with at least one end node.

Equations

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

theorem PDL.OpenLocalTableau.all_spec {X : Sequent} {ltX : OpenLocalTableau X} : ltX ∈ all X