# Library CoLoR.Term.SimpleType.TermsTyping

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
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.