lean2js

Lean2Js.Fuel

source

Imports 2

Taking fuel out of the claims: more of it never changes an answer #

Fuel is what makes the reference semantics total; the language has none. Taking it out of the claims starts here: an answer evalExpr gives at one fuel is the answer it gives at any larger one.

Every statement is in terms of Refines, which carves out the one thing more fuel can change. The recursion is on the fuel rather than the expression, so the traversals get their own statements: inside the induction they are proved from the step below, and once evalExpr_succ is out they follow from it directly.

def

Lean2Js.Fuel.Refines

source
{α : Type} (a b : Except Err α) :
Prop

Two results that agree, unless the first is what running out of fuel looks like.

Equations
Instances For
    Used by
      theorem

      Lean2Js.Fuel.Refines.rfl'

      source
      {α : Type} (a : Except Err α) :
      Refines a a
      Used by
        theorem

        Lean2Js.Fuel.Refines.trans

        source
        {α : Type} {a b c : Except Err α} (h1 : Refines a b) (h2 : Refines b c) :
        Refines a c
        Used by
          theorem

          Lean2Js.Fuel.Refines.bind

          source
          {α β : Type} {a a' : Except Err α} {k k' : α → Except Err β} (ha : Refines a a') (hk : ∀ (v : α), Refines (k v) (k' v)) :
          Refines (a >>= k) (a' >>= k')
          Used by
            theorem

            Lean2Js.Fuel.evalExpr_succ

            source
            (p : Core.Program) (f : Nat) (env : Env) (e : Core.Expr) :
            Refines (evalExpr p f env e) (evalExpr p (f + 1) env e)
            Used by
              theorem

              Lean2Js.Fuel.evalExpr_add

              source
              (p : Core.Program) (env : Env) (e : Core.Expr) (f k : Nat) :
              Refines (evalExpr p f env e) (evalExpr p (f + k) env e)
              Used by
                theorem

                Lean2Js.Fuel.evalExpr_mono

                source
                (p : Core.Program) {f g : Nat} (env : Env) (e : Core.Expr) (h : f ≤ g) :
                Refines (evalExpr p f env e) (evalExpr p g env e)

                More fuel does not change an answer the reference semantics already gave.

                Used by
                  theorem

                  Lean2Js.Fuel.evalExpr_of_le

                  source
                  {p : Core.Program} {f g : Nat} {env : Env} {e : Core.Expr} {r : Except Err Value} (h : f ≤ g) (hne : r ≠ Except.error Err.outOfFuel) (heq : evalExpr p f env e = r) :
                  evalExpr p g env e = r
                  Used by
                    theorem

                    Lean2Js.Fuel.evalArgs_succ

                    source
                    (p : Core.Program) (f : Nat) (env : Env) (es : List Core.Expr) :
                    Refines (evalArgs p f env es) (evalArgs p (f + 1) env es)
                    Used by
                      theorem

                      Lean2Js.Fuel.evalMapItems_succ

                      source
                      (p : Core.Program) (f : Nat) (env : Env) (b : String) (body : Core.Expr) (xs : List Value) :
                      Refines (evalMapItems p f env b body xs) (evalMapItems p (f + 1) env b body xs)
                      Used by
                        theorem

                        Lean2Js.Fuel.evalFilterItems_succ

                        source
                        (p : Core.Program) (f : Nat) (env : Env) (b : String) (body : Core.Expr) (xs : List Value) :
                        Refines (evalFilterItems p f env b body xs) (evalFilterItems p (f + 1) env b body xs)
                        Used by
                          theorem

                          Lean2Js.Fuel.evalFindItems_succ

                          source
                          (p : Core.Program) (f : Nat) (env : Env) (b : String) (body : Core.Expr) (xs : List Value) :
                          Refines (evalFindItems p f env b body xs) (evalFindItems p (f + 1) env b body xs)
                          Used by
                            theorem

                            Lean2Js.Fuel.evalQuantItems_succ

                            source
                            (p : Core.Program) (f : Nat) (env : Env) (op : Core.QuantOp) (b : String) (body : Core.Expr) (xs : List Value) :
                            Refines (evalQuantItems p f env op b body xs) (evalQuantItems p (f + 1) env op b body xs)
                            Used by
                              theorem

                              Lean2Js.Fuel.evalReduceItems_succ

                              source
                              (p : Core.Program) (f : Nat) (env : Env) (a b : String) (body : Core.Expr) (xs : List Value) (acc : Value) :
                              Refines (evalReduceItems p f env a b body acc xs) (evalReduceItems p (f + 1) env a b body acc xs)
                              Used by