Quasi-Tableaux (Def 9.8)

inductive Typ : Type

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

@[instance_reducible]

instance instDecidableEqTyp : DecidableEq Typ

Equations

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

inductive QuasiTab : Type

Simple tree data type for Q in Def. 7.31.

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

def QuasiTab.typ : QuasiTab → Typ

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

Equations

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

def QuasiTab.label : QuasiTab → Sequent

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

Equations

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

def QuasiTab.children : QuasiTab → List QuasiTab

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

Equations

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

@[irreducible]

def QuasiTab.subtrees : QuasiTab → List QuasiTab

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

Equations

• (QuasiTab.QNode k Δ next).subtrees = QuasiTab.QNode k Δ next :: List.flatMap 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 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 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 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 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 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 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 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 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 LoadedCluster.root_rightOnly_mem_lambdaTwo {a✝ : Sequent} {tab : Tableau [] a✝} (C : LoadedCluster tab) : (nodeAt C.root).rightOnly ∈ C.lambdaTwo

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

noncomputable def LoadedCluster.Q {a✝ : Sequent} {tab : Tableau [] a✝} (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 = QuasiTab.build C.lambdaTwo (Finset.seqSort ∘ C.stepOf) [] (nodeAt C.root).rightOnly

@[simp]

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

@[simp]

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

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

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

theorem LoadedCluster.Q_inner_label_mem_lambdaTwo {a✝ : Sequent} {tab : Tableau [] a✝} (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 LoadedCluster.Q_leaf_typ {a✝ : Sequent} {tab : Tableau [] a✝} (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 LoadedCluster.region {a✝ : Sequent} {tab : Tableau [] a✝} (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 Typ.one x✝ = C.plusNodesWithFine x✝
• C.region Typ.two x✝ = C.plusNodesWithFine x✝
• C.region Typ.three x✝ = (C.nodesWithFineRight x✝).toFinset

noncomputable def LoadedCluster.regionOf {a✝ : Sequent} {tab : Tableau [] a✝} (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 QuasiTab.at? : QuasiTab → List ℕ → Option QuasiTab

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

Equations

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

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

Is there a node at address x in q?

Equations

• q.isNodeAt x = (q.at? x).isSome

@[irreducible]

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

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

Equations

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

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

The label Δₓ of the node at address x.

Equations

• q.labelAt x = Option.map QuasiTab.label (q.at? x)

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

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

Equations

• q.typAt x = Option.map QuasiTab.typ (q.at? x)

def 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.at? x with | none => [] | some n => List.map (fun (i : ℕ) => x ++ [i]) (List.range n.children.length)

def 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.at? x with | none => false | some n => n.children.isEmpty

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

L_Q, the set of leaves.

Equations

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

def QuasiTab.rootAddress : List ℕ

r_Q, the root.

Equations

• QuasiTab.rootAddress = []

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

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

Equations

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

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

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

Equations

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

def 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 QuasiTab.companion? (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.companion? x = List.find? (fun (z : List ℕ) => decide (q.labelAt z = q.labelAt x ∧ q.typAt z = some Typ.one)) x.inits.dropLast

def 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 Typ.one) && (q.companion? x).isSome)

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

All repeat leaves of q.

Equations

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

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

Def 9.11: K_Q, the set of companions.

Equations

• q.companions = (List.filterMap q.companion? q.repeatLeaves).dedup

def 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.companion? z with | none => false | some c => c.isPrefixOf x && !c == x && x.isPrefixOf z) q.repeatLeaves

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

Basic facts about addresses

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

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

theorem QuasiTab.at?_append (q : QuasiTab) (x w : List ℕ) : q.at? (x ++ w) = (q.at? x).bind fun (n : QuasiTab) => n.at? w

theorem QuasiTab.isSome_at?_of_isLeafAt {q : QuasiTab} {x : List ℕ} (h : q.isLeafAt x = true) : (q.at? x).isSome = true

theorem QuasiTab.mem_addresses_of_at? (q : QuasiTab) (x : List ℕ) (h : (q.at? x).isSome = true) : x ∈ q.addresses

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

theorem QuasiTab.mem_subtrees_of_at? {q n : QuasiTab} {x : List ℕ} (h : q.at? x = some n) : n ∈ q.subtrees

The node at an address is one of the subtrees.

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

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

Lemma 9.12

theorem 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 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 QuasiTab.cycs_root (q : QuasiTab) : q.cycs rootAddress = []

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

theorem 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 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.