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

• 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

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 ℕ)

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

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 ℕ)

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 ℕ)

q.cycs x written L_<x in the paper is 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 in q. Part of Definition 9.11.

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]

Auxiliary facts for Lemma 9.12

theorem QuasiTab.isSome_at?_of_prefix {q : QuasiTab} {x z : List ℕ} (hxz : x <+: z) (hz : (q.at? z).isSome = true) : (q.at? x).isSome = true

A prefix of the address of a node is again the address of a node.

theorem QuasiTab.exists_at?_of_isSome_at?_append_cons {q : QuasiTab} {x w : List ℕ} {i : ℕ} (h : (q.at? (x ++ i :: w)).isSome = true) : ∃ (n : QuasiTab), q.at? x = some n ∧ i < n.children.length

If x ++ i :: w is a node, then x is a node with at least i + 1 children.

theorem QuasiTab.eq_of_isLeafAt_of_prefix {q : QuasiTab} {x z : List ℕ} (hx : q.isLeafAt x = true) (hxz : x <+: z) (hz : (q.at? z).isSome = true) : x = z

The only node below a leaf is the leaf itself.

theorem QuasiTab.qlt_of_mem_inits_dropLast {c l : List ℕ} (h : c ∈ l.inits.dropLast) : qlt c l

The elements of l.inits.dropLast are the proper prefixes of l.

theorem QuasiTab.qlt_of_companion? {q : QuasiTab} {z c : List ℕ} (h : q.companion? z = some c) : qlt c z

The companion of a node is a proper ancestor of it.

theorem QuasiTab.mem_repeatLeaves (q : QuasiTab) (z : List ℕ) : z ∈ q.repeatLeaves ↔ q.isRepeatLeaf z = true

theorem QuasiTab.isLeafAt_of_isRepeatLeaf {q : QuasiTab} {z : List ℕ} (h : q.isRepeatLeaf z = true) : q.isLeafAt z = true

theorem QuasiTab.isSome_at?_of_mem_addresses (q : QuasiTab) (x : List ℕ) : x ∈ q.addresses → (q.at? x).isSome = true

Every element of q.addresses is the address of a node.

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

theorem QuasiTab.pairwise_snd_lt_zipIdx {α : Type u_1} (l : List α) (n : ℕ) : List.Pairwise (fun (a b : α × ℕ) => a.2 < b.2) (l.zipIdx n)

theorem QuasiTab.append_lt_append_left {p a b : List ℕ} (h : a < b) : p ++ a < p ++ b

theorem QuasiTab.addresses_pairwise (q : QuasiTab) : List.Pairwise (fun (x1 x2 : List ℕ) => x1 < x2) q.addresses

The addresses are listed in (strictly increasing) lexicographic order.

theorem QuasiTab.repeatLeaves_pairwise (q : QuasiTab) : List.Pairwise (fun (x1 x2 : List ℕ) => x1 < x2) q.repeatLeaves

theorem QuasiTab.cycs_pairwise (q : QuasiTab) (x : List ℕ) : List.Pairwise (fun (x1 x2 : List ℕ) => x1 < x2) (q.cycs x)

theorem QuasiTab.prefix_of_qlt_of_length_eq_one {q n : QuasiTab} {x z : List ℕ} (hn : q.at? x = some n) (hlen : n.children.length = 1) (hxz : qlt x z) (hz : (q.at? z).isSome = true) : x ++ [0] <+: z

A node that is not a leaf and has a unique child x ++ [0] lies above every node strictly below it only via that child.

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) first part: 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

Helper for Lemma 9.12 (d). Note that from x <_Q y alone 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. Hence here 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

Helper for Lemma 9.12 (d) cycs_of_noRep_noComp. Note that when x has several children then the inclusion cycs(y) ⊆ cycs(x) may be strict. Still the inclusion holds in general, and it is the direction that we actually use.

theorem QuasiTab.cycs_repeat {r : List ℕ} (q : QuasiTab) : q.isRepeatLeaf r = true → q.cycs r = [r]

Lemma 9.12 (b) second part: every repeat only has itself in cycs.

theorem QuasiTab.cycs_of_one_child (q : QuasiTab) {x y : List ℕ} (one_child : q.childrenAt x = [y]) : (q.cycs y).Perm (q.cycs x ++ List.filter (fun (z : List ℕ) => decide (q.companion? z = some x)) q.repeatLeaves)

Lemma 9.12 (c) main part, without the companion assumption: if x has unique child y, then cycs(y) consists (up to permutation) of cycs(x) together with the repeat leaves whose companion is x.

theorem QuasiTab.cycs_comp_unique_child_disjoint (q : QuasiTab) (x z : List ℕ) : z ∈ q.cycs x → z ∉ List.filter (fun (z : List ℕ) => decide (q.companion? z = some x)) q.repeatLeaves

Lemma 9.12 (c), disjointness: no element of cycs(x) has x as its companion

theorem QuasiTab.cycs_of_noRep_noComp (q : QuasiTab) {x : List ℕ} : ¬q.isRepeatLeaf x = true → x ∉ q.companions → q.cycs x = List.flatMap q.cycs (q.childrenAt x)

Lemma 9.12 (d): If x is neither a repeat leaf nor a companion, then cycs x consists of cycs y for all children y of x.