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

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

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

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

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

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

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

example : optimize_0plus
      (a_plus (a_num 2)
              (a_plus (a_num 0)
                      (a_plus (a_num 0) (a_num 1))))
      
    = a_plus (a_num 2) (a_num 1) := by admit /- proof elided -/

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)

@[simp] def contents (al : List Value) : Multiset :=
  match al with
  | [] => empty
  | a :: bl => union (singleton a) (contents bl)

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 Value : Tm → Prop :=
  | v_const n : Value (c n)

inductive True : Prop where
  | intro : True

def step_normal_form := normal_form Step

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

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

inductive Tm : Type :=
  | tru : Tm
  | fls : Tm
  | ite : Tm → Tm → Tm → Tm
  | zro : Tm
  | scc : Tm → Tm
  | prd : Tm → Tm
  | iszero : Tm → Tm

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

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

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

abbrev t := "t"

abbrev step_normal_form := normal_form Step

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

def optimize_0plus_b (b : BExp) : BExp :=
  match b with
  | b_true => b
  | b_false => b
  | b_eq a₁ a₂ => b_eq (optimize_0plus a₁) (optimize_0plus a₂)
  | b_neq a₁ a₂ => b_neq (optimize_0plus a₁) (optimize_0plus a₂)
  | b_le a₁ a₂ => b_le (optimize_0plus a₁) (optimize_0plus a₂)
  | b_not b₁ => b_not (optimize_0plus_b b₁)
  | b_and b₁ b₂ => b_and (optimize_0plus_b b₁) (optimize_0plus_b b₂)
  | b_or b₁ b₂ => b_or (optimize_0plus_b b₁) (optimize_0plus_b b₂)

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

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

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

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

inductive Tree (α : Type u) where
  | empty  : Tree α
  | tree (c: Color) (l : Tree α) (k : Nat) (v : α) (r : Tree α) : Tree α

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

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

def ex_tree : Tree String :=
  tree black (tree red empty 2 "two" empty) 4 "four" (tree red empty 5 "five" empty)

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

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

def p : Prop := True

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

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

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

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

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

example : maybe_swap [1, 2, 3] = [1, 2, 3] := by admit /- proof elided -/

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

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

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

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

inductive Permutation {α : Type} : List α → List α → Prop :=
  | perm_nil : Permutation [] []
  | perm_skip x l l'
      : Permutation l l' → Permutation (x::l) (x::l')
  | perm_swap x y l : Permutation (y::x::l) (x::y::l)
  | perm_trans l l' l''
      : Permutation l l' → Permutation l' l''
        → Permutation l l''

abbrev State := String → 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 ctrans_sound (ctrans : Com → Com) :=
  ∀ (c : Com), cequiv c (ctrans c)

def normal_form {X : Type} (R : relation X) (t : X) : Prop := ¬∃t', R t t'

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

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

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

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)

Prod.fst in Init.Prelude

abbrev Multiset := Value → Nat

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'

instance : Add Nat where
  add := add

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

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

abbrev total_map α := Nat → α

abbrev y := "y"

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

dc_post (dc_while <{y != x}>
        (fun st => st z = st y * m ∧ st x = m ∧ (st y ≠ st x))
        (dc_pre (fun st => st z + st x = (st y + 1) * m ∧ st x = m) $
        dc_seq
        (dc_asgn z <{z + x}>
          (fun st => st z = (st y + 1) * m ∧ st x = m))
        (dc_asgn y <{y + 1}>
          (fun st => st z = st y * m ∧ st x = m))
    )
  (fun st => st z = st y * m ∧ st x = m ∧ ¬(st y ≠ st x)))
  (fun st => st z = m * m)

Tree in Mathlib.Data.Tree.Basic

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

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

def make_black {α : Type u} (t : Tree α) : Tree α :=
  match t with
  | empty => empty
  | tree _ l k vk r => tree black l k vk r

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

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

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

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

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

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

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

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

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

abbrev z := "z"

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

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

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

def linear_iff A B := (A ⊸ B) & (B ⊸ A)

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

@[simp] def insert (i : Nat) (l : List Nat) :=
  match l with
  | [] => [i]
  | a :: as => if i ≤ a then i :: a :: as else a :: insert i as

example : is_even 2 :=

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

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

Add in Init.Prelude

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

dc_seq
    (dc_asgn y <{0}>
        (fun st => 0 = st y * m ∧ st x = m)) $
    dc_seq
    (dc_asgn z <{0}>
        (fun st => st z = st y * m ∧ st x = m)) $

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

def listOfVec {α : Type} : ∀{n : Nat}, Vec α n → List α
  | 0, Vec.nil => []
  | _, Vec.cons a v => a :: listOfVec v

@[simp] def singleton (v : Value) : Multiset :=
  fun x => if x == v then 1 else 0

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 α

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

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 mul (m n : Nat) : Nat :=
  match n with
  | zero    => zero 
  | succ n' => add (mul m n') m

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

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

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

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

inductive Derivable : Assertion → Com → Assertion → Prop :=
  | h_skip P : Derivable P c_skip P
  | h_asgn Q x a : Derivable (fun st => Q (st[x ↦ aeval st a])) (c_asgn x a) Q
  | h_seq P c Q d R :
      Derivable Q d R → Derivable P c Q → Derivable P (c_seq c d) R
  | h_if P Q b c₁ c₂ :
      Derivable (fun st => P st ∧ beval st b) c₁ Q
      → Derivable (fun st => P st ∧ ¬(beval st b)) c₂ Q
      → Derivable P (c_if b c₁ c₂) Q
  | h_while P b c :
      Derivable (fun st => P st ∧ beval st b) c P
      → Derivable P (c_while b c) (fun st => P st ∧ ¬(beval st b))
  | h_consequence P Q P' Q' c :
      Derivable P' c Q'
      → (P ->> P')
      → (Q' ->> Q)
      → Derivable P c Q

def print_in_binary (p : Positive) : List Nat :=
  match p with
  | xI q => print_in_binary q ++ [1]
  | xO q => print_in_binary q ++ [0]
  | xH => [1]

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

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

Nat.pred in Init.Prelude

def optimize_plus_with_0 (a : AExp) : AExp :=
  optimize_plus0 (optimize_0plus a)

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

abbrev step_normal_form := normal_form Step

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

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 plus2 : Com := <{ x := x + 2 }>

def listOfVec' {α : Type} {n : Nat} : Vec α n → List α
  | Vec.nil => []
  | Vec.cons a v => a :: listOfVec' v

(fun st => st y = st x + st z)

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

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

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

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

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

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

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 x := "x"

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

Prod.snd in Init.Prelude

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

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

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

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

inductive Vec (α : Type) : Nat → Type :=
  | nil : Vec α 0
  | cons (a : α) {n : Nat} (v : Vec α n) : Vec α (n+1)

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

Decidable.or_not_self in Init.PropLemmas

String in Init.Prelude

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

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

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

inductive AEvalR : AExp → Nat → Prop :=
  | e_a_any (n : Nat) : AEvalR a_any n  
  | e_a_num (n : Nat) : AEvalR (a_num n) n
  | e_a_plus (a₁ a₂ : AExp) (n₁ n₂ : Nat) :
      AEvalR a₁ n₁ → AEvalR a₂ n₂ → AEvalR (a_plus a₁ a₂) (n₁ + n₂)
  | e_a_minus (a₁ a₂ : AExp) (n₁ n₂ : Nat) :
      AEvalR a₁ n₁ → AEvalR a₂ n₂ → AEvalR (a_minus a₁ a₂) (n₁ - n₂)
  | e_a_mult (a₁ a₂ : AExp) (n₁ n₂ : Nat) :
      AEvalR a₁ n₁ → AEvalR a₂ n₂ → AEvalR (a_mult a₁ a₂) (n₁ * n₂)

(fun st => True ∧ ¬(st x ≤ st y))
      (dc_pre (fun st => (st x + st z) =st  x + st z) $

Or in Init.Prelude

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

Bool in Init.Prelude

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

def vecOfList {α : Type} : ∀xs : List α, Vec α (List.length xs)
  | [] => Vec.nil
  | x :: xs => Vec.cons x (vecOfList xs)

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

Nat.div in Init.Prelude

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

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

def empty : State := fun _ => 0

def stuck (t: Tm) : Prop :=
  step_normal_form t ∧ ¬ value t

def app {α} n₁ (v₁ : Vec α n₁) n₂ (v₂ : Vec α n₂) : Vec α (n₁+n₂) :=
  match n₁, v₁ with
  | 0, Vec.nil => Eq.symm (Nat.zero_add n₂) ▸ v₂
  | m+1, Vec.cons a u => Nat.succ_add m n₂ ▸ Vec.cons a (app m u n₂ v₂)

Eq in Init.Prelude

abbrev multistep := Multi Step

Nat in Init.Prelude

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

List.all in Init.Data.List.Basic

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)

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 lookup {α : Type u} (d : α) (x : Nat) (t : Tree α) : α :=
  match t with
  | empty => d
  | tree _ l k v r =>
      if x < k then lookup d x l
      else if x > k then lookup d x r
      else v

List.getD in Init.Data.List.BasicAux

abbrev n := "n"

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

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

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 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, v !-> 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)
   
  | cs_par1 : ∀ st c₁ c₁' c₂ st',
      CStep (c₁, st) (c₁', st')
      → CStep (c_par c₁ c₂, st) (c_par c₁' c₂, st')
  | cs_par2 : ∀ st c₁ c₂ c₂' st',
      CStep (c₂, st) (c₂', st')
      → CStep (c_par c₁ c₂, st) (c_par c₁ c₂', st')
  | cs_parDone : ∀ st,
      CStep (c_par c_skip c_skip, st) (c_skip, st)

inductive ForallTree {α : Type u} (p : Nat → α → Prop) : Tree α → Prop where
  | empty : ForallTree p empty
  | tree : ∀ c l k v r,
      p k v → ForallTree p l → ForallTree p r
      → ForallTree p (tree c l k v r)

def relation (X : Type) := X → X → Prop
</all_available_defs>

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

theorem union_comm a b : union a b = union b a

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

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

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

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

theorem value_is_nf v : Value v → normal_form Step v

theorem identity (p : Prop) : p → p

theorem total_relation_is_total : ∀ n m : Nat, TotalRel n m

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

theorem ev_sum (n m : Nat) : Even n → Even m → Even (n + m)

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

theorem excluded_middle__dbl_neg_elim : excluded_middle → dbl_neg_elim

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

theorem trans_aequiv a₁ a₂ a₃ : aequiv a₁ a₂ → aequiv a₂ a₃ → aequiv a₁ a₃

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

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

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

theorem dequeue_empty : dequeue (@empty α) = empty

theorem refl_cequiv c : cequiv c c

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

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

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

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

theorem peek_nonempty (d x : α) (q : List α)  --Hard
    : peek d (enqueue q x) = peek x q

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

theorem step_deterministic : deterministic Step

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

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

theorem trans_cequiv c₁ c₂ c₃ : cequiv c₁ c₂ → cequiv c₂ c₃ → cequiv c₁ c₃

theorem aeval_iff_AEvalR (st : State) (a : AExp) (n : Nat)
    : AEvalR st a n ↔ aeval st a = n

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

theorem subject_expansion
    : (∀ t t' T, Step t t' ∧ HasType t' T → HasType t T)
      ∨ ¬ (∀ t t' T, Step t t' ∧ HasType t' T → HasType t T)

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

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

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

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

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

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

theorem pos2nat2pos p : nat2pos (pos2nat p) = p

theorem cons_of_small_maintains_sort bl y n
    : n = length bl → le_all y bl → Sorted (selsort bl n)
      → Sorted (y :: selsort bl n)

theorem trans_bequiv b₁ b₂ b₃ : bequiv b₁ b₂ → bequiv b₂ b₃ → bequiv b₁ b₃

theorem beval_iff_BEvalR b v
    : b ==>b v ↔ beval b = v

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

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

theorem is_wp_example
    : is_wp (fun st => st y ≤ 4)
              <{x := y + 1}>
            (fun st => st x ≤ 5)

theorem refl_bequiv b : bequiv b b

theorem sorted'_sorted al : sorted' al → Sorted al

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

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

theorem parity_ge_2 x : 2 ≤ x → parity (x - 2) = parity x

theorem optimize_0plus_aexp_sound : atrans_sound optimize_0plus_aexp

theorem selection_sort_perm l : Permutation l (selection_sort l)

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

theorem eval__multistep t n : (t ==> n) → (t ~~>* c n)

theorem reduce_to_zero_correct' :
    {* fun _ => True *}
      reduce_to_zero
    {* fun st => st x = 0 *}

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

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 is_empty_nonempty (q : List α) (x : α)
    : is_empty (enqueue q x) = false

theorem optimize_0plus_bexp_sound : btrans_sound optimize_0plus_bexp

theorem or_elim (p q r : Prop) : p ∨ q → (p → r) → (q → r) → r

theorem exp_exp__mul_exponent (a m n : Nat)
    : exp (exp a m) n = exp a (mul m n)

theorem barber_paradox : ¬(∀ x : men, shaves barber x ↔ ¬ shaves x x)

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

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

theorem sym_aequiv a₁ a₂ : aequiv a₁ a₂ → aequiv a₂ a₁

theorem empty_tree_BST (α : Type u) : BST (@empty_tree α)

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

theorem forallTree_imp {α : Type u} (P Q : Nat → α → Prop) t
    : ForallTree P t → (∀ k v, P k v → Q k v) → ForallTree Q t

theorem permutation_elt (l₁ l₂ l₁' l₂' : List α) a
    : Permutation (l₁ ++ l₂) (l₁' ++ l₂')
      → Permutation (l₁ ++ a :: l₂) (l₁' ++ a :: l₂')

theorem select_contents al bl x y
    : select x al = (y, bl)
      → union (singleton x) (contents al) = union (singleton y) (contents bl)

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

theorem or_commutative (p q : Prop) : p ∨ q ↔ q ∨ p

theorem no_whiles_eqv c : no_whiles c = true ↔ No_whilesR c

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 permutation_app_swap_app (l₁ l₂ l₃ : List α)
    : Permutation (l₁ ++ l₂ ++ l₃) (l₂ ++ l₁ ++ l₃)

theorem all_perm {α} (f : α → Bool) al bl
    : Permutation al bl → all al f → all bl f

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

theorem dbl_negation_intro (p : Prop) : p → ¬¬p

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

theorem slow_assignment m
    : outer_triple_valid (slow_assignment_dec m)

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

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

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

theorem or_intro_l (p q : Prop) : p → p ∨ q

theorem minimum_correct a b : outer_triple_valid (minimum_dec a b)

theorem optimize_plus_with_0_sound (a : AExp)
    : aeval (optimize_plus_with_0 a) = aeval a

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

theorem fold_constants_com_sound : ctrans_sound fold_constants_com

theorem reduce_to_zero_correct''' :
    {* fun _ => True *}
      reduce_to_zero
    {* fun st => st x = 0 *}

theorem Even_is_even (n : Nat) : Even n → is_even n

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

theorem squaring m
    : outer_triple_valid (squaring_dec m)

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

theorem selsort_sorted n al : length al = n → Sorted (selsort al n)

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

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

theorem forallTree_lt {α : Type u} (t : Tree α) k k'
    : ForallTree (fun x _ => x < k) t → k < k'
      → ForallTree (fun x _ => x < k') t

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

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

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

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

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

theorem fold_constants_aexp_sound : atrans_sound fold_constants_aexp

theorem Palindrome_app_rev {α : Type} (l : List α) : Palindrome (l ++ reverse l)

theorem dec_inc' n : n ≠ 0 → n - 1 + 1 = n

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

theorem optimizer_sound: ctrans_sound optimizer

theorem value_is_nf t : value t → step_normal_form t

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

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

theorem and_commutative (p q : Prop) : p ∧ q ↔ q ∧ p

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

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

theorem mul_exp__exp_mul (a b n : Nat)
    : exp (mul a b) n = mul (exp a n) (exp b n)

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

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

theorem selection_sort_sorted al : Sorted (selection_sort al)

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

theorem maybe_swap_perm al : Permutation al (maybe_swap al)

theorem ev_inversion (n : Nat)
    : Even n ↔ n = 0 ∨ ∃n' : Nat, n = succ (succ n') ∧ Even n'

theorem permutation_length (l l' : List α)
    : Permutation l l' → List.length l = List.length l'

theorem wp_is_weakest c Q P' : {* P' *} c {* Q *} → (P' ->> wp c Q)

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

theorem permutation_app_rot (l₁ l₂ l₃ : List α)
    : Permutation (l₁ ++ l₂ ++ l₃) (l₂ ++ l₃ ++ l₁)

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 selection_sort_correct' : is_a_sorting_algorithm' selection_sort

theorem permutation_trans (l l' l'' : List α)
    : Permutation l l' → Permutation l' l''
      → Permutation l l''

theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k)

theorem lookup_empty {α : Type u} (d : α) (k : Nat)
    : lookup d k empty_tree = d

theorem selection_sort_is_correct : is_a_sorting_algorithm selection_sort

theorem peek_empty (d : α) : peek d empty = d

theorem insP {α : Type u} (P : Nat → α → Prop) (t : Tree α) k vk
    : ForallTree P t → P k vk
      → ForallTree P (ins k vk t)

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

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

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 neg_dist' e n : n ≠ 0 -> e - n + 1 = e - (n - 1)

theorem hoare_asgn_weakest Q x a
    : is_wp (fun st => Q (st[x ↦ aeval st a])) <{x := <[a]>}> Q

theorem and_intro (p q : Prop) : p -> q -> p ∧ q

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

theorem step_deterministic : deterministic Step

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

theorem is_empty_empty : is_empty (@empty α)

theorem inequiv_loop_skip : ¬ cequiv loop c_skip

theorem insert_is_trie {α} i x (t : trie_table α)
    : is_trie t → is_trie (insert i x t)

theorem permutation_nil_cons (l : List α) (x : α)
    : ¬ Permutation [] (x::l)

theorem selsort_perm n l : length l = n → Permutation l (selsort l n)

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

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

theorem combined_step_deterministic
    : deterministic Step ∨ ¬ deterministic Step

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 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 nf_same_as_value t : normal_form Step t ↔ Value t

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

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

theorem update_swap x y e₁ e₂ st : x ≠ y
    → (y !-> e₂; x !-> e₁; st) = (x !-> e₁; y !-> e₂; st)

theorem verification_conditions_correct dec
    : verification_conditions_from dec → outer_triple_valid dec

theorem bequiv_example
    : bequiv <{x - x = 0}> <{true}>

theorem normal_forms_unique : deterministic normal_form_of

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

theorem subtract_slowly_outer_triple_valid m n
    : outer_triple_valid (subtract_slowly_dec m n)

theorem c_if_congruence b b' c₁ c₁' c₂ c₂'
    : bequiv b b' → cequiv c₁ c₁' → cequiv c₂ c₂'
      → cequiv (c_if b c₁ c₂) (c_if b' c₁' c₂')

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

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

theorem wp_seq P Q c₁ c₂
    : Derivable P c₁ (wp c₂ Q) → Derivable (wp c₂ Q) c₂ Q
      → Derivable P (c_seq c₁ c₂) Q

theorem or_associative (p q r : Prop) : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r)

theorem dec_while_correct : outer_triple_valid dec_while

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

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

theorem empty_relation_is_empty : ∀ n m : Nat, ¬ EmptyRel n m
</all_available_lemmas>

<local_ctx>
section rewriting

variable (α : Type) (a b c d : α)  -- a, b, c, d are elements of some type

/-
## Rewriting

Recall our equality proof from last time.
-/

example : a = b → c = b → c = d → a = d := by
  intro hab hcb hcd
  apply Eq.trans
  . exact hab
  . apply Eq.trans
    . apply Eq.symm
      exact hcb
    . exact hcd

/-
Notice that in each subgoal, we are attempting to use a hypothesis by way of an equality property.
For example, we invoke the transitive property on `a = d` so that we can use the assumption `a = b` and be left with `b = d` to prove.
In effect, we are substituting `b` for `a` in the goal.

This substitution operation can be seen as rewriting some term in the goal with another, via an equality in the hypothesis.
This rewriting operation is so common that Lean provides a `rw` tactic to do so.
It replaces equals for equals, which could be an equality (`=`) or equivalence (`↔`).

Be default, it rewrites the left-hand side with the right-hand side.
For right-to-left rewriting, a left arrow needs to be indicated before the hypothesis (`←`, typed with `\<-` shortcut) .
-/

example : a = b → c = b → c = d → a = d := by
  intro hab hcb hcd
  rw [hab]
  rw [← hcd]
  rw [hcb]

end rewriting

/-
## reflexivity tactic

One of the most powerful tactics is the _reflexivity_ tactic, written `rfl` in Lean.
It will attempt to conclude that both sides of an equality goal is indeed equal, up to some trivial computation, such as expansion of definitions and function applications.
-/

example : 2 + 5 = 7 := by
  rfl

example : ¬ Even = 3 := by
  intro h
  sorry

namespace Hidden

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

namespace Nat

end Nat

end Hidden

section opendemo

open Nat

end opendemo

namespace Hidden

namespace Nat

end Nat

end Hidden

namespace Hidden

namespace Nat
</local_ctx>

<target_theorem>
theorem add_comm (m n : Nat) : m + n = n + m :=
</target_theorem>

