ladder-calculus/coq/subst.v

153 lines
4.3 KiB
Coq
Raw Normal View History

From Coq Require Import Strings.String.
From Coq Require Import Lists.List.
Import ListNotations.
Require Import terms.
Fixpoint type_fv (τ : type_term) {struct τ} : (list string) :=
match τ with
| type_id s => []
| type_var α => [α]
| type_univ α τ => (remove string_dec α (type_fv τ))
| type_spec σ τ => (type_fv σ) ++ (type_fv τ)
| type_fun σ τ => (type_fv σ) ++ (type_fv τ)
| type_morph σ τ => (type_fv σ) ++ (type_fv τ)
| type_ladder σ τ => (type_fv σ) ++ (type_fv τ)
end.
Open Scope ladder_type_scope.
Example ex_type_fv1 :
(In "T"%string (type_fv [< "U",%"T"% >]))
.
Proof. simpl. left. auto. Qed.
Open Scope ladder_type_scope.
Example ex_type_fv2 :
~(In "T"%string (type_fv [< "T",%"T"% >]))
.
Proof. simpl. auto. Qed.
2024-08-07 15:59:03 +02:00
(* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) : type_term :=
match t0 with
| type_var name => if (eqb v name) then n else t0
| type_fun t1 t2 => (type_fun (type_subst v n t1) (type_subst v n t2))
| type_univ x t => if (eqb v x) then t0 else type_univ x (type_subst v n t)
| type_spec t1 t2 => (type_spec (type_subst v n t1) (type_subst v n t2))
| type_ladder t1 t2 => (type_ladder (type_subst v n t1) (type_subst v n t2))
| t => t
end.
(*
Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop :=
| TSubst_VarReplace :
(type_subst1 x σ (type_var x) σ)
| TSubst_VarKeep : forall y,
(x <> y) ->
(type_subst1 x σ (type_var y) (type_var y))
| TSubst_UnivReplace : forall y τ τ',
~(x = y) ->
~(type_var_free y σ) ->
(type_subst1 x σ τ τ') ->
(type_subst1 x σ (type_univ y τ) (type_univ y τ'))
| TSubst_Id : forall n,
(type_subst1 x σ (type_id n) (type_id n))
| TSubst_Spec : forall τ1 τ2 τ1' τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_spec τ1 τ2) (type_spec τ1' τ2'))
| TSubst_Fun : forall τ1 τ1' τ2 τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_fun τ1 τ2) (type_fun τ1' τ2'))
| TSubst_Morph : forall τ1 τ1' τ2 τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_morph τ1 τ2) (type_morph τ1' τ2'))
| TSubst_Ladder : forall τ1 τ1' τ2 τ2',
(type_subst1 x σ τ1 τ1') ->
(type_subst1 x σ τ2 τ2') ->
(type_subst1 x σ (type_ladder τ1 τ2) (type_ladder τ1' τ2'))
.
*)
Lemma type_subst_symm :
forall x y τ τ',
((type_subst x (type_var y) τ) = τ') ->
((type_subst y (type_var x) τ') = τ)
.
Proof.
intros.
induction H.
unfold type_subst.
induction τ.
reflexivity.
Admitted.
Lemma type_subst_fresh :
forall α τ u,
~ (In α (type_fv τ))
-> (type_subst α u τ) = τ
.
Proof.
intros.
unfold type_subst.
induction τ.
reflexivity.
unfold eqb.
admit.
(*
apply TSubst_Id.
apply TSubst_VarKeep.
contradict H.
rewrite H.
apply TFree_Var.
apply TSubst_Fun.
apply IHτ1.
contradict H.
apply TFree_Fun.
apply H.
apply
*)
Admitted.
(* scoped variable substitution, replaces free occurences of v with n in expression e *)
Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
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_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
| expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e)
| expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
| expr_let x a e => expr_let x (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:type_term) (e0:expr_term) :=
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.