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

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

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

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

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

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

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

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

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

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

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

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

### Your task:
<all_available_defs>
inductive AExp where
  | a_num : Nat → AExp
  | a_plus : AExp → AExp → AExp
  | a_minus : AExp → AExp → AExp
  | a_mult : AExp → AExp → AExp

inductive BExp where
  | b_true : BExp
  | b_false : BExp
  | b_eq : AExp → AExp → BExp
  | b_neq : AExp → AExp → BExp
  | b_le : AExp → AExp → BExp
  | b_not : BExp → BExp
  | b_and : BExp → BExp → BExp
  | b_or : BExp → BExp → BExp

inductive AExp where
  | a_num : Nat → AExp
  | a_id : String → AExp  
  | a_plus : AExp → AExp → AExp
  | a_minus : AExp → AExp → AExp
  | a_mult : AExp → AExp → AExp

abbrev x := "x"

abbrev y := "y"

abbrev z := "z"

inductive BExp where
  | b_true : BExp
  | b_false : BExp
  | b_eq : AExp → AExp → BExp
  | b_neq : AExp → AExp → BExp
  | b_le : AExp → AExp → BExp
  | b_not : BExp → BExp
  | b_and : BExp → BExp → BExp
  | b_or : BExp → BExp → BExp

abbrev State := String → Nat

def empty : State := fun _ => 0

def update (st : State) (k : String) (v : Nat) : State :=
  fun x => if x == k then v else st x

def aeval (st : State) (a : AExp) : Nat :=
  match a with
  | a_num n => n
  | a_id x => st x
  | a_plus a₁ a₂ => (aeval st a₁) + (aeval st a₂)
  | a_minus a₁ a₂ => (aeval st a₁) - (aeval st a₂)
  | a_mult a₁ a₂ => (aeval st a₁) * (aeval st a₂)

def beval (st : State) (b : BExp) : Bool :=
  match b with
  | b_true => true
  | b_false => false
  | b_eq a₁ a₂ => (aeval st a₁) == (aeval st a₂)
  | b_neq a₁ a₂ => (aeval st a₁) != (aeval st a₂)
  | b_le a₁ a₂ => (aeval st a₁) <= (aeval st a₂)
  | b_not b₁ => not (beval st b₁)
  | b_and b₁ b₂ => and (beval st b₁) (beval st b₂)
  | b_or b₁ b₂ => or (beval st b₁) (beval st b₂)

example : aeval (update empty x 5)
    <{3 + x * 2}>
    
    = 13 := by admit /- proof elided -/

def aequiv (a₁ a₂ : AExp) : Prop :=
  ∀ (st : State), aeval st a₁ = aeval st a₂

def bequiv (b₁ b₂ : BExp) : Prop :=
  ∀ (st : State), beval st b₁ = beval st b₂

inductive NValue : Tm → Prop :=
  | nv_0 : NValue zro
  | nv_succ t : NValue t → NValue (scc t)

inductive BValue : Tm → Prop :=
  | bv_true : BValue tru
  | bv_false : BValue fls

def excluded_middle := ∀ (p : Prop), p ∨ ¬ p

def valid_hoare_triple (P : Assertion) (c : Com) (Q : Assertion) : Prop :=
  ∀ st st', P st → (st =[<[c]>]=> st') → Q st'

def sorted' (al : List Nat) := ∀ i j iv jv,
  i < j → get? al i = some iv → get? al j = some jv → iv ≤ jv

dc_asgn y <{x + z}>
      (fun st => st y = st x + st z))

inductive ValidLinearJudgment : List LinearTerm → LinearTerm → Prop :=
  | vl_hyp A : ValidLinearJudgment [A] A
  | vl_exchange Δ Δ' A :
      Permutation Δ Δ' → ValidLinearJudgment Δ A
      → ValidLinearJudgment Δ' A
  | vl_tensor_i Δ Δ' A B :
      ValidLinearJudgment Δ A → ValidLinearJudgment Δ' B
      → ValidLinearJudgment (Δ ++ Δ') (A ⊗ B)
  | vl_tensor_e Δ Δ' A B C :
      ValidLinearJudgment Δ (A ⊗ B) → ValidLinearJudgment (Δ'++[A,B]) C
      → ValidLinearJudgment (Δ ++ Δ') C
  | vl_with_i Δ A B :
      ValidLinearJudgment Δ A → ValidLinearJudgment Δ B
      → ValidLinearJudgment Δ (A & B)
  | vl_with_el Δ A B :
      ValidLinearJudgment Δ (A & B)
      → ValidLinearJudgment Δ A
  | vl_with_er Δ A B :
      ValidLinearJudgment Δ (A & B)
      → ValidLinearJudgment Δ B
  | vl_lolli_i Δ A B :
      ValidLinearJudgment (Δ++[A]) B
      → ValidLinearJudgment Δ (A ⊸ B)
  | vl_lolli_e Δ Δ' A B :
      ValidLinearJudgment Δ (A ⊸ B) → ValidLinearJudgment Δ' A
      → ValidLinearJudgment (Δ ++ Δ') B
  | vl_unit_i : ValidLinearJudgment [] l_unit
  | vl_unit_e Δ Δ' C :
      ValidLinearJudgment Δ l_unit → ValidLinearJudgment Δ' C
      → ValidLinearJudgment (Δ ++ Δ') C
  | vl_top_i Δ : ValidLinearJudgment Δ l_top
  | vl_plus_il Δ A B :
      ValidLinearJudgment Δ A
      → ValidLinearJudgment Δ (A ⊕ B)
  | vl_plus_ir Δ A B :
      ValidLinearJudgment Δ B
      → ValidLinearJudgment Δ (A ⊕ B)
  | vl_plus_e Δ Δ' A B C :
      ValidLinearJudgment Δ (A ⊕ B)
      → ValidLinearJudgment (Δ'++[A]) C → ValidLinearJudgment (Δ'++[B]) C
      → ValidLinearJudgment (Δ ++ Δ') C
  | vl_zero_e Δ Δ' C:
      ValidLinearJudgment Δ l_zero
      → ValidLinearJudgment (Δ ++ Δ') C

Prod.fst in Init.Prelude

def squaring_dec (m : Nat) : Decorated := decorated
  (fun st => st x = m) $
    dc_pre (fun st => 0 = 0 * m ∧ st x = m) $

inductive DCom :=
  | dc_skip (Q : Assertion)
  | dc_seq (d₁ d₂ : DCom)
  | dc_asgn (x : String) (a : AExp) (Q : Assertion)
  | dc_if (b : BExp) (P₁ : Assertion) (d₁ : DCom)
          (P₂ : Assertion) (d₂ : DCom) (Q : Assertion)
  | dc_while (b : BExp) (P : Assertion) (d : DCom)
              (Q : Assertion)
  | dc_pre (P : Assertion) (d : DCom)
  | dc_post (d : DCom) (Q : Assertion)

inductive BEvalR : BExp → Bool → Prop :=
   
  | e_b_true : BEvalR b_true true
  | e_b_false : BEvalR b_false false
  | e_b_eq (a₁ a₂ : AExp) (v₁ v₂ : Nat) : AEvalR a₁ v₁ → AEvalR a₂ v₂ → BEvalR (b_eq a₁ a₂) (v₁ == v₂)
  | e_b_neq (a₁ a₂ : AExp) (v₁ v₂ : Nat) : AEvalR a₁ v₁ → AEvalR a₂ v₂ → BEvalR (b_neq a₁ a₂) (v₁ != v₂)
  | e_b_le (a₁ a₂ : AExp) (v₁ v₂ : Nat) : AEvalR a₁ v₁ → AEvalR a₂ v₂ → BEvalR (b_le a₁ a₂) (v₁ <= v₂)
  | e_b_not (b : BExp) (v : Bool) : BEvalR b v → BEvalR (b_not b) (not v)
  | e_b_and (b₁ b₂ : BExp) (v₁ v₂ : Bool) : BEvalR b₁ v₁ → BEvalR b₂ v₂ → BEvalR (b_and b₁ b₂) (and v₁ v₂)
  | e_b_or (b₁ b₂ : BExp) (v₁ v₂ : Bool) : BEvalR b₁ v₁ → BEvalR b₂ v₂ → BEvalR (b_or b₁ b₂) (or v₁ v₂)

inductive True : Prop where
  | intro : True

def subtract_slowly : Com :=
  <{ while x != 0 do
       <[subtract_slowly_body]>
     end }>

inductive Step : Tm → Tm → Prop :=
  | st_plusConstConst n₁ n₂ : Step (p (c n₁) (c n₂)) (c (n₁ + n₂))
  | st_plus1 t₁ t₁' t₂ : Step t₁ t₁' → Step (p t₁ t₂) (p t₁' t₂)
  | st_plus2 v₁ t₂ t₂' : Value v₁ → Step t₂ t₂' → Step (p v₁ t₂) (p v₁ t₂')

example : collisions [3, 1, 4, 1, 5, 9, 2, 6] = 1 :=

@[simp] def postcondition_from (dec : Decorated) : Assertion :=
  match dec with
  | decorated _ d => post d

inductive CEval : Com → State → State → Prop :=
  | e_skip : ∀ st,
      CEval c_skip st st
  | e_asgn : ∀ a n x st,
      aeval st a = n
      → CEval (c_asgn x a) st (update st x n)
  | e_seq : ∀ c₁ c₂ st st' st'',
      CEval c₁ st st' → CEval c₂ st' st''
      → CEval (c_seq c₁ c₂) st st''
  | e_ifTrue : ∀ b c₁ c₂ st st',
      beval st b = true → CEval c₁ st st'
      → CEval (c_if b c₁ c₂) st st'
  | e_ifFalse : ∀ b c₁ c₂ st st',
      beval st b = false → CEval c₂ st st'
      → CEval (c_if b c₁ c₂) st st'
  | e_whileFalse : ∀ b c st,
      beval st b = false
      → CEval (c_while b c) st st
  | e_whileTrue : ∀ b c st st' st'',
      beval st b = true
      → CEval c st st'
      → CEval (c_while b c) st' st''
      → CEval (c_while b c) st st''

example : fold_constants_com
    
    <{ x := 4 + 5;
       y := x - 3;
       if (x - y) = (2 + 4) then skip
       else y := 0 end;
       if 0 <= (4 - (2 + 1)) then y := 0
       else skip end;
       while y = 0 do
         x := x + 1
       end }>
    = 
    <{ x := 9;
       y := x - 3;
       if (x - y) = 6 then skip
       else y := 0 end;
       y := 0;
       while y = 0 do
         x := x + 1
       end }> := by admit /- proof elided -/

def if_add_simple_dec : Decorated := decorated
  (fun _ => True) $
    dc_if <{x <= 0}>
      (fun st => True ∧ (st x ≤ 0))
      (dc_pre (fun st => st x + 1 ≠ st x) $

abbrev t := "t"

def balance {α : Type u} (c : Color) (l : Tree α) (k : Nat) (vk : α) (r : Tree α) : Tree α :=
  match c with
  | red => tree red l k vk r
  | black =>
    match (l, k, vk, r) with
    | (tree red (tree red a x vx b) y vy c, z, vz, d)
    | (tree red a x vx (tree red b y vy c), z, vz, d)
    | (a, x, vx, tree red (tree red b y vy c) z vz d)
    | (a, x, vx, tree red b y vy (tree red c z vz d))
        => tree red (tree black a x vx b) y vy (tree black c z vz d)
    | _ => tree black l k vk r

abbrev step_normal_form := normal_form Step

inductive AStep (st : State) : AExp → AExp → Prop :=
  | as_id : ∀ v, AStep st (a_id v) (a_num (st v))
  | as_plus1 : ∀ a₁ a₁' a₂,
      AStep st a₁ a₁'
      → AStep st (a_plus a₁ a₂) (a_plus a₁' a₂)
  | as_plus2 : ∀ v₁ a₂ a₂',
      AVal v₁ → AStep st a₂ a₂'
      → AStep st (a_plus v₁ a₂) (a_plus v₁ a₂')
  | as_plus : ∀ (v₁ v₂ : Nat),
      AStep st (a_plus (a_num v₁) (a_num v₂)) (a_num (v₁ + v₂))
  | as_minus1 : ∀ a₁ a₁' a₂,
      AStep st a₁ a₁'
      → AStep st (a_minus a₁ a₂) (a_minus a₁' a₂)
  | as_minus2 : ∀ v₁ a₂ a₂',
      AVal v₁ → AStep st a₂ a₂'
      → AStep st (a_minus v₁ a₂) (a_minus v₁ a₂')
  | as_minus : ∀ (v₁ v₂ : Nat),
      AStep st (a_minus (a_num v₁) (a_num v₂)) (a_num (v₁ - v₂))
  | as_mult1 : ∀ a₁ a₁' a₂,
      AStep st a₁ a₁'
      → AStep st (a_mult a₁ a₂) (a_mult a₁' a₂)
  | as_mult2 : ∀ v₁ a₂ a₂',
      AVal v₁ → AStep st a₂ a₂'
      → AStep st (a_mult v₁ a₂) (a_mult v₁ a₂')
  | as_mult : ∀ (v₁ v₂ : Nat),
      AStep st (a_mult (a_num v₁) (a_num v₂)) (a_num (v₁ * v₂))

local infix:90 " ==> " => AEvalR

inductive Step : Tm → Tm → Prop :=
  | st_ifTrue t₁ t₂ : Step (ite tru t₁ t₂) t₁
  | st_ifFalse t₁ t₂ : Step (ite fls t₁ t₂) t₂
  | st_if c c' t₁ t₂ :
      Step c c' → Step (ite c t₁ t₂) (ite c' t₁ t₂)
  | st_succ t₁ t₁' : Step t₁ t₁' → Step (scc t₁) (scc t₁')
  | st_pred0 : Step (prd zro) zro
  | st_predSucc v : NValue v → Step (prd (scc v)) v
  | st_pred t₁ t₁' : Step t₁ t₁' → Step (prd t₁) (prd t₁')
  | st_iszero0 : Step (iszero zro) tru
  | st_iszeroSucc v : NValue v → Step (iszero (scc v)) fls
  | st_iszero t₁ t₁' :
      Step t₁ t₁' → Step (iszero t₁) (iszero t₁')

inductive HasType : Tm → Ty → Prop :=
  | t_true : HasType tru bool
  | t_false : HasType fls bool
  | t_if t₁ t₂ t₃ T :
      HasType t₁ bool → HasType t₂ T → HasType t₃ T
      → HasType (ite t₁ t₂ t₃) T
  | t_0 : HasType zro nat
  | t_succ t₁ : HasType t₁ nat → HasType (scc t₁) nat
  | t_pred t₁ : HasType t₁ nat → HasType (prd t₁) nat
  | t_iszero t₁ : HasType t₁ nat → HasType (iszero t₁) bool

def evalF (t : Tm) : Nat :=
  match t with
  | c n => n
  | p t1 t2 => evalF t1 + evalF t2

@[simp] def empty : Multiset :=
  fun _ => 0

def append (as bs : List α) : List α :=
  match as with
  | nil        => bs
  | cons a as' => cons a (append as' bs)

Bool in Init.Prelude

inductive Ty : Type :=
  | bool : Ty
  | nat : Ty

inductive Tm : Type :=
  | c : Nat → Tm       
  | p : Tm → Tm → Tm

inductive LinearTerm : Type :=
  
  | l_atom : Prop → LinearTerm
  
  | l_lolli : LinearTerm → LinearTerm → LinearTerm
  | l_tensor : LinearTerm → LinearTerm → LinearTerm
  | l_unit : LinearTerm
  
  | l_with : LinearTerm → LinearTerm → LinearTerm
  | l_top : LinearTerm
  | l_plus : LinearTerm → LinearTerm → LinearTerm
  | l_zero : LinearTerm

example (a : AExp) (n : Nat)
    : a ==> n ↔ aeval a = n := by admit /- proof elided -/

inductive Sorted : List Nat → Prop :=
  | sorted_nil : Sorted []
  | sorted_1 x : Sorted [x]
  | sorted_cons x y l :
      x ≤ y → Sorted (y :: l) → Sorted (x :: y :: l)

def p : Prop := True

inductive Ty : Type :=
  | bool : Ty
  | nat : Ty

def empty_tree {α : Type u} : Tree α := empty

inductive Value : Tm → Prop :=
  | v_const n : Value (c n)
  | v_funny t₁ n : Value (p t₁ (c n))

example : BST ex_tree := by admit /- proof elided -/

def plus2 : Com := <{ x := x + 2 }>

def succ x :=
  match x with
  | xI p => xO (succ p)
  | xO p => xI p
  | xH => xO xH

def relation (X : Type) := X → X → Prop

def subtract_3_from_5_slowly : Com :=
  <{ x := 3;
     z := 5;
     <[subtract_slowly]> }>

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

example : optimize_plus0
      (a_plus (a_num 2)
              (a_plus (a_plus (a_num 1) (a_num 0))
                      (a_num 0)))
    = a_plus (a_num 2) (a_num 1) :=

def empty {α : Type} (default : α) : trie_table α := (default, leaf)

abbrev total_map α := Nat → α

inductive CStep : (Com × State) → (Com × State) → Prop :=
  | cs_asgnStep : ∀ st v a₁ a₁',
      AStep st a₁ a₁'
      → CStep (c_asgn v a₁, st) (c_asgn v a₁', st)
  | cs_asgn : ∀ st v (n : Nat),
      CStep (c_asgn v (a_num n), st) (c_skip, x !-> n; st)
  | cs_seqStep : ∀ st c₁ c₁' st' c₂,
      CStep (c₁, st) (c₁', st')
      → CStep (c_seq c₁ c₂, st) (c_seq c₁' c₂, st')
  | cs_seqFinish : ∀ st c₂,
      CStep (c_seq c_skip c₂, st) (c₂, st)
  | cs_ifStep : ∀ st b₁ b₁' c₁ c₂,
      BStep st b₁ b₁'
      → CStep (c_if b₁ c₁ c₂, st) (c_if b₁' c₁ c₂, st)
  | cs_ifTrue : ∀ st c₁ c₂,
      CStep (c_if b_true c₁ c₂, st) (c₁, st)
  | cs_ifFalse : ∀ st c₁ c₂,
      CStep (c_if b_false c₁ c₂, st) (c₂, st)
  | cs_while : ∀ st b₁ c₁,
      CStep (c_while b₁ c₁, st)
        (c_if b₁ (c_seq c₁ (c_while b₁ c₁)) c_skip, st)

inductive AVal : AExp → Prop :=
  | av_num : ∀ n, AVal (a_num n)

def insert {α : Type}
    (i : Positive) (a : α) (t : trie_table α) : trie_table α :=
  (Prod.fst t, ins (Prod.fst t) i a (Prod.snd t))

def implies_to_or := ∀ (p q : Prop), (p → q) → (¬p ∨ q)

def nat2pos (n : Nat) : Positive := nat2pos' n n

Or in Init.Prelude

/-
exercise (2-star)
-/
example : ∃ t, stuck t :=

@[simp] def verification_conditions_from (dec : Decorated) : Prop :=
  match dec with
  | decorated P d => verification_conditions P d

@[simp] def sort (l : List Nat) : List Nat :=
  match l with
  | [] => []
  | a :: as => insert a (sort as)

def add (m n : Nat) : Nat :=
  match n with
  | zero    => m
  | succ n' => succ (add m n')

def collisions (input : List Nat) : Nat :=
  loop input 0 (fun _ => False)

inductive Step : Tm → Tm → Prop :=
  | st_plusConstConst n₁ n₂ : Step (p (c n₁) (c n₂)) (c (n₁ + n₂))
  | st_plus1 t₁ t₁' t₂ : Step t₁ t₁' → Step (p t₁ t₂) (p t₁' t₂)
  | st_plus2 n₁ t₂ t₂' : Step t₂ t₂' → Step (p (c n₁) t₂) (p (c n₁) t₂')
  | st_ifTrue t₁ t₂ : Step (test tru t₁ t₂) t₁
  | st_ifFalse t₁ t₂ : Step (test fls t₁ t₂) t₂
  | st_if t₀ t₀' t₁ t₂ : Step t₀ t₀' → Step (test t₀ t₁ t₂) (test t₀' t₁ t₂)

instance : Add Nat where
  add := add

def atrans_sound (atrans : AExp → AExp) :=
  ∀ (a : AExp), aequiv a (atrans a)

def is_a_sorting_algorithm' (f : List Nat → List Nat) :=
  ∀ al, contents al = contents (f al) ∧ Sorted (f al)

inductive Multi {X : Type} (R : relation X) : relation X :=
  | multi_refl x : Multi R x x
  | multi_step x y z : R x y → Multi R y z → Multi R x z

inductive Value : Tm → Prop :=
  | v_const n : Value (c n)
  | v_tru : Value tru
  | v_fls : Value fls

inductive Palindrome {α : Type} : List α → Prop where
  | nil : Palindrome nil
  | single (x : α) : Palindrome (cons x nil)
  | sandwich (x : α) (xs : List α)
      : Palindrome xs → Palindrome (cons x xs ++ cons x nil)

inductive BStep (st : State) : BExp → BExp → Prop :=
  | bs_eq1 : ∀ a₁ a₁' a₂,
      AStep st a₁ a₁'
      → BStep st (b_eq a₁ a₂) (b_eq a₁' a₂)
  | bs_eq2 : ∀ v₁ a₂ a₂',
      AVal v₁ → AStep st a₂ a₂'
      → BStep st (b_eq v₁ a₂) (b_eq v₁ a₂')
  | bs_eq : ∀ (v₁ v₂ : Nat),
      BStep st (b_eq (a_num v₁) (a_num v₂))
          (if v₁ == v₂ then b_true else b_false)
  | bs_neq1 : ∀ a₁ a₁' a₂,
      AStep st a₁ a₁'
      → BStep st (b_neq a₁ a₂) (b_neq a₁' a₂)
  | bs_neq2 : ∀ v₁ a₂ a₂',
      AVal v₁ → AStep st a₂ a₂'
      → BStep st (b_neq v₁ a₂) (b_neq v₁ a₂')
  | bs_neq : ∀ (v₁ v₂ : Nat),
      BStep st (b_neq (a_num v₁) (a_num v₂))
          (if v₁ != v₂ then b_true else b_false)
  | bs_le1 : ∀ a₁ a₁' a₂,
      AStep st a₁ a₁'
      → BStep st (b_le a₁ a₂) (b_le a₁' a₂)
  | bs_le2 : ∀ v₁ a₂ a₂',
      AVal v₁ → AStep st a₂ a₂'
      → BStep st (b_le v₁ a₂) (b_le v₁ a₂')
  | bs_le : ∀ (v₁ v₂ : Nat),
      BStep st (b_le (a_num v₁) (a_num v₂))
          (if v₁ <= v₂ then b_true else b_false)
  | bs_notStep : ∀ b₁ b₁',
      BStep st b₁ b₁'
      → BStep st (b_not b₁) (b_not b₁')
  | bs_notTrue : BStep st (b_not b_true) b_false
  | bs_notFalse : BStep st (b_not b_false) b_true
  | bs_andStep : ∀ b₁ b₁' b₂,
      BStep st b₁ b₁'
      → BStep st (b_and b₁ b₂) (b_and b₁' b₂)
  | bs_andFalse : ∀ b₂,
      BStep st (b_and b_false b₂) b_false
  | bs_andTrueStep : ∀ b₂ b₂',
      BStep st b₂ b₂'
      → BStep st (b_and b_true b₂) (b_and b_true b₂')
  | bs_andTrueTrue :
      BStep st (b_and b_true b_true) b_true
  | bs_andTrueFalse :
      BStep st (b_and b_true b_false) b_false
  | bs_orStep : ∀ b₁ b₁' b₂,
      BStep st b₁ b₁'
      → BStep st (b_or b₁ b₂) (b_or b₁' b₂)
  | bs_orTrue : ∀ b₂,
      BStep st (b_or b_true b₂) b_true
  | bs_orFalseStep : ∀ b₂ b₂',
      BStep st b₂ b₂'
      → BStep st (b_or b_false b₂) (b_or b_false b₂')
  | bs_orFalseTrue :
      BStep st (b_or b_false b_true) b_true
  | bs_orFalseFalse :
      BStep st (b_or b_false b_false) b_false

Add in Init.Prelude

example : fold_constants_aexp <{(1 + 2) * x}> = <{3 * x}> := by admit /- proof elided -/

dc_post (dc_while <{x != 0}>
        (fun st => st z + (st x - 1) * st x / 2 + st x = n * (n + 1) / 2 ∧ (st x ≠ 0)) (
      dc_pre (fun st => st z + (st x - 1) * st x / 2 + st x = n * (n + 1) / 2) $ 
      dc_seq (dc_asgn y <{x}>
        (fun st => st z + (st x - 1) * st x / 2 + st x = n * (n + 1) / 2 ∧ st y = st x)) $

) (fun st => st z + st x * (st x + 1) / 2 = n * (n + 1) / 2 ∧ ¬(st x ≠ 0)))
  (fun st => st z = n * (n + 1) / 2)

inductive Positive : Type :=
  | xI : Positive → Positive
  | xO : Positive → Positive
  | xH : Positive

def le_all (x : Nat) (xs : List Nat) := List.all xs (fun y => x ≤ y)

abbrev step_normal_form := normal_form Step

dc_seq (dc_while <{y != 0}> 
          (fun st => st z + st x * (st x + 1) / 2 = n * (n + 1) / 2 ∧ (st x ≠ 0) ∧ (st y ≠ 0)) ( 
        dc_pre (fun st => st z + (st x - 1) * st x / 2 + (st x - st y) = n * (n + 1) / 2) $
        dc_seq (dc_asgn z <{z + 1}>
          (fun st => st z + (st x - 1) * st x / 2 + (st x - (st y - 1) - 2) = n * (n + 1) / 2)) $
        dc_asgn y <{y - 1}>
          (fun st => st z + (st x - 1) * st x / 2 + (st x - st y - 2) = n * (n + 1) / 2)
      ) (fun st => st z + (st x - 1) * st x / 2 + st x = (n * (n + 1) / 2) ∧ ¬(st y ≠ 0))) $

def normalizing {X : Type} (R : relation X) :=
  ∀t, ∃t', (Multi R) t t' ∧ normal_form R t'

def erase_d (dec : Decorated) : Com :=
  match dec with
  | decorated _ d => erase d

def hello := "world"

def subtract_slowly_body : Com :=
  <{ z := z - 1;
     x := x - 1 }>

/-
exercise (2-star)
-/
example : ∃ t, stuck t :=

(fun st => True ∧ ¬(st x ≤ 0))
      (dc_pre (fun st => st x - 1 ≠ st x) $

inductive Value : Tm → Prop :=
  | v_const n : Value (c n)

def lt (n m : Nat) := LEq (succ n) m

inductive Step : Tm → Tm → Prop :=
  | st_funny n : Step (c n) (p (c n) (c 0))   
  | st_plusConstConst n₁ n₂ : Step (p (c n₁) (c n₂)) (c (n₁ + n₂))
  | st_plus1 t₁ t₁' t₂ : Step t₁ t₁' → Step (p t₁ t₂) (p t₁' t₂)
  | st_plus2 v₁ t₂ t₂' : Value v₁ → Step t₂ t₂' → Step (p v₁ t₂) (p v₁ t₂')

example : is_even 2 :=

def selsort (l : List Nat) (n : Nat) : List Nat :=
  match l, n with
  | _, 0 => []  
  | [], _ => []
  | x :: tl, succ n' => let (y, tl') := select x tl; y :: selsort tl' n'

dc_asgn y <{x - 1}>
      (fun st => st y ≠ st x))
  (fun st => st y ≠ st x)

abbrev Multiset := Value → Nat

inductive Step : Tm → Tm → Prop :=
  | st_plusConstConst n₁ n₂ : Step (p (c n₁) (c n₂)) (c (n₁ + n₂))
  | st_plus1 t₁ t₁' t₂ : Step t₁ t₁' → Step (p t₁ t₂) (p t₁' t₂)
  | st_plus2 v₁ t₂ t₂' : Value v₁ → Step t₂ t₂' → Step (p v₁ t₂) (p v₁ t₂')

def fold_constants_aexp (a : AExp) : AExp :=
  match a with
  | a_num _
  | a_id _
    => a
  | a_plus a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => a_num (n1 + n2)
    | (a1', a2') => a_plus a1' a2'
  | a_minus a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => a_num (n1 - n2)
    | (a1', a2') => a_minus a1' a2'
  | a_mult a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => a_num (n1 * n2)
    | (a1', a2') => a_mult a1' a2'

inductive Eval : Tm → Nat → Prop :=
  | e_const n : Eval (c n) n
  | e_plus t₁ t₂ n₁ n₂ : Eval t₁ n₁ → Eval t₂ n₂ → Eval (p t₁ t₂) (n₁ + n₂)

def nat2pos' (n : Nat) (f : Nat) : Positive :=
  match n, f with
  | _, 0 => xH  
  | 0, _ => xH
  | _, Nat.succ f =>
    let q := Nat.div n 2;
    let r := Nat.mod n 2;
    if r == 0 then xO (nat2pos' q f) else xI (nat2pos' q f)

inductive List (α : Type u) where
  | nil  : List α
  | cons : α → List α → List α

inductive BST {α : Type u} : Tree α → Prop where
  | empty : BST empty
  | tree : ∀ c l k v r,
      ForallTree (fun x _ => x < k) l
      → ForallTree (fun x _ => x > k) r
      → BST l
      → BST r
      → BST (tree c l k v r)

inductive EmptyRel : Nat → Nat → Prop where

def insert {α : Type u} (x : Nat) (v : α) (t : Tree α) : Tree α :=
  match t with
  | empty => tree empty x v empty
  | tree l k v' r =>
      if x < k then tree (insert x v l) k v' r
      else if x > k then tree l k v' (insert x v r)
      else tree l x v r

def is_wp P c Q := ({* P *} c {* Q *}) ∧ ∀P', ({* P' *} c {* Q *}) → (P' ->> P)

def positive2nat (p : Positive) : Nat :=
  match p with
  | xI q => 1 + 2 * positive2nat q
  | xO q => 0 + 2 * positive2nat q
  | xH => 1

def optimize_0plus_aexp (a : AExp) : AExp :=
  match a with
  | a_num _ => a
  | a_id _ => a
  | a_plus (a_num 0) a₂ => optimize_0plus_aexp a₂
  | a_plus a₁ a₂ => a_plus (optimize_0plus_aexp a₁) (optimize_0plus_aexp a₂)
  | a_minus a₁ a₂ => a_minus (optimize_0plus_aexp a₁) (optimize_0plus_aexp a₂)
  | a_mult a₁ a₂ => a_mult (optimize_0plus_aexp a₁) (optimize_0plus_aexp a₂)

abbrev Value := Nat

inductive Decorated :=
  | decorated : Assertion → DCom → Decorated

@[simp] def union (a b : Multiset) : Multiset :=
  fun x => a x + b x

abbrev Assertion := State → Prop

def Abs {α : Type} (t : trie_table α) (m : total_map α) :=
  @abstract α t = m

Decidable.or_not_self in Init.PropLemmas

dc_asgn x <{x - 1}>
        (fun st => st z + st x * (st x + 1) / 2 = n * (n + 1) / 2)

inductive Com :=
  | c_skip : Com
  | c_asgn : String → AExp → Com
  | c_seq : Com → Com → Com
  | c_if : BExp → Com → Com → Com
  | c_while : BExp → Com → Com

example : contents (sort [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5])
    = contents [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] := by admit /- proof elided -/

inductive HasType : Tm → Ty → Prop :=
  | t_true : HasType tru bool
  | t_false : HasType fls bool
  | t_if t₁ t₂ t₃ T :
      HasType t₁ bool → HasType t₂ T → HasType t₃ T
      → HasType (ite t₁ t₂ t₃) T
  | t_0 : HasType zro nat
  | t_succ t₁ : HasType t₁ nat → HasType (scc t₁) nat
  | t_pred t₁ : HasType t₁ nat → HasType (prd t₁) nat
  | t_iszero t₁ : HasType t₁ nat → HasType (iszero t₁) bool

def optimize_0plus_com (c : Com) : Com :=
  match c with
  | c_skip => c_skip
  | c_asgn x a => c_asgn x (optimize_0plus_aexp a)
  | c_seq c₁ c₂ => c_seq (optimize_0plus_com c₁) (optimize_0plus_com c₂)
  | c_if b c₁ c₂ => c_if (optimize_0plus_bexp b) (optimize_0plus_com c₁) (optimize_0plus_com c₂)
  | c_while b c => c_while (optimize_0plus_bexp b) (optimize_0plus_com c)

def enqueue (q : List α) (x : α) : List α :=
  match q with
  | [] => [x]
  | head :: tail => head :: enqueue tail x

def mul (m n : Nat) : Nat :=
  match n with
  | zero    => zero 
  | succ n' => add (mul m n') m

List in Init.Prelude

def selection_sort (l : List Nat) : List Nat := selsort l (length l)

def optimize_0plus (a : AExp) : AExp :=
  match a with
  | a_num _ => a
  | a_plus (a_num 0) a₂ => optimize_0plus a₂
  | a_plus a₁ a₂ => a_plus (optimize_0plus a₁) (optimize_0plus a₂)
  | a_minus a₁ a₂ => a_minus (optimize_0plus a₁) (optimize_0plus a₂)
  | a_mult a₁ a₂ => a_mult (optimize_0plus a₁) (optimize_0plus a₂)

def length {α : Type u} (as : List α) : Nat :=
  match as with
  | nil => 0
  | cons _ as => 1 + length as

def normal_form_of t t' := (t ~~>* t') ∧ step_normal_form t'

def outer_triple_valid (dec : Decorated) :=
  {* precondition_from dec *}
    erase_d dec
  {* postcondition_from dec *}

def is_a_sorting_algorithm (f : List Nat → List Nat) :=
  ∀ al, Permutation al (f al) ∧ Sorted (f al)

dc_asgn z <{y - x}>
      (fun st => st y = st x + st z))

def mul (m n : Nat) : Nat :=
  match n with
  | zero    => zero
  | succ n' => add (mul m n') m

abbrev value (t : Tm) := BValue t ∨ NValue t

def xTimesYInZ : Com := <{ z := x * y }>

def pos2nat (n : Positive) : Nat := Nat.pred (positive2nat n)

def exp (a n : Nat) : Nat :=
   
  match n with
  | zero => succ zero 
  | succ n' => mul (exp a n') a

def dbl_neg_elim := ∀ (p : Prop), ¬¬p → p

inductive TotalRel : Nat → Nat → Prop where
  | tot_rel : ∀ n m, TotalRel n m

String in Init.Prelude

@[simp] def post (d : DCom) : Assertion :=
  match d with
  | dc_skip P => P
  | dc_seq _ d₂ => post d₂
  | dc_asgn _ _ Q => Q
  | dc_if _ _ _ _ _ Q => Q
  | dc_while _ _ _ Q => Q
  | dc_pre _ d => post d
  | dc_post _ Q => Q

inductive False : Prop where

List.Sorted in Mathlib.Deprecated.Sort

def parity_dec (m : Nat) : Decorated := decorated
  (fun st => st x = m) $
  sorry

abbrev n := "n"

inductive Step : Tm → Tm → Prop :=
  | st_plusConstConst n₁ n₂ : Step (p (c n₁) (c n₂)) (c (n₁ + n₂))
  | st_plus1 t₁ t₁' t₂ : Step t₁ t₁' → Step (p t₁ t₂) (p t₁' t₂)
  | st_plus2 n₁ t₂ t₂' : Step t₂ t₂' → Step (p (c n₁) t₂) (p (c n₁) t₂')

inductive AEvalR : State → AExp → Nat → Prop :=
  | e_a_num (st : State) (n : Nat) : AEvalR st (a_num n) n
  | e_a_id (st : State) (x : String) (n : Nat) :
      st x = n → AEvalR st (a_id x) n
  | e_a_plus (st : State) (a₁ a₂ : AExp) (n₁ n₂ : Nat) :
      AEvalR st a₁ n₁ → AEvalR st a₂ n₂ → AEvalR st (a_plus a₁ a₂) (n₁ + n₂)
  | e_a_minus (st : State) (a₁ a₂ : AExp) (n₁ n₂ : Nat) :
      AEvalR st a₁ n₁ → AEvalR st a₂ n₂ → AEvalR st (a_minus a₁ a₂) (n₁ - n₂)
  | e_a_mult (st : State) (a₁ a₂ : AExp) (n₁ n₂ : Nat) :
      AEvalR st a₁ n₁ → AEvalR st a₂ n₂ → AEvalR st (a_mult a₁ a₂) (n₁ * n₂)

@[simp] def select (x : Nat) (l : List Nat) : Nat × List Nat :=
  match l with
  | [] => (x, [])
  | hd :: tl =>
    if x <= hd
    then let (j, l') := select x tl; (j, hd :: l')
    else let (j, l') := select hd tl; (j, x :: l')

And in Init.Prelude

Prod in Init.Prelude

inductive Exists {α : Type} : (α → Prop) → Prop where
  | intro : ∀a : α, P a → Exists P

Prod.snd in Init.Prelude

def dequeue (q : List α) : List α :=
  match q with
  | [] => []
  | _ :: tail => tail

def contains {α : Type u} (x : Nat) (t : Tree α) : Bool :=
  match t with
  | empty => false
  | tree l k _ r =>
      if x < k then contains x l
      else if x > k then contains x r
      else true

Tree in Mathlib.Data.Tree.Basic

def parity x :=
  match x with
  | 0 => 0
  | 1 => 1
  | succ (succ x') => parity x'

@[simp] def maybe_swap (al : List Nat) : List Nat :=
  match al with
  | a :: b :: ar => if a > b then b :: a :: ar else al
  | _ => al

def loop : Com :=
  <{ while true do
       skip
     end }>

def if_minus_plus_dec : Decorated := decorated
  (fun _ => True) $
    dc_if <{x <= y}>
      (fun st => True ∧ st x ≤ st y )
      (dc_pre (fun st => st y = st x + (st y - st x) ) $

def assert_implies (P Q : Assertion) : Prop :=
  ∀ st, P st → Q st

List.all in Init.Data.List.Basic

abbrev multistep := Multi Step

Nat.mod in Init.Prelude

inductive AExp where
  | a_num : Nat → AExp
  | a_plus : AExp → AExp → AExp
  | a_minus : AExp → AExp → AExp
  | a_mult : AExp → AExp → AExp
  | a_div : AExp → AExp → AExp

inductive BST {α : Type u} : Tree α → Prop where
  | empty : BST empty
  | tree : ∀ l k v r,
      ForallTree (fun x _ => x < k) l
      → ForallTree (fun x _ => x > k) r
      → BST l
      → BST r
      → BST (tree l k v r)

def reverse {α : Type u} (as : List α) : List α :=
  match as with
  | nil        => nil
  | cons a as' => reverse as' ++ cons a nil

Iff in Init.Core
</all_available_defs>

<all_available_lemmas>
theorem c_seq_congruence c₁ c₁' c₂ c₂'
    : cequiv c₁ c₁' → cequiv c₂ c₂' → cequiv (c_seq c₁ c₂) (c_seq c₁' c₂')

theorem parity_lt_2 x : ¬(2 ≤ x) → parity x = x

theorem union_assoc a b c : union a (union b c) = union (union a b) c

theorem permutation_app_comm (l l' : List α)
    : Permutation (l ++ l') (l' ++ l)

theorem soundness t t' T
    : HasType t T → multistep t t' → ¬ stuck t'

theorem combined_strong_progress
    : (∀ t, Value t ∨ ∃ t', Step t t') ∨ ¬ (∀ t, Value t ∨ ∃ t', Step t t')

theorem preservation t t' T
    : HasType t T → Step t t' → HasType t' T

theorem optimize_0plus_aexp_sound : atrans_sound optimize_0plus_aexp

theorem skip_right c : cequiv <{ <[c]>; skip }> c

theorem maybe_swap_idempotent al
    : maybe_swap (maybe_swap al) = maybe_swap al

theorem tensor_dist_plus_l a b c : [] ⊩ a ⊗ (b ⊕ c) ≣ (a ⊗ b) ⊕ (a ⊗ c)

theorem always_loop_hoare Q :
    {* fun _ => True *} <{ while true do skip end }> {* Q *}

theorem maybe_swap_perm al : Permutation al (maybe_swap al)

theorem multistep_congr_2 v₁ t₂ t₂'
    : (t₂ ~~>* t₂') → (p v₁ t₂ ~~>* p v₁ t₂')

theorem preservation'' t t' T
    : HasType t T → Step t t' → HasType t' T

theorem loop_never_stops st st' : ¬(st =[ <[loop]> ]=> st')

theorem no_whiles_eqv c : no_whiles c = true ↔ No_whilesR c

theorem select_rest_length x l y r
    : select x l = (y, r) → length l = length r

theorem selection_sort_contents n l
    : length l = n → contents l = contents (selection_sort l)

theorem refl_bequiv b : bequiv b b

theorem dequeue_nonempty (x : α) (q : List α) --Hard
    : dequeue (enqueue q x) = if is_empty q then q else enqueue (dequeue q) x

theorem sym_bequiv b₁ b₂ : bequiv b₁ b₂ → bequiv b₂ b₁

theorem insert_contents x l : contents (insert x l) = contents (x :: l)

theorem and_elim_l (p q : Prop) : p ∧ q → p

theorem lookup_insert_neq {α : Type u} (d : α) (k k' : Nat) (v : α) (t : Tree α)
    : k ≠ k' → lookup d k' (insert k v t) = lookup d k' t

theorem if_minus_plus_correct : outer_triple_valid if_minus_plus_dec

theorem refl_aequiv a : aequiv a a

theorem and_elim_r (p q : Prop) : p ∧ q → q

theorem sort_sorted l : Sorted (sort l)

theorem sort_perm l : Permutation l (sort l)

theorem seq_assoc c₁ c₂ c₃
    : cequiv <{(<[c₁]>; <[c₂]>); <[c₃]>}> <{<[c₁]>; (<[c₂]>; <[c₃]>)}>

theorem look_ins_same' {α} d k (v : α) : ∀ t, look d k (ins d k v t) = v

theorem nat_canonical t : HasType t nat → value t → NValue t

theorem balanceP {α : Type u} (P : Nat → α → Prop) c (l : Tree α) k vk (r : Tree α)
    : ForallTree P l → ForallTree P r → P k vk
      → ForallTree P (balance c l k vk r)

theorem multi_R (X : Type) (R : relation X) x y : R x y → Multi R x y

theorem permutation_nil_app_cons (l l' : List α) x
  : ¬ Permutation [] (l++x::l')

theorem swap_correct m n : outer_triple_valid (swap_dec m n)

theorem tensor_dist_into_with_r a b c : [] ⊩ (a & b) ⊗ c ⊸ (a ⊗ c) & (b ⊗ c)

theorem ins_not_empty {α : Type u} (k : Nat) (vk : α) (t : Tree α)
    : ins k vk t ≠ empty

theorem insert_BST {α : Type u} (t : Tree α) k vk
    : BST t → BST (insert k vk t)

theorem same_contents_iff_perm al bl
    : contents al = contents bl ↔ Permutation al bl

theorem par_body_n__Sn n st
    : st x = n ∧ st y = 0
      → Multi CStep (par_loop, st) (par_loop, x !-> n + 1; st)

theorem dec_while_correct : outer_triple_valid dec_while

theorem if_add_simple_correct : outer_triple_valid if_add_simple_dec

theorem permutation_app_head (l tl tl' : List α)
    : Permutation tl tl' → Permutation (l++tl) (l++tl')

theorem par_body_n n st
    : st x = 0 ∧ st y = 0
      → ∃ st', Multi CStep (par_loop, st) (par_loop, st')
          ∧ st' x = n ∧ st' y = 0

theorem refl_cequiv c : cequiv c c

theorem c_asgn_congruence x a a'
    : aequiv a a' → cequiv <{x := <[a]>}> <{x := <[a']>}>

theorem add_succ (m n : Nat) : m + succ n = succ (m + n)

theorem forall_insert_of_forall {α : Type u} (P : Nat → α → Prop) (t : Tree α)
    : ForallTree P t → ∀ k v, P k v → ForallTree P (insert k v t)

theorem lookup_relate {α} i (t : trie_table α) m
    : is_trie t → Abs t m → lookup i t = m (pos2nat i)

theorem select_smallest al bl x y : select x al = (y, bl) → le_all y bl

theorem look_leaf' α (d : α) j : look d j leaf = d

theorem add_cumul' n : n ≠ 0 → n * (n + 1) / 2 = n * (n - 1) / 2 + n

theorem insert_relate {α} k (v : α) t cts
    : is_trie t → Abs t cts
      → Abs (insert k v t) (update cts (pos2nat k) v)

theorem hoare_skip P : {* P *} <{skip}> {* P *}

theorem unit_lolli_ident_l a : [] ⊩ l_unit ⊸ a ≣ a

theorem bool_canonical t : HasType t bool → value t → BValue t

theorem add_comm (m n : Nat) : m + n = n + m

theorem length_append (as bs : List α)
        : length (append as bs) = length as + length bs

theorem optimize_plus0_sound (a : AExp)
    : aeval (optimize_plus0 a) = aeval a

theorem perm_contents al bl
    : Permutation al bl → contents al = contents bl

theorem insertion_sort_correct : is_a_sorting_algorithm sort

theorem insert_sorted' a l : Sorted l → Sorted (insert a l)

theorem permutation_length_1_inv a (l : List α)
    : Permutation [a] l → l = [a]

theorem neg_dist' e n : n ≠ 0 -> e - n + 1 = e - (n - 1)

theorem le_all__le_one lst y n : le_all y lst → elem n lst → y ≤ n

theorem balance_lookup {α : Type u} (d : α) c k k' (vk : α) l r
    : BST l → BST r
      → ForallTree (fun x _ => x < k) l → ForallTree (fun x _ => k < x) r
      → lookup d k' (balance c l k vk r) =
          if k' < k then lookup d k' l
          else if k' > k then lookup d k' r
          else vk

theorem linear_curry' a b c : [(a ⊗ b) ⊸ c] ⊩ a ⊸ b ⊸ c

theorem lookup_insert_eq {α : Type u} (d : α) (k : Nat) (v : α) (t : Tree α)
    : lookup d k (insert k v t) = v

theorem modus_ponens (p q : Prop) : p -> (p -> q) -> q

theorem ex_falso_quodlibet (p : Prop) : False → p

theorem wp_invariant b c Q : valid_hoare_triple
    (fun st => wp (c_while b c) Q st ∧ beval st b) c (wp (c_while b c) Q)

theorem selection_sort_correct' : is_a_sorting_algorithm' selection_sort

theorem selection_sort_is_correct : is_a_sorting_algorithm selection_sort

theorem step_deterministic : deterministic Step

theorem append_nil (as : List α) : append as nil = as

theorem soundness t t' T
    : HasType t T → multistep t t' → ¬ stuck t'

theorem verification_correct d P
    : verification_conditions P d → {* P *} erase d {* post d *}

theorem aequiv_example
    : aequiv <{x - x}> <{0}>

theorem preservation t t' T
    : HasType t T → Step t t' → HasType t' T

theorem permutation_cons_inv (l l' : List α) a
    : Permutation (a::l) (a::l') → Permutation l l'

theorem nat2pos_injective' i j : nat2pos i = nat2pos j → i = j

theorem nil_append (as : List α) : append nil as = as

theorem plus_dist_into_with_r a b c : [] ⊩ (a & b) ⊕ c ⊸ (a ⊕ c) & (b ⊕ c)

theorem lookup_ins_eq {α : Type u} (d : α) t k vk
    : BST t → lookup d k (ins k vk t) = vk

theorem evSSSS_ev (n : Nat) : Even (succ (succ (succ (succ n)))) → Even n

theorem prog_correct' n : outer_triple_valid (prog n)

theorem subtract_slowly_outer_triple_valid m n
    : outer_triple_valid (subtract_slowly_dec m n)

theorem if_add_simple :
    -- { True }
    {* fun _ => True *}
      <{if x <= 0 then y := x + 1 else y := x - 1 end}>
    -- { y ≠ x }
    {* fun st => st y ≠ st x *}

theorem selection_sort_sorted al : Sorted (selection_sort al)

theorem hoare_consequence_post P Q Q' c :
    {* P *} c {* Q' *}
    → Q' ->> Q
    → {* P *} c {* Q *}

theorem lookup_update_eq st (x : String) (v : Nat)
    : (update st x v) x = v

theorem optimize_0plus_b_sound (b : BExp)
    : beval (optimize_0plus_b b) = beval b

theorem is_wp_simple
  : is_wp (fun st => st y ≤ 9)
          <{x := y + 1}>
          (fun st => st x ≤ 10)

theorem multistep__eval t t' : normal_form_of t t' → ∃n, t' = c n ∧ t ==> n

theorem permutation_add_inside a (l l' tl tl' : List α)
    : Permutation l l' → Permutation tl tl'
      → Permutation (l ++ a :: tl) (l' ++ a :: tl')

theorem dec_while_correct'
    : outer_triple_valid dec_while

theorem sort_contents l : contents l = contents (sort l)

theorem and_elim_l' (p q : Prop) : p ∧ q → p

theorem empty_is_trie {α} (default : α) : is_trie (empty default)

theorem par_body_n' n st
    : st x = 0 ∧ st y = 0
      → ∃ st', Multi CStep (par_loop, st) (par_loop, st')
          ∧ st' x = n ∧ st' y = 0

theorem update_overwrite x e₁ e₂ st
    : (x !-> e₂; x !-> e₁; st) = (x !-> e₂; st)

theorem nf_is_value t : normal_form Step t → Value t

theorem preservation' t t' T
    : HasType t T → Step t t' → HasType t' T

theorem mul_comm (m n : Nat) : m * n = n * m

theorem strong_progress t : Value t ∨ ∃t', Step t t'

theorem lookup_insert_neq {α : Type u} (d : α) t k vk
    : BST t → k ≠ k' → lookup d k' (insert k vk t) = lookup d k' t

theorem if_add_simple :
    -- { True }
    {* fun _ => True *}
      <{if x <= 0 then y := x + 1 else y := x - 1 end}>
    -- { y ≠ x }
    {* fun st => st y ≠ st x *}

theorem evSS_ev (n : Nat) : Even (succ (succ n)) → Even n

theorem linear_uncurry a b c : [a ⊸ b ⊸ c] ⊩ (a ⊗ b) ⊸ c

theorem excluded_middle_dbl_neg p : ¬¬(p ∨ ¬ p)

theorem dbl_neg_elim__implies_to_or : dbl_neg_elim → implies_to_or

theorem select_fst_leq al bl x y : select x al = (y, bl) → y ≤ x

theorem or_distributes_over_and_l (p q r : Prop) :
    p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)

theorem empty_tree_BST {α : Type u} : BST (@empty α)

theorem progress t T
    : HasType t T → value t ∨ ∃ t', Step t t'

theorem if_false b c₁ c₂
    : bequiv b <{false}> → cequiv <{if <[b]> then <[c₁]> else <[c₂]> end}> c₂

theorem permutation_middle2 (l₁ l₂ l₃ : List α) a b
    : Permutation (a :: b :: l₁ ++ l₂ ++ l₃) (l₁ ++ a :: l₂ ++ b :: l₃)

theorem permutation_nil (l : List α) : Permutation [] l → l = []

theorem dequeue_empty : dequeue (@empty α) = empty

theorem lolli_dist_plus_r a b c : [] ⊩ (a ⊕ b) ⊸ c ≣ (a ⊸ c) & (b ⊸ c)

theorem permutation_cons_append (l : List α) x
    : Permutation (x :: l) (l ++ [x])

theorem progress'' t T
    : HasType t T → value t ∨ ∃ t', Step t t'

theorem select_in al bl x y : select x al = (y, bl) → elem y (x :: al)

theorem permutation_refl (l : List α) : Permutation l l

theorem squaring m
    : outer_triple_valid (squaring_dec m)

theorem mul_zero (m : Nat) : m * zero = zero

theorem add_infix (m n : Nat) : m.add n = m + n

theorem exp_mul__add_exponent (a m n : Nat)
    : exp a (add m n) = mul (exp a m) (exp a n)

theorem hoare_complete P c Q : valid_hoare_triple P c Q → Derivable P c Q

theorem multi_trans (X : Type) (R : relation X) x y z
    : Multi R x y → Multi R y z → Multi R x z

theorem pos2nat_injective' p q : pos2nat p = pos2nat q → p = q

theorem look_leaf α (d : α) j : look d j leaf = d

theorem balance_BST {α : Type u} c (l : Tree α) k vk (r : Tree α)
    : ForallTree (fun x _ => x < k) l
      -> ForallTree (fun x _ => x > k) r
      -> BST l
      -> BST r
      -> BST (balance c l k vk r)

theorem bst_insert_of_bst {α : Type u} (k : Nat) (v : α) (t : Tree α)
    : BST t → BST (insert k v t)

theorem lolli_top_top a : [] ⊩ a ⊸ l_top ≣ l_top

theorem sorted_sorted' al : Sorted al → sorted' al

theorem linear_curry a b c : [(a ⊗ b) ⊸ c] ⊩ a ⊸ b ⊸ c

theorem preservation' t t' T
    : HasType t T → Step t t' → HasType t' T

theorem value_is_nf t : value t → step_normal_form t

theorem insertion_sort_correct' : is_a_sorting_algorithm' sort

theorem look_ins_same {α} d k (v : α) t : look d k (ins d k v t) = v

theorem lolli_dist_with_l a b c : [] ⊩ a ⊸ (b & c) ≣ (a ⊸ b) & (a ⊸ c)

theorem cons_append (a : α) (as bs : List α)
        : append (cons a as) bs = cons a (append as bs)

theorem skip_left c : cequiv <{ skip; <[c]> }> c

theorem pos2nat2pos p : nat2pos (pos2nat p) = p

theorem mul_assoc (m n k : Nat) : m * n * k = m * (n * k)

theorem contents_insert_other l₁ l₂ x y
    : y ≠ x → contents (l₁ ++ x :: l₂) y = contents (l₁ ++ l₂) y

theorem plus_comm a b : [] ⊩ a ⊕ b ≣ b ⊕ a

theorem or_distributes_over_and_r (p q r : Prop) :
    (p ∧ q) ∨ r ↔ (p ∨ r) ∧ (q ∨ r)

theorem is_empty_empty : is_empty (@empty α)

theorem ins_BST {α : Type u} (t : Tree α) k vk : BST t → BST (ins k vk t)

theorem nat_canonical t : HasType t nat → value t → NValue t

theorem swap_correct a₀ b₀ :
    {* fun st => st x = a₀ ∧ st y = b₀ *}
      swap_program
    {* fun st => st x = b₀ ∧ st y = a₀ *}

theorem sort_perm' l : Permutation l (sort l)

theorem zero_mul (n : Nat) : mul zero n = zero

theorem one_mul (n : Nat) : mul (succ zero) n = n

theorem LEq_transitive : ∀n m k : Nat, LEq n m → LEq m k → LEq n k

theorem exists_not_not_forall : (∃ x, ¬ p x) → (¬ ∀ x, p x)

theorem identity (p : Prop) : p → p

theorem if_add_simple_correct : outer_triple_valid if_add_simple_dec

theorem hoare_seq P Q R c₁ c₂ :
    {* Q *} c₂ {* R *} → {* P *} c₁ {* Q *} → {* P *} c_seq c₁ c₂ {* R *}

theorem with_comm a b : [] ⊩ a & b ≣ b & a

theorem step__eval t t' n
    : Step t t' → (t' ==> n) → t ==> n

theorem permutation_trans (l l' l'' : List α)
    : Permutation l l' → Permutation l' l''
      → Permutation l l''
</all_available_lemmas>

<local_ctx>
import Frap.Equiv

import Frap.Exercises.Equiv

namespace Imp

open AExp

open BExp

open Com

open CEval

def atrans_sound (atrans : AExp → AExp) :=
  ∀ (a : AExp), aequiv a (atrans a)

def btrans_sound (btrans : BExp → BExp) :=
  ∀ (b : BExp), bequiv b (btrans b)

def fold_constants_aexp (a : AExp) : AExp :=
  match a with
  | a_num _
  | a_id _
    => a
  | a_plus a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => a_num (n1 + n2)
    | (a1', a2') => a_plus a1' a2'
  | a_minus a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => a_num (n1 - n2)
    | (a1', a2') => a_minus a1' a2'
  | a_mult a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => a_num (n1 * n2)
    | (a1', a2') => a_mult a1' a2'

example : fold_constants_aexp <{(1 + 2) * x}> = <{3 * x}> := by admit /- proof elided -/

def fold_constants_bexp (b : BExp) : BExp :=
  match b with
  | b_true
  | b_false
    => b
  | b_eq a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => if n1 == n2 then b_true else b_false
    | (a1', a2') => b_eq a1' a2'
  | b_neq a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => if n1 != n2 then b_true else b_false
    | (a1', a2') => b_neq a1' a2'
  | b_le a1 a2 =>
    match (fold_constants_aexp a1, fold_constants_aexp a2) with
    | (a_num n1, a_num n2) => if n1 <= n2 then b_true else b_false
    | (a1', a2') => b_le a1' a2'
  | b_not b1 =>
    match fold_constants_bexp b1 with
    | b_true => b_false
    | b_false => b_true
    | b1' => b_not b1'
  | b_and b1 b2 =>
    match (fold_constants_bexp b1, fold_constants_bexp b2) with
    | (b_true, b_true) => b_true
    | (b_true, b_false) => b_false
    | (b_false, b_true) => b_false
    | (b_false, b_false) => b_false
    | (b1', b2') => b_and b1' b2'
  | b_or b1 b2 =>
    match (fold_constants_bexp b1, fold_constants_bexp b2) with
    | (b_true, b_true) => b_true
    | (b_true, b_false) => b_true
    | (b_false, b_true) => b_true
    | (b_false, b_false) => b_false
    | (b1', b2') => b_or b1' b2'

example : fold_constants_bexp <{true && !(false && true)}> = <{true}> := by admit /- proof elided -/
</local_ctx>

<target_theorem>
theorem fold_constants_bexp_sound : btrans_sound fold_constants_bexp :=
</target_theorem>

