Reduction

Set Implicit Arguments.

Require Import Coq.Program.Equality.
Require Import Definitions Lookup Sequences.

Operational Semantics


Definition resolved_path γ p :=
   v, γ p defv v .

Term-reduction relation
Reserved Notation "t1 '⟼' t2" (at level 40, t2 at level 39).

Inductive red : sta × trm sta × trm Prop :=

γ p q
―――――――――――――――――――――
γ | p γ | q
| red_resolve: γ p q,
    γ p defp q
    (γ, trm_path p) (γ, trm_path q)

γ q λ(x: T)t
―――――――――――――――――――――
γ | q ρ^λ γ | t[ρ^γ/x]
| red_app: γ p q T t,
    γ q defv (λ(T) t)
    resolved_path γ p
    (γ, trm_app q p) (γ, open_trm_p p t)

γ | q q'
―――――――――――――――――――――
γ | q p γ | q' p
| red_ctx_app1: γ p q q',
    (γ, trm_path q) (γ, trm_path q')
    (γ, trm_app q p) (γ, trm_app q' p)

γ | p p'
―――――――――――――――――――――
γ | ρ^γ p γ | ρ^γ p'
| red_ctx_app2: γ p p' q,
    resolved_path γ q
    (γ, trm_path p) (γ, trm_path p')
    (γ, trm_app q p) (γ, trm_app q p')

γ | let x = v in t γ, x = v | tˣ
| red_let_val : v t γ x,
    x # γ
    (γ, trm_let (trm_val v) t) (γ & x ¬ v, open_trm x t)

γ | let y = ρ^γ in t γ | t[p^γ/y]
| red_let_path : t γ p,
    resolved_path γ p
    (γ, trm_let (trm_path p) t) (γ, open_trm_p p t)

γ | t0 γ' | t0'
―――――――――――――――――――――――――――――――――――――――――――――――
γ | let x = t0 in t γ' | let x = t0' in t
| red_let_tgt : t0 t γ t0' γ',
    (γ, t0) (γ', t0')
    (γ, trm_let t0 t) (γ', trm_let t0' t)

γ p ν[q.A](x: T)ds
γ q ⤳* ρ^γ
―――――――――――――――――――――
γ | case p of y: (ρ^γ).A y t1 else t2 γ | t1[p/y]
| red_case_match : γ p q A T ds r t1 t2,
    resolved_path γ r
    γ p defv (ν[qA](T)ds)
    γ defp (open_path_p p q) ⤳* defp r
    (γ, trm_case p r A t1 t2) (γ, open_trm_p p t1)

γ p ν[q.A₁](x: T)ds
γ q ⤳* ρ^γ
ρ ρ A₁ A₂
―――――――――――――――――――――
γ | case p of y: ^γ).A₂ y t1 else t2 γ | t2
| red_case_else : γ p q A1 A2 T ds r1 r2 t1 t2,
    resolved_path γ r1
    resolved_path γ r2
    γ p defv (ν[q A1](T)ds)
    γ defp (open_path_p p q) ⤳* defp r1
    (r1 r2 A1 A2)
    (γ, trm_case p r2 A2 t1 t2) (γ, t2)

γ p λ(x: T)t
―――――――――――――――――――――
γ | case p of y: r.A y t1 else t2 γ | t2
| red_case_lambda : γ p t T r A t1 t2,
    γ p defv (λ(T) t)
    (γ, trm_case p r A t1 t2) (γ, t2)

γ p p'
―――――――――――――――――――――
γ | case p of y: r.A y t1 else t2 γ | case p' of tag r.A y t1 else t2
| red_ctx_case1 : γ p p' r A t1 t2,
    (γ, trm_path p) (γ, trm_path p')
    (γ, trm_case p r A t1 t2) (γ, trm_case p' r A t1 t2)

γ r r'
―――――――――――――――――――――
γ | case ρ^λ of y: r'.A y t1 else t2 γ | case ρ^γ of tag r'.A y t1 else t2
| red_ctx_case2 : γ p r r' A t1 t2,
    resolved_path γ p
    (γ, trm_path r) (γ, trm_path r')
    (γ, trm_case p r A t1 t2) (γ, trm_case p r' A t1 t2)

where "t1 '⟼' t2" := (red t1 t2).

Reflexive, transitive closure of reduction relation
Notation "t1 '⟼*' t2" := (star red t1 t2) (at level 40).

Normal forms

Paths and values are considered to be in normal form.
Inductive norm_form: sta trm Prop :=
| nf_path: γ p, ( v, γ p defv v ) norm_form γ (trm_path p)
| nf_val: γ v, norm_form γ (trm_val v).

Hint Constructors red norm_form.