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>
example : collisions [3, 1, 4, 1, 5, 9, 2, 6] = 1 :=

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

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

abbrev Multiset := Value → Nat

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

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 Tm : Type :=
  | c : Nat → Tm       
  | p : Tm → Tm → Tm

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

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

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

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

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

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

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

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

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)

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

def btrans_sound (btrans : BExp → BExp) :=
  ∀ (b : BExp), bequiv b (btrans 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₁')

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

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

inductive True : Prop where
  | intro : True

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

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

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

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

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

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

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)

abbrev t := "t"

abbrev step_normal_form := normal_form Step

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 empty : Multiset :=
  fun _ => 0

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

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

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

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

Add in Init.Prelude

abbrev State := String → Nat

instance : Add Nat where
  add := add

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

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

def p : Prop := True

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

String in Init.Prelude

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

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

Decidable.or_not_self in Init.PropLemmas

Append in Init.Prelude

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

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

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

def three := xI xH

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

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

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

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

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

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 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 listOfVec' {α : Type} {n : Nat} : Vec α n → List α
  | Vec.nil => []
  | Vec.cons a v => a :: listOfVec' v

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

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

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

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)

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

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

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 → α

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

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

Prod.fst in Init.Prelude

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

Tree in Mathlib.Data.Tree.Basic

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

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

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

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

def hello := "world"

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

Bool in Init.Prelude

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

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

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

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

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

abbrev z := "z"

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

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'

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

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

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

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

example : is_even 2 :=

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

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

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

def step_normal_form := normal_form Step

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

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

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

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

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

def ctrans_sound (ctrans : Com → Com) :=
  ∀ (c : Com), cequiv c (ctrans c)

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

abbrev step_normal_form := normal_form Step

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]

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

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

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

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'

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

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

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

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

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

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

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

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

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

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

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

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 Eq {α : Type} : α → α → Prop where
  | refl : ∀a : α, Eq a a

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

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

Nat.pred in Init.Prelude

Prod.snd in Init.Prelude

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

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

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 fold_constants_com (c : Com) : Com :=
  match c with
  | c_skip => c
  | c_asgn x a => c_asgn x (fold_constants_aexp a)
  | c_seq c1 c2 => c_seq (fold_constants_com c1) (fold_constants_com c2)
  | c_if b c1 c2 =>
    match fold_constants_bexp b with
    | b_true => fold_constants_com c1
    | b_false => fold_constants_com c2
    | b' => c_if b' (fold_constants_com c1) (fold_constants_com c2)
  | c_while b c1 =>
    match fold_constants_bexp b with
    | b_true => loop
    | b_false => c_skip
    | b' => c_while b' (fold_constants_com c1)

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

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

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

List in Init.Prelude
</all_available_defs>

<all_available_lemmas>
theorem with_comm a b : [] ⊩ a & b ≣ b & a

theorem sorted_sorted' al : Sorted al → sorted' al

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

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

theorem minimum_correct a b : outer_triple_valid (minimum_dec a b)

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

theorem ev_double (n : Nat) : Even (double n)

theorem inequiv_loop_skip : ¬ cequiv loop c_skip

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

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

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

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

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

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

theorem selection_sort_perm l : Permutation l (selection_sort l)

theorem insertion_sort_correct' : is_a_sorting_algorithm' sort

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

theorem contents_cons_inv l x n
    : succ n = contents l x
      → ∃ l₁ l₂, l = l₁ ++ x :: l₂ ∧ contents (l₁ ++ l₂) x = n

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

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 value_is_nf t : value t → step_normal_form t

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

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

theorem wp_is_precondition c Q : {* wp c Q *} c {* Q *}

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

theorem maybe_swap_perm al : Permutation al (maybe_swap al)

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

theorem refl_cequiv c : cequiv c c

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

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 optimize_plus0_sound (a : AExp)
    : aeval (optimize_plus0 a) = aeval a

theorem hoare_post_true P Q c : (∀ st, Q st) → {* P *} c {* Q *}

theorem selection_sort_is_correct : is_a_sorting_algorithm selection_sort

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

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

theorem fold_constants_aexp_sound : atrans_sound fold_constants_aexp

theorem zero_add (n : Nat) : zero + n = n

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

theorem append_assoc (as bs cs : List α)
        : append (append as bs) cs = append as (append bs cs)

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

theorem LEq_reflexive : ∀n : Nat, LEq n n

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

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

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

theorem if_minus_plus_correct : outer_triple_valid if_minus_plus_dec

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

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

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

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

theorem optimize_0plus_aexp_sound : atrans_sound optimize_0plus_aexp

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

theorem refl_bequiv b : bequiv b b

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

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

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

theorem parity_outer_triple_valid m
    : outer_triple_valid (parity_dec m)

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

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

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

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

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

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

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

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

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

theorem vl_subst Δ Δ' a c :
    (Δ ⊩ a) → (Δ' ++ [a] ⊩ c)
    → (Δ ++ Δ' ⊩ c)

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

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

theorem add_zero (m : Nat) : m + zero = m

theorem normal_forms_unique : deterministic normal_form_of

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

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

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

theorem mod_two_Eq_zero_of_Even (n : Nat) : Even n → n % 2 = 0

theorem is_empty_nonempty (q : List α) (x : α)
    : is_empty (enqueue q x) = false

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

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

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

theorem plus2_spec n st st' :
    st x = n
    → (st =[ <[plus2]> ]=> st')
    → st' x = n + 2

theorem nf_is_value t : normal_form Step t → Value t

theorem identity (p : Prop) : p → p

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

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

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

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

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

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

theorem ex_falso_quodlibet (p : Prop) : False → p

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 multistep_congr_2 v₁ t₂ t₂'
    : (t₂ ~~>* t₂') → (p v₁ t₂ ~~>* p v₁ t₂')

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

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

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

theorem nat2pos2nat i : pos2nat (nat2pos i) = i

theorem dbl_negation_elim (p : Prop) : ¬p ↔ ¬¬¬p

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

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

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

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

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

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

theorem optimize_0plus_bexp_sound : btrans_sound optimize_0plus_bexp

theorem empty_relate {α} (default : α)
    : Abs (empty default) (fun _ => default)

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

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 if_false b c₁ c₂
    : bequiv b <{false}> → cequiv <{if <[b]> then <[c₁]> else <[c₂]> end}> c₂

theorem aeval_iff_AEvalR (a : AExp) (n : Nat)
    : a ==> n ↔ aeval a = n

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

theorem h_consequence_post P Q Q' c
    : Derivable P c Q' → (Q' ->> Q) → Derivable P c Q

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

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

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

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

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

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

theorem empty_relation_is_empty : ∀ n m : Nat, ¬ EmptyRel n m

theorem look_ins_other {α} d j k (v : α) t
    : j ≠ k → look d j (ins d k v t) = look d j t

theorem step_normalizing : normalizing Step

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

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

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

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

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 and_distributes_over_or (p q r : Prop) :
    p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)

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

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

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

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

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 value_is_nf v : Value v → normal_form Step v

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 permutation_length (l l' : List α)
    : Permutation l l' → List.length l = List.length l'

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

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

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

theorem is_empty_empty : is_empty (@empty α)

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

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

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

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

theorem squaring m
    : outer_triple_valid (squaring_dec m)

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

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

theorem if_add_simple_correct : outer_triple_valid if_add_simple_dec

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

theorem implies_to_or__excluded_middle : implies_to_or → excluded_middle

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

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

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

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

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

theorem selection_sort_sorted al : Sorted (selection_sort al)

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

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 or_elim (p q r : Prop) : p ∨ q → (p → r) → (q → r) → r

theorem dequeue_empty : dequeue (@empty α) = empty

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

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

theorem slow_assignment m
    : outer_triple_valid (slow_assignment_dec m)

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

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

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

theorem sort_specifications_equivalent sort
    : is_a_sorting_algorithm sort ↔ is_a_sorting_algorithm' sort

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

theorem h_consequence_pre P Q P' c
    : (Derivable P' c Q) → (P ->> P') → (Derivable P c Q)

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 unit_lolli_ident_l a : [] ⊩ l_unit ⊸ a ≣ a

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

theorem ev5_nonsense : Even 5 → 2 + 2 = 9

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

theorem and_associative (p q r : Prop) : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r)

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

theorem step_deterministic : deterministic Step

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

theorem tensor_comm a b : [] ⊩ a ⊗ b ≣ b ⊗ a

theorem insert_perm x l : Permutation (x :: l) (insert x l)
</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

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

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 mul_assoc (m n k : Nat) : m * n * k = m * (n * k) :=
</target_theorem>

