Library CoLoR.Term.Lambda.LTerm

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2012-04-05

Lambda-terms

Remark on the structure of the files in this directory: In Coq, functor instantiation generates distinct Inductive's (or Class'es or Record's), i.e. if F(M) provides an Inductive t, N1:=F(M) and N2:=F(M), then N1.t <> N2.t. To get around this problem, we have to define Inductive's outside any module. Moreover, in order to define some module types, we also need some functions (e.g. free variables, substitution, etc.) to be defined outside any module too. Therefore, in this library, the files start by defining some Inductive's and some functions in a section with the necessary abstract parameters. Then, a functor Make provides the properties of these Inductive's and functions when the abstract parameters are correctly set. We use a functor and not a section because, in Coq, modules cannot be defined inside a section and we rely on the FSet and FMap modules defined in the standard Coq library. We also use notations overriding the abstract names. These definitions are therefore put in a module Def in order to be refered later (e.g. tactic unfold).

Set Implicit Arguments.


The set Te of lambda-terms

given a set F of constants and a set X of variables.

Module Export Def.

Section term.

  Variables F X : Type.

  Inductive Te : Type :=
  | Var (x : X)
  | Fun (f : F)
  | App (u v : Te)
  | Lam (x : X) (u : Te).

Predicate saying that a term is not of the form Lam x a.

  Definition not_lam u := forall x a, u <> Lam x a.

Equality on Te is decidable.


  Section dec.

    Variables
      (eq_fun_dec : forall f g : F, {f=g}+{~f=g})
      (eq_var_dec : forall x y : X, {x=y}+{~x=y}).

    Lemma eq_term_dec : forall u v : Te, {u=v}+{~u=v}.

  End dec.

Size of a term


  Fixpoint size (t : Te) :=
    match t with
      | Var _ => 0
      | Fun _ => 0
      | App u v => 1 + max (size u) (size v)
      | Lam _ u => 1 + size u
    end.

Induction principles on term size.

  Lemma intro_size : forall P : Te -> Prop,
    (forall n u, size u < n -> P u) -> forall u, P u.

  Lemma ind_size0 : forall P : Te -> Prop,
    (forall u, (forall v, size v < size u -> P v) -> P u) -> forall u, P u.

  Lemma ind_size1 : forall P : Te -> Prop,
    (forall x, P (Var x)) -> (forall f, P (Fun f)) ->
    (forall u v, P u -> P v -> P (App u v)) ->
    (forall x u, (forall u', size u' <= size u -> P u') -> P (Lam x u)) ->
    forall u, P u.

Application of a term to a vector of terms.


  Notation Tes := (vector Te).

  Fixpoint apps {n} t (us : Tes n) :=
    match us with
      | Vnil => t
      | Vcons u us' => apps (App t u) us'
    end.

  Lemma apps_app_cons t u n (us : Tes n) :
    apps (App t u) us = apps t (Vcons u us).

  Lemma app_apps : forall n (us : Tes n) u v,
    App (apps u us) v = apps u (Vadd us v).

  Lemma apps_app : forall n (us : Tes n) t u, apps (App t u) us
    = App (apps t (Vremove_last (Vcons u us))) (Vlast u us).

  Lemma apps_apps : forall p (ts : Tes p) t q (us : Tes q),
    apps (apps t ts) us = apps t (Vapp ts us).

  Lemma apps_cast : forall n (ts : Tes n) p (h : n=p) t,
    apps t (Vcast ts h) = apps t ts.

  Lemma size_apps_l : forall n (ts : Tes n) t, size t <= size (apps t ts).

  Lemma size_apps_r_in : forall n (ts : Tes n) t ti,
    Vin ti ts -> size ti < size (apps t ts).

  Lemma size_apps_r_nth : forall n (ts : Tes n) t i (hi : i<n),
    size (Vnth ts hi) < size (apps t ts).

Head and arguments of a term.


  Fixpoint head (t : Te) :=
    match t with
      | App u _ => head u
      | _ => t
    end.

  Lemma head_head : forall u, head (head u) = head u.

  Fixpoint nb_args (t : Te) :=
    match t with
      | App u _ => S (nb_args u)
      | _ => 0
    end.

  Fixpoint args (t : Te) :=
    match t as t return Tes (nb_args t) with
      | App u v => Vadd (args u) v
      | _ => Vnil
    end.

  Lemma head_apps : forall n (us : Tes n) t, head (apps t us) = head t.

  Lemma apps_head_args : forall u, u = apps (head u) (args u).

  Lemma nb_args_apps : forall n (ts : Tes n) t,
    nb_args (apps t ts) = nb_args t + n.

  Lemma eq_apps_head : forall p (ts : Tes p) q (us : Tes q) a b,
    apps a ts = apps b us -> nb_args a = nb_args b -> a = b.


  Lemma eq_apps_nb_args : forall p (ts : Tes p) q (us : Tes q) a b,
    apps a ts = apps b us -> nb_args a = nb_args b -> p = q.


  Lemma eq_apps_nb_args_sym : forall p (ts : Tes p) q (us : Tes q) a b,
    apps a ts = apps b us -> nb_args a = nb_args b -> q = p.


  Lemma eq_apps_args : forall p (ts : Tes p) q (us : Tes q) a b
    (h1 : apps a ts = apps b us) (h2 : nb_args a = nb_args b),
    ts = Vcast us (eq_apps_nb_args_sym h1 h2).


  Lemma eq_apps_fun_head : forall f p (ts : Tes p) g q (us : Tes q),
    apps (Fun f) ts = apps (Fun g) us -> f = g.


  Lemma eq_apps_fun_nb_args : forall f p (ts : Tes p) g q (us : Tes q),
    apps (Fun f) ts = apps (Fun g) us -> p = q.


  Lemma eq_apps_fun_nb_args_sym : forall f p (ts : Tes p) g q (us : Tes q),
    apps (Fun f) ts = apps (Fun g) us -> q = p.


  Lemma eq_apps_fun_args : forall f p (ts : Tes p) g q (us : Tes q)
    (h : apps (Fun f) ts = apps (Fun g) us),
    ts = Vcast us (eq_apps_fun_nb_args_sym h).

  Lemma eq_apps_nb_args_head : forall n (ts us : Tes n) t u,
    apps t ts = apps u us -> t = u.


  Lemma eq_apps_nb_args_args : forall n (ts us : Tes n) t u,
    apps t ts = apps u us -> ts = us.


Structure for sets of variables.


  Record Ens := mk_Ens {
    Ens_type : Type;
    Ens_empty : Ens_type;
    Ens_singleton : X -> Ens_type;
    Ens_add : X -> Ens_type -> Ens_type;
    Ens_union : Ens_type -> Ens_type -> Ens_type;
    Ens_remove : X -> Ens_type -> Ens_type;
    Ens_diff : Ens_type -> Ens_type -> Ens_type;
    Ens_In : X -> Ens_type -> Prop;
    Ens_mem : X -> Ens_type -> bool;
    Ens_fold : forall A, (X -> A -> A) -> Ens_type -> A -> A }.

Sets of free and bound variables of a term.


  Section fv.

    Variable ens_X : Ens.

    Notation empty := (Ens_empty ens_X).
    Notation singleton := (Ens_singleton ens_X).
    Notation union := (Ens_union ens_X).
    Notation remove := (Ens_remove ens_X).
    Notation add := (Ens_add ens_X).

    Fixpoint fv (t : Te) :=
      match t with
        | Var x => singleton x
        | Fun _ => empty
        | App u v => union (fv u) (fv v)
        | Lam x u => remove x (fv u)
      end.

    Fixpoint fvs {n} (ts : Tes n) :=
      match ts with
        | Vnil => empty
        | Vcons t ts' => union (fv t) (fvs ts')
      end.

    Fixpoint bv (t : Te) :=
      match t with
        | Var _ => empty
        | Fun _ => empty
        | App u v => union (bv u) (bv v)
        | Lam x u => add x (bv u)
      end.

  End fv.

Predicate saying if a relation on terms is monotone.


  Class Monotone R := {
    mon_app_l : Proper (R ==> Logic.eq ==> R) App;
    mon_app_r : Proper (Logic.eq ==> R ==> R) App;
    mon_lam : Proper (Logic.eq ==> R ==> R) Lam }.

  Global Instance eq_mon : Monotone eq.


Monotone closure of a relation.


  Section clos_mon.

    Variable R : relation Te.

    Inductive clos_mon : relation Te :=
    | m_step : forall u v, R u v -> clos_mon u v
    | m_app_l : forall v u u', clos_mon u u' -> clos_mon (App u v) (App u' v)
    | m_app_r : forall u v v', clos_mon v v' -> clos_mon (App u v) (App u v')
    | m_lam : forall x u u', clos_mon u u' -> clos_mon (Lam x u) (Lam x u').

  End clos_mon.

Supterm relation.


  Inductive supterm : relation Te :=
  | st_app_l : forall u v, supterm (App u v) u
  | st_app_r : forall u v, supterm (App u v) v
  | st_lam : forall x u, supterm (Lam x u) u.

Predicate saying if a relation is invariant on variables.


  Class VarInvL R := { var_inv_l : forall x u, R (Var x) u -> u = Var x }.

  Class VarInvR R := { var_inv_r : forall x u, R u (Var x) -> u = Var x }.

  Global Instance VarInvR_sym R : Symmetric R -> VarInvL R -> VarInvR R.


  Global Instance VarInvL_eq : VarInvL eq.


End term.


Tactics.

Tactic for unfolding the projections of the type Ens.
Tactic for doing induction on the size of a term.

Ltac ind_size1 u :=
  intro u; pattern u; apply ind_size1;
    [clear u; let x := fresh "x" in intro x
    |clear u; let f := fresh "f" in intro f
    |clear u; let u := fresh "u" in let v := fresh "v" in
      let hu := fresh "hu" in let hv := fresh "hv" in
        intros u v hu hv
    |clear u; let x := fresh "x" in let hu := fresh "hu" in intros x u hu].

End Def.

Structure for infinite sets of variables.


Module Type Var.

We assume given a set X for variables and a module XOrd providing a structure of decidable ordered set to X.

  Parameter X : Type.

  Declare Module Export XOrd : OrderedType
  with Definition t := X
  with Definition eq := @Logic.eq X.

Module providing finite sets of variables.

  Declare Module Export XSet : FSetInterface.S with Module E := XOrd.

  Notation ens_X :=
    (@mk_Ens X XSet.t empty singleton add union remove diff In mem fold).

We assume that X is infinite.

  Parameter var_notin : XSet.t -> X.

  Parameter var_notin_ok : forall xs, ~In (var_notin xs) xs.


  Declare Instance var_notin_e : Proper (Equal ==> Logic.eq) var_notin.

End Var.

Example of Var structure using natural numbers.


Module NatVar <: Var.

  Definition X := nat.

  Module XOrd := OrderedTypeEx.Nat_as_OT.

  Module Export XSet := FSetAVL.Make XOrd.

  Notation ens_X :=
    (@mk_Ens X XSet.t empty singleton add union remove diff In mem fold).

  Definition var_notin xs :=
    match max_elt xs with
      | Some k => S k
      | None => 0
    end.

  Lemma var_notin_ok xs : ~In (var_notin xs) xs.

  Module Export XSetUtil := FSetUtil.Make XSet.

  Instance var_notin_e : Proper (Equal ==> Logic.eq) var_notin.


End NatVar.

Structure on which we will define lambda-terms.


Module Type L_Struct.

We assume given a set F for constants and a module FOrd providing a structure of decidable ordered set to F.

  Parameter F : Type.

  Declare Module Export FOrd : OrderedType
  with Definition t := F
  with Definition eq := @Logic.eq F.

We assume given a Var structure.

  Declare Module Export V : Var.

Notations.

  Notation Te := (Te F X).
  Notation Tes := (vector Te).

  Notation Var := (@Var F X).
  Notation Fun := (@Fun F X).
  Notation App := (@App F X).
  Notation Lam := (@Lam F X).

  Notation not_lam := (@not_lam F X).
  Notation size := (@size F X).
  Notation apps := (@apps F X).
  Notation head := (@head F X).
  Notation nb_args := (@nb_args F X).
  Notation args := (@args F X).
  Notation fv := (@fv F X ens_X).
  Notation bv := (@bv F X ens_X).
  Notation fvs := (@fvs F X ens_X).
  Notation Monotone := (@Monotone F X).
  Notation clos_mon := (@clos_mon F X).
  Notation eq_term_dec := (@eq_term_dec F X FOrd.eq_dec XOrd.eq_dec).
  Notation beq_term := (bool_of_rel eq_term_dec).
  Notation supterm := (@supterm F X).

End L_Struct.

Properties of terms.


Module Make (Export L : L_Struct).

Properties of finite set of variables.

  Module Export XSetUtil := FSetUtil.Make XSet.

Tactic doing destruct (eq_dec x y) and unfolding XOrd.eq. Otherwise, Coq's tactic subst does not work.

  Ltac eq_dec x y :=
    unfold eqb; destruct (XOrd.eq_dec x y); unfold XOrd.eq in *.

Equivalence between boolean and propositional equality on variables.

  Lemma eqb_true_iff x y : eqb x y = true <-> x = y.

  Lemma eqb_false_iff x y : eqb x y = false <-> x <> y.

Equality on terms.


  Lemma beq_term_true_iff u v : beq_term u v = true <-> u = v.

  Lemma beq_term_false_iff u v : beq_term u v = false <-> u <> v.

  Lemma beq_term_refl u : beq_term u u = true.

  Lemma beq_term_var x y : beq_term (Var x) (Var y) = eqb x y.

Properties of monotone relations.

  Section mon_apps.

    Variables (R : relation Te) (R_mon : Monotone R).

    Global Instance mon_apps_l n : Proper (R ==> Logic.eq ==> R) (@apps n).


    Lemma mon_apps_app_cons : forall u u', R u u' ->
      forall p (ts : Tes p) q (vs : Tes q) t,
        R (apps t (Vapp ts (Vcons u vs))) (apps t (Vapp ts (Vcons u' vs))).

    Lemma mon_apps_replace : forall u u', R u u' ->
      forall n (ts : Tes n) t i (h1 h2 : i<n),
        R (apps t (Vreplace ts h1 u)) (apps t (Vreplace ts h2 u')).

  End mon_apps.

Tactic trying to simplify and possibly prove goals of the form ?R _ _ when ?R is Monotone.

  Ltac mon := repeat
    match goal with
      | |- ?R (App ?x _) (App ?x _) => apply mon_app_r; [class|refl|idtac]
      | |- ?R (App _ ?x) (App _ ?x) => apply mon_app_l; [class|idtac|refl]
      | |- ?R (Lam ?x _) (Lam ?x _) => apply mon_lam; [class|refl|idtac]
      | |- ?R (apps _ ?ts) (apps _ ?ts) => apply mon_apps_l; [class|idtac|refl]
      | |- ?R (apps ?t (Vapp ?ts (Vcons _ ?vs)))
              (apps ?t (Vapp ?ts (Vcons _ ?vs))) =>
        apply mon_apps_app_cons; [class|idtac]
      | |- ?R (apps ?t (Vreplace ?ts _ _)) (apps ?t (Vreplace ?ts _ _)) =>
        apply mon_apps_replace; [class|idtac]
      | |- ?R ?x ?y => hyp
    end.

Properties of Monotone.

Monotony is compatible with same.
clos_trans preserves Monotone.

  Instance clos_trans_mon R : Monotone R -> Monotone (R!).


clos_refl_trans preserves Monotone.

  Instance clos_refl_trans_mon R : Monotone R -> Monotone (R#).


clos_equiv preserves Monotone.

Properties of clos_mon.


  Instance monotone_clos_mon R : Monotone (clos_mon R).


  Lemma clos_mon_min R S : Monotone S -> R << S -> clos_mon R << S.

The monotone closure is compatible with relation inclusion and equivalence.
The closure by monotony distributes over union.

  Lemma clos_mon_union R S : clos_mon (R U S) == clos_mon R U clos_mon S.

Preservation of some properties by clos_mon.

Properties wrt free variables.


  Lemma notin_fv_lam x y u : y=x \/ ~In x (fv u) <-> ~In x (fv (Lam y u)).

  Lemma In_fvs_Vnth : forall x n (ts : Tes n) i (h : i<n),
    In x (fv (Vnth ts h)) -> In x (fvs ts).


The monotone closure preserves free variables.

  Instance fv_clos_mon : forall R,
    Proper (R --> Subset) fv -> Proper (clos_mon R --> Subset) fv.


  Instance fv_clos_mon_Equal : forall R,
    Proper (R ==> Equal) fv -> Proper (clos_mon R ==> Equal) fv.


  Instance fv_union : forall R S,
    Proper (R --> Subset) fv -> Proper (S --> Subset) fv ->
    Proper (R U S --> Subset) fv.


Properties of supterm.


  Lemma supterm_nth f : forall n (ts : Tes n) i (hi : i<n),
    supterm! (apps (Fun f) ts) (Vnth ts hi).

  Lemma supterm_wf : WF supterm.

  Section union.

    Variables (R : relation Te) (R_mon : Monotone R).

    Lemma supterm_R_mon_commut : supterm @ R << R @ supterm.

    Lemma tc_supterm_R_mon_commut : supterm! @ R << R @ supterm!.

    Lemma SN_supterm_R_mon : forall u, SN R u -> SN (supterm! U R) u.

    Lemma SN_st u v : SN R u -> supterm u v -> SN R v.

    Lemma SN_st_app_l u v : SN R (App u v) -> SN R u.

    Lemma SN_st_app_r u v : SN R (App u v) -> SN R v.

    Lemma SN_st_lam x u : SN R (Lam x u) -> SN R u.

    Lemma supterm_R_mon_wf : WF R -> WF (supterm! U R).

    Section restrict.

      Variables (P : set Te) (P_R : Proper (R ==> impl) P).

      Lemma restrict_tc_supterm_R_mon_wf :
        WF (restrict P R) -> WF (restrict P (supterm! U R)).

    End restrict.

    Lemma restrict_SN_tc_supterm_R_mon_wf : WF (restrict (SN R) (supterm! U R)).

  End union.

End Make.