operational semantics

Stream: general

[Joachim Breitner]

Larry Paulson has written a blog post showing that Isabelle is nice for formalizing PL semantics, with a concrete example. Would be interesting to see someone reproducing it in Lean and comparing the two:
https://lawrencecpaulson.github.io/2023/03/08/Fun_Semantics.html

[Joachim Breitner]

The agda people already responded: https://github.com/pigworker/Samizdat/blob/main/ExampleSemantics.agda

[Trebor Huang]

Would be nice to build on the Agda one and cut out all those repetitions with tactics

[Shreyas Srinivas]

The original blogpost is explicitly about breaking the myth that dependent types are "THE" way to do op-semantics.

[Shreyas Srinivas]

Because typically this is done in something like Coq

[Shreyas Srinivas]

So you have the entire software foundations series.

[Shreyas Srinivas]

full of examples of how do to this in Coq.

[Shreyas Srinivas]

I can't see why doing it in lean is going to tell us anything new

[Henrik Böving]

I dont think this is about telling something new, this is more about showing we can do it as well.

[Shreyas Srinivas]

Okay. I can give it a shot. It will be useful for me. But from what I recall reading here in Zulip, the creator of PLFA is creating a version in Lean. This might be a good demo for us.

[Joachim Breitner]

As Hendrik says. A little Rosetta stone of semantics in theorem provers.

[Sebastian Ullrich]

Should also lend itself nicely to Aesop one-liners

[Sebastian Ullrich]

Shreyas Srinivas said:

Because typically this is done in something like Coq

By the way, as Jon pointed out in the blog post comments, this is a curious statement as Coq formalizations usually are not heavy in dependent types

[Joachim Breitner]

Showing off aesop would be great! This week I chatted with the person behind the Isabelle and Coq formalization of WebAssembly, and he said he'd be quite curious about lean, but is under the impression that the automation is just not there yet, compared to Isabelle's.

[Shreyas Srinivas]

Sebastian Ullrich said:

Shreyas Srinivas said:

Because typically this is done in something like Coq

By the way, as Jon pointed out in the blog post comments, this is a curious statement as Coq formalizations usually are not heavy in dependent types

I am not an expert on this stuff, so I won't speculate on the technical reasons. But even if Isabelle could sledgehammer the proofs away, I think usability-wise lean takes the cake. The fact that it is and works like a programming language makes it ridiculously easy for me to reason about what's happening and what to modularise away, compared to Isabelle, which often feels like some ancient sorcery ritual (especially for program generation stuff). There are some verification related things I am doing in lean, that I first tried on TLA+ and Isabelle. Lean simply makes more intuitive sense for the goal I am trying to achieve.

[Shreyas Srinivas]

Having said that, I'll try a dependent types based approach

[Arthur Adjedj]

Coq has many libraries which helps with formalizing PL related stuff, like AutoSubst, which allows you to generate many weakening/substitution lemmas automatically. This may be one of the reasons why it is seen as the de facto proof-assistant to do this kind of work

[Joachim Breitner]

And also generic program logic libraries like Iris, which keeps coming up all the time right now when I look for work that proves things similar to the things that I'd like to prove (or at least like to have proven). But I wouldn't mind if lean catches up eventually :-)

[Shreyas Srinivas]

Could we write lean versions of these libraries?

[Joachim Breitner]

Sure! It's just lots of work

[Shreyas Srinivas]

Since coq and lean use the same underlying theories, is it possible/feasible/(worthwhile considering) interoperability between coq and lean's term languages?

[Mario Carneiro]

https://github.com/larsk21/iris-lean

[Mario Carneiro]

unfortunately it is not under active development anymore as it was a student project

[Shreyas Srinivas]

I looked for previous work on this topic. In the book titled "Hitchhiker's guide to logical verification" written by people in this zulip, Chapter 8 covers how to do operational semantics and chapter 10, denotational semantics

[Shreyas Srinivas]

In lean ofc

[Andrew Carter]

I have church-rosser for untyped lambda calculus (which isn't quite the original blog post - but maybe in the spirit of it):
https://github.com/calcu16/lean_complexity/blob/main/src/lambda_calculus/utlc/beta/church_rosser.lean
and
https://github.com/calcu16/lean_complexity/blob/main/src/lambda_calculus/utlc/beta_eta/church_rosser.lean
I'm happy to try to get that portion of the repo into mathlib if there is interest (I think it needs a lot of cleaning up).

[Kyle Miller]

@Joachim Breitner Here's a Lean 4 version without using any fancy tactics: (gist link)

import Mathlib.Tactic.SolveByElim
import Std.Tactic.RCases

namespace semantics

/-- A simple expression language. -/
inductive exp
  | T | F | Zero | Succ (x : exp) | IF (p x y : exp) | EQ (x y : exp)

open exp

/-- Small-step semantics for the simple expression language. -/
inductive Eval : exp → exp → Prop
  | IF_T : Eval (IF T x y) x
  | IF_F : Eval (IF F x y) y
  | IF_Eval : Eval p q → Eval (IF p x y) (IF q x y)
  | Succ_Eval : Eval x y → Eval (Succ x) (Succ y)
  | EQ_same : Eval (EQ x x) T
  | EQ_S0 : Eval (EQ (Succ x) Zero) F
  | EQ_0S : Eval (EQ Zero (Succ y)) F
  | EQ_SS : Eval (EQ (Succ x) (Succ y)) (EQ x y)
  | EQ_Eval1 : Eval x z → Eval (EQ x y) (EQ z y)
  | EQ_Eval2 : Eval y z → Eval (EQ x y) (EQ x z)

@[simp] theorem T_simp : ¬ Eval T z := by rintro (_|_)
@[simp] theorem F_simp : ¬ Eval F z := by rintro (_|_)
@[simp] theorem Zero_simp : ¬ Eval Zero z := by rintro (_|_)

inductive tp
  | tbool | tnum

open tp

inductive TP : exp → tp → Prop
  | T : TP T tbool
  | F : TP F tbool
  | Zero : TP Zero tnum
  | IF : TP p tbool → TP x t → TP y t → TP (IF p x y) t
  | Succ : TP x tnum → TP (Succ x) tnum
  | EQ : TP x t → TP y t → TP (EQ x y) tbool

/-- Type preservation: small-step evaluation preserves the type. -/
theorem type_preservation (he : Eval x y) (ht : TP x t) : TP y t := by
  induction he generalizing t
  <;> (try rename_i ih) <;> cases ht
  <;> (try assumption)
  <;> try (constructor <;> (try apply ih) <;> assumption)
  -- One last case. The strategy seems to be to do cases on every `TP a b` where
  -- `a` or `b` isn't a variable, which could be automated.
  rename_i h1 h2
  cases h1
  cases h2
  constructor <;> assumption

/-- Evaluator for expressions. -/
def evl : exp → Nat
  | T => 1
  | F => 0
  | exp.Zero => 0
  | Succ x => evl x + 1
  | IF x y z => if evl x = 1 then evl y else evl z
  | EQ x y => if evl x = evl y then 1 else 0

@[simp] theorem Nat.add_one_ne_zero (a : Nat) : a + 1 ≠ 0 := by
  simp [← Nat.succ_eq_add_one]

/-- Value preservation: the evaluator is constant modulo the small-step semantics. -/
theorem value_preservation (h : Eval x y) : evl x = evl y := by
  induction h <;> simp [evl, *, (Nat.add_one_ne_zero _).symm]

theorem lt_two_of_bool (ht : TP x tbool) : evl x < 2 := by
  generalize h : tbool = t at ht
  induction ht <;> simp [evl]
  <;> subst_vars <;> (try split) <;> simp at * <;> assumption

/-- Reflexive transitive closure of `Eval`. -/
inductive EvalStar : exp → exp → Prop
  | Id : EvalStar x x
  | Step : Eval x y → EvalStar y z → EvalStar x z

attribute [simp] EvalStar.Id

def Eval.Star (h : Eval x y) : EvalStar x y := EvalStar.Step h EvalStar.Id

@[simp] theorem exists_evalstar : ∃ y, EvalStar x y := ⟨x, EvalStar.Id⟩

@[simp] theorem eval_T : EvalStar T u ↔ u = T := by
  constructor
  · generalize hT : T = v
    intro h
    induction h <;> subst_vars <;> simp at *
  · rintro rfl; simp

@[simp] theorem eval_F : EvalStar F u ↔ u = F := by
  constructor
  · generalize hT : F = v
    intro h
    induction h <;> subst_vars <;> simp at *
  · rintro rfl; simp

@[simp] theorem eval_EQ_self : EvalStar (EQ x x) T := by
  apply Eval.Star
  constructor

@[simp] theorem eval_EQ_of_Eval (h : Eval x y) : EvalStar (EQ x y) T := by
  constructor
  apply Eval.EQ_Eval1; assumption
  apply Eval.Star
  constructor

@[simp] theorem eval_EQ_of_Eval2 (h : Eval y x) : EvalStar (EQ x y) T := by
  constructor
  apply Eval.EQ_Eval2; assumption
  apply Eval.Star
  constructor

theorem eval_not_EQ_of_succ_EQ (h : Eval (Succ x) y) : EvalStar (EQ y Zero) F := by
  cases h
  apply Eval.Star; constructor

theorem eval_not_EQ_of_succ_EQ2 (h : Eval (Succ x) y) : EvalStar (EQ Zero y) F := by
  cases h
  apply Eval.Star; constructor

/-- The obvious consequence of `type_preservation`. -/
theorem type_preservation_Star (h : EvalStar x y) (ht : TP x t) : TP y t := by
  induction h <;> solve_by_elim [type_preservation]

theorem EvalStar.Succ (h : EvalStar x y) : EvalStar (Succ x) (Succ y) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem EvalStar.IF (h : EvalStar p q) : EvalStar (IF p x y) (IF q x y) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem EvalStar.EQ1 (h : EvalStar x z) : EvalStar (EQ x y) (EQ z y) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem EvalStar.EQ2 (h : EvalStar y z) : EvalStar (EQ x y) (EQ x z) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem prediamond (f : exp → exp) (thm : {x y : exp} → EvalStar x y → EvalStar (f x) (f y))
    (h : ∃ u, EvalStar x u ∧ EvalStar y u) : ∃ u, EvalStar (f x) u ∧ EvalStar (f y) u := by
  obtain ⟨u, h, h'⟩ := h
  exact ⟨_, thm h, thm h'⟩

/-- Partial Church-Rosser property for big-step semantics. -/
theorem diamond (hy : Eval x y) (hz : Eval x z) : ∃ u, EvalStar y u ∧ EvalStar z u := by
  induction hy generalizing z <;> cases hz <;> simp [*] at *
  <;> try (solve_by_elim [eval_not_EQ_of_succ_EQ, eval_not_EQ_of_succ_EQ2])
  · apply prediamond _ EvalStar.IF; solve_by_elim
  · apply prediamond _ EvalStar.Succ; solve_by_elim
  · rename_i h
    cases h
    rename_i a b c e
    exact ⟨EQ c b, e.Star.EQ1, Eval.EQ_SS.Star⟩
  · rename_i h
    cases h
    rename_i a b c e
    exact ⟨EQ a c, e.Star.EQ2, Eval.EQ_SS.Star⟩
  · rename_i a b c h ih
    cases h
    rename_i y h
    exact ⟨EQ y c, Eval.EQ_SS.Star, h.Star.EQ1⟩
  · apply prediamond _ EvalStar.EQ1; solve_by_elim
  · rename_i a b c e' ih z e
    exact ⟨EQ b z, e.Star.EQ2, e'.Star.EQ1⟩
  · rename_i a b c h ih
    cases h
    rename_i y h
    exact ⟨EQ b y, Eval.EQ_SS.Star, h.Star.EQ2⟩
  · rename_i a b c h ih z h'
    exact ⟨EQ z b, h'.Star.EQ1, h.Star.EQ2⟩
  · rename_i a b c h ih z h'
    -- an interesting application of ih
    obtain ⟨v, g, g'⟩ := ih h'
    exact ⟨EQ c v, g.EQ2, g'.EQ2⟩

end semantics

[Arthur Paulino]

Kyle, did you just write all that? :open_mouth:

[Kyle Miller]

That's 181 lines (and could surely be done better) vs 115 for the Isabelle version.

[Trebor Huang]

Why is EQ T F stuck in the small step semantics? Or did I miss any rules?

[Mario Carneiro]

hm, that does seem like a bug in the formalization

[Mario Carneiro]

Here's a mostly-pointless golf of Kyle's proof (129 lines):

import Mathlib.Tactic.SolveByElim
import Std.Tactic.RCases

namespace semantics

/-- A simple expression language. -/
inductive exp | T | F | Zero | Succ (x : exp) | IF (p x y : exp) | EQ (x y : exp)

/-- Small-step semantics for the simple expression language. -/
inductive Eval : exp → exp → Prop
  | IF_T : Eval (.IF .T x y) x
  | IF_F : Eval (.IF .F x y) y
  | IF_Eval : Eval p q → Eval (.IF p x y) (.IF q x y)
  | Succ_Eval : Eval x y → Eval (.Succ x) (.Succ y)
  | EQ_same : Eval (.EQ x x) .T
  | EQ_S0 : Eval (.EQ (.Succ x) .Zero) .F
  | EQ_0S : Eval (.EQ .Zero (.Succ y)) .F
  | EQ_SS : Eval (.EQ (.Succ x) (.Succ y)) (.EQ x y)
  | EQ_Eval1 : Eval x z → Eval (.EQ x y) (.EQ z y)
  | EQ_Eval2 : Eval y z → Eval (.EQ x y) (.EQ x z)

@[simp] theorem T_simp : ¬ Eval .T z := fun.
@[simp] theorem F_simp : ¬ Eval .F z := fun.
@[simp] theorem Zero_simp : ¬ Eval .Zero z := fun.

inductive tp | bool | num

inductive TP : exp → tp → Prop
  | T : TP .T .bool
  | F : TP .F .bool
  | Zero : TP .Zero .num
  | IF : TP p .bool → TP x t → TP y t → TP (.IF p x y) t
  | Succ : TP x .num → TP (.Succ x) .num
  | EQ : TP x t → TP y t → TP (.EQ x y) .bool

/-- Type preservation: small-step evaluation preserves the type. -/
theorem type_preservation (he : Eval x y) (ht : TP x t) : TP y t := by
  induction he generalizing t <;> cases ht <;> (try assumption)
    <;> constructor <;> (try apply_assumption <;> assumption)
    <;> casesm* TP (.Succ _) _ <;> assumption

def evl : exp → Nat
  | .T => 1
  | .F => 0
  | .Zero => 0
  | .Succ x => evl x + 1
  | .IF x y z => if evl x = 1 then evl y else evl z
  | .EQ x y => if evl x = evl y then 1 else 0

/-- Value preservation: the evaluator is constant modulo the small-step semantics. -/
theorem value_preservation (h : Eval x y) : evl x = evl y := by
  induction h <;> simp [evl, *, (Nat.succ_ne_zero _).symm]

theorem lt_two_of_bool (ht : TP x .bool) : evl x < 2 := by
  generalize h : tp.bool = t at ht; induction ht <;> simp [evl]
    <;> subst_vars <;> (try split) <;> simp [*] at *

inductive EvalStar : exp → exp → Prop
  | id : EvalStar x x
  | step : Eval x y → EvalStar y z → EvalStar x z

attribute [simp] EvalStar.id

def Eval.star (h : Eval x y) : EvalStar x y := .step h .id

@[simp] theorem exists_evalstar : ∃ y, EvalStar x y := ⟨x, .id⟩

@[simp] theorem eval_T : EvalStar .T u ↔ u = .T := by
  constructor
  · generalize hT : exp.T = v
    intro h
    induction h <;> subst_vars <;> simp at *
  · rintro rfl; simp

@[simp] theorem eval_F : EvalStar .F u ↔ u = .F := by
  constructor
  · generalize hT : exp.F = v
    intro h
    induction h <;> subst_vars <;> simp at *
  · rintro rfl; simp

@[simp] theorem eval_EQ_self : EvalStar (.EQ x x) .T := Eval.EQ_same.star

@[simp] theorem eval_EQ_of_Eval (h : Eval x y) : EvalStar (.EQ x y) .T :=
  .step (.EQ_Eval1 h) Eval.EQ_same.star

@[simp] theorem eval_EQ_of_Eval2 (h : Eval y x) : EvalStar (.EQ x y) .T :=
  .step (.EQ_Eval2 h) Eval.EQ_same.star

theorem eval_not_EQ_of_succ_EQ (h : Eval (.Succ x) y) : EvalStar (.EQ y .Zero) .F := by
  cases h; exact Eval.EQ_S0.star

theorem eval_not_EQ_of_succ_EQ2 (h : Eval (.Succ x) y) : EvalStar (.EQ .Zero y) .F := by
  cases h; exact Eval.EQ_0S.star

/-- The obvious consequence of `type_preservation`. -/
theorem type_preservation_Star (h : EvalStar x y) (ht : TP x t) : TP y t := by
  induction h <;> solve_by_elim [type_preservation]

theorem EvalStar.Succ (h : EvalStar x y) : EvalStar (.Succ x) (.Succ y) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem EvalStar.IF (h : EvalStar p q) : EvalStar (.IF p x y) (.IF q x y) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem EvalStar.EQ1 (h : EvalStar x z) : EvalStar (.EQ x y) (.EQ z y) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem EvalStar.EQ2 (h : EvalStar y z) : EvalStar (.EQ x y) (.EQ x z) := by
  induction h <;> constructor <;> (try assumption); constructor; assumption

theorem prediamond (f : exp → exp) (thm : {x y : exp} → EvalStar x y → EvalStar (f x) (f y)) :
    (∃ u, EvalStar x u ∧ EvalStar y u) → ∃ u, EvalStar (f x) u ∧ EvalStar (f y) u
  | ⟨_, h, h'⟩ => ⟨_, thm h, thm h'⟩

/-- Partial Church-Rosser property for big-step semantics. -/
theorem diamond (hy : Eval x y) (hz : Eval x z) : ∃ u, EvalStar y u ∧ EvalStar z u := by
  induction hy generalizing z <;> cases hz <;> simp [*] at *
    <;> try (solve_by_elim [eval_not_EQ_of_succ_EQ, eval_not_EQ_of_succ_EQ2])
  · solve_by_elim [prediamond _ .IF]
  · solve_by_elim [prediamond _ .Succ]
  · next h => let .Succ_Eval h := h; exact ⟨_, h.star.EQ1, Eval.EQ_SS.star⟩
  · next h => let .Succ_Eval h := h; exact ⟨_, h.star.EQ2, Eval.EQ_SS.star⟩
  · next h _ => let .Succ_Eval h := h; exact ⟨_, Eval.EQ_SS.star, h.star.EQ1⟩
  · solve_by_elim [prediamond _ .EQ1]
  · next h' _ _ h => exact ⟨_, h.star.EQ2, h'.star.EQ1⟩
  · next h _ => let .Succ_Eval h := h; exact ⟨_, Eval.EQ_SS.star, h.star.EQ2⟩
  · next h _ _ h' => exact ⟨_, h'.star.EQ1, h.star.EQ2⟩
  · next h ih _ h' => let ⟨v, g, g'⟩ := ih h'; exact ⟨_, g.EQ2, g'.EQ2⟩

[Anand Rao Tadipatri]

Here is a version of @Kyle Miller's code using aesop. It is around 150 lines, but the aesop tags and a few new lemmas are taking up room that can be freed up. Every proof except the last one is a one-liner.

import Mathlib.Tactic.SolveByElim
import Mathlib.Tactic.Use
import Aesop

namespace Semantics

/-- A simple expression language. -/
inductive exp
  | T | F | Zero | Succ (x : exp) | IF (p x y : exp) | EQ (x y : exp)

open exp

/-- Small-step semantics for the simple expression language. -/
inductive Eval : exp → exp → Prop
  | IF_T : Eval (IF T x y) x
  | IF_F : Eval (IF F x y) y
  | IF_Eval : Eval p q → Eval (IF p x y) (IF q x y)
  | Succ_Eval : Eval x y → Eval (Succ x) (Succ y)
  | EQ_same : Eval (EQ x x) T
  | EQ_S0 : Eval (EQ (Succ x) Zero) F
  | EQ_0S : Eval (EQ Zero (Succ y)) F
  | EQ_SS : Eval (EQ (Succ x) (Succ y)) (EQ x y)
  | EQ_Eval1 : Eval x z → Eval (EQ x y) (EQ z y)
  | EQ_Eval2 : Eval y z → Eval (EQ x y) (EQ x z)

@[simp] theorem T_simp : ¬ Eval T z := by aesop (add safe cases [Eval, exp])
@[simp] theorem F_simp : ¬ Eval F z := by aesop (add safe cases [Eval, exp])
@[simp] theorem Zero_simp : ¬ Eval Zero z := by aesop (add safe cases [Eval, exp])


@[aesop safe cases] inductive tp
  | tbool | tnum

open tp

@[aesop unsafe constructors] inductive TP : exp → tp → Prop
  | T : TP T tbool
  | F : TP F tbool
  | Zero : TP Zero tnum
  | IF : TP p tbool → TP x t → TP y t → TP (IF p x y) t
  | Succ : TP x tnum → TP (Succ x) tnum
  | EQ : TP x t → TP y t → TP (EQ x y) tbool

-- Are these lemmas necessary?
@[simp] lemma TP_Succ_not_tbool : ¬(TP (Succ e) tbool) := by aesop (add unsafe cases [TP, exp])

@[aesop safe forward]
lemma TP_tnum_of_TP_Succ_tnum : TP (Succ e) tnum → TP e tnum := by aesop (add unsafe cases [TP, exp])

/-- Type preservation: small-step evaluation preserves the type. -/
theorem type_preservation (he : Eval x y) (ht : TP x t) : TP y t := by
  induction he generalizing t <;> cases ht <;> aesop

/-- Evaluator for expressions. -/
@[aesop norm unfold] def evl : exp → Nat
  | T => 1
  | F => 0
  | exp.Zero => 0
  | Succ x => evl x + 1
  | IF x y z => if evl x = 1 then evl y else evl z
  | EQ x y => if evl x = evl y then 1 else 0

@[simp] theorem Nat.add_one_ne_zero (a : Nat) : a + 1 ≠ 0 := by aesop

/-- Value preservation: the evaluator is constant modulo the small-step semantics. -/
theorem value_preservation (h : Eval x y) : evl x = evl y := by induction h <;> aesop

theorem lt_two_of_bool (ht : TP x tbool) : evl x < 2 := by
  generalize h : tbool = t at ht
  induction ht <;> aesop

/-- Reflexive transitive closure of `Eval`. -/
@[aesop unsafe [cases, constructors]] inductive EvalStar : exp → exp → Prop
  | Id : EvalStar x x
  | Step : Eval x y → EvalStar y z → EvalStar x z

attribute [simp] EvalStar.Id

@[aesop unsafe apply] def Eval.Star (h : Eval x y) : EvalStar x y := EvalStar.Step h EvalStar.Id

@[simp] theorem exists_evalstar : ∃ y, EvalStar x y := ⟨x, EvalStar.Id⟩

@[simp] theorem eval_T : EvalStar T u ↔ u = T := by aesop

@[simp] theorem eval_F : EvalStar F u ↔ u = F := by aesop

@[simp] theorem eval_EQ_self : EvalStar (EQ x x) T := by
  aesop (add safe [apply Eval.Star, constructors Eval])

@[simp] theorem eval_EQ_of_Eval (h : Eval x y) : EvalStar (EQ x y) T := by
  aesop (add safe [apply Eval.EQ_Eval1, constructors Eval])

@[simp] theorem eval_EQ_of_Eval2 (h : Eval y x) : EvalStar (EQ x y) T := by
  aesop (add safe [apply Eval.EQ_Eval2, constructors Eval])

@[aesop unsafe forward, aesop safe apply]
theorem eval_not_EQ_of_succ_EQ (h : Eval (Succ x) y) : EvalStar (EQ y Zero) F := by
  cases h; aesop (add safe [apply Eval.Star, constructors Eval])

@[aesop unsafe forward, aesop safe apply]
theorem eval_not_EQ_of_succ_EQ2 (h : Eval (Succ x) y) : EvalStar (EQ Zero y) F := by
  cases h; aesop (add safe [apply Eval.Star, constructors Eval])

/-- The obvious consequence of `type_preservation`. -/
theorem type_preservation_Star (h : EvalStar x y) (ht : TP x t) : TP y t := by
  induction h <;> aesop (add safe forward [type_preservation])

@[aesop safe apply]
theorem EvalStar.Succ (h : EvalStar x y) : EvalStar (Succ x) (Succ y) := by
  induction h <;> aesop (add safe [constructors Eval])

@[trans] theorem EvalStar.trans (h : EvalStar x y) (h' : EvalStar y z) : EvalStar x z := by
  induction h <;> induction h' <;> aesop (add safe constructors [Eval, EvalStar])

@[aesop safe apply]
theorem EvalStar.IF (h : EvalStar p q) : EvalStar (IF p x y) (IF q x y) := by
  induction h <;> aesop (add safe [constructors Eval])

@[aesop safe apply]
theorem EvalStar.EQ1 (h : EvalStar x z) : EvalStar (EQ x y) (EQ z y) := by
  induction h <;> aesop (add safe [constructors Eval])

@[aesop safe apply]
theorem EvalStar.EQ2 (h : EvalStar y z) : EvalStar (EQ x y) (EQ x z) := by
  induction h <;> aesop (add safe [constructors Eval])

@[aesop safe apply]
theorem prediamond (f : exp → exp) (thm : {x y : exp} → EvalStar x y → EvalStar (f x) (f y))
    (h : ∃ u, EvalStar x u ∧ EvalStar y u) : ∃ u, EvalStar (f x) u ∧ EvalStar (f y) u := by aesop

set_option maxHeartbeats 10000000

/-- Partial Church-Rosser property for big-step semantics. -/
theorem diamond (hy : Eval x y) (hz : Eval x z) : ∃ u, EvalStar y u ∧ EvalStar z u := by
  induction hy generalizing z <;> cases hz <;>
  checkpoint aesop (options := {terminal := false, warnOnNonterminal := false})
  · apply prediamond _ EvalStar.IF; aesop
  · cases a; rename_i z h
    use (EQ z y_1); aesop (add unsafe apply [EvalStar.EQ1, EvalStar.EQ2, Eval.Star, Eval.EQ_SS], safe constructors [Eval])
  · cases a; rename_i y_2 h
    use (EQ x_1 y_2); aesop (add safe apply [Eval.Star], safe constructors [Eval])
  · cases a; rename_i x_2 h
    use (EQ x_2 y_1); aesop (add unsafe apply [EvalStar.EQ1, EvalStar.EQ2, Eval.Star, Eval.EQ_SS], safe constructors [Eval])
  · let ⟨w, _, _⟩ := a_ih a_1
    use (EQ w y_1); aesop (add unsafe apply [EvalStar.EQ1, EvalStar.EQ2, Eval.Star, Eval.EQ_SS])
  · cases a; rename_i y_2 h
    use (EQ x_1 y_2); aesop (add unsafe apply [EvalStar.EQ1, EvalStar.EQ2, Eval.Star, Eval.EQ_SS], safe constructors [Eval])

end Semantics

[Joachim Breitner]

Trebor Huang said:

Why is EQ T F stuck in the small step semantics? Or did I miss any rules?

Yes, that is likely an omission in the original; this was also noticed in the Agda formalization

[Sebastian Ullrich]

Necessity of dependent types aside, I did find Conor McBride's approach quite elegant. Here is a Lean 4 version, making use of tactics where possible (90 lines without blank and comment lines).
In the end there wasn't really any part that could further be simplified with Aesop.

namespace Semantics

/-- A simple type language. -/
inductive Ty where
  | bool | num

/-- A simple expression language, intrinsically typed. -/
inductive Exp : Ty → Type where
  | true : Exp .bool
  | false : Exp .bool
  | zero : Exp .num
  | succ (n : Exp .num) : Exp .num
  | if (p : Exp .bool) (t e : Exp ty) : Exp ty
  | eq (x y : Exp ty) : Exp .bool

section
-- mutual notation/inductive workaround, I should really fix this at some point
set_option hygiene false
local infix:40 "~>" => Eval
/-- Small-step semantics for the simple expression language. -/
inductive Eval : Exp ty → Exp ty → Prop
  | if_true : .if .true t e ~> t
  | if_false : .if .false t e ~> e
  | if_eval : p ~> q →
              .if p t e ~> .if q t e
  | succ_eval : x ~> y →
                .succ x ~> .succ y
  | eq_same : .eq x x ~> .true
  | eq_s0 : .eq (.succ x) .zero ~> .false
  | eq_0s : .eq .zero (.succ y) ~> .false
  | eq_ss : .eq (.succ x) (.succ y) ~> .eq x y
  | eq_tf : .eq .true .false ~> .false
  | eq_ft : .eq .false .true ~> .false
  | eq_l : x ~> x' →
           .eq x y ~> .eq x' y
  | eq_r : y ~> y' →
           .eq x y ~> .eq x y'
end
infix:40 " ~> " => Eval

/-- Typed evaluation. -/
abbrev Val : Ty → Type
  | .bool => Bool
  | .num  => Nat

-- Lean's termination checker is (understandably) not happy when specified as polymorphic recursion
def Val.embed : (ty : Ty) → Val ty → Exp ty
  | .bool, true  => .true
  | .bool, false => .false
  | .num,  n     => n.fold (fun _ => .succ) .zero

instance : DecidableEq (Val ty) := by
  cases ty <;> infer_instance

def eval : Exp ty → Val ty
  | .true     => true
  | .false    => false
  | .zero     => 0
  | .succ n   => eval n + 1
  | .if p t e => if eval p then eval t else eval e
  | .eq x y   => eval x = eval y

/-- The reflexive-transitive closure -/
inductive RTC (r : α → α → Prop) : α → α → Prop where
  | refl : RTC r x x
  | step : r x y → RTC r y z → RTC r x z

theorem RTC.one : r x y → RTC r x y := (.step · .refl)

theorem RTC.map {f : α → β} (hrs : ∀ {x y}, r x y → s (f x) (f y)) : RTC r x y → RTC s (f x) (f y) := by
  intro h
  induction h with
  | refl          => exact .refl
  | step hxz _ ih => exact .step (hrs hxz) ih

theorem RTC.trans : RTC r x y → RTC r y z → RTC r x z := by
  intro hxy hyz
  induction hxy with
  | refl         => exact hyz
  | step hx _ ih => exact .step hx (ih hyz)

infix:40 " ~>* " => RTC Eval

@[simp] theorem Nat.succ_ne_zero : n + 1 ≠ 0 := by intro; trivial
@[simp] theorem Nat.zero_ne_succ : 0 ≠ n + 1 := by intro; trivial

/-- Operational and denotational semantics coincide. -/
theorem eval_eval : x ~>* (eval x).embed := by
  induction x with
    rw [eval]
  | succ => exact RTC.map .succ_eval ‹_›
  | «if» p t e =>
    -- first evaluate the predicate
    -- (Lean needs some help here with the higher-order unification)
    apply RTC.trans (RTC.map (f := (Exp.if · t e)) .if_eval ‹_›)
    -- then do an if_true/if_false step depending on `p`
    cases eval p <;> exact RTC.step (by constructor) ‹_›
  | @eq ty x y =>
    -- first evaluate the LHS and RHS
    apply RTC.trans (RTC.map (f := (Exp.eq · y)) .eq_l ‹_›)
    apply RTC.trans (RTC.map (f := (Exp.eq _ ·)) .eq_r ‹_›)
    -- we want to worry about values, not terms
    generalize eval y = ey
    -- then do a case bash including one induction for the recursive `succ/succ` case
    cases ty <;> induction eval x generalizing ey <;> cases ey
    case num.succ.succ ih _ =>
      apply RTC.step .eq_ss
      -- massage goal a bit to fit IH
      simp only [Val, Nat.succ.injEq]
      apply ih
    -- all non-recursive cases can be solved uniformly
    all_goals exact RTC.one (by constructor)
  | _ => exact .refl

/-- Small steps preserve denotational semantics. -/
theorem step_eval : x ~> y → eval x = eval y := by
  intro hxy
  -- `simp` needs a bit extra help with unfolding `Val .num` to `Nat`
  induction hxy <;> (dsimp [eval, Val]; simp [*])

/-- Partial Church-Rosser is a direct consequence of the above two theorems. -/
theorem diamond : x ~> y → x ~> z → ∃ u, y ~>* u ∧ z ~>* u :=
  fun hxy hxz =>
    ⟨(eval x).embed, step_eval hxy ▸ eval_eval, step_eval hxz ▸ eval_eval⟩

end Semantics