add substitution & opening fixpoints for expressions

coq/terms_debruijn.v

@@ -57,17 +57,17 @@ Notation "σ '~' τ" := (ty_ladder σ τ)
   (in custom ladder_type at level 20, right associativity) : ladder_type_scope.
 Notation "'$' x" := (ty_id x%string)
   (in custom ladder_type at level 10, x constr) : ladder_type_scope.
-Notation "'%' x" := (ty_fvar x)
+Notation "'%' x" := (ty_bvar x)
   (in custom ladder_type at level 10, x constr) : ladder_type_scope.
 
 Notation "[{ e }]" := e
   (e custom ladder_expr at level 99) : ladder_expr_scope.
 Notation "e" := e
   (in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
-Notation "'$' x" := (ex_fvar x)
-  (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
 Notation "'%' x" := (ex_bvar x)
   (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
+Notation "'$' x" := (ex_fvar x)
+  (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
 Notation "'Λ' e" := (ex_ty_abs e)
   (in custom ladder_expr at level 10, e custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
 Notation "'λ' τ '↦' e" := (ex_abs τ e)
@@ -87,6 +87,19 @@ Notation "e '#' τ" := (ex_ty_app e τ)
 Notation "'(' e ')'" := e
   (in custom ladder_expr, e custom ladder_expr at next level, left associativity) : ladder_expr_scope.
 
+(* number of abstractions in a type *)
+Fixpoint type_debruijn_depth (τ:type_DeBruijn) : nat :=
+  match τ with
+  | ty_id s => 0
+  | ty_fvar s => 0
+  | ty_bvar x => 0
+  | ty_func s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  | ty_morph s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  | ty_univ t => (1 + (type_debruijn_depth t))
+  | ty_spec s t => ((type_debruijn_depth s) - 1)
+  | ty_ladder s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  end.
+
 (* get the list of all free variables in a type term *)
 Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : atoms :=
   match τ with
@@ -156,31 +169,117 @@ Inductive type_lc : type_DeBruijn -> Prop :=
   | Tlc_Ladder : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_ladder τ1 τ2)
 .
 
-(* number of abstractions *)
+(** Substitution in Expressions *)
-Fixpoint type_debruijn_depth (τ:type_DeBruijn) : nat :=
+
-  match τ with
+
-  | ty_id s => 0
+(* get the list of all free variables in an expression *)
-  | ty_fvar s => 0
+Fixpoint expr_fv (e : expr_DeBruijn) {struct e} : atoms :=
-  | ty_bvar x => 0
+  match e with
-  | ty_func s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  | ex_fvar n => singleton n
-  | ty_morph s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  | ex_bvar y => {}
-  | ty_univ t => (1 + (type_debruijn_depth t))
+  | ex_ty_abs t' => (expr_fv t')
-  | ty_spec s t => ((type_debruijn_depth s) - 1)
+  | ex_ty_app t' σ => (expr_fv t')
-  | ty_ladder s t => max (type_debruijn_depth s) (type_debruijn_depth t)
+  | ex_morph σ t' => (expr_fv t')
+  | ex_abs σ t' => (expr_fv t')
+  | ex_app t1 t2 => (expr_fv t1) `union` (expr_fv t2)
+  | ex_let t1 t2 => (expr_fv t1) `union` (expr_fv t2)
+  | ex_ascend τ t' => (expr_fv t')
+  | ex_descend τ t' => (expr_fv t')
   end.
 
-
+(* substitute free variable x with expression s in t *)
-(*
+Fixpoint ex_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
-Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
+  match t with
-  match τ with
+  | ex_fvar n => if x == n then s else t
-  | type_id s => ty_id s
+  | ex_bvar y => ex_bvar y
-  | type_var s => ty_fvar (pick fresh )
+  | ex_ty_abs t' => ex_ty_abs (ex_subst x s t')
-  | type_univ x t => let t':=(type_named2debruijn t) in (ty_univ (type_bind_fvar x 0 t'))
+  | ex_ty_app t' σ => ex_ty_app (ex_subst x s t') σ
-  | type_spec s t => ty_spec (type_named2debruijn s) (type_named2debruijn t)
+  | ex_morph σ t' => ex_morph σ (ex_subst x s t')
-  | type_fun s t => ty_func (type_named2debruijn s) (type_named2debruijn t)
+  | ex_abs σ t' => ex_abs σ (ex_subst x s t')
-  | type_morph s t => ty_morph (type_named2debruijn s) (type_named2debruijn t)
+  | ex_app t1 t2 => ex_app (ex_subst x s t1) (ex_subst x s t2)
-  | type_ladder s t => ty_ladder (type_named2debruijn s) (type_named2debruijn t)
+  | ex_let t1 t2 => ex_let (ex_subst x s t1) (ex_subst x s t2)
+  | ex_ascend τ t' => ex_ascend τ (ex_subst x s t')
+  | ex_descend τ t' => ex_descend τ (ex_subst x s t')
   end.
 
-Coercion type_named2debruijn : type_term >-> type_DeBruijn.
+(* substitute free type-variable α with type τ in e *)
-*)
+Fixpoint ex_subst_type (α:atom) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+  | ex_fvar n => ex_fvar n
+  | ex_bvar y => ex_bvar y
+  | ex_ty_abs e' => ex_ty_abs (ex_subst_type α τ e')
+  | ex_ty_app e' σ => ex_ty_app (ex_subst_type α τ e') (subst_type α τ σ)
+  | ex_morph σ e' => ex_morph (subst_type α τ σ) (ex_subst_type α τ e')
+  | ex_abs σ e' => ex_abs (subst_type α τ σ) (ex_subst_type α τ e')
+  | ex_app e1 e2 => ex_app (ex_subst_type α τ e1) (ex_subst_type α τ e2)
+  | ex_let e1 e2 => ex_let (ex_subst_type α τ e1) (ex_subst_type α τ e2)
+  | ex_ascend σ e' => ex_ascend (subst_type α τ σ) (ex_subst_type α τ e')
+  | ex_descend σ e' => ex_descend (subst_type α τ σ) (ex_subst_type α τ e')
+  end.
+
+(* replace a free variable with a new (dangling) bound variable *)
+Fixpoint expr_bind_fvar (x:atom) (n:nat) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+  | ex_fvar s => if x == s then ex_bvar n else e
+  | ex_bvar n => ex_bvar n
+  | ex_ty_abs e' => ex_ty_abs (expr_bind_fvar x n e')
+  | ex_ty_app e' σ => ex_ty_app (expr_bind_fvar x n e') σ
+  | ex_morph σ e' => ex_morph σ (expr_bind_fvar x (S n) e')
+  | ex_abs σ e' => ex_abs σ (expr_bind_fvar x (S n) e')
+  | ex_app e1 e2 => ex_app (expr_bind_fvar x n e1) (expr_bind_fvar x n e2)
+  | ex_let e1 e2 => ex_let (expr_bind_fvar x n e1) (expr_bind_fvar x n e2)
+  | ex_ascend σ e' => ex_ascend σ (expr_bind_fvar x n e')
+  | ex_descend σ e' => ex_descend σ (expr_bind_fvar x n e')
+  end.
+
+(* replace (dangling) index with another expression *)
+Fixpoint expr_open_rec (k:nat) (t:expr_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+    | ex_fvar s => ex_fvar s
+    | ex_bvar i => if k === i then t else e
+    | ex_ty_abs e' => ex_ty_abs (expr_open_rec k t e')
+    | ex_ty_app e' σ => ex_ty_app (expr_open_rec k t e') σ
+    | ex_morph σ e' => ex_morph σ (expr_open_rec (S k) t e')
+    | ex_abs σ e' => ex_abs σ (expr_open_rec (S k) t e')
+    | ex_app e1 e2 => ex_app (expr_open_rec k t e1) (expr_open_rec k t e2)
+    | ex_let e1 e2 => ex_let (expr_open_rec k t e1) (expr_open_rec k t e2)
+    | ex_ascend σ e' => ex_ascend σ (expr_open_rec k t e')
+    | ex_descend σ e' => ex_descend σ (expr_open_rec k t e')
+  end.
+
+Definition expr_open t e := expr_open_rec 0 t e.
+
+
+
+(* replace (dangling) index with another expression *)
+Fixpoint expr_open_type_rec (k:nat) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+  match e with
+    | ex_fvar s => ex_fvar s
+    | ex_bvar s => ex_bvar s
+    | ex_ty_abs e' => ex_ty_abs (expr_open_type_rec (S k) τ e')
+    | ex_ty_app e' σ => ex_ty_app (expr_open_type_rec k τ e') (type_open_rec k τ σ)
+    | ex_morph σ e' => ex_morph (type_open_rec k τ σ) (expr_open_type_rec k τ e')
+    | ex_abs σ e' => ex_abs (type_open_rec k τ σ) (expr_open_type_rec k τ e')
+    | ex_app e1 e2 => ex_app (expr_open_type_rec k τ e1) (expr_open_type_rec k τ e2)
+    | ex_let e1 e2 => ex_let (expr_open_type_rec k τ e1) (expr_open_type_rec k τ e2)
+    | ex_ascend σ e' => ex_ascend σ (expr_open_type_rec k τ e')
+    | ex_descend σ e' => ex_descend σ (expr_open_type_rec k τ e')
+  end.
+
+Definition expr_open_type τ e := expr_open_type_rec 0 τ e.
+
+
+(* is the expression locally closed ? *)
+Inductive expr_lc : expr_DeBruijn -> Prop :=
+  | Elc_Var : forall s, expr_lc (ex_fvar s)
+  | Elc_TypAbs : forall e, expr_lc e -> expr_lc (ex_ty_abs e)
+  | Elc_TypApp : forall e σ, expr_lc e -> type_lc σ -> expr_lc (ex_ty_app e σ)
+  | Elc_Abs : forall σ e1 L,
+      (type_lc σ) ->
+      (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) ->
+      expr_lc (ex_abs σ e1)
+  | Tlc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2)
+  | Tlc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2)
+  | Tlc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e)
+  | Tlc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e)
+.