Skip to content

Lean2Js.Denotes

Imports 4

What one `Core.Expr` claims about one ordinary Lean term #

The certificate a reifier assembles, and the rule it applies at each syntactic form. One lemma per form, each stated so that applying it is the whole of the step: the reifier pastes them together in the order its walk visited the term, and nothing it emits needs a tactic.

Fuel is universally quantified throughout. A declaration that calls another runs the callee on what is left over, so a certificate stated at defaultFuel could not be cited across a call.

def

Lean2Js.Denote.Denotes

(p : Core.Program) (env : Env) (e : Core.Expr) {α : Type} [Enc α] (t : α) :

What one subterm of the author's def claims about one Core.Expr: if the expression returns, it returns the encoding of the term. Fuel is universally quantified because a call runs its callee on what is left over.

Equations

Lean2Js.Denote.Denotes p env e t = ∀ {f : Nat}, f ≤ Lean2Js.defaultFuel → ∀ (v : Lean2Js.Value), Lean2Js.evalExpr p f env e = Except.ok v → v = Lean2Js.Enc.toValue t

Instances For

Used by

theorem

Lean2Js.Denote.denotes_lit

(p : Core.Program) (env : Env) (i : Int) :

Denotes p env (Core.Expr.lit (Core.Lit.int53 i)) i

Used by

theorem

Lean2Js.Denote.denotes_litBool

(p : Core.Program) (env : Env) (b : Bool) :

Denotes p env (Core.Expr.lit (Core.Lit.bool b)) b

Used by

theorem

Lean2Js.Denote.denotes_litStr

(p : Core.Program) (env : Env) (s : String) :

Denotes p env (Core.Expr.lit (Core.Lit.str s)) s

Used by

theorem

Lean2Js.Denote.denotes_var

(p : Core.Program) (env : Env) (name : String) {α : Type} [Enc α] (a : α) (hl : env.lookup? name = some (Enc.toValue a)) :

Denotes p env (Core.Expr.var name) a

Used by

theorem

Lean2Js.Denote.denotes_add

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.add l r) (a + b)

Used by

theorem

Lean2Js.Denote.denotes_sub

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.sub l r) (a - b)

Used by

theorem

Lean2Js.Denote.denotes_mul

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.mul l r) (a * b)

Used by

theorem

Lean2Js.Denote.denotes_div

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.div l r) (Int53.div a b)

Used by

theorem

Lean2Js.Denote.denotes_mod

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.mod l r) (Int53.mod a b)

Used by

Comparison, and the branch it decides #

compareValues answers with an Ordering and the author writes a Prop, so each comparison form needs the one lemma that lines the two up. They are stated about decide rather than the proposition because that is what the condition of an if reifies to.

theorem

Lean2Js.Denote.denotes_lt

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.lt l r) (decide (a < b))

Used by

theorem

Lean2Js.Denote.denotes_le

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.le l r) (decide (a ≤ b))

Used by

theorem

Lean2Js.Denote.denotes_gt

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.gt l r) (decide (a > b))

Used by

theorem

Lean2Js.Denote.denotes_ge

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.ge l r) (decide (a ≥ b))

Used by

theorem

Lean2Js.Denote.denotes_ite

(p : Core.Program) (env : Env) (c t e : Core.Expr) (P : Prop) [Decidable P] {α : Type} [Enc α] (x y : α) (hc : Denotes p env c (decide P)) (ht : Denotes p env t x) (he : Denotes p env e y) :

Denotes p env (c.cond t e) (if P then x else y)

The author writes a proposition and eval branches on a Value, so the condition is carried as decide P and the two sides of the if are walked independently.

Used by

The forms that bind, and the one that crosses a call #

theorem

Lean2Js.Denote.denotes_neg

(p : Core.Program) (env : Env) (e : Core.Expr) (a : Int) (h : Denotes p env e a) :

Denotes p env (Core.Expr.un Core.UnOp.neg e) (-a)

Used by

theorem

Lean2Js.Denote.denotes_abs

(p : Core.Program) (env : Env) (e : Core.Expr) (a : Int) (h : Denotes p env e a) :

Denotes p env (Core.Expr.un Core.UnOp.abs e) (Int53.abs a)

Used by

theorem

Lean2Js.Denote.denotes_toString

(p : Core.Program) (env : Env) (e : Core.Expr) (a : Int) (h : Denotes p env e a) :

Denotes p env (Core.Expr.un Core.UnOp.toString e) (Int53.toString a)

Used by

theorem

Lean2Js.Denote.denotes_range

(p : Core.Program) (env : Env) (e : Core.Expr) (a : Int) (h : Denotes p env e a) :

Denotes p env (Core.Expr.un Core.UnOp.range e) (Arr.range a)

Used by

theorem

Lean2Js.Denote.denotes_letE

(p : Core.Program) (env : Env) (name : String) (ty : Core.Ty) (val body : Core.Expr) {β : Type} [Enc β] (x : β) {α : Type} [Enc α] (t : α) (hv : Denotes p env val x) (hb : Denotes p ((name, Enc.toValue x) :: env) body t) :

Denotes p env (Core.Expr.letE name ty val body) t

Used by

theorem

Lean2Js.Denote.denotes_matchE_of

(p : Core.Program) (env : Env) (scrut : Core.Expr) (alts : List Core.Alt) {β : Type} [Enc β] (x : β) {α : Type} [Enc α] (t : α) (hs : Denotes p env scrut x) (binds : Env) (body : Core.Expr) (hfm : firstMatch alts (Enc.toValue x) = some (binds, body)) (hb : Denotes p (binds ++ env) body t) :

Denotes p env (scrut.matchE alts) t

One arm of a match, once it is known which arm fires. Which one that is depends on the author's value, so this carries the plumbing and deriving Enc generates the per-type lemma that does the case analysis — the subset's matchPat is well-founded and does not reduce on its own.

Used by

theorem

Lean2Js.Denote.denotes_matchE_split

(p : Core.Program) (env : Env) {β : Type} [Enc β] {α : Type} [Enc α] (scrut : Core.Expr) (alts : List Core.Alt) (x : β) (g : β → α) (h : ∀ (y : β), Denotes p env scrut y → Denotes p env (scrut.matchE alts) (g y)) (hs : Denotes p env scrut x) :

Denotes p env (scrut.matchE alts) (g x)

The case analysis a match is read by, stated over every value the scrutinee could take. The splitter could be applied to the scrutinee directly, but its conclusion is the motive applied to what it splits on, and a reifier that writes the motive out leaves the program and the environment in it as holes under that binder: applied to the hole standing for the scrutinee they are not a pattern, and two matches in one term solve each other's scrutinee instead of their own. Asking for h at every y applies the motive to a bound variable, where each of those holes is solved on its own.

Used by

theorem

Lean2Js.Denote.matchPat_bind

(name : String) (v : Value) :

matchPat (Core.Pat.bind name) v = some [(name, v)]

A pattern that only binds accepts any value and binds it. matchPat is well-founded and does not reduce on its own, so the arms a fold is reified to — one per constructor, binding every field — are read through this rather than by computation.

Used by

theorem

Lean2Js.Denote.matchPats_binds

(names : List String) (vs : List Value) :

names.length = vs.length → matchPats (List.map Core.Pat.bind names) vs = some (names.zip vs)

The same for a whole row of them, which is what a fold's alternative is: the binds it makes are the constructor's field names against the rebuilt node's fields, in order.

Used by

theorem

Lean2Js.Denote.ne_of_missed

{α : Sort u} {a b : α} (h : a = b → False) :

b ≠ a

What the matcher's splitter hands an arm about the arms before it, turned around. matchPat compares the pattern's literal against the value, so a proof that an earlier arm missed needs the literal on the left and the splitter states it on the right.

Used by

theorem

Lean2Js.Denote.denotes_decide_eq_true

(p : Core.Program) (env : Env) (e : Core.Expr) (b : Bool) (h : Denotes p env e b) :

Denotes p env e (decide (b = true))

An if on a Bool tests b = true, and the subset's condition is the Bool itself.

Used by

Walking an array #

Each traversal evaluates its body once per element, at the same fuel the node itself ran at, so the element lemma is an induction over the list rather than a step in the walk.

theorem

Lean2Js.Denote.denotes_mapE

(p : Core.Program) (env : Env) (arr : Core.Expr) (binder : String) (body : Core.Expr) {β : Type} [Enc β] (xs : List β) {α : Type} [Enc α] (g : β → α) (ha : Denotes p env arr xs) (hb : ∀ (x : β), Denotes p ((binder, Enc.toValue x) :: env) body (g x)) :

Denotes p env (arr.mapE binder body) (List.map g xs)

Used by

theorem

Lean2Js.Denote.sortPairs_toValue

{β κ : Type} [Enc β] [Enc κ] [Arr.KeyOrd κ] (xs : List β) (g : β → κ) :

sortPairs (List.map (fun (x : β) => (Enc.toValue (g x), Enc.toValue x)) xs) = Except.ok (List.map Enc.toValue (Arr.sortByKey xs g))

The order the walk settles on is the one Arr.sortByKey names. KeyOrd.agrees is what lets the comparison move from the author's key type to the encoded values, and KeyOrd.scalar is what says the sort accepts the keys at all.

Used by

theorem

Lean2Js.Denote.denotes_sortByKeyE

(p : Core.Program) (env : Env) (arr : Core.Expr) (binder : String) (body : Core.Expr) {β : Type} [Enc β] (xs : List β) {κ : Type} [Enc κ] [Arr.KeyOrd κ] (g : β → κ) (ha : Denotes p env arr xs) (hb : ∀ (x : β), Denotes p ((binder, Enc.toValue x) :: env) body (g x)) :

Denotes p env (arr.sortByKeyE binder body) (Arr.sortByKey xs g)

Used by

theorem

Lean2Js.Denote.denotes_filterE

(p : Core.Program) (env : Env) (arr : Core.Expr) (binder : String) (body : Core.Expr) {β : Type} [Enc β] (xs : List β) (q : β → Bool) (ha : Denotes p env arr xs) (hb : ∀ (x : β), Denotes p ((binder, Enc.toValue x) :: env) body (q x)) :

Denotes p env (arr.filterE binder body) (List.filter q xs)

Used by

theorem

Lean2Js.Denote.denotes_findE

(p : Core.Program) (env : Env) (arr : Core.Expr) (binder : String) (body : Core.Expr) {β : Type} [Enc β] (xs : List β) (q : β → Bool) (ha : Denotes p env arr xs) (hb : ∀ (x : β), Denotes p ((binder, Enc.toValue x) :: env) body (q x)) :

Denotes p env (arr.findE binder body) (List.find? q xs)

Used by

theorem

Lean2Js.Denote.denotes_allE

(p : Core.Program) (env : Env) (arr : Core.Expr) (binder : String) (body : Core.Expr) {β : Type} [Enc β] (xs : List β) (q : β → Bool) (ha : Denotes p env arr xs) (hb : ∀ (x : β), Denotes p ((binder, Enc.toValue x) :: env) body (q x)) :

Denotes p env (Core.Expr.quantE Core.QuantOp.all arr binder body) (xs.all q)

Used by

theorem

Lean2Js.Denote.denotes_anyE

(p : Core.Program) (env : Env) (arr : Core.Expr) (binder : String) (body : Core.Expr) {β : Type} [Enc β] (xs : List β) (q : β → Bool) (ha : Denotes p env arr xs) (hb : ∀ (x : β), Denotes p ((binder, Enc.toValue x) :: env) body (q x)) :

Denotes p env (Core.Expr.quantE Core.QuantOp.any arr binder body) (xs.any q)

Used by

theorem

Lean2Js.Denote.denotes_reduceE

(p : Core.Program) (env : Env) (arr init : Core.Expr) (accName elemName : String) (body : Core.Expr) {β : Type} [Enc β] {α : Type} [Enc α] (xs : List β) (a : α) (g : α → β → α) (ha : Denotes p env arr xs) (hi : Denotes p env init a) (hb : ∀ (acc : α) (x : β), Denotes p ((elemName, Enc.toValue x) :: (accName, Enc.toValue acc) :: env) body (g acc x)) :

Denotes p env (arr.reduceE init accName elemName body) (List.foldl g a xs)

Used by

The array itself #

The traversals walk an array; these are the forms that build one, take one apart, or measure it. Reading past the end traps, which is what lets Arr.get be a total Lean function: the certificate claims nothing in the case the subset refuses to answer in.

def

Lean2Js.Denote.DenotesItems

(p : Core.Program) (env : Env) {β : Type} [Enc β] :

List Core.Expr → List β → Prop

The elements of an array literal, against the list the author wrote. It is a list of terms of one type where DenotesArgs is a list of Value: a call's arguments need not share a type and an array's elements do.

Equations

Lean2Js.Denote.DenotesItems p env [] [] = True
Lean2Js.Denote.DenotesItems p env (e :: es) (x_2 :: xs) = (Lean2Js.Denote.Denotes p env e x_2 ∧ Lean2Js.Denote.DenotesItems p env es xs)
Lean2Js.Denote.DenotesItems p env x✝¹ x✝ = False

Instances For

Used by

theorem

Lean2Js.Denote.denotesItems_nil

(p : Core.Program) (env : Env) {β : Type} [Enc β] :

DenotesItems p env [] []

Used by

theorem

Lean2Js.Denote.denotesItems_cons

(p : Core.Program) (env : Env) (e : Core.Expr) (es : List Core.Expr) {β : Type} [Enc β] (x : β) (xs : List β) (h : Denotes p env e x) (hs : DenotesItems p env es xs) :

DenotesItems p env (e :: es) (x :: xs)

Used by

theorem

Lean2Js.Denote.denotes_arrayLit

(p : Core.Program) (env : Env) (elem : Core.Ty) (items : List Core.Expr) {β : Type} [Enc β] (xs : List β) (h : DenotesItems p env items xs) :

Denotes p env (Core.Expr.arrayLit elem items) xs

Used by

theorem

Lean2Js.Denote.denotes_lengthArr

(p : Core.Program) (env : Env) (arr : Core.Expr) {β : Type} [Enc β] (xs : List β) (ha : Denotes p env arr xs) :

Denotes p env arr.length (Arr.length xs)

Used by

theorem

Lean2Js.Denote.denotes_index

(p : Core.Program) (env : Env) (arr idx : Core.Expr) {β : Type} [Enc β] [Inhabited β] (xs : List β) (i : Int) (ha : Denotes p env arr xs) (hi : Denotes p env idx i) :

Denotes p env (arr.index idx) (Arr.get xs i)

Used by

theorem

Lean2Js.Denote.denotes_arraySlice

(p : Core.Program) (env : Env) (arr lo hi : Core.Expr) {β : Type} [Enc β] (xs : List β) (a b : Int) (ha : Denotes p env arr xs) (hlo : Denotes p env lo a) (hhi : Denotes p env hi b) :

Denotes p env (arr.arraySlice lo hi) (Arr.slice xs a b)

Used by

theorem

Lean2Js.Denote.denotes_arrayReverse

(p : Core.Program) (env : Env) (arr : Core.Expr) {β : Type} [Enc β] (xs : List β) (ha : Denotes p env arr xs) :

Denotes p env arr.arrayReverse xs.reverse

Used by

theorem

Lean2Js.Denote.denotes_concatArr

(p : Core.Program) (env : Env) (l r : Core.Expr) {β : Type} [Enc β] (xs ys : List β) (hl : Denotes p env l xs) (hr : Denotes p env r ys) :

Denotes p env (Core.Expr.bin Core.BinOp.concat l r) (xs ++ ys)

Used by

Strings #

A string is a list of code points on both sides — eval counts and slices String.toList, and the generated code goes through Array.from to do the same. What differs is case folding and trimming, where Lean's own functions are full Unicode and the subset's are not: the prelude names the subset's, and the walk reads the prelude rather than String.trim.

theorem

Lean2Js.Denote.denotes_lengthStr

(p : Core.Program) (env : Env) (e : Core.Expr) (s : String) (h : Denotes p env e s) :

Denotes p env e.length (Str.length s)

Used by

theorem

Lean2Js.Denote.denotes_concatStr

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.concat l r) (a ++ b)

Used by

theorem

Lean2Js.Denote.denotes_trim

(p : Core.Program) (env : Env) (e : Core.Expr) (s : String) (h : Denotes p env e s) :

Denotes p env (Core.Expr.strUn Core.StrUnOp.trim e) (Str.trim s)

Used by

theorem

Lean2Js.Denote.denotes_upper

(p : Core.Program) (env : Env) (e : Core.Expr) (s : String) (h : Denotes p env e s) :

Denotes p env (Core.Expr.strUn Core.StrUnOp.upper e) (Str.upper s)

Used by

theorem

Lean2Js.Denote.denotes_toInt

(p : Core.Program) (env : Env) (e : Core.Expr) (s : String) (h : Denotes p env e s) :

Denotes p env (Core.Expr.strUn Core.StrUnOp.toInt e) (Str.toInt? s)

Used by

theorem

Lean2Js.Denote.denotes_lower

(p : Core.Program) (env : Env) (e : Core.Expr) (s : String) (h : Denotes p env e s) :

Denotes p env (Core.Expr.strUn Core.StrUnOp.lower e) (Str.lower s)

Used by

theorem

Lean2Js.Denote.denotes_startsWith

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.strBin Core.StrBinOp.startsWith l r) (Str.startsWith a b)

Used by

theorem

Lean2Js.Denote.denotes_endsWith

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.strBin Core.StrBinOp.endsWith l r) (Str.endsWith a b)

Used by

theorem

Lean2Js.Denote.denotes_includes

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.strBin Core.StrBinOp.includes l r) (Str.includes a b)

Used by

theorem

Lean2Js.Denote.denotes_split

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.strBin Core.StrBinOp.split l r) (Str.split a b)

Used by

theorem

Lean2Js.Denote.denotes_indexOf

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.strBin Core.StrBinOp.indexOf l r) (Str.indexOf? a b)

Used by

theorem

Lean2Js.Denote.denotes_repeat

(p : Core.Program) (env : Env) (l r : Core.Expr) (a : String) (n : Int) (hl : Denotes p env l a) (hr : Denotes p env r n) :

Denotes p env (Core.Expr.strBin Core.StrBinOp.repeat l r) (Str.repeat a n)

Used by

theorem

Lean2Js.Denote.denotes_join

(p : Core.Program) (env : Env) (l r : Core.Expr) (xs : List String) (sep : String) (hl : Denotes p env l xs) (hr : Denotes p env r sep) :

Denotes p env (Core.Expr.strBin Core.StrBinOp.join l r) (Str.join xs sep)

Used by

theorem

Lean2Js.Denote.denotes_substring

(p : Core.Program) (env : Env) (e lo hi : Core.Expr) (s : String) (a b : Int) (hs : Denotes p env e s) (hlo : Denotes p env lo a) (hhi : Denotes p env hi b) :

Denotes p env (e.substring lo hi) (Str.substring s a b)

Used by

Ordering a String is by code point on both sides, but Lean states it as String.lt and eval answers with an Ordering, so each comparison needs the lemma that lines the two up — the same shape the Int comparisons take, over a different order.

theorem

Lean2Js.Denote.denotes_ltStr

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.lt l r) (decide (a < b))

Used by

theorem

Lean2Js.Denote.denotes_leStr

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.le l r) (decide (a ≤ b))

Used by

theorem

Lean2Js.Denote.denotes_gtStr

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.gt l r) (decide (a > b))

Used by

theorem

Lean2Js.Denote.denotes_geStr

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : String) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.ge l r) (decide (a ≥ b))

Used by

Dictionaries #

The keys survive the encoding untouched and the values are encoded one by one, so every form below comes down to one equation between a list operation on the author's entries and the same operation on the encoded ones.

theorem

Lean2Js.Denote.denotes_dictGet

(p : Core.Program) (env : Env) (d key : Core.Expr) {β : Type} [Enc β] (m : Dict β) (k : String) (hd : Denotes p env d m) (hk : Denotes p env key k) :

Denotes p env (d.dictGet key) (m.get k)

Used by

theorem

Lean2Js.Denote.denotes_dictHas

(p : Core.Program) (env : Env) (d key : Core.Expr) {β : Type} [Enc β] (m : Dict β) (k : String) (hd : Denotes p env d m) (hk : Denotes p env key k) :

Denotes p env (d.dictHas key) (m.has k)

Used by

theorem

Lean2Js.Denote.denotes_dictSet

(p : Core.Program) (env : Env) (d key val : Core.Expr) {β : Type} [Enc β] (m : Dict β) (k : String) (x : β) (hd : Denotes p env d m) (hk : Denotes p env key k) (hv : Denotes p env val x) :

Denotes p env (d.dictSet key val) (m.set k x)

Used by

theorem

Lean2Js.Denote.denotes_dictDelete

(p : Core.Program) (env : Env) (d key : Core.Expr) {β : Type} [Enc β] (m : Dict β) (k : String) (hd : Denotes p env d m) (hk : Denotes p env key k) :

Denotes p env (d.dictDelete key) (m.erase k)

Used by

theorem

Lean2Js.Denote.denotes_dictKeys

(p : Core.Program) (env : Env) (d : Core.Expr) {β : Type} [Enc β] (m : Dict β) (hd : Denotes p env d m) :

Denotes p env d.dictKeys m.keys

Used by

theorem

Lean2Js.Denote.denotes_dictValues

(p : Core.Program) (env : Env) (d : Core.Expr) {β : Type} [Enc β] (m : Dict β) (hd : Denotes p env d m) :

Denotes p env d.dictValues m.values

Used by

theorem

Lean2Js.Denote.denotes_lengthDict

(p : Core.Program) (env : Env) (d : Core.Expr) {β : Type} [Enc β] (m : Dict β) (hd : Denotes p env d m) :

Denotes p env d.length m.size

Used by

The same seven over a Dict.Obj. Each proof is its Dict twin with one name substituted: the two spellings encode to the same Value.dict, so what the evaluator does to a receiver does not depend on which of them the author declared.

theorem

Lean2Js.Denote.denotes_dictObjGet

(p : Core.Program) (env : Env) (d key : Core.Expr) {β : Type} [Enc β] (m : Dict.Obj β) (k : String) (hd : Denotes p env d m) (hk : Denotes p env key k) :

Denotes p env (d.dictGet key) (m.get k)

Used by

theorem

Lean2Js.Denote.denotes_dictObjHas

(p : Core.Program) (env : Env) (d key : Core.Expr) {β : Type} [Enc β] (m : Dict.Obj β) (k : String) (hd : Denotes p env d m) (hk : Denotes p env key k) :

Denotes p env (d.dictHas key) (m.has k)

Used by

theorem

Lean2Js.Denote.denotes_dictObjSet

(p : Core.Program) (env : Env) (d key val : Core.Expr) {β : Type} [Enc β] (m : Dict.Obj β) (k : String) (x : β) (hd : Denotes p env d m) (hk : Denotes p env key k) (hv : Denotes p env val x) :

Denotes p env (d.dictSet key val) (m.set k x)

Used by

theorem

Lean2Js.Denote.denotes_dictObjDelete

(p : Core.Program) (env : Env) (d key : Core.Expr) {β : Type} [Enc β] (m : Dict.Obj β) (k : String) (hd : Denotes p env d m) (hk : Denotes p env key k) :

Denotes p env (d.dictDelete key) (m.erase k)

Used by

theorem

Lean2Js.Denote.denotes_dictObjKeys

(p : Core.Program) (env : Env) (d : Core.Expr) {β : Type} [Enc β] (m : Dict.Obj β) (hd : Denotes p env d m) :

Denotes p env d.dictKeys m.keys

Used by

theorem

Lean2Js.Denote.denotes_dictObjValues

(p : Core.Program) (env : Env) (d : Core.Expr) {β : Type} [Enc β] (m : Dict.Obj β) (hd : Denotes p env d m) :

Denotes p env d.dictValues m.values

Used by

theorem

Lean2Js.Denote.denotes_lengthDictObj

(p : Core.Program) (env : Env) (d : Core.Expr) {β : Type} [Enc β] (m : Dict.Obj β) (hd : Denotes p env d m) :

Denotes p env d.length m.size

Used by

def

Lean2Js.Denote.DenotesEntries

(p : Core.Program) (env : Env) {β : Type} [Enc β] :

List (String × Core.Expr) → List (String × β) → Prop

The entries of a dictionary literal. The keys are part of the form rather than evaluated, so what is walked is only the values, and the lemma carries the keys as an equation.

Equations

Lean2Js.Denote.DenotesEntries p env [] [] = True
Lean2Js.Denote.DenotesEntries p env ((k, e) :: es) ((k', x_2) :: xs) = (k = k' ∧ Lean2Js.Denote.Denotes p env e x_2 ∧ Lean2Js.Denote.DenotesEntries p env es xs)
Lean2Js.Denote.DenotesEntries p env x✝¹ x✝ = False

Instances For

Used by

theorem

Lean2Js.Denote.denotesEntries_nil

(p : Core.Program) (env : Env) {β : Type} [Enc β] :

DenotesEntries p env [] []

Used by

theorem

Lean2Js.Denote.denotesEntries_cons

(p : Core.Program) (env : Env) (k : String) (e : Core.Expr) (es : List (String × Core.Expr)) {β : Type} [Enc β] (x : β) (xs : List (String × β)) (h : Denotes p env e x) (hs : DenotesEntries p env es xs) :

DenotesEntries p env ((k, e) :: es) ((k, x) :: xs)

Used by

theorem

Lean2Js.Denote.denotes_dictLit

(p : Core.Program) (env : Env) (value : Core.Ty) (entries : List (String × Core.Expr)) {β : Type} [Enc β] (es : List (String × β)) (h : DenotesEntries p env entries es) :

Denotes p env (Core.Expr.dictLit value false entries) (Dict.ofList es)

Used by

theorem

Lean2Js.Denote.denotes_dictObjLit

(p : Core.Program) (env : Env) (value : Core.Ty) (entries : List (String × Core.Expr)) {β : Type} [Enc β] (es : List (String × β)) (h : DenotesEntries p env entries es) :

Denotes p env (Core.Expr.dictLit value true entries) (Dict.Obj.ofList es)

The twin at the other spelling. The value the two build is the same — Dict.Obj and Dict encode alike — so only the flag the literal carries differs, and with it the type the compiler gives it.

Used by

UInt32 #

The integer that wraps where Int53 traps. Lean's UInt32 wraps at the same bound and divides the same natural numbers, so an author writes the ordinary operators and no prelude function stands between — / and % included, which is what separates this from Int53.

theorem

Lean2Js.Denote.denotes_addU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.add l r) (a + b)

Used by

theorem

Lean2Js.Denote.denotes_subU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.sub l r) (a - b)

Used by

theorem

Lean2Js.Denote.denotes_mulU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.mul l r) (a * b)

Used by

theorem

Lean2Js.Denote.denotes_divU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.div l r) (a / b)

Used by

theorem

Lean2Js.Denote.denotes_modU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.mod l r) (a % b)

Used by

compareValues orders two UInt32s by toNat, and Lean orders them by the same, so each comparison is the Nat one under a different name.

theorem

Lean2Js.Denote.denotes_ltU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.lt l r) (decide (a < b))

Used by

theorem

Lean2Js.Denote.denotes_leU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.le l r) (decide (a ≤ b))

Used by

theorem

Lean2Js.Denote.denotes_gtU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.gt l r) (decide (a > b))

Used by

theorem

Lean2Js.Denote.denotes_geU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.ge l r) (decide (a ≥ b))

Used by

BigInt #

Int took the encoding into Int53, so the integer that need not fit in a JS number is a type of its own. Nothing here traps on a bound — the only form that still refuses is a zero divisor.

theorem

Lean2Js.Denote.denotes_litBig

(p : Core.Program) (env : Env) (i : Int) :

Denotes p env (Core.Expr.lit (Core.Lit.bigint i)) { val := i }

Used by

theorem

Lean2Js.Denote.denotes_addBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.add l r) (a + b)

Used by

theorem

Lean2Js.Denote.denotes_subBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.sub l r) (a - b)

Used by

theorem

Lean2Js.Denote.denotes_mulBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.mul l r) (a * b)

Used by

theorem

Lean2Js.Denote.denotes_divBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.div l r) (a.div b)

Used by

theorem

Lean2Js.Denote.denotes_modBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.mod l r) (a.mod b)

Used by

theorem

Lean2Js.Denote.denotes_negBig

(p : Core.Program) (env : Env) (e : Core.Expr) (a : BigInt) (h : Denotes p env e a) :

Denotes p env (Core.Expr.un Core.UnOp.neg e) (-a)

Used by

theorem

Lean2Js.Denote.denotes_absBig

(p : Core.Program) (env : Env) (e : Core.Expr) (a : BigInt) (h : Denotes p env e a) :

Denotes p env (Core.Expr.un Core.UnOp.abs e) a.abs

Used by

theorem

Lean2Js.Denote.denotes_ltBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.lt l r) (decide (a < b))

Used by

theorem

Lean2Js.Denote.denotes_leBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.le l r) (decide (a ≤ b))

Used by

theorem

Lean2Js.Denote.denotes_gtBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.gt l r) (decide (a > b))

Used by

theorem

Lean2Js.Denote.denotes_geBig

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : BigInt) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.ge l r) (decide (a ≥ b))

Used by

Equality, the short-circuiting connectives, and the two that pick a side #

&& and || do not go through applyBin at all: eval stops before the right operand when the left one settles the answer, so each has a lemma of its own. Lean's && stops too, but for a different reason — its right operand is a value, and there is nothing there to stop.

theorem

Lean2Js.Denote.denotes_eq

(p : Core.Program) (env : Env) (l r : Core.Expr) {β : Type} [Enc β] [BEq β] [Enc.EncBEq β] (a b : β) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.eq l r) (a == b)

Used by

theorem

Lean2Js.Denote.denotes_ne

(p : Core.Program) (env : Env) (l r : Core.Expr) {β : Type} [Enc β] [BEq β] [Enc.EncBEq β] (a b : β) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.ne l r) (a != b)

Used by

theorem

Lean2Js.Denote.denotes_and

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Bool) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.and l r) (a && b)

Used by

theorem

Lean2Js.Denote.denotes_or

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Bool) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.or l r) (a || b)

Used by

theorem

Lean2Js.Denote.denotes_min

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.min l r) (min a b)

Used by

theorem

Lean2Js.Denote.denotes_max

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : Int) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.max l r) (max a b)

Used by

theorem

Lean2Js.Denote.denotes_minU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.min l r) (min a b)

Used by

theorem

Lean2Js.Denote.denotes_maxU32

(p : Core.Program) (env : Env) (l r : Core.Expr) (a b : UInt32) (hl : Denotes p env l a) (hr : Denotes p env r b) :

Denotes p env (Core.Expr.bin Core.BinOp.max l r) (max a b)

Used by

def

Lean2Js.Denote.DenotesArgs

(p : Core.Program) (env : Env) :

List Core.Expr → List Value → Prop

The arguments of a call, paired with the values the callee's certificate is stated about. It is a list of Value rather than of encoded terms because a call's arguments need not share a type.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Denote.DenotesArgs p env [] [] = True
Lean2Js.Denote.DenotesArgs p env x✝¹ x✝ = False

Instances For

Used by

theorem

Lean2Js.Denote.denotesArgs_nil

(p : Core.Program) (env : Env) :

DenotesArgs p env [] []

Used by

theorem

Lean2Js.Denote.denotesArgs_cons

(p : Core.Program) (env : Env) (e : Core.Expr) (es : List Core.Expr) {α : Type} [Enc α] (t : α) (vs : List Value) (h : Denotes p env e t) (hs : DenotesArgs p env es vs) :

DenotesArgs p env (e :: es) (Enc.toValue t :: vs)

Used by

theorem

Lean2Js.Denote.denotes_call

(p : Core.Program) (env : Env) (fn : String) (args : List Core.Expr) (d : Core.Decl) (vs : List Value) {α : Type} [Enc α] (t : α) (hd : p.find? (calleeOf env fn) = some d) (hlen : d.params.length = vs.length) (hargs : DenotesArgs p env args vs) (hbody : Denotes p (bindParams d.params vs) d.body t) :

Denotes p env (Core.Expr.call fn args) t

Where one declaration's certificate cites another's. The callee runs on whatever fuel is left, which is why Denotes quantifies over it: a certificate stated at defaultFuel could not be used here.

Used by

A function that crossed the boundary #

No Lean function value knows which declaration it is, so there is no Enc for one and a function-typed argument is not a value the encoding carries. What crosses is the declaration's name, and what the receiver has to be told about the name is what a certificate says about a declaration. That claim is the hypothesis on the certificate of every declaration that takes a function.

def

Lean2Js.Denote.DenotesFn

(p : Core.Program) (name : String) {α β : Type} [Enc α] [Enc β] (f : α → β) :

The name a function-typed argument arrives as, together with what running it does.

Equations

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

Instances For

Used by

theorem

Lean2Js.Denote.denotesFn_of

(p : Core.Program) (name : String) (d : Core.Decl) {α β : Type} [Enc α] [Enc β] (f : α → β) (hd : p.find? name = some d) (hlen : d.params.length = 1) (hbody : ∀ (a : α), Denotes p (bindParams d.params [Enc.toValue a]) d.body (f a)) :

DenotesFn p name f

Used by

theorem

Lean2Js.Denote.denotesArgs_fnRef

(p : Core.Program) (env : Env) (name : String) (es : List Core.Expr) (vs : List Value) (hd : (p.find? name).isSome = true) (hs : DenotesArgs p env es vs) :

DenotesArgs p env (Core.Expr.fnRef name :: es) (Value.fn name :: vs)

Passing one on. The argument evaluates to the name rather than to an encoding, so this is where DenotesArgs stops being about Enc.

Used by

theorem

Lean2Js.Denote.denotes_callFn

(p : Core.Program) (env : Env) (fn name : String) (arg : Core.Expr) {α β : Type} [Enc α] [Enc β] (f : α → β) (a : α) (hlk : env.lookup? fn = some (Value.fn name)) (hf : DenotesFn p name f) (harg : Denotes p env arg a) :

Denotes p env (Core.Expr.call fn [arg]) (f a)

Calling one. The environment holds the name the caller passed, and calleeOf is what turns the parameter's own name into it.

Used by

Making a value of the author's own type, and taking one apart #

Building one goes through the program: eval looks the type up to find the field names to pair the arguments with, so a certificate that builds a value names the program the way a caller does. Reading a field does not — the encoding of the value already carries the field, whatever program it came from.

theorem

Lean2Js.Denote.denotes_ctor

(p : Core.Program) (env : Env) (typeName ctorName : String) (tyArgs : List Core.Ty) (args : List Core.Expr) (t : Core.TypeDef) (c : Core.CtorDef) (vs : List Value) {α : Type} [Enc α] (x : α) (ht : p.findType? typeName = some t) (hc : t.find? ctorName = some c) (hlen : c.fields.length = vs.length) (hargs : DenotesArgs p env args vs) (henc : Enc.toValue x = Value.obj ctorName ((List.map (fun (x : Core.Field) => x.name) c.fields).zip vs)) :

Denotes p env (Core.Expr.ctor typeName tyArgs ctorName args) x

Used by

theorem

Lean2Js.Denote.denotes_proj

(p : Core.Program) (env : Env) (e : Core.Expr) (field : String) {β : Type} [Enc β] (x : β) {α : Type} [Enc α] (t : α) (ctorName : String) (fields : List (String × Value)) (hx : Denotes p env e x) (henc : Enc.toValue x = Value.obj ctorName fields) (hf : Option.map (fun (x : String × Value) => x.snd) (List.find? (fun (x : String × Value) => x.fst == field) fields) = some (Enc.toValue t)) :

Denotes p env (e.proj field) t

Used by

`Option` and `Except` #

Both have a form of their own rather than being constructors of a declared type, so neither goes through the program. The side the term does not determine is carried as an annotation, which is why each lemma takes a Ty it never looks at.

theorem

Lean2Js.Denote.denotes_noneE

(p : Core.Program) (env : Env) (elem : Core.Ty) {β : Type} [Enc β] :

Denotes p env (Core.Expr.noneE elem) none

Used by

theorem

Lean2Js.Denote.denotes_someE

(p : Core.Program) (env : Env) (e : Core.Expr) {β : Type} [Enc β] (x : β) (hx : Denotes p env e x) :

Denotes p env e.someE (some x)

Used by

theorem

Lean2Js.Denote.denotes_okE

(p : Core.Program) (env : Env) (err : Core.Ty) (e : Core.Expr) {ε β : Type} [Enc ε] [Enc β] (x : β) (hx : Denotes p env e x) :

Denotes p env (Core.Expr.okE err e) (Except.ok x)

Used by

theorem

Lean2Js.Denote.denotes_errorE

(p : Core.Program) (env : Env) (ok : Core.Ty) (e : Core.Expr) {ε β : Type} [Enc ε] [Enc β] (x : ε) (hx : Denotes p env e x) :

Denotes p env (Core.Expr.errorE ok e) (Except.error x)

Used by

Walking a value of a type that names itself #

A fold evaluates its scrutinee and then walks it, and the walk is on the value rather than on the expression, so the step that reads it cannot be one lemma: T.fold is written per type and so is the theorem that the subset's walk computes it. This is everything around that theorem, which is what deriving Enc generates and hands over as hw. denotes_mapE's twin, with the walk abstracted where that one has evalMapItems_denotes.

theorem

Lean2Js.Denote.denotes_foldE

(p : Core.Program) (env : Env) (scrut : Core.Expr) (tn : String) (ta : List Core.Ty) (result : Core.Ty) (alts : List Core.Alt) {β : Type} [Enc β] (x : β) {α : Type} [Enc α] (t : α) (hs : Denotes p env scrut x) (hw : ∀ {f : Nat}, f ≤ defaultFuel → ∀ (v : Value), evalFold p f env tn ta alts (Enc.toValue x) = Except.ok v → v = Enc.toValue t) :

Denotes p env (scrut.foldE tn ta result alts) t

Used by