Library CoLoR.Term.SimpleType.TermsManip

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
In this file some basic operations on terms of simply typed lambda-calculus are defined.

Set Implicit Arguments.


Module TermsManip (Sig : TermsSig.Signature).

  Module Export TS := TermsTyping.TermsTyping Sig.

  Implicit Types M N : Term.

  Definition isVar M : Prop :=
  let (_, _, _, typ) := M in
  match typ with
  | TVar _ => True
  | _ => False
  end.

  Lemma var_is_var : forall M x, term M = %x -> isVar M.

  Definition isFunS M : Prop :=
  let (_, _, _, typ) := M in
  match typ with
  | TFun _ _ => True
  | _ => False
  end.

  Lemma funS_is_funS : forall M f, term M = ^f -> isFunS M.

  Lemma funS_fun : forall M, isFunS M -> exists f, term M = ^f.

  Definition isAbs M : Prop :=
  let (_, _, _, typ) := M in
  match typ with
  | TAbs _ => True
  | _ => False
  end.

  Hint Unfold isVar isFunS isAbs : terms.

  Ltac assert_abs hypName M :=
     assert (hypName : isAbs M);
     [try solve [eauto with terms | term_inv M]
     | idtac
     ].

  Definition absBody M : isAbs M -> Term :=
  match M return (isAbs M -> Term) with
  | buildT typ =>
      match typ return (isAbs (buildT typ) -> Term) with
      | TAbs absT => fun _ : True => buildT absT
      | _ => fun notAbs: False => False_rect Term notAbs
      end
  end.

  Definition absType M : isAbs M -> SimpleType :=
  match M return (isAbs M -> SimpleType) with
  | buildT typ =>
      match typ return (isAbs (buildT typ) -> SimpleType) with
      | @TAbs _ A B _ _ => fun _ : True => A
      | _ => fun notAbs : False => False_rect SimpleType notAbs
      end
  end.

  Lemma abs_isAbs : forall M A Pt, term M = \A => Pt -> isAbs M.

  Lemma absBody_eq_env : forall M N (MAbs: isAbs M) (NAbs: isAbs N),
    env M = env N -> type M = type N -> env (absBody MAbs) = env (absBody NAbs).

  Lemma absBody_equiv_type : forall M N (MAbs: isAbs M) (NAbs: isAbs N),
    type M == type N -> type (absBody MAbs) == type (absBody NAbs).

  Lemma absBody_eq_type : forall M N (MAbs: isAbs M) (NAbs: isAbs N),
    type M = type N -> type (absBody MAbs) = type (absBody NAbs).

  Lemma absBody_term : forall M (Mabs: isAbs M) A Pt,
    term M = \A => Pt -> term (absBody Mabs) = Pt.

  Lemma absBody_env : forall M (Mabs: isAbs M),
    env (absBody Mabs) = decl (absType Mabs) (env M).

  Lemma abs_type : forall M (Mabs: isAbs M) A B,
    type M = A --> B -> absType Mabs = A.

  Hint Rewrite absBody_term absBody_env abs_type
    using solve [auto with terms] : terms.

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

  Lemma absBody_type : forall M (Mabs: isAbs M) A B,
    type M = A --> B -> type (absBody Mabs) = B.

  Lemma abs_type_eq : forall M N (Mabs: isAbs M) (Nabs: isAbs N),
    absType Mabs = absType Nabs ->
    type (absBody Mabs) = type (absBody Nabs) -> type M = type N.

  Lemma abs_proof_irr : forall M (Mabs Mabs': isAbs M), Mabs = Mabs'.

  Lemma absBody_eq : forall M N (Mabs: isAbs M) (Nabs: isAbs N),
    M = N -> absBody Mabs = absBody Nabs.

  Lemma abs_term : forall M (Mabs: isAbs M),
    term M = \ (absType Mabs) => (term (absBody Mabs)).

  Hint Resolve absBody absType abs_isAbs absBody_eq_env funS_is_funS
    absBody_equiv_type absBody_eq_type : terms.
  Hint Rewrite absBody_env : terms.

  Definition isApp M : Prop :=
  let (_, _, _, typ) := M in
  match typ with
  | TApp _ _ => True
  | _ => False
  end.

  Ltac assert_app hypName M :=
     assert (hypName : isApp M);
     [try solve [eauto with terms | term_inv M]
     | idtac
     ].

  Definition appBodyL M : isApp M -> Term :=
  match M return (isApp M -> Term) with
  | buildT typ =>
      match typ return (isApp (buildT typ) -> Term) with
      | TApp L R => fun _ : True => buildT L
      | _ => fun notApp: False => False_rect Term notApp
      end
  end.


  Definition appBodyR M : isApp M -> Term :=
  match M return (isApp M -> Term) with
  | buildT typ =>
      match typ return (isApp (buildT typ) -> Term) with
      | TApp L R => fun _ : True => buildT R
      | _ => fun notApp: False => False_rect Term notApp
      end
  end.


  Lemma app_isApp : forall M Pt0 Pt1, term M = Pt0 @@ Pt1 -> isApp M.

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

  Lemma app_Req_LtypeEq : forall M N (Mapp: isApp M) (Napp: isApp N),
    term (appBodyR Mapp) = term (appBodyR Napp) -> env M = env N ->
    type M = type N -> type (appBodyL Mapp) = type (appBodyL Napp).

  Lemma app_Leq_RtypeEq : forall M N (Mapp: isApp M) (Napp: isApp N),
    term (appBodyL Mapp) = term (appBodyL Napp) -> env M = env N ->
    type M = type N -> type (appBodyR Mapp) = type (appBodyR Napp).

  Lemma appBodyL_env : forall M (Mapp: isApp M), env (appBodyL Mapp) = env M.

  Lemma appBodyR_env : forall M (Mapp: isApp M), env (appBodyR Mapp) = env M.

  Hint Rewrite appBodyL_env appBodyR_env : terms.

  Lemma appBodyL_term : forall M PtL PtR (Mterm: term M = PtL @@ PtR)
    (Mapp: isApp M), term (appBodyL Mapp) = PtL.

  Lemma appBodyR_term : forall M PtL PtR (Mterm: term M = PtL @@ PtR)
    (Mapp: isApp M), term (appBodyR Mapp) = PtR.

  Lemma term_appBodyL_eq : forall M N (Mapp: isApp M) (Napp: isApp N),
    term M = term N -> term (appBodyL Mapp) = term (appBodyL Napp).

  Lemma term_appBodyR_eq : forall M N (Mapp: isApp M) (Napp: isApp N),
    term M = term N -> term (appBodyR Mapp) = term (appBodyR Napp).

  Hint Rewrite appBodyL_term appBodyR_term
    using solve [auto with terms] : terms.

  Lemma app_typeL_type : forall M A B (Mapp: isApp M),
    type (appBodyL Mapp) = A --> B -> type M = B.

  Lemma app_typeR : forall M A B (Mapp: isApp M),
    type (appBodyL Mapp) = A --> B -> type (appBodyR Mapp) = A.

  Hint Rewrite app_typeL_type app_typeR using solve [auto with terms] : terms.

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

  Lemma app_proof_irr : forall M (Mapp Mapp': isApp M), Mapp = Mapp'.

  Lemma app_term : forall M (Mapp: isApp M),
    term M = term (appBodyL Mapp) @@ term (appBodyR Mapp).

  Hint Resolve appBodyL appBodyR app_isApp app_proof_irr app_Req_LtypeEq
    app_Leq_RtypeEq : terms.
  Hint Unfold isApp : terms.
  Hint Rewrite appBodyL_env appBodyR_env : terms.

  Lemma isVar_dec : forall M, {isVar M} + {~isVar M}.

  Lemma isAbs_dec : forall M, {isAbs M} + {~isAbs M}.

  Lemma isFunS_dec : forall M, {isFunS M} + {~isFunS M}.

  Lemma isApp_dec : forall M, {isApp M} + {~isApp M}.

  Definition appUnits M : list Term :=
  let
    fix appUnits_rec M (Mt: TermTyping M) : list Term :=
    match Mt with
    | (TApp Ltyp Rtyp) => (buildT Rtyp) ::
                                    (@appUnits_rec (buildT Ltyp) Ltyp)
    | _ => (buildT Mt)::nil
    end
  in rev (appUnits_rec M M.(typing)).

  Lemma appUnits_not_nil : forall M, appUnits M <> nil.

  Definition appHead M : Term := proj1_sig (head_notNil (appUnits_not_nil M)).

  Definition appArgs M := tail (appUnits M).

  Definition isArg M' M : Prop := In M' (appArgs M).

  Definition isAppUnit M' M : Prop := In M' (appUnits M).

  Definition isNeutral M : Prop := ~ isAbs M.

  Definition isFunApp M : Prop := isFunS (appHead M).

  Definition isPartialFlattening Args M : Prop :=
  match Args with
  | nil => False
  | hd::nil => False
  | hd::tl => appUnits hd ++ tl = appUnits M
  end.

  Hint Resolve appUnits appHead appArgs appUnits_not_nil : terms.
  Hint Unfold isPartialFlattening isFunApp isNeutral : terms.

  Lemma appUnits_notApp : forall M, ~isApp M -> appUnits M = M::nil.

  Lemma appUnit_notApp : forall M Mu, isAppUnit Mu M -> ~isApp M -> Mu = M.

  Lemma appUnit_head_or_arg : forall M M', In M' (appUnits M) ->
    M' = appHead M \/ In M' (appArgs M).

  Lemma appUnits_app : forall M (Mapp: isApp M),
    appUnits M = appUnits (appBodyL Mapp) ++ (appBodyR Mapp)::nil.

  Lemma appUnit_app : forall Mu M (Mapp: isApp M), isAppUnit Mu M ->
    (Mu = appBodyR Mapp \/ isAppUnit Mu (appBodyL Mapp)).

  Lemma appHead_notApp : forall M, ~isApp M -> appHead M = M.

  Lemma appHead_app_aux : forall M (Mapp: isApp M),
    head (appUnits M) = head (appUnits (appBodyL Mapp)).

  Lemma appHead_app : forall M (Mapp: isApp M),
    appHead M = appHead (appBodyL Mapp).

  Lemma appHead_app_explicit : forall E PtL PtR A B (L: E |- PtL := A --> B)
    (R: E |- PtR := A), appHead (buildT (TApp L R)) = appHead (buildT L).

  Lemma appArgs_notApp : forall M, ~isApp M -> appArgs M = nil.

  Lemma appArgs_app : forall M (Mapp: isApp M),
    appArgs M = appArgs (appBodyL Mapp) ++ (appBodyR Mapp)::nil.

  Lemma app_units_app : forall M (Mapp: isApp M),
    appUnits M = appHead M :: nil ++ appArgs M.

  Hint Rewrite appUnits_notApp appUnits_app appHead_notApp appHead_app
    appArgs_notApp appArgs_app : terms.

  Lemma appArg_inv : forall M N (Mapp: isApp M), isArg N M ->
    (isArg N (appBodyL Mapp) \/ N = (appBodyR Mapp)).

  Lemma appArg_is_appUnit : forall M N, isArg M N -> isAppUnit M N.

  Lemma appUnit_left : forall M N (Mapp: isApp M),
    isAppUnit N (appBodyL Mapp) -> isAppUnit N M.

  Lemma appUnit_right : forall M N (Mapp: isApp M),
    N = appBodyR Mapp -> isAppUnit N M.

  Lemma appArg_left : forall M N (Mapp: isApp M),
    isArg N (appBodyL Mapp) -> isArg N M.

  Lemma appArg_right : forall M N (Mapp: isApp M),
    N = appBodyR Mapp -> isArg N M.

  Lemma appArg_app : forall M Marg, isArg Marg M -> isApp M.

  Lemma funS_neutral : forall M, isFunS M -> isNeutral M.

  Lemma app_neutral : forall M, isApp M -> isNeutral M.

  Lemma var_neutral : forall M, isVar M -> isNeutral M.

  Lemma abs_not_neutral : forall M, isAbs M -> isNeutral M -> False.

  Lemma abs_isnot_app : forall M, isAbs M -> ~isApp M.

  Lemma app_isnot_abs : forall M, isApp M -> ~isAbs M.

  Lemma term_case : forall M, {isVar M} + {isFunS M} + {isAbs M} + {isApp M}.

  Hint Resolve appArg_inv appArg_is_appUnit abs_isnot_app app_isnot_abs
               appUnits_notApp appHead_notApp appHead_app appArgs_notApp
               appArgs_app appUnit_left: terms.

  Inductive subterm : relation Term :=
  | AppLsub: forall M N (Mapp: isApp M),
      subterm_le N (appBodyL Mapp) ->
      subterm N M
  | AppRsub: forall M N (Mapp: isApp M),
      subterm_le N (appBodyR Mapp) ->
      subterm N M
  | Abs_sub: forall M N (Mabs: isAbs M),
      subterm_le N (absBody Mabs) ->
      subterm N M
   with subterm_le: relation Term :=
  | subterm_lt: forall M N,
      subterm N M ->
      subterm_le N M
  | subterm_eq: forall M,
      subterm_le M M.

  Definition subterm_gt := transp subterm.

  Module Subterm_Ord <: Ord.

    Module TermSet <: SetA.
      Definition A := Term.
    End TermSet.
    Module S := Eqset_def TermSet.

    Definition A := Term.
    Definition gtA := subterm_gt.
    Definition gtA_eqA_compat := Eqset_def_gtA_eqA_compat subterm_gt.

  End Subterm_Ord.

  Lemma subterm_wf : well_founded subterm.

  Lemma appBodyL_subterm : forall M (Mapp: isApp M), subterm (appBodyL Mapp) M.

  Lemma appBodyR_subterm : forall M (Mapp: isApp M), subterm (appBodyR Mapp) M.

  Lemma absBody_subterm : forall M (Mabs: isAbs M), subterm (absBody Mabs) M.

  Lemma appUnit_subterm : forall M N, isApp M -> isAppUnit N M -> subterm N M.

  Lemma arg_subterm : forall M Ma, isArg Ma M -> subterm Ma M.

  Lemma appUnits_notEmpty : forall M hd tl el,
    appUnits M ++ hd::tl = el::nil -> False.

  Lemma partialFlattening_app : forall M Ms,
    isPartialFlattening Ms M -> isApp M.

  Lemma app_notApp_diffUnits : forall M N,
    isApp M -> ~isApp N -> appUnits M = appUnits N -> False.

  Lemma eq_unitTypes_eq_types : forall M N,
    length (appUnits M) = length (appUnits N) ->
    (forall p Ma Na,
      nth_error (appUnits M) p = Some Ma ->
      nth_error (appUnits N) p = Some Na ->
      type Ma = type Na) -> type M = type N.

  Lemma eq_units_eq_terms : forall M N, appUnits M = appUnits N -> M = N.

  Lemma partialFlattening_subterm_aux : forall N L M,
    L <> nil -> appUnits M ++ L = appUnits N -> subterm M N.

  Lemma partialFlattening_subterm : forall M Ms m,
    isPartialFlattening Ms M -> In m Ms -> subterm m M.

  Lemma funApp_head : forall M, isFunApp M ->
    { f: FunctionSymbol | term (appHead M) = ^f }.

  Lemma funApp : forall M f, term (appHead M) = ^f -> isApp M -> isFunApp M.

  Lemma funS_funApp : forall M, isFunS M -> isFunApp M.

  Lemma appHead_term : forall (M N: Term),
    term M = term N -> term (appHead M) = term (appHead N).

  Lemma appHead_left : forall M (Mapp: isApp M), isFunS (appHead M) ->
    isFunS (appHead (appBodyL Mapp)).

  Lemma headFunS_dec : forall M, {isFunS (appHead M)} + {~isFunS (appHead M)}.

  Lemma isFunApp_dec : forall M, {isFunApp M} + {~isFunApp M}.

  Lemma isFunApp_left : forall M (Mapp: isApp M),
    isFunApp M -> isFunApp (appBodyL Mapp).

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

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

  Lemma notFunApp_left_eq : forall M (Mapp: isApp M) N (Napp: isApp N),
    ~isFunApp M -> appBodyL Mapp = appBodyL Napp -> ~isFunApp N.

  Lemma funAbs_notFunApp : forall M, isAbs (appHead M) -> ~isFunApp M.

  Lemma notFunApp_notFunS : forall M, ~isFunApp M -> ~isFunS M.

  Lemma appUnit_env : forall Mu M, isAppUnit Mu M -> env Mu = env M.

  Lemma partialFlattening_env : forall M Ms, isPartialFlattening Ms M ->
    forall Min, In Min Ms -> env Min = env M.

  Lemma partialFlattening_inv : forall M (Mapp: isApp M) Ms,
    isPartialFlattening Ms M ->
    Ms = appBodyL Mapp :: appBodyR Mapp :: nil
    \/ exists Ns, isPartialFlattening Ns (appBodyL Mapp)
      /\ Ms = Ns ++ appBodyR Mapp :: nil.

  Lemma partialFlattening_desc : forall M (Mapp: isApp M) ML,
    isPartialFlattening ML (appBodyL Mapp) ->
    isPartialFlattening (ML ++ appBodyR Mapp :: nil) M.

  Lemma allPartialFlattenings : forall M, isApp M ->
    { MF: list (list Term)
      | forall Mpf, isPartialFlattening Mpf M <-> In Mpf MF }.

  Lemma term_neq_type : forall M N, type M <> type N -> M <> N.

  Hint Resolve appUnit_subterm partialFlattening_app eq_units_eq_terms
               partialFlattening_subterm funApp_head funApp : terms.

  Module TermSet <: SetA.
     Definition A := Term.
  End TermSet.
  Module TermEqSet := Eqset_def TermSet.

End TermsManip.