Skip to content

Lean2Js.Norm

Imports 2

The shapes of `Js.normTy`, `Js.outTy` and `Js.checkFields`, unfolded once each #

The shapes of Js.normTy, Js.outTy and Js.checkFields, unfolded once each.

All three are well-founded recursions over a value read by name, so none reduces by rfl and none is safe to hand to simp at a use site. The lemmas here are what the proofs about the entry check, its normalisation walk and the walk its result leaves by stand on.

theorem

Lean2Js.Js.lookupField_skip

(pre suf : List (String × JsValue)) (k : String) (h : ∀ (e : String × JsValue), e ∈ pre → e.fst ≠ k) :

lookupField (pre ++ suf) k = lookupField suf k

Used by

theorem

Lean2Js.Js.lookupField_head

(k : String) (v : JsValue) (rest : List (String × JsValue)) :

lookupField ((k, v) :: rest) k = some v

Used by

theorem

Lean2Js.Js.lookupField_cons_ne

{e : String × JsValue} {rest : List (String × JsValue)} {k : String} (h : e.fst ≠ k) :

lookupField (e :: rest) k = lookupField rest k

Used by

normTy and its companions are well-founded recursions, so each shape is unfolded once here rather than by simp at every use.

theorem

Lean2Js.Js.normList_nil

{env : TyEnv} (t : TyDesc) :

normList env [] t = []

Used by

theorem

Lean2Js.Js.normList_cons

{env : TyEnv} (x : JsValue) (xs : List JsValue) (t : TyDesc) :

normList env (x :: xs) t = normTy env x t :: normList env xs t

Used by

theorem

Lean2Js.Js.normEntries_nil

{env : TyEnv} (t : TyDesc) :

normEntries env [] t = []

Used by

theorem

Lean2Js.Js.normEntries_cons

{env : TyEnv} (k : String) (v : JsValue) (es : List (String × JsValue)) (t : TyDesc) :

normEntries env ((k, v) :: es) t = (k, normTy env v t) :: normEntries env es t

Used by

theorem

Lean2Js.Js.normFields_nil

{env : TyEnv} (fields : List (String × JsValue)) :

normFields env fields [] = []

Used by

theorem

Lean2Js.Js.normFields_cons

{env : TyEnv} {fields : List (String × JsValue)} {n : String} {t : TyDesc} {fs : List (String × TyDesc)} {v : JsValue} (h : lookupField fields n = some v) :

normFields env fields ((n, t) :: fs) = (n, normTy env v t) :: normFields env fields fs

Used by

theorem

Lean2Js.Js.normFields_none

{env : TyEnv} {fields : List (String × JsValue)} {n : String} {t : TyDesc} {fs : List (String × TyDesc)} (h : lookupField fields n = none) :

normFields env fields ((n, t) :: fs) = normFields env fields fs

Used by

theorem

Lean2Js.Js.normTy_bool

{env : TyEnv} (b : Bool) :

normTy env (JsValue.bool b) TyDesc.bool = JsValue.bool b

Used by

theorem

Lean2Js.Js.normTy_int53

{env : TyEnv} (i : Int) :

normTy env (JsValue.num i) TyDesc.int53 = JsValue.num i

Used by

theorem

Lean2Js.Js.normTy_uint32

{env : TyEnv} (i : Int) :

normTy env (JsValue.num i) TyDesc.uint32 = JsValue.num i

Used by

theorem

Lean2Js.Js.normTy_string

{env : TyEnv} (s : String) :

normTy env (JsValue.str s) TyDesc.string = JsValue.str s

Used by

theorem

Lean2Js.Js.normTy_bigint

{env : TyEnv} (i : Int) :

normTy env (JsValue.bigint i) TyDesc.bigint = JsValue.bigint i

Used by

theorem

Lean2Js.Js.normTy_array

{env : TyEnv} (xs : List JsValue) (t : TyDesc) :

normTy env (JsValue.arr xs) t.array = JsValue.arr (normList env xs t)

Used by

theorem

Lean2Js.Js.normTy_dict

{env : TyEnv} (es : List (String × JsValue)) (t : TyDesc) :

normTy env (JsValue.dict es) t.dict = JsValue.dict (normEntries env es t)

Used by

theorem

Lean2Js.Js.normTy_dictObj_dict

{env : TyEnv} (es : List (String × JsValue)) (t : TyDesc) :

normTy env (JsValue.dict es) t.dictObj = JsValue.dict (normEntries env es t)

Used by

theorem

Lean2Js.Js.normTy_dictObj_obj

{env : TyEnv} (fields : List (String × JsValue)) (t : TyDesc) :

normTy env (JsValue.obj fields) t.dictObj = JsValue.dict (Runtime.mapSetAll [] (normEntries env fields t))

Used by

theorem

Lean2Js.Js.normTy_none

{env : TyEnv} {fields : List (String × JsValue)} {t : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "none")) :

normTy env (JsValue.obj fields) t.option = JsValue.obj [("tag", JsValue.str "none")]

Used by

theorem

Lean2Js.Js.normTy_some

{env : TyEnv} {fields : List (String × JsValue)} {t : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "some")) :

normTy env (JsValue.obj fields) t.option = JsValue.obj (("tag", JsValue.str "some") :: normFields env fields [("value", t)])

Used by

theorem

Lean2Js.Js.normTy_ok

{env : TyEnv} {fields : List (String × JsValue)} {ok err : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "ok")) :

normTy env (JsValue.obj fields) (ok.result err) = JsValue.obj (("tag", JsValue.str "ok") :: normFields env fields [("value", ok)])

Used by

theorem

Lean2Js.Js.normTy_error

{env : TyEnv} {fields : List (String × JsValue)} {ok err : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "error")) :

normTy env (JsValue.obj fields) (ok.result err) = JsValue.obj (("tag", JsValue.str "error") :: normFields env fields [("error", err)])

Used by

theorem

Lean2Js.Js.normTy_ctors

{env : TyEnv} {fields : List (String × JsValue)} {key ctor : String} {alts : List (String × List (String × TyDesc))} {alt : String × List (String × TyDesc)} (htag : lookupField fields key = some (JsValue.str ctor)) (hf : List.find? (fun (x : String × List (String × TyDesc)) => x.fst == ctor) alts = some alt) :

normTy env (JsValue.obj fields) (TyDesc.ctors key alts) = JsValue.obj ((key, JsValue.str ctor) :: normFields env fields alt.snd)

Used by

theorem

Lean2Js.Js.normEntries_keys

{env : TyEnv} (es : List (String × JsValue)) (t : TyDesc) :

List.map (fun (x : String × JsValue) => x.fst) (normEntries env es t) = List.map (fun (x : String × JsValue) => x.fst) es

Used by

theorem

Lean2Js.Js.checkFields_nil

{env : TyEnv} (fields : List (String × JsValue)) :

checkFields env fields [] = true

Used by

theorem

Lean2Js.Js.checkFields_found

{env : TyEnv} {fields : List (String × JsValue)} {n : String} {t : TyDesc} {ts : List (String × TyDesc)} {v : JsValue} (h : lookupField fields n = some v) :

checkFields env fields ((n, t) :: ts) = (checkTy env v t && checkFields env fields ts)

Used by

theorem

Lean2Js.Js.checkFields_missing

{env : TyEnv} {fields : List (String × JsValue)} {n : String} {t : TyDesc} {ts : List (String × TyDesc)} (h : lookupField fields n = none) :

checkFields env fields ((n, t) :: ts) = false

Used by

theorem

Lean2Js.Js.lookupField_mem

{fields : List (String × JsValue)} {n : String} {v : JsValue} :

lookupField fields n = some v → (n, v) ∈ fields

Used by

theorem

Lean2Js.Js.lookupField_cases

(fields : List (String × JsValue)) (n : String) :

(∃ (v : JsValue ), lookupField fields n = some v) ∨ lookupField fields n = none

Used by

theorem

Lean2Js.Js.checkFields_cons

{env : TyEnv} {fields : List (String × JsValue)} {n : String} {t : TyDesc} {ts : List (String × TyDesc)} (h : checkFields env fields ((n, t) :: ts) = true) :

∃ (v : JsValue ), lookupField fields n = some v ∧ checkTy env v t = true ∧ checkFields env fields ts = true

Used by

theorem

Lean2Js.Js.checkFields_congr

{env : TyEnv} (ds : List (String × TyDesc)) (jfs jfs' : List (String × JsValue)) :

(∀ (n : String), n ∈ List.map (fun (x : String × TyDesc) => x.fst) ds → lookupField jfs n = lookupField jfs' n) → checkFields env jfs ds = checkFields env jfs' ds

checkFields reads only the keys the descriptor names, so two objects that answer those the same way answer the check the same way.

Used by

theorem

Lean2Js.Js.normFields_congr

{env : TyEnv} (ds : List (String × TyDesc)) (jfs jfs' : List (String × JsValue)) :

(∀ (n : String), n ∈ List.map (fun (x : String × TyDesc) => x.fst) ds → lookupField jfs n = lookupField jfs' n) → normFields env jfs ds = normFields env jfs' ds

normFields reads only the keys the descriptor names, so two objects that answer those the same way normalise the same way.

Used by

theorem

Lean2Js.Js.normFields_skip

{env : TyEnv} (e : String × JsValue) (rest : List (String × JsValue)) (ds : List (String × TyDesc)) (h : ∀ (n : String), n ∈ List.map (fun (x : String × TyDesc) => x.fst) ds → n ≠ e.fst) :

normFields env (e :: rest) ds = normFields env rest ds

Used by

theorem

Lean2Js.Js.checkFields_skip

{env : TyEnv} (e : String × JsValue) (rest : List (String × JsValue)) (ds : List (String × TyDesc)) (h : ∀ (n : String), n ∈ List.map (fun (x : String × TyDesc) => x.fst) ds → n ≠ e.fst) :

checkFields env (e :: rest) ds = checkFields env rest ds

Used by

theorem

Lean2Js.Js.namesOk_head

{key n : String} {t : TyDesc} {ts : List (String × TyDesc)} (h : namesOk key ((n, t) :: ts) = true) :

(∀ (m : String), m ∈ List.map (fun (x : String × TyDesc) => x.fst) ts → m ≠ n) ∧ namesOk key ts = true

Used by

theorem

Lean2Js.Js.namesOk_not_key

{key : String} {fs : List (String × TyDesc)} :

namesOk key fs = true → ∀ (m : String), m ∈ List.map (fun (x : String × TyDesc) => x.fst) fs → m ≠ key

Used by

theorem

Lean2Js.Js.altsOk_find

{depth : Nat} {alts : List (String × List (String × TyDesc))} {key ctor : String} {alt : String × List (String × TyDesc)} (h : altsOk depth key alts = true) (hf : List.find? (fun (x : String × List (String × TyDesc)) => x.fst == ctor) alts = some alt) :

namesOk key alt.snd = true ∧ fieldsOk depth alt.snd = true

Used by

The walk on the way out #

outTy is a well-founded recursion for the reason normTy is, so its shapes are unfolded once here too. Every one of them but outTy_dictObj says the same thing its normTy twin says.

theorem

Lean2Js.Js.outList_nil

{env : TyEnv} (t : TyDesc) :

outList env [] t = []

Used by

theorem

Lean2Js.Js.outList_cons

{env : TyEnv} (x : JsValue) (xs : List JsValue) (t : TyDesc) :

outList env (x :: xs) t = outTy env x t :: outList env xs t

Used by

theorem

Lean2Js.Js.outEntries_nil

{env : TyEnv} (t : TyDesc) :

outEntries env [] t = []

Used by

theorem

Lean2Js.Js.outEntries_cons

{env : TyEnv} (k : String) (v : JsValue) (es : List (String × JsValue)) (t : TyDesc) :

outEntries env ((k, v) :: es) t = (k, outTy env v t) :: outEntries env es t

Used by

theorem

Lean2Js.Js.outFields_nil

{env : TyEnv} (fields : List (String × JsValue)) :

outFields env fields [] = []

Used by

theorem

Lean2Js.Js.outFields_cons

{env : TyEnv} {fields : List (String × JsValue)} {n : String} {t : TyDesc} {fs : List (String × TyDesc)} {v : JsValue} (h : lookupField fields n = some v) :

outFields env fields ((n, t) :: fs) = (n, outTy env v t) :: outFields env fields fs

Used by

theorem

Lean2Js.Js.outFields_none

{env : TyEnv} {fields : List (String × JsValue)} {n : String} {t : TyDesc} {fs : List (String × TyDesc)} (h : lookupField fields n = none) :

outFields env fields ((n, t) :: fs) = outFields env fields fs

Used by

theorem

Lean2Js.Js.outTy_bool

{env : TyEnv} (b : Bool) :

outTy env (JsValue.bool b) TyDesc.bool = JsValue.bool b

Used by

theorem

Lean2Js.Js.outTy_int53

{env : TyEnv} (i : Int) :

outTy env (JsValue.num i) TyDesc.int53 = JsValue.num i

Used by

theorem

Lean2Js.Js.outTy_uint32

{env : TyEnv} (i : Int) :

outTy env (JsValue.num i) TyDesc.uint32 = JsValue.num i

Used by

theorem

Lean2Js.Js.outTy_string

{env : TyEnv} (s : String) :

outTy env (JsValue.str s) TyDesc.string = JsValue.str s

Used by

theorem

Lean2Js.Js.outTy_bigint

{env : TyEnv} (i : Int) :

outTy env (JsValue.bigint i) TyDesc.bigint = JsValue.bigint i

Used by

theorem

Lean2Js.Js.outTy_array

{env : TyEnv} (xs : List JsValue) (t : TyDesc) :

outTy env (JsValue.arr xs) t.array = JsValue.arr (outList env xs t)

Used by

theorem

Lean2Js.Js.outTy_dict

{env : TyEnv} (es : List (String × JsValue)) (t : TyDesc) :

outTy env (JsValue.dict es) t.dict = JsValue.dict (outEntries env es t)

Used by

theorem

Lean2Js.Js.outTy_dictObj

{env : TyEnv} (es : List (String × JsValue)) (t : TyDesc) :

outTy env (JsValue.dict es) t.dictObj = JsValue.obj (outEntries env es t)

The one node the two walks part at: a Map is handed back as the object its declared type says it crosses as.

Used by

theorem

Lean2Js.Js.outTy_dictObj_obj

{env : TyEnv} (fields : List (String × JsValue)) (t : TyDesc) :

outTy env (JsValue.obj fields) t.dictObj = JsValue.obj fields

A value that is already an object at a dictObj is handed back as it stands. Inside the module a dictionary is a Map whatever it crosses as, so this is a shape a body does not produce; giving it the identity rather than a walk is what keeps the branch out of the helper's proof.

Used by

theorem

Lean2Js.Js.outTy_none

{env : TyEnv} {fields : List (String × JsValue)} {t : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "none")) :

outTy env (JsValue.obj fields) t.option = JsValue.obj [("tag", JsValue.str "none")]

Used by

theorem

Lean2Js.Js.outTy_some

{env : TyEnv} {fields : List (String × JsValue)} {t : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "some")) :

outTy env (JsValue.obj fields) t.option = JsValue.obj (("tag", JsValue.str "some") :: outFields env fields [("value", t)])

Used by

theorem

Lean2Js.Js.outTy_ok

{env : TyEnv} {fields : List (String × JsValue)} {ok err : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "ok")) :

outTy env (JsValue.obj fields) (ok.result err) = JsValue.obj (("tag", JsValue.str "ok") :: outFields env fields [("value", ok)])

Used by

theorem

Lean2Js.Js.outTy_error

{env : TyEnv} {fields : List (String × JsValue)} {ok err : TyDesc} (h : lookupField fields "tag" = some (JsValue.str "error")) :

outTy env (JsValue.obj fields) (ok.result err) = JsValue.obj (("tag", JsValue.str "error") :: outFields env fields [("error", err)])

Used by

theorem

Lean2Js.Js.outTy_ctors

{env : TyEnv} {fields : List (String × JsValue)} {key ctor : String} {alts : List (String × List (String × TyDesc))} {alt : String × List (String × TyDesc)} (htag : lookupField fields key = some (JsValue.str ctor)) (hf : List.find? (fun (x : String × List (String × TyDesc)) => x.fst == ctor) alts = some alt) :

outTy env (JsValue.obj fields) (TyDesc.ctors key alts) = JsValue.obj ((key, JsValue.str ctor) :: outFields env fields alt.snd)

Used by

theorem

Lean2Js.Js.outEntries_keys

{env : TyEnv} (es : List (String × JsValue)) (t : TyDesc) :

List.map (fun (x : String × JsValue) => x.fst) (outEntries env es t) = List.map (fun (x : String × JsValue) => x.fst) es

Used by

theorem

Lean2Js.Js.outFields_congr

{env : TyEnv} (ds : List (String × TyDesc)) (jfs jfs' : List (String × JsValue)) :

(∀ (n : String), n ∈ List.map (fun (x : String × TyDesc) => x.fst) ds → lookupField jfs n = lookupField jfs' n) → outFields env jfs ds = outFields env jfs' ds

outFields reads only the keys the descriptor names, so two objects that answer those the same way leave the same way.

Used by

theorem

Lean2Js.Js.outFields_skip

{env : TyEnv} (e : String × JsValue) (rest : List (String × JsValue)) (ds : List (String × TyDesc)) (h : ∀ (n : String), n ∈ List.map (fun (x : String × TyDesc) => x.fst) ds → n ≠ e.fst) :

outFields env (e :: rest) ds = outFields env rest ds

Used by

Where the two walks are one walk #

A return type reaching no dictObj is handed back exactly as it came, so its entry emits no walk out and the package it is compiled into is byte-for-byte what it was before a dictionary could cross as a plain object. That is what the lemma below is for.

theorem

Lean2Js.Js.outTy_eq_normTy

{env : TyEnv} {v : JsValue} {d : TyDesc} (he : envNoDictObj env = true) (hd : descNoDictObj d = true) :

outTy env v d = normTy env v d

Where nothing the descriptor reaches crosses the boundary as a plain object, the walk out is the walk in.

Used by