# Library CoLoR.Term.Lambda.LSimple

CoLoR, a Coq library on rewriting and termination.
• Frederic Blanqui, 2012-04-05

# Simply-typed lambda-terms

Set Implicit Arguments.

# Simple types over a set So of type constants or sorts.

Section simple.

Variable So : Type.

Inductive Ty : Type :=
| Base : So -> Ty
| Arr : Ty -> Ty -> Ty.

Infix "~~>" := Arr (at level 55, right associativity).

Notation Tys := (vector Ty).

Basic functions on simple types.

Fixpoint arity (T : Ty) :=
match T with
| Base _ => 0
| Arr _ T' => S (arity T')
end.

Fixpoint inputs (T : Ty) :=
match T as T return Tys (arity T) with
| Base _ => Vnil
| Arr T1 T2 => Vcons T1 (inputs T2)
end.

Fixpoint output (T : Ty) k {struct k} :=
match k, T with
| S k', Arr U V => output V k'
| _, _ => T
end.

Fixpoint output_base (T : Ty) :=
match T with
| Base b => b
| Arr _ T' => output_base T'
end.

Lemma output_arity : forall T, output T (arity T) = Base (output_base T).

Lemma arity_output : forall p T, arity (output T p) = arity T - p.

Lemma output_output : forall p q T, output (output T p) q = output T (p+q).

Lemma inputs_output_aux : forall p T,
p <= arity T -> p + arity (output T p) <= arity T.

Lemma inputs_output : forall p T (h : p <= arity T),
inputs (output T p) = Vsub (inputs T) (inputs_output_aux h).

Lemma output_Base (s : So) n : output (Base s) n = Base s.

Lemma output_arrow_elim : forall n (A B C : Ty), output A n = B ~~> C
-> output A (S n) = C /\ exists h : S n <= arity A, Vnth (inputs A) h = B.

Building the type T1 ~~> .. ~~> Tn -> U from the type vector Ts and the type U.

Fixpoint arrow n (Ts : Tys n) U :=
match Ts with
| Vnil => U
| Vcons T Ts' => T ~~> arrow Ts' U
end.

Lemma arrow_cast : forall n (Ts : Tys n) U n' (h:n=n'),
arrow (Vcast Ts h) U = arrow Ts U.

Lemma arrow_output : forall T p q (h : p+q<=arity T),
arrow (Vsub (inputs T) h) (output T (p+q)) = output T p.

Decidability of equality on types.

Section dec.

Variable eq_so_dec : forall a b : So, {a=b}+{~a=b}.

Lemma eq_typ_dec : forall A B : Ty, {A=B}+{~A=B}.

End dec.

occurs a T says if T contains some a.

Section occurs.

Fixpoint occurs a T :=
match T with
| Base b => a = b
| Arr A B => occurs a A \/ occurs a B
end.

Variable eq_dec : forall x y : So, {x = y}+{~x = y}.

Lemma occurs_dec : forall a T, {occurs a T}+{~occurs a T}.

End occurs.

Predicate saying that a type constant occurs only positively/negatively in a simple type.

Section pos.

Variable a : So.

Fixpoint pos T :=
match T with
| Base _ => True
| Arr A B => neg A /\ pos B
end

with neg T :=
match T with
| Base b => b <> a
| Arr A B => pos A /\ neg B
end.

Lemma pos_base : forall b, pos (Base b) <-> True.

Lemma pos_arrow : forall A B, pos (A ~~> B) <-> neg A /\ pos B.

Lemma neg_base : forall b, neg (Base b) <-> b <> a.

Lemma neg_arrow : forall A B, neg (A ~~> B) <-> pos A /\ neg B.

Some properties of occurs, pos and neg.

Lemma not_occurs_pos_neg : forall {T}, ~occurs a T -> pos T /\ neg T.

Lemma not_occurs_pos : forall {T}, ~occurs a T -> pos T.

Lemma not_occurs_neg : forall {T}, ~occurs a T -> neg T.

End pos.

End simple.

Infix "~~>" := Arr (at level 55, right associativity).

Hint Rewrite pos_base pos_arrow neg_base neg_arrow : pos.

Ltac simpl_pos := autorewrite with pos; simpl.

## Functor building a Cmp structure for simple types from a Cmp

structure for type constants.

Module ST_Cmp (Export BCmp : Cmp) <: Cmp.

Definition t := Ty BCmp.t.

Fixpoint cmp A B :=
match A, B with
| Base a, Base b => BCmp.cmp a b
| Base _, Arr _ _ => Lt
| Arr _ _, Base _ => Gt
| Arr A1 A2, Arr B1 B2 =>
match cmp A1 B1 with
| Eq => cmp A2 B2
| c => c
end
end.

Lemma cmp_opp : forall x y, cmp x y = CompOpp (cmp y x).

End ST_Cmp.

## Functor building a CmpTransLeibniz structure for simple types

from a CmpTransLeibniz structure for type constants.

Module ST_CmpTransLeibniz (Export BCmpTransLeibniz : CmpTransLeibniz)
<: CmpTransLeibniz.

Module C := ST_Cmp BCmpTransLeibniz.

Include C.

Lemma cmp_eq : forall x y, cmp x y = Eq -> x = y.

Lemma cmp_lt_trans :
forall x y z, cmp x y = Lt -> cmp y z = Lt -> cmp x z = Lt.
Module CF := CmpFacts C.   Qed.

End ST_CmpTransLeibniz.

# Typing relation

Note that, for typing an abstraction Lam x u in E, we do not assume that x does not occur in E, but overrides its type in E. This is a restricted form of weakening.

Section typing.

Variables F X So : Type.

Notation Te := (@Te F X).
Notation Tes := (vector Te).
Notation Var := (@Var F X).
Notation Fun := (@Fun F X).
Notation Ty := (@Ty So).

Variable typ : F -> Ty.

Definition TypArgs f := vector Te (arity (typ f)).

Record Env := mk_Env {
Env_type : Type;
Env_empty : Env_type;
Env_add : X -> Ty -> Env_type -> Env_type;
Env_In : X -> Env_type -> Prop;
Env_MapsTo : X -> Ty -> Env_type -> Prop;
Env_Equal : relation Env_type }.

Variable env : Env.

Notation En := (Env_type env).
Notation MapsTo := (Env_MapsTo env).

Inductive tr : En -> Te -> Ty -> Prop :=
| tr_var : forall E x T, MapsTo x T E -> tr E (Var x) T
| tr_fun : forall E f, tr E (Fun f) (typ f)
| tr_app : forall E u v V T, tr E u (V ~~> T) -> tr E v V -> tr E (App u v) T
| tr_lam : forall E x X v V, tr (add x X E) v V -> tr E (Lam x v) (X ~~> V).

Lemma tr_apps : forall n (us : Tes n) E t T (hn : n <= arity T),
tr E t T
-> (forall i (hi : i < n),
tr E (Vnth us hi) (Vnth (inputs T) (lt_le_trans hi hn)))
-> tr E (apps t us) (output T n).

Lemma tr_apps_fun_inv E f :
forall n (ts : Tes n) T, tr E (apps (Fun f) ts) T
-> T = output (typ f) n
/\ exists nf : n <= arity (typ f), forall i (hi : i < n),
tr E (Vnth ts hi) (Vnth (inputs (typ f)) (lt_le_trans hi nf)).

End typing.

Ltac env :=
unfold Env_type, Env_empty, Env_add, Env_In, Env_MapsTo, Env_Equal in *.

# Structure over which we will define typing.

Module Type ST_Struct.

Declare Module Export L : L_Struct.

Parameter So : Type.

Notation Ty := (Ty So).
Notation Tys := (vector Ty).

Parameter typ : F -> Ty.

Notation TypArgs := (@TypArgs F X So typ).

Module providing finite maps on variables.

Declare Module Export XMap : FMapInterface.S with Module E := XOrd.

Notation En := (@XMap.t Ty).
Notation empty := (@XMap.empty Ty).
Notation In := (@XMap.In Ty).
Notation MapsTo := (@XMap.MapsTo Ty).
Notation Equal := (@XMap.Equal Ty).
Notation env := (mk_Env empty add In MapsTo Equal).

End ST_Struct.

# Typing relation over an ST structure.

Module Make (Export ST : ST_Struct).

Module Export B := LBeta.Make ST.L.

## Typing environments

are finite maps from variables to types.

Module XMapUtil := FMapUtil.Make XMap.
Module Export Domain := XMapUtil.Domain XSet.
Export XMapUtil.

## Typing.

Notation tr := (@tr F X So typ env).

Notation "E '|-' v '~:' V" := (tr E v V) (at level 70).

If a term v is typable in E, then its free variable are in E. In fact, any subterm of v is typable in some extension of restrict_dom E (fv v).

Lemma tr_fv_dom : forall E v V, E |- v ~: V -> fv v [<=] dom E.

Weakening: tr is compatible with le.
Contraction: only the type of free variables need to be given.

Lemma tr_contraction : forall E v V,
E |- v ~: V -> forall y, ~XSet.In y (fv v) -> remove y E |- v ~: V.

Lemma tr_restrict : forall E v V,
E |- v ~: V -> restrict_dom E (fv v) |- v ~: V.

## Well-typed substitutions.

Definition wt s E F := forall x T, MapsTo x T E -> F |- s x ~: T.

Notation "F |-s s ~: E" := (wt s E F) (at level 70).

Instance wt_le : Proper (Logic.eq ==> le --> le ==> impl) wt.

Lemma tr_subs : forall E v V, E |- v ~: V ->
forall s F, F |-s s ~: E -> F |- subs s v ~: V.

## Subject reduction for beta.

Instance tr_beta_aeq :
Proper (Logic.eq ==> beta_aeq ==> Logic.eq ==> impl) tr.

End Make.