initial definition of expand_morphisms

coq/_CoqProject

@@ -4,6 +4,7 @@ equiv.v
 subst.v
 subtype.v
 typing.v
+morph.v
 smallstep.v
 bbencode.v
 

coq/morph.v

@@ -0,0 +1,68 @@
+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.