coq: implement substitutions (on type- & expr-terms)

coq/subst.v

@@ -0,0 +1,42 @@
+From Coq Require Import Strings.String.
+Require Import terms.
+
+Include Terms.
+
+Module Subst.
+
+(* scoped variable substitution in type terms *)
+Fixpoint type_subst (v:string) (n:ladder_type) (t0:ladder_type) :=
+  match t0 with
+  | type_var name => if (eqb v name) then n else t0
+  | type_abs x t => if (eqb v x) then t0 else type_abs x (type_subst v n t)
+  | type_app t1 t2 => (type_app (type_subst v n t1) (type_subst v n t2))
+  | type_fun t1 t2 => (type_fun (type_subst v n t1) (type_subst v n t2))
+  | type_rung t1 t2 => (type_rung (type_subst v n t1) (type_subst v n t2))
+  | t => t
+  end.
+
+(* scoped variable substitution, replaces free occurences of v with n in expression e *)
+Fixpoint expr_subst (v:string) (n:expr) (e0:expr) :=
+  match e0 with
+  | expr_var name => if (eqb v name) then n else e0
+  | expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
+  | expr_ty_app e t => expr_ty_app (expr_subst v n e) t
+  | expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs x t (expr_subst v n e)
+  | expr_tm_app e a => expr_tm_app (expr_subst v n e) (expr_subst v n a)
+  | expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
+  | expr_ascend t e => expr_ascend t (expr_subst v n e)
+  | expr_descend t e => expr_descend t (expr_subst v n e)
+  end.
+
+(* replace only type variables in expression *)
+Fixpoint expr_specialize (v:string) (n:ladder_type) (e0:expr) :=
+  match e0 with
+  | expr_ty_app e t => expr_ty_app (expr_specialize v n e) (type_subst v n t)
+  | expr_ascend t e => expr_ascend (type_subst v n t) (expr_specialize v n e)
+  | expr_descend t e => expr_descend (type_subst v n t) (expr_specialize v n e)
+  | e => e
+  end.
+  
+  
+End Subst.