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

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

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

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

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

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

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

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

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

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

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

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

### Your task:
<all_available_defs>
def empty {α : Type u} : List α :=
  []

def is_empty (q : List α) : Bool :=
  match q with
  | [] => true
  | _ :: _ => false

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

def peek (default : α) (q : List α) : α :=
  match q with
  | [] => default
  | head :: _ => head

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

def p : Prop := True

def q : Prop := False

def minimum_dec (a b : Nat) : Decorated := decorated
  (fun _ => True) $
    dc_pre (fun st => 0 + min a b = min a b) $
    dc_seq (dc_asgn x (a_num a)
      (fun st => 0 + min (st x) b = min a b)) $
    dc_seq (dc_asgn y (a_num b)
      (fun st => 0 + min (st x) (st y) = min a b )) $
    dc_seq (dc_asgn z <{0}>
      (fun st => st z + min (st x) (st y) = min a b )) $
    dc_post (dc_while <{x != 0 && y != 0}>
        (fun st => (st z) + (min (st x) (st y)) = min a b ∧ (st x ≠ 0 && st y ≠ 0) )
        (dc_pre (fun st => (st z + 1) + (min (st x - 1) (st y - 1)) = min a b) $
      dc_seq (dc_asgn x <{x - 1}> (fun st => (st z + 1) + (min (st x) (st y - 1)) = min a b)) $
      dc_seq (dc_asgn y <{y - 1}> (fun st => (st z + 1) + (min (st x) (st y)) = min a b)) $
      dc_asgn z <{z + 1}> (fun st => (st z) + (min (st x) (st y)) = min a b)
      ) (fun st => st z + (min (st x) (st y)) = min a b ∧ ¬(st x ≠ 0 && st y ≠ 0)))
  (fun st => st z = min a b)

abbrev t := "t"

def swap_program : Com := <{
  t := x;
  x := y;
  y := t
}>

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

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

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

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

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

abbrev step_normal_form := normal_form Step

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

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

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

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

abbrev multistep := Multi Step

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

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

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

instance : Add Nat where
  add := add

instance : Mul Nat where
  mul := mul

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

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

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)

 

example :
    optimize_0plus_com <{ while x != 0 do x := 0 + x - 1 end }>
    = <{ while x != 0 do x := x - 1 end }> := by admit /- proof elided -/

def optimizer (c : Com) := optimize_0plus_com (fold_constants_com c)

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

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

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

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

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

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

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

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  

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

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 : BST ex_tree := by admit /- proof elided -/

def no_whiles (c : Com) : Bool :=
  match c with
  | c_skip => true
  | c_asgn _ _ => true
  | c_seq c₁ c₂ => and (no_whiles c₁) (no_whiles c₂)
  | c_if _ c₁ c₂ => and (no_whiles c₁) (no_whiles c₂)
  | c_while _ _ => false

inductive No_whilesR : Com → Prop :=
   
  | nw_skip  : No_whilesR Com.c_skip
  | nw_asgn  : ∀ (x : String) (e : AExp), No_whilesR (c_asgn x e)
  | nw_seq   : ∀ (c1 c2 : Com), No_whilesR c1 → No_whilesR c2 → No_whilesR (c_seq c1 c2)
  | nw_if    : ∀ (b : BExp) (c1 c2 : Com), No_whilesR c1 → No_whilesR c2 → No_whilesR (c_if b c1 c2)
  | nw_while : ∀ (b : BExp) (c : Com), false → No_whilesR (c_while b c)

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

inductive Even : Nat → Prop where
  | ev_zero : Even 0
  | ev_add_two (n : Nat) : Even n → Even (n + 2)

def double (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | succ n' => succ (succ (double n'))

inductive And : Prop → Prop → Prop where
  | intro : a → b → And a b

inductive Or : Prop → Prop → Prop where
  | inl : a → Or a b
  | inr : b → Or a b

inductive Iff : Prop → Prop → Prop where
  | intro : (a → b) → (b → a) → Iff a b

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

inductive True : Prop where
  | intro : True

inductive False : Prop where

inductive Eq {α : Type} : α → α → Prop where
  | refl : ∀a : α, Eq a a

def is_even (x : Nat) := ∃n : Nat, x = double n

example : is_even 2 :=

inductive LEq : Nat → Nat → Prop where
  | le_n (n : Nat) : LEq n n
  | le_S (n m : Nat) : LEq n m → LEq n (succ m)

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

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

inductive EmptyRel : Nat → Nat → Prop where

def reduce_to_zero : Com :=
  <{
    while x != 0 do
      x := x - 1

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

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

def dec_while : Decorated := decorated (fun _ => True) (
  dc_post (
    dc_while <{x != 0}> (fun st => True ∧ st x ≠ 0) (
      dc_pre (fun _ => True) $
      dc_asgn x <{x - 1}> (fun _ => True)
    ) (fun st => True ∧ ¬(st x ≠ 0))
  ) (fun st => st x = 0)
)

@[simp] def erase (d : DCom) : Com :=
  match d with
  | dc_skip _ => c_skip
  | dc_seq d₁ d₂ => c_seq (erase d₁) (erase d₂)
  | dc_asgn x a _ => c_asgn x a
  | dc_if b _ d₁ _ d₂ _ => c_if b (erase d₁) (erase d₂)
  | dc_while b _ d _ => c_while b (erase d)
  | dc_pre _ d => erase d
  | dc_post d _ => erase d

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

@[simp] def precondition_from (dec : Decorated) : Assertion :=
  match dec with
  | decorated P _ => P

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

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

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

@[simp] def verification_conditions (P : Assertion) (d : DCom) : Prop :=
  match d with
  | dc_skip Q =>
      P ->> Q
  | dc_seq d₁ d₂ =>
      verification_conditions P d₁
      ∧ verification_conditions (post d₁) d₂
  | dc_asgn x a Q =>
      (P ->> fun st => Q (st[x ↦ aeval st a]))
  | dc_if b P₁ d₁ P₂ d₂ Q =>
      ((fun st => P st ∧ beval st b) ->> P₁)
      ∧ ((fun st => P st ∧ ¬(beval st b)) ->> P₂)
      ∧ (post d₁ ->> Q) ∧ (post d₂ ->> Q)
      ∧ verification_conditions P₁ d₁
      ∧ verification_conditions P₂ d₂
  | dc_while b Q d R =>
      
      (P ->> post d)
      ∧ ((fun st => post d st ∧ beval st b) ->> Q)
      ∧ ((fun st => post d st ∧ ¬(beval st b)) ->> R)
      ∧ verification_conditions Q d
  | dc_pre Q d =>
      (P ->> Q)
      ∧ verification_conditions Q d
  | dc_post d Q =>
      verification_conditions P d
      ∧ (post d ->> Q)

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

def swap_dec (m n : Nat) : Decorated := decorated
  (fun st => st x = m ∧ st y = n) $
  dc_pre (fun st => (st x + st y) - ((st x + st y) - st y) = n
                    ∧ (st x + st y) - st y = m) $
  dc_seq (
    dc_asgn x <{x + y}> (fun st => st x - (st x - st y) = n ∧ (st x - st y) = m)
  ) $
  dc_seq (
    dc_asgn y <{x - y}> (fun st => st x - st y = n ∧ st y = m)
  ) $
  dc_asgn x <{x - y}> (fun st => st x = n ∧ st y = m)

inductive AVal : AExp → Prop :=
  | av_num : ∀ n, AVal (a_num 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₂))

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

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

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)

def par_loop : Com :=
  c_par
    (c_asgn y (a_num 1))
    (c_while (b_eq (a_id y) (a_num 0))
      (c_asgn x (a_plus (a_id x) (a_num 1))))

/-
In particular, it can terminate with `x` set to `0`.
-/

example : ∃ st',
    Multi CStep (par_loop, empty) (c_skip, st')
    ∧ st' x = 0 :=

abbrev total_map α := Nat → α

def update (t : total_map α) (k : Nat) (v : α) : total_map α :=
  fun x => if x == k then v else t x

def loop (input : List Nat) (c : Nat) (table : Nat → Bool) : Nat :=
  match input with
  | [] => c
  | a::al => if table a then loop al (c+1) table
                        else loop al c (update table a True)

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

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

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

def ten := xO (xI (xO xH))

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

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]

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

inductive Z : Type :=
  | Z₀ : Z
  | Zpos : Positive → Z
  | Zneg : Positive → Z

inductive Trie (α : Type) :=
  | leaf : Trie α
  | node : Trie α → α → Trie α → Trie α

def trie_table (α : Type) : Type := α × Trie α

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

def look {α : Type} (default : α) (i : Positive) (m : Trie α) : α :=
  match m with
  | leaf => default
  | node l x r =>
    match i with
    | xH => x
    | xO i' => look default i' l
    | xI i' => look default i' r

def lookup {α : Type} (i : Positive) (t : trie_table α) : α :=
  look (Prod.fst t) i (Prod.snd t)

def ins {α : Type} (default : α) (i : Positive) (a : α) (m : Trie α) : Trie α :=
  match m with
  | leaf =>
    match i with
    | xH => node leaf a leaf
    | xO i' => node (ins default i' a leaf) default leaf
    | xI i' => node leaf default (ins default i' a leaf)
  | node l o r =>
    match i with
    | xH => node l a r
    | xO i' => node (ins default i' a l) o r
    | xI i' => node l o (ins default i' a r)

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

def three := xI xH

def three_ten : trie_table Bool :=
  insert three True (insert ten True (empty False))

def loop (input : List Positive) (c : Nat) (table : trie_table Bool) : Nat :=
  match input with
  | [] => c
  | a::al => if lookup a table
                then loop al (c+1) table
                else loop al c (insert a True table)

def collisions (input : List Positive) := loop input 0 (empty False)

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)

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

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

def is_trie {α : Type} (t : trie_table α) : Prop :=
   
  sorry

def abstract {α : Type} {t : trie_table α} (n : Nat) : α :=
  lookup (nat2pos n) t

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

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

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

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 beval (b : BExp) : Bool :=
  match b with
  | b_true => true
  | b_false => false
  | b_eq a₁ a₂ => (aeval a₁) == (aeval a₂)
  | b_neq a₁ a₂ => (aeval a₁) != (aeval a₂)
  | b_le a₁ a₂ => (aeval a₁) <= (aeval a₂)
  | b_not b₁ => not (beval b₁)
  | b_and b₁ b₂ => and (beval b₁) (beval b₂)
  | b_or b₁ b₂ => or (beval b₁) (beval b₂)

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

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

def optimize_plus0 (a : AExp) : AExp :=
  sorry

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

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

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

 

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

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

inductive 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₂)
  | e_a_div (a₁ a₂ : AExp) (n₁ n₂ n₃ : Nat) :  
      AEvalR a₁ n₁ → AEvalR a₂ n₂ → n₂ > 0
      → n₂ * n₃ = n₁ → AEvalR (a_div a₁ a₂) n₃

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

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

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

abbrev w := "w"

abbrev x := "x"

abbrev y := "y"

abbrev z := "z"

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

abbrev State := String → Nat

def empty : State := fun _ => 0

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

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

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

 

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

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

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

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

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

def factorial_in_lean4 : Com :=
  <{ z := x;
     y := 1;
     while z != 0 do
       y := y * z;
       z := (z - 1)
     end }>

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

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

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

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

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

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

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

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

def hello := "world"

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

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

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

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

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

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

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

abbrev n := "n"

def prog (n : Nat) : Decorated := decorated
  (fun st => st x = n) $
    dc_pre (fun _ => 0 + n * (n + 1) / 2 = n * (n + 1) / 2) $
    dc_seq (dc_asgn z <{0}>
      (fun st => st z + n * (n + 1) / 2 = n * (n + 1) / 2)) $
    dc_seq (dc_asgn x <{n}>
      (fun st => st z + st x * (st x + 1) / 2 = n * (n + 1) / 2)) $

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

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

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

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

def subtract_slowly_dec (m n : Nat) : Decorated := decorated
  (fun st => st x = m ∧ st y = n) $
    dc_pre (fun st => st y - st x = n - m) $
    dc_while <{x != 0}>
        (fun st => st y - st x = n - m ∧ st x ≠ 0)
        (dc_pre (fun st => (st y - 1) - (st x - 1) = n - m) $
      dc_seq
      (dc_asgn y <{y - 1}>
        (fun st => st y - (st x - 1) = n - m))
      (dc_asgn x <{x - 1}>
        (fun st => st y - st x = n - m))
    )
  (fun st => st y = n - m)

def slow_assignment_dec (m : Nat) : Decorated := decorated
  (fun st => st x = m) $
    dc_pre (fun st => 0 + st x = m) $
    dc_seq
    (dc_asgn y <{0}>
        (fun st => st x = m ∧ st y = 0)) $
    dc_post (dc_while <{x != 0}>
        (fun st => st y + st x = m ∧ (st x ≠ 0))
        (dc_pre (fun st => (st y + 1) + (st x - 1) = m) $
        dc_seq
        (dc_asgn x <{x - 1}>
          (fun st => (st y + 1) + st x = m))
        (dc_asgn y <{y + 1}>
          (fun st => st y + st x = m))
    )
  (fun st => st y + st x = m ∧ ¬(st x ≠ 0)))
  (fun st => st y = m)

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

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

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

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

    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 is_wp P c Q := ({* P *} c {* Q *}) ∧ ∀P', ({* P' *} c {* Q *}) → (P' ->> P)

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 wp (c : Com) (Q : Assertion) : Assertion :=
  fun s => ∀ s', (s =[<[c]>]=> s') → Q s'

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

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

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

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

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

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

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

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

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

abbrev Value := Nat

abbrev Multiset := Value → Nat

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

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

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

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

 

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

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

@[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 selsort (l : List Nat) (n : Nat) : List Nat :=
  match l, n with
  | _, 0 => []  
  | [], _ => []
  | x :: tl, succ n' => let (y, tl') := select x tl; y :: selsort tl' n'

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

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

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

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

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

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

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

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

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

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

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

def deterministic {X : Type} (R : relation X) :=
  ∀ x y₁ y₂, R x y₁ → R x y₂ → y₁ = y₂

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

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

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

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

def step_normal_form := normal_form Step

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

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

inductive Tm : Type :=
  | c : Nat → Tm
  | p : Tm → Tm → Tm
  | tru : Tm
  | fls : Tm
  | test : Tm → Tm → Tm → Tm

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

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

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

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

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

@[simp] def first_le_second (al : List Nat) : Prop :=
  match al with
  | a :: b :: _ => a ≤ b
  | _ => True

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

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

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

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

def sorted'' (al : List Nat) := ∀ i j,
  i < j → j < length al → getD al i 0 ≤ getD al j 0

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

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

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

def ceval_fun_no_while (st : State) (c : Com) : State :=
  match c with
  | c_skip => st
  | c_asgn x a =>
      update st x (aeval st a)
  | c_seq c₁ c₂ =>
      let st' := ceval_fun_no_while st c₁
      ceval_fun_no_while st' c₂
  | c_if b c₁ c₂ =>
      if beval st b
      then ceval_fun_no_while st c₁
      else ceval_fun_no_while st c₂
  | c_while _ _ => st  

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

def cequiv (c₁ c₂ : Com) : Prop :=
  ∀ st st' : State, (st =[<[c₁]>]=> st') ↔ (st =[<[c₂]>]=> st')

def refines (c₁ c₂ : Com) : Prop :=
  ∀ st st' : State, (st =[<[c₁]>]=> st') → (st =[<[c₂]>]=> st')

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

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

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

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

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

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

inductive Color where
  | red
  | black

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

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

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

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

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

def ins {α : Type u} (x : Nat) (vx : α) (t : Tree α) : Tree α :=
  match t with
  | empty => tree red empty x vx empty
  | tree c l k vk r =>
      if x < k then balance c (ins x vx l) k vk r
      else if x > k then balance c l k vk (ins x vx r)
      else tree c l x vx r  

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

def insert {α : Type u} (x : Nat) (vx : α) (t : Tree α) : Tree α :=
  make_black (ins x vx t)

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)

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

 

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

abbrev step_normal_form := normal_form Step

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

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

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

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

abbrev multistep := Multi Step

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

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

instance (α : Type u) : Append (List α) where
  append := append

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

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

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

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

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

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

abbrev Assertion := State → Prop

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

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

macro s:term "[" name:term "↦" val:term "]" : term =>
  `(update $s $name $val)

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

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

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

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

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

And in Init.Prelude

Nat in Init.Prelude

Iff in Init.Core

String in Init.Prelude

Bool in Init.Prelude

List in Init.Prelude

Decidable in Init.Prelude

Decidable.or_not_self in Init.PropLemmas

Eq in Init.Prelude

List.getD in Init.Data.List.BasicAux

List.Sorted in Mathlib.Deprecated.Sort

Prod in Init.Prelude

Prod.fst in Init.Prelude

Prod.snd in Init.Prelude

List.all in Init.Data.List.Basic

Nat.div in Init.Prelude

Nat.mod in Init.Prelude

Nat.pred in Init.Prelude

Or in Init.Prelude

Add in Init.Prelude

Mul in Init.Prelude

Append in Init.Prelude

Tree in Mathlib.Data.Tree.Basic
</all_available_defs>

<all_available_lemmas>
theorem is_empty_empty : is_empty (@empty α)

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

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

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

theorem dequeue_empty : dequeue (@empty α) = empty

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

theorem identity (p : Prop) : p → p

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

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

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

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

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

theorem minimum_correct a b : outer_triple_valid (minimum_dec a b)

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

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

theorem value_is_nf t : value t → step_normal_form t

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem sort_sorted' l : Sorted (sort l)

theorem sort_perm' l : Permutation l (sort l)

theorem insertion_sort_correct' : is_a_sorting_algorithm sort

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

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

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

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

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

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

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

theorem mul_succ (m n : Nat) : m * succ n = add (m * n) m

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

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

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

theorem optimize_0plus_aexp_sound : atrans_sound optimize_0plus_aexp

theorem optimize_0plus_bexp_sound : btrans_sound optimize_0plus_bexp

theorem optimize_0plus_com_sound : ctrans_sound optimize_0plus_com

theorem optimizer_sound: ctrans_sound optimizer

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

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

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

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

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

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

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

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 empty_tree_BST (α : Type u) : BST (@empty_tree α)

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 bst_insert_of_bst {α : Type u} (k : Nat) (v : α) (t : Tree α)
    : BST t → BST (insert k v t)

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

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

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

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

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

theorem no_whiles_eqv c : no_whiles c = true ↔ No_whilesR c

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

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

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

theorem one_not_even : ¬ Even 1

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

theorem ev5_nonsense : Even 5 → 2 + 2 = 9

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

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

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

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

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

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

theorem LEq_reflexive : ∀n : Nat, LEq n n

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

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

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

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

theorem verification_conditions_correct dec
    : verification_conditions_from dec → outer_triple_valid dec

theorem dec_while_correct : outer_triple_valid dec_while

theorem dec_while_correct'
    : outer_triple_valid dec_while

theorem swap_correct m n : outer_triple_valid (swap_dec m n)

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

theorem 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 par_loop_any_x n
    : ∃ st', Multi CStep (par_loop, empty) (c_skip, st')
        ∧ st' x = n

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

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

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

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

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

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

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

theorem ex_falso_quodlibet (p : Prop) : False → p

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

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

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

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

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

theorem pos2nat2pos p : nat2pos (pos2nat p) = p

theorem nat2pos2nat i : pos2nat (nat2pos i) = i

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

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

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

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

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

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

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

theorem optimize_0plus_sound (a : AExp)
    : aeval (optimize_0plus a) = aeval a

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

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

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

theorem lookup_update_neq st (x x' : String) (v : Nat)
    : x' ≠ x
      → (update st x v) x' = st x'

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

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

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

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

theorem lookup_insert_eq {α : Type u} (d : α) t k vk
    : BST t → lookup d k (insert k vk t) = 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 optimize_plus_with_0_sound (a : AExp)
    : aeval (optimize_plus_with_0 a) = aeval a

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

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

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

theorem excluded_middle__dbl_neg_elim : excluded_middle → dbl_neg_elim

theorem dbl_neg_elim__implies_to_or : dbl_neg_elim → implies_to_or

theorem implies_to_or__excluded_middle : implies_to_or → excluded_middle

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

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

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

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

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

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 prog_correct' n : outer_triple_valid (prog n)

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

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

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

theorem subtract_slowly_outer_triple_valid m n
    : outer_triple_valid (subtract_slowly_dec 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 parity_lt_2 x : ¬(2 ≤ x) → parity x = x

theorem parity_outer_triple_valid m
    : outer_triple_valid (parity_dec m)

theorem squaring m
    : outer_triple_valid (squaring_dec m)

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

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

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

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

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 wp_is_weakest c Q P' : {* P' *} c {* Q *} → (P' ->> wp c Q)

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 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 hoare_complete P c Q : valid_hoare_triple P c Q → Derivable P c Q

theorem if_minus_plus :
    -- { True }
    {* fun _ => True *}
      <{if x <= y then z := y - x else y := x + z end}>
    -- { y = x + z }
    {* fun st => st y = st x + st z *}

theorem if_minus_plus_correct : outer_triple_valid if_minus_plus_dec

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 if_add_simple_correct : outer_triple_valid if_add_simple_dec

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

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

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

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

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

theorem insertion_sort_correct' : is_a_sorting_algorithm' sort

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

theorem contents_nil_inv l : (∀ x, 0 = contents l x) → l = []

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

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

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

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

theorem sort_specifications_equivalent sort
    : is_a_sorting_algorithm sort ↔ is_a_sorting_algorithm' sort

theorem select_perm x l y r
    : select x l = (y, r) → Permutation (x :: l) (y :: r)

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

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

theorem selection_sort_perm l : Permutation l (selection_sort l)

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

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

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

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

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 selsort_sorted n al : length al = n → Sorted (selsort al n)

theorem selection_sort_sorted al : Sorted (selection_sort al)

theorem selection_sort_is_correct : is_a_sorting_algorithm selection_sort

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

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

theorem selection_sort_correct' : is_a_sorting_algorithm' selection_sort

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

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

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

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

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

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

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

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

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

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

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

theorem step_deterministic : deterministic Step

theorem step_deterministic : deterministic Step

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

theorem value_is_nf v : Value v → normal_form Step v

theorem nf_is_value t : normal_form Step t → Value t

theorem nf_same_as_value t : normal_form Step t ↔ Value t

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

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

theorem normal_forms_unique : deterministic normal_form_of

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

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

theorem step_normalizing : normalizing Step

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

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

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

theorem combined_step_deterministic
    : deterministic Step ∨ ¬ deterministic Step

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

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

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

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

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

theorem permutation_app (l m l' m' : List α)
    : Permutation l l' → Permutation m m'
      → Permutation (l++m) (l'++m')

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

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

theorem existential_negation : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x)

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

theorem ceval_deterministic c st st₁ st₂ :
    (st =[ <[c]> ]=> st₁) → (st =[ <[c]> ]=> st₂) → st₁ = st₂

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

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

theorem if_true_simple c₁ c₂
    : cequiv <{if true then <[c₁]> else <[c₂]> end}> c₁

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

theorem swap_if_branches b c₁ c₂
    : cequiv
        <{if <[b]> then <[c₁]> else <[c₂]> end}>
        <{if !<[b]> then <[c₂]> else <[c₁]> end}>

theorem while_false b c : bequiv b <{false}> →
    cequiv <{while <[b]> do <[c]> end}> <{skip}>

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

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

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 forallTree_lt {α : Type u} (t : Tree α) k k'
    : ForallTree (fun x _ => x < k) t → k < k'
      → ForallTree (fun x _ => x < k') t

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

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

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

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

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

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

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_ins_eq {α : Type u} (d : α) t k vk
    : BST t → lookup d k (ins k vk t) = vk

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 loop_never_stops st st' : ¬(st =[ <[loop]> ]=> st')

theorem while_true_nonterm b c st st' :
    bequiv b <{true}> → ¬(st =[while <[b]> do <[c]> end]=> st')

theorem while_true b c :
    bequiv b <{true}> → cequiv <{while <[b]> do <[c]> end}> loop

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

theorem refl_aequiv a : aequiv a a

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

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

theorem refl_bequiv b : bequiv b b

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

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

theorem refl_cequiv c : cequiv c c

theorem sym_cequiv c₁ c₂ : cequiv c₁ c₂ → cequiv c₂ c₁

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

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

theorem c_while_congruence b b' c c'
    : bequiv b b' → cequiv c c'
      → cequiv <{while <[b]> do <[c]> end}> <{while <[b']> do <[c']> end}>

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

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 fold_constants_aexp_sound : atrans_sound fold_constants_aexp

theorem fold_constants_bexp_sound : btrans_sound fold_constants_bexp

theorem fold_constants_com_sound : ctrans_sound fold_constants_com

theorem value_is_nf t : value t → step_normal_form t

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem singleton_reverse (a : α) : reverse (cons a nil) = cons a nil

theorem reverse_append {α : Type u} (as bs : List α)
    : reverse (as ++ bs) = reverse bs ++ reverse as

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

theorem Palindrome_rev {α : Type} (l : List α)
    : Palindrome l → l = reverse l

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

theorem 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 look_leaf' α (d : α) j : look d j leaf = d

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

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

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

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 if_add_simple_correct : outer_triple_valid if_add_simple_dec

theorem inequiv_loop_skip : ¬ cequiv loop c_skip

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

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

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

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

theorem hoare_asgn Q x a :
    {* fun st => Q (st[x ↦ aeval st a]) *} c_asgn x a {* Q *}

theorem hoare_asgn_fwd m a (P : Assertion) :
    {* fun st => P st ∧ st x = m *}
      c_asgn x a
    {* fun st' => P (st'[x ↦ m]) ∧ st' x = aeval (st'[x ↦ m]) a *}

theorem hoare_asgn_fwd_exists a (P : Assertion) :
    {* P *}
      c_asgn x a
    {* fun st' => ∃ m, P (st'[x ↦ m]) ∧ st' x = aeval (st'[x ↦ m]) a *}

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

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

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

theorem hoare_if P Q b c₁ c₂ :
    {* fun st => P st ∧ beval st b *} c₁ {* Q *}
    → {* fun st => P st ∧ ¬(beval st b) *} c₂ {* Q *}
    → {* P *} c_if b c₁ c₂ {* Q *}

theorem hoare_while P b c :
    {* fun st => P st ∧ beval st b *} c {* P *}
    → {* P *} c_while b c {* fun st => P st ∧ ¬(beval st b) *}

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

theorem length_listOfVec {α : Type} (n : Nat) (v : Vec α n)
    : List.length (listOfVec v) = n

theorem listOfVec_reverse α l
    : @listOfVec α (List.length l) (vecOfList l) = l

theorem curry (p q r : Prop) : (p ∧ q → r) → (p → q → r)

theorem uncurry (p q r : Prop) : (p → q → r) → (p ∧ q → r)
</all_available_lemmas>

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

open Permutation
</local_ctx>

<target_theorem>
theorem permutation_app_comm (l l' : List α)
    : Permutation (l ++ l') (l' ++ l) :=
</target_theorem>

