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>
def ident := String deriving BEq, Repr, Hashable

inductive aexp : Type where
  | CONST (n : Int)               
  | VAR (x : ident)               
  | PLUS (a1 : aexp) (a2 : aexp)  
  | MINUS (a1 : aexp) (s2 : aexp) 

def store : Type := ident → Int

@[grind] def aeval (s : store) (a : aexp) : Int :=
  match a with
  | .CONST n => n
  | .VAR x => s x
  | .PLUS a1 a2 => aeval s a1 + aeval s a2
  | .MINUS a1 a2 => aeval s a1 - aeval s a2

@[grind] def free_in_aexp (x : ident) (a : aexp) : Prop :=
  match a with
  | .CONST _ => False
  | .VAR y => y = x
  | .PLUS a1 a2
  | .MINUS a1 a2 => free_in_aexp x a1 ∨ free_in_aexp x a2

inductive bexp : Type where
  | TRUE                              
  | FALSE                             
  | EQUAL (a1 : aexp) (a2 : aexp)     
  | LESSEQUAL (a1 : aexp) (a2 : aexp) 
  | NOT (b1 : bexp)                   
  | AND (b1 : bexp) (b2 : bexp)       

def NOTEQUAL (a1 a2 : aexp) : bexp := .NOT (.EQUAL a1 a2)

def GREATEREQUAL (a1 a2 : aexp) : bexp := .LESSEQUAL a2 a1

def GREATER (a1 a2 : aexp) : bexp := .NOT (.LESSEQUAL a1 a2)

def LESS (a1 a2 : aexp) : bexp := GREATER a2 a1

@[grind] def OR (b1 b2 : bexp) : bexp := .NOT (.AND (.NOT b1) (.NOT b2))

@[grind] def beval (s : store) (b : bexp) : Bool :=
  match b with
  | .TRUE => true
  | .FALSE => false
  | .EQUAL a1 a2 => aeval s a1 = aeval s a2
  | .LESSEQUAL a1 a2 => aeval s a1 <= aeval s a2
  | .NOT b1 =>  !(beval s b1)
  | .AND b1 b2 => beval s b1 && beval s b2

inductive com : Type where
  | SKIP                                        
  | ASSIGN (x : ident) (a : aexp)               
  | SEQ (c1 : com) (c2 : com)                   
  | IFTHENELSE (b : bexp) (c1 : com) (c2 : com) 
  | WHILE (b : bexp) (c1 : com)                 

def Euclidean_division :=
  .ASSIGN "r" (.VAR "a") ;;
  .ASSIGN "q" (.CONST 0) ;;
  .WHILE (.LESSEQUAL (.VAR "b") (.VAR "r"))
    (.ASSIGN "r" (.MINUS (.VAR "r") (.VAR "b")) ;;
     .ASSIGN "q" (.PLUS (.VAR "q") (.CONST 1)))

@[grind] def update (x : ident) (v : Int) (s : store) : store :=
  fun y => if x == y then v else s y

@[grind] inductive cexec : store → com → store → Prop where
  | cexec_skip :
      cexec s .SKIP s
  | cexec_assign :
      cexec s (.ASSIGN x a) (update x (aeval s a) s)
  | cexec_seq :
      cexec s c1 s' -> cexec s' c2 s'' ->
      cexec s (.SEQ c1 c2) s''
  | cexec_ifthenelse :
      cexec s (if beval s b then c1 else c2) s' ->
      cexec s (.IFTHENELSE b c1 c2) s'
  | cexec_while_done :
      beval s b = false ->
      cexec s (.WHILE b c) s
  | cexec_while_loop :
      beval s b = true -> cexec s c s' -> cexec s' (.WHILE b c) s'' ->
      cexec s (.WHILE b c) s''

@[grind] def cexec_bounded (fuel : Nat) (s : store) (c : com) : Option store :=
  match fuel with
  | .zero => .none
  | .succ fuel' =>
    match c with
    | .SKIP => .some s
    | .ASSIGN x a => .some (update x (aeval s a) s)
    | .SEQ c1 c2 =>
      match cexec_bounded fuel' s c1 with
      | .none => .none
      | .some s' => cexec_bounded fuel' s' c2
    | .IFTHENELSE b c1 c2 =>
      if beval s b then cexec_bounded fuel' s c1 else cexec_bounded fuel' s c2
    | .WHILE b c1 =>
      if beval s b then
        match cexec_bounded fuel' s c1 with
        | .none => .none
        | .some s' => cexec_bounded fuel' s' (.WHILE b c1)
      else
        .some s

@[grind] inductive red : com × store → com × store → Prop where
  | red_assign : ∀ x a s,
      red (.ASSIGN x a, s) (.SKIP, update x (aeval s a) s)
  | red_seq_done : ∀ c s,
      red (.SEQ .SKIP c, s) (c, s)
  | red_seq_step : ∀ c1 c s1 c2 s2,
      red (c1, s1) (c2, s2) →
      red (.SEQ c1 c, s1) (.SEQ c2 c, s2)
  | red_ifthenelse : ∀ b c1 c2 s,
      red (.IFTHENELSE b c1 c2, s) ((if beval s b then c1 else c2), s)
  | red_while_done : ∀ b c s,
      beval s b = false →
      red (.WHILE b c, s) (.SKIP, s)
  | red_while_loop : ∀ b c s,
      beval s b = true →
      red (.WHILE b c, s) (.SEQ c (.WHILE b c), s)

def goes_wrong (c : com) (s : store) : Prop := ∃ c', ∃ s', star red (c, s) (c', s') ∧ irred red (c', s') ∧ c' ≠ .SKIP

@[grind] inductive cont where
| Kstop
| Kseq (c : com) (k : cont)
| Kwhile (b : bexp) (c : com) (k : cont)

@[grind] def apply_cont (k : cont) (c : com) : com :=
  match k with
  | .Kstop => c
  | .Kseq c1 k1 => apply_cont k1 (.SEQ c c1)
  | .Kwhile b1 c1 k1 => apply_cont k1 (.SEQ c (.WHILE b1 c1))

inductive step : com × cont × store -> com × cont × store -> Prop where
  | step_assign : ∀ x a k s,
      step (.ASSIGN x a, k, s) (.SKIP, k, update x (aeval s a) s)
    
  | step_seq : ∀ c1 c2 s k,
      step (.SEQ c1 c2, k, s) (c1, .Kseq c2 k, s)
      
  | step_ifthenelse : ∀ b c1 c2 k s,
      step (.IFTHENELSE b c1 c2, k, s) ((if beval s b then c1 else c2), k, s)
      
  | step_while_done : ∀ b c k s,
      beval s b = false ->
      step (.WHILE b c, k, s) (.SKIP, k, s)
      
  | step_while_true : ∀ b c k s,
      beval s b = true ->
      step (.WHILE b c, k, s) (c, .Kwhile b c k, s)
      
  | step_skip_seq : ∀ c k s,
      step (.SKIP, .Kseq c k, s) (c, k, s)
      
  | step_skip_while : ∀ b c k s,
      step (.SKIP, .Kwhile b c k, s) (.WHILE b c, k, s)

@[grind] class OrderStruct (α : Sort u) where
  eq : α → α → Prop
  le : α → α → Prop
  beq : α → α → Bool
  le_trans : ∀ x y z, le x y -> le y z -> le x z
  beq_true' : ∀ x y : α, beq x y = true → eq x y := by admit /- proof elided -/

@[grind] def gt {α : Sort u} [OrderStruct α] (x y : α) : Prop := le y x ∧ ¬eq y x

def gt_well_founded {α : Sort u} [OrderStruct α] : WellFounded (gt : α → α → Prop) :=

class OrderWithBot (α : Sort u) extends OrderStruct α where
  bot : α
  bot_smallest : ∀ x, le bot x

class Monotone (α : Sort u) (F : α → α) [OrderStruct α] where
  F_mon : ∀ {x y : α}, le x y → le (F x) (F y)

def cannotExtractFixpoint [Monotone α F] : α :=
  let fixpoint := fixpoint_exists_1 α F
  match fixpoint with
  | ⟨x, P⟩ => x

instance : WellFoundedRelation α  where
  rel := gt
  wf := gt_wf

@[grind] def iterate (x : α) (PRE : le x (F x)) (SMALL : ∀ z, le (F z) z -> le x z) : α :=
  if beq x (F x) then x else iterate (F x) (by admit /- proof elided -/
  ) (by admit /- proof elided -/
  )
  termination_by x
  decreasing_by
    grind [beq_false']

@[grind] def fixpoint' : α := iterate α F bot (by admit /- proof elided -/
) (by admit /- proof elided -/
)

@[grind] def Eq' (S1 S2 : Store) : Prop := Equal S1 S2

def Eq'_sym : ∀ S1 S2, Eq' S1 S2 → Eq' S2 S1 :=

@[grind] def Gt (S1 S2 : Store) := Le S2 S1 ∧ ¬ Eq' S2 S1

@[grind] def Increasing (F : Store → Store) := ∀ x y, Le x y → Le (F x) (F y)

noncomputable instance : OrderStruct Store where
  eq := Equal
  le := Le
  beq (S1 S2 : Store) :=  Decidable.decide (Equal S1 S2)
  le_trans := Le_trans
  gt_wf := Gt_wf

instance : Monotone Store (fun x => Join Init (F x)) where
  F_mon := by admit /- proof elided -/

noncomputable def fixpoint_join : Store :=

noncomputable instance wrapper (F : Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) : Monotone Store F where
  F_mon := by admit /- proof elided -/

noncomputable def fixpoint_join' (S : Store) (F : Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) :=

noncomputable def Cexec' : (c : com) →  {F : Store → Store // ∀ x y, le x y → le (F x) (F y)}
| .SKIP => ⟨(fun S => S), by admit /- proof elided -/
⟩
| .ASSIGN x a => ⟨(fun S => Update x (Aeval S a) S), by admit /- proof elided -/
      ⟩
| .SEQ c1 c2 =>
  let ⟨ f₁, mon₁ ⟩ := Cexec' c1
  let ⟨ f₂, mon₂ ⟩ := Cexec' c2
  ⟨ (fun S => f₂ (f₁ S)), by admit /- proof elided -/
  ⟩
| .IFTHENELSE b c1 c2 =>
  let ⟨ f₁, mon₁ ⟩ := Cexec' c1
  let ⟨ f₂, mon₂ ⟩ := Cexec' c2
  ⟨ (fun S =>
    match Beval S b with
    | .some true => f₁ S
    | .some false => f₂ S
    | .none => Join (f₁ S) (f₂ S)
    ), by admit /- proof elided -/
        ⟩
| .WHILE b c1 =>
   let ⟨ f₁, mon₁ ⟩ := Cexec' c1
   ⟨ fun S => fixpoint_join' S f₁ mon₁, by admit /- proof elided -/
      ⟩

noncomputable def Cexec_Constprop (c : com) : Store → Store := (Cexec' c).val

instance (c : com) : Monotone Store (Cexec_Constprop c) where
  F_mon := by admit /- proof elided -/

@[grind] inductive instr : Type where
  | Iconst (n : Int)             
  | Ivar (x : ident)             
  | Isetvar (x : ident)          
  | Iadd                         
  | Iopp                         
  | Ibranch (d : Int)            
  | Ibeq (d1 : Int) (d0 : Int)   
  | Ible (d1 : Int) (d0 : Int)   
  | Ihalt                        
    deriving Repr

@[grind] def codelen (c : List instr) : Int := c.length

def stack : Type := List Int

def config : Type := Int × stack × store

@[grind] def instr_at (C : List instr) (pc : Int) : Option instr :=
  match C with
  | [] => .none
  | i :: C' => if pc = 0 then .some i else instr_at C' (pc - 1)

@[grind] inductive transition (C : List instr) : config → config → Prop where
  | trans_const : ∀ pc stk s n,
      instr_at C pc = .some (.Iconst n) →
      transition C (pc    , stk     , s)
                   (pc + 1, n :: stk, s)
  | trans_var : ∀ pc stk s x,
      instr_at C pc = .some (.Ivar x) ->
      transition C (pc    , stk       , s)
                   (pc + 1, s x :: stk, s)
  | trans_setvar : ∀ pc stk s x n,
      instr_at C pc = .some (.Isetvar x) ->
      transition C (pc    , n :: stk, s)
                   (pc + 1, stk     , update x n s)
  | trans_add : ∀ pc stk s n1 n2,
      instr_at C pc = .some (.Iadd) ->
      transition C (pc    , n2 :: n1 :: stk , s)
                   (pc + 1, (n1 + n2) :: stk, s)
  | trans_opp : ∀ pc stk s n,
      instr_at C pc = .some (.Iopp) ->
      transition C (pc    , n :: stk    , s)
                   (pc + 1, (- n) :: stk, s)
  | trans_branch : ∀ pc stk s d pc',
      instr_at C pc = .some (.Ibranch d) ->
      pc' = pc + 1 + d ->
      transition C (pc , stk, s)
                   (pc', stk, s)
  | trans_beq : ∀ pc stk s d1 d0 n1 n2 pc',
      instr_at C pc = .some (.Ibeq d1 d0) ->
      pc' = pc + 1 + (if n1 = n2 then d1 else d0) ->
      transition C (pc , n2 :: n1 :: stk, s)
                   (pc', stk            , s)
  | trans_ble : ∀ pc stk s d1 d0 n1 n2 pc',
      instr_at C pc = .some (.Ible d1 d0) ->
      pc' = pc + 1 + (if n1 ≤ n2 then d1 else d0) ->
      transition C (pc , n2 :: n1 :: stk, s)
                   (pc', stk            , s)

@[grind] def transitions (C : List instr) : config → config → Prop :=
  star (transition C)

def machine_terminates (C : List instr) (s_init : store) (s_final : store) : Prop :=
  ∃ pc, transitions C (0, [], s_init) (pc, [], s_final)
          ∧ instr_at C pc = .some .Ihalt

def machine_diverges (C : List instr) (s_init : store) : Prop :=
  infseq (transition C) (0, [], s_init)

def machine_goes_wrong (C : List instr) (s_init : store) : Prop :=
  ∃ pc stk s,
      transitions C (0, [], s_init) (pc, stk, s)
   ∧ irred (transition C) (pc, stk, s)
   ∧ (instr_at C pc ≠ .some .Ihalt ∨ stk ≠ [])

@[grind] def compile_aexp (a : aexp) : List instr :=
  match a with
  | .CONST n => .Iconst n :: []
  | .VAR x => .Ivar x :: []
  | .PLUS a1 a2  => (compile_aexp a1) ++ (compile_aexp a2) ++ (.Iadd :: [])
  | .MINUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ (.Iopp :: .Iadd :: [])

@[grind] def compile_bexp (b : bexp) (d1 : Int) (d0 : Int) : List instr :=
  match b with
  | .TRUE => if d1 = 0 then [] else .Ibranch d1 :: []
  | .FALSE => if d0 = 0 then [] else .Ibranch d0 :: []
  | .EQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ .Ibeq d1 d0 :: []
  | .LESSEQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ .Ible d1 d0 :: []
  | .NOT b1 => compile_bexp b1 d0 d1
  | .AND b1 b2 =>
      let code2 := compile_bexp b2 d1 d0
      let code1 := compile_bexp b1 0 (codelen code2 + d0)
      code1 ++ code2

@[grind] def compile_com (c : com) : List instr :=
  match c with
  | .SKIP =>
      []
  | .ASSIGN x a =>
      compile_aexp a ++ .Isetvar x :: []
  | .SEQ c1 c2 =>
      compile_com c1 ++ compile_com c2
  | .IFTHENELSE b ifso ifnot =>
      let code_ifso := compile_com ifso
      let code_ifnot := compile_com ifnot
      compile_bexp b 0 (codelen code_ifso + 1)
      ++ code_ifso
      ++ .Ibranch (codelen code_ifnot)
      :: code_ifnot
  | .WHILE b body =>
      let code_body := compile_com body
      let code_test := compile_bexp b 0 (codelen code_body + 1)
      code_test
      ++ code_body
      ++ .Ibranch (- (codelen code_test + codelen code_body + 1)) :: []

def compile_program (p : com) : List instr :=
  compile_com p ++ .Ihalt :: []

def smart_Ibranch (d : Int) : List instr :=
  if d = 0 then [] else .Ibranch d :: []

@[grind] inductive code_at : List instr → Int → List instr → Prop where
  | code_at_intro : ∀ C1 C2 C3 pc,
      pc = codelen C1 ->
      code_at (C1 ++ C2 ++ C3) pc C2

inductive compile_cont (C : List instr) : cont -> Int -> Prop where
  | ccont_stop : ∀ pc,
      instr_at C pc = .some .Ihalt ->
      compile_cont C .Kstop pc
  | ccont_seq : ∀ c k pc pc',
      code_at C pc (compile_com c) ->
      pc' = pc + codelen (compile_com c) ->
      compile_cont C k pc' ->
      compile_cont C (.Kseq c k) pc
  | ccont_while : ∀ b c k pc d pc' pc'',
      instr_at C pc = .some (.Ibranch d) ->
      pc' = pc + 1 + d ->
      code_at C pc' (compile_com (.WHILE b c)) ->
      pc'' = pc' + codelen (compile_com (.WHILE b c)) ->
      compile_cont C k pc'' ->
      compile_cont C (.Kwhile b c k) pc
  | ccont_branch : ∀ d k pc pc',
      instr_at C pc = .some (.Ibranch d) ->
      pc' = pc + 1 + d ->
      compile_cont C k pc' ->
      compile_cont C k pc

inductive match_config (C : List instr) : com × cont × store -> config -> Prop where
  | match_config_intro : ∀ c k st pc,
      code_at C pc (compile_com c) ->
      compile_cont C k (pc + codelen (compile_com c)) ->
      match_config C (c, k, st) (pc, [], st)

def com_size (c : com) : Nat :=
  match c with
  | .SKIP => 1
  | .ASSIGN _ _ => 1
  | (c1 ;; c2) => (com_size c1 + com_size c2 + 1)
  | .IFTHENELSE _ c1 c2 => (com_size c1 + com_size c2 + 1)
  | .WHILE _ c1 => (com_size c1 + 1)

def cont_size (k : cont) : Nat :=
  match k with
  | .Kstop => 0
  | .Kseq c k' => (com_size c + cont_size k')
  | .Kwhile _ _ k' => cont_size k'

def measure' (impconf : com × cont × store) : Nat :=
  match impconf with
  | (c, k, _) => (com_size c + cont_size k)

instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where
  beq m n := Id.run do
    if m.size != n.size then return false
    for e in m do
      match n.get? e.1 with
      | none => return false
      | some v => if e.2 != v then return false
    return true

@[grind] def mk_PLUS_CONST (a : aexp) (n : Int) : aexp :=
  if n = 0 then a else
  match a with
  | .CONST m => .CONST (m + n)
  | .PLUS a (.CONST m) => .PLUS a (.CONST (m + n))
  | _ => .PLUS a (.CONST n)

@[grind] def mk_PLUS (a1 a2 : aexp) : aexp :=
  match a1, a2 with
  | .CONST m, _ => mk_PLUS_CONST a2 m
  | _, .CONST m => mk_PLUS_CONST a1 m
  | .PLUS a1 (.CONST m1), .PLUS a2 (.CONST m2) => mk_PLUS_CONST (.PLUS a1 a2) (m1 + m2)
  | .PLUS a1 (.CONST m1), _ => mk_PLUS_CONST (.PLUS a1 a2) m1
  | _, .PLUS a2 (.CONST m2) => mk_PLUS_CONST (.PLUS a1 a2) m2
  | _, _ => .PLUS a1 a2

@[grind] def mk_MINUS (a1 a2 : aexp) : aexp :=
  match a1, a2 with
  | _, .CONST m => mk_PLUS_CONST a1 (-m)
  | .PLUS a1 (.CONST m1), .PLUS a2 (.CONST m2) => mk_PLUS_CONST (.MINUS a1 a2) (m1 - m2)
  | .PLUS a1 (.CONST m1), _ => mk_PLUS_CONST (.MINUS a1 a2) m1
  | _, .PLUS a2 (.CONST m2) => mk_PLUS_CONST (.MINUS a1 a2) (-m2)
  | _, _ => .MINUS a1 a2

@[grind] def simplif_aexp (a : aexp) : aexp :=
  match a with
  | .CONST n => .CONST n
  | .VAR x => .VAR x
  | .PLUS a1 a2 => mk_PLUS (simplif_aexp a1) (simplif_aexp a2)
  | .MINUS a1 a2 => mk_MINUS (simplif_aexp a1) (simplif_aexp a2)

@[grind] def mk_EQUAL (a1 a2 : aexp) : bexp :=
  match a1, a2 with
  | .CONST n1, .CONST n2 => if n1 = n2 then .TRUE else .FALSE
  | .PLUS a1 (.CONST n1), .CONST n2 => .EQUAL a1 (.CONST (n2 - n1))
  | _, _ => .EQUAL a1 a2

@[grind] def mk_LESSEQUAL (a1 a2 : aexp) : bexp :=
  match a1, a2 with
  | .CONST n1, .CONST n2 => if n1 <= n2 then .TRUE else .FALSE
  | .PLUS a1 (.CONST n1), .CONST n2 => .LESSEQUAL a1 (.CONST (n2 - n1))
  | _, _ => .LESSEQUAL a1 a2

@[grind] def mk_NOT (b : bexp) : bexp :=
  match b with
  | .TRUE => .FALSE
  | .FALSE => .TRUE
  | .NOT b => b
  | _ => .NOT b

@[grind] def mk_AND (b1 b2 : bexp) : bexp :=
  match b1, b2 with
  | .TRUE, _ => b2
  | _, .TRUE => b1
  | .FALSE, _ => .FALSE
  | _, .FALSE => .FALSE
  | _, _ => .AND b1 b2

@[grind] def mk_IFTHENELSE (b : bexp) (c1 c2 : com) : com :=
  match b with
  | .TRUE => c1
  | .FALSE => c2
  | _ => .IFTHENELSE b c1 c2

@[grind] def mk_WHILE (b : bexp) (c : com) : com :=
  match b with
  | .FALSE => .SKIP
  | _ => .WHILE b c

def Store := Std.HashMap ident Int

@[grind] def matches' (s : store) (S : Store) : Prop :=
  ∀ x n, S.get? x = .some n -> s x = n

@[grind] def Le (S1 S2 : Store) : Prop :=
  ∀ x n, S2.get? x = .some n -> S1.get? x = .some n

@[grind] def Top : Store := Std.HashMap.emptyWithCapacity

@[grind] def Join (S1 S2 : Store) : Store :=
  S1.filter (fun key _ => S2.get? key == S1.get? key)

def Equal (S1 S2 : Store) := Std.HashMap.Equiv S1 S2

noncomputable instance : Decidable (Equal S' S) :=
  Classical.propDecidable (Equal S' S)

@[grind] def lift1 {A B : Type} (f : A -> B) (o : Option A) : Option B :=
  match o with
  | .some x => .some (f x)
  | .none => .none

@[grind] def lift2 {A B C : Type} (f : A -> B -> C) (o1 : Option A) (o2 : Option B) : Option C :=
  match o1, o2 with
  | .some x1, .some x2 => .some (f x1 x2) | _, _ => .none

@[grind] def Aeval (S : Store) (a : aexp) : Option Int :=
  match a with
  | .CONST n => .some n
  | .VAR x => S.get? x
  | .PLUS a1 a2 => lift2 (Int.add) (Aeval S a1) (Aeval S a2)
  | .MINUS a1 a2 => lift2 (Int.sub) (Aeval S a1) (Aeval S a2)

@[grind] def Beval (S : Store) (b : bexp) : Option Bool :=
  match b with
  | .TRUE => .some true
  | .FALSE => .some false
  | .EQUAL a1 a2 => lift2 (fun m n => m == n) (Aeval S a1) (Aeval S a2)
  | .LESSEQUAL a1 a2 => lift2 (fun m n => m <= n) (Aeval S a1) (Aeval S a2)
  | .NOT b1 => lift1 (fun m => !m) (Beval S b1)
  | .AND b1 b2 => lift2 (fun m n => m && n) (Beval S b1) (Beval S b2)

@[grind] def Update (x : ident) (N : Option Int) (S : Store) : Store :=
  match N with
  | .none => S.erase x
  | .some n => S.insert x n

@[grind] noncomputable def fixpoint_rec (F : Store -> Store) (fuel : Nat) (S : Store) : Store :=
  match fuel with
  | 0 => Top
  | fuel + 1 =>
      let S' := F S
      if Equal S' S then S else fixpoint_rec F fuel S'

@[grind] def num_iter : Nat := 20

@[grind] noncomputable def fixpoint (F : Store -> Store) (init_S : Store) : Store :=
  fixpoint_rec F num_iter init_S

@[grind] noncomputable def Cexec (S : Store) (c : com) : Store :=
  match c with
  | .SKIP => S
  | .ASSIGN x a => Update x (Aeval S a) S
  | .SEQ c1 c2 => Cexec (Cexec S c1) c2
  | .IFTHENELSE b c1 c2 =>
      match Beval S b with
      | .some true => Cexec S c1
      | .some false => Cexec S c2
      | .none => Join (Cexec S c1) (Cexec S c2)
  | .WHILE _ c1 =>
      fixpoint (fun x => Join S (Cexec x c1)) S

@[grind =] def cp_aexp (S : Store) (a : aexp) : aexp :=
  match a with
  | .CONST n => .CONST n
  | .VAR x => match S.get? x with
    | .some n => .CONST n
    | .none => .VAR x
  | .PLUS a1 a2 => mk_PLUS (cp_aexp S a1) (cp_aexp S a2)
  | .MINUS a1 a2 => mk_MINUS (cp_aexp S a1) (cp_aexp S a2)

@[grind] def cp_bexp (S : Store) (b : bexp) : bexp :=
  match b with
  | .TRUE => .TRUE
  | .FALSE => .FALSE
  | .EQUAL a1 a2 => mk_EQUAL (cp_aexp S a1) (cp_aexp S a2)
  | .LESSEQUAL a1 a2 => mk_LESSEQUAL (cp_aexp S a1) (cp_aexp S a2)
  | .NOT b => mk_NOT (cp_bexp S b)
  | .AND b1 b2 => mk_AND (cp_bexp S b1) (cp_bexp S b2)

@[grind] noncomputable def cp_com (S : Store) (c : com) : com :=
  match c with
  | .SKIP => .SKIP
  | .ASSIGN x a =>
      .ASSIGN x (cp_aexp S a)
  | .SEQ c1 c2 =>
      .SEQ (cp_com S c1) (cp_com (Cexec S c1) c2)
  | .IFTHENELSE b c1 c2 =>
      mk_IFTHENELSE (cp_bexp S b) (cp_com S c1) (cp_com S c2)
  | .WHILE b c =>
      let sfix := Cexec S (.WHILE b c)
      mk_WHILE (cp_bexp sfix b) (cp_com sfix c)

@[grind] inductive star (R : α → α → Prop) : α → α → Prop where
  | star_refl : ∀ x : α, star R x x
  | star_step : ∀ {x y z}, R x y → star R y z → star R x z

@[grind cases]
inductive plus (R : α → α → Prop) : α → α → Prop where
| plus_left : ∀ {a b c}, R a b → star R b c → plus R a c


grind_pattern plus.plus_left => star R b c, plus R a c

@[grind] def irred (R : α → α → Prop) (a : α) : Prop := ∀ b, ¬(R a b)

def all_seq_inf (R : α → α → Prop) (x : α) : Prop :=
  ∀ y : α, star R x y → ∃ z, R y z

def infseq_with_function (R : α → α → Prop) (a: α) : Prop :=
  ∃ f : Nat → α, f 0 = a ∧ ∀ i, R (f i) (f (1 + i))

def infseq {α} (R : α → α → Prop) : α → Prop :=
  λ x : α => ∃ y, R x y ∧ infseq R y
  coinductive_fixpoint

def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
    infseq R x = ∃ y, R x y ∧ infseq R y :=

def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → infseq R x :=

abbrev IdentSet := Std.HashSet ident

instance : HasSubset IdentSet where
  Subset (a b : IdentSet) := ∀ x ∈ a, x ∈ b

noncomputable instance (a b : IdentSet) : Decidable (a ⊆ b) := Classical.propDecidable (a ⊆ b)

instance : EmptyCollection IdentSet where
  emptyCollection := Std.HashSet.emptyWithCapacity

@[grind] def fv_aexp (a : aexp) : IdentSet :=
  match a with
  | .CONST _ => ∅
  | .VAR v => Std.HashSet.instSingleton.singleton v
  | .PLUS a1 a2 =>  (fv_aexp a1) ∪ (fv_aexp a2)
  | .MINUS a1 a2 => (fv_aexp a1) ∪ (fv_aexp a2)

@[grind] def fv_bexp (b : bexp) : IdentSet :=
  match b with
  | .TRUE => ∅
  | .FALSE => ∅
  | .EQUAL a1 a2 => (fv_aexp a1) ∪ (fv_aexp a2)
  | .LESSEQUAL a1 a2 => (fv_aexp a1) ∪ (fv_aexp a2)
  | .NOT b1 => fv_bexp b1
  | .AND b1 b2 => (fv_bexp b1) ∪ (fv_bexp b2)

@[grind] def fv_com (c : com) : IdentSet :=
  match c with
  | .SKIP => ∅
  | .ASSIGN _ a => fv_aexp a
  | .SEQ c1 c2 => (fv_com c1) ∪ (fv_com c2)
  | .IFTHENELSE b c1 c2 => (fv_bexp b) ∪ ((fv_com c1) ∪ (fv_com c2))
  | .WHILE b c => (fv_bexp b) ∪ (fv_com c)

@[grind] noncomputable def deadcode_fixpoint_rec (F : IdentSet → IdentSet) (default : IdentSet) (fuel : Nat) (x : IdentSet) : IdentSet :=
  match fuel with
  | 0 => default
  | fuel + 1 =>
      let x' := F x
      if x' ⊆ x then x else deadcode_fixpoint_rec F default fuel x'

@[grind] noncomputable def deadcode_fixpoint (F : IdentSet → IdentSet) (default : IdentSet) : IdentSet :=
  deadcode_fixpoint_rec F default 20 ∅

@[grind] noncomputable def live (c : com) (L : IdentSet) : IdentSet :=
  match c with
  | .SKIP => L
  | .ASSIGN x a =>
      if x ∈ L
      then (L.erase x) ∪ (fv_aexp a)
      else L
  | .SEQ c1 c2 =>
      live c1 (live c2 L)
  | .IFTHENELSE b c1 c2 =>
       (fv_bexp b) ∪ ((live c1 L) ∪ (live c2 L))
  | .WHILE b c =>
      let L' := (fv_bexp b) ∪  L
      let default := (fv_com (.WHILE b c)) ∪ L
      deadcode_fixpoint (fun x => L' ∪ (live c x)) default

@[grind] noncomputable def dce (c : com) (L : IdentSet) : com :=
  match c with
  | .SKIP => .SKIP
  | .ASSIGN x a => if x ∈ L then .ASSIGN x a else .SKIP
  | .SEQ c1 c2 => .SEQ (dce c1 (live c2 L)) (dce c2 L)
  | .IFTHENELSE b c1 c2 => .IFTHENELSE b (dce c1 L) (dce c2 L)
  | .WHILE b c => .WHILE b (dce c (live (.WHILE b c) L))

@[grind] def agree (L : IdentSet) (s1 s2 : store) : Prop :=
  ∀ x, x  ∈ L -> s1 x = s2 x

Bool in Init.Prelude

WellFounded in Init.WF

WellFoundedRelation in Init.WF

Equiv in Mathlib.Logic.Equiv.Defs

List in Init.Prelude

List.Subperm in Batteries.Data.List.Basic

List.Pairwise in Init.Data.List.Basic

InvImage in Init.Core

Nat in Init.Prelude

Nat.lt in Init.Prelude

Nat.lt_wfRel in Init.WF

Subrelation in Init.Core

Decidable in Init.Prelude

Std.HashSet in Std.Data.HashSet.Basic

HasSubset in Init.Core

Classical.propDecidable in Init.Classical

EmptyCollection in Init.Core

Std.HashSet.emptyWithCapacity in Std.Data.HashSet.Basic

Iff in Init.Core

Std.HashSet.instSingleton in Std.Data.HashSet.Basic

BEq in Init.Prelude

Hashable in Init.Prelude

Std.HashMap in Std.Data.HashMap.Basic

Id in Init.Control.Id

Id.run in Init.Control.Id

Int in Init.Data.Int.Basic

Std.HashMap.emptyWithCapacity in Std.Data.HashMap.Basic

Std.HashMap.Equiv in Std.Data.HashMap.Basic

Option in Init.Prelude

Int.add in Init.Data.Int.Basic

Int.sub in Init.Data.Int.Basic

Repr in Init.Data.Repr

And in Init.Prelude

Exists in Init.Core

Or in Init.Prelude

String in Init.Prelude
</all_available_defs>

<all_available_lemmas>
theorem aeval_xplus1 : ∀ s x, aeval s (.PLUS (.VAR x) (.CONST 1)) > aeval s (.VAR x)

theorem aeval_free (s1 s2 a) (h : ∀ x, free_in_aexp x a → s1 x = s2 x) :
    aeval s1 a = aeval s2 a

theorem beval_OR : beval s (OR b1 b2) = beval s b1 ∨ beval s b2

theorem cexec_infinite_loop (s : store) : ¬ ∃ s', cexec s (.WHILE .TRUE .SKIP) s'

theorem cexec_bounded_sound {fuel s c s'} :
    cexec_bounded fuel s c = .some s' → cexec s c s'

theorem cexec_bounded_complete (s s' : store) (c : com) :
  cexec s c s' →
  ∃ fuel1, ∀ fuel, (fuel ≥ fuel1) → cexec_bounded fuel s c = .some s'

theorem red_progress :
  ∀ c s, c = .SKIP ∨ ∃ c', ∃ s', red (c, s) (c', s')

@[grind] theorem red_seq_steps (c2 c c' : com) (s s' : store) : star red (c, s) (c', s') → star red ((c;;c2), s) ((c';;c2), s')

theorem cexec_to_reds (s s' : store) (c : com) : cexec s c s' → star red (c, s) (.SKIP, s')

@[grind] theorem red_append_cexec (c1 c2 : com) (s1 s2 : store) (h : red (c1, s1) (c2, s2)) (h₂ : cexec s2 c2 s) :
    cexec s1 c1 s

theorem reds_to_cexec (s s' : store) (c : com) (h : star red (c, s) (.SKIP, s')) :
    cexec s c s'

theorem fixpoint_exists_1 [Monotone α F] : ∃ x : α, eq x (F x)

@[grind] theorem iterate_correct (x : α) (PRE : le x (F x)) (SMALL : ∀ z, le (F z) z -> le x z) (heq : y = iterate _ F x PRE SMALL ) : eq y (F y) ∧ ∀ z, le (F z) z → le y z

theorem fixpoint_correct :
  eq (fixpoint' F) (F (fixpoint' F)) ∧ ∀ z : α, le (F z) z → le (fixpoint' F) z

@[grind] theorem Equal_Eq' : ∀ S1 S2, (Equal S1 S2 == true) → Eq' S1 S2

@[grind] theorem Equal_nEq : ∀ S1 S2, (Equal S1 S2 == false) → ¬Eq' S1 S2

@[grind] theorem Eq_Le : ∀ S1 S2, Eq' S1 S2 → Le S1 S2

@[grind] theorem Le_trans : ∀ S1 S2 S3, Le S1 S2 → Le S2 S3 → Le S1 S3

theorem hash_set_incl_size_leq (S1 S2 : Store) : Le S2 S1 → List.Subperm (S1.toList) (S2.toList)

@[grind] theorem Le_cardinal :
  ∀ S T : Store,
  Le T S ->
  S.size <= T.size ∧ (S.size = T.size → Equal S T)

@[grind] theorem Gt_cardinal :
  ∀ S S', Gt S S' -> S.size < S'.size

theorem Gt_wf : WellFounded Gt

theorem fixpoint_join_eq : Eq' (Join Init (F (fixpoint_join Init F) )) (fixpoint_join Init F)

theorem fixpoint_join_sound : Le Init (fixpoint_join Init F) /\ Le (F (fixpoint_join Init F)) (fixpoint_join Init F)

theorem fixpoint_join_smallest :
  ∀ S, Le (Join Init (F S)) S -> Le (fixpoint_join Init F) S

@[grind] theorem Join_increasing :
  ∀ S1 S2 S3 S4,
  Le S1 S2 -> Le S3 S4 -> Le (Join S1 S3) (Join S2 S4)

@[grind] theorem Aeval_increasing : ∀ S1 S2, Le S1 S2 ->
  ∀ a n, Aeval S2 a = .some n -> Aeval S1 a =.some n

@[grind] theorem Beval_increasing : ∀ S1 S2, Le S1 S2 ->
  ∀ b n, Beval S2 b = .some n -> Beval S1 b = .some n

theorem Update_increasing :
  ∀ S1 S2 x a,
  Le S1 S2 ->
  Le (Update x (Aeval S1 a) S1) (Update x (Aeval S2 a) S2)

theorem fixpoint_join_increasing (_ : Store) (F : Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) (S1 S2 : Store) : le S1 S2 → le (fixpoint_join' S1 F F_mon) (fixpoint_join' S2 F F_mon)

@[grind =] theorem codelen_singleton : codelen [i] = 1

@[grind] theorem instr_at_app :
  ∀ i c2 c1 pc,
  pc = codelen c1 ->
  instr_at (c1 ++ (i :: c2)) pc = .some i

theorem code_at_head :
  ∀ C pc i C',
  code_at C pc (i :: C') ->
  instr_at C pc = .some i

@[grind] theorem code_at_tail :
   ∀ C pc i C',
  code_at C pc (i :: C') →
  code_at C (pc + 1) C'

@[grind] theorem code_at_app_left :
  ∀ C pc C1 C2,
  code_at C pc (C1 ++ C2) ->
  code_at C pc C1

@[grind] theorem code_at_app_right2 : ∀ C pc C1 C2 C3,
  code_at C pc (C1 ++ C2 ++ C3) →
  code_at C (pc + codelen C1) C2

@[grind] theorem code_at_nil : ∀ C pc C1,
  code_at C pc C1 -> code_at C pc []

@[grind] theorem instr_at_code_at_nil :
  ∀ C pc i, instr_at C pc = .some i -> code_at C pc []

theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s c s') :
 ∀ C pc stk, code_at C pc (compile_com c) →
  transitions C
      (pc, stk, s)
      (pc + codelen (compile_com c), stk, s')

theorem com_size_nonzero : ∀ c, (com_size c > 0)

theorem instr_at_len : instr_at (C ++ [i]) (codelen C) = .some i

@[grind] theorem mk_PLUS_CONST_sound :
  ∀ s a n, aeval s (mk_PLUS_CONST a n) = aeval s a + n

theorem mk_PLUS_sound :
  ∀ s a1 a2, aeval s (mk_PLUS a1 a2) = aeval s a1 + aeval s a2

theorem mk_MINUS_sound :
  ∀ s a1 a2, aeval s (mk_MINUS a1 a2) = aeval s a1 - aeval s a2

theorem simplif_aexp_sound : ∀ s a, aeval s (simplif_aexp a) = aeval s a

theorem mk_EQUAL_sound :
  ∀ s a1 a2, beval s (mk_EQUAL a1 a2) = (aeval s a1 = aeval s a2)

theorem mk_LESSEQUAL_sound :
  ∀ s a1 a2, beval s (mk_LESSEQUAL a1 a2) = (aeval s a1 <= aeval s a2)

theorem mk_NOT_sound :
  ∀ s b, beval s (mk_NOT b) = ¬ (beval s b)

theorem mk_AND_sound :
  ∀ s b1 b2, beval s (mk_AND b1 b2) = (beval s b1 ∧ beval s b2)

theorem cexec_mk_IFTHENELSE : ∀ s1 b c1 c2 s2,
  cexec s1 (if beval s1 b then c1 else c2) s2 ->
  cexec s1 (mk_IFTHENELSE b c1 c2) s2

theorem cexec_mk_WHILE_done : ∀ s1 b c,
  beval s1 b = false ->
  cexec s1 (mk_WHILE b c) s1

theorem cexec_mk_WHILE_loop : ∀ b c s1 s2 s3,
  beval s1 b = true -> cexec s1 c s2 -> cexec s2 (mk_WHILE b c) s3 ->
  cexec s1 (mk_WHILE b c) s3

theorem matches_Le : ∀ s S1 S2, Le S1 S2 -> matches' s S1 -> matches' s S2

theorem Le_Top : ∀ S, Le S Top

@[grind] theorem Join_characterization :
∀ S1 S2 x n,
  (Join S1 S2).get? x = .some n ↔
  S1.get? x = .some n ∧ S2.get? x = .some n

theorem Le_Join_l : ∀ S1 S2, Le S1 (Join S1 S2)

theorem  Le_Join_r : ∀ S1 S2, Le S2 (Join S1 S2)

theorem Equal_Le : ∀ S1 S2, Equal S1 S2 -> Le S1 S2

@[grind] theorem Aeval_sound :
  ∀ s S, matches' s S ->
  ∀ a n, Aeval S a = .some n -> aeval s a = n

theorem Beval_sound :
  ∀ s S, matches' s S ->
  ∀ b n, Beval S b = .some n -> beval s b = n

@[grind] theorem update_characterisation : ∀ S x N y,
  (Update x N S).get? y = if x == y then N else S.get? y

theorem matches_update : ∀ s S x n N,
  matches' s S ->
  (∀ i, N = .some i -> n = i) ->
  matches' (update x n s) (Update x N S)

theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint F init_S) :
  Le (F S) S

@[grind] theorem Cexec_sound :
  ∀ c s1 s2 S1,
  cexec s1 c s2 -> matches' s1 S1 -> matches' s2 (Cexec S1 c)

@[grind] theorem cp_aexp_sound :
  ∀ s S, matches' s S ->
  ∀ a, aeval s (cp_aexp S a) = aeval s a

theorem cp_bexp_sound :
  ∀ s S, matches' s S ->
  ∀ b, beval s (cp_bexp S b) = beval s b

theorem cp_com_correct_terminating :
  ∀ c s1 s2 S1,
  cexec s1 c s2 -> matches' s1 S1 -> cexec s1 (cp_com S1 c) s2

@[grind] theorem star_one (R : α → α → Prop) {a b : α} (h : R a b) : star R a b

@[grind] theorem star_trans {α} (R : α → α → Prop) (a b : α) (sab : star R a b) : ∀ c : α, star R b c → star R a c

@[grind ←]
theorem plus_one {a b} (h : R a b) : plus R a b

@[grind] theorem plus_star {a b} (h : plus R a b) : star R a b

@[grind] theorem plus_star_trans (R : α → α → Prop) : ∀ (a b c : α), star R a b → plus R b c → plus R a c

theorem star_plus_trans :
  ∀ a b c, star R a b -> plus R b c -> plus R a c

theorem plus_right : star R a b -> R b c -> plus R a c

theorem infseq_coinduction_principle {α} (h : α → Prop) (R : α → α → Prop)
    (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x

theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x

theorem infseq_coinduction_principle_2
    (X : α → Prop) (h₁ : ∀ (a : α), X a → ∃ b, plus R a b ∧ X b) (a : α) (rel : X a) : infseq R a

theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a

theorem star_star_inv (sab : star R a b) :
    ∀ c, star R a c → star R b c ∨ star R c b

theorem finseq_unique :
  ∀ a b b', star R a b → irred R b → star R a b' → irred R b' → b = b'

@[grind] theorem infseq_star_inv  : ∀ a b, star R a b → infseq R a → infseq R b

theorem infseq_finseq_excl : ∀ a b, star R a b → irred R b → infseq R a → False

theorem infseq_all_seq_inf : ∀ a, infseq R a → all_seq_inf R a

@[grind =] theorem subset_def (a b : IdentSet) : a ⊆ b ↔ ∀ x ∈ a, x ∈ b

@[grind] theorem union_characterisation2 (a b c : IdentSet) : a ⊆ b ∧ a ⊆ c → a ⊆ (b ∪ c)

@[grind] theorem insert_characterisation (a : IdentSet) (x : ident) : x ∈ a.insert x

@[grind] theorem  fixpoint_charact' (n : Nat) (x : IdentSet)  (F : IdentSet → IdentSet) (default : IdentSet) :
  ((F (deadcode_fixpoint_rec F default n x)) ⊆ (deadcode_fixpoint_rec F default n x)) ∨ (deadcode_fixpoint_rec F default n x = default)

theorem fixpoint_charact (F : IdentSet → IdentSet) (default : IdentSet) :
    ((F (deadcode_fixpoint F default)) ⊆ (deadcode_fixpoint F default)) ∨ (deadcode_fixpoint F default = default)

@[grind]
theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F_stable : ∀ x , x ⊆ default -> (F x) ⊆ default) : deadcode_fixpoint F default ⊆ default

@[grind]
theorem live_upper_bound :
  ∀ c L,
   (live c L) ⊆ ((fv_com c) ∪ L)

theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet)
  (eq : L' = live (.WHILE b c) L) :
  (fv_bexp b) ⊆ L' ∧ L ⊆ L' ∧ (live c L') ⊆ L'

@[grind] theorem agree_mon :
  ∀ L L' s1 s2,
  agree L' s1 s2 -> L ⊆ L' -> agree L s1 s2

@[grind] theorem aeval_agree :
  ∀ L s1 s2, agree L s1 s2 ->
  ∀ a, (fv_aexp a) ⊆ L -> aeval s1 a = aeval s2 a

theorem beval_agree :
  ∀ L s1 s2, agree L s1 s2 ->
  ∀ b, (fv_bexp b) ⊆ L -> beval s1 b = beval s2 b

theorem agree_update_live :
  ∀ s1 s2 L x v,
  agree (L.erase x) s1 s2 ->
  agree L (update x v s1) (update x v s2)

theorem agree_update_dead :
  ∀ s1 s2 L x v,
  agree L s1 s2 -> ¬x ∈ L ->
  agree L (update x v s1) s2

theorem dce_correct_terminating :
  ∀ s c s', cexec s c s' ->
  ∀ L s1, agree (live c L) s s1 ->
  ∃ s1', cexec s1 (dce c L) s1' /\ agree L s' s1'
</all_available_lemmas>

<local_ctx>
import LeroyCompilerVerificationCourse.Imp

@[grind] inductive instr : Type where
  | Iconst (n : Int)             
  | Ivar (x : ident)             
  | Isetvar (x : ident)          
  | Iadd                         
  | Iopp                         
  | Ibranch (d : Int)            
  | Ibeq (d1 : Int) (d0 : Int)   
  | Ible (d1 : Int) (d0 : Int)   
  | Ihalt                        
    deriving Repr

@[grind] def codelen (c : List instr) : Int := c.length

def stack : Type := List Int

def config : Type := Int × stack × store

@[grind] def instr_at (C : List instr) (pc : Int) : Option instr :=
  match C with
  | [] => .none
  | i :: C' => if pc = 0 then .some i else instr_at C' (pc - 1)

@[grind] inductive transition (C : List instr) : config → config → Prop where
  | trans_const : ∀ pc stk s n,
      instr_at C pc = .some (.Iconst n) →
      transition C (pc    , stk     , s)
                   (pc + 1, n :: stk, s)
  | trans_var : ∀ pc stk s x,
      instr_at C pc = .some (.Ivar x) ->
      transition C (pc    , stk       , s)
                   (pc + 1, s x :: stk, s)
  | trans_setvar : ∀ pc stk s x n,
      instr_at C pc = .some (.Isetvar x) ->
      transition C (pc    , n :: stk, s)
                   (pc + 1, stk     , update x n s)
  | trans_add : ∀ pc stk s n1 n2,
      instr_at C pc = .some (.Iadd) ->
      transition C (pc    , n2 :: n1 :: stk , s)
                   (pc + 1, (n1 + n2) :: stk, s)
  | trans_opp : ∀ pc stk s n,
      instr_at C pc = .some (.Iopp) ->
      transition C (pc    , n :: stk    , s)
                   (pc + 1, (- n) :: stk, s)
  | trans_branch : ∀ pc stk s d pc',
      instr_at C pc = .some (.Ibranch d) ->
      pc' = pc + 1 + d ->
      transition C (pc , stk, s)
                   (pc', stk, s)
  | trans_beq : ∀ pc stk s d1 d0 n1 n2 pc',
      instr_at C pc = .some (.Ibeq d1 d0) ->
      pc' = pc + 1 + (if n1 = n2 then d1 else d0) ->
      transition C (pc , n2 :: n1 :: stk, s)
                   (pc', stk            , s)
  | trans_ble : ∀ pc stk s d1 d0 n1 n2 pc',
      instr_at C pc = .some (.Ible d1 d0) ->
      pc' = pc + 1 + (if n1 ≤ n2 then d1 else d0) ->
      transition C (pc , n2 :: n1 :: stk, s)
                   (pc', stk            , s)

@[grind] def transitions (C : List instr) : config → config → Prop :=
  star (transition C)

def machine_terminates (C : List instr) (s_init : store) (s_final : store) : Prop :=
  ∃ pc, transitions C (0, [], s_init) (pc, [], s_final)
          ∧ instr_at C pc = .some .Ihalt

@[grind] def compile_aexp (a : aexp) : List instr :=
  match a with
  | .CONST n => .Iconst n :: []
  | .VAR x => .Ivar x :: []
  | .PLUS a1 a2  => (compile_aexp a1) ++ (compile_aexp a2) ++ (.Iadd :: [])
  | .MINUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ (.Iopp :: .Iadd :: [])

@[grind] def compile_bexp (b : bexp) (d1 : Int) (d0 : Int) : List instr :=
  match b with
  | .TRUE => if d1 = 0 then [] else .Ibranch d1 :: []
  | .FALSE => if d0 = 0 then [] else .Ibranch d0 :: []
  | .EQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ .Ibeq d1 d0 :: []
  | .LESSEQUAL a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ .Ible d1 d0 :: []
  | .NOT b1 => compile_bexp b1 d0 d1
  | .AND b1 b2 =>
      let code2 := compile_bexp b2 d1 d0
      let code1 := compile_bexp b1 0 (codelen code2 + d0)
      code1 ++ code2

@[grind] def compile_com (c : com) : List instr :=
  match c with
  | .SKIP =>
      []
  | .ASSIGN x a =>
      compile_aexp a ++ .Isetvar x :: []
  | .SEQ c1 c2 =>
      compile_com c1 ++ compile_com c2
  | .IFTHENELSE b ifso ifnot =>
      let code_ifso := compile_com ifso
      let code_ifnot := compile_com ifnot
      compile_bexp b 0 (codelen code_ifso + 1)
      ++ code_ifso
      ++ .Ibranch (codelen code_ifnot)
      :: code_ifnot
  | .WHILE b body =>
      let code_body := compile_com body
      let code_test := compile_bexp b 0 (codelen code_body + 1)
      code_test
      ++ code_body
      ++ .Ibranch (- (codelen code_test + codelen code_body + 1)) :: []

def compile_program (p : com) : List instr :=
  compile_com p ++ .Ihalt :: []

@[grind] inductive code_at : List instr → Int → List instr → Prop where
  | code_at_intro : ∀ C1 C2 C3 pc,
      pc = codelen C1 ->
      code_at (C1 ++ C2 ++ C3) pc C2

inductive compile_cont (C : List instr) : cont -> Int -> Prop where
  | ccont_stop : ∀ pc,
      instr_at C pc = .some .Ihalt ->
      compile_cont C .Kstop pc
  | ccont_seq : ∀ c k pc pc',
      code_at C pc (compile_com c) ->
      pc' = pc + codelen (compile_com c) ->
      compile_cont C k pc' ->
      compile_cont C (.Kseq c k) pc
  | ccont_while : ∀ b c k pc d pc' pc'',
      instr_at C pc = .some (.Ibranch d) ->
      pc' = pc + 1 + d ->
      code_at C pc' (compile_com (.WHILE b c)) ->
      pc'' = pc' + codelen (compile_com (.WHILE b c)) ->
      compile_cont C k pc'' ->
      compile_cont C (.Kwhile b c k) pc
  | ccont_branch : ∀ d k pc pc',
      instr_at C pc = .some (.Ibranch d) ->
      pc' = pc + 1 + d ->
      compile_cont C k pc' ->
      compile_cont C k pc

inductive match_config (C : List instr) : com × cont × store -> config -> Prop where
  | match_config_intro : ∀ c k st pc,
      code_at C pc (compile_com c) ->
      compile_cont C k (pc + codelen (compile_com c)) ->
      match_config C (c, k, st) (pc, [], st)

def com_size (c : com) : Nat :=
  match c with
  | .SKIP => 1
  | .ASSIGN _ _ => 1
  | (c1 ;; c2) => (com_size c1 + com_size c2 + 1)
  | .IFTHENELSE _ c1 c2 => (com_size c1 + com_size c2 + 1)
  | .WHILE _ c1 => (com_size c1 + 1)

def cont_size (k : cont) : Nat :=
  match k with
  | .Kstop => 0
  | .Kseq c k' => (com_size c + cont_size k')
  | .Kwhile _ _ k' => cont_size k'

def measure' (impconf : com × cont × store) : Nat :=
  match impconf with
  | (c, k, _) => (com_size c + cont_size k)
</local_ctx>

<target_theorem>
theorem compile_program_correct_terminating_2 :
  ∀ c s s',
  star step (c, .Kstop, s) (.SKIP, .Kstop, s') ->
  machine_terminates (compile_program c) s s' :=
</target_theorem>

