Library CoLoR.Term.SimpleType.TermsSubst

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
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.

  Lemma subst_envs_comp_head a :
    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),
      isFunS (appHead M) -> isFunS (appHead (subst MG)).

  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.