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 equiv (P Q : Expr) : Prop := ∀ (Γ : Context),
  P.val? Γ = Q.val? Γ

instance : Equivalence equiv where
  refl := equiv_refl
  symm := equiv_symm
  trans := equiv_trans

def equiv' (S T : Statement) : Prop := ∀ (Γ : Context), S.eval Γ ↔ T.eval Γ

instance : Equivalence equiv' where
  refl := equiv_refl
  symm := equiv_symm
  trans := equiv_trans

inductive Expr
| num : Nat → Expr
| bool : Bool → Expr
| var : String → Expr
| add : Expr → Expr → Expr
| sub : Expr → Expr → Expr
| mul : Expr → Expr → Expr
| eq : Expr → Expr → Expr
| lt : Expr → Expr → Expr
| gt : Expr → Expr → Expr
| le : Expr → Expr → Expr
| ge : Expr → Expr → Expr
| and : Expr → Expr → Expr
| or : Expr → Expr → Expr
deriving Repr, DecidableEq

inductive Com
| assign : String → Expr → Com
| seq : Com → Com → Com
| cond : Expr → Com → Com → Com
| while : Expr → Com → Com
| skip : Com

instance : Coe Nat Expr := ⟨Expr.num⟩

instance : Coe Bool Expr := ⟨Expr.bool⟩

instance : Coe Lean.NumLit (Lean.TSyntax `expr) where
  coe s := ⟨s.raw⟩

instance : Coe Lean.Ident (Lean.TSyntax `expr) where
  coe s := ⟨s.raw⟩

@[app_unexpander While.Expr.num]
def unexpandNum : Lean.PrettyPrinter.Unexpander
  | `($_ $x:num) => `([nexpr| $x:num])
  | `($_ $x:ident) => `([nexpr| $($x)])
  | _ => throw ()

@[app_unexpander While.Expr.bool]
def unexpandBool : Lean.PrettyPrinter.Unexpander
  | `($_ Bool.true) => `([bexpr| true])
  | `($_ Bool.false) => `([bexpr| false])
  | `($_ «true») => `([bexpr| true])
  | `($_ «false») => `([bexpr| false])
  | _ => throw ()

@[app_unexpander While.Expr.var]
def unexpandIdent : Lean.PrettyPrinter.Unexpander
  | `($_ $x:str) =>
    let identLit := Lean.mkIdent $ Lean.Name.mkSimple x.getString
    `([nexpr| $identLit:ident])
  | `($_ $x:ident) => `([nexpr| $($x)])
  | _ => throw ()

@[app_unexpander While.Expr.add]
def unexpandAdd : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([nexpr| $x + $y])
  | _ => throw ()

@[app_unexpander While.Expr.sub]
def unexpandSub : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([nexpr| $x - $y])
  | _ => throw ()

@[app_unexpander While.Expr.mul]
def unexpandMul : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([nexpr| $x * $y])
  | _ => throw ()

@[app_unexpander While.Expr.eq]
def unexpandEq : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([bexpr| $x:nexpr == $y:nexpr])
  | _ => throw ()

@[app_unexpander While.Expr.lt]
def unexpandLt : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([bexpr| $x:nexpr < $y])
  | _ => throw ()

@[app_unexpander While.Expr.gt]
def unexpandGt : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([bexpr| $x:nexpr > $y])
  | _ => throw ()

@[app_unexpander While.Expr.le]
def unexpandLe : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([bexpr| $x:nexpr <= $y])
  | _ => throw ()

@[app_unexpander While.Expr.ge]
def unexpandGe : Lean.PrettyPrinter.Unexpander
  | `($_ [nexpr| $x] [nexpr| $y]) => `([bexpr| $x:nexpr >= $y])
  | _ => throw ()

@[app_unexpander While.Expr.and]
def unexpandAnd : Lean.PrettyPrinter.Unexpander
  | `($_ [bexpr| $x] [bexpr| $y]) => `([bexpr| $x && $y])
  | _ => throw ()

@[app_unexpander While.Expr.or]
def unexpandOr : Lean.PrettyPrinter.Unexpander
  | `($_ [bexpr| $x] [bexpr| $y]) => `([bexpr| $x || $y])
  | _ => throw ()

@[app_unexpander While.Com.skip]
def unexpandSkip : Lean.PrettyPrinter.Unexpander
  | `($_) => `([com| skip])

@[app_unexpander While.Com.seq]
def unexpandSeq : Lean.PrettyPrinter.Unexpander
  | `($_ [com| $c1] [com| $c2]) => `([com| $c1; $c2])
  | _ => throw ()

@[app_unexpander While.Com.cond]
def unexpandCond : Lean.PrettyPrinter.Unexpander
  | `($_ [bexpr| $e] [com| $c1] [com| $c2]) => `([com| if $e then $c1 else $c2 fi])
  | _ => throw ()

@[app_unexpander While.Com.while]
def unexpandWhile : Lean.PrettyPrinter.Unexpander
  | `($_ [bexpr| $e] [com| $c]) => `([com| while $e do $c od])
  | _ => throw ()

@[app_unexpander While.Com.assign]
def unexpandAssign : Lean.PrettyPrinter.Unexpander
  | `($_ $x:str  [nexpr| $e:nexpr]) =>
    let xl := Lean.mkIdent $ Lean.Name.mkSimple x.getString
    `([com| let $xl := $e])
  | _ => throw ()

def addBinOp (opString : String) (e₁ e₂ : Std.Format) : Std.Format :=
 e₁ ++ opString ++ e₂

def Expr.reprPrec (e : Expr) (prec : Nat) : Format := match e with
    | .num n => Repr.reprPrec n prec
    | .bool b => Repr.reprPrec b prec
    | .var v => v
    | .add e₁ e₂ => addBinOp " + " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .sub e₁ e₂ => addBinOp " - " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .mul e₁ e₂ => addBinOp " * " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .or e₁ e₂ => addBinOp " || " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .and e₁ e₂ => addBinOp " && " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .ge e₁ e₂ => addBinOp " >= " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .le e₁ e₂ => addBinOp " <= " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .lt e₁ e₂ => addBinOp " < " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .gt e₁ e₂ => addBinOp " > " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)
    | .eq e₁ e₂ => addBinOp " == " (Expr.reprPrec e₁ prec) (Expr.reprPrec e₂ prec)

instance : Repr Expr := ⟨Expr.reprPrec⟩

  def Com.reprPrec (c : Com) (prec : Nat) : Format := match c with
    | .skip => "skip"
    | .assign v e => v ++ " := " ++ Repr.reprPrec e prec
    | .seq c₁ c₂ => reprPrec c₁ prec ++ ";" ++ Format.line ++ reprPrec c₂ prec
    | .cond b c₁ c₂ => "if" ++ Format.line ++ (Repr.reprPrec b prec) ++ reprPrec c₁ prec ++ ";" ++ Format.line ++ reprPrec c₂ prec ++ Format.line ++ "fi"
    | .while b c => "while" ++ Format.line ++ (Repr.reprPrec b prec) ++ " do " ++ Format.line ++ reprPrec c prec ++ Format.line ++ "od"

instance : Repr Com := ⟨Com.reprPrec⟩

def main : IO Unit :=
  IO.println s!"Hello, hello!"

def sqrt : Com := [com|
  S := 0;
  while ((S + 1) * (S + 1)) <= X do
    S := S + 1
  od
  ]

def sqrt_spec (x : Nat) : Triple :=
  {X == $(x) ∧ X >= 0}
  S := 0;
  while ((S + 1) * (S + 1)) <= X do
    S := S + 1
  od
  {X == $(x) ∧ S * S == X }

def simplifyConstants : Expr → Expr
| Expr.add e1 e2 =>
    let s1 := simplifyConstants e1
    let s2 := simplifyConstants e2
    match s1, s2 with
    | Expr.num n1, Expr.num n2 => Expr.num (n1 + n2)
    | _, _ => Expr.add s1 s2
| Expr.sub e1 e2 =>
    let s1 := simplifyConstants e1
    let s2 := simplifyConstants e2
    match s1, s2 with
    | Expr.num n1, Expr.num n2 => Expr.num (n1 - n2)
    | _, _ => Expr.sub s1 s2
| Expr.mul e1 e2 =>
    let s1 := simplifyConstants e1
    let s2 := simplifyConstants e2
    match s1, s2 with
    | Expr.num n1, Expr.num n2 => Expr.num (n1 * n2)
    | _, _ => Expr.mul s1 s2
| Expr.var x => Expr.var x
| e => e

def normalizeEq (e1 e2 : Expr) : Expr :=
match e1, e2 with
| Expr.var x, e2 => Expr.eq (Expr.var x) (simplifyConstants e2)
| e2, Expr.var x => Expr.eq (Expr.var x) (simplifyConstants e2)
| Expr.add (Expr.var x) e, e2 => Expr.eq (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.add e (Expr.var x), e2 => Expr.eq (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.sub (Expr.var x) e, e2 => Expr.eq (Expr.var x) (simplifyConstants (Expr.add e2 e))
| Expr.sub e (Expr.var x), e2 => Expr.eq (Expr.var x) (simplifyConstants (Expr.sub e e2))
| _, _ => Expr.eq e1 e2

def normalizeGe (e1 e2 : Expr) : Expr :=
match e1, e2 with
| Expr.var x, e2 => Expr.ge (Expr.var x) (simplifyConstants e2)
| e2, Expr.var x => Expr.le (Expr.var x) (simplifyConstants e2)
| Expr.add (Expr.var x) e, e2 => Expr.ge (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.add e (Expr.var x), e2 => Expr.ge (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.sub (Expr.var x) e, e2 => Expr.ge (Expr.var x) (simplifyConstants (Expr.add e2 e))
| Expr.sub e (Expr.var x), e2 => Expr.ge (Expr.var x) (simplifyConstants (Expr.sub e e2))
| _, _ => Expr.ge e1 e2

def normalizeLe (e1 e2 : Expr) : Expr :=
match e1, e2 with
| Expr.var x, e2 => Expr.le (Expr.var x) (simplifyConstants e2)
| e2, Expr.var x => Expr.ge (Expr.var x) (simplifyConstants e2)
| Expr.add (Expr.var x) e, e2 => Expr.le (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.add e (Expr.var x), e2 => Expr.le (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.sub (Expr.var x) e, e2 => Expr.le (Expr.var x) (simplifyConstants (Expr.add e2 e))
| Expr.sub e (Expr.var x), e2 => Expr.le (Expr.var x) (simplifyConstants (Expr.sub e e2))
| _, _ => Expr.le e1 e2

def normalizeGt (e1 e2 : Expr) : Expr :=
match e1, e2 with
| Expr.var x, e2 => Expr.gt (Expr.var x) (simplifyConstants e2)
| e2, Expr.var x => Expr.lt (Expr.var x) (simplifyConstants e2)
| Expr.add (Expr.var x) e, e2 => Expr.gt (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.add e (Expr.var x), e2 => Expr.gt (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.sub (Expr.var x) e, e2 => Expr.gt (Expr.var x) (simplifyConstants (Expr.add e2 e))
| Expr.sub e (Expr.var x), e2 => Expr.gt (Expr.var x) (simplifyConstants (Expr.sub e e2))
| _, _ => Expr.gt e1 e2

def normalizeLt (e1 e2 : Expr) : Expr :=
match e1, e2 with
| Expr.var x, e2 => Expr.lt (Expr.var x) (simplifyConstants e2)
| e2, Expr.var x => Expr.gt (Expr.var x) (simplifyConstants e2)
| Expr.add (Expr.var x) e, e2 => Expr.lt (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.add e (Expr.var x), e2 => Expr.lt (Expr.var x) (simplifyConstants (Expr.sub e2 e))
| Expr.sub (Expr.var x) e, e2 => Expr.lt (Expr.var x) (simplifyConstants (Expr.add e2 e))
| Expr.sub e (Expr.var x), e2 => Expr.lt (Expr.var x) (simplifyConstants (Expr.sub e e2))
| _, _ => Expr.lt e1 e2

def Expr.normalize : Expr → Expr
| Expr.eq e1 e2 => normalizeEq e1 e2
| Expr.add e1 e2 => Expr.add (Expr.normalize e1) (Expr.normalize e2)
| Expr.sub e1 e2 => Expr.sub (Expr.normalize e1) (Expr.normalize e2)
| Expr.mul e1 e2 => Expr.mul (Expr.normalize e1) (Expr.normalize e2)
| Expr.or e1 e2 => Expr.or (Expr.normalize e1) (Expr.normalize e2)
| Expr.and e1 e2 => Expr.and (Expr.normalize e1) (Expr.normalize e2)
| Expr.ge e1 e2 => normalizeGe (Expr.normalize e1) (Expr.normalize e2)
| Expr.le e1 e2 => normalizeLe (Expr.normalize e1) (Expr.normalize e2)
| Expr.gt e1 e2 => normalizeGt (Expr.normalize e1) (Expr.normalize e2)
| Expr.lt e1 e2 => normalizeLt (Expr.normalize e1) (Expr.normalize e2)
| Expr.var x => Expr.var x
| Expr.bool b => Expr.bool b
| Expr.num n => Expr.num n

def Statement.normalize : Statement → Statement
| Statement.atom e => Statement.atom (Expr.normalize e)
| Statement.conj s1 s2 => Statement.conj (Statement.normalize s1) (Statement.normalize s2)
| Statement.disj s1 s2 => Statement.disj (Statement.normalize s1) (Statement.normalize s2)
| Statement.neg s => Statement.neg (Statement.normalize s)
| Statement.impl s1 s2 => Statement.impl (Statement.normalize s1) (Statement.normalize s2)
| Statement.equiv s1 s2 => Statement.equiv (Statement.normalize s1) (Statement.normalize s2)

inductive Expr.Step {Γ : Context} : Expr → Expr → Prop
  | add {n1 n2 : Nat} {e1 e2 : Expr} : Expr.Step e1 (Expr.num n1) → Expr.Step e2 (Expr.num n2) →
      Expr.Step (Expr.add e1 e2) (Expr.num (n1 + n2))
  | sub {n1 n2 : Nat} {e1 e2 : Expr} : Expr.Step e1 (Expr.num n1) → Expr.Step e2 (Expr.num n2) →
      Expr.Step (Expr.sub e1 e2) (Expr.num (n1 - n2))
  | mul {n1 n2 : Nat} {e1 e2 : Expr} : Expr.Step e1 (Expr.num n1) → Expr.Step e2 (Expr.num n2) →
      Expr.Step (Expr.mul e1 e2) (Expr.num (n1 * n2))
  | eq_bool {b1 b2 : Bool} {e1 e2 : Expr} : Expr.Step e1 (Expr.bool b1) → Expr.Step e2 (Expr.bool b2) →
      Expr.Step (Expr.eq e1 e2) (Expr.bool (b1 == b2))
  | eq_num {n1 n2 : Nat} {e1 e2 : Expr} : Expr.Step e1 (Expr.num n1) → Expr.Step e2 (Expr.num n2) →
      Expr.Step (Expr.eq e1 e2) (Expr.bool (n1 == n2))
  | lt {n1 n2 : Nat} {e1 e2 : Expr} : Expr.Step e1 (Expr.num n1) → Expr.Step e2 (Expr.num n2) →
      Expr.Step (Expr.lt e1 e2) (Expr.bool (n1 < n2))
  | gt {n1 n2 : Nat} {e1 e2 : Expr} : Expr.Step e1 (Expr.num n1) → Expr.Step e2 (Expr.num n2) →
      Expr.Step (Expr.gt e1 e2) (Expr.bool (n1 > n2))
  | var {x : String} {v : Val} : Γ.getVal? x = some v → Expr.Step (Expr.var x) v.toExpr

def Expr.isValue : Expr → Prop
  | Expr.num _ => True
  | Expr.bool _ => True
  | _ => False

inductive Com.Step : Context × Com → Context × Com → Prop
  | assign {Γ Γ' : Context} {x : String} {e : Expr} {v : Val} :
      @Expr.Step Γ e v.toExpr →
      Com.Step (Γ, Com.assign x e) (Γ.assign x v, Com.skip)
  | seq {Γ₁ Γ₂ Γ₃ : Context} {c₁ c₂ c₃ : Com} :
      Com.Step (Γ₁, c₁) (Γ₂, Com.skip) →
      Com.Step (Γ₂, c₂) (Γ₃, c₃) → Com.Step (Γ₁, Com.seq c₁ c₂) (Γ₃, c₃)
  | cond_true {Γ : Context} {c₁ c₂ : Com} {e : Expr} :
      @Expr.Step Γ e (Expr.bool .true) →
      Com.Step (Γ, Com.cond e c₁ c₂) (Γ, c₁)
  | cond_false {Γ : Context} {c₁ c₂ : Com} {e : Expr} :
      @Expr.Step Γ e (Expr.bool .false) →
      Com.Step (Γ, Com.cond e c₁ c₂) (Γ, c₁)
  | while_true {Γ Γ' : Context} {c : Com} {e : Expr} :
      @Expr.Step Γ e (Expr.bool .true) →
      Com.Step (Γ, Com.while e c) (Γ, Com.seq c (Com.while e c))
  | while_false {Γ : Context} {c : Com} {e : Expr} :
      @Expr.Step Γ e (Expr.bool .false) →
      Com.Step (Γ, Com.while e c) (Γ, Com.skip)

instance {Γ : Context} : Trans (@Expr.Step Γ) (Relation.TransGen (@Expr.Step Γ)) (Relation.TransGen (@Expr.Step Γ)) where
  trans h₁ h₂ :=  Relation.TransGen.trans (Relation.TransGen.single h₁) h₂

instance {Γ : Context} : Trans (Relation.TransGen (@Expr.Step Γ)) (@Expr.Step Γ) (Relation.TransGen (@Expr.Step Γ)) where
  trans :=  Relation.TransGen.tail

instance {Γ : Context} : Trans (Relation.TransGen (@Expr.Step Γ)) (Relation.TransGen (@Expr.Step Γ)) (Relation.TransGen (@Expr.Step Γ)) where
  trans :=  Relation.TransGen.trans

def Com.reduces (c : Com) (Γ Γ' : Context) : Prop := (Γ, c) ⟹* (Γ', Com.skip)

def Com.equivalent (c1 c2 : Com) : Prop := ∀ (Γ : Context),
  ∃ (Γ' : Context), c1.reduces Γ Γ' → c2.reduces Γ Γ'

def Expr.subst (x : String) (e : Expr) (e' : Expr) : Expr :=
  match e' with
  | Expr.var y => if x == y then e else e'
  | Expr.num n => Expr.num n
  | Expr.bool b => Expr.bool b
  | Expr.add e1 e2 => Expr.add (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.sub e1 e2 => Expr.sub (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.mul e1 e2 => Expr.mul (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.eq e1 e2 => Expr.eq (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.lt e1 e2 => Expr.lt (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.gt e1 e2 => Expr.gt (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.le e1 e2 => Expr.le (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.ge e1 e2 => Expr.ge (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.and e1 e2 => Expr.and (Expr.subst x e e1) (Expr.subst x e e2)
  | Expr.or e1 e2 => Expr.or (Expr.subst x e e1) (Expr.subst x e e2)

def Statement.subst (x : String) (e : Expr) (P : Statement) : Statement :=
  match P with
  | Statement.atom expr => Statement.atom (Expr.subst x e expr)
  | Statement.conj P₁ P₂ => Statement.conj (Statement.subst x e P₁) (Statement.subst x e P₂)
  | Statement.disj P₁ P₂ => Statement.disj (Statement.subst x e P₁) (Statement.subst x e P₂)
  | Statement.neg P' => Statement.neg (Statement.subst x e P')
  | Statement.impl P₁ P₂ => Statement.impl (Statement.subst x e P₁) (Statement.subst x e P₂)
  | Statement.equiv P₁ P₂ => Statement.equiv (Statement.subst x e P₁) (Statement.subst x e P₂)

inductive TripleHolds : Triple → Prop
  | skip {P : Statement} {c : Com} : TripleHolds {$(P)} $(c) {$(P)} 
  | assign {P : Statement} {e : Expr} {x : String} {c : Com} : TripleHolds {$(Statement.subst x e P)} $(c) {$(P)}
  
  
  
  | assign' (P : Statement) (e : Expr) (x : String) (c : Com) : TripleHolds {$(Statement.subst x e P)} $(c) {$(P)}
  
  
  | seq {P Q R : Statement} {c₁ c₂ : Com} :
      TripleHolds {$(P)} $(c₁) {$(Q)} → TripleHolds {$(Q)} $(c₂) {$(R)} →
      TripleHolds {$(P)} $(c₁);$(c₂) {$(Q)}
  | conditional {P Q : Statement} {B : Expr} {c₁ c₂ : Com}:
      TripleHolds {$(P) ∧ $(.atom B)} $(c₁) {$(Q)} → TripleHolds {$(P) ∧ ¬$(.atom B)} $(c₂) {$(Q)} →
      TripleHolds {$(P)} if $(B) then $(c₁) else $(c₂) fi {$(Q)}
  | while {P : Statement} {B : Expr} {c : Com}:
      TripleHolds {$(P) ∧ $(.atom B)} $(c) {$(Q)} →
      TripleHolds {$(P)} while $(B) do $(c) od {$(P) ∧ ¬$(.atom B)}
  | impl {P₁ P₂ Q₁ Q₂ : Statement} {c : Com}:
      (∀ Γ, P₁.eval Γ → P₂.eval Γ) → (∀ Γ, Q₂.eval Γ → Q₁.eval Γ) →
      TripleHolds {$(P₂)} $(c) {$(Q₂)} → TripleHolds {$(P₁)} $(c) {$(Q₁)}

inductive Ty
| num : Ty
| bool : Ty
deriving Repr, DecidableEq

inductive WellTyped : Expr → Ty → Prop
| num : WellTyped (Expr.num _) Ty.num
| bool : WellTyped (Expr.bool _) Ty.bool
| add : ∀ e1 e2, WellTyped e1 Ty.num → WellTyped e2 Ty.num →
    WellTyped (Expr.add e1 e2) Ty.num
| sub : ∀ e1 e2, WellTyped e1 Ty.num → WellTyped e2 Ty.num →
    WellTyped (Expr.sub e1 e2) Ty.num
| mul : ∀ e1 e2, WellTyped e1 Ty.num → WellTyped e2 Ty.num →
    WellTyped (Expr.mul e1 e2) Ty.num
| eq : ∀ e1 e2 t, WellTyped e1 t → WellTyped e2 t →
    WellTyped (Expr.eq e1 e2) Ty.bool
| lt : ∀ e1 e2, WellTyped e1 Ty.num → WellTyped e2 Ty.num →
    WellTyped (Expr.lt e1 e2) Ty.bool
| gt : ∀ e1 e2, WellTyped e1 Ty.num → WellTyped e2 Ty.num →
    WellTyped (Expr.gt e1 e2) Ty.bool
| le : ∀ e1 e2, WellTyped e1 Ty.num → WellTyped e2 Ty.num →
    WellTyped (Expr.le e1 e2) Ty.bool
| ge : ∀ e1 e2, WellTyped e1 Ty.num → WellTyped e2 Ty.num →
    WellTyped (Expr.ge e1 e2) Ty.bool
| and : ∀ e1 e2, WellTyped e1 Ty.bool → WellTyped e2 Ty.bool →
    WellTyped (Expr.and e1 e2) Ty.bool
| or : ∀ e1 e2, WellTyped e1 Ty.bool → WellTyped e2 Ty.bool →
    WellTyped (Expr.or e1 e2) Ty.bool

def Expr.ty : Expr → Option Ty
  | Expr.num _ => Ty.num
  | Expr.bool _ => Ty.bool
  | Expr.add e1 e2 => if e1.ty = some .num ∧ e2.ty = some .num then some .num else none
  | Expr.sub e1 e2 => if e1.ty = some .num ∧ e2.ty = some .num then some .num else none
  | Expr.mul e1 e2 => if e1.ty = some .num ∧ e2.ty = some .num then some .num else none
  | Expr.eq e1 e2 => if e1.ty = e2.ty ∧ e1.ty.isSome then some .bool else none
  | Expr.lt e1 e2 => if e1.ty = some .num ∧ e2.ty = some .num then some .bool else none
  | Expr.gt e1 e2 => if e1.ty = some .num ∧ e2.ty = some .num then some .bool else none
  | Expr.le e1 e2 => if e1.ty = some .num ∧ e2.ty = some .num then some .bool else none
  | Expr.ge e1 e2 => if e1.ty = some .num ∧ e2.ty = some .num then some .bool else none
  | Expr.and e1 e2 => if e1.ty = some .bool ∧ e2.ty = some .bool then some .bool else none
  | Expr.or e1 e2 => if e1.ty = some .bool ∧ e2.ty = some .bool then some .bool else none
  | Expr.var _ => none 

def WellTyped.decide (e : Expr) (ty : Ty) : Decidable (WellTyped e ty) :=
  match e with
    | Expr.num _ => match ty with
      | .num => isTrue WellTyped.num
      | .bool => isFalse (by admit /- proof elided -/
      )
    | Expr.bool _ => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => isTrue WellTyped.bool
    | Expr.add e1 e2 => match ty with
      | .num => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.add e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
      | .bool => isFalse (by admit /- proof elided -/
      )
    | Expr.sub e1 e2 => match ty with
      | .num => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.sub e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
      | .bool => isFalse (by admit /- proof elided -/
      )
    | Expr.mul e1 e2 => match ty with
      | .num => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.mul e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
      | .bool => isFalse (by admit /- proof elided -/
      )
    | Expr.eq e1 e2 => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.eq e1 e2 .num h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse _ =>  match WellTyped.decide e1 Ty.bool with
          | isTrue h1 => match WellTyped.decide e2 Ty.bool with
             | isTrue h2 => isTrue (WellTyped.eq e1 e2 .bool h1 h2)
             | isFalse h2 => isFalse (by admit /- proof elided -/
             )
          | isFalse h1 => isFalse (by admit /- proof elided -/
          )
    | Expr.lt e1 e2 => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.lt e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
    | Expr.gt e1 e2 => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.gt e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
    | Expr.le e1 e2 => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.le e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
    | Expr.ge e1 e2 => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => match WellTyped.decide e1 Ty.num with
        | isTrue h1 => match WellTyped.decide e2 Ty.num with
           | isTrue h2 => isTrue (WellTyped.ge e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
    | Expr.and e1 e2 => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => match WellTyped.decide e1 Ty.bool with
        | isTrue h1 => match WellTyped.decide e2 Ty.bool with
           | isTrue h2 => isTrue (WellTyped.and e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
    | Expr.or e1 e2 => match ty with
      | .num => isFalse (by admit /- proof elided -/
      )
      | .bool => match WellTyped.decide e1 Ty.bool with
        | isTrue h1 => match WellTyped.decide e2 Ty.bool with
           | isTrue h2 => isTrue (WellTyped.or e1 e2 h1 h2)
           | isFalse h2 => isFalse (by admit /- proof elided -/
           )
        | isFalse h1  => isFalse (by admit /- proof elided -/
        )
    | Expr.var _ => isFalse (by admit /- proof elided -/
    ) 

instance {e : Expr} {ty : Ty} : Decidable (WellTyped e ty) := WellTyped.decide e ty

def Expr.isBool (e : Expr) : Prop := e.ty = some .bool

def Expr.isNum (e : Expr) : Prop := e.ty = some .num

inductive Statement
  | atom : While.Expr → Statement
  | disj : Statement → Statement → Statement
  | conj : Statement → Statement → Statement
  | neg : Statement → Statement
  | impl : Statement → Statement → Statement
  | equiv : Statement → Statement → Statement
deriving DecidableEq

instance : Coe (Lean.TSyntax `expr) (Lean.TSyntax `stmt) where
  coe s := ⟨s.raw⟩

@[app_unexpander Statement.atom]
def unexpandAtom : Lean.PrettyPrinter.Unexpander
  | `($_ [bexpr| $e:bexpr]) => `([stmt| $e:bexpr])
  | _ => throw ()

@[app_unexpander Statement.disj]
def unexpandDisj : Lean.PrettyPrinter.Unexpander
  | `($_ [stmt| $p:stmt] [stmt| $q:stmt]) => `([stmt| $p ∨ $q])
  | _ => throw ()

@[app_unexpander Statement.conj]
def unexpandConj : Lean.PrettyPrinter.Unexpander
  | `($_ [stmt| $p:stmt] [stmt| $q:stmt]) => `([stmt| $p ∧ $q])
  | _ => throw ()

@[app_unexpander Statement.neg]
def unexpandNeg : Lean.PrettyPrinter.Unexpander
  | `($_ [stmt| $p:stmt]) => `([stmt| ¬$p])
  | _ => throw ()

@[app_unexpander Statement.impl]
def unexpandImpl : Lean.PrettyPrinter.Unexpander
  | `($_ [stmt| $p:stmt] [stmt| $q:stmt]) => `([stmt| $p ⇒ $q])
  | _ => throw ()

@[app_unexpander Statement.equiv]
def unexpandEquiv : Lean.PrettyPrinter.Unexpander
  | `($_ [stmt| $p:stmt] [stmt| $q:stmt]) => `([stmt| $p ⇔ $q])
  | _ => throw ()

def Statement.eval (Γ : While.Context) : Statement  → Prop
  | atom e => match e.val? Γ with
    | some (While.Val.bool b) => (b = .true)
    | _ => False
  | disj p q => p.eval Γ ∨ q.eval Γ
  | conj p q => p.eval Γ ∧ q.eval Γ
  | neg p => ¬ p.eval Γ
  | impl p q => p.eval Γ → q.eval Γ
  | equiv p q => p.eval Γ ↔ q.eval Γ

instance {Γ : While.Context} {e : While.Expr} : Decidable (Statement.eval Γ (Statement.atom e)) :=
   match While.decideVal? (Γ:=Γ) (e:=e) with
       | isTrue h => isTrue (by admit /- proof elided -/
       )
       | isFalse h => isFalse <| by
         simp [Statement.eval]
         cases he : e.val? Γ
         · simp
         · case some v =>
            cases hv : v
            · case num _ => simp
            · case bool b =>
                cases hb : b
                · case «false» => simp
                · case «true» => rw [he, hv, hb] at h; simp_all

def Statement.decidable  (Γ  : While.Context) (s : Statement) : Decidable (Statement.eval Γ s) :=
   match s with
     | .atom e => inferInstance
     | .disj p q => match decidable Γ p with
       | isTrue h =>  isTrue (Or.inl h)
       | isFalse h => match decidable Γ q with
         | isTrue h' => isTrue (Or.inr h')
         | isFalse h' => isFalse (by admit /- proof elided -/
         )
      | .conj p q => match decidable Γ p with
        | isTrue h => match decidable Γ q with
          | isTrue h' => isTrue ⟨h, h'⟩
          | isFalse h' => isFalse (by admit /- proof elided -/
          )
        | isFalse h => isFalse (by admit /- proof elided -/
        )
      | .neg p => match decidable Γ p with
        | isTrue h => isFalse (by admit /- proof elided -/
        )
        | isFalse h => isTrue (by admit /- proof elided -/
        )
      | .impl p q => match decidable Γ p with
        | isTrue h => match decidable Γ q with
          | isTrue h' => isTrue (by admit /- proof elided -/
          )
          | isFalse h' => isFalse (by admit /- proof elided -/
          )
        | isFalse h => isTrue (by admit /- proof elided -/
        )
      | .equiv p q => match decidable Γ p with
        | isTrue h => match decidable Γ q with
          | isTrue h' => isTrue (by admit /- proof elided -/
          )
          | isFalse h' => isFalse (by admit /- proof elided -/
          )
        | isFalse h => match decidable Γ q with
          | isTrue h' => isFalse (by admit /- proof elided -/
          )
          | isFalse h' => isTrue (by admit /- proof elided -/
          )

instance {s : Statement} {Γ  : While.Context} : Decidable (Statement.eval Γ s) := Statement.decidable Γ s

inductive Val
  | num : Nat → Val
  | bool : Bool → Val

instance : Coe Nat Val := ⟨Val.num⟩

instance : Coe Bool Val := ⟨Val.bool⟩

instance {n : Nat} : CoeDep Val (Val.num n) Nat := ⟨n⟩

instance {b : Bool} : CoeDep Val (Val.bool b) Bool := ⟨b⟩

instance : OfNat Val n := ⟨Val.num n⟩

def Val.toExpr : Val → Expr
  | Val.num n => Expr.num n
  | Val.bool b => Expr.bool b

instance : Repr Val where
  reprPrec
    | Val.num n => reprPrec n
    | Val.bool b => reprPrec b

instance : Coe Val Expr := ⟨Val.toExpr⟩

abbrev Context := List (String × Val)

def Context.getVal? (ctx : Context) (x : String) : Option Val := ctx.lookup x

def Context.assign (ctx : Context) (x : String) (v : Val) : Context :=
  match ctx.lookup x with
    | none  => (x, v) :: ctx
    | some _ =>  ctx.map (fun (x', v') => if x' == x then (x, v) else (x', v'))

def Context.empty : Context := []

instance : EmptyCollection Context := ⟨Context.empty⟩

def Context.reprPrec : Context → Nat → Std.Format
  | [], _ => Std.Format.nil
  | (x, v) :: ctx, n => x ++ " ↦ " ++ repr v ++ "; " ++ reprPrec ctx n

instance : Repr Context := ⟨Context.reprPrec⟩

private def testCtxt : Context := [ x ↦ 1]c

def foo : Triple :=
{(X + 1) == 2}
X := X + 1
{X == 2}

def foo' : Triple :=
{(X + 1) == 2}
X := X + 2
{X == 2}

structure Triple where
  (P : While.Statement)
  (c : While.Com)
  (Q : While.Statement)

@[app_unexpander Hoare.Triple.mk]
def unexpandTriple : Lean.PrettyPrinter.Unexpander
  | `($_ [stmt| $p] [com| $c] [stmt| $q]) => `({$p} $c {$q})
  | `($_ [stmt| $p] $c:term [stmt| $q]) => `({$p} $($c) {$q})
  | `($_ $p:term $c:term [stmt| $q]) => `({$($p)} $($c) {$q})
  | `($_ $p:term [com| $c] $q:term) => `({$($p)} $c {$($q)})
  | _ => throw ()

def Expr.val? (Γ : Context) : Expr → Option Val
  | Expr.num n => Val.num n
  | Expr.bool b => Val.bool b
  | Expr.var x => Γ.getVal? x
  | Expr.add e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.num (n1 + n2))
    | _, _ => none
  | Expr.sub e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.num (n1 - n2))
    | _, _ => none
  | Expr.mul e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.num (n1 * n2))
    | _, _ => none
  | Expr.eq e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.bool (n1 == n2))
    | some (Val.bool b1), some (Val.bool b2) => some (Val.bool (b1 == b2))
    | _, _ => none
  | Expr.lt e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.bool (n1 < n2))
    | _, _ => none
  | Expr.gt e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.bool (n1 > n2))
    | _, _ => none
  | Expr.le e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.bool (n1 ≤ n2))
    | _, _ => none
  | Expr.ge e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.num n1), some (Val.num n2) => some (Val.bool (n1 ≥ n2))
    | _, _ => none
  | Expr.and e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.bool b1), some (Val.bool b2) => some (Val.bool (b1 && b2))
    | _, _ => none
  | Expr.or e1 e2 => match e1.val? Γ, e2.val? Γ with
    | some (Val.bool b1), some (Val.bool b2) => some (Val.bool (b1 || b2))
    | _, _ => none

partial def Com.eval (Γ : Context := Context.empty) : Com → Context
  | Com.skip => Γ
  | Com.assign x e => match Expr.val? Γ e with
    | some v => Γ.assign x v
    | none => Γ
  | Com.seq c₁ c₂ => Com.eval (Com.eval Γ c₁) c₂
  | Com.cond e c₁ c₂ => match Expr.val? Γ e with
    | some (Val.bool .true) => Com.eval Γ c₁
    | some (Val.bool .false) => Com.eval Γ c₂
    | _ => Γ
  | Com.while e c => match Expr.val? Γ e with
    | some (Val.bool .true) => Com.eval (Com.eval Γ c) (Com.while e c)
    | some (Val.bool .false) => Γ
    | _ => Γ

instance decideVal? {Γ : Context} {e : Expr} : Decidable (e.val? Γ =  some (Val.bool .true)) :=
  match e.val? Γ with
    | some (Val.bool .true) => isTrue rfl
    | some (Val.bool .false) => isFalse (by admit /- proof elided -/
    )
    | some (Val.num _) => isFalse (by admit /- proof elided -/
    )
    | none => isFalse (by admit /- proof elided -/
    )

def Val.ty : Val → Ty
  | num _ => .num
  | bool _ => .bool

def Expr.val_ty (e : Expr) (t : Ty) : Prop :=
  ∀ Γ, ∀ val, (e.val? Γ = .some val) → val.ty = t

IO in Init.System.IO

Unit in Init.Prelude

IO.println in Init.System.IO

String in Init.Prelude

impl in Mathlib.Deprecated.MLList.BestFirst

DecidableEq in Init.Prelude

Coe in Init.Coe

Lean.TSyntax in Init.Prelude

Lean.PrettyPrinter.Unexpander in Init.Prelude

Decidable in Init.Prelude

bool in Init.Control.Basic

Or in Init.Prelude

Or.inl in Init.Prelude

Or.inr in Init.Prelude

Eq in Init.Prelude

Equivalence in Init.Core

Nat in Init.Prelude

Bool in Init.Prelude

CoeDep in Init.Coe

OfNat in Init.Prelude

Repr in Init.Data.Repr

List in Init.Prelude

Option in Init.Prelude

EmptyCollection in Init.Core

Std.Format in Init.Data.Format.Basic

Std.Format.nil in Init.Data.Format.Basic

repr in Init.Data.Repr

Relation.TransGen in Init.Core

Trans in Init.Prelude

Relation.TransGen.single in Init.Core

Relation.TransGen.tail in Init.Core

cond in Init.Prelude

Lean.Name in Init.Prelude

Lean.Name.mkSimple in Init.Prelude

Lean.mkIdent in Init.Meta.Defs

Repr.reprPrec in Init.Data.Repr

Std.Format.line in Init.Data.Format.Basic

Option.isSome in Init.Data.Option.Basic
</all_available_defs>

<all_available_lemmas>
theorem equiv_symm {P Q : Expr} : equiv P Q → equiv Q P

theorem equiv_trans {P Q R : Expr} : equiv P Q → equiv Q R → equiv P R

theorem equiv_refl (P : Expr) : equiv P P

theorem equiv'_equiv_eval (S T : Statement) : equiv' S T ↔ ∀ Γ,(Statement.equiv S T).eval Γ

theorem equiv_symm {P Q : Statement} : equiv' P Q → equiv' Q P

theorem equiv_trans {P Q R : Statement} : equiv' P Q → equiv' Q R → equiv' P R

theorem equiv_refl (P : Statement) : equiv' P P

theorem equiv_expr_equiv_atoms {e₁ e₂ : Expr} :
   e₁.equiv e₂ → (Statement.atom e₁).equiv' (Statement.atom e₂)

theorem bool_atoms_bool_expr_equiv {e₁ e₂ : Expr} :
  (Statement.atom e₁).equiv' (Statement.atom e₂) → e₁.isBool → e₁.equiv e₂

theorem sqrt_spec_holds : ∀ x, TripleHolds (sqrt_spec x)

theorem simplifyConstants_preserves_eval (e : Expr) (Γ : Context) :
  Expr.val? Γ (simplifyConstants e) = Expr.val? Γ e

theorem normalizeEq_equiv (e₁ e₂ : Expr) (Γ : Context) :
  Expr.val? Γ (normalizeEq e₁ e₂) = Expr.val? Γ (Expr.eq e₁ e₂)

 theorem NormalizeAdd (Γ : Context) (x : String) (e e2 : Expr) :
  Expr.val? Γ (Expr.eq (Expr.add (Expr.var x) e) e2) =
  Expr.val? Γ (normalizeEq (Expr.add (Expr.var x) e) e2)

theorem NormalisEquiv (P : Expr) : Equiv.expressions (Expr.normalize P) P

theorem foo_holds' : TripleHolds foo

theorem foo'_holds : TripleHolds foo'

theorem Expr.val_add {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.add e₁ e₂).val? Γ = val →
  ∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.num (n₁ + n₂)

theorem Expr.val_sub {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.sub e₁ e₂).val? Γ = val →
  ∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.num (n₁ - n₂)

theorem Expr.val_mul {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.mul e₁ e₂).val? Γ = val →
  ∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.num (n₁ * n₂)

theorem Expr.val_eq {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.eq e₁ e₂).val? Γ = val →
  (∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.bool (n₁ == n₂)) ∨
  (∃ b₁ b₂, e₁.val? Γ = Val.bool b₁ ∧ e₂.val? Γ = Val.bool b₂ ∧ val = Val.bool (b₁ == b₂))

theorem Expr.val_lt {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.lt e₁ e₂).val? Γ = val →
  ∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.bool (n₁ < n₂)

theorem Expr.val_gt {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.gt e₁ e₂).val? Γ = val →
  ∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.bool (n₁ > n₂)

theorem Expr.val_le {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.le e₁ e₂).val? Γ = val →
  ∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.bool (n₁ ≤ n₂)

theorem Expr.val_ge {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.ge e₁ e₂).val? Γ = val →
  ∃ n₁ n₂, e₁.val? Γ = Val.num n₁ ∧ e₂.val? Γ = Val.num n₂ ∧ val = Val.bool (n₁ ≥ n₂)

theorem Expr.val_and {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.and e₁ e₂).val? Γ = val →
  ∃ b₁ b₂, e₁.val? Γ = Val.bool b₁ ∧ e₂.val? Γ = Val.bool b₂ ∧ val = Val.bool (b₁ && b₂)

theorem Expr.val_or {e₁ e₂ : Expr} {val : Val} {Γ : Context} :
   (Expr.or e₁ e₂).val? Γ = val →
  ∃ b₁ b₂, e₁.val? Γ = Val.bool b₁ ∧ e₂.val? Γ = Val.bool b₂ ∧ val = Val.bool (b₁ || b₂)

theorem Expr.var_not_val_ty (s) : ∀ t : Ty, ¬ (Expr.var s).val_ty t

theorem Expr.well_typed_val {t : Ty} {e : Expr} : WellTyped e t ↔ e.val_ty t
</all_available_lemmas>

<local_ctx>
import Hoare.While.Syntax

namespace While

inductive Ty
| num : Ty
| bool : Ty
deriving Repr, DecidableEq
</local_ctx>

<target_theorem>
theorem WellTyped.not_welltyped_not_eq_ty {e1 e2 : Expr} {t : Ty} :
  WellTyped e1 t → ¬ WellTyped e2 t → ∀ t', ¬ (WellTyped (Expr.eq e1 e2) t') :=
</target_theorem>

