Formalisation of L1 operational semantics, with various proofs

L1Semantics.agda

{-
    This is a formalisation of the operational semantics and typing rules of L1, a 
    small language introduced in the Semantics of Programming Languages module in
    Part 1B of the Uni of Cambridge Computer Science course (2022-2023)

    The definitions and proofs could be extended to L2 and L3 as an exercise!
-}
module L1Semantics where

    open import Data.String hiding (toList)
    open import Level hiding (suc ; zero)
    open import Data.Nat hiding (_≟_)
    open import Data.Bool hiding (_≟_)
    open import Data.Unit hiding (_≟_)
    open import Data.Empty
    open import Data.Sum
    open import Data.Product
    open import Data.List
    open import Relation.Nullary.Decidable using (⌊_⌋)
    open import Relation.Nullary
    open import Relation.Binary.PropositionalEquality

    -- Essentially just used when we need to tell the checker explicitly "this case doesn't arise"
    -- in proofs
    absurd : {A : Set} → ⊥ → A
    absurd = ⊥-elim

    -- ==== L1  DEFINITIONS ====

    Loc : Set
    Loc = String

    Store : Set
    Store = List (Loc × ℕ)

    get : Loc → Store → ℕ
    get l [] = 0
    get l ((l' , m) ∷ s) with ⌊ l ≟ l' ⌋ 
    ... | true = m
    ... | false = get l s

    store-contains : Loc → Store → Set
    store-contains l [] = ⊥
    store-contains l ((l′ , m) ∷ s) with l ≟ l′
    ... | yes refl = ⊤
    ... | no _ = store-contains l s

    -- Whether the store contains a location is decideable
    store-contains? : (l : Loc) → (s : Store) → Dec (store-contains l s)
    store-contains? l [] = no (λ x → x)
    store-contains? l ((l′ , m) ∷ s) with l ≟ l′
    ... | yes refl = yes tt
    ... | no _ = store-contains? l s

    store-contains-first : {s : Store} {l : Loc} {n : ℕ} → store-contains l ((l , n) ∷ s)
    store-contains-first {s} {l} {n} with l ≟ l
    ... | yes refl = tt
    ... | no ¬p    = absurd (¬p refl)

    store-contains-weaken : {s : Store} {l l′ : Loc} {n : ℕ} → store-contains l s → store-contains l ((l′ , n) ∷ s)
    store-contains-weaken {s} {l} {l′} {n} l-in-s with l ≟ l′
    ... | yes refl = tt
    ... | no _     = l-in-s

    -- ==== SYNTAX ====

    data Op : Set where
        Add : Op
        GTEQ : Op

    data L1 : Set where
        Int : ℕ → L1
        Boolean : Bool → L1
        App : Op → L1 → L1 → L1
        If_Then_Else_ : L1 → L1 → L1 → L1
        Skip : L1
        Seq : L1 → L1 → L1
        Assign : Loc → L1 → L1
        Deref : Loc → L1
        While_Do_ : L1 → L1 → L1

    isValue : L1 → Set
    isValue (Int _) = ⊤
    isValue (Boolean _) = ⊤
    isValue Skip = ⊤
    isValue _ = ⊥

    isValue? : (e : L1) → Dec (isValue e)
    isValue? (Int _) = yes tt
    isValue? (Boolean _) = yes tt
    isValue? Skip = yes tt
    isValue? (App op e e₁) = no (λ x → x)
    isValue? (If e Then e₁ Else e₂) = no (λ x → x)
    isValue? (Seq e e₁) = no (λ x → x)
    isValue? (Assign l e) = no (λ x → x)
    isValue? (Deref l) = no (λ x → x)
    isValue? (While e Do e₁) = no (λ x → x)

    -- ==== REDUCTION RULES ====

    data Config : Set where
        ⟨_,_⟩ : L1 → Store → Config

    -- Small-step reduction relation
    data _⟶_ : Config → Config → Set where
        op+ : {n m : ℕ} {s : Store} 
            → ⟨ App Add (Int n) (Int m) , s ⟩ ⟶ ⟨ Int (n + m) , s ⟩
        op≥ : {n m : ℕ} {s : Store} 
            → ⟨ App GTEQ (Int n) (Int m) , s ⟩ ⟶ ⟨ Boolean ⌊ n ≥? m ⌋ , s ⟩
        op1 : {op : Op} {e₁ e₁′ e₂ : L1} {s s′ : Store}
            → ⟨ e₁ , s ⟩ ⟶ ⟨ e₁′ , s′ ⟩ 
            → ⟨ App op e₁ e₂ , s ⟩ ⟶ ⟨ App op e₁′ e₂ , s′ ⟩
        op2 : {op : Op} {v e₂ e₂′ : L1} {s s′ : Store}
            → isValue v
            → ⟨ e₂ , s ⟩ ⟶ ⟨ e₂′ , s′ ⟩ 
            → ⟨ App op v e₂ , s ⟩ ⟶ ⟨ App op v e₂′ , s′ ⟩
        seq1 : {e : L1} {s : Store}
            → ⟨ Seq Skip e , s ⟩ ⟶ ⟨ e , s ⟩
        seq2 : {e₁ e₁′ e₂ : L1} {s s′ : Store}
            → ⟨ e₁ , s ⟩ ⟶ ⟨ e₁′ , s′ ⟩ 
            → ⟨ Seq e₁ e₂ , s ⟩ ⟶ ⟨ Seq e₁′ e₂ , s′ ⟩
        if1 : {e₁ e₂ : L1} {s : Store}
            → ⟨ If (Boolean true) Then e₁ Else e₂ , s ⟩ ⟶ ⟨ e₁ , s ⟩
        if2 : {e₁ e₂ : L1} {s : Store}
            → ⟨ If (Boolean false) Then e₁ Else e₂ , s ⟩ ⟶ ⟨ e₂ , s ⟩
        if3 : {e₁ e₁′ e₂ e₃ : L1} {s s′ : Store}
            → ⟨ e₁ , s ⟩ ⟶ ⟨ e₁′ , s′ ⟩ 
            → ⟨ If e₁ Then e₂ Else e₃ , s ⟩ ⟶ ⟨ If e₁′ Then e₂ Else e₃ , s′ ⟩
        deref : {l : Loc} {s : Store}
            → store-contains l s
            → ⟨ Deref l , s ⟩ ⟶ ⟨ Int (get l s) , s ⟩
        assign1 : {l : Loc} {n : ℕ} {s : Store}
            → store-contains l s
            → ⟨ Assign l (Int n) , s ⟩ ⟶ ⟨ Skip , (l , n) ∷ s ⟩
        assign2 : {e e′ : L1} {l : Loc} {s s′ : Store}
            → ⟨ e , s ⟩ ⟶ ⟨ e′ , s′ ⟩ 
            → ⟨ Assign l e , s ⟩ ⟶ ⟨ Assign l e′ , s′ ⟩
        while : {e₁ e₂ : L1} {s : Store}
            → ⟨ While e₁ Do e₂ , s ⟩ ⟶ ⟨ If e₁ Then (Seq e₂ (While e₁ Do e₂)) Else Skip , s ⟩

    -- Two functions to extract information from a reduction rule (rarely used)
    codomain-expr : {e e′ : L1} {s s′ : Store} → ⟨ e , s ⟩ ⟶ ⟨ e′ , s′ ⟩ → L1
    codomain-expr {e′ = e′} r = e′
    codomain-store : {e e′ : L1} {s s′ : Store} → ⟨ e , s ⟩ ⟶ ⟨ e′ , s′ ⟩ → Store
    codomain-store {s′ = s′} r = s′

    -- ==== TYPING RULES ====

    data Type : Set where
        int : Type
        bool : Type
        unit : Type

    -- Type equality is decideable (comes in useful for type inference)

    ¬int≡bool : ¬ (_≡_ {A = Type} int bool)
    ¬int≡bool ()

    ¬int≡unit : ¬ (_≡_ {A = Type} int unit)
    ¬int≡unit ()

    ¬unit≡bool : ¬ (_≡_ {A = Type} unit bool)
    ¬unit≡bool ()

    _≟ᵗ_ : (T T′ : Type) → Dec (T ≡ T′)
    int  ≟ᵗ int  = yes refl
    int  ≟ᵗ bool = no ¬int≡bool
    int  ≟ᵗ unit = no ¬int≡unit
    bool ≟ᵗ int  = no (λ p → ¬int≡bool (sym p))
    bool ≟ᵗ bool = yes refl
    bool ≟ᵗ unit = no (λ p → ¬unit≡bool (sym p))
    unit ≟ᵗ int  = no (λ p → ¬int≡unit (sym p))
    unit ≟ᵗ bool = no ¬unit≡bool
    unit ≟ᵗ unit = yes refl  

    data TLoc : Set where
        intref : TLoc

    Context : Set
    Context = List (Loc × TLoc)

    Γ-contains : Loc → Context → Set
    Γ-contains l [] = ⊥
    Γ-contains l ((l′ , m) ∷ Γ) with l ≟ l′
    ... | yes refl = ⊤
    ... | no _ = Γ-contains l Γ

    Γ-contains? : (l : Loc) → (Γ : Context) → Dec (Γ-contains l Γ)
    Γ-contains? l [] = no (λ x → x)
    Γ-contains? l ((l′ , m) ∷ Γ) with l ≟ l′
    ... | yes refl = yes tt
    ... | no _ = Γ-contains? l Γ

    data _⊢_꞉_ : Context → L1 → Type → Set where
        int : {Γ : Context} {n : ℕ} → Γ ⊢ Int n ꞉ int
        bool : {Γ : Context} {b : Bool} → Γ ⊢ Boolean b ꞉ bool
        op+ : {Γ : Context} {e₁ e₂ : L1} 
            → Γ ⊢ e₁ ꞉ int → Γ ⊢ e₂ ꞉ int
            → Γ ⊢ App Add e₁ e₂ ꞉ int
        op≥ : {Γ : Context} {e₁ e₂ : L1} 
            → Γ ⊢ e₁ ꞉ int → Γ ⊢ e₂ ꞉ int
            → Γ ⊢ App GTEQ e₁ e₂ ꞉ bool
        if : {Γ : Context} {e₁ e₂ e₃ : L1} {T : Type}
            → Γ ⊢ e₁ ꞉ bool → Γ ⊢ e₂ ꞉ T → Γ ⊢ e₃ ꞉ T
            → Γ ⊢ If e₁ Then e₂ Else e₃ ꞉ T
        assign : {Γ : Context} {e : L1} {l : Loc}
            → Γ-contains l Γ
            → Γ ⊢ e ꞉ int
            → Γ ⊢ Assign l e ꞉ unit
        deref : {Γ : Context} {l : Loc}
            → Γ-contains l Γ
            → Γ ⊢ Deref l ꞉ int
        skip : {Γ : Context} → Γ ⊢ Skip ꞉ unit
        seq : {Γ : Context} {e₁ e₂ : L1} {T : Type}
            → Γ ⊢ e₁ ꞉ unit → Γ ⊢ e₂ ꞉ T
            → Γ ⊢ Seq e₁ e₂ ꞉ T
        while : {Γ : Context} {e₁ e₂ : L1}
            → Γ ⊢ e₁ ꞉ bool → Γ ⊢ e₂ ꞉ unit
            → Γ ⊢ While e₁ Do e₂ ꞉ unit

    -- Equivalent to the statement "dom(Γ) ⊆ dom(s)" (used often in the proofs)
    all-locations : (Γ : Context) → (s : Store) → Set
    all-locations Γ s = {l : Loc} → Γ-contains l Γ → store-contains l s

    -- Equivalent to the statement "dom(Γ) ⊆ dom(s) implies dom(Γ) ⊆ dom((l , n) ∷ s)"
    all-locations-weaken : {Γ : Context} {s : Store} {n : ℕ} → (l : Loc) 
        → all-locations Γ s → all-locations Γ ((l , n) ∷ s)
    all-locations-weaken {Γ} {s} {n} l all-locs {l′} l′∈Γ with l ≟ l′
    ... | yes refl = store-contains-first {s} {l} {n}
    ... | no ¬p = store-contains-weaken {s} {l′} {l} {n} (all-locs l′∈Γ)

    -- An obvious-but-not-obvious lemma that is needed in various proofs:
    -- You cannot reduce a value (proven by inspecting the definition of ⟶)
    value-cannot-reduce : {e : L1} {s : Store} → isValue e 
        → ¬ (Σ[ e′ ∈ L1 ] Σ[ s′ ∈ Store ] ⟨ e , s ⟩ ⟶ ⟨ e′ , s′ ⟩)
    value-cannot-reduce {e} v-is-value x with isValue? e
    value-cannot-reduce {Int x}     v-is-value () | yes _
    value-cannot-reduce {Boolean x} v-is-value () | yes _
    value-cannot-reduce {Skip}      v-is-value () | yes _
    value-cannot-reduce {e}         e-is-value _  | no ¬e-is-value = ¬e-is-value e-is-value

    -- ==== PROOFS ====

    determinacy : {e e₁ e₂ : L1} {s s₁ s₂ : Store}
        → ⟨ e , s ⟩ ⟶ ⟨ e₁ , s₁ ⟩ → ⟨ e , s ⟩ ⟶ ⟨ e₂ , s₂ ⟩
        → (e₁ ≡ e₂) × (s₁ ≡ s₂)
    determinacy {App op e e₁} (op1 r) (op1 r′) with determinacy r r′
    ... | (p , q) = cong (λ x → App op x e₁) p , q
    determinacy {App op v e₁} (op2 v-is-value r) (op2 v-is-value′ r′) with determinacy r r′
    ... | (p , q) = cong (λ x → App op v x) p , q
    determinacy {App op v e₁} (op2 v-is-value r) (op1 r′) = absurd (value-cannot-reduce v-is-value (codomain-expr r′ , codomain-store r′ , r′))
    determinacy {App op v e₁} (op1 r) (op2 v-is-value r′) = absurd (value-cannot-reduce v-is-value (codomain-expr r , codomain-store r , r))
    determinacy {App Add (Int n) (Int m)} op+ op+ = refl , refl
    determinacy {App GTEQ (Int n) (Int m)} op≥ op≥ = refl , refl
    determinacy {If (Boolean true) Then e₁ Else e₂} if1 if1 = refl , refl
    determinacy {If (Boolean false) Then e₁ Else e₂} if2 if2 = refl , refl
    determinacy {If e Then e₁ Else e₂} (if3 r) (if3 r′) with determinacy r r′
    ... | (p , q) = cong (λ x → If x Then e₁ Else e₂) p , q
    determinacy {Seq Skip e₁} seq1 seq1 = refl , refl
    determinacy {Seq e e₁} (seq2 r) (seq2 r′) with determinacy r r′
    ... | (p , q) = cong (λ x → Seq x e₁) p , q
    determinacy {Assign l (Int n)} (assign1 _) (assign1 _) = refl , refl
    determinacy {Assign l e} (assign2 r) (assign2 r′) with determinacy r r′
    ... | (p , q) = cong (λ x → Assign l x) p , q
    determinacy {Deref l} (deref _) (deref _) = refl , refl
    determinacy {While e₁ Do e₂} while while = refl , refl

    progress : {e : L1} {s : Store} {Γ : Context} {T : Type}
        → Γ ⊢ e ꞉ T → all-locations Γ s
        → isValue e ⊎ (Σ[ e′ ∈ L1 ] Σ[ s′ ∈ Store ] ⟨ e , s ⟩ ⟶ ⟨ e′ , s′ ⟩)
    progress {Int n} _ _ = inj₁ tt
    progress {Boolean b} _ _ = inj₁ tt
    progress {Skip} t _ = inj₁ tt
    progress {App Add e e₁} {s} (op+ t t₁) all-locs with progress {e} {s} t all-locs | progress {e₁} {s} t₁ all-locs
    progress {App Add (Int n) (Int m)} {s} (op+ t t₁) all-locs | inj₁ n-is-value | inj₁ m-is-value = inj₂ (Int (n + m) , s , op+)
    progress {App Add v e₁} {s} (op+ t t₁) all-locs | inj₁ n-is-value | inj₂ (e′ , s′ , r) = inj₂ (App Add v e′ , s′ , op2 n-is-value r)
    progress {App Add e v} {s} (op+ t t₁) all-locs | inj₂ (e′ , s′ , r) | _ = inj₂ (App Add e′ v , s′ , op1 r)
    progress {App GTEQ e e₁} {s} (op≥ t t₁) all-locs with progress {e} {s} t all-locs | progress {e₁} {s} t₁ all-locs
    progress {App GTEQ (Int n) (Int m)} {s} (op≥ t t₁) all-locs | inj₁ n-is-value | inj₁ m-is-value = inj₂ (Boolean ⌊ n ≥? m ⌋ , s , op≥)
    progress {App GTEQ v e₁} {s} (op≥ t t₁) all-locs | inj₁ n-is-value | inj₂ (e′ , s′ , r) = inj₂ (App GTEQ v e′ , s′ , op2 n-is-value r)
    progress {App GTEQ e v} {s} (op≥ t t₁) all-locs | inj₂ (e′ , s′ , r) | _ = inj₂ (App GTEQ e′ v , s′ , op1 r)
    progress {If e Then e₁ Else e₂} {s} (if t t₁ t₂) all-locs with progress {e} {s} t all-locs
    progress {If (Boolean true)  Then e₁ Else e₂} {s} (if t t₁ t₂) all-locs | inj₁ b-is-value = inj₂ (e₁ , s , if1)
    progress {If (Boolean false) Then e₁ Else e₂} {s} (if t t₁ t₂) all-locs | inj₁ b-is-value = inj₂ (e₂ , s , if2)
    progress {If e Then e₁ Else e₂} {s} (if t t₁ t₂) all-locs | inj₂ (e′ , s′ , r) = inj₂ (If e′ Then e₁ Else e₂ , s′ , if3 r)
    progress {Seq e e₁} {s} (seq t t₁) all-locs with progress {e} {s} t all-locs
    progress {Seq Skip e₁} {s} (seq t t₁) all-locs | inj₁ skip-is-value = inj₂ (e₁ , s , seq1)
    progress {Seq e e₁} {s} (seq t t₁) all-locs | inj₂ (e′ , s′ , r) = inj₂ (Seq e′ e₁ , s′ , seq2 r)
    progress {Assign l e} {s} (assign l-in-Γ t) all-locs with progress {e} {s} t all-locs
    progress {Assign l (Int n)} {s} (assign l-in-Γ t) all-locs | inj₁ n-is-value = inj₂ ((Skip , (l , n) ∷ s , assign1 (all-locs l-in-Γ)))
    progress {Assign l e} {s} (assign l-in-Γ t) all-locs | inj₂ (e′ , s′ , r) = inj₂ (Assign l e′ , s′ , assign2 r)
    progress {Deref l} {s} (deref l-in-Γ) all-locs = inj₂ ((Int (get l s) , s , deref (all-locs l-in-Γ)))
    progress {While e Do e₁} {s} (while t t₁) _ = inj₂ (If e Then (Seq e₁ (While e Do e₁)) Else Skip , s , while)
    
    type-uniqueness : {e : L1} {Γ : Context} {T T′ : Type} 
        → Γ ⊢ e ꞉ T → Γ ⊢ e ꞉ T′ → T ≡ T′
    type-uniqueness {Int n} int int = refl
    type-uniqueness {Boolean n} bool bool = refl
    type-uniqueness {App Add e e₁} (op+ _ _) (op+ _ _) = refl
    type-uniqueness {App GTEQ e e₁} (op≥ _ _) (op≥ _ _) = refl
    type-uniqueness {If e Then e₁ Else e₂} (if _ b _) (if _ b′ _) = type-uniqueness b b′
    type-uniqueness {Skip} skip skip = refl
    type-uniqueness {Seq e e₁} (seq _ b) (seq _ b′) = type-uniqueness b b′
    type-uniqueness {Assign l e} (assign _ _) (assign _ _) = refl
    type-uniqueness {Deref l} (deref _) (deref _) = refl
    type-uniqueness {While e₁ Do e₂} (while _ _) (while _ _) = refl

    type-preservation : {e e′ : L1} {Γ : Context} {T : Type} {s s′ : Store}
        → Γ ⊢ e ꞉ T → all-locations Γ s → (⟨ e , s ⟩ ⟶ ⟨ e′ , s′ ⟩) 
        → (Γ ⊢ e′ ꞉ T) × (all-locations Γ s′)
    type-preservation {App Add (Int n) (Int m)} (op+ _ _) all-locs op+ = int , all-locs
    type-preservation {App GTEQ (Int n) (Int m)} (op≥ _ _) all-locs op≥ = bool , all-locs
    type-preservation {App Add e e₁} (op+ t t₁) all-locs (op1 r) with type-preservation t all-locs r 
    ... | (t′ , all-locs′) = op+ t′ t₁ , all-locs′
    type-preservation {App GTEQ e e₁} (op≥ t t₁) all-locs (op1 r) with type-preservation t all-locs r 
    ... | (t′ , all-locs′) = op≥ t′ t₁ , all-locs′
    type-preservation {App Add v e₁} (op+ t t₁) all-locs (op2 v-is-value r) with type-preservation t₁ all-locs r 
    ... | (t₁′ , all-locs′) = op+ t t₁′ , all-locs′
    type-preservation {App GTEQ v e₁} (op≥ t t₁) all-locs (op2 v-is-value r) with type-preservation t₁ all-locs r
    ... | (t₁′ , all-locs′) = op≥ t t₁′ , all-locs′
    type-preservation {If (Boolean true) Then e₁ Else e₂} (if t t₁ t₂) all-locs if1 = t₁ , all-locs
    type-preservation {If (Boolean false) Then e₁ Else e₂} (if t t₁ t₂) all-locs if2 = t₂ , all-locs
    type-preservation {If e Then e₁ Else e₂} (if t t₁ t₂) all-locs (if3 r) with type-preservation t all-locs r
    ... | (t′ , all-locs′) = if t′ t₁ t₂ , all-locs′
    type-preservation {Seq Skip e₁} (seq t t₁) all-locs seq1 = t₁ , all-locs
    type-preservation {Seq e e₁} (seq t t₁) all-locs (seq2 r) with type-preservation t all-locs r
    ... | (t′ , all-locs′) = seq t′ t₁ , all-locs′
    type-preservation {Assign l (Int n)} (assign {Γ} locs t) all-locs (assign1 {.l} {n} {s} _) = skip , all-locations-weaken {Γ} {s} {n} l all-locs
    type-preservation {Assign l e} (assign locs t) all-locs (assign2 r) with type-preservation t all-locs r 
    ... | (t′ , all-locs′) = assign locs t′ , all-locs′
    type-preservation {Deref l} (deref Γ-locs) all-locs (deref s-locs) = int , all-locs
    type-preservation {While e Do e₁} (while t t₁) all-locs while = if t (seq t₁ (while t t₁)) skip , all-locs

    -- Explicit typing rule inversions (used for type inference proof)

    op+-inv₁ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ App Add e e₁ ꞉ T → Γ ⊢ e ꞉ int
    op+-inv₁ (op+ t _) = t

    op+-inv₂ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ App Add e e₁ ꞉ T → Γ ⊢ e₁ ꞉ int
    op+-inv₂ (op+ _ t) = t

    op≥-inv₁ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ App GTEQ e e₁ ꞉ T → Γ ⊢ e ꞉ int
    op≥-inv₁ (op≥ t _) = t

    op≥-inv₂ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ App GTEQ e e₁ ꞉ T → Γ ⊢ e₁ ꞉ int
    op≥-inv₂ (op≥ _ t) = t

    if-inv₁ : {e e₁ e₂ : L1} {Γ : Context} {T : Type} → Γ ⊢ If e Then e₁ Else e₂ ꞉ T → Γ ⊢ e ꞉ bool
    if-inv₁ (if t _ _) = t

    if-inv₂ : {e e₁ e₂ : L1} {Γ : Context} {T : Type} → Γ ⊢ If e Then e₁ Else e₂ ꞉ T → Γ ⊢ e₁ ꞉ T
    if-inv₂ (if _ t _) = t

    if-inv₃ : {e e₁ e₂ : L1} {Γ : Context} {T : Type} → Γ ⊢ If e Then e₁ Else e₂ ꞉ T → Γ ⊢ e₂ ꞉ T
    if-inv₃ (if _ _ t) = t

    seq-inv₁ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ Seq e e₁ ꞉ T → Γ ⊢ e ꞉ unit
    seq-inv₁ (seq t _) = t

    seq-inv₂ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ Seq e e₁ ꞉ T → Γ ⊢ e₁ ꞉ T
    seq-inv₂ (seq _ t) = t

    assign-inv₁ : {e : L1} {Γ : Context} {l : Loc} {T : Type} → Γ ⊢ Assign l e ꞉ T → Γ-contains l Γ
    assign-inv₁ (assign l∈Γ _) = l∈Γ

    assign-inv₂ : {e : L1} {Γ : Context} {l : Loc} {T : Type} → Γ ⊢ Assign l e ꞉ T → Γ ⊢ e ꞉ int
    assign-inv₂ (assign _ t) = t

    deref-inv : {Γ : Context} {l : Loc} {T : Type} → Γ ⊢ Deref l ꞉ T → Γ-contains l Γ
    deref-inv (deref l∈Γ) = l∈Γ

    while-inv₁ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ While e Do e₁ ꞉ T → Γ ⊢ e ꞉ bool
    while-inv₁ (while t _) = t

    while-inv₂ : {e e₁ : L1} {Γ : Context} {T : Type} → Γ ⊢ While e Do e₁ ꞉ T → Γ ⊢ e₁ ꞉ unit
    while-inv₂ (while _ t) = t

    -- Decidability of type inference - the below provides a type inference algorithm and 
    -- simultaneously proves it correct by returning a derivation tree alongside the inferred type,
    -- or shows that a derivation tree cannot exist for any T
    is-typeable? : (Γ : Context) (e : L1) → Dec (Σ[ T ∈ Type ] Γ ⊢ e ꞉ T)
    is-typeable? Γ (Int n) = yes (int , int)
    is-typeable? Γ (Boolean b) = yes (bool , bool)
    is-typeable? Γ (App Add e e₁) with is-typeable? Γ e | is-typeable? Γ e₁
    is-typeable? Γ (App Add e e₁) | yes (T , t) | yes (T′ , t′) with T ≟ᵗ int | T′ ≟ᵗ int
    is-typeable? Γ (App Add e e₁) | yes (T , t) | yes (T′ , t′) | yes refl   | yes refl    = yes (int , op+ t t′)
    is-typeable? Γ (App Add e e₁) | yes (T , t) | _             | no ¬e-int  | _           = no (λ (T , r) → ¬e-int (type-uniqueness t (op+-inv₁ r)))
    is-typeable? Γ (App Add e e₁) | _           | yes (T′ , t′) | _          | no ¬e₁-int  = no (λ (T , r) → ¬e₁-int (type-uniqueness t′ (op+-inv₂ r)))
    is-typeable? Γ (App Add e e₁) | no ¬e-typeable | _               = no (λ (_ , t) → ¬e-typeable (int , op+-inv₁ t))
    is-typeable? Γ (App Add e e₁) | _              | no ¬e₁-typeable = no (λ (_ , t) → ¬e₁-typeable (int , op+-inv₂ t))
    is-typeable? Γ (App GTEQ e e₁) with is-typeable? Γ e | is-typeable? Γ e₁
    is-typeable? Γ (App GTEQ e e₁) | yes (T , t) | yes (T′ , t′) with T ≟ᵗ int | T′ ≟ᵗ int
    is-typeable? Γ (App GTEQ e e₁) | yes (T , t) | yes (T′ , t′) | yes refl   | yes refl    = yes (bool , op≥ t t′)
    is-typeable? Γ (App GTEQ e e₁) | yes (T , t) | _             | no ¬e-int  | _           = no (λ (T , r) → ¬e-int (type-uniqueness t (op≥-inv₁ r)))
    is-typeable? Γ (App GTEQ e e₁) | _           | yes (T′ , t′) | _          | no ¬e₁-int  = no (λ (T , r) → ¬e₁-int (type-uniqueness t′ (op≥-inv₂ r)))
    is-typeable? Γ (App GTEQ e e₁) | no ¬e-typeable | _ = no (λ (_ , t) → ¬e-typeable (int , op≥-inv₁ t))
    is-typeable? Γ (App GTEQ e e₁) | _ | no ¬e₁-typeable = no (λ (_ , t) → ¬e₁-typeable (int , op≥-inv₂ t))
    is-typeable? Γ (If e Then e₁ Else e₂) with is-typeable? Γ e | is-typeable? Γ e₁ | is-typeable? Γ e₂
    is-typeable? Γ (If e Then e₁ Else e₂) | yes (T , t) | yes (T₁ , t₁) | yes (T₂ , t₂) with T ≟ᵗ bool | T₁ ≟ᵗ T₂
    is-typeable? Γ (If e Then e₁ Else e₂) | yes (T , t) | yes (T₁ , t₁) | yes (T₂ , t₂) | yes refl   | yes refl  = yes (T₁ , if t t₁ t₂)
    is-typeable? Γ (If e Then e₁ Else e₂) | yes (T , t) | yes (T₁ , t₁) | yes (T₂ , t₂) | no ¬e-bool | _         = no (λ (T , r) → ¬e-bool (type-uniqueness t (if-inv₁ r)))
    is-typeable? Γ (If e Then e₁ Else e₂) | yes (T , t) | yes (T₁ , t₁) | yes (T₂ , t₂) | _          | no ¬T₁≡T₂ = no (λ (T , r) → ¬T₁≡T₂ (trans (type-uniqueness t₁ (if-inv₂ r)) (sym (type-uniqueness t₂ (if-inv₃ r)))))
    is-typeable? Γ (If e Then e₁ Else e₂) | no ¬e-typeable  | _ | _ = no (λ (_ , t) → ¬e-typeable (bool , if-inv₁ t))
    is-typeable? Γ (If e Then e₁ Else e₂) | _ | no ¬e₁-typeable | _ = no (λ (T , t) → ¬e₁-typeable (T , if-inv₂ t))
    is-typeable? Γ (If e Then e₁ Else e₂) | _ | _ | no ¬e₂-typeable = no (λ (T , t) → ¬e₂-typeable (T , if-inv₃ t))
    is-typeable? Γ Skip = yes (unit , skip)
    is-typeable? Γ (Seq e e₁) with is-typeable? Γ e | is-typeable? Γ e₁
    is-typeable? Γ (Seq e e₁) | yes (T , t) | yes (T′ , t′) with T ≟ᵗ unit
    is-typeable? Γ (Seq e e₁) | yes (T , t) | yes (T′ , t′) | yes refl   = yes (T′ , seq t t′) 
    is-typeable? Γ (Seq e e₁) | yes (T , t) | _             | no ¬e-unit = no (λ (T , r) → ¬e-unit (type-uniqueness t (seq-inv₁ r)))
    is-typeable? Γ (Seq e e₁) | no ¬e-typeable | _               = no (λ (_ , t) → ¬e-typeable (unit , seq-inv₁ t))
    is-typeable? Γ (Seq e e₁) | _              | no ¬e₁-typeable = no (λ (T , t) → ¬e₁-typeable (T , seq-inv₂ t))
    is-typeable? Γ (Assign l e) with is-typeable? Γ e
    is-typeable? Γ (Assign l e) | yes (T , t) with T ≟ᵗ int | Γ-contains? l Γ
    is-typeable? Γ (Assign l e) | yes (T , t) | yes refl   | yes l∈Γ = yes (unit , assign l∈Γ t)
    is-typeable? Γ (Assign l e) | yes (T , t) | no ¬e-unit | _       = no (λ (T , r) → ¬e-unit (type-uniqueness t (assign-inv₂ r)))
    is-typeable? Γ (Assign l e) | yes (T , t) | _          | no ¬l∈Γ = no (λ (T , r) → ¬l∈Γ (assign-inv₁ r))
    is-typeable? Γ (Assign l e) | no ¬e-typeable = no (λ (_ , t) → ¬e-typeable (int , assign-inv₂ t))
    is-typeable? Γ (Deref l) with Γ-contains? l Γ
    is-typeable? Γ (Deref l) | yes l∈Γ = yes (int , deref l∈Γ)
    is-typeable? Γ (Deref l) | no ¬l∈Γ = no (λ (_ , t) → ¬l∈Γ (deref-inv t))
    is-typeable? Γ (While e Do e₁) with is-typeable? Γ e | is-typeable? Γ e₁
    is-typeable? Γ (While e Do e₁) | yes (T , t) | yes (T′ , t′) with T ≟ᵗ bool | T′ ≟ᵗ unit
    is-typeable? Γ (While e Do e₁) | yes (T , t) | yes (T′ , t′) | yes refl   | yes refl   = yes (unit , while t t′)
    is-typeable? Γ (While e Do e₁) | yes (T , t) | yes (T′ , t′) | no ¬e-bool | _          = no (λ (T , r) → ¬e-bool (type-uniqueness t (while-inv₁ r)))
    is-typeable? Γ (While e Do e₁) | yes (T , t) | yes (T′ , t′) | _          | no ¬e-unit = no (λ (T , r) → ¬e-unit (type-uniqueness t′ (while-inv₂ r)))
    is-typeable? Γ (While e Do e₁) | no ¬e-typeable | _ = no (λ (_ , t) → ¬e-typeable (bool , while-inv₁ t))
    is-typeable? Γ (While e Do e₁) | _ | no ¬e₁-typeable = no (λ (_ , t) → ¬e₁-typeable (unit , while-inv₂ t))

    -- Decidability of type checking - provides an algorithm for type checking, that returns
    -- a derivation tree if the program type checks, or a proof that the derivation tree cannot
    -- exist otherwise
    type-checks? : (Γ : Context) (e : L1) (T : Type) → Dec (Γ ⊢ e ꞉ T)
    type-checks? Γ e T with is-typeable? Γ e
    type-checks? Γ e T | yes (T′ , t) with T ≟ᵗ T′
    type-checks? Γ e T | yes (T′ , t) | yes refl = yes t
    type-checks? Γ e T | yes (T′ , t) | no ¬T≡T′ = no (λ t′ → ¬T≡T′ (type-uniqueness t′ t))
    type-checks? Γ e T | no ¬e-typeable = no (λ t → ¬e-typeable (T , t))
    
    -- ==== ⟶* PROOFS ====

    -- n-step reduction relation, used to define the reflexive-transitive closure of ⟶
    data _[_]⟶_ : Config → ℕ → Config → Set where
        refl⟶* : {e : L1} {s : Store} → ⟨ e , s ⟩ [ 0 ]⟶ ⟨ e , s ⟩
        trans⟶* : {e e′ e″ : L1} {s s′ s″ : Store} {n : ℕ} 
            → ⟨ e , s ⟩ [ n ]⟶ ⟨ e′ , s′ ⟩ 
            → ⟨ e′ , s′ ⟩ ⟶ ⟨ e″ , s″ ⟩
            → ⟨ e , s ⟩ [ suc n ]⟶ ⟨ e″ , s″ ⟩

    -- The reflexive-transitive closure of ⟶
    _⟶*_ : Config → Config → Set
    c ⟶* c′ = Σ[ k ∈ ℕ ] c [ k ]⟶ c′


    -- Proof of type safety via mathematical induction

    -- First a lemma - essentially the reflexive-transitive closure of the type-preservation property
    type-preservation* : {e e′ : L1} {Γ : Context} {T : Type} {s s′ : Store}
        → Γ ⊢ e ꞉ T → all-locations Γ s → (⟨ e , s ⟩ ⟶* ⟨ e′ , s′ ⟩) 
        → (Γ ⊢ e′ ꞉ T) × (all-locations Γ s′)
    type-preservation* t all-locs (0 , refl⟶*) = t , all-locs
    type-preservation* t all-locs (suc n , trans⟶* rs r) with type-preservation* t all-locs (n , rs)
    ... | t′ , all-locs′ = type-preservation t′ all-locs′ r
    
    -- Then we show type safety holds after n ⟶-steps...
    n-step-type-safety : {e e′ : L1} {s s′ : Store} {Γ : Context} {T : Type} 
        → (n : ℕ)
        → (Γ ⊢ e ꞉ T) → all-locations Γ s → (⟨ e , s ⟩ [ n ]⟶ ⟨ e′ , s′ ⟩) 
        → (isValue e′) ⊎ (Σ[ e″ ∈ L1 ] Σ[ s″ ∈ Store ] ⟨ e′ , s′ ⟩ ⟶ ⟨ e″ , s″ ⟩)
    n-step-type-safety zero t all-locs refl⟶* = progress t all-locs
    n-step-type-safety {e} {e′} {s} {s′} (suc n) t all-locs (trans⟶* rs r) with n-step-type-safety n t all-locs rs | type-preservation* t all-locs (n , rs)
    ... | inj₁ middle-e-is-value | _ = absurd (value-cannot-reduce middle-e-is-value (e′ , s′ , r))
    ... | _ | t′ , all-locs′ = let (t″ , all-locs″) = type-preservation t′ all-locs′ r in progress t″ all-locs″
 
    -- ... which, since n is arbitrary, gives us type safety as a corollary.
    type-safety : {e e′ : L1} {s s′ : Store} {Γ : Context} {T : Type}
        → (Γ ⊢ e ꞉ T) → all-locations Γ s →  (⟨ e , s ⟩ ⟶* ⟨ e′ , s′ ⟩) 
        → (isValue e′) ⊎ (Σ[ e″ ∈ L1 ] Σ[ s″ ∈ Store ] ⟨ e′ , s′ ⟩ ⟶ ⟨ e″ , s″ ⟩)
    type-safety t all-locs (n , r) = n-step-type-safety n t all-locs r

    -- Bonus lemma: if you have a reduction path ⟨ e , s ⟩ ⟶* ⟨ e′ , s′ ⟩ where e is a value, then
    -- the path is necessarily refl⟶* (i.e. it is 0 ⟶-steps long)

    -- To prove this, we need a lemma that is completely obvious on paper, but is often required 
    -- when dealing with equality in Agda:
    transport : {A : Set}{a b : A} → (P : A → Set) → (p : a ≡ b) → P a → P b
    transport P refl x = x

    value-reduction-is-refl⟶* : {e e′ : L1} {s s′ : Store} → isValue e 
        → (⟨ e , s ⟩ ⟶* ⟨ e′ , s′ ⟩) → (e ≡ e′) × (s ≡ s′)
    value-reduction-is-refl⟶* v-is-value (0 , refl⟶*) = refl , refl
    value-reduction-is-refl⟶* e-is-value ((suc 0) , trans⟶* {e} {_} {e′} {s} {_} {s′} refl⟶* r) = absurd (value-cannot-reduce e-is-value (e′ , (s′ , r)))
    value-reduction-is-refl⟶* e-is-value ((suc (suc n)) , trans⟶* {e} {e′} {e″} {s} {s′} {s″} t r) with value-reduction-is-refl⟶* e-is-value (suc n , t)
    ... | (p , _)= absurd (value-cannot-reduce (transport isValue p e-is-value) (e″ , s″ , r))