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>
namespace Juvix.Core.Main
  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
end Juvix.Core.Main

namespace Juvix.Core.Main
  inductive Object : Type where
    | value : Value → Object
    | delayed : (env : List Object) → Expr → Object
    deriving Inhabited
end Juvix.Core.Main

namespace Juvix.Core.Main
abbrev Env : Type := List Object
end Juvix.Core.Main

namespace Juvix.Core.Main
abbrev cons_value (v : Value) (env : Env) : Env := Object.value v :: env
end Juvix.Core.Main

namespace Juvix.Core.Main
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"
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂))
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
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)
end Juvix.Core.Main

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

namespace Juvix.Core.Main
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₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
@[aesop safe cases]
inductive Value.Approx.Indexed.Inversion (n : Nat) : Value → Value → Prop where
  | unit : Value.Approx.Indexed.Inversion n Value.unit Value.unit
  | const {c} : Value.Approx.Indexed.Inversion n (Value.const c) (Value.const c)
  | constr_app {ctr_name args_rev args_rev'} :
    (∀ k < n, args_rev ≲ₐ(k) args_rev') →
    Value.Approx.Indexed.Inversion n (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev')
  | closure {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.Approx.Indexed.Inversion n (Value.closure env₁ body₁) (Value.closure env₂ body₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

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

namespace Juvix.Core.Main
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₂
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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
end Juvix.Core.Main

namespace Juvix.Core.Main
def Eval.Defined (env : Env) (e : Expr) : Prop :=
  ∃ v, env ⊢ e ↦ v
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂
end Juvix.Core.Main

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
end Juvix.Core.Main

namespace Juvix.Core.Main
def Value.Equiv (v v' : Value) : Prop :=
  v ≲ᵥ v' ∧ v' ≲ᵥ v
end Juvix.Core.Main

namespace Juvix.Core.Main
def Object.Equiv (o o' : Object) : Prop :=
  o ≲ₒ o' ∧ o' ≲ₒ o
end Juvix.Core.Main

namespace Juvix.Core.Main
def Env.Equiv : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ Object.Equiv
end Juvix.Core.Main

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

namespace Juvix.Core.Main
def Expr.Equiv (e₁ e₂ : Expr) : Prop :=
  e₁ ≲ e₂ ∧ e₂ ≲ e₁
end Juvix.Core.Main

namespace Juvix.Core.Main
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
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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)
end Juvix.Core.Main

namespace Juvix.Core.Main
def Value.Approx (v v' : Value) : Prop :=
  ∀ n, v ≲ᵥ(n) v'
end Juvix.Core.Main

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

namespace Juvix.Core.Main
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₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
def Env.Approx : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ Object.Approx
end Juvix.Core.Main

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

namespace Juvix.Core.Main
@[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₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
abbrev Name : Type := String
end Juvix.Core.Main

namespace Juvix.Core.Main
inductive Constant : Type where
  | int : Int → Constant
  | string : String → Constant
  deriving Inhabited, BEq, DecidableEq
end Juvix.Core.Main

namespace Juvix.Core.Main
inductive BinaryOp : Type where
  | add_int : BinaryOp
  | sub_int : BinaryOp
  | mul_int : BinaryOp
  | div_int : BinaryOp
  deriving Inhabited, BEq, DecidableEq
end Juvix.Core.Main

namespace Juvix.Core.Main
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
end Juvix.Core.Main

namespace Juvix.Core.Main
def Expr.mk_app (f : Expr) : List Expr → Expr
  | [] => f
  | x :: xs => Expr.mk_app (Expr.app f x) xs
end Juvix.Core.Main

namespace Juvix.Core.Main.Syntax
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
end Juvix.Core.Main.Syntax

namespace Juvix.Core.Main.Syntax
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
end Juvix.Core.Main.Syntax

namespace Juvix.Core.Main.Syntax
instance : Coe Syntax (TSyntax `expr) where
  coe s := ⟨s⟩
end Juvix.Core.Main.Syntax

namespace Juvix.Core.Main.Pretty
def mkVar {m} [Monad m] [MonadRef m] (name : Ident) (i : TSyntax `num) : 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.node3 info `Juvix.Core.Main.Syntax.expr_var
              name (Lean.Syntax.atom info "♯") i)
            (Lean.Syntax.atom info "⟫")
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
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 "⟫")
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
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
end Juvix.Core.Main.Pretty

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

namespace Juvix.Core.Main.Pretty
@[app_unexpander Expr.unit]
def unexpandUnit : Unexpander
  | `($_unit) => `(⟪υ⟫)
end Juvix.Core.Main.Pretty

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

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

namespace Juvix.Core.Main.Pretty
@[app_unexpander Expr.constr]
def unexpandConstr : Unexpander
  | `($_constr $s:str) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪ $name ⟫)
  | _ => throw ()
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
@[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 ()
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
@[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 ()
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
@[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
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
@[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 ()
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
@[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 ()
end Juvix.Core.Main.Pretty

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

namespace Juvix.Core.Main.Pretty
@[app_unexpander Expr.fail]
def unexpandFail : Unexpander
  | `($_bot) => `(⟪⊥⟫)
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main.Pretty
@[category_parenthesizer expr]
def expr.parenthesizer : CategoryParenthesizer := term.parenthesizer
end Juvix.Core.Main.Pretty

namespace Juvix.Core.Main
def Expr.Equiv.Contextual (e₁ e₂ : Expr) : Prop :=
  e₁ ≲ᶜ e₂ ∧ e₂ ≲ᶜ e₁
end Juvix.Core.Main

List in Init.Prelude

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

Transitive in Mathlib.Order.Defs.Unbundled

closure in Mathlib.Topology.Defs.Basic

Lean.MonadRef in Init.Prelude

Lean.Syntax in Init.Prelude

Lean.TSyntax in Init.Prelude

Monad in Init.Prelude

Lean.MonadRef.mkInfoFromRefPos in Init.Prelude

Lean.Syntax.atom in Init.Prelude

Lean.Syntax.node3 in Init.Prelude

Lean.TSyntaxArray in Init.Prelude

Lean.Syntax.node in Init.Prelude

Lean.Syntax.node2 in Init.Prelude

Option in Init.Prelude

String in Init.Prelude

Lean.Name.mkSimple in Init.Prelude

Lean.mkIdent in Init.Meta.Defs

guard in Init.Control.Basic

Lean.Expr in Lean.Expr

Lean.Expr.const in Lean.Expr

List.toArray in Init.Prelude

BEq in Init.Prelude

Inhabited in Init.Prelude

DecidableEq in Init.Prelude

Int in Init.Data.Int.Basic

Nat in Init.Prelude

Lean.MonadQuotation in Init.Prelude

Lean.Syntax.mkStrLit in Init.Meta.Defs

Coe in Init.Coe

IsEmpty in Mathlib.Logic.IsEmpty

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

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

List.map in Init.Prelude

Prod in Init.Prelude

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

List.cons in Init.Prelude

List.nil in Init.Prelude
</all_available_defs>

<all_available_lemmas>
namespace Juvix.Core.Main
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₂
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
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)
end Juvix.Core.Main

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

namespace Juvix.Core.Main
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
end Juvix.Core.Main

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

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

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

namespace Juvix.Core.Main
lemma Termination.var {env name i v} :
  env[i]? = some (Object.value v) →
  env ⊢ Expr.var name i ↓
end Juvix.Core.Main

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

namespace Juvix.Core.Main
lemma Termination.unit {env} :
  env ⊢ Expr.unit ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Termination.const {env c} :
  env ⊢ Expr.const c ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Termination.constr {env nm} :
  env ⊢ Expr.constr nm ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂ ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Termination.constr_app {env e₁ e₂ e₁₁ e₁₂} :
  env ⊢ e₁ ↦ Value.constr_app e₁₁ e₁₂ →
  env ⊢ e₂ ↓ →
  env ⊢ Expr.constr_app e₁ e₂ ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂ ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Termination.lambda {env name e} : env ⊢ Expr.lambda name e ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Termination.save {env name e₁ e₂ v} :
  env ⊢ e₁ ↦ v →
  v ∷ env ⊢ e₂ ↓ →
  env ⊢ Expr.save name e₁ e₂ ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
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' ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
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' ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Termination.recur {env name e} :
  Object.delayed env (Expr.recur name e) :: env ⊢ e ↓ →
  env ⊢ Expr.recur name e ↓
end Juvix.Core.Main

namespace Juvix.Core.Main
theorem Eval.deterministic {env e v₁ v₂} (h₁ : env ⊢ e ↦ v₁) (h₂ : env ⊢ e ↦ v₂) : v₁ = v₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.congruence {e₁ e₂} (C : Context) : e₁ ≲ e₂ → C.subst e₁ ≲ C.subst e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_app₁ {e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.app e₁ e₂ ≲ Expr.app e₁' e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_app₂ {e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.app e₁ e₂ ≲ Expr.app e₁ e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_app {e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.app e₁ e₂ ≲ Expr.app e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_constr_app₁ {e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁' e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_constr_app₂ {e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁ e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_constr_app {e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_binop₁ {op e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁' e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_binop₂ {op e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁ e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_binop {op e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_lambda {name e e'} : e ≲ e' → Expr.lambda name e ≲ Expr.lambda name e'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_save₁ {name e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.save name e₁ e₂ ≲ Expr.save name e₁' e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_save₂ {name e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.save name e₁ e₂ ≲ Expr.save name e₁ e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_save {name e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.save name e₁ e₂ ≲ Expr.save name e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_branch₁ {constr names e e' next} : e ≲ e' → Expr.branch constr names e next ≲ Expr.branch constr names e' next
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_branch₂ {constr names e next next'} : next ≲ next' → Expr.branch constr names e next ≲ Expr.branch constr names e next'
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.cong_recur {name e e'} : e ≲ e' → Expr.recur name e ≲ Expr.recur name e'
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.Param.cong_unit {env env'} :
  Expr.unit ≲⟨env, env'⟩ Expr.unit
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.Param.cong_const {c env env'} :
  Expr.const c ≲⟨env, env'⟩ Expr.const c
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.Param.cong_constr {cname env env'} :
  Expr.constr cname ≲⟨env, env'⟩ Expr.constr cname
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.Param.cong_fail {e env env'} :
  Expr.fail ≲⟨env, env'⟩ e
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.Context.Indexed.preserved_step (k : Nat) :
  Context.Indexed.Preserved k → Context.Indexed.Preserved (k + 1)
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.Context.Indexed.preserved (k : Nat) :
  Context.Indexed.Preserved k
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂
end Juvix.Core.Main

namespace Juvix.Core.Main
theorem Expr.Approx.soundness (e₁ e₂ : Expr) : e₁ ≲ e₂ → e₁ ≲ᶜ e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Eval.Indexed.monotone {n n' env e v} (h : env ⊢ e ↦(n) v) (h' : n ≤ n') : env ⊢ e ↦(n') v
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Eval.Indexed.toEval {n env e v} (h : env ⊢ e ↦(n) v) : env ⊢ e ↦ v
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Eval.toIndexed {env e v} (h : env ⊢ e ↦ v) : ∃ n, env ⊢ e ↦(n) v
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Value.Equiv.toApprox₁ {v₁ v₂} : v₁ ≈ᵥ v₂ → v₁ ≲ᵥ v₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Value.Equiv.toApprox₂ {v₁ v₂} : v₁ ≈ᵥ v₂ → v₂ ≲ᵥ v₁
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Value.Approx.toEquiv {v₁ v₂} : v₁ ≲ᵥ v₂ → v₂ ≲ᵥ v₁ → v₁ ≈ᵥ v₂
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Value.Equiv.refl {v} : v ≈ᵥ v
end Juvix.Core.Main

namespace Juvix.Core.Main
@[symm]
lemma Value.Equiv.symm {v₁ v₂} : v₁ ≈ᵥ v₂ → v₂ ≈ᵥ v₁
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Value.Equiv.trans {v₁ v₂ v₃} : v₁ ≈ᵥ v₂ → v₂ ≈ᵥ v₃ → v₁ ≈ᵥ v₃
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Object.Equiv.toApprox {o₁ o₂} : o₁ ≈ₒ o₂ → o₁ ≲ₒ o₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Object.Equiv.toApprox' {o₁ o₂} : o₁ ≈ₒ o₂ → o₂ ≲ₒ o₁
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Object.Approx.toEquiv {o₁ o₂} : o₁ ≲ₒ o₂ → o₂ ≲ₒ o₁ → o₁ ≈ₒ o₂
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Object.Equiv.refl {o} : o ≈ₒ o
end Juvix.Core.Main

namespace Juvix.Core.Main
@[symm]
lemma Object.Equiv.symm {o₁ o₂} : o₁ ≈ₒ o₂ → o₂ ≈ₒ o₁
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Object.Equiv.trans {o₁ o₂ o₃} : o₁ ≈ₒ o₂ → o₂ ≈ₒ o₃ → o₁ ≈ₒ o₃
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Env.Equiv.toApprox₁ {env₁ env₂} : env₁ ≈ₑ env₂ → env₁ ≲ₑ env₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Env.Equiv.toApprox₂ {env₁ env₂} : env₁ ≈ₑ env₂ → env₂ ≲ₑ env₁
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Env.Equiv.toApprox {env₁ env₂} : env₁ ≈ₑ env₂ → env₁ ≲ₑ env₂ ∧ env₂ ≲ₑ env₁
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Env.Approx.toEquiv {env₁ env₂} : env₁ ≲ₑ env₂ → env₂ ≲ₑ env₁ → env₁ ≈ₑ env₂
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Env.Equiv.refl {env} : env ≈ₑ env
end Juvix.Core.Main

namespace Juvix.Core.Main
@[symm]
lemma Env.Equiv.symm {env₁ env₂} : env₁ ≈ₑ env₂ → env₂ ≈ₑ env₁
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Env.Equiv.trans {env₁ env₂ env₃} : env₁ ≈ₑ env₂ → env₂ ≈ₑ env₃ → env₁ ≈ₑ env₃
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.toParam {e₁ e₂ env₁ env₂} : e₁ ≈ e₂ → env₁ ≈ₑ env₂ → e₁ ≈⟨env₁, env₂⟩ e₂
end Juvix.Core.Main

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

namespace Juvix.Core.Main
lemma Expr.Equiv.toApprox₁ {e₁ e₂} : e₁ ≈ e₂ → e₁ ≲ e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.toApprox₂ {e₁ e₂} : e₁ ≈ e₂ → e₂ ≲ e₁
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.toApprox {e₁ e₂} : e₁ ≈ e₂ → e₁ ≲ e₂ ∧ e₂ ≲ e₁
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.toEquiv {e₁ e₂} : e₁ ≲ e₂ → e₂ ≲ e₁ → e₁ ≈ e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.Approx.equiv {e₁ e₂} : e₁ ≈ e₂ ↔ e₁ ≲ e₂ ∧ e₂ ≲ e₁
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Expr.Equiv.refl {e} : e ≈ e
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Expr.Equiv.trans {e₁ e₂ e₃} : e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃
end Juvix.Core.Main

namespace Juvix.Core.Main
@[symm]
lemma Expr.Equiv.symm {e₁ e₂} : e₁ ≈ e₂ → e₂ ≈ e₁
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.const {c₁ c₂} :
  Expr.const c₁ ≈ Expr.const c₂ →
  c₁ = c₂
end Juvix.Core.Main

namespace Juvix.Core.Main
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₃)
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Value.Approx.refl v : v ≲ᵥ v
end Juvix.Core.Main

namespace Juvix.Core.Main
@[simp]
lemma Value.Approx.unit_left {v} : v ≲ᵥ Value.unit ↔ v = Value.unit
end Juvix.Core.Main

namespace Juvix.Core.Main
@[simp]
lemma Value.Approx.unit_right {v} : Value.unit ≲ᵥ v ↔ v = Value.unit
end Juvix.Core.Main

namespace Juvix.Core.Main
@[simp]
lemma Value.Approx.const_left {v c} : v ≲ᵥ Value.const c ↔ v = Value.const c
end Juvix.Core.Main

namespace Juvix.Core.Main
@[simp]
lemma Value.Approx.const_right {v c} : Value.const c ≲ᵥ v ↔ v = Value.const c
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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'
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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'
end Juvix.Core.Main

namespace Juvix.Core.Main
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
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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'
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
@[aesop unsafe destruct]
lemma Value.Approx.invert {v v'} :
  v ≲ᵥ v' →
  Value.Approx.Inversion v v'
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲ᵥ(n) v₂ → v₂ ≲ᵥ v₃ → v₁ ≲ᵥ(n) v₃
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Value.Approx.trans {v₁ v₂ v₃} : v₁ ≲ᵥ v₂ → v₂ ≲ᵥ v₃ → v₁ ≲ᵥ v₃
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Expr.Approx.Param.refl {env} e : e ≲⟨env, env⟩ e
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.Param.trans {env₁ env₂ env₃ e₁ e₂ e₃} :
  e₁ ≲⟨env₁, env₂⟩ e₂ → e₂ ≲⟨env₂, env₃⟩ e₃ → e₁ ≲⟨env₁, env₃⟩ e₃
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Object.Approx.refl {o} : o ≲ₒ o
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Object.Approx.trans {o₁ o₂ o₃} : o₁ ≲ₒ o₂ → o₂ ≲ₒ o₃ → o₁ ≲ₒ o₃
end Juvix.Core.Main

namespace Juvix.Core.Main
@[refl]
lemma Env.Approx.refl {env} : env ≲ₑ env
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Env.Approx.trans {env₁ env₂ env₃} :
  env₁ ≲ₑ env₂ → env₂ ≲ₑ env₃ → env₁ ≲ₑ env₃
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Env.Approx.cons {env₁ env₂ o₁ o₂} :
  o₁ ≲ₒ o₂ → env₁ ≲ₑ env₂ → (o₁ :: env₁) ≲ₑ (o₂ :: env₂)
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Env.Approx.cons_value {v₁ v₂ env} :
  v₁ ≲ᵥ v₂ → v₁ ∷ env ≲ₑ v₂ ∷ env
end Juvix.Core.Main

namespace Juvix.Core.Main
@[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₂
end Juvix.Core.Main

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

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

namespace Juvix.Core.Main
lemma Expr.Approx.toIndexed {e₁ e₂} : e₁ ≲ e₂ → ∀ n, e₁ ≲'(n) e₂
end Juvix.Core.Main

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

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

namespace Juvix.Core.Main
@[refl]
lemma Expr.Approx.relf {e} : e ≲ e
end Juvix.Core.Main

namespace Juvix.Core.Main
@[trans]
lemma Expr.Approx.trans {e₁ e₂ e₃} : e₁ ≲ e₂ → e₂ ≲ e₃ → e₁ ≲ e₃
end Juvix.Core.Main

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

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

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

namespace Juvix.Core.Main
lemma Expr.Approx.const_left {c e env} :
  Expr.const c ≲ e →
  env ⊢ e ↦ Value.const c
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.const_right {c e env v} :
  e ≲ Expr.const c →
  env ⊢ e ↦ v →
  v = Value.const c
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Approx.const {c₁ c₂} :
  Expr.const c₁ ≲ Expr.const c₂ →
  c₁ = c₂
end Juvix.Core.Main

namespace Juvix.Core.Main
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₃)
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂
end Juvix.Core.Main

namespace Juvix.Core.Main
theorem Expr.Equiv.soundness (e₁ e₂ : Expr) : e₁ ≈ e₂ → e₁ ≈ᶜ e₂
end Juvix.Core.Main

namespace Juvix.Utils
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₃
end Juvix.Utils

namespace Juvix.Core.Main
lemma Expr.Equiv.congruence {e₁ e₂} (C : Context) : e₁ ≈ e₂ → C.subst e₁ ≈ C.subst e₂
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.cong_app {e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.app e₁ e₂ ≈ Expr.app e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.cong_constr_app {e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.constr_app e₁ e₂ ≈ Expr.constr_app e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.cong_binop {op e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.binop op e₁ e₂ ≈ Expr.binop op e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.cong_lambda {name e₁ e₁'} : e₁ ≈ e₁' → Expr.lambda name e₁ ≈ Expr.lambda name e₁'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.cong_save {name e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.save name e₁ e₂ ≈ Expr.save name e₁' e₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.cong_recur {name e e'} : e ≈ e' → Expr.recur name e ≈ Expr.recur name e'
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.Param.cong_unit {env env'} :
  Expr.unit ≈⟨env, env'⟩ Expr.unit
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.Param.cong_const {c env env'} :
  Expr.const c ≈⟨env, env'⟩ Expr.const c
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.Param.cong_constr {name env env'} :
  Expr.constr name ≈⟨env, env'⟩ Expr.constr name
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₁'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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₂'
end Juvix.Core.Main

namespace Juvix.Core.Main
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'
end Juvix.Core.Main

namespace Juvix.Core.Main
lemma Expr.Equiv.Param.cong_fail {env env'} :
  Expr.fail ≈⟨env, env'⟩ Expr.fail
end Juvix.Core.Main
</all_available_lemmas>

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

import Juvix.Core.Main.Semantics.Eval.Indexed

import Juvix.Utils

import Mathlib.Tactic.Linarith

import Mathlib.Data.List.Forall2

import Aesop

namespace Juvix.Core.Main

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₂))

notation:40 v:40 " ≲ᵥ(" n:40 ") " v':40 => Value.Approx.Indexed n v v'

notation:40 args₁:40 " ≲ₐ(" n:40 ") " args₂:40 => List.Forall₂ (Value.Approx.Indexed n) args₁ args₂

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₂)

notation:40 e:40 " ≲(" n:40 ")⟨" env:40 ", " env':40 "⟩ " e':40 => Expr.Approx.Param.Indexed n env env' e e'

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 Env.Approx.Indexed' (n : Nat) : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ (Object.Approx.Indexed' n)

notation:40 v:40 " ≲ₒ'(" n:40 ") " v':40 => Object.Approx.Indexed' n v v'

notation:40 env₁:40 " ≲ₑ'(" n:40 ") " env₂:40 => Env.Approx.Indexed' n env₁ env₂

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₂)

notation:40 e:40 " ≲'(" n:40 ") " e':40 => Expr.Approx.Indexed' n e e'

macro "invert" h:term : tactic => `(tactic| (cases ($h).invert <;> try clear $h))

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₂

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 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)

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 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 Env.Approx.Indexed'.concat {n env₁ env₂ env₁' env₂'}
  (h₁ : env₁ ≲ₑ'(n) env₁')
  (h₂ : env₂ ≲ₑ'(n) env₂') :
  env₁ ++ env₂ ≲ₑ'(n) env₁' ++ env₂'

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

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

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

@[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'

@[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₂

@[aesop safe cases]
inductive Value.Approx.Indexed.Inversion (n : Nat) : Value → Value → Prop where
  | unit : Value.Approx.Indexed.Inversion n Value.unit Value.unit
  | const {c} : Value.Approx.Indexed.Inversion n (Value.const c) (Value.const c)
  | constr_app {ctr_name args_rev args_rev'} :
    (∀ k < n, args_rev ≲ₐ(k) args_rev') →
    Value.Approx.Indexed.Inversion n (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev')
  | closure {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.Approx.Indexed.Inversion n (Value.closure env₁ body₁) (Value.closure env₂ body₂)

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

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

