Lean2Js.Probe

Imports 3

Trying a shipped theorem's hypotheses at an argument #

A theorem nothing can satisfy proves cleanly: it compiles, it reaches no axiom past the three, and it ships looking like a guarantee. What emit does about that is sample — it offers the theorem's data binders the edge cases the vectors are drawn from, and decides the hypotheses at each tuple until one meets them.

Sampling is not deciding. Whether an arbitrary Prop has a witness is not a question this answers, so what is reported is what was done: no argument among the ones tried meets these hypotheses, never these hypotheses cannot be met. A theorem whose witness lies outside the sample is honest, and refusing it would be the compiler lying in the other direction.

Nothing here imports Lean's frontend, and nothing crosses back into it. Main.lean folds the claim's binders into one closed term ending in probe, and that term is compiled and run inside the environment of the user's own module — so every constant it names has to be one that environment holds, and the sample is generated on this side of the crossing rather than carried over it as a literal.

structure

Lean2Js.Probe.Outcome

source

Type

What one claim's probe found.

witness : Option (List Value)
The first tuple of sampled arguments to meet the hypotheses, where the sample holds one.
decoded : Nat
How many of the tuples offered decoded into the types the binders ask for, and so had the hypotheses decided at them. A sample that does not decode is not an argument at all.

Instances For

Used by

instance

Lean2Js.Probe.instInhabitedOutcome

source

@[instance_reducible]

Inhabited Outcome

Equations

Lean2Js.Probe.instInhabitedOutcome = { default := Lean2Js.Probe.instInhabitedOutcome.default }

Used by

def

Lean2Js.Probe.instReprOutcome.repr

source

Outcome → Nat → Std.Format

Equations

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

Instances For

Used by

instance

Lean2Js.Probe.instReprOutcome

source

@[instance_reducible]

Repr Outcome

Equations

Lean2Js.Probe.instReprOutcome = { reprPrec := Lean2Js.Probe.instReprOutcome.repr }

Used by

def

Lean2Js.Probe.arg

source

{α : Type} [Enc α] (k : α → List Value → Option Bool) :

List Value → Option Bool

One data binder of a claim, decoded out of the head of the tuple.

Enc.ofValue is partial — a Value need not be the encoding of anything in α — and a sample that does not decode says nothing about the hypotheses, so it answers none rather than false. The continuation carries the rest of the tuple, which is what lets a claim of any arity fold into one closed term.

Equations

Lean2Js.Probe.arg k [] = none
Lean2Js.Probe.arg k (v :: rest) = (Lean2Js.Enc.ofValue v).bind fun (a : α) => k a rest

Instances For

Used by

def

Lean2Js.Probe.decided

source

(met : Bool) (_rest : List Value) :

Option Bool

The innermost of that fold: every binder decoded, and the hypotheses decided at them.

Equations

Lean2Js.Probe.decided met _rest = some met

Instances For

Used by

def

Lean2Js.Probe.run

source

(f : List Value → Option Bool) :

List (List Value) → Nat → Outcome

Walks the sample, stopping at the first tuple that meets the hypotheses.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Probe.run f [] x✝ = { witness := none, decoded := x✝ }

Instances For

Used by

def

Lean2Js.Probe.perBinder

source

(cap arity : Nat) :

Nat

How many values each binder is offered, so that the product over them stays under cap. The budget is shared evenly rather than spent on the first binder: a claim whose second argument decides its hypothesis is worth as much as one whose first does.

Equations

Lean2Js.Probe.perBinder cap arity = if (arity == 0) = true then 0 else (List.filter (fun (k : Nat) => decide (k ^ arity ≤ cap)) (List.range (cap + 1))).getLastD 1

Instances For

Used by

def

Lean2Js.Probe.tuples

source

List (List Value) → List (List Value)

The tuples, last binder varying fastest, so the values a Ty's own edge cases put first are tried first. A hypothesis nothing meets is usually false at the first argument it is offered.

Equations

Lean2Js.Probe.tuples [] = [[]]
Lean2Js.Probe.tuples (vs :: rest) = List.flatMap (fun (v : Lean2Js.Value) => List.map (fun (x : List Lean2Js.Value) => v :: x) (Lean2Js.Probe.tuples rest)) vs

Instances For

Used by

def

Lean2Js.Probe.probe

source

(p : Core.Program) (cap width : Nat) (tys : List Core.Ty) (f : List Value → Option Bool) :

Outcome

The whole of one claim's probe, as the one term Main.lean builds and evaluates: the sample comes from the same edgeCases the vectors are drawn from, so an argument this finds is one the differential run would also have offered the declaration.

Equations

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

Instances For

Used by