Library CoLoR.Term.SimpleType.TermsSubstConv

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Convertibility of substituted terms.

Set Implicit Arguments.


Module TermsSubstConv (Sig : TermsSig.Signature).

  Module Export TS := TermsSubst.TermsSubst Sig.

  Record subst_conv_with (G1: Subst) (G2: Subst) (Q: EnvSubst) : Prop := {
    sc_lr: forall x y T, Q.(envSub) x y -> G1 |-> x/T ->
      exists T', G2 |-> y/T' /\ T ~(Q) T';
    sc_rl: forall x y T',Q.(envSub) x y -> G2 |-> y/T' ->
      exists T, G1 |-> x/T /\ T ~(Q) T';
    sc_inj_l: forall x T, G1 |-> x/T -> exists y, Q.(envSub) x y;
    sc_inj_r: forall y T, G2 |-> y/T -> exists x, Q.(envSub) x y }.

  Notation "G ~~ ( S ) H" := (subst_conv_with G H S) (at level 70).

  Definition subst_conv G1 G2 := exists S, G1 ~~(S) G2.

  Infix "~~" := subst_conv (at level 70).

  Lemma subst_empty_conv : forall S, nil ~~(S) nil.

  Lemma conv_subst_udecl G G' Q x y :
    G ~~(Q) G' -> Q.(envSub) x y -> G |-> x/- -> G' |-> y/- .

 Lemma singletonSubst_conv T T' G G' Q :
   isSingletonSubst T G -> isSingletonSubst T' G' -> G ~~(Q) G' -> T ~(Q) T'.

  Lemma singletonSubst_conv_rev T T' G G' Q : isSingletonSubst T G ->
    isSingletonSubst T' G' -> envSub Q 0 0 -> T ~(Q) T' -> G ~~(Q) G'.

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

  Lemma subst_conv_singleton M G G' Q :
    Q.(envSub) 0 0 -> isSingletonSubst M G -> G ~~(Q) G' ->
    exists M', isSingletonSubst M' G' /\ M ~(Q) M'.

  Lemma subst_conv_sym G1 G2 S : G1 ~~(S) G2 -> G2 ~~(envSubst_transp S) G1.

  Lemma subst_conv_cons G G' Q : G ~~(Q) G' ->
    None :: (lift_subst G 1) ~~(envSubst_lift1 Q) None :: (lift_subst G' 1).

  Lemma conv_subst_conv_term_aux :
    forall M M' G G' Q, conv_term M M' Q -> G ~~(Q) G' ->
                        conv_term (presubst M G) (presubst M' G') Q.

  Definition subst_envMinimal G := forall x T, G |-> x/T -> envMinimal T.

  Lemma subst_ran_decl_conv G G' S x y A :
    G ~~(S) G' -> envSub S x y -> subst_envs_comp G -> subst_envMinimal G' ->
    subst_ran G' |= y := A -> subst_ran G |= x := A.

  Lemma conv_subst_correct M M' G G' S :
    M ~(S) M' -> envMinimal M' -> G ~~(S) G' -> subst_envs_comp G' ->
    subst_envMinimal G' -> correct_subst M G -> correct_subst M' G'.

  Lemma conv_subst_singleton_build M M' T G Q : envSub Q 0 0 -> M ~(Q) M' ->
    envSub_minimal Q M -> isSingletonSubst T G -> correct_subst M G ->
    exists Q' G' T',
      correct_subst M' G' /\ isSingletonSubst T' G' /\ Q' |=> Q /\ G ~~(Q') G'.

  Lemma conv_subst_conv :
    forall M M' G G' Q (MG: correct_subst M G) (M'G': correct_subst M' G'),
      M ~(Q) M' -> G ~~(Q) G' -> (subst MG) ~(Q) (subst M'G').

  Lemma presubst_singleton_conv_sim_aux : forall M M' T T' Q R R' i,
    (forall j, j <= i -> envSub Q j j) -> conv_term M M' Q ->
    (lift T i) ~(Q) (lift T' i) ->
    conv_term R R' Q -> presubst_aux M i (copy i None ++ {x/T}) = R ->
    presubst_aux M' i (copy i None ++ {x/T'}) = R'.

  Lemma presubst_singleton_conv_sim M M' T T' Q R R' :
    envSub Q 0 0 -> conv_term M M' Q -> T ~(Q) T' -> conv_term R R' Q ->
    presubst M {x/T} = R -> presubst M' {x/T'} = R'.

End TermsSubstConv.