ladder-calculus/coq/terms/eval.v

76 lines
1.7 KiB
Coq
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

From Coq Require Import Lists.List.
Import ListNotations.
Require Import Atom.
Require Import debruijn.
Require Import subtype.
Require Import morph.
Require Import typing.
Open Scope ladder_expr_scope.
Inductive is_value : expr_DeBruijn -> Prop :=
| V_TAbs : forall e,
is_value [{ Λ e }]
| V_Abs : forall σ e,
is_value [{ λ σ e }]
| V_Morph : forall σ e,
is_value [{ λ σ morph e }]
| V_Ascend : forall τ e,
is_value e ->
is_value [{ e as τ }]
| V_Descend : forall τ e,
is_value e ->
is_value [{ e des τ }]
.
Reserved Notation " s '-->eval' t " (at level 40).
Inductive eval : expr_DeBruijn -> expr_DeBruijn -> Prop :=
| E_App1 : forall e1 e1' e2,
e1 -->eval e1' ->
[{ e1 e2 }] -->eval [{ e1' e2 }]
| E_App2 : forall v1 e2 e2',
(is_value v1) ->
e2 -->eval e2' ->
[{ v1 e2 }] -->eval [{ v1 e2' }]
| E_TypApp : forall e e',
e -->eval e' ->
[{ Λ e }] -->eval [{ Λ e' }]
| E_TypAppLam : forall e τ,
[{ (Λ e) # τ }] -->eval (expr_open_type τ e)
| E_AppLam : forall τ e a,
[{ (λ τ e) a }] -->eval (expr_open a e)
| E_AppMorph : forall τ e a,
[{ (λ τ morph e) a }] -->eval (expr_open a e)
| E_Let : forall e a,
[{ let a in e }] -->eval (expr_open a e)
| E_StripAscend : forall τ e,
[{ e as τ }] -->eval e
| E_StripDescend : forall τ e,
[{ e des τ }] -->eval e
| E_Ascend : forall τ e e',
(e -->eval e') ->
[{ e as τ }] -->eval [{ e' as τ }]
| E_AscendCollapse : forall τ' τ e,
[{ (e as τ) as τ' }] -->eval [{ e as (τ'~τ) }]
| E_DescendCollapse : forall τ' τ e,
(τ':<=τ) ->
[{ (e des τ') des τ }] -->eval [{ e des τ }]
where "s '-->eval' t" := (eval s t).