Library CoLoR.Term.Lambda.LSimple

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

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

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

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

  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

  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

    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

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

    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

  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).
  Notation add := (Env_add 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 add := (@XMap.add 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.


  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.

Typing is compatible with alpha-equivalence.

Subject reduction for beta.

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

End Make.