Library CoLoR.Term.SimpleType.TermsActiveEnv

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Definition and properties of active environments: subset of term environments with declarations that are really used in a term.

Set Implicit Arguments.


Module TermsActiveEnv (Sig : TermsSig.Signature).

  Module Export TE := TermsEnv.TermsEnv Sig.

  Definition activeEnv (M: Term) : Env :=
    match M with
    | @buildT E Pt T M0 =>
      Typing_rect
      (fun E0 Pt0 T0 _ => Env)
      (fun _ x A _ => copy x None ++ A [#] EmptyEnv)
      (fun _ _ => EmptyEnv)
      (fun _ _ _ _ _ Ein => tail Ein)
      (fun _ _ _ _ _ _ El _ Er => El [+] Er)
      M0
    end.

  Definition envMinimal M := env M = activeEnv M.

  Lemma activeEnv_length : forall M, length (activeEnv M) <= length (env M).

  Lemma activeEnv_abs : forall M (Mabs: isAbs M),
    activeEnv M = tail (activeEnv (absBody Mabs)).

  Lemma activeEnv_app : forall M (Mapp: isApp M),
    activeEnv M = activeEnv (appBodyL Mapp) [+] activeEnv (appBodyR Mapp).

  Lemma activeEnv_funS : forall M (Mfs: isFunS M), activeEnv M = EmptyEnv.

  Lemma activeEnv_var_det : forall M x i A,
    term M = %x -> activeEnv M |= i := A -> i = x /\ A = type M.

  Lemma activeEnv_var_single : forall M x y A,
    term M = %x -> activeEnv M |= y := A -> x = y.

  Lemma activeEnv_var_type : forall M x y A,
    term M = %x -> activeEnv M |= y := A -> A = type M.

  Lemma activeEnv_subset : forall M, envSubset (activeEnv M) (env M).

  Lemma activeEnv_abs0 : forall M (Mabs: isAbs M) A,
    activeEnv (absBody Mabs) |= 0 := A -> A = absType Mabs.

  Lemma activeEnv_app_comp : forall M (Mapp: isApp M),
    activeEnv (appBodyL Mapp) [<->] activeEnv (appBodyR Mapp).

  Lemma activeEnv_appBodyL_varD : forall M (Mapp: isApp M),
    envSubset (activeEnv (appBodyL Mapp)) (activeEnv M).

  Lemma activeEnv_appBodyR_varD : forall M (Mapp: isApp M),
    envSubset (activeEnv (appBodyR Mapp)) (activeEnv M).

  Lemma typing_activeEnv : forall M, activeEnv M |- term M := type M.

  Lemma term_env_activeEnv : forall M, env M = env M [+] activeEnv M.

  Lemma equiv_term_activeEnv : forall M N,
    term M = term N -> env M [<->] env N -> activeEnv M = activeEnv N.

  Lemma activeEnv_var : forall M x,
    term M = %x -> activeEnv M = copy x None ++ type M [#] EmptyEnv.

  Lemma activeEnv_var_decl : forall M x A,
    term M = %x -> env M |= x := A -> activeEnv M |= x := A.

  Lemma activeEnv_lift_aux : forall M n k,
    activeEnv (proj1_sig (lift_aux n M k)) [=] liftedEnv n (activeEnv M) k.

  Lemma activeEnv_lift : forall M n,
    activeEnv (lift M n) [=] liftedEnv n (activeEnv M) 0.

  Lemma activeEnv_lower_aux : forall M n (Menv: env M |= n :!),
    activeEnv (proj1_sig (lower_aux M Menv)) = loweredEnv (activeEnv M) n.

  Lemma activeEnv_lower : forall M Menv,
    activeEnv (lower M Menv) = loweredEnv (activeEnv M) 0.

  Lemma activeEnv_minimal_len : forall M M', env M [<->] env M' ->
    term M = term M' -> length (activeEnv M) = length (activeEnv M').

  Lemma activeEnv_minimal_aux : forall M M', env M [<->] env M' ->
    term M = term M' -> envSubset (activeEnv M) (activeEnv M').

  Lemma activeEnv_minimal : forall M M',
    env M [<->] env M' -> term M = term M' -> activeEnv M = activeEnv M'.

  Lemma envMinimal_app : forall M Ml Mr (Mapp: isApp M),
    envMinimal Ml -> envMinimal Mr -> env Ml [<->] env Mr ->
    env M = env Ml [+] env Mr -> term M = term Ml @@ term Mr -> envMinimal M.

  Lemma envMinimal_abs : forall M N (Mabs: isAbs M),
    term (absBody Mabs) = term N ->
    tail (env (absBody Mabs)) = tail (env N) ->
    (env N |= 0 :! \/ env N |= 0 := absType Mabs) ->
    envMinimal N -> envMinimal M.

  Lemma activeEnv_subset_unit : forall Mu M,
    isAppUnit Mu M -> envSubset (activeEnv Mu) (activeEnv M).

  Lemma activeEnv_subset_arg : forall Marg M, isArg Marg M ->
    envSubset (activeEnv Marg) (activeEnv M).

  Lemma activeEnv_subset_units : forall M N,
    (forall N', In N' (appUnits N) -> envSubset (activeEnv N') (activeEnv M)) ->
    envSubset (activeEnv N) (activeEnv M).

  Lemma activeEnv_subset_partialFlattening : forall M N Ns,
    isPartialFlattening Ns N ->
    (forall N', In N' Ns -> envSubset (activeEnv N') (activeEnv M)) ->
    envSubset (activeEnv N) (activeEnv M).

End TermsActiveEnv.