Bisimulation chapter wrong

[srghma]

PLFaLean/Plfl/More/Bisimulation.lean

Line 18 in 138c217

| let : Sim l l' → Sim m m' → Sim (.let l m) (.let l' m')

https://plfa.github.io/Bisimulation/#simulation

The let should simulate abs, but simulates let

Should be more like

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)

_† : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A
(` x) †          = ` x
(ƛ N) †         = ƛ (N †)
(L · M) †       = (L †) · (M †)
(`let M N) †    = (ƛ (N †)) · (M †)

infix  4 _~_
infix  5 ~ƛ_
infix  7 _~·_

data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

  ~` : ∀ {Γ A} {x : Γ ∋ A}
     ---------
   → ` x ~ ` x

  ~ƛ_ : ∀ {Γ A B} {N N† : Γ , A ⊢ B}
    → N ~ N†
      ----------
    → ƛ N ~ ƛ N†

  _~·_ : ∀ {Γ A B} {L L† : Γ ⊢ A ⇒ B} {M M† : Γ ⊢ A}
    → L ~ L†
    → M ~ M†
      ---------------
    → L · M ~ L† · M†

  ~let : ∀ {Γ A B} {M M† : Γ ⊢ A} {N N† : Γ , A ⊢ B}
    → M ~ M†
    → N ~ N†
      ----------------------
    → `let M N ~ (ƛ N†) · M†

~val⁻¹ : ∀ {Γ A} {M M† : Γ ⊢ A}
  → M ~ M†
  → Value M†
    --------
  → Value M
~val⁻¹ ~`           ()
~val⁻¹ (~ƛ ~N)      V-ƛ  =  V-ƛ
~val⁻¹ (~L ~· ~M)   ()
~val⁻¹ (~let ~M ~N) ()

M~M† : ∀ {Γ A} (M : Γ ⊢ A) → M ~ (M †)
M~M† (` x)       = ~`
M~M† (ƛ N)      = ~ƛ (M~M† N)
M~M† (L · M)    = (M~M† L) ~· (M~M† M)
M~M† (`let M N) = ~let (M~M† M) (M~M† N)

†-to-~ : ∀ {Γ A} {M N : Γ ⊢ A}
  → M † ≡ N
    -------
  → M ~ N
†-to-~ {M = M} refl = M~M† M

~-to-† : ∀ {Γ A} {M N : Γ ⊢ A}
  → M ~ N
    -------
  → M † ≡ N
~-to-† ~`             = refl
~-to-† (~ƛ ~N)        = cong ƛ (~-to-† ~N)
~-to-† (~L ~· ~M)     = cong₂ _·_ (~-to-† ~L) (~-to-† ~M)
~-to-† (~let ~M ~N)   = cong₂ (λ N† M† → (ƛ N†) · M†) (~-to-† ~N) (~-to-† ~M)

[rami3l]

@srghma Thanks for pointing out the erratum! Please feel free to propose a fix if you can.