Denotational Semantics repo to learn Lean

Stream: new members

[Juanjo Madrigal]

Hi! I'm Juanjo Madrigal from Madrid, good to see you all :wave:

I'm relatively new to Lean, so to improve my Lean knowledge (and learn some other topics related to Denotational Semantics), I've started to read the book "The Formal Semantics of Programming Languages" (Glynn Winskel, 1993) and translate all its concepts to Lean. It's on https://github.com/juanjomadrigal/denotational-lean ; I plan to upload some content every few days.

I'm sure right now it is terribly un-idiomatic :smile: and with lots of things to improve. I would like to ask your help to make it better. Any feedback will be much appreciated :pray:

Any other advice to exercise and sharpen Lean coding ability? I would like to, little by little, acquire the experience needed to write production-quality Lean code.

Thank you!!

[Juanjo Madrigal]

I need some hint about a part of the formalization that is clearly not ok :sweat_smile:
It is referenced here and the self-contained code would be

abbrev Loc := String

inductive Aexp : Type where
  | Nat : Nat -> Aexp
  | Loc : Loc -> Aexp
  | Add : Aexp -> Aexp -> Aexp
  | Sub : Aexp -> Aexp -> Aexp
  | Mul : Aexp -> Aexp -> Aexp

inductive Bexp : Type where
  | Bool : Bool -> Bexp
  | Eq : Aexp -> Aexp -> Bexp
  | Le : Aexp -> Aexp -> Bexp
  | Not : Bexp -> Bexp
  | And : Bexp -> Bexp -> Bexp
  | Or  : Bexp -> Bexp -> Bexp

inductive Com : Type where
  | Skip : Com
  | Assing : Loc -> Aexp -> Com
  | Seq : Com -> Com -> Com
  | Ite : Bexp -> Com -> Com -> Com
  | While : Bexp -> Com -> Com

abbrev State := List (Loc × Nat)
namespace State
def lookup(σ : State) : Loc -> Nat := fun l => match σ with
  | [] => 0
  | ((l',n)::xs) => if l == l' then n else lookup xs l
end State

abbrev Config := Aexp × State
inductive a_deriv : Config -> Nat -> Prop
  | num {n σ} : a_deriv (Aexp.Nat n, σ) n
  | loc {l σ} : a_deriv (Aexp.Loc l, σ) (State.lookup σ l)
  | add {a0 n0 a1 n1 σ} : a_deriv (a0,σ) n0 -> a_deriv (a1,σ) n1 -> a_deriv (Aexp.Add a0 a1,σ) (n0+n1)
  | sub {a0 n0 a1 n1 σ} : a_deriv (a0,σ) n0 -> a_deriv (a1,σ) n1 -> a_deriv (Aexp.Sub a0 a1,σ) (n0-n1)
  | mul {a0 n0 a1 n1 σ} : a_deriv (a0,σ) n0 -> a_deriv (a1,σ) n1 -> a_deriv (Aexp.Mul a0 a1,σ) (n0*n1)

abbrev BConfig := Bexp × State
inductive b_deriv : BConfig -> Bool -> Prop
  | bool {t σ} : b_deriv (Bexp.Bool t, σ) t
  | eq {a0 n0 a1 n1 σ} : a_deriv (a0, σ) n0 -> a_deriv (a1, σ) n1 -> b_deriv (Bexp.Eq a0 a1, σ) (n0 == n1)
  | le {a0 n0 a1 n1 σ} : a_deriv (a0, σ) n0 -> a_deriv (a1, σ) n1 -> b_deriv (Bexp.Le a0 a1, σ) (n0 <= n1)
  | not {b t σ} : b_deriv (b, σ) t -> b_deriv (Bexp.Not b, σ) (!t)
  | and {b0 t0 b1 t1 σ} : b_deriv (b0, σ) t0 -> b_deriv (b1, σ) t1 -> b_deriv (Bexp.And b0 b1, σ) (t0 && t1)
  | or  {b0 t0 b1 t1 σ} : b_deriv (b0, σ) t0 -> b_deriv (b1, σ) t1 -> b_deriv (Bexp.Or  b0 b1, σ) (t0 || t1)

abbrev CConfig := Com × State

-- fixme : target should be Prop, but it then fails to show termination in the example below
inductive c_deriv : CConfig -> State -> Type
  | skip {σ} : c_deriv (Com.Skip, σ) σ
  | assign {a n l σ} : a_deriv (a, σ) n -> c_deriv (Com.Assing l a, σ) ((l,n)::σ)
  | seq {c0 c1 σ σ' σ''} : c_deriv (c0,σ) σ'' -> c_deriv (c1,σ'') σ' -> c_deriv (Com.Seq c0 c1, σ) σ'
  | ite_true  {b c0 c1 σ σ'} : b_deriv (b,σ) true  -> c_deriv (c0,σ) σ' -> c_deriv (Com.Ite b c0 c1, σ) σ'
  | ite_false {b c0 c1 σ σ'} : b_deriv (b,σ) false -> c_deriv (c1,σ) σ' -> c_deriv (Com.Ite b c0 c1, σ) σ'
  | while_false {b c σ} : b_deriv (b,σ) false -> c_deriv (Com.While b c, σ) σ
  | while_true {b c σ σ' σ''} : b_deriv (b,σ) true -> c_deriv (c, σ) σ'' -> c_deriv (Com.While b c, σ'') σ' -> c_deriv (Com.While b c, σ) σ'

/- example: ⟨while true do skip, σ⟩ -> σ' is not achievable  -/

-- fixme : this definition should be inside the example below,
-- but then it's tricky to make the recursive definition
def aux (σ σ' : State) (hh : c_deriv (Com.While (Bexp.Bool true) Com.Skip, σ) σ') : False :=
  match hh with
    | c_deriv.while_false bd => by cases bd
    | @c_deriv.while_true _ _ σ σ' σ'' _ cd wcd => by
      have h : σ = σ'' := by cases cd; grind
      simp [<-h] at wcd
      exact aux σ σ' wcd

example : ¬ ∃ (σ σ' : State) , Nonempty (c_deriv (Com.While (Bexp.Bool true) Com.Skip, σ) σ') := by
  intro ⟨σ,σ',⟨h⟩⟩
  exact aux σ σ' h

The idea is roughly as follows: I declare three inductive types for arithmetical expressions, boolean expressions and commands, respectively. Then I declare Props for expressions to derivable into some natural number ($\langle a,\sigma \rangle \longrightarrow n$) or boolean ($\langle b,\sigma \rangle \longrightarrow T/F$).

It should be done similar for commands, but in this case, if the target is Prop, I get into some termination problems for proving very easy things, so I turned it into Type. So it really seems there is something that must be done differently.

Any idea...?

[pandaman]

You need to use induction hh for Prop.

[pandaman]

This works

-- fixme : target should be Prop, but it then fails to show termination in the example below
inductive c_deriv : CConfig -> State -> Prop where
  | skip {σ} : c_deriv (Com.Skip, σ) σ
  | assign {a n l σ} : a_deriv (a, σ) n -> c_deriv (Com.Assing l a, σ) ((l,n)::σ)
  | seq {c0 c1 σ σ' σ''} : c_deriv (c0,σ) σ'' -> c_deriv (c1,σ'') σ' -> c_deriv (Com.Seq c0 c1, σ) σ'
  | ite_true  {b c0 c1 σ σ'} : b_deriv (b,σ) true  -> c_deriv (c0,σ) σ' -> c_deriv (Com.Ite b c0 c1, σ) σ'
  | ite_false {b c0 c1 σ σ'} : b_deriv (b,σ) false -> c_deriv (c1,σ) σ' -> c_deriv (Com.Ite b c0 c1, σ) σ'
  | while_false {b c σ} : b_deriv (b,σ) false -> c_deriv (Com.While b c, σ) σ
  | while_true {b c σ σ' σ''} : b_deriv (b,σ) true -> c_deriv (c, σ) σ'' -> c_deriv (Com.While b c, σ'') σ' -> c_deriv (Com.While b c, σ) σ'

/- example: ⟨while true do skip, σ⟩ -> σ' is not achievable  -/

-- fixme : this definition should be inside the example below,
-- but then it's tricky to make the recursive definition
def aux (cfg : CConfig) (σ σ' : State) (hh : c_deriv cfg σ') (h : cfg = (Com.While (Bexp.Bool true) Com.Skip, σ)) : False := by
  induction hh with
  | skip | assign | seq | ite_true | ite_false => grind
  | while_false bd =>
    simp only [Prod.mk.injEq, Com.While.injEq] at h
    simp only [h] at bd
    nomatch bd
  | @while_true b c σ₁ σ₂ σ₃ _ cd wcd ih₁ ih₂ =>
    have h' : σ = σ₃ := by cases cd <;> grind
    simp only [Prod.mk.injEq, Com.While.injEq] at h
    simp [h, h'] at ih₂

example : ¬ ∃ (σ σ' : State) , Nonempty (c_deriv (Com.While (Bexp.Bool true) Com.Skip, σ) σ') := by
  intro ⟨σ,σ',⟨h⟩⟩
  exact aux _ σ σ' h rfl

[Juanjo Madrigal]

Great!! I've refactored it a little bit, much nicer now (commit).

[Juanjo Madrigal]

Thanks a lot @pandaman !!

[Juanjo Madrigal]

Hi again,

I'm trying to use this induction tactic to simplify other parts (e.g.) and I have found something funny related to the grind tactic.

The goal is to prove unicity of derivations for both arithmetic and boolean expressions. For the boolean case (b_unique), it turns out to be very easy (and perhaps there are easier ways). But for the arithmetic case, the very same structure does not work, and it's strange, because the expressions are built in a similar fashion. What I am missing?

abbrev Loc := String

inductive Aexp : Type where
  | Nat : Nat -> Aexp
  | Loc : Loc -> Aexp
  | Add : Aexp -> Aexp -> Aexp
  | Sub : Aexp -> Aexp -> Aexp
  | Mul : Aexp -> Aexp -> Aexp

inductive Bexp : Type where
  | Bool : Bool -> Bexp
  | Eq : Aexp -> Aexp -> Bexp
  | Le : Aexp -> Aexp -> Bexp
  | Not : Bexp -> Bexp
  | And : Bexp -> Bexp -> Bexp
  | Or  : Bexp -> Bexp -> Bexp

abbrev State := List (Loc × Nat)
namespace State
def lookup(σ : State) : Loc -> Nat := fun l => match σ with
  | [] => 0
  | ((l',n)::xs) => if l == l' then n else lookup xs l
end State

abbrev Config := Aexp × State
inductive a_deriv : Config -> Nat -> Prop
  | num {n σ} : a_deriv (Aexp.Nat n, σ) n
  | loc {l σ} : a_deriv (Aexp.Loc l, σ) (State.lookup σ l)
  | add {a0 n0 a1 n1 σ} : a_deriv (a0,σ) n0 -> a_deriv (a1,σ) n1 -> a_deriv (Aexp.Add a0 a1,σ) (n0+n1)
  | sub {a0 n0 a1 n1 σ} : a_deriv (a0,σ) n0 -> a_deriv (a1,σ) n1 -> a_deriv (Aexp.Sub a0 a1,σ) (n0-n1)
  | mul {a0 n0 a1 n1 σ} : a_deriv (a0,σ) n0 -> a_deriv (a1,σ) n1 -> a_deriv (Aexp.Mul a0 a1,σ) (n0*n1)

abbrev BConfig := Bexp × State
inductive b_deriv : BConfig -> Bool -> Prop
  | bool {t σ} : b_deriv (Bexp.Bool t, σ) t
  | eq {a0 n0 a1 n1 σ} : a_deriv (a0, σ) n0 -> a_deriv (a1, σ) n1 -> b_deriv (Bexp.Eq a0 a1, σ) (n0 == n1)
  | le {a0 n0 a1 n1 σ} : a_deriv (a0, σ) n0 -> a_deriv (a1, σ) n1 -> b_deriv (Bexp.Le a0 a1, σ) (n0 <= n1)
  | not {b t σ} : b_deriv (b, σ) t -> b_deriv (Bexp.Not b, σ) (!t)
  | and {b0 t0 b1 t1 σ} : b_deriv (b0, σ) t0 -> b_deriv (b1, σ) t1 -> b_deriv (Bexp.And b0 b1, σ) (t0 && t1)
  | or  {b0 t0 b1 t1 σ} : b_deriv (b0, σ) t0 -> b_deriv (b1, σ) t1 -> b_deriv (Bexp.Or  b0 b1, σ) (t0 || t1)

-- does not work
theorem a_unique (a : Aexp) (σ : State) : a_deriv (a,σ) n0 ∧ a_deriv (a,σ) n1 -> n0 = n1 := by
  intro ⟨h0,h1⟩
  induction a with
  | Nat n => cases h0; cases h1; trivial
  | Loc l => cases h0; cases h1; trivial
  | Add a0 a1 => cases h0; cases h1; grind
  | Sub a0 a1 => cases h0; cases h1; grind
  | Mul a0 a1 => cases h0; cases h1; grind

theorem b_unique (b : Bexp) (σ : State) : b_deriv (b,σ) t0 ∧ b_deriv (b,σ) t1 -> t0 = t1 := by
  intro ⟨h0,h1⟩
  induction b with
  | Bool t => cases h0; cases h1; trivial
  | Eq a0 a1 => cases h0; cases h1; grind [a_unique]
  | Le a0 a1 => cases h0; cases h1; grind [a_unique]
  | Not b => cases h0; cases h1; grind
  | And b0 b1 => cases h0; cases h1; grind
  | Or  b0 b1 => cases h0; cases h1; grind