Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Reversing precedence constraints

Lax434175.PrecedenceReversal · concepts/Lax434175/PrecedenceReversal.lean · lax-434175

proven

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

    Theorem

    Reversing a relation turns every arc i→ji \to j into j→ij \to i. Reversal maps intrees to outtrees and outtrees to intrees, and every other class of the precedence field except quasi-interval orders, divide-and-conquer graphs and level orders to itself; these three are called not reversible here. Reversing the data of a value of the precedence field reverses the relation and transposes arbitrary lags, lij′=ljil'_{ij} = l_{ji}; other lags are kept.

    Theorem. For a reversible class, the reverse of a relation of the class belongs to the reversed class; reversed lags satisfy the same sign condition.

    Concept map
    4 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 inClass_reverse proven

    2 lags_admits_reverse proven

    3 lags_view_reverse proven

    4 view_reverse proven

    Lean source view on GitHub

    1import Lax434175.Precedence
    2
    3/-!
    4---
    5title: Reversing precedence constraints
    6type: theorem
    7---
    8Reversing a relation turns every arc i→ji \to j into j→ij \to i. Reversal maps
    9intrees to outtrees and outtrees to intrees, and every other class of the
    10precedence field except quasi-interval orders, divide-and-conquer graphs and
    11level orders to itself; these three are called not reversible here.
    12Reversing the data of a value of the precedence field reverses the relation
    13and transposes arbitrary lags, lij′=ljil'_{ij} = l_{ji}; other lags are kept.
    14
    15**Theorem.** For a reversible class, the reverse of a relation of the class
    16belongs to the reversed class; reversed lags satisfy the same sign
    17condition.
    18-/
    19
    20namespace Lax434175.PrecedenceReversal
    21open Lax434175.Precedence
    22
    23/-- The class of the reverses of the relations of a class. -/
    24def reverse : Order → Order
    25 | .intree => .outtree
    26 | .outtree => .intree
    27 | o => o
    28
    29/-- The classes whose reverses are shown to stay in a class. -/
    30def reversible : Order → Bool
    31 | .quasiInterval | .divideAndConquer | .levelOrder => false
    32 | _ => true
    33
    34/-- The reversed relation of a value. -/
    35def reverseData {n : ℕ} : (o : Order) → o.Data n → (reverse o).Data n
    36 | .none, _ => ()
    37 | .chains, r | .intree, r | .outtree, r | .tree, r | .opposingForest, r
    38 | .seriesParallel, r | .divideAndConquer, r | .intervalOrder, r | .quasiInterval, r
    39 | .overInterval, r | .aOrder, r | .levelOrder, r | .boundedHeight, r | .dimensionTwo, r
    40 | .boundedDimension, r | .prec, r => fun i j => r j i
    41
    42/-- The transposed lags of a value. -/
    43def lagsReverseData {n : ℕ} : (l : Lags) → l.Data n → l.Data n
    44 | .arbitrary, d | .arbitraryNonpositive, d | .arbitraryPositive, d => fun i j => d j i
    45 | .zero, d | .unit, d | .constant, d | .constantNonpositive, d | .constantPositive, d => d
    46
    47axiom view_reverse {n : ℕ} (o : Order) (d : o.Data n) (i j : Fin n) :
    48 (reverse o).view (reverseData o d) i j ↔ o.view d j i
    49
    50axiom lags_view_reverse {n : ℕ} (l : Lags) (d : l.Data n) (i j : Fin n) :
    51 l.view (lagsReverseData l d) i j = l.view d j i
    52
    53axiom inClass_reverse {n : ℕ} (m : ℕ) (o : Order) (h : reversible o = true)
    54 (r : Fin n → Fin n → Prop) : o.InClass m r → (reverse o).InClass m (fun i j => r j i)
    55
    56axiom lags_admits_reverse {n : ℕ} (l : Lags) (d : l.Data n) :
    57 l.Admits (l.view d) → l.Admits (l.view (lagsReverseData l d))
    58
    59end Lax434175.PrecedenceReversal
    60
    Show ProofShow ProofShow ProofShow Proof
    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…