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 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,
|
||
expr_lc [{ Λ e }] ->
|
||
is_value [{ Λ e }]
|
||
|
||
| V_Abs : forall σ e,
|
||
expr_lc [{ λ σ ↦ 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,
|
||
(expr_lc 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',
|
||
expr_lc [{ Λ e }] ->
|
||
e -->eval e' ->
|
||
[{ Λ e }] -->eval [{ Λ e' }]
|
||
|
||
| E_TypAppLam : forall e τ,
|
||
expr_lc [{ (Λ e ) }] ->
|
||
[{ (Λ e) # τ }] -->eval (expr_open_type τ e)
|
||
|
||
| E_AppLam : forall τ e a,
|
||
expr_lc [{ (λ τ ↦ e) }] ->
|
||
[{ (λ τ ↦ e) a }] -->eval (expr_open a e)
|
||
|
||
| E_AppMorph : forall τ e a,
|
||
expr_lc [{ (λ τ ↦morph e) }] ->
|
||
[{ (λ τ ↦morph e) a }] -->eval (expr_open a e)
|
||
|
||
| E_Let : forall e a,
|
||
expr_lc [{ let a in e }] ->
|
||
[{ let a in e }] -->eval (expr_open a 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).
|