68 lines
No EOL
1.7 KiB
Coq
68 lines
No EOL
1.7 KiB
Coq
From Coq Require Import Strings.String.
|
||
Require Import terms.
|
||
Require Import subst.
|
||
Require Import equiv.
|
||
Require Import subtype.
|
||
Require Import typing.
|
||
|
||
Include Terms.
|
||
Include Subst.
|
||
Include Equiv.
|
||
Include Subtype.
|
||
Include Typing.
|
||
|
||
Module Morph.
|
||
|
||
|
||
Reserved Notation "Γ '|-' '[[' e ']]' '=' t" (at level 101, e at next level, t at level 0).
|
||
|
||
Inductive expand_morphisms : context -> expr_term -> expr_term -> Prop :=
|
||
|
||
| Expand_Transform : forall Γ e h τ τ',
|
||
(context_contains Γ h (type_morph τ τ')) ->
|
||
(Γ |- e \is τ) ->
|
||
(Γ |- [[ e ]] = (expr_app (expr_var h) e))
|
||
|
||
| Expand_Otherwise : forall Γ e,
|
||
(Γ |- [[ e ]] = e)
|
||
|
||
| Expand_App : forall Γ f f' a a' σ τ,
|
||
(Γ |- f \compatible (type_fun σ τ)) ->
|
||
(Γ |- a \compatible σ) ->
|
||
(Γ |- [[ f ]] = f') ->
|
||
(Γ |- [[ a ]] = a') ->
|
||
(Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
|
||
|
||
where "Γ '|-' '[[' e ']]' '=' t" := (expand_morphisms Γ e t).
|
||
|
||
|
||
(* For every well-typed term, there is an expanded exactly typed term *)
|
||
Lemma well_typed_is_expandable :
|
||
forall (e:expr_term),
|
||
(is_well_typed e) ->
|
||
exists Γ e', (expand_morphisms Γ e e') -> (is_exactly_typed e')
|
||
.
|
||
Proof.
|
||
Admitted.
|
||
|
||
|
||
Example expand1 :
|
||
(ctx_assign "morph-radix"
|
||
[< <%"PosInt"% %"16"%> ->morph <%"PosInt"% %"10"%> >]
|
||
(ctx_assign "fn-decimal"
|
||
[< <%"PosInt"% %"10"%> -> <%"PosInt"% %"10"%> >]
|
||
(ctx_assign "x"
|
||
[< <%"PosInt"% %"16"%> >]
|
||
ctx_empty)))
|
||
|
||
|- [[ (expr_app (expr_var "fn-decimal") (expr_var "x")) ]]
|
||
|
||
= (expr_app (expr_var "fn-decimal")
|
||
(expr_app (expr_var "morph-radix") (expr_var "x")))
|
||
.
|
||
Proof.
|
||
apply Expand_App with (f':=(expr_var "fn-decimal")) (σ:=[< < %"PosInt"% %"10"% > >]) (τ:=[< < %"PosInt"% %"10"% > >]).
|
||
apply TCompat_Native.
|
||
Admitted.
|
||
|
||
End Morph. |