Library CoLoR.Term.SimpleType.TermsConv

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
This file contains development concerning convertibility relation of simply-typed lambda terms. This convertibility relation is an extension of alpha-conversion to environments. So terms equal up to permutation of the order of declarations of ground variables in environment are identified.

Set Implicit Arguments.


Module TermsConv (Sig : TermsSig.Signature).

  Module Export TP := TermsPos.TermsPos Sig.

  Record EnvSubst : Type := build_envSub {
    envSub: relation nat;
    size: nat;
    envSub_dec: forall i j, {envSub i j} + {~envSub i j};
    envSub_Lok: forall i j j', envSub i j -> envSub i j' -> j = j';
    envSub_Rok: forall i i' j, envSub i j -> envSub i' j -> i = i';
    sizeOk: forall i j, envSub i j -> i < size /\ j < size
  }.

  Lemma envSubst_dec : forall i Q,
    {j: nat | envSub Q i j} + {forall j, ~envSub Q i j}.

  Definition envSubst_extends S1 S2 :=
    forall i j, envSub S2 i j -> envSub S1 i j.

  Notation "S1 |=> S2" := (envSubst_extends S1 S2) (at level 70).

  Definition envSubst_eq S1 S2 := S1 |=> S2 /\ S2 |=> S1.

  Notation "S1 <=> S2" := (envSubst_eq S1 S2) (at level 70).

  Lemma envSubst_eq_def : forall S1 S2 i j,
    S1 <=> S2 -> (envSub S1 i j <-> envSub S2 i j).

  Lemma envSubst_extends_refl : forall S, S |=> S.

  Lemma envSubst_extends_trans : forall S1 S2 S3,
    S1 |=> S2 -> S2 |=> S3 -> S1 |=> S3.

  Lemma envSubst_eq_refl : forall S, S <=> S.

  Lemma envSubst_eq_sym : forall S1 S2, S1 <=> S2 -> S2 <=> S1.

  Lemma envSubst_eq_trans : forall S1 S2 S3,
    S1 <=> S2 -> S2 <=> S3 -> S1 <=> S3.

  Instance envSubst_eq_Equivalence : Equivalence envSubst_eq.


  Instance envSubst_extends_morph :
    Proper (envSubst_eq ==> envSubst_eq ==> iff) envSubst_extends.


  Definition emptyEnvSubst: EnvSubst.


  Definition singletonEnvSubst : nat -> nat -> EnvSubst.


  Definition idEnvSubst : nat -> EnvSubst.


  Definition compEnvSubst : forall (E1 E2: Env), E1 [<->] E2 -> EnvSubst.


  Definition sumEnvSubst : forall Q Q1 Q2, Q |=> Q1 -> Q |=> Q2 -> EnvSubst.


  Lemma sumEnvSubst_or : forall Q Ql Qr (QQl: Q |=> Ql) (QQr: Q |=> Qr) p q,
    envSub (sumEnvSubst QQl QQr) p q -> envSub Ql p q \/ envSub Qr p q.

  Lemma sumEnvSubst_ext_l : forall Q Ql Qr (QQl: Q |=> Ql) (QQr: Q |=> Qr),
    sumEnvSubst QQl QQr |=> Ql.

  Lemma sumEnvSubst_ext_r : forall Q Ql Qr (QQl: Q |=> Ql) (QQr: Q |=> Qr),
    sumEnvSubst QQl QQr |=> Qr.

  Lemma sumEnvSubst_ext : forall Q Ql Qr (QQl: Q |=> Ql) (QQr: Q |=> Qr),
    Q |=> sumEnvSubst QQl QQr.

  Definition addEnvSubst : forall (Q: EnvSubst) (i: nat) (j: nat)
    (ok: envSub Q i j \/ (forall x, ~envSub Q i x /\ ~envSub Q x j)), EnvSubst.

    Import Psatz.
  Definition liftEnvSubst : forall (n: nat) (k: nat) (size: nat), EnvSubst.


  Definition lowerEnvSubst : forall (k: nat) (size: nat), EnvSubst.


  Definition envSubst_lower : EnvSubst -> EnvSubst.


  Definition envSubst_lift1 : EnvSubst -> EnvSubst.


  Fixpoint envSubst_lift (Q: EnvSubst) (n: nat) : EnvSubst :=
    match n with
    | 0 => Q
    | S x => envSubst_lift1 (envSubst_lift Q x)
    end.

  Lemma envSubst_lift1_ext : forall Q Q',
    Q' |=> Q -> envSubst_lift1 Q' |=> envSubst_lift1 Q.

  Lemma envSubst_lift1_ext_rev : forall Q Q',
    envSubst_lift1 Q' |=> envSubst_lift1 Q -> Q' |=> Q.

  Lemma envSubst_lift1_absurdR : forall i Q,
    envSub (envSubst_lift1 Q) 0 (S i) -> False.

  Lemma envSubst_lift1_absurdL : forall i Q,
    envSub (envSubst_lift1 Q) (S i) 0 -> False.

  Definition envSubst_transp : forall E : EnvSubst, EnvSubst.


  Definition envSubst_compose : forall (E1 E2 : EnvSubst), EnvSubst.


  Lemma envSubst_transp_def : forall p q Q,
    envSub Q p q -> envSub (envSubst_transp Q) q p.

  Lemma envSubst_transp_lower : forall S,
    envSubst_transp (envSubst_lower S) <=> envSubst_lower (envSubst_transp S).

  Lemma envSubst_transp_lift : forall S,
    envSubst_transp (envSubst_lift1 S) <=> envSubst_lift1 (envSubst_transp S).

  Lemma envSubst_transp_twice : forall S,
    envSubst_transp (envSubst_transp S) <=> S.

  Lemma envSubst_lift_lower : forall Q,
    envSub Q 0 0 -> envSubst_lift1 (envSubst_lower Q) <=> Q.

  Lemma envSubst_lower_lift : forall Q, envSubst_lower (envSubst_lift1 Q) <=> Q.

  Lemma envSubst_eq_cons : forall S1 S2,
    envSubst_lower S1 <=> envSubst_lower S2 ->
    envSub S1 0 0 -> envSub S2 0 0 -> S1 <=> S2.

  Lemma envSubst_eq_abs : forall M N (Mabs: isAbs M) (Nabs: isAbs N)
    (MN: env M [<->] env N) (MNin: env (absBody Mabs) [<->] env (absBody Nabs)),
    envSubst_lift1 (compEnvSubst MN) <=> compEnvSubst MNin.

  Lemma envSubst_lift_eq : forall S1 S2,
    S1 <=> S2 -> envSubst_lift1 S1 <=> envSubst_lift1 S2.

  Lemma envSubst_lift_compose : forall S1 S2,
    envSubst_lift1 (envSubst_compose S1 S2) <=>
    envSubst_compose (envSubst_lift1 S1) (envSubst_lift1 S2).

  Lemma lift_liftEnvSubst : forall n k s,
    envSubst_lift1 (liftEnvSubst n k s) <=> liftEnvSubst n (S k) (S s).

  Lemma lift_lowerEnvSubst : forall k s,
    envSubst_lift1 (lowerEnvSubst k s) <=> lowerEnvSubst (S k) (S s).

  Inductive conv_term: Preterm -> Preterm -> EnvSubst -> Prop :=
  | ConvVar: forall x y S,
      S.(envSub) x y ->
      conv_term (%x) (%y) S
  | ConvFun: forall f S,
      conv_term (^f) (^f) S
  | ConvAbs: forall A L R S,
      conv_term L R (envSubst_lift1 S) ->
      conv_term (\A => L) (\A => R) S
  | ConvApp: forall LL LR RL RR S,
      conv_term LL RL S ->
      conv_term LR RR S ->
      conv_term (LL @@ LR) (RL @@ RR) S.

  Lemma conv_term_morph_aux :
    forall (x x0 : Preterm) (x1 x2 : EnvSubst),
    x1 <=> x2 -> conv_term x x0 x1 -> conv_term x x0 x2.

  Instance conv_term_morph :
    Proper (eq ==> eq ==> envSubst_eq ==> iff) conv_term.


  Lemma conv_term_refl : forall M,
    conv_term (term M) (term M) (idEnvSubst (length (env M))).

  Lemma conv_term_comp_refl : forall M N (MN: env M [<->] env N),
    term M = term N -> conv_term (term M) (term N) (compEnvSubst MN).

  Lemma conv_term_sym : forall PtL PtR S, conv_term PtL PtR S ->
    conv_term PtR PtL (envSubst_transp S).

  Lemma conv_term_trans : forall M N P mn np,
    conv_term M N mn -> conv_term N P np ->
    conv_term M P (envSubst_compose mn np).

  Lemma conv_term_lift : forall M n k,
    conv_term (term M) (prelift_aux n (term M) k)
    (liftEnvSubst n k (length (env M))).

  Lemma conv_term_lower : forall M k (M0: env M |= k :!),
    conv_term (term M) (prelower_aux (term M) k)
    (lowerEnvSubst k (length (env M))).

  Lemma conv_term_lifted_aux : forall M N i Q, conv_term M N Q ->
    (forall j, j < i -> Q.(envSub) j j) ->
    conv_term (prelift_aux 1 M i) (prelift_aux 1 N i) (envSubst_lift1 Q).

  Lemma conv_term_lifted : forall M N Q, conv_term M N Q ->
    conv_term (prelift M 1) (prelift N 1) (envSubst_lift1 Q).

  Lemma conv_term_unique : forall M N N' Q,
    conv_term M N Q -> conv_term M N' Q -> N = N'.

  Lemma conv_term_ext : forall M N Q Q',
    conv_term M N Q -> Q' |=> Q -> conv_term M N Q'.

  Definition activeEnv_compSubst_on M N x y :=
    forall A, activeEnv M |= x := A <-> activeEnv N |= y := A.

  Definition conv_env (M N: Term) (S: EnvSubst) :=
    forall x y, S.(envSub) x y -> activeEnv_compSubst_on M N x y.

  Instance conv_env_morph :
    Proper (eq ==> eq ==> envSubst_eq ==> iff) conv_env.


  Lemma conv_env_refl : forall M, conv_env M M (idEnvSubst (length (env M))).

  Lemma conv_env_sym : forall M N mn,
    conv_env M N mn -> conv_env N M (envSubst_transp mn).

  Lemma conv_env_trans : forall M N P mn np,
    conv_env M N mn -> conv_env N P np -> conv_env M P (envSubst_compose mn np).

  Lemma conv_env_empty : forall M N, conv_env M N emptyEnvSubst.

  Lemma terms_conv_var_usage : forall M N Q x y,
    (forall A B, activeEnv M |= x := A -> activeEnv N |= y := B -> A = B) ->
    envSub Q x y -> conv_term (term M) (term N) Q ->
    activeEnv_compSubst_on M N x y.

  Lemma conv_env_absBody : forall M N (Mabs: isAbs M) (Nabs: isAbs N) Q,
    conv_term (term M) (term N) Q -> conv_env M N Q ->
    conv_env (absBody Mabs) (absBody Nabs) (envSubst_lift1 Q).

  Lemma conv_env_abs : forall M N (Mabs: isAbs M) (Nabs: isAbs N) Q,
    conv_term (term M) (term N) Q ->
    conv_env (absBody Mabs) (absBody Nabs) (envSubst_lift1 Q) ->
    conv_env M N Q.

  Lemma conv_env_app : forall M N (Mapp: isApp M) (Napp: isApp N) Q,
    conv_term (term M) (term N) Q ->
    conv_env (appBodyL Mapp) (appBodyL Napp) Q ->
    conv_env (appBodyR Mapp) (appBodyR Napp) Q ->
    conv_env M N Q.

  Lemma conv_env_var: forall M N x y Q,
    envSub Q x y -> term M = %x -> term N = %y ->
    type M = type N -> conv_env M N Q.

  Lemma conv_env_lifted : forall M N Q, conv_env M N Q ->
    conv_env (lift M 1) (lift N 1) (envSubst_lift1 Q).

  Lemma conv_env_lift : forall M n,
    conv_env M (lift M n) (liftEnvSubst n 0 (length (env M))).

  Lemma conv_env_lower : forall M Menv,
    conv_env M (lower M Menv) (lowerEnvSubst 0 (length (env M))).

  Lemma conv_env_appBodyL : forall M N (Mapp: isApp M) (Napp: isApp N) Q,
    conv_env M N Q ->
    conv_term (term M) (term N) Q -> conv_env (appBodyL Mapp) (appBodyL Napp) Q.

  Lemma conv_env_appBodyR : forall M N (Mapp: isApp M) (Napp: isApp N) Q,
    conv_env M N Q ->
    conv_term (term M) (term N) Q -> conv_env (appBodyR Mapp) (appBodyR Napp) Q.

  Lemma conv_env_ext : forall M N Q Q',
    conv_term (term M) (term N) Q -> conv_env M N Q ->
    Q' |=> Q -> conv_env M N Q'.

  Definition terms_conv_with S M N :=
    conv_term (term M) (term N) S /\ conv_env M N S.

  Notation "M ~ ( S ) N" := (terms_conv_with S M N) (at level 5).

  Lemma terms_conv_with_morph_aux :
    forall x1 x2 : EnvSubst,
    x1 <=> x2 -> forall x x0 : Term, x ~ (x1)x0 -> x ~ (x2)x0.

  Instance terms_conv_with_morph :
    Proper (envSubst_eq ==> eq ==> eq ==> iff) terms_conv_with.


  Definition terms_conv M N := exists S, M ~(S) N.

  Infix "~" := terms_conv (at level 7).

  Lemma terms_conv_criterion : forall M N,
    env M [<->] env N -> term M = term N -> M ~ N.

  Lemma terms_conv_criterion_strong : forall M N,
    activeEnv M = activeEnv N -> term M = term N -> M ~ N.

  Lemma terms_conv_eq_type : forall M N, M ~ N -> type M = type N.

  Lemma terms_conv_refl : forall M, M ~ M.

  Lemma terms_conv_sym_aux : forall M N Q, M ~(Q) N -> N ~(envSubst_transp Q) M.

  Lemma terms_conv_sym : forall M N, M ~ N -> N ~ M.

  Lemma terms_conv_trans : forall M N P, M ~ N -> N ~ P -> M ~ P.

  Lemma terms_eq_conv : forall M N, M = N -> M ~ N.

  Instance terms_conv_Equivalence : Equivalence terms_conv.


  Instance isApp_morph : Proper (terms_conv ==> iff) isApp.


  Instance isVar_morph : Proper (terms_conv ==> iff) isVar.


  Instance isAbs_morph : Proper (terms_conv ==> iff) isAbs.


  Instance isNeutral_morph : Proper (terms_conv ==> iff) isNeutral.


  Instance isFunS_morph : Proper (terms_conv ==> iff) isFunS.


  Lemma conv_by : forall M N Q, M ~(Q) N -> M ~ N.

  Lemma abs_conv_absBody_aux : forall M N Q (Mabs: isAbs M) (Nabs: isAbs N),
    M ~(Q) N -> (absBody Mabs) ~(envSubst_lift1 Q) (absBody Nabs).

  Lemma abs_conv_absBody : forall M N (Mabs: isAbs M) (Nabs: isAbs N), M ~ N ->
    terms_conv (absBody Mabs) (absBody Nabs).

  Lemma abs_conv_absType : forall M N (Mabs: isAbs M) (Nabs: isAbs N), M ~ N ->
    absType Mabs = absType Nabs.

  Lemma abs_conv : forall M N (Mabs: isAbs M) (Nabs: isAbs N) Q,
    absType Mabs = absType Nabs ->
    (absBody Mabs) ~(envSubst_lift1 Q) (absBody Nabs) -> M ~(Q) N.

  Lemma app_conv_app_left_aux : forall M N (Mapp: isApp M) (Napp: isApp N) Q,
    M ~(Q) N -> (appBodyL Mapp) ~(Q) (appBodyL Napp).

  Lemma app_conv_app_left : forall M N (Mapp: isApp M) (Napp: isApp N), M ~ N ->
    terms_conv (appBodyL Mapp) (appBodyL Napp).

  Lemma app_conv_app_right_aux : forall M N (Mapp: isApp M) (Napp: isApp N) Q,
    M ~(Q) N -> (appBodyR Mapp) ~(Q) (appBodyR Napp).

  Lemma app_conv_app_right : forall M N (Mapp: isApp M) (Napp: isApp N),
    M ~ N -> terms_conv (appBodyR Mapp) (appBodyR Napp).

  Lemma app_conv : forall M N (Mapp: isApp M) (Napp: isApp N) Q,
    (appBodyL Mapp) ~(Q) (appBodyL Napp)
    -> (appBodyR Mapp) ~(Q) (appBodyR Napp) -> M ~(Q) N.

  Lemma terms_conv_conv_lift : forall M N Q,
    M ~(Q) N -> (lift M 1) ~(envSubst_lift1 Q) (lift N 1).

  Lemma terms_lift_conv : forall M n, terms_conv M (lift M n).

  Lemma terms_lower_conv :
    forall M (Menv: env M |= 0 :!), terms_conv M (lower M Menv).

  Lemma appHead_conv : forall M N Q, M ~(Q) N -> (appHead M) ~(Q) (appHead N).

  Instance appHead_morph : Proper (terms_conv ==> terms_conv) appHead.


  Instance isFunApp_morph : Proper (terms_conv ==> iff) isFunApp.


  Lemma terms_conv_activeEnv: forall M N Q, M ~(Q) N ->
    forall p A, activeEnv M |= p := A -> exists q, envSub Q p q.

  Lemma terms_conv_activeEnv_rev : forall N M Q, M ~(Q) N ->
    forall q A, activeEnv N |= q := A -> exists p, envSub Q p q.

  Lemma terms_conv_activeEnv_sub : forall M M' N N' Q, M ~(Q) M' ->
    envSubset (activeEnv N) (activeEnv M) -> N ~(Q) N' ->
    envSubset (activeEnv N') (activeEnv M').

  Lemma terms_conv_extend_subst : forall M N Q Q',
    M ~(Q) N -> Q' |=> Q -> M ~(Q') N.

  Lemma terms_conv_shrink_subst : forall M N Q Q', M ~(Q') N -> Q' |=> Q ->
    (forall x A, activeEnv M |= x := A -> exists y, envSub Q x y) -> M ~(Q) N.

  Lemma terms_conv_diff_env : forall M N N' Q, M ~(Q) N -> term N' = term N ->
    activeEnv N' = activeEnv N -> M ~(Q) N'.

  Lemma terms_conv_diff_env_rev : forall M N M' Q,
    M ~(Q) N -> term M' = term M -> activeEnv M' = activeEnv M -> M' ~(Q) N.

  Definition envSub_minimal Q M :=
    forall x y, envSub Q x y -> exists A, activeEnv M |= x := A.

  Lemma envSub_minimal_rev : forall Q M M' x y, envSub_minimal Q M ->
    M ~(Q) M' -> envSub Q x y -> exists A, activeEnv M' |= y := A.

  Lemma envSubst_add: forall Q i j,
    envSub Q i j \/ (forall x, ~envSub Q i x /\ ~envSub Q x j) ->
    exists Q', Q' |=> Q /\ envSub Q' i j /\
      (forall p q, envSub Q' p q -> (envSub Q p q \/ (p = i /\ q = j))).

  Lemma envSub_min_ex : forall M N Q, M ~(Q) N -> exists Q',
    M ~(Q') N /\ envSub_minimal Q' M /\ Q |=> Q'.

  Lemma envSubst_extend : forall i Q E,
    (forall j, ~envSub Q i j) -> exists Q',
      Q' |=> Q /\ exists j, envSub Q' i j /\ E |= j :! /\
        (forall k l, envSub Q' k l -> (k <> i \/ l <> j) -> envSub Q k l).

  Lemma term_build_conv : forall M Q E,
    (forall x y A B, envSub Q x y -> activeEnv M |= x := A ->
      E |= y := B -> A = B) ->
    exists Q', Q' |=> Q /\ exists M',
      M ~(Q') M' /\ env M' [<->] E /\ envMinimal M' /\
      (forall x y, envSub Q' x y -> envSub Q x y \/ E |= y :!).

  Lemma term_build_conv_ext : forall M Q, exists Q', Q' |=> Q /\
    exists M', M ~(Q') M' /\ envMinimal M'.

  Lemma term_build_conv_rel : forall M N N' Q,
    envSubset (activeEnv N) (activeEnv M) ->
    N ~(Q) N' -> envSub_minimal Q N -> exists Q', Q' |=> Q /\
      exists M', M ~(Q') M' /\ envSubset (env N') (env M').

  Lemma term_build_conv_sim : forall M M' N Q,
    M ~(Q) M' -> envSub_minimal Q M -> env M = env N ->
    envSubset (activeEnv N) (activeEnv M) ->
    exists N', env M' = env N' /\ N ~(Q) N'.

  Lemma conv_arg : forall M Marg N Q, M ~(Q) N -> isArg Marg M ->
    exists Narg, isArg Narg N /\ Marg ~(Q) Narg.

  Lemma conv_arg_rev : forall M N Narg Q, M ~(Q) N -> isArg Narg N ->
    exists Marg, isArg Marg M /\ Marg ~(Q) Narg.

  Hint Resolve terms_eq_conv terms_conv_eq_type terms_conv_sym terms_conv_refl
    terms_conv_trans app_conv_app_left app_conv_app_right : terms_eq.

  Definition conv_list Ms Ns Q := list_sim (fun M N => M ~(Q) N) Ms Ns.

  Lemma appUnits_conv : forall M N Q,
    M ~(Q) N -> conv_list (appUnits M) (appUnits N) Q.

  Lemma appArgs_conv : forall M N Q,
    M ~(Q) N -> conv_list (appArgs M) (appArgs N) Q.

  Lemma appUnit_conv_appUnit : forall M M' N Q, M ~(Q) N -> isAppUnit M' M ->
    exists N', isAppUnit N' N /\ M' ~(Q) N'.

  Lemma appArg_conv_appArg : forall M M' N Q, M ~(Q) N -> isArg M' M ->
    exists N', isArg N' N /\ M' ~(Q) N'.

  Lemma partialFlattening_conv : forall M Ms N Q,
    M ~(Q) N -> isPartialFlattening Ms M ->
    exists Ns, isPartialFlattening Ns N /\ conv_list Ms Ns Q.

  Lemma apply_variable : forall M, isArrowType M.(type) ->
    exists MA: Term, exists Mapp: isApp MA,
      (appBodyL Mapp) ~ M /\ term (appBodyR Mapp) = %length (env M) /\
      env MA = env M ++ Some (type_left (type M))::EmptyEnv.

End TermsConv.