/-
Inspired by https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification/topic/.E2.9C.94.20Small-step.20operational.20semantics
-/
import Batteries.Tactic.Basic
-- import Batteries.Tactic.RCases
import Batteries.CodeAction

inductive Tm where
| C : Nat → Tm
| P : Tm → Tm → Tm

namespace Tm

def evalF: Tm → Nat
| C n => n
| P l r => l.evalF + r.evalF

set_option hygiene false in
infixl:25 " ==> " => eval

inductive eval : Tm → Nat → Prop where
| EConst : ∀ n, C n ==> n
| EPlus : ∀ t₁ t₂ n₁ n₂,
    t₁ ==> n₁ →
    t₂ ==> n₂ →
    P t₁ t₂ ==> n₁ + n₂

-- Repeating this helps delaboration
infixl:25 " ==> " => eval

set_option hygiene false in
infixl:25 " ~~> " => step

inductive step : Tm → Tm → Prop where
| StPlusConstConst :
    P (C n₁) (C n₂) ~~> C (n₁ + n₂)
| StPlusLeft (t₁ t₁' t₂ : Tm):
    t₁ ~~> t₁' →
    P t₁ t₂ ~~> P t₁' t₂
| StPlusRight (t₂ t₂' : Tm):
    t₂ ~~> t₂' →
    P (C n) t₂ ~~> P (C n) t₂'

-- Repeating this helps delaboration
infixl:25 " ~~> " => step

end Tm

def Relation (α: Type) := α → α → Prop

def Relation.deterministic (R: Relation α) : Prop :=
  ∀ {x y₁ y₂: α}, R x y₁ → R x y₂ → y₁ = y₂

theorem EvalSmallStep.deterministic : Relation.deterministic Tm.step := by
Goals accomplished! 🐙
  unfold 
Relation.deterministic: {α : Type} → Relation α → Prop
Relation.deterministic
∀ {x y₁ y₂ : Tm}, x ~~> y₁ → x ~~> y₂ → y₁ = y₂
  intro 
x: Tm
x 
y₁: Tm
y₁ 
y₂: Tm
y₂ 
hy₁: x ~~> y₁
hy₁ 
hy₂: x ~~> y₂
hy₂
x, y₁, y₂: Tm
hy₁: x ~~> y₁
hy₂: x ~~> y₂
y₁ = y₂
  induction 
hy₁: x ~~> y₁
hy₁ generalizing 
y₂: Tm
y₂
x, y₁: Tm
n₁✝, n₂✝: Nat
y₂: Tm
hy₂: (Tm.C n₁✝).P (Tm.C n₂✝) ~~> y₂
StPlusConstConst
Tm.C (n₁✝ + n₂✝) = y₂
x, y₁, t₁✝, t₁'✝, t₂✝: Tm
a✝: t₁✝ ~~> t₁'✝
a_ih✝: ∀ {y₂ : Tm}, t₁✝ ~~> y₂ → t₁'✝ = y₂
y₂: Tm
hy₂: t₁✝.P t₂✝ ~~> y₂
StPlusLeft
t₁'✝.P t₂✝ = y₂
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
y₂: Tm
hy₂: (Tm.C n✝).P t₂✝ ~~> y₂
StPlusRight
(Tm.C n✝).P t₂'✝ = y₂ <;>
x, y₁: Tm
n₁✝, n₂✝: Nat
y₂: Tm
hy₂: (Tm.C n₁✝).P (Tm.C n₂✝) ~~> y₂
StPlusConstConst
Tm.C (n₁✝ + n₂✝) = y₂
x, y₁, t₁✝, t₁'✝, t₂✝: Tm
a✝: t₁✝ ~~> t₁'✝
a_ih✝: ∀ {y₂ : Tm}, t₁✝ ~~> y₂ → t₁'✝ = y₂
y₂: Tm
hy₂: t₁✝.P t₂✝ ~~> y₂
StPlusLeft
t₁'✝.P t₂✝ = y₂
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
y₂: Tm
hy₂: (Tm.C n✝).P t₂✝ ~~> y₂
StPlusRight
(Tm.C n✝).P t₂'✝ = y₂ first
  |
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
y₂: Tm
hy₂: (Tm.C n✝).P t₂✝ ~~> y₂
StPlusRight
(Tm.C n✝).P t₂'✝ = y₂ cases 
hy₂: (Tm.C n₁✝).P (Tm.C n₂✝) ~~> y₂
hy₂
x, y₁: Tm
n✝: Nat
t₂'✝: Tm
n₂✝: Nat
a✝: Tm.C n₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, Tm.C n₂✝ ~~> y₂ → t₂'✝ = y₂
StPlusRight.StPlusConstConst
(Tm.C n✝).P t₂'✝ = Tm.C (n✝ + n₂✝)
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
a✝¹: t₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
t₁'✝: Tm
a✝: Tm.C n✝ ~~> t₁'✝
StPlusRight.StPlusLeft
(Tm.C n✝).P t₂'✝ = t₁'✝.P t₂✝
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
a✝¹: t₂✝ ~~> t₂'✝¹
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ <;>
x, y₁: Tm
n✝: Nat
t₂'✝: Tm
n₂✝: Nat
a✝: Tm.C n₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, Tm.C n₂✝ ~~> y₂ → t₂'✝ = y₂
StPlusRight.StPlusConstConst
(Tm.C n✝).P t₂'✝ = Tm.C (n✝ + n₂✝)
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
a✝¹: t₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
t₁'✝: Tm
a✝: Tm.C n✝ ~~> t₁'✝
StPlusRight.StPlusLeft
(Tm.C n✝).P t₂'✝ = t₁'✝.P t₂✝
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
a✝¹: t₂✝ ~~> t₂'✝¹
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ rename_i 
h: Tm.C n✝ ~~> t₁'✝
h
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
a✝: t₂✝ ~~> t₂'✝¹
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
h: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ <;>
x, y₁: Tm
n₁✝, h: Nat
StPlusConstConst.StPlusConstConst
Tm.C (n₁✝ + h) = Tm.C (n₁✝ + h)
x, y₁: Tm
n₁✝, n₂✝: Nat
t₁'✝: Tm
h: Tm.C n₁✝ ~~> t₁'✝
StPlusConstConst.StPlusLeft
Tm.C (n₁✝ + n₂✝) = t₁'✝.P (Tm.C n₂✝)
x, y₁: Tm
n₁✝, n₂✝: Nat
t₂'✝: Tm
h: Tm.C n₂✝ ~~> t₂'✝
StPlusConstConst.StPlusRight
Tm.C (n₁✝ + n₂✝) = (Tm.C n₁✝).P t₂'✝ first |
x, y₁, t₁'✝: Tm
n₁✝, n₂✝: Nat
a✝: Tm.C n₁✝ ~~> t₁'✝
h: ∀ {y₂ : Tm}, Tm.C n₁✝ ~~> y₂ → t₁'✝ = y₂
StPlusLeft.StPlusConstConst
t₁'✝.P (Tm.C n₂✝) = Tm.C (n₁✝ + n₂✝) rfl
x, y₁: Tm
n₁✝, n₂✝: Nat
t₂'✝: Tm
h: Tm.C n₂✝ ~~> t₂'✝
StPlusConstConst.StPlusRight
Tm.C (n₁✝ + n₂✝) = (Tm.C n₁✝).P t₂'✝ |
x, y₁, t₁'✝: Tm
n₁✝, n₂✝: Nat
a✝: Tm.C n₁✝ ~~> t₁'✝
h: ∀ {y₂ : Tm}, Tm.C n₁✝ ~~> y₂ → t₁'✝ = y₂
StPlusLeft.StPlusConstConst
t₁'✝.P (Tm.C n₂✝) = Tm.C (n₁✝ + n₂✝) cases 
h: ∀ {y₂ : Tm}, Tm.C n₁✝ ~~> y₂ → t₁'✝ = y₂
h
x, y₁, t₁'✝: Tm
n₁✝, n₂✝: Nat
a✝: Tm.C n₁✝ ~~> t₁'✝
h: ∀ {y₂ : Tm}, Tm.C n₁✝ ~~> y₂ → t₁'✝ = y₂
x✝: Tm.C n₁✝ ~~> ?m.6631 → t₁'✝ = ?m.6631
StPlusLeft.StPlusConstConst
t₁'✝.P (Tm.C n₂✝) = Tm.C (n₁✝ + n₂✝)
  |
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
a_ih✝: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
y₂: Tm
hy₂: (Tm.C n✝).P t₂✝ ~~> y₂
StPlusRight
(Tm.C n✝).P t₂'✝ = y₂ rename_i 
h: t₁✝ ~~> t₁'✝
h 
hP: ∀ {y₂ : Tm}, t₁✝ ~~> y₂ → t₁'✝ = y₂
hP
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
h: t₂✝ ~~> t₂'✝
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
y₂: Tm
hy₂: (Tm.C n✝).P t₂✝ ~~> y₂
StPlusRight
(Tm.C n✝).P t₂'✝ = y₂; cases 
hy₂: t₁✝.P t₂✝ ~~> y₂
hy₂
x, y₁: Tm
n✝: Nat
t₂'✝: Tm
n₂✝: Nat
h: Tm.C n₂✝ ~~> t₂'✝
hP: ∀ {y₂ : Tm}, Tm.C n₂✝ ~~> y₂ → t₂'✝ = y₂
StPlusRight.StPlusConstConst
(Tm.C n✝).P t₂'✝ = Tm.C (n✝ + n₂✝)
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
h: t₂✝ ~~> t₂'✝
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
t₁'✝: Tm
a✝: Tm.C n✝ ~~> t₁'✝
StPlusRight.StPlusLeft
(Tm.C n✝).P t₂'✝ = t₁'✝.P t₂✝
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ <;>
x, y₁: Tm
n✝: Nat
t₂'✝: Tm
n₂✝: Nat
h: Tm.C n₂✝ ~~> t₂'✝
hP: ∀ {y₂ : Tm}, Tm.C n₂✝ ~~> y₂ → t₂'✝ = y₂
StPlusRight.StPlusConstConst
(Tm.C n✝).P t₂'✝ = Tm.C (n✝ + n₂✝)
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝: Tm
h: t₂✝ ~~> t₂'✝
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝ = y₂
t₁'✝: Tm
a✝: Tm.C n✝ ~~> t₁'✝
StPlusRight.StPlusLeft
(Tm.C n✝).P t₂'✝ = t₁'✝.P t₂✝
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ first |
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ contradiction
Goals accomplished! 🐙 |
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ cases 
_: ?m.7523
_
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
x✝: ?m.9168
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ |
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝ (
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
a✝: t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝rename_i 
h': t₂✝ ~~> t₂'✝
h'
x, y₁, t₁✝, t₁'✝¹, t₂✝: Tm
h: t₁✝ ~~> t₁'✝¹
hP: ∀ {y₂ : Tm}, t₁✝ ~~> y₂ → t₁'✝¹ = y₂
t₁'✝: Tm
h': t₁✝ ~~> t₁'✝
StPlusLeft.StPlusLeft
t₁'✝¹.P t₂✝ = t₁'✝.P t₂✝; rw [
x, y₁: Tm
n✝: Nat
t₂✝, t₂'✝¹: Tm
h: t₂✝ ~~> t₂'✝¹
hP: ∀ {y₂ : Tm}, t₂✝ ~~> y₂ → t₂'✝¹ = y₂
t₂'✝: Tm
h': t₂✝ ~~> t₂'✝
StPlusRight.StPlusRight
(Tm.C n✝).P t₂'✝¹ = (Tm.C n✝).P t₂'✝
hP: ∀ {y₂ : Tm}, t₁✝ ~~> y₂ → t₁'✝¹ = y₂
hP 
h': t₂✝ ~~> t₂'✝
h'
x, y₁, t₁✝, t₁'✝¹, t₂✝: Tm
h: t₁✝ ~~> t₁'✝¹
hP: ∀ {y₂ : Tm}, t₁✝ ~~> y₂ → t₁'✝¹ = y₂
t₁'✝: Tm
h': t₁✝ ~~> t₁'✝
StPlusLeft.StPlusLeft
t₁'✝.P t₂✝ = t₁'✝.P t₂✝]
Goals accomplished! 🐙)
Goals accomplished! 🐙
  -- induction hy₁ generalizing y₂ with
  -- | StPlusConstConst =>
  --   cases hy₂ <;> rename_i h₂ <;> first | rfl | cases h₂
  --   -- cases hy₂ with
  --   -- | StPlusConstConst => rfl
  --   -- | StPlusLeft =>
  --   --   rename_i hl
  --   --   cases hl
  --   -- | StPlusRight =>
  --   --   rename_i hr
  --   --   cases hr
  -- | StPlusLeft =>
  --   rename_i h hP
  --   cases hy₂ <;> first | contradiction | cases _ | (rename_i h'; rw [hP h'])
  --   -- rename_i hl hPl
  --   -- cases hy₂ with
  --   -- | StPlusConstConst => contradiction
  --   -- | StPlusLeft =>
  --   --   rename_i hl'
  --   --   rw [hPl hl']
  --   -- | StPlusRight => cases hl
  -- | StPlusRight =>
  --   rename_i h hP
  --   cases hy₂ <;> first | contradiction | cases _ | (rename_i h'; rw [hP h'])
  --   -- rename_i hr hPr
  --   -- cases hy₂ with
  --   -- | StPlusConstConst => contradiction
  --   -- | StPlusLeft =>
  --   --   rename_i hl'
  --   --   cases hl'
  --   -- | StPlusRight =>
  --   --   rename_i hr'
  --   --   rw [hPr hr']
  done
Goals accomplished! 🐙