Library CoLoR.Term.SimpleType.TermsLifting

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Operation of lifting (increasing indexes of variables) and lowering (decreasing them) on terms of simply typed lambda-calculus (which is an equivalent of renaming of variables for the representation of terms using de Bruijn indices) is defined in this file.

Set Implicit Arguments.


Module TermsLifting (Sig : TermsSig.Signature).

  Module Export TB := TermsManip.TermsManip Sig.

  Fixpoint prelift_aux (n: nat) (P: Preterm) (k: nat) : Preterm :=
    match P with
    | Fun _ => P
    | Var i =>
        match (le_gt_dec k i) with
        | left _ => Var (i + n)
        | right _ => Var i
        end
    | App M N => App (prelift_aux n M k) (prelift_aux n N k)
    | Abs A M => Abs A (prelift_aux n M (S k))
    end.
  Definition prelift P n := prelift_aux n P 0.

  Definition liftedEnv (n: nat) (E: Env) (k: nat) : Env :=
    initialSeg E k ++ copy n None ++ finalSeg E k.

  Lemma liftedEnv_next : forall A E n k,
    liftedEnv n (decl A E) (S k) = decl A (liftedEnv n E k).

  Hint Rewrite liftedEnv_next : terms.

  Lemma liftedEnv_var_lifted : forall E x A k n, E |= x := A -> x >= k ->
    liftedEnv n E k |= x + n := A.

  Lemma liftedEnv_var_notLifted : forall E x A k n,
    E |= x := A -> x < k -> liftedEnv n E k |= x := A.

  Lemma var_liftedEnv_var_lifted : forall E x A k n,
    liftedEnv n E k |= x + n := A -> x >= k -> E |= x := A.

  Lemma var_liftedEnv_var_notLifted : forall E x A k n,
    liftedEnv n E k |= x := A -> x < k -> E |= x := A.

  Hint Rewrite liftedEnv_var_lifted liftedEnv_var_notLifted
    var_liftedEnv_var_lifted var_liftedEnv_var_notLifted
    using solve [omega | auto] : terms.

  Definition lift_aux : forall (n: nat) (M: Term) (k: nat),
   {N: Term | env N = liftedEnv n (env M) k
              /\ term N = prelift_aux n (term M) k /\ type N = type M }.


  Definition lift (M: Term)(n: nat) : Term :=
    proj1_sig (lift_aux n M 0).

  Definition Subst := list (option Term).

  Definition lift_subst_comp P l :=
    match P with
    | None => None
    | Some P => Some (lift P l)
    end.

  Definition lift_subst (G: Subst)(l: nat) : Subst := map (fun T => lift_subst_comp T l) G.

  Hint Resolve prelift_aux : terms.
  Hint Unfold lift : terms.

  Lemma lift_env : forall M n, env (lift M n) = liftedEnv n (env M) 0.

  Lemma lift_term : forall M n, term (lift M n) = prelift (term M) n.

  Lemma lift_type : forall M n, type (lift M n) = type M.

  Hint Rewrite lift_env lift_term lift_type : terms.

  Lemma in_lift_subst : forall Q G i, In (Some Q) (lift_subst G i) ->
    (exists2 W, In (Some W) G & Q = lift W i).

  Lemma lift_subst_distr : forall G H i,
    lift_subst (G ++ H) i = lift_subst G i ++ lift_subst H i.

  Lemma prelift_aux_0 : forall Pt i, prelift_aux 0 Pt i = Pt.

  Lemma prelift_0 : forall Pt, prelift Pt 0 = Pt.

  Lemma lift_0 : forall (M: Term), lift M 0 = M.

  Lemma lift_subst_0 : forall (G: Subst), lift_subst G 0 = G.

  Hint Rewrite prelift_aux_0 prelift_0 lift_0 lift_subst_0 : terms.

  Lemma prelift_aux_fold_aux : forall Pt m n i j, j >= i -> j <= n + i ->
    prelift_aux m (prelift_aux n Pt i) j = prelift_aux (m + n) Pt i.

  Lemma prelift_aux_fold : forall Pt m n i,
    prelift_aux (m + n) Pt i = prelift_aux m (prelift_aux n Pt i) i.

  Lemma prelift_fold : forall Pt m n,
    prelift Pt (m + n) = prelift (prelift Pt n) m.

  Lemma lift_fold : forall Pt m n, lift Pt (m + n) = lift (lift Pt m) n.

  Lemma lift_fold_1out : forall M n, lift (lift M n) 1 = lift M (S n).

  Lemma lift_fold_1in : forall M n, lift (lift M 1) n = lift M (S n).

  Lemma lift_subst_fold : forall G m n,
    lift_subst G (m+n) = lift_subst (lift_subst G m) n.

  Hint Rewrite lift_fold lift_subst_fold : terms.

  Lemma lift_empty_subst : forall m i,
    lift_subst (copy m None) i = copy m None.

  Lemma length_lift_subst : forall G i, length (lift_subst G i) = length G.

  Hint Rewrite lift_empty_subst length_lift_subst : terms.

  Lemma nth_lift_subst_n : forall (G: Subst) i x, nth_error G x = None ->
    nth_error (lift_subst G i) x = None.

  Lemma nth_lift_subst_n_rev : forall (G: Subst) i x,
    nth_error (lift_subst G i) x = None -> nth_error G x = None.

  Lemma nth_lift_subst_sn : forall G i x, nth_error G x = Some None ->
    nth_error (lift_subst G i) x = Some None.

  Lemma nth_lift_subst_sn_rev : forall G i x,
    nth_error (lift_subst G i) x = Some None -> nth_error G x = Some None.

  Lemma nth_lift_subst_s : forall G i x T, nth_error G x = Some (Some T) ->
    nth_error (lift_subst G i) x = Some (Some (lift T i)).

  Hint Rewrite nth_lift_subst_n nth_lift_subst_n_rev nth_lift_subst_sn
    nth_lift_subst_sn_rev
    using solve [auto with terms] : terms.

  Lemma nth_lift_subst_s_rev : forall G i x T,
    nth_error (lift_subst G i) x = Some (Some T) ->
    exists T', nth_error G x = Some (Some T') /\ T = lift T' i.

  Lemma nth_lift_normal : forall G i x T,
    nth_error (lift_subst G i) x = Some (Some T) ->
    exists2 Tg, T = lift Tg i & nth_error G x = Some (Some Tg).

  Lemma app_lift_app_aux : forall M (Mapp: isApp M) n k,
    isApp (proj1_sig (lift_aux n M k)).

  Lemma app_lift_app : forall M (Mapp: isApp M) n, isApp (lift M n).

  Lemma lift_absBody : forall E Pt A B (M: decl A E |- Pt := B) n k
    (MLabs: isAbs (proj1_sig (lift_aux n (buildT (TAbs M)) k))),
    absBody MLabs = proj1_sig (lift_aux n (buildT M) (S k)).

  Lemma lift_appBodyL : forall E PtL PtR A B n k (Ml: E |- PtL := A --> B)
    (Mr: E |- PtR := A)
    (MLapp: isApp (proj1_sig (lift_aux n (buildT (TApp Ml Mr)) k))),
    appBodyL MLapp = proj1_sig (lift_aux n (buildT Ml) k).

  Lemma lift_appBodyR : forall E PtL PtR A B n k (Ml: E |- PtL := A --> B)
    (Mr: E |- PtR := A)
    (MLapp: isApp (proj1_sig (lift_aux n (buildT (TApp Ml Mr)) k))),
    appBodyR MLapp = proj1_sig (lift_aux n (buildT Mr) k).

  Lemma term_prelift_eq : forall M N i j,
    prelift_aux i M j = prelift_aux i N j -> M = N .

  Lemma terms_lift_eq : forall M N, lift M 1 = lift N 1 -> M = N.

  Fixpoint prelower_aux (P: Preterm) (k: nat) : Preterm :=
    match P with
    | Fun _ => P
    | Var i =>
        match (le_gt_dec k i) with
        | left _ => Var (pred i)
        | right _ => Var i
        end
    | App M N => App (prelower_aux M k) (prelower_aux N k)
    | Abs A M => Abs A (prelower_aux M (S k))
    end.
  Definition prelower P := prelower_aux P 0.

  Definition loweredEnv (E: Env) (k: nat) : Env :=
    initialSeg E k ++ finalSeg E (S k).

  Lemma loweredEnv_var_lowered : forall E x A k,
    E |= k :! -> E |= x := A -> k <= x -> loweredEnv E k |= pred x := A.

  Lemma loweredEnv_var_notLowered : forall E x A k,
    E |= k :! -> E |= x := A -> k > x -> loweredEnv E k |= x := A.

  Lemma var_loweredEnv_var_lowered : forall E x A k,
    E |= k :! -> loweredEnv E k |= x := A -> k <= x -> E |= S x := A.

  Lemma var_loweredEnv_var_notLowered : forall E x A k,
    E |= k :! -> loweredEnv E k |= x := A -> k > x -> E |= x := A.

  Lemma prelower_prelift_aux : forall Pt i j k, k >= j -> k <= i + j + 1 ->
    prelift_aux i Pt j = prelower_aux (prelift_aux (i + 1) Pt j) k.

  Lemma prelower_prelift : forall Pt i,
    prelift Pt i = prelower_aux (prelift Pt (i + 1)) i.

  Definition lower_aux : forall (M: Term) (k: nat), env M |= k :! ->
    {N: Term | env N = loweredEnv (env M) k
               /\ term N = prelower_aux (term M) k /\ type N = type M }.


  Definition lower (M: Term) (ME: env M |= 0 :!) : Term :=
    proj1_sig (lower_aux M ME).

  Lemma lower_env : forall M ME, env (lower M ME) = loweredEnv (env M) 0.

  Lemma lower_term : forall M ME, term (lower M ME) = prelower (term M).

  Lemma lower_type : forall M ME, type (lower M ME) = type M.

  Hint Rewrite lower_env lower_term lower_type : terms.

  Lemma prelift_prelower_aux : forall M i, env M |= i :! ->
    prelift_aux 1 (prelower_aux (term M) i) i = (term M).

  Lemma prelift_prelower : forall M M0, term (lift (lower M M0) 1) = term M.

  Lemma lower_absBody : forall E Pt A B (M: decl A E |- Pt := B) n
    (Menv: E |= n :!) (M'env: decl A E |= S n :!)
    (MLabs: isAbs (proj1_sig (lower_aux (buildT (TAbs M)) Menv))),
    absBody MLabs = proj1_sig (lower_aux (buildT M) M'env).

  Lemma lower_appBodyL : forall E PtL PtR A B n (Menv: E |= n :!)
    (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
    (MLapp: isApp (proj1_sig (lower_aux (buildT (TApp Ml Mr)) Menv))),
    appBodyL MLapp = proj1_sig (lower_aux (buildT Ml) Menv).

  Lemma lower_appBodyR : forall E PtL PtR A B n (Menv: E |= n :!)
    (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
    (MLapp: isApp (proj1_sig (lower_aux (buildT (TApp Ml Mr)) Menv))),
    appBodyR MLapp = proj1_sig (lower_aux (buildT Mr) Menv).

End TermsLifting.