78 lines
1.8 KiB
Coq
78 lines
1.8 KiB
Coq
|
From Coq Require Import Lists.List.
|
|||
|
|
Import ListNotations.
|
|||
|
|
Require Import Atom.
|
|||
|
|
Require Import terms_debruijn.
|
|||
|
|
Require Import subtype_debruijn.
|
|||
|
|
Require Import context_debruijn.
|
|||
|
|
Require Import morph_debruijn.
|
|||
|
|
Require Import typing_debruijn.
|
|||
|
|
|
|||
|
|
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).
|