Quasi-Tableaux (Def 9.8)

inductive PDL.Typ : Type

The three node types used in constructing a pre-interpolant.

• one : Typ
• two : Typ
• three : Typ

@[instance_reducible]

instance PDL.instDecidableEqTyp : DecidableEq Typ

Equations

• PDL.instDecidableEqTyp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive PDL.QuasiTab : Type

Simple tree data type for Q in Def. 7.31.

• QNode (k : Typ) (Δ : Sequent) (next : List QuasiTab) : QuasiTab

def PDL.QuasiTab.typ : QuasiTab → Typ

The type k(x) of the root of a quasi-tableau.

Equations

• (PDL.QuasiTab.QNode k Δ next).typ = k

def PDL.QuasiTab.label : QuasiTab → Sequent

The label Δₓ of the root of a quasi-tableau.

Equations

• (PDL.QuasiTab.QNode k Δ next).label = Δ

def PDL.QuasiTab.children : QuasiTab → List QuasiTab

The children ⋖Q of the root of a quasi-tableau.

Equations

• (PDL.QuasiTab.QNode k Δ next).children = next

@[irreducible]

def PDL.QuasiTab.subtrees : QuasiTab → List QuasiTab

All nodes of a quasi-tableau, each given by the subtree rooted at it.

Equations

• (PDL.QuasiTab.QNode k Δ next).subtrees = PDL.QuasiTab.QNode k Δ next :: List.flatMap PDL.QuasiTab.subtrees next

Termination of the construction of Q

The construction of Q terminates because along a branch of Q the label of a node of type 1 is either a repeat or a new element of the finite list Λ₂[C], and in the latter case it is added to the history. Hence the number of elements of Λ₂[C] that are not yet in the history decreases.

theorem PDL.countP_lt_countP_of_mem {α : Type u_1} {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p x = true → q x = true) {a : α} (ha : a ∈ l) (hq : q a = true) (hp : ¬p a = true) : List.countP p l < List.countP q l

theorem PDL.length_filter_notMem_cons_lt {α : Type u_1} [DecidableEq α] {l Hist : List α} {a : α} (ha : a ∈ l) (ha' : a ∉ Hist) : (List.filter (fun (z : α) => decide (z ∉ a :: Hist)) l).length < (List.filter (fun (z : α) => decide (z ∉ Hist)) l).length

@[irreducible]

def PDL.QuasiTab.build (inC : Finset Sequent) (step : Sequent → List Sequent) (Hist : List Sequent) (Δ : Sequent) : QuasiTab

Def 9.8: the quasi-tableau, given the list inC of labels Λ₂[C] and the function step that maps a label to the labels of the children obtained by applying the right rule. Both are provided by LoadedCluster.lambdaTwo and LoadedCluster.stepOf in LoadedCluster.Q below.

Following the paper we make the case distinction at the node of type 1: it is a leaf iff it is a repeat (i.e. Δ ∈ Hist) or Δ ∉ Λ₂[C], and in the latter case Δ ∈ Λ₂[C⁺] \ Λ₂[C] by the invariant. Otherwise it has a unique child of type 2, which has a unique child of type 3, whose children are given by step and are again of type 1. Note that only nodes of type 1 add their label to the history — this is the "identify repeats at the first opportunity" from Definition 9.11.

Equations

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

theorem PDL.QuasiTab.build_of_leaf {inC : Finset Sequent} {step : Sequent → List Sequent} {Hist : List Sequent} {Δ : Sequent} (h : ¬(Δ ∈ inC ∧ Δ ∉ Hist)) : build inC step Hist Δ = QNode Typ.one Δ []

A node of Q of type 1 that is a repeat or an exit is a leaf.

theorem PDL.QuasiTab.build_of_node {inC : Finset Sequent} {step : Sequent → List Sequent} {Hist : List Sequent} {Δ : Sequent} (h : Δ ∈ inC ∧ Δ ∉ Hist) : build inC step Hist Δ = QNode Typ.one Δ [QNode Typ.two Δ [QNode Typ.three Δ (List.map (fun (Pi : Sequent) => build inC step (Δ :: Hist) Pi) (step Δ))]]

A node of Q of type 1 that is neither a repeat nor an exit has a child of type 2, which has a child of type 3, whose children are given by step.

theorem PDL.QuasiTab.build_leaf_typ {inC : Finset Sequent} {step : Sequent → List Sequent} (hstep : ∀ Δ ∈ inC, step Δ ≠ []) (Hist : List Sequent) (Δ : Sequent) (q : QuasiTab) : q ∈ (build inC step Hist Δ).subtrees → q.children = [] → q.typ = Typ.one

Remark 9.9: all leaves of the quasi-tableau have type 1. Here we need that a node of type 3 does have children, which by Lemma 9.7 (d), (e) and (f) holds for all Δ ∈ Λ₂[C].

theorem PDL.QuasiTab.build_label_mem {inC lam : Finset Sequent} {step : Sequent → List Sequent} (hstep : ∀ (Δ Pi : Sequent), Pi ∈ step Δ → Pi ∈ lam) (Hist : List Sequent) (Δ : Sequent) : Δ ∈ lam → ∀ q ∈ (build inC step Hist Δ).subtrees, q.label ∈ lam

Invariant of Def 9.8: if all labels produced by step are in lam, then all nodes of the quasi-tableau built from a label in lam are again labelled with elements of lam.

theorem PDL.QuasiTab.build_inner_label_mem {inC : Finset Sequent} {step : Sequent → List Sequent} (Hist : List Sequent) (Δ : Sequent) (q : QuasiTab) : q ∈ (build inC step Hist Δ).subtrees → q.children ≠ [] → q.label ∈ inC

The invariant of Def 9.8: every node of the quasi-tableau that is not a leaf has a label in Λ₂[C], i.e. C_{Δₓ} ≠ ∅ by LoadedCluster.mem_lambdaTwo_iff.

theorem PDL.LoadedCluster.root_rightOnly_mem_lambdaTwo {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : (nodeAt C.root).rightOnly ∈ C.lambdaTwo

The right component of the root of the cluster is in Λ₂[C].

noncomputable def PDL.LoadedCluster.Q {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : QuasiTab

Def 9.8: the quasi-tableau associated with the cluster C. Its root has type 1 and is labelled with the right component Λ₂(r) of the root r of the cluster.

Equations

• C.Q = PDL.QuasiTab.build C.lambdaTwo (Finset.pdlSeqSort ∘ C.stepOf) [] (PDL.nodeAt C.root).rightOnly

@[simp]

theorem PDL.LoadedCluster.Q_typ {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : C.Q.typ = Typ.one

@[simp]

theorem PDL.LoadedCluster.Q_label {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : C.Q.label = (nodeAt C.root).rightOnly

theorem PDL.LoadedCluster.Q_label_mem_lambdaTwoPlus {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (q : QuasiTab) : q ∈ C.Q.subtrees → q.label ∈ C.lambdaTwoPlus

All nodes of Q are labelled with elements of Λ₂[C⁺].

theorem PDL.LoadedCluster.Q_inner_label_mem_lambdaTwo {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (q : QuasiTab) : q ∈ C.Q.subtrees → q.children ≠ [] → q.label ∈ C.lambdaTwo

The invariant of Def 9.8 for Q: every inner node of Q has a label in Λ₂[C].

theorem PDL.LoadedCluster.Q_leaf_typ {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (h97d : ∀ Δ ∈ C.lambdaTwo, C.nodesWithFineRight Δ ≠ []) (q : QuasiTab) : q ∈ C.Q.subtrees → q.children = [] → q.typ = Typ.one

Remark 9.9 for Q: all leaves of the quasi-tableau have type 1. Here h97d is Lemma 9.7 (d), which we state as a hypothesis: for every label in Λ₂[C] there is a node of the cluster with that right component where a right rule is applied.

noncomputable def PDL.LoadedCluster.region {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Typ → Sequent → Finset (FinePathIn tab)

Def 9.10: the region Rₓ ⊆ C⁺ represented by a node x of the quasi-tableau. For type 1 and 2 these are all nodes of C⁺ with right component Δₓ, and for type 3 those nodes of C with right component Δₓ where a right rule is applied.

Equations

• C.region PDL.Typ.one x✝ = C.plusNodesWithFine x✝
• C.region PDL.Typ.two x✝ = C.plusNodesWithFine x✝
• C.region PDL.Typ.three x✝ = (C.nodesWithFineRight x✝).toFinset

noncomputable def PDL.LoadedCluster.regionOf {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (q : QuasiTab) : Finset (FinePathIn tab)

Def 9.10, applied to a node of the quasi-tableau.

Equations

• C.regionOf q = C.region q.typ q.label

Addresses: the nodes of a quasi-tableau (Def 9.11)

QuasiTab is an inductive tree, so its nodes are not determined by their type and label: several nodes of Q may carry the same type and the same label. To speak about the nodes of Q, and in particular about the tree order <_Q needed for repeats and companions, we identify a node with its address, i.e. with the list of child indices that leads to it from the root. Hence r_Q is the empty address, x ≤_Q y becomes "x is a prefix of y" and x <_Q y becomes "x is a proper prefix of y".

def PDL.QuasiTab.atOpt : QuasiTab → List ℕ → Option QuasiTab

The subtree of q rooted at the node with address x, if there is such a node.

Equations

• x✝.atOpt [] = some x✝
• x✝.atOpt (i :: rest) = match x✝.children[i]? with | none => none | some c => c.atOpt rest

def PDL.QuasiTab.isNodeAt (q : QuasiTab) (x : List ℕ) : Bool

Is there a node at address x in q?

Equations

• q.isNodeAt x = (q.atOpt x).isSome

@[irreducible]

def PDL.QuasiTab.addresses : QuasiTab → List (List ℕ)

The set Q of all nodes, given by their addresses.

Equations

• (PDL.QuasiTab.QNode k Δ next).addresses = [] :: List.flatMap (fun (p : List (List ℕ) × ℕ) => List.map (fun (a : List ℕ) => p.2 :: a) p.1) (List.map PDL.QuasiTab.addresses next).zipIdx

def PDL.QuasiTab.labelAt (q : QuasiTab) (x : List ℕ) : Option Sequent

The label Δₓ of the node at address x.

Equations

• q.labelAt x = Option.map PDL.QuasiTab.label (q.atOpt x)

def PDL.QuasiTab.typAt (q : QuasiTab) (x : List ℕ) : Option Typ

The type k(x) of the node at address x.

Equations

• q.typAt x = Option.map PDL.QuasiTab.typ (q.atOpt x)

def PDL.QuasiTab.childrenAt (q : QuasiTab) (x : List ℕ) : List (List ℕ)

The addresses of the children of the node at address x.

Equations

• q.childrenAt x = match q.atOpt x with | none => [] | some n => List.map (fun (i : ℕ) => x ++ [i]) (List.range n.children.length)

def PDL.QuasiTab.isLeafAt (q : QuasiTab) (x : List ℕ) : Bool

Is the node at address x a leaf? (Also false when there is no node at x.)

Equations

• q.isLeafAt x = match q.atOpt x with | none => false | some n => n.children.isEmpty

def PDL.QuasiTab.leaves (q : QuasiTab) : List (List ℕ)

L_Q, the set of leaves.

Equations

• q.leaves = List.filter q.isLeafAt q.addresses

def PDL.QuasiTab.rootAddress : List ℕ

r_Q, the root.

Equations

• PDL.QuasiTab.rootAddress = []

def PDL.QuasiTab.qle (x y : List ℕ) : Prop

x ≤_Q y, the reflexive-transitive closure of ⋖Q, which on addresses is the prefix order.

Equations

• PDL.QuasiTab.qle x y = (x <+: y)

def PDL.QuasiTab.qlt (x y : List ℕ) : Prop

x <_Q y, the transitive closure of ⋖Q, which on addresses is the proper prefix order.

Equations

• PDL.QuasiTab.qlt x y = (x <+: y ∧ x ≠ y)

def PDL.QuasiTab.qedge (q : QuasiTab) (x y : List ℕ) : Prop

x ⋖Q y, i.e. y is a child of x.

Equations

• q.qedge x y = (y ∈ q.childrenAt x)

def PDL.QuasiTab.companionOpt (q : QuasiTab) (x : List ℕ) : Option (List ℕ)

Def 9.11: the companion c(x) of a repeat leaf x, that is, the node z <_Q x of type 1 with the same label as x. Because repeats are identified at the first opportunity there is at most one such node in a quasi-tableau; here we simply take the one closest to the root.

Equations

• q.companionOpt x = List.find? (fun (z : List ℕ) => decide (q.labelAt z = q.labelAt x ∧ q.typAt z = some PDL.Typ.one)) x.inits.dropLast

def PDL.QuasiTab.isRepeatLeaf (q : QuasiTab) (x : List ℕ) : Bool

Def 9.8: x is a repeat leaf of q, i.e. a leaf of type 1 that has a companion.

Equations

• q.isRepeatLeaf x = (q.isLeafAt x && decide (q.typAt x = some PDL.Typ.one) && (q.companionOpt x).isSome)

def PDL.QuasiTab.repeatLeaves (q : QuasiTab) : List (List ℕ)

All repeat leaves of q.

Equations

• q.repeatLeaves = List.filter q.isRepeatLeaf q.leaves

def PDL.QuasiTab.companions (q : QuasiTab) : List (List ℕ)

Def 9.11: K_Q, the set of companions.

Equations

• q.companions = (List.filterMap q.companionOpt q.repeatLeaves).dedup

def PDL.QuasiTab.cycs (q : QuasiTab) (x : List ℕ) : List (List ℕ)

Def 9.11: cycs(x), the set of repeat leaves z with c(z) <_Q x ≤_Q z, i.e. the repeat leaves below x whose companion is a proper ancestor of x.

Equations

• q.cycs x = List.filter (fun (z : List ℕ) => match q.companionOpt z with | none => false | some c => c.isPrefixOf x && !c == x && x.isPrefixOf z) q.repeatLeaves

theorem PDL.QuasiTab.mem_cycs_iff (q : QuasiTab) (x z : List ℕ) : z ∈ q.cycs x ↔ z ∈ q.repeatLeaves ∧ ∃ (c : List ℕ), q.companionOpt z = some c ∧ qlt c x ∧ qle x z

Basic facts about addresses

These general facts about atOpt, addresses, subtrees and childrenAt are used both here and in the files building on this one.

theorem PDL.QuasiTab.atOpt_cons_none {q : QuasiTab} {i : ℕ} {rest : List ℕ} (h : q.children[i]? = none) : q.atOpt (i :: rest) = none

theorem PDL.QuasiTab.atOpt_append (q : QuasiTab) (x w : List ℕ) : q.atOpt (x ++ w) = (q.atOpt x).bind fun (n : QuasiTab) => n.atOpt w

theorem PDL.QuasiTab.isSome_atOpt_of_isLeafAt {q : QuasiTab} {x : List ℕ} (h : q.isLeafAt x = true) : (q.atOpt x).isSome = true

theorem PDL.QuasiTab.mem_addresses_of_atOpt (q : QuasiTab) (x : List ℕ) (h : (q.atOpt x).isSome = true) : x ∈ q.addresses

Every address of a node of q is in q.addresses.

theorem PDL.QuasiTab.mem_subtrees_of_atOpt {q n : QuasiTab} {x : List ℕ} (h : q.atOpt x = some n) : n ∈ q.subtrees

The node at an address is one of the subtrees.

theorem PDL.QuasiTab.childrenAt_of_atOpt {q n : QuasiTab} {x : List ℕ} (hx : q.atOpt x = some n) : q.childrenAt x = List.map (fun (i : ℕ) => x ++ [i]) (List.range n.children.length)

theorem PDL.QuasiTab.childrenAt_eq_singleton_iff (q : QuasiTab) {x y : List ℕ} : q.childrenAt x = [y] ↔ ∃ (n : QuasiTab), q.atOpt x = some n ∧ n.children.length = 1 ∧ y = x ++ [0]

Lemma 9.12

theorem PDL.QuasiTab.typAt_of_isRepeatLeaf (q : QuasiTab) {x : List ℕ} (h : q.isRepeatLeaf x = true) : q.typAt x = some Typ.one

Lemma 9.12 (a), first half: a repeat leaf has type 1.

theorem PDL.QuasiTab.typAt_of_mem_companions (q : QuasiTab) {x : List ℕ} (h : x ∈ q.companions) : q.typAt x = some Typ.one

Lemma 9.12 (a), second half: a companion node has type 1.

theorem PDL.QuasiTab.cycs_root (q : QuasiTab) : q.cycs rootAddress = []

Lemma 9.12 (b): the root has no cycles below it, cycs(r_Q) = ∅.

theorem PDL.QuasiTab.mem_cycs_of_mem_cycs_of_qlt (q : QuasiTab) {x y z : List ℕ} (hxy : qlt x y) (hz : z ∈ q.cycs x) (hyz : qle y z) : z ∈ q.cycs y

Lemma 9.12 (c) does not hold as stated in the paper: from x <_Q y we cannot conclude cycs(x) ⊆ cycs(y), because a repeat leaf z ∈ cycs(x) may lie below a different child of x than y does. (For counterexamples, and for a precise account of when (c) does hold, see the file Pdl.ClusterCorrection.) What does hold — and what the proofs in the paper actually use — is the following version, where we additionally demand y ≤_Q z.

theorem PDL.QuasiTab.cycs_subset_of_qedge (q : QuasiTab) {x y : List ℕ} (hx : x ∉ q.companions) (hxy : q.qedge x y) (z : List ℕ) : z ∈ q.cycs y → z ∈ q.cycs x

Lemma 9.12 (d) does not hold as stated in the paper either: when x has several children then the inclusion cycs(y) ⊆ cycs(x) may be strict. (For counterexamples, and for a precise account of when equality does hold — namely whenever x has at most one child, hence at all nodes of a quasi-tableau of a cluster that are not of type 3 — see the file Pdl.ClusterCorrection.) Here is the inclusion that does hold in general, and it is the direction that the proofs in the paper actually use.