Lax Lean Archive

φ-patterns

Lax185574.PhiPatterns · concepts/Lax185574/PhiPatterns.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    For a first-order formula φ(x̄, z), a φ-pattern is a (φ, ψ)-pattern with ψ(y, z) = E(y, z) or ψ(y, z) = ¬E(y, z). These are called a (φ, E)-pattern and a (φ, ¬E)-pattern, respectively. Such a pattern consists of tuples ā₁, …, ā_s ∈ V(G)^{|x̄|}, vertices b₁, …, b_t ∈ V(G) and (c_{i,j} : i ∈ [s], j ∈ [t]). The tuple b̄ = (b₁, …, b_t) is the base of the pattern.

    Concept map
    2 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 22 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.PhiPsiPatterns
    2
    3/-!
    4---
    5title: φ-patterns
    6type: definition
    7---
    8For a first-order formula φ(x̄, z), a *φ-pattern* is a (φ, ψ)-pattern
    9with ψ(y, z) = E(y, z) or ψ(y, z) = ¬E(y, z). These are called a
    10*(φ, E)-pattern* and a *(φ, ¬E)-pattern*, respectively. Such a pattern
    11consists of tuples ā₁, …, ā_s ∈ V(G)^{|x̄|}, vertices b₁, …, b_t ∈ V(G)
    12and (c_{i,j} : i ∈ [s], j ∈ [t]). The tuple b̄ = (b₁, …, b_t) is the
    13*base* of the pattern.
    14
    15# Formalization notes
    16
    17The formula E(y, z) is the adjacency atom with y the single variable of
    18the left summand and z the variable of the right summand, as in
    19`PhiPsiPatterns`. A φ-pattern is a pattern for this formula or for its
    20negation. The base vertex bⱼ is the single entry of the tuple b̄ⱼ of
    21length one.
    22-/
    23
    24namespace Lax185574.PhiPatterns
    25
    26open FirstOrder FirstOrder.Language
    27open Lax185574.PhiPsiPatterns
    28
    29universe u
    30
    31variable {V : Type u}
    32
    33/-- The formula `E(y, z)`. -/
    34def edgeFormula : Language.graph.Formula (Fin 1 ⊕ Fin 1) :=
    35 Relations.formula₂ Language.adj (Term.var (Sum.inl 0)) (Term.var (Sum.inr 0))
    36
    37/-- `G` contains a `φ`-pattern of order `s × t`: a `(φ, E)`-pattern or a
    38`(φ, ¬E)`-pattern. -/
    39def HasPhiPattern (G : SimpleGraph V) {p : ℕ}
    40 (φ : Language.graph.Formula (Fin p ⊕ Fin 1)) (s t : ℕ) : Prop :=
    41 HasPattern G φ edgeFormula s t ∨ HasPattern G φ edgeFormula.not s t
    42
    43end Lax185574.PhiPatterns
    44
    Formalization notes

    The formula E(y, z) is the adjacency atom with y the single variable of the left summand and z the variable of the right summand, as in PhiPsiPatternsPhiPsiPatterns. A φ-pattern is a pattern for this formula or for its negation. The base vertex bⱼ is the single entry of the tuple b̄ⱼ of length one.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…