Library CoLoR.Term.SimpleType.TermsPos

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Positions in terms, replacement of term at position, monotonicity property.

Set Implicit Arguments.


Module TermsPos (Sig : TermsSig.Signature).

  Module Export TB := TermsBuilding.TermsBuilding Sig.

  Inductive Pos : Term -> Type :=
  | PThis: forall M, Pos M
  | PAbs: forall E A B Pt AbsB,
              Pos (buildT AbsB) ->
              Pos (buildT (@TAbs E A B Pt AbsB))
  | PAppL: forall E A B PtL PtR AppL AppR,
              Pos (buildT AppL) ->
              Pos (buildT (@TApp E A B PtL PtR AppL AppR))
  | PAppR: forall E A B PtL PtR AppL AppR,
              Pos (buildT AppR) ->
              Pos (buildT (@TApp E A B PtL PtR AppL AppR)).

  Fixpoint termAtPos M (pos: Pos M) : Term :=
  match pos with
  | PThis M => M
  | PAbs pos => termAtPos pos
  | PAppL _ pos => termAtPos pos
  | PAppR _ pos => termAtPos pos
  end.
  Notation "M // pos" := (@termAtPos M pos) (at level 40).

  Fixpoint swap_term M (pos: Pos M) (R: Term) : Preterm :=
    match pos with
    | PThis M => term R
    | @PAbs _ A _ _ _ pos => Abs A (swap_term pos R)
    | @PAppL _ _ _ PtL PtR _ _ pos => swap_term pos R @@ PtR
    | @PAppR _ _ _ PtL PtR _ _ pos => PtL @@ swap_term pos R
    end.

  Definition PlaceHolder M pos :=
    { T: Term |
        env (M // pos) = env T &
        type (M // pos) = type T
    }.

  Definition swap_aux : forall M (pos: Pos M) (R: PlaceHolder pos),
    {N: Term | env N = env M /\ type N = type M
               /\ term N = swap_term pos (proj1_sig2 R)}.


  Definition swap M pos N : Term := proj1_sig (swap_aux (M := M) (pos := pos) N).

  Lemma swap_type_eq : forall M (pos: Pos M) (N: PlaceHolder pos), type (swap N) = type M.

  Lemma swap_env_eq : forall M (pos: Pos M) (N: PlaceHolder pos), env (swap N) = env M.

  Lemma swap_term_is : forall M (pos: Pos M) (N: PlaceHolder pos),
    term (swap N) = swap_term pos (proj1_sig2 N).

  Lemma swap_this : forall T (Mpos: PlaceHolder (PThis T)) (M := proj1_sig2 Mpos), swap Mpos = M.

  Lemma posThis_dec : forall T (pos: Pos T), {pos = PThis T} + {pos <> PThis T}.

  Lemma swap_appL_eq : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Mr)) (Mpos: PlaceHolder (PAppR Ml pos)) (Npos: PlaceHolder (PAppR Ml pos))
      (Lapp: isApp (swap Mpos)) (Rapp: isApp (swap Npos)), appBodyL Lapp = appBodyL Rapp.

  Lemma swap_appR_eq : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Ml)) (Mpos: PlaceHolder (PAppL Mr pos)) (Npos: PlaceHolder (PAppL Mr pos))
      (Lapp: isApp (swap Mpos)) (Rapp: isApp (swap Npos)), appBodyR Lapp = appBodyR Rapp.

  Lemma appBodyR_swap_in_appL : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Ml)) (Mpos: PlaceHolder pos) (MLpos: PlaceHolder (PAppL Mr pos))
      (MLapp: isApp (swap MLpos)), proj1_sig2 Mpos = proj1_sig2 MLpos ->
      appBodyR (M:=swap MLpos) MLapp = buildT Mr.

  Lemma swap_in_appL : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Ml)) (Mpos: PlaceHolder pos) (MLpos: PlaceHolder (PAppL Mr pos))
      (MLapp: isApp (swap MLpos)), proj1_sig2 Mpos = proj1_sig2 MLpos ->
      swap Mpos = appBodyL (M := swap MLpos) MLapp.

  Lemma swap_in_appR : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Mr)) (Mpos: PlaceHolder pos) (MLpos: PlaceHolder (PAppR Ml pos))
      (MLapp: isApp (swap MLpos)), proj1_sig2 Mpos = proj1_sig2 MLpos ->
      swap Mpos = appBodyR (M := swap MLpos) MLapp.

  Lemma appBodyL_swap_in_appR : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Mr)) (Mpos: PlaceHolder pos) (MLpos: PlaceHolder (PAppR Ml pos))
      (MLapp: isApp (swap MLpos)), proj1_sig2 Mpos = proj1_sig2 MLpos ->
      appBodyL (M := swap MLpos) MLapp = buildT Ml.

  Lemma swap_in_abs : forall E Pt A B (M: E |- \A => Pt := A --> B) (Min: decl A E |- Pt := B)
      (pos: Pos (buildT Min)) (Mpos: PlaceHolder pos) (Min_pos: PlaceHolder (PAbs pos))
      (Min_abs: isAbs (swap Min_pos)), proj1_sig2 Mpos = proj1_sig2 Min_pos ->
      swap Mpos = absBody (M := swap Min_pos) Min_abs.

  Lemma swap_left_app : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Ml)) (N: PlaceHolder (PAppL Mr pos)), isApp (swap N).

  Lemma swap_right_app : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Mr)) (N: PlaceHolder (PAppR Ml pos)), isApp (swap N).

  Lemma app_swap_app : forall M (pos: Pos M) (MP: PlaceHolder pos), pos <> PThis M ->
    isApp M -> isApp (swap MP).

  Lemma swap_abs : forall E Pt A B (Mb: decl A E |- Pt := B) (pos: Pos (buildT Mb))
      (N: PlaceHolder (PAbs pos)), isAbs (swap N).

  Lemma placeHolder_appL : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Ml)) (N: PlaceHolder (PAppL Mr pos)),
      { W: PlaceHolder pos | proj1_sig2 W = proj1_sig2 N }.

  Lemma placeHolder_appR : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A)
      (pos: Pos (buildT Mr)) (N: PlaceHolder (PAppR Ml pos)),
      { W: PlaceHolder pos | proj1_sig2 W = proj1_sig2 N }.

  Lemma placeHolder_abs : forall E Pt A B (Mb: decl A E |- Pt := B) (pos: Pos (buildT Mb))
      (N: PlaceHolder (PAbs pos)), { W: PlaceHolder pos | proj1_sig2 W = proj1_sig2 N }.

  Lemma swap_isFunApp : forall T (pos: Pos T) (Mpos: PlaceHolder pos) (M := proj1_sig2 Mpos),
      isFunApp T -> ~isFunApp (T // pos) -> isFunApp (swap Mpos).

  Lemma swap_not_funApp : forall T (pos: Pos T) (Mpos: PlaceHolder pos) (M := proj1_sig2 Mpos),
    pos <> PThis T -> ~isFunApp T -> (isFunApp M -> isBaseType (type M)) -> ~isFunApp (swap Mpos).

  Section Monotonicity.

    Variable R : relation Term.

    Notation "X -R-> Y" := (R X Y) (at level 50).

    Definition monotonous :=
      forall T (pos: Pos T) (Mpos: PlaceHolder pos) (Npos: PlaceHolder pos),
        proj1_sig2 Mpos -R-> proj1_sig2 Npos ->
        swap Mpos -R-> swap Npos.

    Lemma monotonicity_criterion :
        (forall M M' (Mapp: isApp M) (M'app: isApp M'),
          appBodyL Mapp -R-> appBodyL M'app ->
          appBodyR Mapp = appBodyR M'app ->
          M -R-> M'
        ) ->
        (forall M M' (Mapp: isApp M) (M'app: isApp M'),
          appBodyL Mapp = appBodyL M'app ->
          appBodyR Mapp -R-> appBodyR M'app ->
          M -R-> M'
        ) ->
        (forall N N' (Nabs: isAbs N) (N'abs: isAbs N'),
          absType Nabs = absType N'abs ->
          absBody Nabs -R-> absBody N'abs ->
          N -R-> N'
        ) ->
        monotonous.

    Variable R_monotonous : monotonous.

    Variable R_type_preserving : forall M N, M -R-> N -> type M = type N.

    Variable R_env_preserving: forall M N, M -R-> N -> env M = env N.

    Definition posAppLeft : forall M (Mapp: isApp M), Pos M.


    Lemma monotonous_appL : forall M N (Mapp: isApp M) (Napp: isApp N),
        appBodyL Mapp -R-> appBodyL Napp -> appBodyR Mapp = appBodyR Napp -> M -R-> N.

  End Monotonicity.

End TermsPos.