Documentation

Provenance.Algorithms.CompOp

Comparison operator for HAVING enumeration algorithms #

Shared definition used by Provenance.Algorithms.CountEnum, Provenance.Algorithms.SumDP and Provenance.HavingMinMax. The operator parameter is op ∈ {=, ≠, <, ≤, >, ≥}.

inductive CompOp :

Comparison operator, as used by the HAVING enumeration algorithms.

eq : CompOp
ne : CompOp
lt : CompOp
le : CompOp
gt : CompOp
ge : CompOp

Instances For

Dependency graph

@[instance_reducible]

instance instDecidableEqCompOp :

DecidableEq CompOp

Equations

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

Dependency graph

def instReprCompOp.repr :

CompOp → ℕ → Std.Format

Equations

instReprCompOp.repr CompOp.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CompOp.eq")).group prec✝
instReprCompOp.repr CompOp.ne prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CompOp.ne")).group prec✝
instReprCompOp.repr CompOp.lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CompOp.lt")).group prec✝
instReprCompOp.repr CompOp.le prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CompOp.le")).group prec✝
instReprCompOp.repr CompOp.gt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CompOp.gt")).group prec✝
instReprCompOp.repr CompOp.ge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CompOp.ge")).group prec✝

Instances For

Dependency graph

@[instance_reducible]

instance instReprCompOp :

Equations

instReprCompOp = { reprPrec := instReprCompOp.repr }

Dependency graph

def CompOp.eval {V : Type u_1} [LinearOrder V] :

CompOp → V → V → Prop

Semantics of a comparison operator over any linearly ordered value domain (the aggregate values compared by a HAVING predicate; the enumeration algorithms use it at V = ℕ).

Equations

CompOp.eq.eval x✝¹ x✝ = (x✝¹ = x✝)
CompOp.ne.eval x✝¹ x✝ = (x✝¹ ≠ x✝)
CompOp.lt.eval x✝¹ x✝ = (x✝¹ < x✝)
CompOp.le.eval x✝¹ x✝ = (x✝¹ ≤ x✝)
CompOp.gt.eval x✝¹ x✝ = (x✝¹ > x✝)
CompOp.ge.eval x✝¹ x✝ = (x✝¹ ≥ x✝)

Instances For

Dependency graph

@[instance_reducible]

instance instDecidableEval {V : Type u_1} [LinearOrder V] (op : CompOp) (a b : V) :

Decidable (op.eval a b)

Equations

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

Dependency graph

def CompOp.negate :

CompOp → CompOp

The complementary comparison operator: op.negate holds exactly when op does not. This is how ProvSQL interprets NOT over an aggregate comparison (PostgreSQL's operator negator), with NOT pushed through Boolean combinations by De Morgan duality.

Equations

Instances For

Dependency graph

theorem CompOp.negate_eval {V : Type u_1} [LinearOrder V] (op : CompOp) (a b : V) :

op.negate.eval a b ↔ ¬op.eval a b

op.negate evaluates to the classical negation of op.

Dependency graph