You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
inductive Value : Type where
    | unit : Value
    | const : Constant → Value
    | constr_app : (constr : Name) → (args_rev : List Value) → Value
    | closure : (env : List Object) → (value : Expr) → Value
    deriving Inhabited

inductive Object : Type where
    | value : Value → Object
    | delayed : (env : List Object) → Expr → Object
    deriving Inhabited

abbrev Env : Type := List Object

abbrev cons_value (v : Value) (env : Env) : Env := Object.value v :: env

def eval_binop_int (op : BinaryOp) (i₁ i₂ : Int) : Int :=
  match op with
  | BinaryOp.add_int => i₁ + i₂
  | BinaryOp.sub_int => i₁ - i₂
  | BinaryOp.mul_int => i₁ * i₂
  | BinaryOp.div_int => i₁ / i₂

@[aesop unsafe constructors]
inductive Eval : Env → Expr → Value → Prop where
  | var {env name idx val} :
    env[idx]? = some (Object.value val) →
    Eval env (Expr.var name idx) val
  | var_rec {env name idx env' expr val} :
    env[idx]? = some (Object.delayed env' expr) →
    Eval env' expr val →
    Eval env (Expr.var name idx) val
  | unit {env} :
    Eval env Expr.unit Value.unit
  | const {env c} :
    Eval env (Expr.const c) (Value.const c)
  | constr {env name} :
    Eval env (Expr.constr name) (Value.constr_app name [])
  | app {env env' f body arg val val'} :
    Eval env f (Value.closure env' body) →
    Eval env arg val →
    Eval (val ∷ env') body val' →
    Eval env (Expr.app f arg) val'
  | constr_app {env ctr ctr_name ctr_args_rev arg val} :
    Eval env ctr (Value.constr_app ctr_name ctr_args_rev) →
    Eval env arg val →
    Eval env (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev))
  | binop {env op arg₁ arg₂ val₁ val₂} :
    Eval env arg₁ (Value.const (Constant.int val₁)) →
    Eval env arg₂ (Value.const (Constant.int val₂)) →
    Eval env (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂)))
  | lambda {env name body} :
    Eval env (Expr.lambda name body) (Value.closure env body)
  | save {env name value body val val'} :
    Eval env value val →
    Eval (val ∷ env) body val' →
    Eval env (Expr.save name value body) val'
  | branch_matches {env name args_rev body val} :
    Eval (args_rev.map Object.value ++ env) body val →
    Eval (Value.constr_app name args_rev ∷ env) (Expr.branch name _ body _) val
  | branch_fails {env name name' args_rev next val} :
    name ≠ name' →
    Eval (Value.constr_app name args_rev ∷ env) next val →
    Eval (Value.constr_app name args_rev ∷ env) (Expr.branch name' _ _ next) val
  | recur {env name body val} :
    Eval (Object.delayed env (Expr.recur name body) :: env) body val →
    Eval env (Expr.recur name body) val

inductive Context : Type where
  | hole : Context
  | app_left : Context → Expr → Context
  | app_right : Expr → Context → Context
  | constr_app_left : Context → Expr → Context
  | constr_app_right : Expr → Context → Context
  | binop_left : (oper : BinaryOp) → (arg₁ : Context) → (arg₂ : Expr) → Context
  | binop_right : (oper : BinaryOp) → (arg₁ : Expr) → (arg₂ : Context) → Context
  | lambda : (var_name : String) → (body : Context) → Context
  | save_left : (var_name : String) → (value : Context) → (body : Expr) → Context
  | save_right : (var_name : String) → (value : Expr) → (body : Context) → Context
  | branch_left : (constr : Name) → (var_names : List Name) → (body : Context) → (next : Expr) → Context
  | branch_right : (constr : Name) → (var_names : List Name) → (body : Expr) → (next : Context) → Context
  | recur : (var_name : Name) → (ctx : Context) → Context
  deriving Inhabited, BEq

abbrev Name : Type := String

inductive Constant : Type where
  | int : Int → Constant
  | string : String → Constant
  deriving Inhabited, BEq, DecidableEq

inductive BinaryOp : Type where
  | add_int : BinaryOp
  | sub_int : BinaryOp
  | mul_int : BinaryOp
  | div_int : BinaryOp
  deriving Inhabited, BEq, DecidableEq

inductive Expr : Type where
  | var : (name : String) → (index : Nat) → Expr
  | unit : Expr
  | const : Constant → Expr
  | constr : Name → Expr
  | app : Expr → Expr → Expr
  | constr_app : Expr → Expr → Expr
  | binop : (oper : BinaryOp) → (arg₁ arg₂ : Expr) → Expr
  | lambda : (var_name : String) → (body : Expr) → Expr
  | save : (var_name : String) → (value : Expr) → (body : Expr) → Expr
  | branch : (constr : Name) → (var_names : List Name) → (body : Expr) → (next : Expr) → Expr
  | recur : (var_name : Name) → (body : Expr) → Expr
  | fail : Expr
  deriving Inhabited, BEq, DecidableEq

def Expr.Equiv.Contextual (e₁ e₂ : Expr) : Prop :=
  e₁ ≲ᶜ e₂ ∧ e₂ ≲ᶜ e₁

def Eval.Defined (env : Env) (e : Expr) : Prop :=
  ∃ v, env ⊢ e ↦ v

Lean.Syntax.mkStrLit in Init.Meta.Defs

Monad in Init.Prelude

def mkConstrApp {m} [Monad m] [MonadRef m] (name : Ident) (es : TSyntaxArray `expr) : m Syntax := do
  let info ← Lean.MonadRef.mkInfoFromRefPos
  pure $
    Lean.Syntax.node3 info `Juvix.Core.Main.Syntax.term_of_expr
      (Lean.Syntax.atom info "⟪")
      (Lean.Syntax.node2 info `Juvix.Core.Main.Syntax.expr_constr_app
        name
        (Lean.Syntax.node info `null es))
      (Lean.Syntax.atom info "⟫")

def Env.Approx : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ Object.Approx

List.toArray in Init.Prelude

Lean.MonadQuotation in Init.Prelude

String in Init.Prelude

Lean.Name.mkSimple in Init.Prelude

def Value.Equiv (v v' : Value) : Prop :=
  v ≲ᵥ v' ∧ v' ≲ᵥ v

instance : Coe Syntax (TSyntax `expr) where
  coe s := ⟨s⟩

List.map in Init.Prelude

def Context.Indexed.Preserved (k : Nat) : Prop :=
  ∀ n m,
    n + m < k →
    ∀ e₁ e₂,
      e₁ ≲'(n + m) e₂ → ∀ (C : Context) env₁ env₂ v₁,
      env₁ ≲ₑ'(n + m) env₂ →
      env₁ ⊢ C.subst e₁ ↦(n) v₁ →
      ∃ v₂, env₂ ⊢ C.subst e₂ ↦ v₂ ∧ v₁ ≲ᵥ(m) v₂

def unfoldListLit (node : Syntax) : Option (List String) :=
  match node with
  | (Lean.Syntax.node _ _ args0) =>
    match args0 with
    | #[Lean.Syntax.atom _ "[", node', Lean.Syntax.atom _ "]"] =>
      match node' with
      | (Lean.Syntax.node _ _ args) =>
        let rec go : List Syntax → List String → Option (List String)
          | [], acc => some acc.reverse
          | [ ns ], acc =>
            match ns with
            | `($s:str) =>
              some (s.getString :: acc).reverse
            | _ => none
          | ( ns :: Lean.Syntax.atom _ "," :: xs), acc =>
            match ns with
            | `($s:str) =>
                go xs (s.getString :: acc)
            | _ => none
          | _, _ => none
        go args.toList []
      | _ => none
    | _ => none
  | _ => none

@[app_unexpander Expr.fail]
def unexpandFail : Unexpander
  | `($_bot) => `(⟪⊥⟫)

List in Init.Prelude

def Env.Approx.Indexed' (n : Nat) : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ (Object.Approx.Indexed' n)

def Expr.Approx.Indexed' (n : Nat) (e₁ e₂ : Expr) : Prop :=
  (∀ n₁ n₂ v₁, n₁ + n₂ ≤ n →
    ∀ env₁ env₂, env₁ ≲ₑ'(n₁ + n₂) env₂ → env₁ ⊢ e₁ ↦(n₁) v₁ → ∃ v₂, env₂ ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ(n₂) v₂)

inductive Object.Approx.Indexed' (n : Nat) : Object → Object → Prop where
  | value {v₁ v₂} :
    v₁ ≲ᵥ(n) v₂ →
    Object.Approx.Indexed' n (Object.value v₁) (Object.value v₂)
  | delayed {env₁ env₂ e₁ e₂} :
    e₁ ≲(n)⟨env₁, env₂⟩ e₂ →
    Object.Approx.Indexed' n (Object.delayed env₁ e₁) (Object.delayed env₂ e₂)
  | delayed_eq {env₁ env₂ e} :
    List.Forall₂ (Object.Approx.Indexed' n) env₁ env₂ →
    Object.Approx.Indexed' n (Object.delayed env₁ e) (Object.delayed env₂ e)

def Expr.Equiv.Param (env₁ env₂ : Env) (e₁ e₂ : Expr) : Prop :=
  e₁ ≲⟨env₁, env₂⟩ e₂ ∧ e₂ ≲⟨env₂, env₁⟩ e₁

def Expr.Approx.Param.Indexed (n : Nat) (env₁ env₂ : Env) (e₁ e₂ : Expr) : Prop :=
  (∀ n₁ n₂ v₁, n₁ + n₂ ≤ n → env₁ ⊢ e₁ ↦(n₁) v₁ → ∃ v₂, env₂ ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ(n₂) v₂)

Prod in Init.Prelude

List.cons in Init.Prelude

Transitive in Mathlib.Order.Defs.Unbundled

@[delab app.Juvix.Core.Main.Expr.binop]
def delabBinop : Delab := do
  let e ← getExpr
  guard $ e.isAppOfArity' `Juvix.Core.Main.Expr.binop 3
  match e.getAppArgs' with
  | #[Lean.Expr.const op _, e₁, e₂] =>
    let e₁' ← match ← delab e₁ with
      | `(⟪$e'⟫) => pure e'
      | _ => failure
    let e₂' ← match ← delab e₂ with
      | `(⟪$e'⟫) => pure e'
      | _ => failure
    match op with
    | `Juvix.Core.Main.BinaryOp.add_int => `(⟪$e₁' + $e₂'⟫)
    | `Juvix.Core.Main.BinaryOp.sub_int => `(⟪$e₁' - $e₂'⟫)
    | `Juvix.Core.Main.BinaryOp.mul_int => `(⟪$e₁' * $e₂'⟫)
    | `Juvix.Core.Main.BinaryOp.div_int => `(⟪$e₁' / $e₂'⟫)
    | _ => failure
  | _ => failure

def Object.Equiv (o o' : Object) : Prop :=
  o ≲ₒ o' ∧ o' ≲ₒ o

List.Forall₂.nil in Batteries.Data.List.Basic

Lean.Expr in Lean.Expr

partial def eval (env : Env) : Expr -> Value
  | Expr.var _ idx => match env[idx]! with
    | Object.value val => val
    | Object.delayed env' expr => eval env' expr
  | Expr.unit => Value.unit
  | Expr.const c => Value.const c
  | Expr.constr name => Value.constr_app name []
  | Expr.app f arg => match eval env f with
    | Value.closure env' body => eval (eval env arg ∷ env') body
    | _ => panic! "expected closure"
  | Expr.constr_app ctr arg => match eval env ctr with
    | Value.constr_app ctr_name ctr_args_rev => Value.constr_app ctr_name (eval env arg :: ctr_args_rev)
    | _ => panic! "expected constructor application"
  | Expr.binop op arg₁ arg₂ => match eval env arg₁, eval env arg₂ with
    | Value.const (Constant.int val₁), Value.const (Constant.int val₂) =>
      Value.const (Constant.int (eval_binop_int op val₁ val₂))
    | _, _ => panic! "expected integer constants"
  | Expr.lambda _ body => Value.closure env body
  | Expr.save _ value body => eval (eval env value ∷ env) body
  | Expr.branch name _ body next => match env with
    | Object.value (Value.constr_app name' args_rev) :: env' =>
      if name = name' then
        eval (args_rev.map Object.value ++ env') body
      else
        eval env next
    | _ => panic! "expected constructor application"
  | Expr.recur name body =>
    eval (Object.delayed env (Expr.recur name body) :: env) body
  | Expr.fail => panic! "evaluation failed"

@[app_unexpander Expr.lambda]
def unexpandLambda : Unexpander
  | `($_lambda $s:str ⟪λ $ss:ident* . $e:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪λ $name $ss* . $e⟫)
  | `($_lambda $s:str ⟪$e⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪λ $name . $e⟫)
  | _ => throw ()

List.nil in Init.Prelude

@[app_unexpander Expr.app]
def unexpandApp : Unexpander
  | `($_app ⟪$e₁⟫ ⟪$e₂⟫) => `(⟪$e₁ $e₂⟫)
  | _ => throw ()

@[app_unexpander Expr.unit]
def unexpandUnit : Unexpander
  | `($_unit) => `(⟪υ⟫)

closure in Mathlib.Topology.Defs.Basic

List.Forall₂.cons in Batteries.Data.List.Basic

def Expr.Approx.Param (env₁ env₂ : Env) (e₁ e₂ : Expr) : Prop :=
  (∀ v₁, env₁ ⊢ e₁ ↦ v₁ → ∃ v₂, env₂ ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂)

Lean.Expr.const in Lean.Expr

List.Forall₂ in Batteries.Data.List.Basic

Lean.TSyntax in Init.Prelude

@[app_unexpander Expr.const]
def unexpandConst : Unexpander
  | `($_const $x) =>
    match x with
    | `($_ $n:num) => `(⟪$n⟫)
    | `($_ $s:str) => `(⟪$s⟫)
    | _ => throw ()
  | _ => throw ()

guard in Init.Control.Basic

@[app_unexpander Expr.constr_app]
def unexpandConstrApp : Unexpander
  | `($_constr_app ⟪ $s ⟫ ⟪$e⟫) => `(⟪ $s $e⟫)
  | `($_constr_app ⟪ $s:ident $es* ⟫ ⟪$e⟫) => mkConstrApp s (es.push e)
  | _ => throw ()

Lean.Syntax.atom in Init.Prelude

def Expr.Equiv (e₁ e₂ : Expr) : Prop :=
  e₁ ≲ e₂ ∧ e₂ ≲ e₁

reduceCtorEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

def Env.Equiv : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ Object.Equiv

DecidableEq in Init.Prelude

@[category_parenthesizer expr]
def expr.parenthesizer : CategoryParenthesizer := term.parenthesizer

def Value.Approx (v v' : Value) : Prop :=
  ∀ n, v ≲ᵥ(n) v'

Inhabited in Init.Prelude

Lean.MonadRef.mkInfoFromRefPos in Init.Prelude

@[app_unexpander Expr.recur]
def unexpandRecur : Unexpander
  | `($_recur $s:str ⟪$b:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪rec $name $b⟫)
  | _ => throw ()

def mkLambdas {m} [Monad m] [MonadQuotation m] (ss : TSyntaxArray `ident) (e : TSyntax `expr) : m (TSyntax `term) := do
  let body ← `(⟪ $e ⟫)
  ss.foldrM (fun s acc => `(Expr.lambda $(Lean.Syntax.mkStrLit s.getId.toString) $acc)) body

Coe in Init.Coe

Lean.Syntax.node2 in Init.Prelude

@[simp]
def Context.subst (C : Context) (e : Expr) : Expr :=
  match C with
  | Context.hole => e
  | Context.app_left C' e' => Expr.app (C'.subst e) e'
  | Context.app_right e' C' => Expr.app e' (C'.subst e)
  | Context.constr_app_left C' e' => Expr.constr_app (C'.subst e) e'
  | Context.constr_app_right e' C' => Expr.constr_app e' (C'.subst e)
  | Context.binop_left oper C₁ e₂ => Expr.binop oper (C₁.subst e) e₂
  | Context.binop_right oper e₁ C₂ => Expr.binop oper e₁ (C₂.subst e)
  | Context.lambda s C' => Expr.lambda s (C'.subst e)
  | Context.save_left s C' e' => Expr.save s (C'.subst e) e'
  | Context.save_right s e' C' => Expr.save s e' (C'.subst e)
  | Context.branch_left constr names C' next => Expr.branch constr names (C'.subst e) next
  | Context.branch_right constr names body C' => Expr.branch constr names body (C'.subst e)
  | Context.recur name C' => Expr.recur name (C'.subst e)

Lean.MonadRef in Init.Prelude

IsEmpty in Mathlib.Logic.IsEmpty

inductive Object.Approx : Object → Object → Prop where
  | value {v₁ v₂} : v₁ ≲ᵥ v₂ → Object.Approx (Object.value v₁) (Object.value v₂)
  | delayed {env₁ env₂ e₁ e₂} :
    e₁ ≲⟨env₁, env₂⟩ e₂ →
    Object.Approx (Object.delayed env₁ e₁) (Object.delayed env₂ e₂)

@[app_unexpander Expr.var]
def unexpandVar : Unexpander
  | `($_var $s:str $i:num) =>
    let name := mkIdent $ Name.mkSimple s.getString
    mkVar name i
  | _ => throw ()

inductive Eval.Indexed : Nat → Env → Expr → Value → Prop where
  | var {n env name idx val} :
    env[idx]? = some (Object.value val) →
    Eval.Indexed n env (Expr.var name idx) val
  | var_rec {n env name idx env' expr val} :
    env[idx]? = some (Object.delayed env' expr) →
    Eval.Indexed n env' expr val →
    Eval.Indexed n env (Expr.var name idx) val
  | unit {n env} :
    Eval.Indexed n env Expr.unit Value.unit
  | const {n env c} :
    Eval.Indexed n env (Expr.const c) (Value.const c)
  | constr {n env name} :
    Eval.Indexed n env (Expr.constr name) (Value.constr_app name [])
  | app {n n₁ n₂ env env' f body arg val val'} :
    n₁ + n₂ + 1 ≤ n →
    Eval.Indexed n₁ env f (Value.closure env' body) →
    Eval.Indexed (n₁ + 1) env arg val →
    Eval.Indexed n₂ (val ∷ env') body val' →
    Eval.Indexed n env (Expr.app f arg) val'
  | constr_app {n n' env ctr ctr_name ctr_args_rev arg val} :
    n' < n →
    Eval.Indexed n env ctr (Value.constr_app ctr_name ctr_args_rev) →
    Eval.Indexed n' env arg val →
    Eval.Indexed n env (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev))
  | binop {n env op arg₁ arg₂ val₁ val₂} :
    Eval.Indexed n env arg₁ (Value.const (Constant.int val₁)) →
    Eval.Indexed n env arg₂ (Value.const (Constant.int val₂)) →
    Eval.Indexed n env (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂)))
  | lambda {n env name body} :
    Eval.Indexed n env (Expr.lambda name body) (Value.closure env body)
  | save {n n₁ n₂ env name value body val val'} :
    n₁ + n₂ ≤ n →
    Eval.Indexed n₁ env value val →
    Eval.Indexed n₂ (val ∷ env) body val' →
    Eval.Indexed n env (Expr.save name value body) val'
  | branch_matches {n n' env name args_rev body val} :
    n' < n →
    Eval.Indexed n' (args_rev.map Object.value ++ env) body val →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) (Expr.branch name _ body _) val
  | branch_fails {n env name name' args_rev next val} :
    name ≠ name' →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) next val →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) (Expr.branch name' _ _ next) val
  | recur {n n' env name body val} :
    n' < n →
    Eval.Indexed n' (Object.delayed env (Expr.recur name body) :: env) body val →
    Eval.Indexed n env (Expr.recur name body) val

BEq in Init.Prelude

def Expr.mk_app (f : Expr) : List Expr → Expr
  | [] => f
  | x :: xs => Expr.mk_app (Expr.app f x) xs

@[app_unexpander Expr.branch]
def unexpandBranch : Unexpander
  | `($_branch $s:str $lst ⟪$body:expr⟫ ⟪cases| $c:cases⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    match unfoldListLit lst with
    | some ss =>
      let names := List.toArray $ ss.map fun s' => mkIdent (Name.mkSimple s')
      if ss.isEmpty then
        `(⟪cases| | $name => $body $c⟫)
      else
        `(⟪cases| | $name $names* => $body $c⟫)
    | none =>
      throw ()
  | `($_branch $s:str $lst ⟪$body:expr⟫ ⟪⊥⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    match unfoldListLit lst with
    | some ss =>
      let names := List.toArray $ ss.map fun s' => mkIdent (Name.mkSimple s')
      if ss.isEmpty then
        `(⟪cases| | $name => $body⟫)
      else
        `(⟪cases| | $name $names* => $body⟫)
    | none =>
      throw ()
  | `($_branch $s:str $lst ⟪$body:expr⟫ ⟪$next:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    match unfoldListLit lst with
    | some ss =>
      let names := List.toArray $ ss.map fun s' => mkIdent (Name.mkSimple s')
      if ss.isEmpty then
        `(⟪cases| | $name => $body | _ => $next⟫)
      else
        `(⟪cases| | $name $names* => $body | _ => $next⟫)
    | none =>
      throw ()
  | _ => throw ()

@[app_unexpander Expr.save]
def unexpandSave : Unexpander
  | `($_save "_case_" ⟪$v:expr⟫ ⟪cases| $c⟫) =>
    `(⟪case $v of $c end⟫)
  | `($_save $s:str ⟪rec $sname:ident $v:expr⟫ ⟪$b:expr⟫) =>
    if sname.getId.toString == s.getString then
      `(⟪letrec $sname := $v in $b⟫)
    else
      throw ()
  | `($_save $s:str ⟪$v:expr⟫ ⟪$b:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪let $name := $v in $b⟫)
  | _ => throw ()

def Value.Approx.Indexed (n : Nat) (v₁ v₂ : Value) : Prop :=
  (v₁ = Value.unit ∧ v₂ = Value.unit) ∨
  (∃ c, v₁ = Value.const c ∧ v₂ = Value.const c) ∨
  (∃ ctr_name args_rev args_rev',
    v₁ = Value.constr_app ctr_name args_rev ∧
    v₂ = Value.constr_app ctr_name args_rev' ∧
    (∀ k < n, List.Forall₂ (Value.Approx.Indexed k) args_rev args_rev')) ∨
  (∃ env₁ body₁ env₂ body₂,
    v₁ = Value.closure env₁ body₁ ∧
    v₂ = Value.closure env₂ body₂ ∧
    (∀ n₁ n₂, n₁ + n₂ < n →
      ∀ a₁ a₂ r₁,
        Value.Approx.Indexed (n₁ + n₂) a₁ a₂ →
        a₁ ∷ env₁ ⊢ body₁ ↦(n₁) r₁ →
        ∃ r₂,
          a₂ ∷ env₂ ⊢ body₂ ↦ r₂ ∧
          Value.Approx.Indexed n₂ r₁ r₂))

Nat in Init.Prelude

Lean.TSyntaxArray in Init.Prelude

Lean.Syntax in Init.Prelude

Option in Init.Prelude

Lean.Syntax.node3 in Init.Prelude

@[aesop safe cases]
inductive Value.Approx.Inversion : Value -> Value -> Prop where
  | unit : Value.Approx.Inversion Value.unit Value.unit
  | const {c} : Value.Approx.Inversion (Value.const c) (Value.const c)
  | constr_app {ctr_name args_rev args_rev'} :
    args_rev ≲ₐ args_rev' →
    Value.Approx.Inversion (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev')
  | closure {env₁ body₁ env₂ body₂} :
    (∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂) →
    Value.Approx.Inversion (Value.closure env₁ body₁) (Value.closure env₂ body₂)

def Value.Approx.Indexed.Preservation (k : Nat) : Prop :=
  ∀ m n env env' e v,
    m + n < k →
    env ≲ₑ'(m + n) env' →
    env ⊢ e ↦(n) v →
    ∃ v', env' ⊢ e ↦ v' ∧ v ≲ᵥ(m) v'

def Expr.Approx.Contextual (e₁ e₂ : Expr) : Prop :=
  ∀ (C : Context) env, env ⊢ C.subst e₁ ↓ → env ⊢ C.subst e₂ ↓

def Expr.Approx (e₁ e₂ : Expr) : Prop :=
  ∀ env₁ env₂, env₁ ≲ₑ env₂ → e₁ ≲⟨env₁, env₂⟩ e₂

def mkConstrApp {m} [Monad m] [MonadQuotation m] (s : TSyntax `ident) (es : TSyntaxArray `expr) : m (TSyntax `term) := do
  let ctr ← `(Expr.constr $(Lean.Syntax.mkStrLit s.getId.toString))
  es.foldlM (fun acc e => `(Expr.constr_app $acc ⟪$e⟫)) ctr

Lean.Syntax.node in Init.Prelude

Lean.mkIdent in Init.Meta.Defs

Int in Init.Data.Int.Basic
</all_available_defs>

<all_available_lemmas>
lemma Termination.var {env name i v} :
  env[i]? = some (Object.value v) →
  env ⊢ Expr.var name i ↓

lemma Termination.var_rec {env name i env' e} :
    env[i]? = some (Object.delayed env' e) →
    env' ⊢ e ↓ →
    env ⊢ (Expr.var name i) ↓

lemma Termination.unit {env} :
  env ⊢ Expr.unit ↓

lemma Termination.const {env c} :
  env ⊢ Expr.const c ↓

lemma Termination.constr {env nm} :
  env ⊢ Expr.constr nm ↓

lemma Termination.app {env e₁ e₂ v env' body} :
  env ⊢ e₁ ↦ Value.closure env' body →
  env ⊢ e₂ ↦ v →
  v ∷ env' ⊢ body ↓ →
  env ⊢ Expr.app e₁ e₂ ↓

lemma Termination.constr_app {env e₁ e₂ e₁₁ e₁₂} :
  env ⊢ e₁ ↦ Value.constr_app e₁₁ e₁₂ →
  env ⊢ e₂ ↓ →
  env ⊢ Expr.constr_app e₁ e₂ ↓

lemma Termination.binop {env op e₁ e₂ c₁ c₂} :
  env ⊢ e₁ ↦ Value.const (Constant.int c₁) →
  env ⊢ e₂ ↦ Value.const (Constant.int c₂) →
  env ⊢ Expr.binop op e₁ e₂ ↓

lemma Termination.lambda {env name e} : env ⊢ Expr.lambda name e ↓

lemma Termination.save {env name e₁ e₂ v} :
  env ⊢ e₁ ↦ v →
  v ∷ env ⊢ e₂ ↓ →
  env ⊢ Expr.save name e₁ e₂ ↓

lemma Termination.branch_matches {env name vnames args_rev e e'} :
  args_rev.map Object.value ++ env ⊢ e ↓ →
  Value.constr_app name args_rev ∷ env ⊢ Expr.branch name vnames e e' ↓

lemma Termination.branch_fails {env name name' vnames args_rev e e'} :
  name ≠ name' →
  Value.constr_app name args_rev ∷ env ⊢ e' ↓ →
  Value.constr_app name args_rev ∷ env ⊢ Expr.branch name' vnames e e' ↓

lemma Termination.recur {env name e} :
  Object.delayed env (Expr.recur name e) :: env ⊢ e ↓ →
  env ⊢ Expr.recur name e ↓

theorem Eval.deterministic {env e v₁ v₂} (h₁ : env ⊢ e ↦ v₁) (h₂ : env ⊢ e ↦ v₂) : v₁ = v₂

lemma Value.Equiv.toApprox₁ {v₁ v₂} : v₁ ≈ᵥ v₂ → v₁ ≲ᵥ v₂

@[refl]
lemma Value.Approx.Indexed.refl {n} v : v ≲ᵥ(n) v

lemma Expr.Equiv.Param.cong_unit {env env'} :
  Expr.unit ≈⟨env, env'⟩ Expr.unit

lemma Expr.Approx.const {c₁ c₂} :
  Expr.const c₁ ≲ Expr.const c₂ →
  c₁ = c₂

lemma Expr.Approx.cong_app {e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.app e₁ e₂ ≲ Expr.app e₁' e₂'

lemma Expr.Equiv.eval_const {op a₁ a₂ i₁ i₂ i₃} :
  a₁ ≈ Expr.const (Constant.int i₁) →
  a₂ ≈ Expr.const (Constant.int i₂) →
  i₃ = eval_binop_int op i₁ i₂ →
  Expr.binop op a₁ a₂ ≈
    Expr.const (Constant.int i₃)

lemma Expr.Approx.Param.trans {env₁ env₂ env₃ e₁ e₂ e₃} :
  e₁ ≲⟨env₁, env₂⟩ e₂ → e₂ ≲⟨env₂, env₃⟩ e₃ → e₁ ≲⟨env₁, env₃⟩ e₃

@[symm]
lemma Value.Equiv.symm {v₁ v₂} : v₁ ≈ᵥ v₂ → v₂ ≈ᵥ v₁

lemma Expr.Approx.cong_app₁ {e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.app e₁ e₂ ≲ Expr.app e₁' e₂

lemma Env.Approx.Indexed'.anti_monotone {n n' env₁ env₂}
    (h : env₁ ≲ₑ'(n) env₂)
    (h' : n' ≤ n)
    : env₁ ≲ₑ'(n') env₂

@[aesop unsafe 90% destruct]
lemma Value.Approx.closure_inv_right {env₁ body₁ v} :
  Value.closure env₁ body₁ ≲ᵥ v →
  ∃ env₂ body₂,
    v = Value.closure env₂ body₂ ∧
    (∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂)

lemma Expr.Equiv.Param.cong_var {v v' x x' env env' name name'} :
  env[x]? = some (Object.value v) →
  env'[x']? = some (Object.value v') →
  v ≈ᵥ v' →
  Expr.var name x ≈⟨env, env'⟩ Expr.var name' x'

lemma Expr.Approx.cong_binop {op e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁' e₂'

@[aesop unsafe 90% destruct]
lemma Value.Approx.closure_inv_left {env₂ body₂ v} :
  v ≲ᵥ Value.closure env₂ body₂ →
  ∃ env₁ body₁,
    v = Value.closure env₁ body₁ ∧
    (∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂)

lemma Object.Approx.toIndexed {o₁ o₂} : o₁ ≲ₒ o₂ → ∀ n, o₁ ≲ₒ'(n) o₂

lemma Expr.Approx.cong_app₂ {e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.app e₁ e₂ ≲ Expr.app e₁ e₂'

@[refl]
lemma Value.Approx.refl v : v ≲ᵥ v

lemma Expr.Approx.to_preservation {e₁ e₂} :
  e₁ ≲ e₂ →
  ∀ env v₁, env ⊢ e₁ ↦ v₁ → ∃ v₂, env ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂

lemma Env.Approx.Indexed'.delayed {n i : Nat} {env₁ env₂ env e}
  (h₁ : env₁ ≲ₑ'(n) env₂)
  (h₂ : env₁[i]? = some (Object.delayed env e)) :
  (∃ env' e', e ≲(n)⟨env, env'⟩ e' ∧ env₂[i]? = some (Object.delayed env' e')) ∨
  ∃ env', env ≲ₑ'(n) env' ∧ env₂[i]? = some (Object.delayed env' e)

@[refl]
lemma Env.Approx.refl {env} : env ≲ₑ env

lemma Expr.Approx.cong_constr_app₂ {e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁ e₂'

lemma Env.Approx.Indexed'.value {n i : Nat} {env env' v}
  (h₁ : env ≲ₑ'(n) env')
  (h₂ : env[i]? = some (Object.value v)) :
  ∃ v', env'[i]? = some (Object.value v') ∧ v ≲ᵥ(n) v'

lemma Expr.Approx.cong_branch₂ {constr names e next next'} : next ≲ next' → Expr.branch constr names e next ≲ Expr.branch constr names e next'

lemma Object.Approx.Indexed'.anti_monotone {n n' o₁ o₂} (h : o₁ ≲ₒ'(n) o₂) (h' : n' ≤ n) : o₁ ≲ₒ'(n') o₂

@[trans]
lemma Value.Equiv.trans {v₁ v₂ v₃} : v₁ ≈ᵥ v₂ → v₂ ≈ᵥ v₃ → v₁ ≈ᵥ v₃

lemma Value.Approx.constr_app_inv_length {ctr_name args_rev args_rev'} :
  Value.constr_app ctr_name args_rev ≲ᵥ Value.constr_app ctr_name args_rev' →
  args_rev.length = args_rev'.length

lemma Expr.Approx.Param.cong_var {v v' x x' env env' name name'} :
  env[x]? = some (Object.value v) →
  env'[x']? = some (Object.value v') →
  v ≲ᵥ v' →
  Expr.var name x ≲⟨env, env'⟩ Expr.var name' x'

lemma Value.Approx.Indexed.Preservation.anti_monotone {k k'} (h : Value.Approx.Indexed.Preservation k) (h' : k' ≤ k) : Value.Approx.Indexed.Preservation k'

lemma Env.Approx.Indexed'.cons {n o₁ o₂ env₁ env₂}
  (h₁ : o₁ ≲ₒ'(n) o₂)
  (h₂ : env₁ ≲ₑ'(n) env₂) :
  o₁ :: env₁ ≲ₑ'(n) o₂ :: env₂

@[aesop safe destruct]
lemma Value.Approx.constr_app_inv {ctr_name args_rev args_rev'} :
  Value.constr_app ctr_name args_rev ≲ᵥ Value.constr_app ctr_name args_rev' →
  args_rev ≲ₐ args_rev'

@[symm]
lemma Env.Equiv.symm {env₁ env₂} : env₁ ≈ₑ env₂ → env₂ ≈ₑ env₁

lemma Expr.Equiv.Param.cong_constr_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≈⟨env, env'⟩ e₁' →
  e₂ ≈⟨env, env'⟩ e₂' →
  Expr.constr_app e₁ e₂ ≈⟨env, env'⟩ Expr.constr_app e₁' e₂'

lemma Expr.Approx.Param.cong_const {c env env'} :
  Expr.const c ≲⟨env, env'⟩ Expr.const c

@[refl]
lemma Object.Approx.refl {o} : o ≲ₒ o

@[simp]
lemma Value.Approx.unit_left {v} : v ≲ᵥ Value.unit ↔ v = Value.unit

lemma Expr.Approx.Param.cong_constr {cname env env'} :
  Expr.constr cname ≲⟨env, env'⟩ Expr.constr cname

lemma Env.Equiv.toApprox₁ {env₁ env₂} : env₁ ≈ₑ env₂ → env₁ ≲ₑ env₂

lemma Value.Equiv.toApprox₂ {v₁ v₂} : v₁ ≈ᵥ v₂ → v₂ ≲ᵥ v₁

@[refl]
lemma Expr.Approx.Param.refl {env} e : e ≲⟨env, env⟩ e

lemma Expr.Approx.congruence {e₁ e₂} (C : Context) : e₁ ≲ e₂ → C.subst e₁ ≲ C.subst e₂

lemma Expr.Equiv.cong_constr_app {e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.constr_app e₁ e₂ ≈ Expr.constr_app e₁' e₂'

lemma Expr.Equiv.cong_save {name e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.save name e₁ e₂ ≈ Expr.save name e₁' e₂'

lemma Expr.Approx.Param.preserved {e e' env₁ env₂ env₃} :
  e ≲⟨env₁, env₂⟩ e' →
  env₂ ≲ₑ env₃ →
  e ≲⟨env₁, env₃⟩ e'

lemma Expr.Approx.cong_save₂ {name e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.save name e₁ e₂ ≲ Expr.save name e₁ e₂'

lemma Expr.Approx.from_preservation {e₁ e₂}
  (h : ∀ env v₁, env ⊢ e₁ ↦ v₁ → ∃ v₂, env ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂)
  : e₁ ≲ e₂

lemma Expr.Equiv.fromParam {e₁ e₂} : (∀ env₁ env₂, env₁ ≈ₑ env₂ → e₁ ≈⟨env₁, env₂⟩ e₂) → e₁ ≈ e₂

@[simp]
lemma Value.Approx.unit_right {v} : Value.unit ≲ᵥ v ↔ v = Value.unit

lemma Expr.Equiv.cong_branch {constr names e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.branch constr names e₁ e₂ ≈ Expr.branch constr names e₁' e₂'

lemma Expr.Approx.cong_save {name e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.save name e₁ e₂ ≲ Expr.save name e₁' e₂'

lemma Value.Approx.toEquiv {v₁ v₂} : v₁ ≲ᵥ v₂ → v₂ ≲ᵥ v₁ → v₁ ≈ᵥ v₂

lemma Object.Approx.Indexed'.refl' {n o} (h : ∀ v, v ≲ᵥ(n) v) : o ≲ₒ'(n) o

lemma Env.Approx.toIndexed {env₁ env₂} : env₁ ≲ₑ env₂ → ∀ n, env₁ ≲ₑ'(n) env₂

lemma Env.Equiv.toApprox₂ {env₁ env₂} : env₁ ≈ₑ env₂ → env₂ ≲ₑ env₁

@[refl]
lemma Object.Equiv.refl {o} : o ≈ₒ o

lemma Expr.Approx.cong_branch₁ {constr names e e' next} : e ≲ e' → Expr.branch constr names e next ≲ Expr.branch constr names e' next

lemma Expr.Equiv.Param.cong_constr {name env env'} :
  Expr.constr name ≈⟨env, env'⟩ Expr.constr name

lemma Env.Approx.cons_value {v₁ v₂ env} :
  v₁ ≲ᵥ v₂ → v₁ ∷ env ≲ₑ v₂ ∷ env

theorem Value.Approx.Indexed.preserved :
  ∀ m n env env' e v,
    env ≲ₑ'(m + n) env' →
    env ⊢ e ↦(n) v →
    ∃ v', env' ⊢ e ↦ v' ∧ v ≲ᵥ(m) v'

lemma Expr.Approx.toIndexed {e₁ e₂} : e₁ ≲ e₂ → ∀ n, e₁ ≲'(n) e₂

lemma Expr.Equiv.Param.cong_lambda {e₁ e₁' env env' name name'} :
  (∀ a₁ a₂, a₁ ≈ᵥ a₂ → e₁ ≈⟨a₁ ∷ env, a₂ ∷ env'⟩ e₁') →
  Expr.lambda name e₁ ≈⟨env, env'⟩ Expr.lambda name' e₁'

theorem Expr.Equiv.soundness (e₁ e₂ : Expr) : e₁ ≈ e₂ → e₁ ≈ᶜ e₂

lemma Expr.Equiv.toApprox₁ {e₁ e₂} : e₁ ≈ e₂ → e₁ ≲ e₂

lemma Env.Approx.Indexed'.refl' {n env} (h : ∀ v, v ≲ᵥ(n) v) : env ≲ₑ'(n) env

@[symm]
lemma Expr.Equiv.symm {e₁ e₂} : e₁ ≈ e₂ → e₂ ≈ e₁

@[aesop unsafe apply]
lemma Value.Approx.closure {env₁ body₁ env₂ body₂} :
  (∀ a₁ a₂,
    a₁ ≲ᵥ a₂ →
    body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂) →
  Value.closure env₁ body₁ ≲ᵥ Value.closure env₂ body₂

lemma Expr.Approx.cong_lambda {name e e'} : e ≲ e' → Expr.lambda name e ≲ Expr.lambda name e'

lemma Env.Approx.cons {env₁ env₂ o₁ o₂} :
  o₁ ≲ₒ o₂ → env₁ ≲ₑ env₂ → (o₁ :: env₁) ≲ₑ (o₂ :: env₂)

lemma Expr.Approx.Param.cong_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≲⟨env, env'⟩ e₁' →
  e₂ ≲⟨env, env'⟩ e₂' →
  Expr.app e₁ e₂ ≲⟨env, env'⟩ Expr.app e₁' e₂'

lemma Expr.Approx.const_left {c e env} :
  Expr.const c ≲ e →
  env ⊢ e ↦ Value.const c

lemma Expr.Approx.Param.cong_lambda {e e' env₁ env₂ name₁ name₂} :
  (∀ a₁ a₂, a₁ ≲ᵥ a₂ → e ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ e') →
  Expr.lambda name₁ e ≲⟨env₁, env₂⟩ Expr.lambda name₂ e'

lemma Expr.Approx.eval_const₁ {op a₁ a₂ i₁ i₂ i₃} :
  a₁ ≲ Expr.const (Constant.int i₁) →
  a₂ ≲ Expr.const (Constant.int i₂) →
  i₃ = eval_binop_int op i₁ i₂ →
  Expr.binop op a₁ a₂ ≲
    Expr.const (Constant.int i₃)

lemma Expr.Approx.eval_const₂ {op a₁ a₂ i₁ i₂ i₃} :
  Expr.const (Constant.int i₁) ≲ a₁ →
  Expr.const (Constant.int i₂) ≲ a₂ →
  i₃ = eval_binop_int op i₁ i₂ →
  Expr.const (Constant.int i₃) ≲
  Expr.binop op a₁ a₂

@[aesop unsafe apply]
lemma Value.Approx.constr_app {ctr_name args_rev args_rev'} :
  args_rev ≲ₐ args_rev' →
  Value.constr_app ctr_name args_rev ≲ᵥ Value.constr_app ctr_name args_rev'

@[refl]
lemma Expr.Equiv.refl {e} : e ≈ e

lemma Expr.Approx.Param.cong_constr_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≲⟨env, env'⟩ e₁' →
  e₂ ≲⟨env, env'⟩ e₂' →
  Expr.constr_app e₁ e₂ ≲⟨env, env'⟩ Expr.constr_app e₁' e₂'

@[trans]
lemma Expr.Equiv.trans {e₁ e₂ e₃} : e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃

lemma Expr.Equiv.Param.cong_recur {e e' env env' name name'} :
  e ≈⟨Object.delayed env (Expr.recur name e) :: env, Object.delayed env' (Expr.recur name' e') :: env'⟩ e' →
  Expr.recur name e ≈⟨env, env'⟩ Expr.recur name' e'

lemma Expr.Approx.cong_save₁ {name e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.save name e₁ e₂ ≲ Expr.save name e₁' e₂

@[refl]
lemma Expr.Approx.relf {e} : e ≲ e

lemma Expr.Approx.Param.cong_binop {op e₁ e₂ e₁' e₂' env env'} :
  e₁ ≲⟨env, env'⟩ e₁' →
  e₂ ≲⟨env, env'⟩ e₂' →
  Expr.binop op e₁ e₂ ≲⟨env, env'⟩ Expr.binop op e₁' e₂'

lemma Expr.Equiv.toApprox {e₁ e₂} : e₁ ≈ e₂ → e₁ ≲ e₂ ∧ e₂ ≲ e₁

lemma Expr.Approx.cong_branch {constr names e e' next next'} : e ≲ e' → next ≲ next' → Expr.branch constr names e next ≲ Expr.branch constr names e' next'

lemma Expr.Approx.Param.cong_recur {e e' env env' name name'} :
  e ≲⟨Object.delayed env (Expr.recur name e) :: env, Object.delayed env' (Expr.recur name' e') :: env'⟩ e' →
  Expr.recur name e ≲⟨env, env'⟩ Expr.recur name' e'

@[trans]
lemma Env.Equiv.trans {env₁ env₂ env₃} : env₁ ≈ₑ env₂ → env₂ ≈ₑ env₃ → env₁ ≈ₑ env₃

lemma Value.Approx.Indexed.anti_monotone {n n' v₁ v₂} (h : v₁ ≲ᵥ(n) v₂) (h' : n' ≤ n) : v₁ ≲ᵥ(n') v₂

lemma Expr.Equiv.Param.cong_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≈⟨env, env'⟩ e₁' →
  e₂ ≈⟨env, env'⟩ e₂' →
  Expr.app e₁ e₂ ≈⟨env, env'⟩ Expr.app e₁' e₂'

lemma Value.Approx.closure_inv {env₁ body₁ env₂ body₂}
  (h : Value.closure env₁ body₁ ≲ᵥ Value.closure env₂ body₂) :
  ∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂

lemma Expr.Approx.const_right {c e env v} :
  e ≲ Expr.const c →
  env ⊢ e ↦ v →
  v = Value.const c

lemma Value.Approx.Indexed.preserved_step {k} :
  (∀ k' < k, Preservation k') → Preservation k

lemma Expr.Approx.cong_recur {name e e'} : e ≲ e' → Expr.recur name e ≲ Expr.recur name e'

lemma Object.Approx.toEquiv {o₁ o₂} : o₁ ≲ₒ o₂ → o₂ ≲ₒ o₁ → o₁ ≈ₒ o₂

lemma Expr.Approx.Context.Indexed.preserved_step (k : Nat) :
  Context.Indexed.Preserved k → Context.Indexed.Preserved (k + 1)

@[trans]
lemma Object.Equiv.trans {o₁ o₂ o₃} : o₁ ≈ₒ o₂ → o₂ ≈ₒ o₃ → o₁ ≈ₒ o₃

lemma Value.Approx.Indexed.preserved' {k} : Preservation k

lemma Expr.Equiv.cong_binop {op e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.binop op e₁ e₂ ≈ Expr.binop op e₁' e₂'

lemma Expr.Approx.toEquiv {e₁ e₂} : e₁ ≲ e₂ → e₂ ≲ e₁ → e₁ ≈ e₂

lemma Env.Approx.Indexed'.get {n i : Nat} {env env' o₁}
  (h₁ : env ≲ₑ'(n) env')
  (h₂ : env[i]? = some o₁) :
  ∃ o₂, env'[i]? = some o₂ ∧ o₁ ≲ₒ'(n) o₂

@[trans]
lemma Expr.Approx.trans {e₁ e₂ e₃} : e₁ ≲ e₂ → e₂ ≲ e₃ → e₁ ≲ e₃

lemma Expr.Approx.Context.preserved (e₁ e₂ : Expr) :
  e₁ ≲ e₂ →
  ∀ (C : Context) env₁ env₂ v₁,
  env₁ ≲ₑ env₂ → env₁ ⊢ C.subst e₁ ↦ v₁ →
  ∃ v₂, env₂ ⊢ C.subst e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂

lemma Expr.Equiv.Param.cong_fail {env env'} :
  Expr.fail ≈⟨env, env'⟩ Expr.fail

lemma Expr.Approx.cong_binop₂ {op e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁ e₂'

lemma Env.Approx.toEquiv {env₁ env₂} : env₁ ≲ₑ env₂ → env₂ ≲ₑ env₁ → env₁ ≈ₑ env₂

lemma Expr.Equiv.Param.cong_binop {op e₁ e₂ e₁' e₂' env env'} :
  e₁ ≈⟨env, env'⟩ e₁' →
  e₂ ≈⟨env, env'⟩ e₂' →
  Expr.binop op e₁ e₂ ≈⟨env, env'⟩ Expr.binop op e₁' e₂'

lemma Expr.Approx.Param.cong_save {e₁ e₂ e₁' e₂' env env' name name'} :
  (env ⊢ e₁↓ → env' ⊢ e₁'↓) →
  (∀ a a', env ⊢ e₁ ↦ a → env' ⊢ e₁' ↦ a' → e₂ ≲⟨a ∷ env, a' ∷ env'⟩ e₂') →
  Expr.save name e₁ e₂ ≲⟨env, env'⟩ Expr.save name' e₁' e₂'

@[aesop unsafe apply]
lemma Value.Approx.Indexed.unit {n} : Value.unit ≲ᵥ(n) Value.unit

@[aesop unsafe destruct]
lemma Value.Approx.Indexed.invert {n v v'} :
  v ≲ᵥ(n) v' →
  Value.Approx.Indexed.Inversion n v v'

@[aesop unsafe apply]
lemma Value.Approx.Indexed.closure {n env₁ body₁ env₂ body₂} :
    (∀ n₁ n₂, n₁ + n₂ < n →
      ∀ a₁ a₂ v₁,
        a₁ ≲ᵥ(n₁ + n₂) a₂ →
        a₁ ∷ env₁ ⊢ body₁ ↦(n₁) v₁ →
        ∃ v₂, a₂ ∷ env₂ ⊢ body₂ ↦ v₂ ∧ v₁ ≲ᵥ(n₂) v₂) →
    Value.closure env₁ body₁ ≲ᵥ(n) Value.closure env₂ body₂

lemma Expr.Approx.cong_constr_app {e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁' e₂'

@[trans]
lemma Env.Approx.trans {env₁ env₂ env₃} :
  env₁ ≲ₑ env₂ → env₂ ≲ₑ env₃ → env₁ ≲ₑ env₃

@[trans]
lemma Value.Approx.trans {v₁ v₂ v₃} : v₁ ≲ᵥ v₂ → v₂ ≲ᵥ v₃ → v₁ ≲ᵥ v₃

theorem forall₂_trans' {α} {P Q R : α → α → Prop} {l₁ l₂ l₃}
  (h : ∀ x y z, P x y → Q y z → R x z)
  (h₁ : List.Forall₂ P l₁ l₂)
  (h₂ : List.Forall₂ Q l₂ l₃)
  : List.Forall₂ R l₁ l₃

lemma Expr.Approx.preservation {e₁ e₂} :
  e₁ ≲ e₂ ↔
  ∀ env v₁, env ⊢ e₁ ↦ v₁ → ∃ v₂, env ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂

lemma Expr.Equiv.Approx.equiv {e₁ e₂} : e₁ ≈ e₂ ↔ e₁ ≲ e₂ ∧ e₂ ≲ e₁

@[aesop unsafe 90% destruct]
lemma Value.Approx.constr_app_inv_right {ctr_name args_rev v} :
  Value.constr_app ctr_name args_rev ≲ᵥ v →
  ∃ args_rev',
    v = Value.constr_app ctr_name args_rev' ∧
    args_rev ≲ₐ args_rev'

@[refl]
lemma Value.Equiv.refl {v} : v ≈ᵥ v

@[aesop unsafe apply]
lemma Value.Approx.Indexed.constr_app {n ctr_name args_rev args_rev'} :
    (∀ k < n, args_rev ≲ₐ(k) args_rev') →
    Value.constr_app ctr_name args_rev ≲ᵥ(n) Value.constr_app ctr_name args_rev'

lemma Env.Equiv.toApprox {env₁ env₂} : env₁ ≈ₑ env₂ → env₁ ≲ₑ env₂ ∧ env₂ ≲ₑ env₁

@[refl]
lemma Env.Equiv.refl {env} : env ≈ₑ env

lemma Expr.Approx.Context.Indexed.preserved (k : Nat) :
  Context.Indexed.Preserved k

lemma Expr.Approx.Param.Indexed.anti_monotone {n n' env₁ env₂ e₁ e₂}
  (h : e₁ ≲(n)⟨env₁, env₂⟩ e₂)
  (h' : n' ≤ n)
  : e₁ ≲(n')⟨env₁, env₂⟩ e₂

lemma Expr.Approx.Param.cong_branch {constr names names' e e' next next' a a' env env'} :
  a ≲ᵥ a' →
  (∀ args args', a = Value.constr_app constr args → a' = Value.constr_app constr args' →
    e ≲⟨args.map Object.value ++ env, args'.map Object.value ++ env'⟩ e') →
  next ≲⟨a ∷ env, a' ∷ env'⟩ next' →
  Expr.branch constr names e next ≲⟨a ∷ env, a' ∷ env'⟩ Expr.branch constr names' e' next'

lemma Expr.Approx.cong_binop₁ {op e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁' e₂

lemma Expr.Equiv.Context.preserved (e₁ e₂ : Expr) :
  e₁ ≈ e₂ →
  ∀ (C : Context) env₁ env₂ v₁,
  env₁ ≈ₑ env₂ → env₁ ⊢ C.subst e₁ ↦ v₁ →
  ∃ v₂, env₂ ⊢ C.subst e₂ ↦ v₂ ∧ v₁ ≈ᵥ v₂

lemma Env.Approx.Indexed'.concat {n env₁ env₂ env₁' env₂'}
  (h₁ : env₁ ≲ₑ'(n) env₁')
  (h₂ : env₂ ≲ₑ'(n) env₂') :
  env₁ ++ env₂ ≲ₑ'(n) env₁' ++ env₂'

@[aesop unsafe apply]
lemma Value.Approx.Indexed.const {n c} : Value.const c ≲ᵥ(n) Value.const c

lemma Expr.Approx.Indexed'.anti_monotone {n n' e₁ e₂}
  (h : e₁ ≲'(n) e₂)
  (h' : n' ≤ n)
  : e₁ ≲'(n') e₂

lemma Expr.Equiv.cong_app {e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.app e₁ e₂ ≈ Expr.app e₁' e₂'

lemma Expr.Equiv.Param.cong_const {c env env'} :
  Expr.const c ≈⟨env, env'⟩ Expr.const c

lemma Env.Approx.Indexed'.from_value {n l₁ l₂} (h : l₁ ≲ₐ(n) l₂) :
  List.map Object.value l₁ ≲ₑ'(n) List.map Object.value l₂

lemma Expr.Equiv.congruence {e₁ e₂} (C : Context) : e₁ ≈ e₂ → C.subst e₁ ≈ C.subst e₂

theorem Value.Approx.preserved :
  ∀ env env' e v,
    env ≲ₑ env' →
    env ⊢ e ↦ v →
    ∃ v', env' ⊢ e ↦ v' ∧ v ≲ᵥ v'

lemma Env.Approx.Indexed'.from_delayed {n env₁ env₂ l} (h : env₁ ≲ₑ'(n) env₂) :
  List.map (Object.delayed env₁) l ≲ₑ'(n) List.map (Object.delayed env₂) l

lemma Expr.Equiv.cong_lambda {name e₁ e₁'} : e₁ ≈ e₁' → Expr.lambda name e₁ ≈ Expr.lambda name e₁'

@[simp]
lemma Value.Approx.const_left {v c} : v ≲ᵥ Value.const c ↔ v = Value.const c

@[trans]
lemma Object.Approx.trans {o₁ o₂ o₃} : o₁ ≲ₒ o₂ → o₂ ≲ₒ o₃ → o₁ ≲ₒ o₃

lemma Object.Equiv.toApprox {o₁ o₂} : o₁ ≈ₒ o₂ → o₁ ≲ₒ o₂

lemma Expr.Approx.cong_constr_app₁ {e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁' e₂

@[refl]
lemma Env.Approx.Indexed'.refl {n env} : env ≲ₑ'(n) env

lemma Expr.Equiv.cong_recur {name e e'} : e ≈ e' → Expr.recur name e ≈ Expr.recur name e'

@[simp]
lemma Value.Approx.const_right {v c} : Value.const c ≲ᵥ v ↔ v = Value.const c

lemma Expr.Equiv.toApprox₂ {e₁ e₂} : e₁ ≈ e₂ → e₂ ≲ e₁

@[aesop unsafe 90% destruct]
lemma Value.Approx.constr_app_inv_left {ctr_name args_rev' v} :
  v ≲ᵥ Value.constr_app ctr_name args_rev' →
  ∃ args_rev,
    v = Value.constr_app ctr_name args_rev ∧
    args_rev ≲ₐ args_rev'

theorem Expr.Approx.soundness (e₁ e₂ : Expr) : e₁ ≲ e₂ → e₁ ≲ᶜ e₂

lemma Expr.Equiv.Param.cong_branch {constr names₁ names₂ e₁ e₂ e₁' e₂' a a' env env'} :
  a ≈ᵥ a' →
  (∀ args args', a = Value.constr_app constr args → a' = Value.constr_app constr args' →
    e₁ ≈⟨args.map Object.value ++ env, args'.map Object.value ++ env'⟩ e₁') →
  e₂ ≈⟨a ∷ env, a' ∷ env'⟩ e₂' →
  Expr.branch constr names₁ e₁ e₂ ≈⟨a ∷ env, a' ∷ env'⟩ Expr.branch constr names₂ e₁' e₂'

@[symm]
lemma Object.Equiv.symm {o₁ o₂} : o₁ ≈ₒ o₂ → o₂ ≈ₒ o₁

lemma Expr.Approx.Param.cong_unit {env env'} :
  Expr.unit ≲⟨env, env'⟩ Expr.unit

@[refl]
lemma Object.Approx.Indexed'.refl {n o} : o ≲ₒ'(n) o

lemma Object.Equiv.toApprox' {o₁ o₂} : o₁ ≈ₒ o₂ → o₂ ≲ₒ o₁

lemma Expr.Approx.Param.cong_fail {e env env'} :
  Expr.fail ≲⟨env, env'⟩ e

lemma Expr.Equiv.Param.cong_save {e₁ e₂ e₁' e₂' env env' name name'} :
  (env ⊢ e₁↓ → env' ⊢ e₁'↓) →
  (env' ⊢ e₁'↓ → env ⊢ e₁↓) →
  (∀ a a', env ⊢ e₁ ↦ a → env' ⊢ e₁' ↦ a' → e₂ ≈⟨a ∷ env, a' ∷ env'⟩ e₂') →
  Expr.save name e₁ e₂ ≈⟨env, env'⟩ Expr.save name' e₁' e₂'

lemma Expr.Equiv.const {c₁ c₂} :
  Expr.const c₁ ≈ Expr.const c₂ →
  c₁ = c₂

@[aesop unsafe destruct]
lemma Value.Approx.invert {v v'} :
  v ≲ᵥ v' →
  Value.Approx.Inversion v v'
</all_available_lemmas>

<local_ctx>
import Juvix.Core.Main.Semantics.Eval

import Mathlib.Tactic.Linarith

namespace Juvix.Core.Main

inductive Eval.Indexed : Nat → Env → Expr → Value → Prop where
  | var {n env name idx val} :
    env[idx]? = some (Object.value val) →
    Eval.Indexed n env (Expr.var name idx) val
  | var_rec {n env name idx env' expr val} :
    env[idx]? = some (Object.delayed env' expr) →
    Eval.Indexed n env' expr val →
    Eval.Indexed n env (Expr.var name idx) val
  | unit {n env} :
    Eval.Indexed n env Expr.unit Value.unit
  | const {n env c} :
    Eval.Indexed n env (Expr.const c) (Value.const c)
  | constr {n env name} :
    Eval.Indexed n env (Expr.constr name) (Value.constr_app name [])
  | app {n n₁ n₂ env env' f body arg val val'} :
    n₁ + n₂ + 1 ≤ n →
    Eval.Indexed n₁ env f (Value.closure env' body) →
    Eval.Indexed (n₁ + 1) env arg val →
    Eval.Indexed n₂ (val ∷ env') body val' →
    Eval.Indexed n env (Expr.app f arg) val'
  | constr_app {n n' env ctr ctr_name ctr_args_rev arg val} :
    n' < n →
    Eval.Indexed n env ctr (Value.constr_app ctr_name ctr_args_rev) →
    Eval.Indexed n' env arg val →
    Eval.Indexed n env (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev))
  | binop {n env op arg₁ arg₂ val₁ val₂} :
    Eval.Indexed n env arg₁ (Value.const (Constant.int val₁)) →
    Eval.Indexed n env arg₂ (Value.const (Constant.int val₂)) →
    Eval.Indexed n env (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂)))
  | lambda {n env name body} :
    Eval.Indexed n env (Expr.lambda name body) (Value.closure env body)
  | save {n n₁ n₂ env name value body val val'} :
    n₁ + n₂ ≤ n →
    Eval.Indexed n₁ env value val →
    Eval.Indexed n₂ (val ∷ env) body val' →
    Eval.Indexed n env (Expr.save name value body) val'
  | branch_matches {n n' env name args_rev body val} :
    n' < n →
    Eval.Indexed n' (args_rev.map Object.value ++ env) body val →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) (Expr.branch name _ body _) val
  | branch_fails {n env name name' args_rev next val} :
    name ≠ name' →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) next val →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) (Expr.branch name' _ _ next) val
  | recur {n n' env name body val} :
    n' < n →
    Eval.Indexed n' (Object.delayed env (Expr.recur name body) :: env) body val →
    Eval.Indexed n env (Expr.recur name body) val

notation:40 env:40 " ⊢ " e:40 " ↦(" n ") " v:40 => Eval.Indexed n env e v
</local_ctx>

<target_theorem>
lemma Eval.toIndexed {env e v} (h : env ⊢ e ↦ v) : ∃ n, env ⊢ e ↦(n) v :=
</target_theorem>

