Reduction

Set Implicit Arguments.

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

Operational Semantics

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

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

γ ⊢ q ⤳* λ(T)t
―――――――――――――――――――――
γ | q p ⟼ γ | tᵖ
| red_app: ∀ γ p q T t,
    γ ⟦ defp q ⤳* defv (λ(T) t) ⟧ →
    (γ, trm_app q p) ⟼ (γ, open_trm_p p t)

γ | 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 = p in t ⟼ γ | tᵖ
| red_let_path : ∀ t γ 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)

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: trm → Prop :=
| nf_path: ∀ p, norm_form (trm_path p)
| nf_val: ∀ v, norm_form (trm_val v).

Hint Constructors red norm_form.