Documentation

DescriptiveComplexity.Problems.Qsat.Prefix

The quantifier prefix of the constructed instance #

The constructed instance is well formed (DescriptiveComplexity.qsatWf_qsatInterp), and its prefix splits into the blocks the correctness proof peels off.

An element of the constructed instance is a tagged pair, named DescriptiveComplexity.qVar when its tag is a variable tag and DescriptiveComplexity.qCl when it is a clause tag; every relation of the instance is read on those named constructors rather than on raw pairs, since the universe of an interpretation is a non-reducible definition.

A block is a set of variables sharing their block coordinates DescriptiveComplexity.keyTriple, and the position just before it is the set of variables whose coordinates are strictly smaller (DescriptiveComplexity.QPlayed). The two facts the peeling lemmas of DescriptiveComplexity.Problems.Qsat.Blocks ask for – being the next block, and downward closure of the position – hold for every triple (DescriptiveComplexity.qBlock_qBlk, DescriptiveComplexity.qDownClosed_qPlayed), so a peeling step is only ever a matter of recognizing which triple comes next (DescriptiveComplexity.qPlayed_step).

def DescriptiveComplexity.qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (p q : A) :

QM A

The element standing for the variable v at the coordinates (p, q).

Equations

DescriptiveComplexity.qVar v p q = (Sum.inl v, ![p, q])

Instances For

Dependency graph

def DescriptiveComplexity.qCl {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (p q : A) :

QM A

The element standing for the clause c at the coordinates (p, q).

Equations

DescriptiveComplexity.qCl c p q = (Sum.inr c, ![p, q])

Instances For

Dependency graph

theorem DescriptiveComplexity.qVar_inj {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {v v' : QVarTag} {p q p' q' : A} (h : qVar v p q = qVar v' p' q') :

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

Dependency graph

theorem DescriptiveComplexity.qm_cases {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (x : QM A) :

(∃ (v : QVarTag) (p : A) (q : A), x = qVar v p q) ∨ ∃ (c : QClTag) (p : A) (q : A), x = qCl c p q

Every element is a variable or a clause at some pair of coordinates.

Dependency graph

The relations, read on the named constructors #

@[simp]

theorem DescriptiveComplexity.isQVar_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (p q : A) :

IsQVar (qVar v p q) ↔ QVarOn v p q

Dependency graph

@[simp]

theorem DescriptiveComplexity.not_isQVar_qCl {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (p q : A) :

¬IsQVar (qCl c p q)

Dependency graph

@[simp]

theorem DescriptiveComplexity.isQAll_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (p q : A) :

IsQAll (qVar v p q) ↔ v = QVarTag.sB ∧ QVarOn v p q

Dependency graph

@[simp]

theorem DescriptiveComplexity.not_isQAll_qCl {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (p q : A) :

¬IsQAll (qCl c p q)

Dependency graph

@[simp]

theorem DescriptiveComplexity.isClause_qCl {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (p q : A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsIsClause ![qCl c p q] ↔ QClOn c p q

Dependency graph

@[simp]

theorem DescriptiveComplexity.not_isClause_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (p q : A) :

¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsIsClause ![qVar v p q]

Dependency graph

@[simp]

theorem DescriptiveComplexity.qPrec_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v v' : QVarTag) (p q p' q' : A) :

QPrec (qVar v p q) (qVar v' p' q') ↔ QVarOn v p q ∧ QVarOn v' p' q' ∧ KeyLt v p q v' p' q'

Dependency graph

@[simp]

theorem DescriptiveComplexity.posIn_qCl_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (v : QVarTag) (p q r s : A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsPosIn ![qCl c p q, qVar v r s] ↔ ∃ l ∈ qLits c, l.vt = v ∧ l.sign = true ∧ QClOn c p q ∧ QVarOn v r s ∧ LinkOn l.link p q r s

Dependency graph

@[simp]

theorem DescriptiveComplexity.negIn_qCl_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (v : QVarTag) (p q r s : A) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsNegIn ![qCl c p q, qVar v r s] ↔ ∃ l ∈ qLits c, l.vt = v ∧ l.sign = false ∧ QClOn c p q ∧ QVarOn v r s ∧ LinkOn l.link p q r s

Dependency graph

Well-formedness #

theorem DescriptiveComplexity.qsatWf_qsatInterp {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] :

The constructed instance is well formed: the prefix is the lexicographic comparison of the keys, which is a strict linear order on the variables because a variable is determined by its key and its coordinates.

Dependency graph

Blocks #

def DescriptiveComplexity.QBlk {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (T : ℕ × A × ℕ) :

QM A → Prop

The variables of the block with block coordinates T.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.QPlayed {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (T : ℕ × A × ℕ) :

QM A → Prop

The variables quantified before the block with block coordinates T.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.qBlk_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} {v : QVarTag} {p q : A} (hv : QVarOn v p q) (h : keyTriple v p q = T) :

QBlk T (qVar v p q)

Dependency graph

theorem DescriptiveComplexity.qPlayed_qVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} {v : QVarTag} {p q : A} (hv : QVarOn v p q) (h : TripleLt (keyTriple v p q) T) :

QPlayed T (qVar v p q)

Dependency graph

theorem DescriptiveComplexity.qBlk_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} {v : QVarTag} {p q : A} :

QBlk T (qVar v p q) ↔ QVarOn v p q ∧ keyTriple v p q = T

Dependency graph

theorem DescriptiveComplexity.qPlayed_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} {v : QVarTag} {p q : A} :

QPlayed T (qVar v p q) ↔ QVarOn v p q ∧ TripleLt (keyTriple v p q) T

Dependency graph

theorem DescriptiveComplexity.qBlock_qBlk {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (T : ℕ × A × ℕ) :

QBlock (QPlayed T) (QBlk T)

The block is the next one to be quantified at its position.

Dependency graph

theorem DescriptiveComplexity.qDownClosed_qPlayed {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (T : ℕ × A × ℕ) :

QDownClosed (QPlayed T)

The position is downward closed, so the peeling lemmas can be iterated.

Dependency graph

theorem DescriptiveComplexity.qPlayed_step {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T T' : ℕ × A × ℕ} (h : ∀ (v : QVarTag) (p q : A), QVarOn v p q → (TripleLt (keyTriple v p q) T' ↔ TripleLt (keyTriple v p q) T ∨ keyTriple v p q = T)) :

qUnion (QPlayed T) (QBlk T) = QPlayed T'

Passing to the next block: the variables played before the block T' are those played before T together with those of T, as soon as the block coordinates of every variable say so.

Dependency graph