Documentation

DescriptiveComplexity.Problems.Qsat.Tags

The shape of the QSAT instance built by the Savitch reduction #

The bookkeeping of the reduction of SUCCINCT-REACH to QSAT: what its elements are, which propositional variable each of them stands for, which clause, and in which order the prefix quantifies them. Everything here is semantic – a predicate on the coordinates of a tagged pair – so that the defining formulas of DescriptiveComplexity.Problems.Qsat.Interp have something to be compared with.

The variables (`DescriptiveComplexity.QVarTag`) #

Write SV for the state variables of the input instance and ⊥ for the minimum of the input order. Levels of the Savitch recursion are indexed by the state variables themselves, in the ambient order.

tag	coordinates	meaning
`sS`, `sT`	`(x, ⊥)`, `x ∈ SV`	the two endpoints `S`, `T` of the walk
`sZ`	`(ℓ, x)`	the midpoint `Z_ℓ` chosen at level `ℓ`
`sU`, `sV`	`(ℓ, x)`	the pair `(U_ℓ, V_ℓ)` passed below level `ℓ`
`sB`	`(ℓ, ⊥)`	the universal bit `b_ℓ` choosing which half is checked
`aS`, `aT`, `aP`	`(a, ⊥)`, `a` arbitrary	the valuations satisfying the three clause groups
`sE`	`(⊥, ⊥)`	the bit saying that the base case is an equality, not a step

The clauses (`DescriptiveComplexity.QClTag`) #

cSrc, cTgt, cStep copy the three clause groups of the input, read on aS, aT and aP; lS, lT, lU, lV tie those valuations to the states they must read and write; bE is the equality branch of the base case; lev is the eight clauses of one level. Each of them is a fixed list of literals (DescriptiveComplexity.qLits), a literal being the tag of its variable, its sign, and a DescriptiveComplexity.QLink saying which coordinates that variable has – which is what keeps the whole matrix clausal and the case analysis finite.

The prefix #

Every variable tag gets a key (grp, lev, slot, sec, ord), of which grp, slot and ord are static numerals (DescriptiveComplexity.keyGrp, DescriptiveComplexity.keySlot, DescriptiveComplexity.keyOrd) and lev, sec are the two coordinates in one order or the other; the prefix is the lexicographic comparison DescriptiveComplexity.KeyLt of the keys. It orders the prefix as S, T – then, for each level ℓ in increasing order, Z_ℓ, b_ℓ, U_ℓ, V_ℓ – then all the auxiliary variables, with b_ℓ the only universal one. Blocks of like polarity are exactly the sets of variables sharing the first three components (DescriptiveComplexity.keyTriple).

Tags #

inductive DescriptiveComplexity.QVarTag :

The tags of the propositional variables of the QSAT instance built by the Savitch reduction.

sS : QVarTag
The source endpoint S of the walk.
sT : QVarTag
The target endpoint T of the walk.
sZ : QVarTag
The midpoint Z_ℓ guessed at level ℓ.
sU : QVarTag
The first component U_ℓ of the pair passed below level ℓ.
sV : QVarTag
The second component V_ℓ of the pair passed below level ℓ.
sB : QVarTag
The universal bit b_ℓ choosing which half of level ℓ is checked.
aS : QVarTag
The valuation satisfying the source clauses.
aT : QVarTag
The valuation satisfying the target clauses.
aP : QVarTag
The valuation satisfying the transition clauses.
sE : QVarTag
The bit saying that the base case is an equality rather than a step.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqQVarTag :

DecidableEq QVarTag

Equations

DescriptiveComplexity.instDecidableEqQVarTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

inductive DescriptiveComplexity.QClTag :

The tags of the clauses of the QSAT instance built by the Savitch reduction.

cSrc : QClTag
A copy of a source clause, read on aS.
cTgt : QClTag
A copy of a target clause, read on aT.
cStep : QClTag
A copy of a transition clause, read on aP and guarded by sE.
lS : Bool → QClTag
aS reads the source endpoint S, in one of the two directions.
lT : Bool → QClTag
aT reads the target endpoint T, in one of the two directions.
lU : Bool → QClTag
aP reads U at the bottom level, guarded by sE.
lV : Bool → QClTag
aP writes V at the bottom level, guarded by sE.
bE : Bool → QClTag
The equality branch of the base case, guarded by sE.
lev : Bool → Bool → Bool → QClTag
One of the eight clauses of a level: the branch of b_ℓ, the component of the pair, and the sign.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqQClTag :

DecidableEq QClTag

Equations

DescriptiveComplexity.instDecidableEqQClTag = DescriptiveComplexity.instDecidableEqQClTag.decEq

Dependency graph

def DescriptiveComplexity.instDecidableEqQClTag.decEq (x✝ x✝¹ : QClTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.QTag :

The tags of the interpretation: a variable tag or a clause tag.

Equations

DescriptiveComplexity.QTag = (DescriptiveComplexity.QVarTag ⊕ DescriptiveComplexity.QClTag)

Instances For

Dependency graph

instance DescriptiveComplexity.instFiniteQVarTag :

Dependency graph

instance DescriptiveComplexity.instFiniteQClTag :

Dependency graph

instance DescriptiveComplexity.instNonemptyQTag :

Dependency graph

inductive DescriptiveComplexity.QLink :

Where a literal's variable sits, relative to the coordinates (p, q) of its clause. Each link determines the variable's coordinates, except the last two, which range over the literals of a clause of the input instance.

atP : QLink
The variable (p, ⊥).
atQ : QLink
The variable (q, ⊥).
botBoth : QLink
The variable (⊥, ⊥).
maxAtP : QLink
The variable (ℓ_max, p), at the bottom level.
same : QLink
The variable (p, q).
minAtQ : QLink
The variable (q, ⊥), only when p is the top level.
predAtQ : QLink
The variable (ℓ', q) for ℓ' the level above p.
occPos : QLink
A variable (r, ⊥) occurring positively in the clause p of the input.
occNeg : QLink
A variable (r, ⊥) occurring negatively in the clause p of the input.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqQLink :

DecidableEq QLink

Equations

DescriptiveComplexity.instDecidableEqQLink x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

structure DescriptiveComplexity.QLit :

A literal of a clause of the constructed instance: the tag of its variable, its sign, and where the variable sits.

vt : QVarTag
The tag of the variable the literal is on.
sign : Bool
The sign of the literal.
link : QLink
Where the variable sits, relative to the clause's coordinates.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqQLit :

DecidableEq QLit

Equations

DescriptiveComplexity.instDecidableEqQLit = DescriptiveComplexity.instDecidableEqQLit.decEq

Dependency graph

def DescriptiveComplexity.instDecidableEqQLit.decEq (x✝ x✝¹ : QLit) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

Dependency graph

The literals of each clause #

def DescriptiveComplexity.levInLits (b w s : Bool) :

The literal of a level clause carrying the input of the level: the midpoint Z_ℓ on the two matching branches, and one of the two endpoints of the level – S/U at the top, T/V at the bottom – on the two others.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.qLits :

QClTag → List QLit

The literals of each clause of the constructed instance. A clause of the input contributes its own literals through DescriptiveComplexity.QLink.occPos and DescriptiveComplexity.QLink.occNeg; every other clause is a fixed list of two or three literals.

Equations

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

Instances For

Dependency graph

The semantics of the tags #

def DescriptiveComplexity.IsSV {A : Type} [FirstOrder.Language.transSys.Structure A] (x : A) :

The element x is a state variable of the input instance.

Equations

DescriptiveComplexity.IsSV x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStateVar ![x]

Instances For

Dependency graph

def DescriptiveComplexity.IsMinSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (x : A) :

The element x is the first state variable: the top level.

Equations

DescriptiveComplexity.IsMinSV x = (DescriptiveComplexity.IsSV x ∧ ∀ (z : A), DescriptiveComplexity.IsSV z → ¬z < x)

Instances For

Dependency graph

def DescriptiveComplexity.IsMaxSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (x : A) :

The element x is the last state variable: the bottom level.

Equations

DescriptiveComplexity.IsMaxSV x = (DescriptiveComplexity.IsSV x ∧ ∀ (z : A), DescriptiveComplexity.IsSV z → ¬x < z)

Instances For

Dependency graph

def DescriptiveComplexity.IsPredSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (x y : A) :

The state variable x is the one just above the state variable y.

Equations

DescriptiveComplexity.IsPredSV x y = (DescriptiveComplexity.IsSV x ∧ DescriptiveComplexity.IsSV y ∧ x < y ∧ ∀ (z : A), DescriptiveComplexity.IsSV z → ¬(x < z ∧ z < y))

Instances For

Dependency graph

def DescriptiveComplexity.QVarOn {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] :

QVarTag → A → A → Prop

Which tagged pairs are variables: the mark each variable tag puts on its coordinates.

Equations

DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.sS = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ IsBot q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.sT = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ IsBot q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.sB = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ IsBot q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.sZ = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ DescriptiveComplexity.IsSV q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.sU = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ DescriptiveComplexity.IsSV q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.sV = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ DescriptiveComplexity.IsSV q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.aS = fun (x q : A) => IsBot q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.aT = fun (x q : A) => IsBot q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.aP = fun (x q : A) => IsBot q
DescriptiveComplexity.QVarOn DescriptiveComplexity.QVarTag.sE = fun (p q : A) => IsBot p ∧ IsBot q

Instances For

Dependency graph

def DescriptiveComplexity.QClOn {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] :

QClTag → A → A → Prop

Which tagged pairs are clauses: the guard of each clause tag.

Equations

DescriptiveComplexity.QClOn DescriptiveComplexity.QClTag.cSrc = fun (p q : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsSrcCl ![p] ∧ IsBot q
DescriptiveComplexity.QClOn DescriptiveComplexity.QClTag.cTgt = fun (p q : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsTgtCl ![p] ∧ IsBot q
DescriptiveComplexity.QClOn DescriptiveComplexity.QClTag.cStep = fun (p q : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStepCl ![p] ∧ IsBot q
DescriptiveComplexity.QClOn (DescriptiveComplexity.QClTag.lS a) = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ IsBot q
DescriptiveComplexity.QClOn (DescriptiveComplexity.QClTag.lT a) = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ IsBot q
DescriptiveComplexity.QClOn (DescriptiveComplexity.QClTag.lU a) = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ IsBot q
DescriptiveComplexity.QClOn (DescriptiveComplexity.QClTag.lV a) = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNext ![p, q]
DescriptiveComplexity.QClOn (DescriptiveComplexity.QClTag.bE a) = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ IsBot q
DescriptiveComplexity.QClOn (DescriptiveComplexity.QClTag.lev a b c) = fun (p q : A) => DescriptiveComplexity.IsSV p ∧ DescriptiveComplexity.IsSV q

Instances For

Dependency graph

def DescriptiveComplexity.LinkOn {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] :

QLink → A → A → A → A → Prop

Where a literal's variable sits: the coordinates (r, s) of the variable of a literal of the clause (p, q).

Equations

DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.atP = fun (p x r s : A) => r = p ∧ IsBot s
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.atQ = fun (x q r s : A) => r = q ∧ IsBot s
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.botBoth = fun (x x_1 r s : A) => IsBot r ∧ IsBot s
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.maxAtP = fun (p x r s : A) => DescriptiveComplexity.IsMaxSV r ∧ s = p
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.same = fun (p q r s : A) => r = p ∧ s = q
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.minAtQ = fun (p q r s : A) => DescriptiveComplexity.IsMinSV p ∧ r = q ∧ IsBot s
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.predAtQ = fun (p q r s : A) => DescriptiveComplexity.IsPredSV r p ∧ s = q
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.occPos = fun (p x r s : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![p, r] ∧ IsBot s
DescriptiveComplexity.LinkOn DescriptiveComplexity.QLink.occNeg = fun (p x r s : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![p, r] ∧ IsBot s

Instances For

Dependency graph

The quantifier prefix #

def DescriptiveComplexity.keyGrp :

QVarTag → ℕ

The outermost component of the key: the endpoints, then the levels, then the auxiliary variables.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.keySlot :

QVarTag → ℕ

The middle component of the key: within a level, the midpoint, then the universal bit, then the pair.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.keyOrd :

QVarTag → ℕ

The innermost component of the key, breaking ties between tags that share everything else.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.levFst :

QVarTag → Bool

Whether the level of a variable is its first coordinate (its second one otherwise).

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.qKey_inj {v v' : QVarTag} (hg : keyGrp v = keyGrp v') (hs : keySlot v = keySlot v') (ho : keyOrd v = keyOrd v') :

v = v'

The key of a variable tag is injective: the triples (keyGrp, keySlot, keyOrd) are pairwise distinct, which is what makes the prefix a linear order.

Dependency graph

def DescriptiveComplexity.keyLev {A : Type} (v : QVarTag) (p q : A) :

A

The coordinate of a variable that carries its level.

Equations

DescriptiveComplexity.keyLev v p q = if DescriptiveComplexity.levFst v = true then p else q

Instances For

Dependency graph

def DescriptiveComplexity.keySec {A : Type} (v : QVarTag) (p q : A) :

A

The coordinate of a variable that does not carry its level.

Equations

DescriptiveComplexity.keySec v p q = if DescriptiveComplexity.levFst v = true then q else p

Instances For

Dependency graph

def DescriptiveComplexity.keyTriple {A : Type} (v : QVarTag) (p q : A) :

ℕ × A × ℕ

The block coordinates of a variable: the components of its key that a whole quantifier block shares.

Equations

DescriptiveComplexity.keyTriple v p q = (DescriptiveComplexity.keyGrp v, DescriptiveComplexity.keyLev v p q, DescriptiveComplexity.keySlot v)

Instances For

Dependency graph

def DescriptiveComplexity.TripleLt {A : Type} [LinearOrder A] (t t' : ℕ × A × ℕ) :

The lexicographic comparison of block coordinates.

Equations

DescriptiveComplexity.TripleLt t t' = (t.1 < t'.1 ∨ t.1 = t'.1 ∧ (t.2.1 < t'.2.1 ∨ t.2.1 = t'.2.1 ∧ t.2.2 < t'.2.2))

Instances For

Dependency graph

def DescriptiveComplexity.KeyLt {A : Type} [LinearOrder A] (v : QVarTag) (p q : A) (v' : QVarTag) (p' q' : A) :

The quantifier prefix: the lexicographic comparison of the keys, first on the block coordinates and then on the two remaining components.

Equations

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

Instances For

Dependency graph

The prefix is a strict linear order #

theorem DescriptiveComplexity.tripleLt_irrefl {A : Type} [LinearOrder A] (t : ℕ × A × ℕ) :

Dependency graph

theorem DescriptiveComplexity.tripleLt_trans {A : Type} [LinearOrder A] {t t' t'' : ℕ × A × ℕ} (h : TripleLt t t') (h' : TripleLt t' t'') :

Dependency graph

theorem DescriptiveComplexity.tripleLt_total {A : Type} [LinearOrder A] {t t' : ℕ × A × ℕ} (hne : t ≠ t') :

TripleLt t t' ∨ TripleLt t' t

Dependency graph

theorem DescriptiveComplexity.keyLt_irrefl {A : Type} [LinearOrder A] (v : QVarTag) (p q : A) :

¬KeyLt v p q v p q

Dependency graph

theorem DescriptiveComplexity.keyLt_trans {A : Type} [LinearOrder A] {v v' v'' : QVarTag} {p q p' q' p'' q'' : A} (h : KeyLt v p q v' p' q') (h' : KeyLt v' p' q' v'' p'' q'') :

KeyLt v p q v'' p'' q''

Dependency graph

theorem DescriptiveComplexity.eq_of_key_eq {A : Type} {v v' : QVarTag} {p q p' q' : A} (htr : keyTriple v p q = keyTriple v' p' q') (hs : keySec v p q = keySec v' p' q') (ho : keyOrd v = keyOrd v') :

v = v' ∧ p = p' ∧ q = q'

A variable is determined by its key together with its coordinates: this is what makes distinct variables comparable.

Dependency graph

theorem DescriptiveComplexity.keyLt_total {A : Type} [LinearOrder A] {v v' : QVarTag} {p q p' q' : A} (hne : ¬(v = v' ∧ p = p' ∧ q = q')) :

KeyLt v p q v' p' q' ∨ KeyLt v' p' q' v p q

The prefix is total on the variables: two distinct variables are comparable.

Dependency graph

theorem DescriptiveComplexity.keyLt_of_tripleLt {A : Type} [LinearOrder A] {v v' : QVarTag} {p q p' q' : A} (h : TripleLt (keyTriple v p q) (keyTriple v' p' q')) :

KeyLt v p q v' p' q'

A variable of a block precedes every variable of a later block.

Dependency graph

theorem DescriptiveComplexity.tripleLt_or_eq_of_keyLt {A : Type} [LinearOrder A] {v v' : QVarTag} {p q p' q' : A} (h : KeyLt v p q v' p' q') :

TripleLt (keyTriple v p q) (keyTriple v' p' q') ∨ keyTriple v p q = keyTriple v' p' q'

Comparable variables have comparable block coordinates.

Dependency graph