Reduction
Set Implicit Arguments.
Require Import Coq.Program.Equality.
Require Import Definitions Lookup Sequences.
Require Import Coq.Program.Equality.
Require Import Definitions Lookup Sequences.
Term-reduction relation
Reserved Notation "t1 '⟼' t2" (at level 40, t2 at level 39).
Inductive red : sta × trm → sta × trm → Prop :=
Inductive red : sta × trm → sta × trm → Prop :=
γ ⊢ p ⤳ q
―――――――――――――――――――――
γ | p ⟼ γ | q
―――――――――――――――――――――
γ | p ⟼ γ | q
γ ⊢ q ⤳ λ(x: T)t
―――――――――――――――――――――
γ | q ρ^λ ⟼ γ | t[ρ^γ/x]
―――――――――――――――――――――
γ | 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 ⤳ defv (λ(T) t) ⟧ →
resolved_path γ p →
(γ, trm_app q p) ⟼ (γ, open_trm_p p t)
γ | q ⟼ q'
―――――――――――――――――――――
γ | q p ⟼ γ | q' p
―――――――――――――――――――――
γ | q p ⟼ γ | q' p
| red_ctx_app1: ∀ γ p q q',
(γ, trm_path q) ⟼ (γ, trm_path q') →
(γ, trm_app q p) ⟼ (γ, trm_app q' p)
(γ, trm_path q) ⟼ (γ, trm_path q') →
(γ, trm_app q p) ⟼ (γ, trm_app q' p)
γ | p ⟼ 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')
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ˣ
γ | let y = ρ^γ in t ⟼ γ | t[p^γ/y]
γ | t0 ⟼ γ' | t0'
―――――――――――――――――――――――――――――――――――――――――――――――
γ | let x = t0 in t ⟼ γ' | let x = t0' in t
―――――――――――――――――――――――――――――――――――――――――――――――
γ | let x = t0 in t ⟼ γ' | let x = t0' in t
γ ⊢ p ⤳ ν[q.A](x: T)ds
γ ⊢ q ⤳* ρ^γ
―――――――――――――――――――――
γ | case p of y: (ρ^γ).A y ⇒ t1 else t2 ⟼ γ | t1[p/y]
γ ⊢ 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 (ν[q↘A](T)ds) ⟧ →
γ ⟦ defp (open_path_p p q) ⤳* defp r ⟧ →
(γ, trm_case p r A t1 t2) ⟼ (γ, open_trm_p p t1)
resolved_path γ r →
γ ⟦ p ⤳ defv (ν[q↘A](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
γ ⊢ 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)
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
―――――――――――――――――――――
γ | 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 ⤳ 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
―――――――――――――――――――――
γ | 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)
(γ, 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
―――――――――――――――――――――
γ | 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).
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