# Library CoLoR.Term.SimpleType.TermsSubst

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
Operation of substitution for simple typed lambda-calculus is defined in this file.

Set Implicit Arguments.

Module TermsSubst (Sig : TermsSig.Signature).

Module Export TC := TermsConv.TermsConv Sig.

Notation "{x/ N }" := (Some N::nil).
Notation "{x/ N ,y/ M }" := (Some N::Some M::nil).

Definition varSubstTo (G: Subst) x T : Prop := nth_error G x = Some (Some T).
Notation "G |-> x / T" := (varSubstTo G x T) (at level 50, x at level 0).

Definition varIsSubst (G: Subst) x : Type := {T: Term | G |-> x/T}.
Notation "G |-> x /*" := (varIsSubst G x) (at level 50, x at level 0).

Definition varIsNotSubst (G: Subst) x : Prop :=
nth_error G x = None \/ nth_error G x = Some None.
Notation "G |-> x /-" := (varIsNotSubst G x) (at level 50, x at level 0).

Definition isEmptySubst G : Prop := forall x, G |-> x/- .

Definition isSingletonSubst M G : Prop :=
G |-> 0 / M /\ forall i, G |-> (S i)/- .

Lemma singletonSubst_cond M : isSingletonSubst M {x/M}.

Hint Unfold varSubstTo varIsSubst varIsNotSubst : terms.

Lemma varSubst_dec G x : {T: Term | G |-> x/T} + { G |-> x/- }.

Lemma var_notSubst_lift G x i : G |-> x/- -> (lift_subst G i) |-> x/-.

Lemma var_notSubst_lift_rev G x i : (lift_subst G i) |-> x/- -> G |-> x/- .

Lemma var_subst_lift G x i T :
G |-> x/T -> (lift_subst G i) |-> x/(lift T i).

Lemma var_subst_lift_rev G x i T :
(lift_subst G i) |-> x/T -> exists T', G |-> x/T' /\ T = lift T' i.

Lemma var_notSubst_cons G x : G |-> x/- -> (None::G) |-> (S x)/- .

Lemma var_cons_notSubst G x : (None::G) |-> (S x)/- -> G |-> x/- .

Lemma var_subst_cons G x T : G |-> x / T -> (None :: G) |-> (S x) / T.

Lemma lift_subst_app : forall G1 G2 i,
lift_subst (G1 ++ G2) i = lift_subst G1 i ++ lift_subst G2 i.

Definition subst_dom (G: Subst) : Env :=
map (fun T =>
match T with
| None => None
| Some T => Some (type T)
end) G.

Definition subst_ran (G: Subst) : Env :=
fold_left (fun E S =>
match S with
| None => E
| Some T => E [+] env T
end
) G EmptyEnv.

Definition subst_envs_comp (G: Subst) : Prop :=
forall i j Ti Tj,
G |-> i/Ti ->
G |-> j/Tj ->
env Ti [<->] env Tj.

Lemma subst_ran_single T : subst_ran {x/T} = env T.

Lemma subst_ran_single_after_empty T :
forall i, subst_ran (copy i None ++ {x/T}) = env T.

Lemma subst_envs_comp_single : forall T, subst_envs_comp {x/T}.

Lemma subst_envs_comp_singleton :
forall G T, isSingletonSubst T G -> subst_envs_comp G.

Record correct_subst (M: Term) (G: Subst) : Prop := {
envs_c: subst_envs_comp G;
dom_c: subst_dom G [<->] env M;
ran_c: subst_ran G [-] subst_dom G [<->] env M
}.

Lemma one_var_subst_correct M N :
(forall A, env M |= 0 := A -> A = type N) ->
env M [<->] env N -> correct_subst M {x/N}.

Lemma subst_dom_varNotSubst : forall G x, G |-> x/- -> subst_dom G |= x :!.

Lemma subst_dom_varNotSubst_rev :
forall G x, subst_dom G |= x :! -> G |-> x/- .

Lemma subst_dom_varSubst :
forall G x T, G |-> x/T -> subst_dom G |= x := type T.

Lemma subst_dom_varSubst_rev : forall G x A,
subst_dom G |= x := A -> exists T, G |-> x/T /\ type T = A.

Lemma subst_dom_lifted :
forall G n, subst_dom (lift_subst G n) = subst_dom G.

Lemma lifted_subst_envs_comp G n :
subst_envs_comp G -> subst_envs_comp (lift_subst G n).

Lemma subst_ran_cons_none G : subst_ran (None::G) = subst_ran G.

Lemma fold_subst_ran : forall G l
(f := fun E S => match S with Some T => E[+]env T | None => E end),
fold_left f G l = l [+] fold_left f G nil.

Lemma subst_ran_cons_some t G :
subst_ran (Some t::G) = env t [+] subst_ran G.

Lemma subst_ran_decl : forall G x A,
subst_ran G |= x := A -> exists T p, G |-> p/T /\ env T |= x := A.

Hint Rewrite subst_ran_single subst_ran_cons_none subst_ran_cons_some : terms.

Lemma subst_cons_empty G : isEmptySubst G -> isEmptySubst (None::G).

Lemma subst_tail_empty G : isEmptySubst (None::G) -> isEmptySubst G.

Hint Resolve subst_cons_empty subst_tail_empty : terms.

Lemma subst_nil_empty : isEmptySubst nil.

Lemma subst_lift_empty G i : isEmptySubst G -> isEmptySubst (lift_subst G i).

Lemma subst_lift_empty_rev G i :
isEmptySubst (lift_subst G i) -> isEmptySubst G.

Hint Resolve subst_lift_empty subst_lift_empty_rev : terms.

Lemma subst_empty_dec : forall G, {isEmptySubst G} + {~isEmptySubst G}.

Ltac prove_correct_subst :=
match goal with
| |- correct_subst ?M ?G =>
(
constructor; [
auto with terms |
autorewrite with terms datatypes using unfold decl, liftedEnv; try_solve |
destruct (subst_empty_dec G);
autorewrite with terms datatypes using unfold decl, liftedEnv; try_solve
]
)
| _ => fail "Goal is not of required shape"
end.

Lemma subst_ran_empty : forall G, isEmptySubst G -> subst_ran G = EmptyEnv.

Lemma subst_dom_Empty : forall G, isEmptySubst G -> emptyEnv (subst_dom G).

Lemma subst_ran_singleton G T : isSingletonSubst T G -> subst_ran G = env T.

Lemma subst_dom_singleton G T : isSingletonSubst T G ->
exists E, subst_dom G = Some (type T) :: E /\ emptyEnv E.

Lemma subst_dom_singleton_after_none_decl : forall i T,
subst_dom (copy i None ++ {x/T}) |= i := type T.

Lemma subst_dom_singleton_after_none_nodecl : forall i j T, i <> j ->
subst_dom (copy i None ++ {x/T}) |= j :! .

Lemma subst_ran_lifted_empty : forall G,
isEmptySubst G -> subst_ran (lift_subst G 1) = EmptyEnv.

Lemma subst_dom_lifted_Empty G :
isEmptySubst G -> emptyEnv (subst_dom (lift_subst G 1)).

Lemma subst_ran_lifted_ne : forall G, ~isEmptySubst G ->
subst_ran (lift_subst G 1) = None :: subst_ran G.

Hint Rewrite subst_ran_empty subst_ran_lifted_empty subst_ran_lifted_ne
using solve [auto with terms] : terms.

Lemma subst_ran_lifted_noDecl G : subst_ran (lift_subst G 1) |= 0 :! .

Hint Rewrite subst_ran_single subst_dom_lifted subst_ran_cons_none
subst_ran_cons_some : terms.

Fixpoint presubst_aux (P: Preterm) (l: nat) (G: Subst) : Preterm :=
match P with
| Fun _ => P
| Var i =>
match (nth_error G i) with
| Some (Some Q) => term (lift Q l)
| _ => Var i
end
| App M N => App (presubst_aux M l G) (presubst_aux N l G)
| Abs A M => Abs A (presubst_aux M (S l) (None::G) )
end.

Definition presubst P G := presubst_aux P 0 G.

Lemma subst_lift_subst_aux: forall Pt G m n,
presubst_aux Pt (m + n) G = presubst_aux Pt m (lift_subst G n).

Lemma subst_lift_subst Pt G i :
presubst_aux Pt i G = presubst Pt (lift_subst G i).

Lemma subst_type_comp M G x T :
correct_subst M G -> G |-> x/T -> env M |= x := type T \/ env M |= x :!.

Lemma subst_envs_comp_tail a G : subst_envs_comp (a::G) -> subst_envs_comp G.

forall G, subst_envs_comp (Some a::G) -> env a [<->] subst_ran G.

Lemma subst_ran_component_comp : forall G x T,
G |-> x/T -> subst_envs_comp G ->
forall p A, env T |= p := A -> subst_ran G |= p := A.

Lemma subst_comp_comp_ran G x T :
G |-> x/T -> subst_envs_comp G -> env T [<->] subst_ran G.

Lemma subst_comp_env : forall G x T,
G |-> x/T -> subst_envs_comp G -> subst_ran G = subst_ran G [+] env T.

Lemma typing_in_subst_env M G (C: correct_subst M G) x T :
G |-> x/T -> subst_ran G |- term T := type T.

Lemma presubst_beyond_aux : forall Pt i j k G,
j + k >= length G -> (forall p, p < k -> G |-> p/-) ->
presubst_aux (prelift_aux j Pt k) i G = prelift_aux j Pt k.

Lemma presubst_beyond Pt i j G :
j >= length G -> presubst_aux (prelift Pt j) i G = prelift Pt j.

Lemma presubst_prelift_aux : forall M G i j,
presubst_aux (prelift_aux j M i) i (copy (i + j) None ++ lift_subst G j)
= prelift_aux j (presubst_aux M i (copy i None ++ G)) i.

Lemma presubst_prelift_comm Pt i G :
presubst (prelift Pt i) (copy i None ++ lift_subst G i)
= prelift (presubst Pt G) i.

Definition subst_aux : forall (M: Term) (G: Subst) (C: correct_subst M G),
{Q: Term | env Q = env M [-] subst_dom G [+] subst_ran G
/\ term Q = presubst (term M) G
/\ type Q = type M }.

Definition subst (M: Term) (G: Subst) (C: correct_subst M G) : Term :=
proj1_sig (subst_aux C).

Lemma subst_env M G (C: correct_subst M G) :
env (subst C) = env M [-] subst_dom G [+] subst_ran G.

Lemma subst_term M G (C: correct_subst M G) :
term (subst C) = presubst (term M) G.

Lemma subst_type M G (C: correct_subst M G) : type (subst C) = type M.

Hint Rewrite subst_env subst_term subst_type : terms.

Lemma subst_env_cont_subst_comp M G x (MG: correct_subst M G) T :
G |-> x/T -> env (subst MG) = env (subst MG) [+] env T.

Lemma subst_proof_irr M G (C1 C2: correct_subst M G) : subst C1 = subst C2.

Lemma subst_eq M M' G (MG: correct_subst M G) (MG': correct_subst M' G) :
M = M' -> subst MG = subst MG'.

Lemma subst_env_compat M G x T (MG: correct_subst M G) :
G |-> x / T -> env (subst MG) [<->] env T.

Hint Resolve presubst_aux : terms.
Hint Unfold subst presubst : terms.

Definition emptySubst : Subst := nil.

Lemma emptySubst_correct : forall M, correct_subst M emptySubst.

Lemma emptySubst_empty : isEmptySubst (emptySubst).

Lemma empty_presubst_neutral_aux : forall Pt i G,
(forall x, In x G -> x = None) -> Pt = presubst_aux Pt i G.

Lemma empty_presubst_neutral : forall Pt G,
(forall x, In x G -> x = None) -> presubst Pt G = Pt.

Lemma emptySubst_neutral : forall M S (CS: correct_subst M S),
isEmptySubst S -> subst CS = M.

Definition idSubst : forall M : Term, Subst.

Lemma idSubst_decl0 M A (M0: env M |= 0 := A) :
idSubst M = {x/buildT (TVar M0)}.

Lemma idSubst_correct M : correct_subst M (idSubst M).

Lemma idSubst_neutral_aux :
forall M n, presubst_aux (term M) n (copy n None ++ idSubst M) = term M.

Lemma idSubst_neutral M : (subst (idSubst_correct M)) ~ M.

Lemma presubst_lift_beyond : forall Pt G m n i (W := prelift_aux n Pt m),
m <= i -> m + n >= i + length G -> presubst W (copy i None ++ G) = W.

Lemma presubst_var_beyond G i x :
x >= length G -> presubst_aux (%x) i G = %x.

Lemma presubst_aux_disjoint :
forall Pt Pt_x G i k (shift := fun k G => copy k None ++ G)
(EL := shift k (lift_subst (None::G) (S k))) (ER := shift k {x/Pt_x})
(EC := shift k (Some Pt_x :: lift_subst G (S k))),
presubst_aux (presubst_aux Pt i EL) i ER = presubst_aux Pt i EC.

Lemma presubst_disjoint : forall Pt Pt_x G,
presubst (presubst Pt (lift_subst (None::G) 1)) {x/Pt_x} =
presubst Pt (Some Pt_x :: lift_subst G 1).

Lemma subst_disjoint_c M G P
(S: correct_subst M (lift_subst (None::G) 1))
(S': correct_subst (subst S) {x/P}) :
correct_subst M (Some P::lift_subst G 1).

Lemma fold_progress : forall (A B: Type) (conv: B -> A) g l (a init: A)
(f := fun r el => match el with None => r | Some e => g r (conv e) end),
(forall a b c, g (g a b) c = g a (g b c)) ->
(forall a, g a init = g init a) ->
g a (fold_left f l init) = fold_left f l (g init a).

Lemma subst_disjoint M G P
(S: correct_subst M (None :: lift_subst G 1))
(S': correct_subst (subst S) {x/P})
(Sj: correct_subst M (Some P :: lift_subst G 1)) : subst S' = subst Sj.

Lemma singleton_correct_single M P G :
correct_subst M G -> isSingletonSubst P G -> correct_subst M {x/P}.

Lemma singleton_presubst : forall M P G i j, isSingletonSubst P G ->
presubst_aux (term M) j (copy i None ++ {x/P})
= presubst_aux (term M) j (copy i None ++ G).

Lemma singleton_subst M P G
(CS: correct_subst M {x/P}) (CS': correct_subst M G) :
isSingletonSubst P G -> subst CS = subst CS'.

Lemma app_subst_app (M: Term) (Mapp: isApp M) G (CS: correct_subst M G) :
isApp (subst CS).

Lemma abs_subst_abs M (Mabs: isAbs M) G (CS: correct_subst M G) :
isAbs (subst CS).

Lemma subst_appL_c : forall (M: Term) (Mapp: isApp M) G,
correct_subst M G -> correct_subst (appBodyL Mapp) G.

Lemma subst_appR_c M (Mapp: isApp M) G :
correct_subst M G -> correct_subst (appBodyR Mapp) G.

Lemma subst_abs_c M (Mabs: isAbs M) G :
correct_subst M G -> correct_subst (absBody Mabs) (None :: lift_subst G 1).

Lemma var_subst M G (MG: correct_subst M G) : isVar M ->
{ T:Term & { x:nat | G |-> x/T & term (subst MG) = term T }}
+ { term (subst MG) = term M }.

Lemma funS_presubst M G (MG: correct_subst M G) :
isFunS M -> term (subst MG) = term M.

Lemma funS_subst M G (MG: correct_subst M G) : isFunS M -> (subst MG) ~ M.

Lemma funS_subst_funS M G (MG: correct_subst M G) :
isFunS M -> isFunS (subst MG).

Lemma app_subst M (Mapp: isApp M) G (S: correct_subst M G)
(SL : correct_subst (appBodyL Mapp) G := subst_appL_c Mapp S)
(SR : correct_subst (appBodyR Mapp) G := subst_appR_c Mapp S)
(Sapp : isApp (subst S) := app_subst_app Mapp S) :
appBodyL Sapp = subst SL /\ appBodyR Sapp = subst SR.

Lemma type_appBodyL_subst M G (MG: correct_subst M G) (Mapp: isApp M)
(MGapp: isApp (subst MG) := app_subst_app Mapp MG) :
type (appBodyL Mapp) = type (appBodyL MGapp).

Lemma abs_subst M (Mabs: isAbs M) G (S: correct_subst M G)
(Sabs : isAbs (subst S) := abs_subst_abs Mabs S)
(S' : correct_subst (absBody Mabs) (None :: lift_subst G 1)
:= subst_abs_c Mabs S) :
absType Sabs = absType Mabs /\ absBody Sabs = subst S'.

Lemma funS_headS_subst : forall M f G (MG: correct_subst M G),
term (appHead M) = ^f -> term (appHead (subst MG)) = ^f.

Lemma funS_head_subst : forall M G (MG: correct_subst M G),

Lemma funApp_subst_funApp :
forall M G (MG: correct_subst M G), isFunApp M -> isFunApp (subst MG).

Lemma appUnits_subst_c M G W i (MG: correct_subst M G) :
nth_error (appUnits M) i = Some W -> correct_subst W G.

Lemma appUnits_subst_length : forall M G (MG: correct_subst M G),
isFunS (appHead M) -> length (appUnits (subst MG)) = length (appUnits M).

Lemma appUnits_subst_rev : forall M G i W' (MG: correct_subst M G),
isFunS (appHead M) -> nth_error (appUnits (subst MG)) i = Some W' ->
exists W, exists Mi: nth_error (appUnits M) i = Some W,
W' = subst (appUnits_subst_c i MG Mi).

Lemma subst_arg : forall M Marg G (MG: correct_subst M G), isArg Marg M ->
exists MGarg, isArg MGarg (subst MG)
/\ exists MargG: correct_subst Marg G, MGarg = subst MargG.

Ltac term_ind X :=
intro X;
match goal with
| |- ?G =>
apply well_founded_ind with (R := subterm)(P := fun M: Term => G)
end;
[apply subterm_wf | idtac | trivial].

Lemma eq_term_arg_aux : forall M Marg M', isArg Marg M -> term M = term M' ->
exists M'arg, isArg M'arg M' /\ term M'arg = term Marg.

Lemma subst_arg_rev : forall M G MGarg (MG: correct_subst M G),
isArg MGarg (subst MG) ->
(exists Marg, isArg Marg M
/\ exists MGin: correct_subst Marg G, MGarg = subst MGin)
\/ (exists p T Targ, isArg Targ T /\ G |-> p / T /\ term MGarg = term Targ).

Lemma singleton_subst_activeEnv_noSubst_aux : forall M T i
(MG: correct_subst M (copy i None ++ Some T :: nil)),
activeEnv M |= i :! -> activeEnv M = activeEnv (subst MG).

Lemma singleton_subst_activeEnv_noSubst M G T (MG: correct_subst M G) :
activeEnv M |= 0 :! -> isSingletonSubst T G ->
activeEnv M = activeEnv (subst MG).

Lemma singleton_subst_term_noSubst_aux :
forall M T i (MG: correct_subst M (copy i None ++ {x/T})),
activeEnv M |= i :! -> term M = term (subst MG).

Lemma singleton_subst_term_noSubst : forall M G T (MG: correct_subst M G),
isSingletonSubst T G -> activeEnv M |= 0 :! -> term M = term (subst MG).

Lemma singleton_subst_active_aux : forall El Er El' Er' E i,
(forall j, j <> i -> env_comp_on E El j) ->
(forall j, j <> i -> env_comp_on E Er j) ->
(forall j A, j <> i -> (El |= j := A <-> El' |= j := A)) ->
(forall j A, j <> i -> (Er |= j := A <-> Er' |= j := A)) ->
El' [<->] Er' -> El |= i :! -> Er |= i :! ->
El [+] E [+] Er
[=] (initialSeg (El' [+] Er') i ++ None :: finalSeg (El' [+] Er') (S i))
[+] E.

Opaque activeEnv.

Lemma singleton_subst_activeEnv_subst_aux :
forall M T i A (MG: correct_subst M (copy i None ++ Some T :: nil)),
(activeEnv M |= i := A) ->
activeEnv (subst MG)
[=] (initialSeg (activeEnv M) i ++ None :: finalSeg (activeEnv M) (S i))
[+] activeEnv T.

Lemma singleton_subst_activeEnv_subst : forall M G T (MG: correct_subst M G),
isSingletonSubst T G -> (exists A, activeEnv M |= 0 := A) ->
activeEnv (subst MG) [=] (None :: tail (activeEnv M)) [+] activeEnv T.

Definition subst_list Ms Ns G := list_sim
(fun M N => exists MG: correct_subst M G, N = subst MG) Ms Ns.

Lemma subst_list_units : forall M G (MG: correct_subst M G),
isFunS (appHead M) -> subst_list (appUnits M) (appUnits (subst MG)) G.

Lemma subst_list_args : forall M G (MG: correct_subst M G),
isFunS (appHead M) -> subst_list (appArgs M) (appArgs (subst MG)) G.

Lemma subst_list_partialFlattening : forall M Ms G (MG: correct_subst M G),
isPartialFlattening Ms M ->
exists Ns, isPartialFlattening Ns (subst MG) /\ subst_list Ms Ns G.

End TermsSubst.