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

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
abbrev t := "t"
end Imp.Hoare

namespace Imp.Hoare
def swap_program : Com := <{
  t := x;
  x := y;
  y := t
}>
end Imp.Hoare

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

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

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

namespace TM
abbrev value (t : Tm) := BValue t ∨ NValue t
end TM

namespace TM
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₁')
end TM

namespace TM
abbrev step_normal_form := normal_form Step
end TM

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

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

namespace TM
inductive Ty : Type :=
  | bool : Ty
  | nat : Ty
end TM

namespace TM
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
end TM

namespace TM
abbrev multistep := Multi Step
end TM

namespace Hidden
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat
end Hidden

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

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

namespace Hidden.Nat
instance : Add Nat where
  add := add
end Hidden.Nat

namespace Hidden.Nat
instance : Mul Nat where
  mul := mul
end Hidden.Nat

namespace Imp
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₂)
end Imp

namespace Imp
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₂)
end Imp

namespace Imp
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 -/
end Imp

namespace Imp
def optimizer (c : Com) := optimize_0plus_com (fold_constants_com c)
end Imp

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

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

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

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

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

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

namespace Tree
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
end Tree

namespace Tree
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
end Tree

namespace Tree
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  
end Tree

namespace Tree
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)
end Tree

namespace Tree
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 -/
end Tree

namespace Imp
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
end Imp

namespace Imp
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)
end Imp

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

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

namespace Hidden
inductive And : Prop → Prop → Prop where
  | intro : a → b → And a b
end Hidden

namespace Hidden
inductive Or : Prop → Prop → Prop where
  | inl : a → Or a b
  | inr : b → Or a b
end Hidden

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

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

namespace Hidden
inductive True : Prop where
  | intro : True
end Hidden

namespace Hidden
inductive False : Prop where
end Hidden

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

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

namespace Imp.Hoare
def reduce_to_zero : Com :=
  <{
    while x != 0 do
      x := x - 1
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
inductive Decorated :=
  | decorated : Assertion → DCom → Decorated
end Imp.Hoare

namespace Imp.Hoare
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)
)
end Imp.Hoare

namespace Imp.Hoare
@[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
end Imp.Hoare

namespace Imp.Hoare
def erase_d (dec : Decorated) : Com :=
  match dec with
  | decorated _ d => erase d
end Imp.Hoare

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

namespace Imp.Hoare
@[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
end Imp.Hoare

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

namespace Imp.Hoare
def outer_triple_valid (dec : Decorated) :=
  {* precondition_from dec *}
    erase_d dec
  {* postcondition_from dec *}
end Imp.Hoare

namespace Imp.Hoare
@[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)
end Imp.Hoare

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

namespace Imp.Hoare
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)
end Imp.Hoare

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)

namespace CImp
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   
end CImp

namespace CImp
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)
end CImp

namespace CImp
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 :=
end CImp

abbrev total_map α := Nat → α

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

namespace VerySlow
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)
end VerySlow

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

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

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

namespace FastEnough
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)
end FastEnough

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

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

namespace Hidden.AExp
inductive AExp where
  | a_num : Nat → AExp
  | a_plus : AExp → AExp → AExp
  | a_minus : AExp → AExp → AExp
  | a_mult : AExp → AExp → AExp
end Hidden.AExp

namespace Hidden.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
end Hidden.AExp

namespace Hidden.AExp
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₂)
end Hidden.AExp

namespace Hidden.AExp
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₂)
end Hidden.AExp

namespace Hidden.AExp
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 -/
end Hidden.AExp

namespace Hidden.AExp
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) :=
end Hidden.AExp

namespace Hidden.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₂)

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

 

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

namespace AEvalR_division
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  
end AEvalR_division

namespace AEvalR_division
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₃
end AEvalR_division

namespace AEvalR_extended
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
end AEvalR_extended

namespace AEvalR_extended
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₂)
end AEvalR_extended

namespace Imp
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
end Imp

namespace Imp
abbrev w := "w"
end Imp

namespace Imp
abbrev x := "x"
end Imp

namespace Imp
abbrev y := "y"
end Imp

namespace Imp
abbrev z := "z"
end Imp

namespace Imp
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
end Imp

namespace Imp
abbrev State := String → Nat
end Imp

namespace Imp
def empty : State := fun _ => 0
end Imp

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

namespace Imp
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₂)
end Imp

namespace Imp
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 -/
end Imp

namespace Imp
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₂)
end Imp

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

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

namespace Imp
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
end Imp

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

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

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

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

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

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

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

namespace Hidden.AExp
def optimize_plus_with_0 (a : AExp) : AExp :=
  optimize_plus0 (optimize_0plus a)
end Hidden.AExp

namespace Hidden.AExp
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₂)
end Hidden.AExp

namespace Hidden.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₂)
end Hidden.AExp

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)

namespace LocalNat
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat
end LocalNat

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

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

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

namespace Imp.Hoare
abbrev n := "n"
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
def parity x :=
  match x with
  | 0 => 0
  | 1 => 1
  | succ (succ x') => parity x'
end Imp.Hoare

namespace Imp.Hoare
def parity_dec (m : Nat) : Decorated := decorated
  (fun st => st x = m) $
  sorry
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
def is_wp P c Q := ({* P *} c {* Q *}) ∧ ∀P', ({* P' *} c {* Q *}) → (P' ->> P)
end Imp.Hoare

namespace Imp.Hoare
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
end Imp.Hoare

namespace Imp.Hoare
def wp (c : Com) (Q : Assertion) : Assertion :=
  fun s => ∀ s', (s =[<[c]>]=> s') → Q s'
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

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

namespace SimpleArith1
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₂')
end SimpleArith1

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'

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

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

namespace Combined
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₂)
end Combined

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

namespace Imp.Hidden
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
end Imp.Hidden

namespace Imp
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  
end Imp

namespace Imp
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''
end Imp

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

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

namespace Toy.Temp1
inductive Value : Tm → Prop :=
  | v_const n : Value (c n)
  | v_funny t₁ n : Value (p t₁ (c n))   
end Toy.Temp1

namespace Toy.Temp1
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₂')
end Toy.Temp1

namespace Toy.Temp2
inductive Value : Tm → Prop :=
  | v_const n : Value (c n)
end Toy.Temp2

namespace Toy.Temp2
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₂')
end Toy.Temp2

namespace Toy.Temp3
inductive Value : Tm → Prop :=
  | v_const n : Value (c n)
end Toy.Temp3

namespace Toy.Temp3
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₂)
end Toy.Temp3

inductive Color where
  | red
  | black

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

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

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

namespace Tree
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
end Tree

namespace Tree
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
end Tree

namespace Tree
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
end Tree

namespace Tree
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  
end Tree

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

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

namespace Tree
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)
end Tree

namespace Tree
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 -/
end Tree

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

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

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

namespace Imp
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 -/
end Imp

namespace Imp
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 -/
end Imp

namespace Imp
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 -/
end Imp

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

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

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

namespace TM
abbrev value (t : Tm) := BValue t ∨ NValue t
end TM

namespace TM
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₁')
end TM

namespace TM
abbrev step_normal_form := normal_form Step
end TM

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

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

namespace TM
inductive Ty : Type :=
  | bool : Ty
  | nat : Ty
end TM

namespace TM
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
end TM

namespace TM
abbrev multistep := Multi Step
end TM

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

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

namespace Hidden.List
instance (α : Type u) : Append (List α) where
  append := append
end Hidden.List

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

namespace Hidden.List
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)
end Hidden.List

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
abbrev Assertion := State → Prop
end Imp.Hoare

namespace Imp.Hoare
def assert_implies (P Q : Assertion) : Prop :=
  ∀ st, P st → Q st
end Imp.Hoare

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

namespace Imp.Hoare
macro s:term "[" name:term "↦" val:term "]" : term =>
  `(update $s $name $val)
end Imp.Hoare

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

namespace Imp.Hoare
theorem minimum_correct a b : outer_triple_valid (minimum_dec a b)
end Imp.Hoare

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

namespace Imp.Hoare
theorem swap_correct a₀ b₀ :
    {* fun st => st x = a₀ ∧ st y = b₀ *}
      swap_program
    {* fun st => st x = b₀ ∧ st y = a₀ *}
end Imp.Hoare

namespace TM
theorem value_is_nf t : value t → step_normal_form t
end TM

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

namespace Hidden.Nat
theorem add_zero (m : Nat) : m + zero = m
end Hidden.Nat

namespace Hidden.Nat
theorem add_succ (m n : Nat) : m + succ n = succ (m + n)
end Hidden.Nat

namespace Hidden.Nat
theorem zero_add (n : Nat) : zero + n = n
end Hidden.Nat

namespace Hidden.Nat
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k)
end Hidden.Nat

namespace Hidden.Nat
theorem succ_add (m n : Nat) : succ (m + n) = succ m + n
end Hidden.Nat

namespace Hidden.Nat
theorem add_comm (m n : Nat) : m + n = n + m
end Hidden.Nat

namespace Hidden.Nat
theorem mul_zero (m : Nat) : m * zero = zero
end Hidden.Nat

namespace Hidden.Nat
theorem mul_succ (m n : Nat) : m * succ n = add (m * n) m
end Hidden.Nat

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

namespace Hidden.Nat
theorem mul_assoc (m n k : Nat) : m * n * k = m * (n * k)
end Hidden.Nat

namespace Hidden.Nat
theorem mul_comm (m n : Nat) : m * n = n * m
end Hidden.Nat

namespace Imp
theorem optimize_0plus_aexp_sound : atrans_sound optimize_0plus_aexp
end Imp

namespace Imp
theorem optimize_0plus_bexp_sound : btrans_sound optimize_0plus_bexp
end Imp

namespace Imp
theorem optimize_0plus_com_sound : ctrans_sound optimize_0plus_com
end Imp

namespace Imp
theorem optimizer_sound: ctrans_sound optimizer
end Imp

namespace Hidden.List
theorem nil_append (as : List α) : append nil as = as
end Hidden.List

namespace Hidden.List
theorem cons_append (a : α) (as bs : List α)
        : append (cons a as) bs = cons a (append as bs)
end Hidden.List

namespace Hidden.List
theorem append_nil (as : List α) : append as nil = as
end Hidden.List

namespace Hidden.List
theorem append_assoc (as bs cs : List α)
        : append (append as bs) cs = append as (append bs cs)
end Hidden.List

namespace Hidden.List
theorem length_append (as bs : List α)
        : length (append as bs) = length as + length bs
end Hidden.List

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

namespace TM
theorem preservation'' t t' T
    : HasType t T → Step t t' → HasType t' T
end TM

namespace TM
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)
end TM

namespace Tree
theorem empty_tree_BST (α : Type u) : BST (@empty_tree α)
end Tree

namespace 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)
end Tree

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

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

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

namespace Tree
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
end Tree

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

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

namespace Imp
theorem no_whiles_eqv c : no_whiles c = true ↔ No_whilesR c
end Imp

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

namespace Imp.Hoare
theorem reduce_to_zero_correct' :
    {* fun _ => True *}
      reduce_to_zero
    {* fun st => st x = 0 *}
end Imp.Hoare

namespace Imp.Hoare
theorem reduce_to_zero_correct''' :
    {* fun _ => True *}
      reduce_to_zero
    {* fun st => st x = 0 *}
end Imp.Hoare

namespace Imp.Hoare
theorem verification_correct d P
    : verification_conditions P d → {* P *} erase d {* post d *}
end Imp.Hoare

namespace Imp.Hoare
theorem verification_conditions_correct dec
    : verification_conditions_from dec → outer_triple_valid dec
end Imp.Hoare

namespace Imp.Hoare
theorem dec_while_correct : outer_triple_valid dec_while
end Imp.Hoare

namespace Imp.Hoare
theorem dec_while_correct'
    : outer_triple_valid dec_while
end Imp.Hoare

namespace Imp.Hoare
theorem swap_correct m n : outer_triple_valid (swap_dec m n)
end Imp.Hoare

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

namespace CImp
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
end CImp

namespace CImp
theorem par_loop_any_x n
    : ∃ st', Multi CStep (par_loop, empty) (c_skip, st')
        ∧ st' x = n
end CImp

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)

namespace Hidden.AExp
theorem optimize_0plus_sound (a : AExp)
    : aeval (optimize_0plus a) = aeval a
end Hidden.AExp

namespace Hidden.AExp
theorem optimize_plus0_sound (a : AExp)
    : aeval (optimize_plus0 a) = aeval a
end Hidden.AExp

namespace Hidden.AExp
theorem aeval_iff_AEvalR (a : AExp) (n : Nat)
    : a ==> n ↔ aeval a = n
end Hidden.AExp

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

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

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

namespace Imp
theorem aequiv_example
    : aequiv <{x - x}> <{0}>
end Imp

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

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

namespace Tree
theorem lookup_insert_eq {α : Type u} (d : α) t k vk
    : BST t → lookup d k (insert k vk t) = vk
end Tree

namespace Tree
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
end Tree

namespace Hidden.AExp
theorem optimize_plus_with_0_sound (a : AExp)
    : aeval (optimize_plus_with_0 a) = aeval a
end Hidden.AExp

namespace Hidden.AExp
theorem optimize_0plus_b_sound (b : BExp)
    : beval (optimize_0plus_b b) = beval b
end Hidden.AExp

namespace Hidden.AExp
theorem beval_iff_BEvalR b v
    : b ==>b v ↔ beval b = v
end Hidden.AExp

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

namespace LocalNat
theorem zero_mul (n : Nat) : mul zero n = zero
end LocalNat

namespace LocalNat
theorem one_mul (n : Nat) : mul (succ zero) n = n
end LocalNat

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

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

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

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

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

namespace Imp.Hoare
theorem prog_correct' n : outer_triple_valid (prog n)
end Imp.Hoare

namespace Imp.Hoare
theorem add_cumul' n : n ≠ 0 → n * (n + 1) / 2 = n * (n - 1) / 2 + n
end Imp.Hoare

namespace Imp.Hoare
theorem neg_dist' e n : n ≠ 0 -> e - n + 1 = e - (n - 1)
end Imp.Hoare

namespace Imp.Hoare
theorem dec_inc' n : n ≠ 0 → n - 1 + 1 = n
end Imp.Hoare

namespace Imp.Hoare
theorem subtract_slowly_outer_triple_valid m n
    : outer_triple_valid (subtract_slowly_dec m n)
end Imp.Hoare

namespace Imp.Hoare
theorem slow_assignment m
    : outer_triple_valid (slow_assignment_dec m)
end Imp.Hoare

namespace Imp.Hoare
theorem parity_ge_2 x : 2 ≤ x → parity (x - 2) = parity x
end Imp.Hoare

namespace Imp.Hoare
theorem parity_lt_2 x : ¬(2 ≤ x) → parity x = x
end Imp.Hoare

namespace Imp.Hoare
theorem parity_outer_triple_valid m
    : outer_triple_valid (parity_dec m)
end Imp.Hoare

namespace Imp.Hoare
theorem squaring m
    : outer_triple_valid (squaring_dec m)
end Imp.Hoare

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

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

namespace Imp.Hoare
theorem h_consequence_pre P Q P' c
    : (Derivable P' c Q) → (P ->> P') → (Derivable P c Q)
end Imp.Hoare

namespace Imp.Hoare
theorem h_consequence_post P Q Q' c
    : Derivable P c Q' → (Q' ->> Q) → Derivable P c Q
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_sound P c Q : Derivable P c Q → valid_hoare_triple P c Q
end Imp.Hoare

namespace Imp.Hoare
theorem wp_is_precondition c Q : {* wp c Q *} c {* Q *}
end Imp.Hoare

namespace Imp.Hoare
theorem wp_is_weakest c Q P' : {* P' *} c {* Q *} → (P' ->> wp c Q)
end Imp.Hoare

namespace Imp.Hoare
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
end Imp.Hoare

namespace Imp.Hoare
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)
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_complete P c Q : valid_hoare_triple P c Q → Derivable P c Q
end Imp.Hoare

namespace Imp.Hoare
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 *}
end Imp.Hoare

namespace Imp.Hoare
theorem if_minus_plus_correct : outer_triple_valid if_minus_plus_dec
end Imp.Hoare

namespace Imp.Hoare
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 *}
end Imp.Hoare

namespace Imp.Hoare
theorem if_add_simple_correct : outer_triple_valid if_add_simple_dec
end Imp.Hoare

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

namespace SimpleArith2
theorem step_deterministic : deterministic Step
end SimpleArith2

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

namespace Combined
theorem combined_step_deterministic
    : deterministic Step ∨ ¬ deterministic Step
end Combined

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

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_refl (l : List α) : Permutation l l

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

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

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

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

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 permutation_cons_append (l : List α) x
    : Permutation (x :: l) (l ++ [x])

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

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

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

theorem permutation_app_middle (l l₁ l₂ l₃ l₄ : List α)
    : Permutation (l₁ ++ l₂) (l₃ ++ l₄)
      → Permutation (l₁ ++ l ++ l₂) (l₃ ++ l ++ l₄)

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

theorem permutation_middle (l₁ l₂ : List α) a
    : Permutation (a :: l₁ ++ l₂) (l₁ ++ a :: l₂)

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

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

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

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

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

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

theorem maybe_swap_perm al : Permutation al (maybe_swap al)

theorem maybe_swap_correct al
    : Permutation al (maybe_swap al)
      ∧ first_le_second (maybe_swap al)

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

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

theorem sort_sorted l : Sorted (sort l)

theorem insert_perm x l : Permutation (x :: l) (insert x l)

theorem sort_perm l : Permutation l (sort l)

theorem insertion_sort_correct : is_a_sorting_algorithm sort

theorem sorted_sorted' al : Sorted al → sorted' al

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

namespace Tree
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)
end Tree

namespace Tree
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)
end Tree

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

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

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

namespace Tree
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
end Tree

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

namespace Tree
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
end Tree

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

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

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

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

namespace Imp
theorem refl_aequiv a : aequiv a a
end Imp

namespace Imp
theorem sym_aequiv a₁ a₂ : aequiv a₁ a₂ → aequiv a₂ a₁
end Imp

namespace Imp
theorem trans_aequiv a₁ a₂ a₃ : aequiv a₁ a₂ → aequiv a₂ a₃ → aequiv a₁ a₃
end Imp

namespace Imp
theorem refl_bequiv b : bequiv b b
end Imp

namespace Imp
theorem sym_bequiv b₁ b₂ : bequiv b₁ b₂ → bequiv b₂ b₁
end Imp

namespace Imp
theorem trans_bequiv b₁ b₂ b₃ : bequiv b₁ b₂ → bequiv b₂ b₃ → bequiv b₁ b₃
end Imp

namespace Imp
theorem refl_cequiv c : cequiv c c
end Imp

namespace Imp
theorem sym_cequiv c₁ c₂ : cequiv c₁ c₂ → cequiv c₂ c₁
end Imp

namespace Imp
theorem trans_cequiv c₁ c₂ c₃ : cequiv c₁ c₂ → cequiv c₂ c₃ → cequiv c₁ c₃
end Imp

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

namespace Imp
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}>
end Imp

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

namespace Imp
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₂')
end Imp

namespace Imp
theorem fold_constants_aexp_sound : atrans_sound fold_constants_aexp
end Imp

namespace Imp
theorem fold_constants_bexp_sound : btrans_sound fold_constants_bexp
end Imp

namespace Imp
theorem fold_constants_com_sound : ctrans_sound fold_constants_com
end Imp

namespace TM
theorem value_is_nf t : value t → step_normal_form t
end TM

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)

namespace Hidden.List
theorem nil_append (as : List α) : nil ++ as = as
end Hidden.List

namespace Hidden.List
theorem cons_append (a : α) (as bs : List α)
        : (cons a as) ++ bs = cons a (as ++ bs)
end Hidden.List

namespace Hidden.List
theorem append_nil (as : List α) : as ++ nil = as
end Hidden.List

namespace Hidden.List
theorem append_assoc (as bs cs : List α)
        : (as ++ bs) ++ cs = as ++ (bs ++ cs)
end Hidden.List

namespace Hidden.List
theorem singleton_reverse (a : α) : reverse (cons a nil) = cons a nil
end Hidden.List

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

namespace Hidden.List.Palindrome
theorem Palindrome_app_rev {α : Type} (l : List α) : Palindrome (l ++ reverse l)
end Hidden.List.Palindrome

namespace Hidden.List.Palindrome
theorem Palindrome_rev {α : Type} (l : List α)
    : Palindrome l → l = reverse l
end Hidden.List.Palindrome

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

namespace CImp
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
end CImp

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

namespace Imp.Hoare
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 *}
end Imp.Hoare

namespace Imp.Hoare
theorem if_add_simple_correct : outer_triple_valid if_add_simple_dec
end Imp.Hoare

namespace Imp
theorem inequiv_loop_skip : ¬ cequiv loop c_skip
end Imp

namespace Imp.Hoare
theorem hoare_post_true P Q c : (∀ st, Q st) → {* P *} c {* Q *}
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_pre_false P Q c : (∀ st, ¬ P st) → {* P *} c {* Q *}
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_skip P : {* P *} <{skip}> {* P *}
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_seq P Q R c₁ c₂ :
    {* Q *} c₂ {* R *} → {* P *} c₁ {* Q *} → {* P *} c_seq c₁ c₂ {* R *}
end Imp.Hoare

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

namespace Imp.Hoare
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 *}
end Imp.Hoare

namespace Imp.Hoare
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 *}
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_consequence_pre P P' Q c :
    {* P' *} c {* Q *}
    → P ->> P'
    → {* P *} c {* Q *}
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_consequence_post P Q Q' c :
    {* P *} c {* Q' *}
    → Q' ->> Q
    → {* P *} c {* Q *}
end Imp.Hoare

namespace Imp.Hoare
theorem hoare_consequence P P' Q Q' c :
    {* P' *} c {* Q' *}
    → P ->> P'
    → Q' ->> Q
    → {* P *} c {* Q *}
end Imp.Hoare

namespace Imp.Hoare
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 *}
end Imp.Hoare

namespace Imp.Hoare
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) *}
end Imp.Hoare

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

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>
import Frap.SmallStep

namespace TM

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

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

open BValue

open NValue

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

open Step

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

theorem value_is_nf t : value t → step_normal_form t

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

open 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

open HasType

example  -- `⊢ if false then 0 else (succ 0) ∈ nat`
    : HasType (ite fls zro (scc zro)) nat := by
  apply t_if
  . apply t_false
  . apply t_0
  . apply t_succ
    apply t_0

/-
It's important to realize that the typing relation is a _conservative_ (or _static_) approximation: it does not consider what happens when the term is reduced.
In particular, it does not calculate the type of its normal form.
-/

example  -- `⊢ if false then zero else true ∉ bool`
    : ¬ HasType (ite fls zro tru) bool := by
  intro contra
  cases contra
  rename_i contra _
  cases contra

/-
exercise (1-star)
-/
example t : HasType (scc t) nat → HasType t nat := by
  intro ht
  cases ht
  assumption

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

theorem nat_canonical t : HasType t nat → value t → NValue t
</local_ctx>

<target_theorem>
theorem progress t T
    : HasType t T → value t ∨ ∃ t', Step t t' :=
</target_theorem>

