Library CoLoR.Term.SimpleType.TermsTyping

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Some results concerning typing of terms of simply typed lambda-calculus are introduced in this file.

Set Implicit Arguments.


Module TermsTyping (Sig : TermsSig.Signature).

  Module Export TD := TermsDef.TermsDef Sig.

  Lemma baseType_dec : forall A, {isBaseType A} + {isArrowType A}.

  Lemma type_discr : forall A B, ~A = A --> B.

  Lemma type_discr2 : forall A B C, ~A = (A --> B) --> C.

Section Equality_Decidable.

  Lemma eq_nat_dec : forall (m n: nat), {m=n}+{m<>n}.

  Hint Resolve eq_nat_dec : terms.

  Lemma eq_SimpleType_dec : forall (A B: SimpleType), {A=B} + {A<>B}.

  Hint Resolve eq_SimpleType_dec : terms.

  Lemma eq_Env_dec : forall (E1 E2 : Env), {E1=E2} + {E1<>E2}.

  Hint Resolve eq_Env_dec : terms.

  Lemma eq_Preterm_dec : forall (F G: Preterm), {F=G}+{F<>G}.

  Hint Resolve eq_Preterm_dec : terms.

  Lemma isVarDecl_dec : forall E x,
    {A: SimpleType | E |= x := A} + {E |= x :!}.

  Lemma eq_EPS_dec :
    forall (a b : Env * Preterm * SimpleType), {a=b} + {a<>b}.

End Equality_Decidable.

Section Typing.

  Lemma VarD_unique : forall E x A (v1 v2 : VarD E x A), v1 = v2.

  Lemma Type_unique : forall Pt E T1 T2 (d1 : Typing E Pt T1)
    (d2 : Typing E Pt T2), T1 = T2.

  Lemma typing_unique : forall E Pt T (d1 d2 : Typing E Pt T), d1 = d2.

  Lemma deriv_uniq : forall M N, env M = env N -> term M = term N ->
    type M = type N -> M = N.

  Lemma typing_uniq : forall M N, env M = env N -> term M = term N ->
    type M = type N.

  Lemma term_eq : forall M N, env M = env N -> term M = term N -> M = N.

  Lemma eq_Term_dec : forall (M N: Term), {M=N} + {M<>N}.

End Typing.

  Hint Resolve typing_uniq deriv_uniq term_eq : terms.

Section Auto_Typing.

  Definition autoType : forall E Pt, {N: Term | env N = E & term N = Pt} +
    {~exists N: Term, env N = E /\ term N = Pt}.


  Definition typeTerm (E: Env) (Pt: Preterm) (T: SimpleType) : option Term.


End Auto_Typing.

Module TermsSet <: SetA.
  Definition A := Term.
End TermsSet.

Module TermsEqset <: Eqset := Eqset_def TermsSet.

Module TermsEqset_dec <: Eqset_dec.

  Module Export Eq := TermsEqset.

  Definition eqA_dec := eq_Term_dec.

End TermsEqset_dec.

Ltac infer_tt :=
  compute;
    match goal with
    | |- _ |- ?t := _ =>
      match t with
      | App _ _ => eapply TApp; infer_tt
      | Abs _ _ => eapply TAbs; infer_tt
      | Fun _ => intuition
      | Var _ => eapply TVar; compute; trivial
      end
    end.

End TermsTyping.