Improvable lower bounds.

The typeclass Estimator a ε, where a : Thunk α and ε : Type, states that e : ε carries the data of a lower bound for a.get, in the form bound_le : bound a e ≤ a.get, along with a mechanism for asking for a better bound improve e : Option ε, satisfying

match improve e with
| none => bound e = a.get
| some e' => bound e < bound e'

i.e. it returns none if the current bound is already optimal, and otherwise a strictly better bound.

(The value in α is hidden inside a Thunk to prevent evaluating it: the point of this typeclass is to work with cheap-to-compute lower bounds for expensive values.)

An appropriate well-foundedness condition would then ensure that repeated improvements reach the exact value.

class EstimatorData {α : Type u_1} (a : Thunk α) (ε : Type u_2) : Type (max u_1 u_2)

• bound : ε → α

  The value of the bound for a representation by a term of ε.

• improve : ε → Option ε

  Generate an improved lower bound.

Given [EstimatorData a ε]

• a term e : ε can be interpreted via bound a e : α as a lower bound for a, and
• we can ask for an improved lower bound via improve a e : Option ε.

The value a in α that we are estimating is hidden inside a Thunk to avoid evaluation.

class Estimator {α : Type u_1} [Preorder α] (a : Thunk α) (ε : Type u_2) extends EstimatorData : Type (max u_1 u_2)

• bound : ε → α
• improve : ε → Option ε
• bound_le : ∀ (e : ε), EstimatorData.bound a e ≤ Thunk.get a

  The calculated bounds are always lower bounds.

• improve_spec : ∀ (e : ε), match EstimatorData.improve a e with | none => EstimatorData.bound a e = Thunk.get a | some e' => EstimatorData.bound a e < EstimatorData.bound a e'

  Calling improve either gives a strictly better bound, or a proof that the current bound is exact.

Given [Estimator a ε]

• we have bound a e ≤ a.get, and
• improve a e returns none iff bound a e = a.get, and otherwise it returns a strictly better bound.

instance instEstimatorPureSubtypeEq {α : Type u_1} [Preorder α] (a : α) : Estimator (Thunk.pure a) { x // x = a }

A trivial estimator.

def Estimator.improveUntilAux {α : Type u_1} {ε : Type u_2} [PartialOrder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool) : Except (Option ε) ε

Implementation of Estimator.improveUntil.

Equations

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

def Estimator.improveUntil {α : Type u_1} {ε : Type u_2} [PartialOrder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) : Except (Option ε) ε

Improve an estimate until it satisfies a predicate, or else return the best available estimate, if any improvement was made.

theorem Estimator.improveUntilAux_spec {α : Type u_2} [PartialOrder α] {ε : Type u_1} (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool) : match Estimator.improveUntilAux a p e r with | Except.error a => ¬p (Thunk.get a) = true | Except.ok e' => p (EstimatorData.bound a e') = true

If Estimator.improveUntil a p e returns some e', then bound a e' satisfies p. Otherwise, that value a must not satisfy p.

theorem Estimator.improveUntil_spec {α : Type u_2} [PartialOrder α] {ε : Type u_1} (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) : match Estimator.improveUntil a p e with | Except.error a => ¬p (Thunk.get a) = true | Except.ok e' => p (EstimatorData.bound a e') = true

If Estimator.improveUntil a p e returns some e', then bound a e' satisfies p. Otherwise, that value a must not satisfy p.

instance instWellFoundedGTElemRangeBoundToEstimatorDataToPreorderLtToLTMemSetInstMembershipSet {α : Type u_1} [PartialOrder α] [∀ (a : α), WellFoundedGT { x // x ≤ a }] {a : Thunk α} {ε : Type u_2} [Estimator a ε] : WellFoundedGT ↑(Set.range (EstimatorData.bound a))

structure Estimator.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : Thunk (α × β)) (ε : Type u_3) [Estimator p ε] : Type u_3

• inner : ε

  The wrapped bound for a value in α × β, which we will use as a bound for the first component.

An estimator for (a, b) can be turned into an estimator for a, simply by repeatedly running improve until the first factor "improves". The hypothesis that > is well-founded on { q // q ≤ (a, b) } ensures this terminates.

instance instEstimatorDataFstToPreorderToPreorderProd {α : Type u_1} {β : Type u_2} [PartialOrder α] [DecidableRel fun x x_1 => x < x_1] [PartialOrder β] {a : Thunk α} {b : Thunk β} (ε : Type u_3) [Estimator (Thunk.prod a b) ε] [∀ (p : α × β), WellFoundedGT { q // q ≤ p }] : EstimatorData a (Estimator.fst (Thunk.prod a b) ε)

def Estimator.fstInst {α : Type u_1} {β : Type u_2} [PartialOrder α] [DecidableRel fun x x_1 => x < x_1] [PartialOrder β] [∀ (p : α × β), WellFoundedGT { q // q ≤ p }] (a : Thunk α) (b : Thunk β) {ε : Type u_3} (i : Estimator (Thunk.prod a b) ε) : Estimator a (Estimator.fst (Thunk.prod a b) ε)

Given an estimator for a pair, we can extract an estimator for the first factor.