Library CoLoR.Term.SimpleType.TermsBuilding

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

Set Implicit Arguments.


Module TermsBuilding (Sig : TermsSig.Signature).

  Module Export TAE := TermsActiveEnv.TermsActiveEnv Sig.

  Record appCond : Type := {
     appL: Term;
     appR: Term;
     eqEnv: env appL = env appR;
     typArr: isArrowType (type appL);
     typOk: type_left (type appL) = type appR
  }.

  Definition buildApp : appCond -> Term.


  Lemma buildApp_isApp : forall a, isApp (buildApp a).

  Lemma buildApp_Lok : forall a, appBodyL (buildApp_isApp a) = a.(appL).

  Lemma buildApp_Rok : forall a, appBodyR (buildApp_isApp a) = a.(appR).

  Lemma buildApp_preterm : forall a,
    term (buildApp a) = term a.(appL) @@ term a.(appR).

  Lemma buildApp_env_l : forall a, env (buildApp a) = env a.(appL).

  Lemma buildApp_type : forall a,
    type (buildApp a) = type_right (type a.(appL)).

  Record absCond : Type := {
    absB: Term;
    absT: SimpleType;
    envNotEmpty: env absB |= 0 := absT
  }.

  Definition buildAbs : absCond -> Term.


  Lemma buildAbs_isAbs: forall a, isAbs (buildAbs a).

  Lemma buildAbs_absBody : forall a, absBody (buildAbs_isAbs a) = a.(absB).

  Lemma buildAbs_absType : forall a, absType (buildAbs_isAbs a) = a.(absT).

  Lemma buildAbs_env : forall a, env (buildAbs a) = tail (env a.(absB)).

  Definition buildVar : forall A x, (copy x None ++ A [#] EmptyEnv) |- %x := A.


  Lemma buildVar_minimal : forall A x, envMinimal (buildT (buildVar A x)).

End TermsBuilding.