Library CoLoR.Term.SimpleType.TermsAlgebraic

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Algebraic terms (functions with arity; simple output type of a function assumed) encoded via lambda-terms.

Set Implicit Arguments.


Module TermsAlgebraic (Sig : TermsSig.Signature).

  Module Export TE := TermsEta.TermsEta Sig.

  Inductive algebraic: Term -> Prop :=
  | AlgVar: forall M,
       isVar M ->
       algebraic M
  | AlgAbs: forall M (Mabs: isAbs M),
       algebraic (absBody Mabs) ->
       algebraic M
  | AlgApp: forall M,
       isApp M ->
       ~isFunApp M ->
       (forall M', isAppUnit M' M -> algebraic M') ->
       algebraic M
  | AlgFunApp: forall M,
       isFunApp M ->
       isBaseType (type M) ->
       (forall M', isArg M' M -> algebraic M') ->
       algebraic M.

  Lemma algebraic_morph_aux :
    forall x1 x2 : Term, x1 ~ x2 -> (algebraic x1 -> algebraic x2).

  Instance algebraic_morph : Proper (terms_conv ==> iff) algebraic.


  Lemma algebraic_funApp_datatype :
    forall M, algebraic M -> isFunApp M -> isBaseType (type M).

  Lemma algebraic_arrowType :
    forall M, algebraic M -> isArrowType (type M) -> ~isFunApp M.

  Lemma algebraic_absBody : forall M (Mabs: isAbs M),
      algebraic M -> algebraic (absBody Mabs).

  Lemma algebraic_arg : forall M Marg (Mapp: isApp M),
      algebraic M -> isArg Marg M -> algebraic Marg.

  Lemma algebraic_appBodyL : forall M (Mapp: isApp M),
      ~isFunApp M -> algebraic M -> algebraic (appBodyL Mapp).

  Lemma algebraic_appBodyR : forall M (Mapp: isApp M),
      algebraic M -> algebraic (appBodyR Mapp).

  Lemma algebraic_appUnits : forall M, algebraic M -> ~isFunApp M ->
    forall M', isAppUnit M' M -> algebraic M'.

  Lemma algebraic_app : forall M (Mapp: isApp M), algebraic (appBodyL Mapp) ->
    algebraic (appBodyR Mapp) -> algebraic M.

  Lemma algebraic_var : forall M (Mvar: isVar M), algebraic M.

  Lemma algebraic_lift : forall M i, algebraic M -> algebraic (lift M i).

  Lemma algebraic_lower : forall M Me, algebraic M -> algebraic (lower M Me).

  Lemma algebraic_app_notFunApp : forall M (Mapp: isApp M),
      algebraic (appBodyL Mapp) -> algebraic (appBodyR Mapp) -> ~isFunApp M.

  Lemma algebraic_funS M : algebraic M -> isFunS M -> isBaseType (type M).

  Lemma funS_algebraic: forall M,
      isBaseType (type M) -> isFunS M -> algebraic M.

  Definition algebraicSubstitution G := forall p T, G |-> p/T -> algebraic T.

  Lemma singletonSubst_algebraic : forall G T,
      isSingletonSubst T G -> algebraic T -> algebraicSubstitution G.

  Lemma algebraicSubstitution_cons_none : forall G,
      algebraicSubstitution G -> algebraicSubstitution (None :: G).

  Lemma algebraicSubstitution_cons_some : forall G T, algebraicSubstitution G ->
    algebraic T -> algebraicSubstitution (Some T :: G).

  Lemma algebraicSubstitution_cons_rev : forall G T,
      algebraicSubstitution (T :: G) -> algebraicSubstitution G.

  Lemma algebraicSubstitution_lifted : forall G i,
      algebraicSubstitution G -> algebraicSubstitution (lift_subst G i).

  Lemma notFunApp_subst : forall M G (MG: correct_subst M G),
      isApp M -> algebraicSubstitution G -> ~isFunApp M -> ~isFunApp (subst MG).

  Lemma algebraic_subst : forall M G (MG: correct_subst M G),
      algebraic M -> algebraicSubstitution G -> algebraic (subst MG).

  Lemma betaStep_algebraic_preserving :
    forall M N, algebraic M -> BetaStep M N -> algebraic N.

  Lemma beta_algebraic_preserving :
    forall M N, algebraic M -> M -b-> N -> algebraic N.

  Lemma algebraic_dec: forall M, {algebraic M} + {~algebraic M}.

  Section Monotonicity.

    Variable R : relation Term.

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

    Definition algebraic_monotonicity :=
      forall T (pos: Pos T) (Mpos: PlaceHolder pos) (Npos: PlaceHolder pos)
        (M := proj1_sig2 Mpos) (N := proj1_sig2 Npos),
        algebraic T -> algebraic M -> algebraic N -> ~isFunApp (T // pos) ->
        M -R-> N -> swap Mpos -R-> swap Npos.

    Lemma monotonicity_algebraicMonotonicity :
      monotonous R -> algebraic_monotonicity.

    Lemma algebraic_swap_this : forall M (pos: Pos M) (MP: PlaceHolder pos)
      (P := proj1_sig2 MP), pos = PThis M -> algebraic P -> algebraic (swap MP).

    Lemma algebraic_swap_abs :
      forall M (pos: Pos M) (MP: PlaceHolder pos) (P := proj1_sig2 MP),
        (forall Min (pos: Pos Min) (MP: PlaceHolder pos) (P := proj1_sig2 MP),
            subterm Min M -> ~isFunApp (Min // pos) -> algebraic Min ->
            algebraic P -> algebraic (swap MP)) ->
        pos <> PThis M -> isAbs M -> ~isFunApp (M // pos) -> algebraic M ->
        algebraic P -> algebraic (swap MP).

    Lemma algebraic_swap_notFunApp :
      forall M (pos: Pos M) (MP: PlaceHolder pos) (P := proj1_sig2 MP),
        (forall Min (pos: Pos Min) (MP: PlaceHolder pos) (P := proj1_sig2 MP),
            subterm Min M -> ~isFunApp (Min // pos) -> algebraic Min ->
            algebraic P -> algebraic (swap MP)) ->
        pos <> PThis M -> ~isFunApp M -> ~isFunApp (M // pos) ->
        (forall M', isAppUnit M' M -> algebraic M') -> algebraic P ->
        (forall M', isAppUnit M' (swap MP) -> algebraic M').

    Lemma algebraic_swap_isFunApp :
      forall M (pos: Pos M) (MP: PlaceHolder pos) (P := proj1_sig2 MP),
        (forall Min (pos: Pos Min) (MP: PlaceHolder pos) (P := proj1_sig2 MP),
            subterm Min M -> ~isFunApp (Min // pos) -> algebraic Min ->
            algebraic P -> algebraic (swap MP)) ->
        isFunApp M -> ~isFunApp (M // pos) ->
        (forall M', isArg M' M -> algebraic M') ->
        algebraic P -> (forall M', isArg M' (swap MP) -> algebraic M').

    Lemma algebraic_swap_app : forall M (pos: Pos M) (MP: PlaceHolder pos)
      (P := proj1_sig2 MP),
      (forall Min (pos: Pos Min) (MP: PlaceHolder pos) (P := proj1_sig2 MP),
        subterm Min M -> ~isFunApp (Min // pos) -> algebraic Min ->
        algebraic P -> algebraic (swap MP)
      ) ->
      pos <> PThis M -> ~isFunApp (M // pos) -> isApp M -> algebraic M ->
      algebraic P -> algebraic (swap MP).

    Lemma algebraic_swap : forall M (pos: Pos M) (MP: PlaceHolder pos)
      (P := proj1_sig2 MP),
      ~isFunApp (M // pos) -> algebraic M -> algebraic P -> algebraic (swap MP).

    Lemma algebraic_swap_funApp : forall T (pos: Pos T)
        (Mpos: PlaceHolder pos) (Npos: PlaceHolder pos)
        (M := proj1_sig2 Mpos) (N := proj1_sig2 Npos),
        ~isFunApp (T // pos) -> isFunApp T ->
        exists l t (tp: Pos t) (ph: PlaceHolder tp * PlaceHolder tp),
          isArg t T /\ ~isFunApp (t // tp) /\
          proj1_sig2 (fst ph) = M /\ proj1_sig2 (snd ph) = N /\
          appHead (swap Mpos) = appHead (swap Npos) /\
          appArgs (swap Mpos) = fst l ++ (swap (fst ph)) :: snd l /\
          appArgs (swap Npos) = fst l ++ (swap (snd ph)) :: snd l.

    Definition appMonCond := forall M M' (Mapp: isApp M) (M'app: isApp M'),
        algebraic M -> algebraic M' ->
        (
          ~isFunApp M /\ ~isFunApp M' /\
          appBodyL Mapp -R-> appBodyL M'app /\
          appBodyR Mapp = appBodyR M'app
        ) \/
        (
          ~isFunApp M /\ ~isFunApp M' /\
          appBodyL Mapp = appBodyL M'app /\
          appBodyR Mapp -R-> appBodyR M'app
        ) \/
        (
          isFunApp M /\ appHead M = appHead M' /\
          exists ll, exists m, exists m',
            appArgs M = fst ll ++ m :: snd ll /\
            appArgs M' = fst ll ++ m' :: snd ll /\
            m -R-> m'
        ) ->
        M -R-> M'.

    Definition absMonCond := forall N N' (Nabs: isAbs N) (N'abs: isAbs N'),
        algebraic (absBody Nabs) -> algebraic (absBody N'abs) ->
        absType Nabs = absType N'abs ->
        absBody Nabs -R-> absBody N'abs ->
        N -R-> N'.

    Lemma algebraic_monotonicity_criterion :
      appMonCond -> absMonCond -> algebraic_monotonicity.

  End Monotonicity.

  Definition AlgTerm := { T: Term | algebraic T }.

  Definition algTerm (T: AlgTerm) : Term := proj1_sig T.

  Coercion algTerm: AlgTerm >-> Term.

  Module AlgTermsSet <: SetA.
    Definition A := AlgTerm.
  End AlgTermsSet.

  Module AlgTermsEqset <: Eqset := Eqset_def AlgTermsSet.

End TermsAlgebraic.