Properties of Lambda operational semantics #
This module contains normal-form, closure-lifting, substitution, factory-call,
and metadata-insensitivity lemmas used to reason about Step and StepStar.
Evaluator-specific top-level theorems live in LExprEvalProps and
LExprEvalSound.
theorem
Lambda.LExpr.mkHave_beta
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
(F : Factory Tbase)
(rf : Env Tbase)
(m : Tbase.Metadata)
(name : String)
(ty : Option LMonoTy)
(value body : LExpr Tbase.mono)
:
Beta-reduction behavior of have-bindings: mkHave m name ty value body
steps to body with the bound variable substituted by value.
theorem
Lambda.step_const_stuck
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
{m : Tbase.mono.base.Metadata}
(F : Factory Tbase)
(r : Env Tbase)
(x : LConst)
(e : LExpr Tbase.mono)
:
¬Step F r (LExpr.const m x) e
theorem
Lambda.substK_eraseMetadata_congr₂
{Tbase : LExprParams}
(e₁ e₂ : LExpr Tbase.mono)
(k : Nat)
(s₁ s₂ : Tbase.Metadata → LExpr Tbase.mono)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
(h_s : ∀ (m₁ m₂ : Tbase.Metadata), (s₁ m₁).eraseMetadata = (s₂ m₂).eraseMetadata)
:
theorem
Lambda.getLFuncCall_mkApp_op
{Tbase : LExprParams}
(m_app m_op : Tbase.Metadata)
(name : Identifier Tbase.IDMeta)
(ty : Option LMonoTy)
(args : List (LExpr Tbase.mono))
:
theorem
Lambda.callOfLFunc_mkApp_op
{Tbase : LExprParams}
(F : Factory Tbase)
(m_app : Tbase.Metadata)
(op_expr : LExpr Tbase.mono)
(args args' : List (LExpr Tbase.mono))
(lfunc : LFunc Tbase)
(h_op :
∃ (m : Tbase.mono.base.Metadata), ∃ (name : Identifier Tbase.mono.base.IDMeta), ∃ (ty : Option Tbase.mono.TypeType), op_expr = LExpr.op m name ty)
(h_call : F.callOfLFunc (LExpr.mkApp m_app op_expr args) = some (op_expr, args, lfunc))
(h_len : args'.length = args.length)
:
theorem
Lambda.callOfLFunc_app_arg_mem
{Tbase : LExprParams}
(F : Factory Tbase)
(e1 e2 : LExpr Tbase.mono)
(m : Tbase.Metadata)
(op : LExpr Tbase.mono)
(args : List (LExpr Tbase.mono))
(f : LFunc Tbase)
(aPA : Bool)
(h : F.callOfLFunc (LExpr.app m e1 e2) aPA = some (op, args, f))
:
If callOfLFunc (with either allowPartialApp) recognizes .app m e1 e2 as a call, its
argument e2 is among the call's arguments (the last one).
theorem
Lambda.isValue_app_left
{Tbase : LExprParams}
(F : Factory Tbase)
(m : Tbase.Metadata)
(e1 e2 : LExpr Tbase.mono)
(hc : LExpr.isValue F (LExpr.app m e1 e2) = true)
:
The function part e1 of an application .app m e1 e2 that is a value is a value.
theorem
Lambda.isValue_getVars_nil
{Tbase : LExprParams}
(F : Factory Tbase)
(e : LExpr Tbase.mono)
(hc : LExpr.isValue F e = true)
:
Values have no free variables.
theorem
Lambda.value_not_step
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
(F : Factory Tbase)
(rf : Env Tbase)
(e : LExpr Tbase.mono)
(hWF : FactoryWF F)
(hc : LExpr.isValue F e = true)
(e' : LExpr Tbase.mono)
:
theorem
Lambda.eraseMetadata_app_congr
{Tbase : LExprParams}
{m₁ m₂ : Tbase.Metadata}
{f₁ f₂ a₁ a₂ : LExpr Tbase.mono}
(hf : f₁.eraseMetadata = f₂.eraseMetadata)
(ha : a₁.eraseMetadata = a₂.eraseMetadata)
:
theorem
Lambda.StepStar_getLFuncCall_args
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
{F : Factory Tbase}
{rf : Env Tbase}
(e op : LExpr Tbase.mono)
(args args' : List (LExpr Tbase.mono))
(h_get : getLFuncCall e = (op, args))
(h_len : args.length = args'.length)
(h_steps : ∀ (i : Nat) (hi : i < args.length), StepStar F rf (args.get ⟨i, hi⟩) (args'.get ⟨i, ⋯⟩))
:
∃ (e' : LExpr Tbase.mono), StepStar F rf e e' ∧ e'.eraseMetadata = LExpr.mkApp () op.eraseMetadata (List.map LExpr.eraseMetadata args')
theorem
Lambda.getLFuncCall_eraseMetadata_congr
{Tbase : LExprParams}
(e₁ e₂ : LExpr Tbase.mono)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
:
(getLFuncCall e₁).fst.eraseMetadata = (getLFuncCall e₂).fst.eraseMetadata ∧ List.map LExpr.eraseMetadata (getLFuncCall e₁).snd = List.map LExpr.eraseMetadata (getLFuncCall e₂).snd
theorem
Lambda.callOfLFunc_eraseMetadata_congr
{Tbase : LExprParams}
(F : Factory Tbase)
(e₁ e₂ : LExpr Tbase.mono)
(aPA : Bool)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
:
match F.callOfLFunc e₁ aPA, F.callOfLFunc e₂ aPA with
| some (op₁, args₁, f₁), some (op₂, args₂, f₂) =>
f₁ = f₂ ∧ List.map LExpr.eraseMetadata args₁ = List.map LExpr.eraseMetadata args₂ ∧ op₁.eraseMetadata = op₂.eraseMetadata
| none, none => True
| x, x_1 => False
theorem
Lambda.callOfLFunc_none_of_eraseMetadata_eq
{Tbase : LExprParams}
(F : Factory Tbase)
(e₁ e₂ : LExpr Tbase.mono)
(aPA : Bool)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
(h_none : F.callOfLFunc e₁ aPA = none)
:
theorem
Lambda.callOfLFunc_some_of_eraseMetadata_eq
{Tbase : LExprParams}
(F : Factory Tbase)
(e₁ e₂ : LExpr Tbase.mono)
(aPA : Bool)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
(op₁ : LExpr Tbase.mono)
(args₁ : List (LExpr Tbase.mono))
(f : LFunc Tbase)
(h_some : F.callOfLFunc e₁ aPA = some (op₁, args₁, f))
:
theorem
Lambda.eql_eraseMetadata_eq
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
(F : Factory Tbase)
(e₁ e₂ e₁' e₂' : LExpr Tbase.mono)
(h₁ : e₁.eraseMetadata = e₁'.eraseMetadata)
(h₂ : e₂.eraseMetadata = e₂'.eraseMetadata)
:
theorem
Lambda.step_to_const_via_IH
{Tbase : LExprParams}
[DecidableEq Tbase.Metadata]
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
[Std.ToFormat Tbase.Metadata]
[Std.ToFormat Tbase.IDMeta]
[Traceable LExpr.EvalProvenance Tbase.Metadata]
(F : Factory Tbase)
(env : Env Tbase)
(e e' : LExpr Tbase.mono)
(mc : Tbase.Metadata)
(c : LConst)
(hstep : StepStar F env e e')
(h_eM : e'.eraseMetadata = (LExpr.const mc c).eraseMetadata)
:
theorem
Lambda.StepStar_to_substFvarsFromEnv_abs
{Tbase : LExprParams}
[DecidableEq Tbase.Metadata]
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
[Std.ToFormat Tbase.Metadata]
[Std.ToFormat Tbase.IDMeta]
[Traceable LExpr.EvalProvenance Tbase.Metadata]
(F : Factory Tbase)
(env : Env Tbase)
(m : Tbase.Metadata)
(name : String)
(ty : Option LMonoTy)
(body : LExpr Tbase.mono)
:
StepStar F env (LExpr.abs m name ty body) (LExpr.substFvarsFromEnv env (LExpr.abs m name ty body))
theorem
Lambda.StepStar_to_substFvarsFromEnv_quant
{Tbase : LExprParams}
[DecidableEq Tbase.Metadata]
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
[Std.ToFormat Tbase.Metadata]
[Std.ToFormat Tbase.IDMeta]
[Traceable LExpr.EvalProvenance Tbase.Metadata]
(F : Factory Tbase)
(env : Env Tbase)
(m : Tbase.Metadata)
(qk : QuantifierKind)
(name : String)
(ty : Option LMonoTy)
(tr body : LExpr Tbase.mono)
:
StepStar F env (LExpr.quant m qk name ty tr body) (LExpr.substFvarsFromEnv env (LExpr.quant m qk name ty tr body))
theorem
Lambda.StepStar_to_substFvarsFromEnv
{Tbase : LExprParams}
[DecidableEq Tbase.Metadata]
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
[Std.ToFormat Tbase.Metadata]
[Std.ToFormat Tbase.IDMeta]
[Traceable LExpr.EvalProvenance Tbase.Metadata]
(F : Factory Tbase)
(env : Env Tbase)
(e : LExpr Tbase.mono)
:
StepStar F env e (LExpr.substFvarsFromEnv env e)
Every expression steps to its free-variable substitution from the environment.
theorem
Lambda.isValue_eraseMetadata_eq
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
(F : Factory Tbase)
(e₁ e₂ : LExpr Tbase.mono)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
:
theorem
Lambda.isConstrApp_eraseMetadata_eq
{Tbase : LExprParams}
(F : Factory Tbase)
(e₁ e₂ : LExpr Tbase.mono)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
:
theorem
Lambda.isInlineArg_eraseMetadata_eq
{Tbase : LExprParams}
(F : Factory Tbase)
(e₁ e₂ : LExpr Tbase.mono)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
:
Whether an expression is an inlineIfAllValues unfolding argument (isInlineArg)
depends only on the expression with its metadata erased.
theorem
Lambda.substFvarsLifting_zip_eraseMetadata_congr
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
(e : LExpr Tbase.mono)
(keys : List Tbase.Identifier)
(vals₁ vals₂ : List (LExpr Tbase.mono))
(h_vals : List.map LExpr.eraseMetadata vals₁ = List.map LExpr.eraseMetadata vals₂)
:
(e.substFvarsLifting (keys.zip vals₁)).eraseMetadata = (e.substFvarsLifting (keys.zip vals₂)).eraseMetadata
theorem
Lambda.evalCore_eraseMetadata_congr
{Tbase : LExprParams}
[DecidableEq Tbase.IDMeta]
[Inhabited Tbase.IDMeta]
[Std.ToFormat Tbase.Metadata]
[Std.ToFormat Tbase.IDMeta]
[Traceable LExpr.EvalProvenance Tbase.Metadata]
(n' : Nat)
(F : Factory Tbase)
(env : Env Tbase)
(e₁ e₂ : LExpr Tbase.mono)
(h_eM : e₁.eraseMetadata = e₂.eraseMetadata)
(ih :
∀ (e₁ e₂ : LExpr Tbase.mono),
e₁.eraseMetadata = e₂.eraseMetadata →
(LExpr.eval n' F env e₁).fst.eraseMetadata = (LExpr.eval n' F env e₂).fst.eraseMetadata)
:
theorem
Lambda.computeTypeSubst_eraseMetadata_congr
{T : LExprParams}
(fn : LFunc T)
(op₁ op₂ : LExpr T.mono)
(args₁ args₂ : List (LExpr T.mono))
(h_op : op₁.eraseMetadata = op₂.eraseMetadata)
(h_args : List.map LExpr.eraseMetadata args₁ = List.map LExpr.eraseMetadata args₂)
: