Library CoLoR.Term.WithArity.AContext

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sebastien Hinderer, 2004-02-09
  • Frederic Blanqui, 2005-02-17
one-hole contexts

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation terms := (vector term).

contexts

  Inductive context : Type :=
  | Hole : context
  | Cont : forall (f : Sig) (i j : nat), i + S j = arity f ->
    terms i -> context -> terms j -> context.


  Lemma cont_eq_intro : forall f f', f = f' -> forall c c', c = c' ->
    forall i v1 i' v1' (h1 : i'=i) j v2 (e : i+S j=arity f) j' v2' (h2 : j'=j)
      (e' : i'+S j'=arity f'), v1 = Vcast v1' h1 -> v2 = Vcast v2' h2 ->
      Cont e v1 c v2 = Cont e' v1' c' v2'.

replacement of the hole

  Fixpoint fill (c : context) (t : term) : term :=
    match c with
      | Hole => t
      | Cont H v1 c' v2 =>
        Fun _ (Vcast (Vapp v1 (Vcons (fill c' t) v2)) H)
    end.

context composition

  Fixpoint comp (C : context) : context -> context :=
    match C with
      | Hole => fun E => E
      | Cont H ts1 D ts2 => fun E => Cont H ts1 (comp D E) ts2
    end.

  Lemma fill_fill : forall C D u, fill C (fill D u) = fill (comp C D) u.

  Lemma comp_comp : forall C D E, comp (comp C D) E = comp C (comp D E).

  Lemma cont_case : forall c, c = Hole \/ exists d, exists f,
    exists i, exists vi, exists j, exists vj, exists e : i + S j = arity f,
      c = comp d (Cont e vi Hole vj).

properties of fill

  Lemma var_eq_fill : forall x c t, Var x = fill c t -> c = Hole /\ t = Var x.

  Lemma fun_eq_fill : forall f ts c u, Fun f ts = fill c u ->
    c = Hole \/ exists i, exists j, exists H : i + S j = arity f,
      exists ti, exists d, exists tj, c = Cont H ti d tj.

  Lemma fun_eq_nth_fill : forall f v i (h : i < arity f),
    let v1 := Vsub v (Veq_app_cons_aux1 h) in
      let v2 := Vsub v (Veq_app_cons_aux2 h) in
        let H := Veq_app_cons_aux3 h in
          let c := Cont H v1 Hole v2 in Fun f v = fill c (Vnth v h).

  Lemma fill_eq : forall t u c, fill c t = fill c u <-> t = u.

  Lemma comp_eq : forall c d e, comp c d = comp c e <-> d = e.

  Lemma size_fill : forall t c, size (fill c t) >= size t.

  Lemma wf_term : forall (t : term) c, t = fill c t -> c = Hole.

subterm ordering

  Definition subterm_eq u t := exists C, t = fill C u.

  Definition subterm u t := exists C, C <> Hole /\ t = fill C u.

  Definition supterm := transp subterm.

  Definition supterm_eq := transp subterm_eq.

  Global Instance subterm_eq_refl : Reflexive subterm_eq.


  Global Instance supterm_eq_refl : Reflexive supterm_eq.


  Lemma subterm_eq_var : forall u x, subterm_eq u (Var x) -> u = Var x.

  Lemma subterm_fun_elim : forall u f ts,
    subterm u (Fun f ts) -> exists t, Vin t ts /\ subterm_eq u t.

  Lemma subterm_fun : forall f ts u, Vin u ts -> subterm u (Fun f ts).

  Lemma subterm_size : forall t u : term, subterm t u -> size t < size u.

  Lemma subterm_strict : forall u t, subterm u t -> subterm_eq u t.

  Lemma subterm_noteq : forall u t, subterm_eq u t -> u <> t -> subterm u t.

  Lemma rc_subterm : subterm_eq == subterm%.

  Lemma rc_supterm : supterm_eq == supterm%.

  Lemma subterm_eq_split : forall t u, subterm_eq t u -> t = u \/ subterm t u.

transitivity of the subterm ordering

  Global Instance subterm_trans : Transitive subterm.


  Global Instance subterm_eq_trans : Transitive subterm_eq.


  Global Instance supterm_trans : Transitive supterm.


  Global Instance supterm_eq_trans : Transitive supterm_eq.


  Lemma subterm_trans_eq1 : forall t u v,
    subterm_eq t u -> subterm u v -> subterm t v.

  Lemma subterm_trans_eq2 : forall t u v,
    subterm t u -> subterm_eq u v -> subterm t v.

subterm-based induction principle

  Lemma forall_subterm_eq : forall (P : term -> Prop) t,
    (forall u, subterm_eq u t -> P u) -> P t.

  Lemma subterm_ind_sub : forall (P : term -> Prop)
    (IH : forall t, (forall u, subterm u t -> P u) -> P t),
    forall t u, subterm_eq u t -> P u.

  Lemma subterm_ind : forall (P : term -> Prop)
    (IH : forall t, (forall u, subterm u t -> P u) -> P t),
    forall t, P t.

boolean function deciding subterm_eq

  Fixpoint bsubterm_eq (t u : term) : bool :=
    match u with
      | Var _ => beq_term t u
      | Fun _ us => beq_term t u || bVexists (bsubterm_eq t) us
    end.

  Lemma bsubterm_eq_ok : forall t u, bsubterm_eq t u = true <-> subterm_eq t u.

  Definition bsupterm_eq t u := bsubterm_eq u t.

boolean function deciding subterm

  Definition bsubterm (t u : term) : bool :=
    match u with
      | Var x => false
      | Fun _ us => bVexists (bsubterm_eq t) us
    end.

  Lemma bsubterm_ok : forall t u, bsubterm t u = true <-> subterm t u.

  Definition bsupterm t u := bsubterm u t.

subterms and variables

  Lemma subterm_eq_vars : forall u t x,
    subterm_eq u t -> List.In x (vars u) -> List.In x (vars t).

  Lemma in_vars_subterm_eq : forall x t,
    List.In x (vars t) -> subterm_eq (Var x) t.

  Lemma in_vars_fun : forall x f ts,
    List.In x (vars (Fun f ts)) -> exists t, Vin t ts /\ subterm_eq (Var x) t.

variables of a context

  Fixpoint cvars (c : context) : variables :=
    match c with
      | Hole => List.nil
      | Cont H v1 c' v2 => vars_vec v1 ++ cvars c' ++ vars_vec v2
    end.

  Lemma vars_fill_elim : forall t c, vars (fill c t) [= cvars c ++ vars t.

  Lemma vars_fill_intro : forall t c, cvars c ++ vars t [= vars (fill c t).

symbols of a context

  Fixpoint csymbs (c : context) : list Sig :=
    match c with
      | Hole => List.nil
      | @Cont f _ _ _ v1 c' v2 =>
        f :: (symbs_vec v1 ++ csymbs c' ++ symbs_vec v2)
    end.

  Lemma symbs_fill_elim : forall t c, symbs (fill c t) [= csymbs c ++ symbs t.

  Lemma symbs_fill_intro : forall t c, csymbs c ++ symbs t [= symbs (fill c t).

End S.

declarations of implicit arguments