Comparison operator for HAVING enumeration algorithms

Shared definition used by both Provenance.Algorithms.CountEnum and Provenance.Algorithms.SumDP. Matches the operator parameter op ∈ {=, ≠, <, ≤, >, ≥} of the algorithms in the HAVING / ProvSQL paper.

inductive CompOp : Type

Comparison operator on natural numbers, as used by the HAVING enumeration algorithms.

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

@[implicit_reducible]

instance instDecidableEqCompOp : DecidableEq CompOp

Equations

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

@[implicit_reducible]

instance instReprCompOp : Repr CompOp

Equations

• instReprCompOp = { reprPrec := instReprCompOp.repr }

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✝

def CompOp.eval : CompOp → ℕ → ℕ → Prop

Semantics of a comparison operator on natural numbers.

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✝)

@[implicit_reducible]

instance instDecidableEval (op : CompOp) (a b : ℕ) : Decidable (op.eval a b)

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite