Imp.lean

import Maps
-- ------------------ ARITHMETIC AND BOOLEAN EXPRESSIONS -----------------------

-- Arithmetic expressions
inductive AExp : Type where
  | ANum (n : Nat)
  | APlus (a1 a2 : AExp)
  | AMinus (a1 a2 : AExp)
  | AMult (a1 a2 : AExp)

-- Boolean expressions
inductive BExp : Type where
  | BTrue
  | BFalse
  | BEq (a1 a2 : AExp)
  | BNeq (a1 a2 : AExp)
  | BLe (a1 a2 : AExp)
  | BGt (a1 a2 : AExp)
  | BNot (b : BExp)
  | BAnd (b1 b2 : BExp)

open AExp BExp

-- ------------------ EVALUATION -----------------------

-- Evaluate arithmetic expression to Nat
def aeval (a : AExp) : Nat :=
  match a with
  | ANum n => n
  | APlus a1 a2 => aeval a1 + aeval a2
  | AMinus a1 a2 => aeval a1 - aeval a2
  | AMult a1 a2 => aeval a1 * aeval a2

example : aeval (APlus (ANum 2) (ANum 2)) = 4 := rfl

-- Evaluate boolean expression to Bool
-- Coq: =? is Nat.eqb, <=? is Nat.leb, negb is !, andb is &&
def beval (b : BExp) : Bool :=
  match b with
  | BTrue => true
  | BFalse => false
  | BExp.BEq a1 a2 => aeval a1 == aeval a2
  | BNeq a1 a2 => !(aeval a1 == aeval a2)
  | BLe a1 a2 => aeval a1 ≤ aeval a2   -- Nat has Decidable LE, returns Bool in this context
  | BGt a1 a2 => !(aeval a1 ≤ aeval a2)
  | BNot b1 => !beval b1
  | BAnd b1 b2 => beval b1 && beval b2

-- ------------------ OPTIMIZATION -----------------------

-- Remove 0 + e, replacing with just e
def optimize_0plus (a : AExp) : AExp :=
  match a with
  | ANum n => ANum n
  | APlus (ANum 0) e2 => optimize_0plus e2
  | APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2)
  | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2)
  | AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2)

example : optimize_0plus (APlus (ANum 2)
                           (APlus (ANum 0)
                             (APlus (ANum 0) (ANum 1))))
          = APlus (ANum 2) (ANum 1) := rfl

theorem optimize_0plus_sound (a : AExp) : aeval (optimize_0plus a) = aeval a := by
  induction a with
  | ANum n => rfl
  | APlus a1 a2 IHa1 IHa2 =>
    cases a1 with
    | ANum n =>
      cases n with
      | zero => simp_all [optimize_0plus, aeval]
      | succ n => simp_all [optimize_0plus, aeval]
    | APlus _ _ => simp_all [optimize_0plus, aeval]
    | AMinus _ _ => simp_all [optimize_0plus, aeval]
    | AMult _ _ => simp_all [optimize_0plus, aeval]
  | AMinus a1 a2 IHa1 IHa2 => simp_all [optimize_0plus, aeval]
  | AMult a1 a2 IHa1 IHa2 => simp_all [optimize_0plus, aeval]


-- ------------------ ROCQ AUTOMATION -----------------------

-- Coq's `try T` = Lean's `try T`
-- If T fails, `try T` does nothing instead of failing

theorem silly1 (P : Prop) (HP : P) : P := by
  try rfl  -- would fail, but try catches it
  exact HP

theorem silly2 (ae : AExp) : aeval ae = aeval ae := by
  try rfl  -- succeeds

-- Coq's `T1; T2` applies T2 to all goals generated by T1
-- Lean's `<;>` does the same
theorem foo (n : Nat) : (0 ≤ n) = true := by
  cases n
  · simp
  · simp

theorem foo' (n : Nat) : (0 ≤ n) = true := by
  cases n <;> simp

theorem optimize_0plus_sound' (a : AExp) : aeval (optimize_0plus a) = aeval a := by
  induction a with
  | ANum n => rfl
  | APlus a1 a2 IHa1 IHa2 =>
    cases a1 with
    | ANum n => cases n <;> simp_all [optimize_0plus, aeval]
    | _ => simp_all [optimize_0plus, aeval]
  | _ => simp_all [optimize_0plus, aeval]

-- ------------------ THE REPEAT TACTICAL -----------------------

-- Coq's `repeat T` keeps applying T until it fails
-- Lean's `repeat T` does the same

-- List membership: Lean uses `∈` for List.Mem
theorem In10 : 10 ∈ [1,2,3,4,5,6,7,8,9,10] := by
  repeat (first | exact List.Mem.head _ | apply List.Mem.tail)

-- Alternative
theorem In10' : 10 ∈ [1,2,3,4,5,6,7,8,9,10] := by
  decide  -- Lean can just compute this

-- Warning: repeat with a tactic that always succeeds will loop forever
-- theorem repeat_loop (m n : Nat) : m + n = n + m := by
--   repeat rw [Nat.add_comm]  -- infinite loop!


def optimize_0plus_b (b : BExp) : BExp :=
  match b with
  | BTrue => BTrue
  | BFalse => BFalse
  | BExp.BEq a1 a2 => BEq (optimize_0plus a1) (optimize_0plus a2)
  | BNeq a1 a2 => BNeq (optimize_0plus a1) (optimize_0plus a2)
  | BLe a1 a2 => BLe (optimize_0plus a1) (optimize_0plus a2)
  | BGt a1 a2 => BGt (optimize_0plus a1) (optimize_0plus a2)
  | BNot b1 => BNot (optimize_0plus_b b1)
  | BAnd b1 b2 => BAnd (optimize_0plus_b b1) (optimize_0plus_b b2)

example : optimize_0plus_b (BNot (BGt (APlus (ANum 0) (ANum 4)) (ANum 8)))
        = BNot (BGt (ANum 4) (ANum 8)) := rfl

example : optimize_0plus_b (BAnd (BLe (APlus (ANum 0) (ANum 4)) (ANum 5)) BTrue)
        = BAnd (BLe (ANum 4) (ANum 5)) BTrue := rfl

theorem optimize_0plus_b_sound (b : BExp) : beval (optimize_0plus_b b) = beval b := by
  induction b with
  | BTrue => rfl
  | BFalse => rfl
  | BEq a1 a2 => simp [optimize_0plus_b, beval, optimize_0plus_sound]
  | BNeq a1 a2 => simp [optimize_0plus_b, beval, optimize_0plus_sound]
  | BLe a1 a2 => simp [optimize_0plus_b, beval, optimize_0plus_sound]
  | BGt a1 a2 => simp [optimize_0plus_b, beval, optimize_0plus_sound]
  | BNot b1 IHb1 => simp [optimize_0plus_b, beval, IHb1]
  | BAnd b1 b2 IHb1 IHb2 => simp [optimize_0plus_b, beval, IHb1, IHb2]

-- ------------------ DEFINING NEW TACTICS -----------------------

-- Coq's `Ltac invert H := inversion H; subst; clear H`
-- Lean uses macros to define custom tactics
macro "invert" h:ident : tactic =>
  `(tactic| (cases $h:ident; subst_vars))

theorem invert_example1 (a b c : Nat) (H : [a, b] = [a, c]) : b = c := by
  invert H
  rfl

-- ------------------ THE OMEGA TACTIC -----------------------

-- Coq's `lia` is Lean's `omega`
example (m n o p : Nat) (H : m + n ≤ n + o ∧ o + 3 = p + 3) : m ≤ p := by
  omega

example (m n : Nat) : m + n = n + m := by
  omega

example (m n p : Nat) : m + (n + p) = m + n + p := by
  omega

-- ------------------ EVALUATION AS A RELATION -----------------------

-- Instead of a function aeval : AExp → Nat, define a relation
-- aevalR : AExp → Nat → Prop

inductive AEvalR : AExp → Nat → Prop where
  | E_ANum (n : Nat) : AEvalR (ANum n) n
  | E_APlus (e1 e2 : AExp) (n1 n2 : Nat) :
      AEvalR e1 n1 → AEvalR e2 n2 → AEvalR (APlus e1 e2) (n1 + n2)
  | E_AMinus (e1 e2 : AExp) (n1 n2 : Nat) :
      AEvalR e1 n1 → AEvalR e2 n2 → AEvalR (AMinus e1 e2) (n1 - n2)
  | E_AMult (e1 e2 : AExp) (n1 n2 : Nat) :
      AEvalR e1 n1 → AEvalR e2 n2 → AEvalR (AMult e1 e2) (n1 * n2)

-- Notation: Coq uses `e ==> n`, we use infix
infix:50 " ==> " => AEvalR

-- ------------------ EQUIVALENCE OF DEFINITIONS -----------------------

theorem aevalR_iff_aeval (a : AExp) (n : Nat) : (a ==> n) ↔ aeval a = n := by
  constructor
  -- → direction: relation implies function
  · intro H
    induction H with
    | E_ANum n => rfl
    | E_APlus _ _ _ _ _ _ IH1 IH2 => simp [aeval, IH1, IH2]
    | E_AMinus _ _ _ _ _ _ IH1 IH2 => simp [aeval, IH1, IH2]
    | E_AMult _ _ _ _ _ _ IH1 IH2 => simp [aeval, IH1, IH2]
  -- ← direction: function implies relation
  · intro H
    induction a generalizing n with
    | ANum m => simp [aeval] at H; subst H; exact AEvalR.E_ANum m
    | APlus a1 a2 IH1 IH2 =>
      simp [aeval] at H; subst H
      exact AEvalR.E_APlus a1 a2 _ _ (IH1 _ rfl) (IH2 _ rfl)
    | AMinus a1 a2 IH1 IH2 =>
      simp [aeval] at H; subst H
      exact AEvalR.E_AMinus a1 a2 _ _ (IH1 _ rfl) (IH2 _ rfl)
    | AMult a1 a2 IH1 IH2 =>
      simp [aeval] at H; subst H
      exact AEvalR.E_AMult a1 a2 _ _ (IH1 _ rfl) (IH2 _ rfl)

-- ------------------ BOOLEAN EVALUATION RELATION -----------------------

inductive BEvalR : BExp → Bool → Prop where
  | E_BTrue : BEvalR BTrue true
  | E_BFalse : BEvalR BFalse false
  | E_BEq (e1 e2 : AExp) (n1 n2 : Nat) :
      AEvalR e1 n1 → AEvalR e2 n2 → BEvalR (BEq e1 e2) (n1 == n2)
  | E_BNeq (e1 e2 : AExp) (n1 n2 : Nat) :
      AEvalR e1 n1 → AEvalR e2 n2 → BEvalR (BNeq e1 e2) (!(n1 == n2))
  | E_BLe (e1 e2 : AExp) (n1 n2 : Nat) :
      AEvalR e1 n1 → AEvalR e2 n2 → BEvalR (BLe e1 e2) (decide (n1 ≤ n2))
  | E_BGt (e1 e2 : AExp) (n1 n2 : Nat) :
      AEvalR e1 n1 → AEvalR e2 n2 → BEvalR (BGt e1 e2) (!(decide (n1 ≤ n2)))
  | E_BNot (e : BExp) (b : Bool) :
      BEvalR e b → BEvalR (BNot e) (!b)
  | E_BAnd (e1 e2 : BExp) (b1 b2 : Bool) :
      BEvalR e1 b1 → BEvalR e2 b2 → BEvalR (BAnd e1 e2) (b1 && b2)

infix:50 " ==>b " => BEvalR

theorem bevalR_iff_beval (b : BExp) (bv : Bool) : (b ==>b bv) ↔ beval b = bv := by
  constructor
  · intro H
    induction H with
    | E_BTrue => rfl
    | E_BFalse => rfl
    | E_BEq _ _ n1 n2 H1 H2 =>
      simp [beval, (aevalR_iff_aeval _ _).mp H1, (aevalR_iff_aeval _ _).mp H2]
    | E_BNeq _ _ n1 n2 H1 H2 =>
      simp [beval, (aevalR_iff_aeval _ _).mp H1, (aevalR_iff_aeval _ _).mp H2]
    | E_BLe _ _ n1 n2 H1 H2 =>
      simp [beval, (aevalR_iff_aeval _ _).mp H1, (aevalR_iff_aeval _ _).mp H2]
    | E_BGt _ _ n1 n2 H1 H2 =>
      simp [beval, (aevalR_iff_aeval _ _).mp H1, (aevalR_iff_aeval _ _).mp H2]
    | E_BNot _ _ _ IH => simp [beval, IH]
    | E_BAnd _ _ _ _ _ _ IH1 IH2 => simp [beval, IH1, IH2]
  · intro H
    induction b generalizing bv with
    | BTrue => simp [beval] at H; subst H; exact BEvalR.E_BTrue
    | BFalse => simp [beval] at H; subst H; exact BEvalR.E_BFalse
    | BEq a1 a2 =>
      simp [beval] at H; subst H
      exact BEvalR.E_BEq a1 a2 _ _ ((aevalR_iff_aeval _ _).mpr rfl) ((aevalR_iff_aeval _ _).mpr rfl)
    | BNeq a1 a2 =>
      rw [← H]
      exact BEvalR.E_BNeq a1 a2 _ _ ((aevalR_iff_aeval _ _).mpr rfl) ((aevalR_iff_aeval _ _).mpr rfl)
    | BLe a1 a2 =>
      simp [beval] at H; rw [← H]
      exact BEvalR.E_BLe a1 a2 _ _ ((aevalR_iff_aeval _ _).mpr rfl) ((aevalR_iff_aeval _ _).mpr rfl)
    | BGt a1 a2 =>
      rw [← H]
      exact BEvalR.E_BGt a1 a2 _ _ ((aevalR_iff_aeval _ _).mpr rfl) ((aevalR_iff_aeval _ _).mpr rfl)
    | BNot b1 IH =>
      rw [← H]
      exact BEvalR.E_BNot b1 _ (IH _ rfl)
    | BAnd b1 b2 IH1 IH2 =>
      simp [beval] at H; subst H
      exact BEvalR.E_BAnd b1 b2 _ _ (IH1 _ rfl) (IH2 _ rfl)

-- ------------------ COMPUTATIONAL VS RELATIONAL DEFINITIONS -----------------------

-- Example: Adding division - hard with functions (what is 5/0?), easy with relations

namespace AEvalR_Division

inductive AExp' : Type where
  | ANum (n : Nat)
  | APlus (a1 a2 : AExp')
  | AMinus (a1 a2 : AExp')
  | AMult (a1 a2 : AExp')
  | ADiv (a1 a2 : AExp')  -- NEW

open AExp'

inductive AEvalR' : AExp' → Nat → Prop where
  | E_ANum (n : Nat) : AEvalR' (ANum n) n
  | E_APlus (a1 a2 : AExp') (n1 n2 : Nat) :
      AEvalR' a1 n1 → AEvalR' a2 n2 → AEvalR' (APlus a1 a2) (n1 + n2)
  | E_AMinus (a1 a2 : AExp') (n1 n2 : Nat) :
      AEvalR' a1 n1 → AEvalR' a2 n2 → AEvalR' (AMinus a1 a2) (n1 - n2)
  | E_AMult (a1 a2 : AExp') (n1 n2 : Nat) :
      AEvalR' a1 n1 → AEvalR' a2 n2 → AEvalR' (AMult a1 a2) (n1 * n2)
  | E_ADiv (a1 a2 : AExp') (n1 n2 n3 : Nat) :  -- NEW
      AEvalR' a1 n1 → AEvalR' a2 n2 → n2 > 0 → n2 * n3 = n1 → AEvalR' (ADiv a1 a2) n3

-- This relation is partial: ADiv (ANum 5) (ANum 0) has no evaluation

end AEvalR_Division

-- Example: Nondeterminism - impossible with functions, easy with relations

namespace AEvalR_Extended

inductive AExp'' : Type where
  | AAny            -- NEW: evaluates to any number
  | ANum (n : Nat)
  | APlus (a1 a2 : AExp'')
  | AMinus (a1 a2 : AExp'')
  | AMult (a1 a2 : AExp'')

open AExp''

inductive AEvalR'' : AExp'' → Nat → Prop where
  | E_Any (n : Nat) : AEvalR'' AAny n  -- NEW: any n is valid
  | E_ANum (n : Nat) : AEvalR'' (ANum n) n
  | E_APlus (a1 a2 : AExp'') (n1 n2 : Nat) :
      AEvalR'' a1 n1 → AEvalR'' a2 n2 → AEvalR'' (APlus a1 a2) (n1 + n2)
  | E_AMinus (a1 a2 : AExp'') (n1 n2 : Nat) :
      AEvalR'' a1 n1 → AEvalR'' a2 n2 → AEvalR'' (AMinus a1 a2) (n1 - n2)
  | E_AMult (a1 a2 : AExp'') (n1 n2 : Nat) :
      AEvalR'' a1 n1 → AEvalR'' a2 n2 → AEvalR'' (AMult a1 a2) (n1 * n2)

-- AAny can evaluate to any natural number - nondeterministic

end AEvalR_Extended

-- ------------------ EXPRESSIONS WITH VARIABLES -----------------------

-- State maps variable names (strings) to values (nats)
def State := TotalMap Nat

-- Redefine AExp with variables
inductive AExp' : Type where
  | ANum (n : Nat)
  | AId (x : String)       -- NEW: variable lookup
  | APlus (a1 a2 : AExp')
  | AMinus (a1 a2 : AExp')
  | AMult (a1 a2 : AExp')

-- Common variable names
def W : String := "W"
def X : String := "X"
def Y : String := "Y"
def Z : String := "Z"

-- Redefine BExp (same structure, but uses new AExp)
inductive BExp' : Type where
  | BTrue
  | BFalse
  | BEq (a1 a2 : AExp')
  | BNeq (a1 a2 : AExp')
  | BLe (a1 a2 : AExp')
  | BGt (a1 a2 : AExp')
  | BNot (b : BExp')
  | BAnd (b1 b2 : BExp')

open AExp' BExp'

-- Coq uses custom notation <{ 3 + (X * 2) }>
-- We use explicit constructors: APlus (ANum 3) (AMult (AId X) (ANum 2))

def example_aexp : AExp' := APlus (ANum 3) (APlus (AId X) (ANum 2))
def example_bexp : BExp' := BAnd BTrue (BNot (BLe (AId X) (ANum 4)))

-- ------------------ EVALUATION WITH STATE -----------------------

-- aeval now takes a state to look up variables
def aeval' (st : State) (a : AExp') : Nat :=
  match a with
  | AExp'.ANum n => n
  | AExp'.AId x => st x                           -- look up variable in state
  | AExp'.APlus a1 a2 => aeval' st a1 + aeval' st a2
  | AExp'.AMinus a1 a2 => aeval' st a1 - aeval' st a2
  | AExp'.AMult a1 a2 => aeval' st a1 * aeval' st a2

-- beval now takes a state
def beval' (st : State) (b : BExp') : Bool :=
  match b with
  | BExp'.BTrue => true
  | BExp'.BFalse => false
  | BExp'.BEq a1 a2 => aeval' st a1 == aeval' st a2
  | BExp'.BNeq a1 a2 => !(aeval' st a1 == aeval' st a2)
  | BExp'.BLe a1 a2 => decide (aeval' st a1 ≤ aeval' st a2)
  | BExp'.BGt a1 a2 => !(decide (aeval' st a1 ≤ aeval' st a2))
  | BExp'.BNot b1 => !beval' st b1
  | BExp'.BAnd b1 b2 => beval' st b1 && beval' st b2

-- Empty state: all variables map to 0
def empty_st : State := tEmpty 0

-- Notation for single binding: X !-> 5 means update empty_st with X -> 5
-- We use tUpdate directly
-- Coq: (X !-> 5) means (X !-> 5 ; empty_st)

-- Examples
-- aeval (X !-> 5) <{ 3 + (X * 2) }> = 13
example : aeval' (tUpdate empty_st X 5) (APlus (ANum 3) (AMult (AId X) (ANum 2))) = 13 := rfl

-- aeval (X !-> 5 ; Y !-> 4) <{ Z + (X * Y) }> = 20
-- Z is not bound, so Z -> 0
example : aeval' (tUpdate (tUpdate empty_st Y 4) X 5)
                (APlus (AId Z) (AMult (AId X) (AId Y))) = 20 := rfl

-- beval (X !-> 5) <{ true && ~(X <= 4) }> = true
example : beval' (tUpdate empty_st X 5)
                (BAnd BTrue (BNot (BLe (AId X) (ANum 4)))) = true := rfl

-- ------------------ COMMANDS -----------------------

inductive Com : Type where
  | CSkip
  | CAsgn (x : String) (a : AExp')
  | CSeq (c1 c2 : Com)
  | CIf (b : BExp') (c1 c2 : Com)
  | CWhile (b : BExp') (c : Com)

open Com

-- Coq uses custom notation <{ skip }>, <{ X := 3 }>, etc.
-- We use explicit constructors.

-- Factorial program:
--   Z := X;
--   Y := 1;
--   while Z <> 0 do
--     Y := Y * Z;
--     Z := Z - 1
--   end
def fact_in_lean : Com :=
  CSeq (CAsgn Z (AId X))
    (CSeq (CAsgn Y (ANum 1))
      (CWhile (BNeq (AId Z) (ANum 0))
        (CSeq (CAsgn Y (AMult (AId Y) (AId Z)))
              (CAsgn Z (AMinus (AId Z) (ANum 1))))))

-- ------------------ MORE EXAMPLES -----------------------

-- Assignment: X := X + 2
def plus2 : Com :=
  CAsgn X (APlus (AId X) (ANum 2))

-- Z := X * Y
def XtimesYinZ : Com :=
  CAsgn Z (AMult (AId X) (AId Y))

-- Loops

-- Z := Z - 1; X := X - 1
def subtract_slowly_body : Com :=
  CSeq (CAsgn Z (AMinus (AId Z) (ANum 1)))
       (CAsgn X (AMinus (AId X) (ANum 1)))

-- while X <> 0 do subtract_slowly_body end
def subtract_slowly : Com :=
  CWhile (BNeq (AId X) (ANum 0)) subtract_slowly_body

-- X := 3; Z := 5; subtract_slowly
def subtract_3_from_5_slowly : Com :=
  CSeq (CAsgn X (ANum 3))
    (CSeq (CAsgn Z (ANum 5))
          subtract_slowly)

-- Infinite loop: while true do skip end
def loop : Com :=
  CWhile BTrue CSkip


-- ------------------ EVALUATING COMMANDS -----------------------

-- Evaluation as a function (failed attempt)
-- While is bogus - just returns current state (can't define terminating function)
def ceval_fun_no_while (st : State) (c : Com) : State :=
  match c with
  | CSkip => st
  | CAsgn x a => tUpdate st x (aeval' st a)
  | CSeq c1 c2 =>
      let st' := ceval_fun_no_while st c1
      ceval_fun_no_while st' c2
  | CIf b c1 c2 =>
      if beval' st b
      then ceval_fun_no_while st c1
      else ceval_fun_no_while st c2
  | CWhile _ _ => st  -- bogus!

-- ------------------ EVALUATION AS A RELATION -----------------------

inductive CEval : Com → State → State → Prop where
  | E_Skip (st : State) :
      CEval CSkip st st
  | E_Asgn (st : State) (a : AExp') (n : Nat) (x : String) :
      aeval' st a = n →
      CEval (CAsgn x a) st (tUpdate st x n)
  | E_Seq (c1 c2 : Com) (st st' st'' : State) :
      CEval c1 st st' →
      CEval c2 st' st'' →
      CEval (CSeq c1 c2) st st''
  | E_IfTrue (st st' : State) (b : BExp') (c1 c2 : Com) :
      beval' st b = true →
      CEval c1 st st' →
      CEval (CIf b c1 c2) st st'
  | E_IfFalse (st st' : State) (b : BExp') (c1 c2 : Com) :
      beval' st b = false →
      CEval c2 st st' →
      CEval (CIf b c1 c2) st st'
  | E_WhileFalse (b : BExp') (st : State) (c : Com) :
      beval' st b = false →
      CEval (CWhile b c) st st
  | E_WhileTrue (st st' st'' : State) (b : BExp') (c : Com) :
      beval' st b = true →
      CEval c st st' →
      CEval (CWhile b c) st' st'' →
      CEval (CWhile b c) st st''

-- Notation: st =[ c ]=> st'
notation:40 st " =[ " c " ]=> " st' => CEval c st st'

-- ------------------ EXAMPLES -----------------------

-- Example 1:
--   empty_st =[ X := 2; if (X <= 1) then Y := 3 else Z := 4 end ]=> (Z !-> 4 ; X !-> 2)
example : empty_st =[
    CSeq (CAsgn X (ANum 2))
         (CIf (BLe (AId X) (ANum 1)) (CAsgn Y (ANum 3)) (CAsgn Z (ANum 4)))
  ]=> tUpdate (tUpdate empty_st X 2) Z 4 := by
  apply CEval.E_Seq (st' := tUpdate empty_st X 2)
  · -- X := 2
    apply CEval.E_Asgn; rfl
  · -- if (X <= 1) then Y := 3 else Z := 4 end
    apply CEval.E_IfFalse
    · -- beval' (X !-> 2) (X <= 1) = false (since 2 <= 1 is false)
      native_decide
    · -- Z := 4
      apply CEval.E_Asgn; rfl

-- Example 2:
--   empty_st =[ X := 0; Y := 1; Z := 2 ]=> (Z !-> 2 ; Y !-> 1 ; X !-> 0)
example : empty_st =[
    CSeq (CAsgn X (ANum 0))
         (CSeq (CAsgn Y (ANum 1))
               (CAsgn Z (ANum 2)))
  ]=> tUpdate (tUpdate (tUpdate empty_st X 0) Y 1) Z 2 := by
  apply CEval.E_Seq (st' := tUpdate empty_st X 0)
  · apply CEval.E_Asgn; rfl
  · apply CEval.E_Seq (st' := tUpdate (tUpdate empty_st X 0) Y 1)
    · apply CEval.E_Asgn; rfl
    · apply CEval.E_Asgn; rfl

-- ------------------ MORE EXAMPLES -----------------------

-- Sum from 1 to X, store in Y
-- Y := 0; while X > 0 do Y := Y + X; X := X - 1 end
def pup_to_n : Com :=
  CSeq (CAsgn Y (ANum 0))
       (CWhile (BGt (AId X) (ANum 0))
               (CSeq (CAsgn Y (APlus (AId Y) (AId X)))
                     (CAsgn X (AMinus (AId X) (ANum 1)))))

theorem pup_to_2_ceval :
    (tUpdate empty_st X 2) =[
      pup_to_n
    ]=> (tUpdate (tUpdate (tUpdate (tUpdate (tUpdate (tUpdate empty_st X 2) Y 0) Y 2) X 1) Y 3) X 0) := by
  unfold pup_to_n
  apply CEval.E_Seq (st' := tUpdate (tUpdate empty_st X 2) Y 0)
  · apply CEval.E_Asgn; rfl
  · apply CEval.E_WhileTrue (st' := tUpdate (tUpdate (tUpdate (tUpdate empty_st X 2) Y 0) Y 2) X 1)
    · native_decide
    · apply CEval.E_Seq (st' := tUpdate (tUpdate (tUpdate empty_st X 2) Y 0) Y 2)
      · apply CEval.E_Asgn; rfl
      · apply CEval.E_Asgn; rfl
    · apply CEval.E_WhileTrue (st' := tUpdate (tUpdate (tUpdate (tUpdate (tUpdate (tUpdate empty_st X 2) Y 0) Y 2) X 1) Y 3) X 0)
      · native_decide
      · apply CEval.E_Seq (st' := tUpdate (tUpdate (tUpdate (tUpdate (tUpdate empty_st X 2) Y 0) Y 2) X 1) Y 3)
        · apply CEval.E_Asgn; rfl
        · apply CEval.E_Asgn; rfl
      · apply CEval.E_WhileFalse
        native_decide

-- ------------------- DETERMINISM OF EVALUATION -------------------

theorem ceval_deterministic : ∀ c (st st1 st2 : State),
    CEval c st st1 →
    CEval c st st2 →
    st1 = st2 := by
  intro c st st1 st2 E1 E2
  induction E1 generalizing st2 with
  | E_Skip st =>
    cases E2
    rfl
  | E_Asgn st a n x Ha =>
    cases E2 with
    | E_Asgn _ _ n' _ Ha' =>
      simp [Ha] at Ha'
      subst Ha'
      rfl
  | E_Seq c1 c2 st st' st'' _ _ ih1 ih2 =>
    cases E2 with
    | E_Seq _ _ _ st'0 _ H1 H2 =>
      have : st' = st'0 := ih1 st'0 H1
      subst this
      exact ih2 st2 H2
  | E_IfTrue st st' b c1 c2 Hb _ ih =>
    cases E2 with
    | E_IfTrue _ _ _ _ _ _ H => exact ih st2 H
    | E_IfFalse _ _ _ _ _ Hb' _ => simp [Hb] at Hb'
  | E_IfFalse st st' b c1 c2 Hb _ ih =>
    cases E2 with
    | E_IfTrue _ _ _ _ _ Hb' _ => simp [Hb] at Hb'
    | E_IfFalse _ _ _ _ _ _ H => exact ih st2 H
  | E_WhileFalse b st c Hb =>
    cases E2 with
    | E_WhileFalse _ _ _ _ => rfl
    | E_WhileTrue _ _ _ _ _ Hb' _ _ => simp [Hb] at Hb'
  | E_WhileTrue st st' st'' b c Hb _ _ ih1 ih2 =>
    cases E2 with
    | E_WhileFalse _ _ _ Hb' => simp [Hb] at Hb'
    | E_WhileTrue _ st'0 _ _ _ _ H1 H2 =>
      have : st' = st'0 := ih1 st'0 H1
      subst this
      exact ih2 st2 H2

-- ------------------- REASONING ABOUT IMP PROGRAMS -------------------

theorem plus2_spec : ∀ (st : State) n (st' : State),
    st X = n →
    CEval plus2 st st' →
    st' X = n + 2 := by
  intro st n st' HX Heval
  cases Heval with
  | E_Asgn _ _ _ _ Ha =>
    simp [tUpdate_eq]
    simp [aeval', HX] at Ha
    omega

theorem XtimesYinZ_spec : ∀ (st : State) m n (st' : State),
    st X = m →
    st Y = n →
    CEval XtimesYinZ st st' →
    st' Z = m * n := by
  intro st m n st' HX HY Heval
  cases Heval with
  | E_Asgn _ _ _ _ Ha =>
    simp [tUpdate_eq]
    simp [aeval', HX, HY] at Ha
    omega

-- ------------------- LOOP NEVER STOPS -------------------

theorem loop_never_stops : ∀ (st st' : State),
    ¬(CEval loop st st') := by
  intro st st' contra
  unfold loop at contra
  generalize Hloop : Com.CWhile BExp'.BTrue Com.CSkip = loopdef at contra
  induction contra with
  | E_Skip => injection Hloop
  | E_Asgn => injection Hloop
  | E_Seq => injection Hloop
  | E_IfTrue => injection Hloop
  | E_IfFalse => injection Hloop
  | E_WhileFalse b st c Hb =>
    injection Hloop with Hb' Hc'
    subst Hb' Hc'
    simp [beval'] at Hb
  | E_WhileTrue st st' st'' b c Hb _ _ _ ih2 =>
    injection Hloop with Hb' Hc'
    subst Hb' Hc'
    exact ih2 rfl

-- ------------------- NO WHILES -------------------

def no_whiles (c : Com) : Bool :=
  match c with
  | .CSkip => true
  | .CAsgn _ _ => true
  | .CSeq c1 c2 => no_whiles c1 && no_whiles c2
  | .CIf _ c1 c2 => no_whiles c1 && no_whiles c2
  | .CWhile _ _ => false

inductive NoWhilesR : Com → Prop where
  | Skip : NoWhilesR .CSkip
  | Asgn (x : String) (a : AExp') : NoWhilesR (.CAsgn x a)
  | Seq (c1 c2 : Com) : NoWhilesR c1 → NoWhilesR c2 → NoWhilesR (.CSeq c1 c2)
  | If (b : BExp') (c1 c2 : Com) : NoWhilesR c1 → NoWhilesR c2 → NoWhilesR (.CIf b c1 c2)

theorem no_whiles_eqv : ∀ c, no_whiles c = true ↔ NoWhilesR c := by
  intro c
  constructor
  · intro H
    induction c with
    | CSkip => exact NoWhilesR.Skip
    | CAsgn x a => exact NoWhilesR.Asgn x a
    | CSeq c1 c2 ih1 ih2 =>
      simp [no_whiles] at H
      exact NoWhilesR.Seq c1 c2 (ih1 H.1) (ih2 H.2)
    | CIf b c1 c2 ih1 ih2 =>
      simp [no_whiles] at H
      exact NoWhilesR.If b c1 c2 (ih1 H.1) (ih2 H.2)
    | CWhile _ _ => simp [no_whiles] at H
  · intro H
    induction H with
    | Skip => rfl
    | Asgn _ _ => rfl
    | Seq _ _ _ _ ih1 ih2 => simp [no_whiles, ih1, ih2]
    | If _ _ _ _ _ ih1 ih2 => simp [no_whiles, ih1, ih2]

theorem no_whiles_terminating : ∀ c, NoWhilesR c → ∀ (st : State), ∃ st', CEval c st st' := by
  intro c H
  induction H with
  | Skip =>
    intro st
    exact ⟨st, CEval.E_Skip st⟩
  | Asgn x a =>
    intro st
    exact ⟨tUpdate st x (aeval' st a), CEval.E_Asgn st a (aeval' st a) x rfl⟩
  | Seq c1 c2 _ _ ih1 ih2 =>
    intro st
    have ⟨st1, H1⟩ := ih1 st
    have ⟨st2, H2⟩ := ih2 st1
    exact ⟨st2, CEval.E_Seq c1 c2 st st1 st2 H1 H2⟩
  | If b c1 c2 _ _ ih1 ih2 =>
    intro st
    have ⟨st1, H1⟩ := ih1 st
    have ⟨st2, H2⟩ := ih2 st
    cases Hb : beval' st b with
    | true => exact ⟨st1, CEval.E_IfTrue st st1 b c1 c2 Hb H1⟩
    | false => exact ⟨st2, CEval.E_IfFalse st st2 b c1 c2 Hb H2⟩



-- ------------------------ ADDITIONAL EXERCISES --------------------------------

-- ------------------- STACK COMPILER -------------------

inductive SInstr : Type where
  | SPush (n : Nat)
  | SLoad (x : String)
  | SPlus
  | SMinus
  | SMult
  deriving Repr

open SInstr

def s_execute (st : State) (stack : List Nat) (prog : List SInstr) : List Nat :=
  match prog with
  | [] => stack
  | SPush n :: prog' => s_execute st (n :: stack) prog'
  | SLoad x :: prog' => s_execute st (st x :: stack) prog'
  | SPlus :: prog' =>
      match stack with
      | n2 :: n1 :: stack' => s_execute st ((n1 + n2) :: stack') prog'
      | _ => s_execute st stack prog'
  | SMinus :: prog' =>
      match stack with
      | n2 :: n1 :: stack' => s_execute st ((n1 - n2) :: stack') prog'
      | _ => s_execute st stack prog'
  | SMult :: prog' =>
      match stack with
      | n2 :: n1 :: stack' => s_execute st ((n1 * n2) :: stack') prog'
      | _ => s_execute st stack prog'

example : s_execute empty_st [] [SPush 5, SPush 3, SPush 1, SMinus] = [2, 5] := rfl

example : s_execute (tUpdate empty_st X 3) [3, 4] [SPush 4, SLoad X, SMult, SPlus] = [15, 4] := rfl

def s_compile (e : AExp') : List SInstr :=
  match e with
  | .ANum n => [SPush n]
  | .AId x => [SLoad x]
  | .APlus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SPlus]
  | .AMinus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMinus]
  | .AMult a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMult]

-- s_compile <{ X - (2*Y) }> = [SLoad X, SPush 2, SLoad Y, SMult, SMinus]
example : s_compile (AExp'.AMinus (AExp'.AId X) (AExp'.AMult (AExp'.ANum 2) (AExp'.AId Y)))
        = [SLoad X, SPush 2, SLoad Y, SMult, SMinus] := rfl

-- ------------------- STACK COMPILER CORRECTNESS -------------------

theorem execute_app : ∀ (st : State) p1 p2 stack,
    s_execute st stack (p1 ++ p2) = s_execute st (s_execute st stack p1) p2 := by
  intro st p1 p2
  induction p1 with
  | nil => simp [s_execute]
  | cons s p1' ih =>
    intro stack
    cases s with
    | SPush n => simp [s_execute]; exact ih (n :: stack)
    | SLoad x => simp [s_execute]; exact ih (st x :: stack)
    | SPlus =>
      simp [s_execute]
      cases stack with
      | nil => exact ih []
      | cons n2 stack' =>
        cases stack' with
        | nil => exact ih [n2]
        | cons n1 stack'' => exact ih ((n1 + n2) :: stack'')
    | SMinus =>
      simp [s_execute]
      cases stack with
      | nil => exact ih []
      | cons n2 stack' =>
        cases stack' with
        | nil => exact ih [n2]
        | cons n1 stack'' => exact ih ((n1 - n2) :: stack'')
    | SMult =>
      simp [s_execute]
      cases stack with
      | nil => exact ih []
      | cons n2 stack' =>
        cases stack' with
        | nil => exact ih [n2]
        | cons n1 stack'' => exact ih ((n1 * n2) :: stack'')

theorem s_compile_correct_aux : ∀ (st : State) e stack,
    s_execute st stack (s_compile e) = aeval' st e :: stack := by
  intro st e
  induction e with
  | ANum n => intro stack; rfl
  | AId x => intro stack; rfl
  | APlus a1 a2 ih1 ih2 =>
    intro stack
    simp [s_compile, aeval']
    rw [execute_app, execute_app, ih1, ih2]
    rfl
  | AMinus a1 a2 ih1 ih2 =>
    intro stack
    simp [s_compile, aeval']
    rw [execute_app, execute_app, ih1, ih2]
    rfl
  | AMult a1 a2 ih1 ih2 =>
    intro stack
    simp [s_compile, aeval']
    rw [execute_app, execute_app, ih1, ih2]
    rfl

theorem s_compile_correct : ∀ (st : State) (e : AExp'),
    s_execute st [] (s_compile e) = [aeval' st e] := by
  intro st e
  exact s_compile_correct_aux st e []

-- ------------------- SHORT CIRCUIT EVALUATION -------------------

def beval_short_circuit (st : State) (b : BExp') : Bool :=
  match b with
  | .BTrue => true
  | .BFalse => false
  | .BEq a1 a2 => aeval' st a1 == aeval' st a2
  | .BNeq a1 a2 => !(aeval' st a1 == aeval' st a2)
  | .BLe a1 a2 => decide (aeval' st a1 ≤ aeval' st a2)
  | .BGt a1 a2 => !(decide (aeval' st a1 ≤ aeval' st a2))
  | .BNot b1 => !beval_short_circuit st b1
  | .BAnd b1 b2 =>
      match beval_short_circuit st b1 with
      | false => false
      | true => beval_short_circuit st b2

theorem beval_short_circuit_eq : ∀ (st : State) (b : BExp'),
    beval_short_circuit st b = beval' st b := by
  intro st b
  induction b with
  | BTrue => rfl
  | BFalse => rfl
  | BEq _ _ => rfl
  | BNeq _ _ => rfl
  | BLe _ _ => rfl
  | BGt _ _ => rfl
  | BNot b ih => simp [beval_short_circuit, beval', ih]
  | BAnd b1 b2 ih1 ih2 =>
    simp [beval_short_circuit, beval']
    cases h : beval_short_circuit st b1 with
    | false => simp_all
    | true => simp_all

-- ------------------- BREAK IMP -------------------

namespace BreakImp

inductive Com : Type where
  | CSkip
  | CBreak
  | CAsgn (x : String) (a : AExp')
  | CSeq (c1 c2 : Com)
  | CIf (b : BExp') (c1 c2 : Com)
  | CWhile (b : BExp') (c : Com)

open Com

inductive Result : Type where
  | SContinue
  | SBreak
  deriving Repr, DecidableEq

open Result

inductive CEval : Com → State → Result → State → Prop where
  | E_Skip (st : State) :
      CEval CSkip st SContinue st
  | E_Break (st : State) :
      CEval CBreak st SBreak st
  | E_Asgn (st : State) (a : AExp') (n : Nat) (x : String) :
      aeval' st a = n →
      CEval (CAsgn x a) st SContinue (tUpdate st x n)
  | E_Seq1 (c1 c2 : Com) (st st' : State) :
      CEval c1 st SBreak st' →
      CEval (CSeq c1 c2) st SBreak st'
  | E_Seq2 (c1 c2 : Com) (st st' st'' : State) (s : Result) :
      CEval c1 st SContinue st' →
      CEval c2 st' s st'' →
      CEval (CSeq c1 c2) st s st''
  | E_IfTrue (st st' : State) (b : BExp') (c1 c2 : Com) (s : Result) :
      beval' st b = true →
      CEval c1 st s st' →
      CEval (CIf b c1 c2) st s st'
  | E_IfFalse (st st' : State) (b : BExp') (c1 c2 : Com) (s : Result) :
      beval' st b = false →
      CEval c2 st s st' →
      CEval (CIf b c1 c2) st s st'
  | E_WhileFalse (b : BExp') (st : State) (c : Com) :
      beval' st b = false →
      CEval (CWhile b c) st SContinue st
  | E_WhileTrue1 (st st' : State) (b : BExp') (c : Com) :
      beval' st b = true →
      CEval c st SBreak st' →
      CEval (CWhile b c) st SContinue st'
  | E_WhileTrue2 (st st' st'' : State) (b : BExp') (c : Com) :
      beval' st b = true →
      CEval c st SContinue st' →
      CEval (CWhile b c) st' SContinue st'' →
      CEval (CWhile b c) st SContinue st''

theorem break_ignore : ∀ c (st st' : State) s,
    CEval (CSeq CBreak c) st s st' →
    st = st' := by
  intro c st st' s H
  cases H with
  | E_Seq1 _ _ _ _ Hbreak =>
    cases Hbreak
    rfl
  | E_Seq2 _ _ _ _ _ _ Hcont _ =>
    cases Hcont

theorem while_continue : ∀ b c (st st' : State) s,
    CEval (CWhile b c) st s st' →
    s = SContinue := by
  intro b c st st' s H
  cases H <;> rfl

theorem while_stops_on_break : ∀ b c (st st' : State),
    beval' st b = true →
    CEval c st SBreak st' →
    CEval (CWhile b c) st SContinue st' := by
  intro b c st st' Hb Hc
  exact CEval.E_WhileTrue1 st st' b c Hb Hc

theorem seq_continue : ∀ c1 c2 (st st' st'' : State),
    CEval c1 st SContinue st' →
    CEval c2 st' SContinue st'' →
    CEval (CSeq c1 c2) st SContinue st'' := by
  intro c1 c2 st st' st'' H1 H2
  exact CEval.E_Seq2 c1 c2 st st' st'' SContinue H1 H2

theorem seq_stops_on_break : ∀ c1 c2 (st st' : State),
    CEval c1 st SBreak st' →
    CEval (CSeq c1 c2) st SBreak st' := by
  intro c1 c2 st st' H
  exact CEval.E_Seq1 c1 c2 st st' H

theorem while_break_true : ∀ b c (st st' : State),
    CEval (CWhile b c) st SContinue st' →
    beval' st' b = true →
    ∃ st'', CEval c st'' SBreak st' := by
  intro b c st st' H Hb'
  generalize Hs : SContinue = s at H
  generalize Hloop : CWhile b c = loopdef at H
  induction H with
  | E_Skip _ => injection Hloop
  | E_Break _ => injection Hloop
  | E_Asgn _ _ _ _ _ => injection Hloop
  | E_Seq1 _ _ _ _ _ => injection Hloop
  | E_Seq2 _ _ _ _ _ _ _ _ => injection Hloop
  | E_IfTrue _ _ _ _ _ _ _ _ => injection Hloop
  | E_IfFalse _ _ _ _ _ _ _ _ => injection Hloop
  | E_WhileFalse b' st'' c' Hb =>
    injection Hloop with Hbeq Hceq
    subst Hbeq Hceq
    simp [Hb] at Hb'
  | E_WhileTrue1 st1 st1' b' c' Hb Hc =>
    injection Hloop with Hbeq Hceq
    subst Hbeq Hceq
    exact ⟨st1, Hc⟩
  | E_WhileTrue2 st1 st1' st1'' b' c' Hb _ _ _ ih2 =>
    injection Hloop with Hbeq Hceq
    subst Hbeq Hceq
    exact ih2 Hb' rfl rfl

theorem ceval_deterministic : ∀ (c : Com) (st st1 st2 : State) (s1 s2 : Result),
    CEval c st s1 st1 →
    CEval c st s2 st2 →
    st1 = st2 ∧ s1 = s2 := by
  intro c st st1 st2 s1 s2 E1 E2
  induction E1 generalizing st2 s2 with
  | E_Skip st =>
    cases E2
    exact ⟨rfl, rfl⟩
  | E_Break st =>
    cases E2
    exact ⟨rfl, rfl⟩
  | E_Asgn st a n x Ha =>
    cases E2 with
    | E_Asgn _ _ n' _ Ha' =>
      simp [Ha] at Ha'
      subst Ha'
      exact ⟨rfl, rfl⟩
  | E_Seq1 c1 c2 st st' H1 ih1 =>
    cases E2 with
    | E_Seq1 _ _ _ _ H1' =>
      have ⟨Heq, _⟩ := ih1 st2 SBreak H1'
      exact ⟨Heq, rfl⟩
    | E_Seq2 _ _ _ st'0 _ _ H1' _ =>
      have ⟨_, Hcontra⟩ := ih1 st'0 SContinue H1'
      contradiction
  | E_Seq2 c1 c2 st st' st'' s H1 H2 ih1 ih2 =>
    cases E2 with
    | E_Seq1 _ _ _ _ H1' =>
      have ⟨_, Hcontra⟩ := ih1 st2 SBreak H1'
      contradiction
    | E_Seq2 _ _ _ st'0 _ _ H1' H2' =>
      have ⟨Heq, _⟩ := ih1 st'0 SContinue H1'
      subst Heq
      exact ih2 st2 s2 H2'
  | E_IfTrue st st' b c1 c2 s Hb H ih =>
    cases E2 with
    | E_IfTrue _ _ _ _ _ _ _ H' => exact ih st2 s2 H'
    | E_IfFalse _ _ _ _ _ _ Hb' _ => simp [Hb] at Hb'
  | E_IfFalse st st' b c1 c2 s Hb H ih =>
    cases E2 with
    | E_IfTrue _ _ _ _ _ _ Hb' _ => simp [Hb] at Hb'
    | E_IfFalse _ _ _ _ _ _ _ H' => exact ih st2 s2 H'
  | E_WhileFalse b st c Hb =>
    cases E2 with
    | E_WhileFalse _ _ _ _ => exact ⟨rfl, rfl⟩
    | E_WhileTrue1 _ _ _ _ Hb' _ => simp [Hb] at Hb'
    | E_WhileTrue2 _ _ _ _ _ Hb' _ _ => simp [Hb] at Hb'
  | E_WhileTrue1 st st' b c Hb Hc ih =>
    cases E2 with
    | E_WhileFalse _ _ _ Hb' => simp [Hb] at Hb'
    | E_WhileTrue1 _ _ _ _ _ Hc' =>
      have ⟨Heq, _⟩ := ih st2 SBreak Hc'
      exact ⟨Heq, rfl⟩
    | E_WhileTrue2 _ st'0 _ _ _ _ Hc' _ =>
      have ⟨_, Hcontra⟩ := ih st'0 SContinue Hc'
      contradiction
  | E_WhileTrue2 st st' st'' b c Hb Hc Hw ih1 ih2 =>
    cases E2 with
    | E_WhileFalse _ _ _ Hb' => simp [Hb] at Hb'
    | E_WhileTrue1 _ _ _ _ _ Hc' =>
      have ⟨_, Hcontra⟩ := ih1 st2 SBreak Hc'
      contradiction
    | E_WhileTrue2 _ st'0 _ _ _ _ Hc' Hw' =>
      have ⟨Heq, _⟩ := ih1 st'0 SContinue Hc'
      subst Heq
      exact ih2 st2 SContinue Hw'

-- ------------------- FOR IMP -------------------

namespace ForImp

inductive Com : Type where
  | CSkip
  | CBreak
  | CAsgn (x : String) (a : AExp')
  | CSeq (c1 c2 : Com)
  | CIf (b : BExp') (c1 c2 : Com)
  | CWhile (b : BExp') (c : Com)
  | CFor (b : BExp') (pre post c : Com)  -- NEW

open Com

inductive Result : Type where
  | SContinue
  | SBreak
  deriving Repr, DecidableEq

open Result

inductive CEval : Com → State → Result → State → Prop where
  | E_Skip (st : State) :
      CEval CSkip st SContinue st
  | E_Break (st : State) :
      CEval CBreak st SBreak st
  | E_Asgn (st : State) (a : AExp') (n : Nat) (x : String) :
      aeval' st a = n →
      CEval (CAsgn x a) st SContinue (tUpdate st x n)
  | E_Seq1 (c1 c2 : Com) (st st' : State) :
      CEval c1 st SBreak st' →
      CEval (CSeq c1 c2) st SBreak st'
  | E_Seq2 (c1 c2 : Com) (st st' st'' : State) (s : Result) :
      CEval c1 st SContinue st' →
      CEval c2 st' s st'' →
      CEval (CSeq c1 c2) st s st''
  | E_IfTrue (st st' : State) (b : BExp') (c1 c2 : Com) (s : Result) :
      beval' st b = true →
      CEval c1 st s st' →
      CEval (CIf b c1 c2) st s st'
  | E_IfFalse (st st' : State) (b : BExp') (c1 c2 : Com) (s : Result) :
      beval' st b = false →
      CEval c2 st s st' →
      CEval (CIf b c1 c2) st s st'
  | E_WhileFalse (b : BExp') (st : State) (c : Com) :
      beval' st b = false →
      CEval (CWhile b c) st SContinue st
  | E_WhileTrue1 (st st' : State) (b : BExp') (c : Com) :
      beval' st b = true →
      CEval c st SBreak st' →
      CEval (CWhile b c) st SContinue st'
  | E_WhileTrue2 (st st' st'' : State) (b : BExp') (c : Com) :
      beval' st b = true →
      CEval c st SContinue st' →
      CEval (CWhile b c) st' SContinue st'' →
      CEval (CWhile b c) st SContinue st''
  | E_For (b : BExp') (st st' : State) (pre post c : Com) (s : Result) :
      CEval (CSeq pre (CWhile b (CSeq c post))) st s st' →
      CEval (CFor b pre post c) st s st'

theorem ceval_deterministic : ∀ (c : Com) (st st1 st2 : State) (s1 s2 : Result),
    CEval c st s1 st1 →
    CEval c st s2 st2 →
    st1 = st2 ∧ s1 = s2 := by
  intro c st st1 st2 s1 s2 E1 E2
  induction E1 generalizing st2 s2 with
  | E_Skip st =>
    cases E2
    exact ⟨rfl, rfl⟩
  | E_Break st =>
    cases E2
    exact ⟨rfl, rfl⟩
  | E_Asgn st a n x Ha =>
    cases E2 with
    | E_Asgn _ _ n' _ Ha' =>
      simp [Ha] at Ha'
      subst Ha'
      exact ⟨rfl, rfl⟩
  | E_Seq1 c1 c2 st st' H1 ih1 =>
    cases E2 with
    | E_Seq1 _ _ _ _ H1' =>
      have ⟨Heq, _⟩ := ih1 st2 SBreak H1'
      exact ⟨Heq, rfl⟩
    | E_Seq2 _ _ _ st'0 _ _ H1' _ =>
      have ⟨_, Hcontra⟩ := ih1 st'0 SContinue H1'
      contradiction
  | E_Seq2 c1 c2 st st' st'' s H1 H2 ih1 ih2 =>
    cases E2 with
    | E_Seq1 _ _ _ _ H1' =>
      have ⟨_, Hcontra⟩ := ih1 st2 SBreak H1'
      contradiction
    | E_Seq2 _ _ _ st'0 _ _ H1' H2' =>
      have ⟨Heq, _⟩ := ih1 st'0 SContinue H1'
      subst Heq
      exact ih2 st2 s2 H2'
  | E_IfTrue st st' b c1 c2 s Hb H ih =>
    cases E2 with
    | E_IfTrue _ _ _ _ _ _ _ H' => exact ih st2 s2 H'
    | E_IfFalse _ _ _ _ _ _ Hb' _ => simp [Hb] at Hb'
  | E_IfFalse st st' b c1 c2 s Hb H ih =>
    cases E2 with
    | E_IfTrue _ _ _ _ _ _ Hb' _ => simp [Hb] at Hb'
    | E_IfFalse _ _ _ _ _ _ _ H' => exact ih st2 s2 H'
  | E_WhileFalse b st c Hb =>
    cases E2 with
    | E_WhileFalse _ _ _ _ => exact ⟨rfl, rfl⟩
    | E_WhileTrue1 _ _ _ _ Hb' _ => simp [Hb] at Hb'
    | E_WhileTrue2 _ _ _ _ _ Hb' _ _ => simp [Hb] at Hb'
  | E_WhileTrue1 st st' b c Hb Hc ih =>
    cases E2 with
    | E_WhileFalse _ _ _ Hb' => simp [Hb] at Hb'
    | E_WhileTrue1 _ _ _ _ _ Hc' =>
      have ⟨Heq, _⟩ := ih st2 SBreak Hc'
      exact ⟨Heq, rfl⟩
    | E_WhileTrue2 _ st'0 _ _ _ _ Hc' _ =>
      have ⟨_, Hcontra⟩ := ih st'0 SContinue Hc'
      contradiction
  | E_WhileTrue2 st st' st'' b c Hb Hc Hw ih1 ih2 =>
    cases E2 with
    | E_WhileFalse _ _ _ Hb' => simp [Hb] at Hb'
    | E_WhileTrue1 _ _ _ _ _ Hc' =>
      have ⟨_, Hcontra⟩ := ih1 st2 SBreak Hc'
      contradiction
    | E_WhileTrue2 _ st'0 _ _ _ _ Hc' Hw' =>
      have ⟨Heq, _⟩ := ih1 st'0 SContinue Hc'
      subst Heq
      exact ih2 st2 SContinue Hw'
  | E_For b st st' pre post c s H ih =>
    cases E2 with
    | E_For _ _ _ _ _ _ _ H' =>
      exact ih st2 s2 H'

end ForImp