Library CoLoR.SemLab.ASemLab

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-06-22
semantic labelling (with ordered labels) (Zantema, Fundamenta Informaticae, 1995, volume 24, pages 89-105)

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

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

labels

  Variable L : Sig -> Type.
  Variable beq : forall f g, L f -> L g -> bool.
  Variable beq_ok : forall f (l m : L f), beq l m = true <-> l = m.

labelled signature

  Variable I : interpretation Sig.

  Notation int := (@term_int _ I).

  Record lab_symb : Type := mk {
    l_symb : Sig;
    l_lab : L l_symb }.

  Notation eq_symb_dec := (@eq_symb_dec Sig).

  Ltac Leqtac := repeat
    match goal with
      | H : @mk ?x _ = @mk ?x _ |- _ =>
        let h1 := fresh in
          (injection H; intro h1; ded (inj_existT eq_symb_dec h1);
            clear h1; clear H)
      | H : @mk _ _ = @mk _ _ |- _ =>
        let h1 := fresh in let h2 := fresh in
          (injection H; clear H; intros h1 h2; subst;
            ded (inj_existT eq_symb_dec h1); clear h1; subst)
    end.

  Definition beq_lab_symb (fl1 fl2 : lab_symb) :=
    let (f1,l1) := fl1 in let (f2,l2) := fl2 in beq_symb f1 f2 && beq l1 l2.

  Lemma beq_lab_symb_ok : forall fl1 fl2,
    beq_lab_symb fl1 fl2 = true <-> fl1 = fl2.

  Definition lab_arity (fl : lab_symb) := let (f,_) := fl in arity f.

  Definition lab_sig := mkSignature lab_arity beq_lab_symb_ok.

  Notation Sig' := lab_sig. Notation Fun' := (@Fun Sig').
  Notation term' := (ATerm.term Sig'). Notation terms' := (vector term').
  Notation rule' := (ATrs.rule Sig'). Notation rules' := (rules Sig').

labelling

  Variable pi : forall f : Sig, vector I (arity f) -> L f.

  Fixpoint lab v t :=
    match t with
      | Var x => Var x
      | Fun f ts => Fun' (mk (pi f (Vmap (int v) ts))) (Vmap (lab v) ts)
    end.

  Definition lab_rule v (a : rule) :=
    let (l,r) := a in mkRule (lab v l) (lab v r).

  Definition lab_rules R a := exists b, exists v, R b /\ a = lab_rule v b.

  Definition lab_sub v s (x : variable) := lab v (s x).

  Lemma lab_sub_eq : forall v s t,
    lab v (sub s t) = sub (lab_sub v s) (lab (beta v s) t).


  Lemma lab_fval : forall v t n, n > maxvar t -> lab (fval v n) t = lab v t.

  Lemma lab_rule_fval : forall v a n,
    n > maxvar_rule a -> lab_rule (fval v n) a = lab_rule v a.

  Notation fold_max := (@fold_max Sig).


  Lemma map_lab_rule_fval : forall v R n, n > maxvar_rules R ->
    map (lab_rule (fval v n)) R = map (lab_rule v) R.

ordering of labels

  Variable Lgt : forall f, relation (L f). Infix ">L" := Lgt (at level 50).

  Let Lge f := @Lgt f %. Infix ">=L" := Lge (at level 50).

  Definition Fun'_vars f (a : L f) := Fun' (mk a) (fresh_vars (arity f)).

  Definition decr f (a b : L f) := mkRule (Fun'_vars a) (Fun'_vars b).

  Definition Decr (rho : rule') :=
    exists f, exists a : L f, exists b, a >L b /\ rho = decr a b.

  Lemma Lge_Decr : forall f (ts : terms' (arity f)) (a b : L f),
    a >=L b -> red Decr # (Fun' (mk a) ts) (Fun' (mk b) ts).

unlabelling


  Definition F (f' : Sig') := let (f,_) := f' in f.

  Lemma HF : forall f', arity f' = arity (F f').

  Definition unlab := Ft HF.
  Definition unlab_rules := Frs HF.
  Definition unlab_rules_fin := Fl HF.

  Lemma Ft_epi : forall v t, unlab (lab v t) = t.

  Lemma Frs_iso : forall R, unlab_rules (lab_rules R) [=] R.

  Lemma red_Frs_Decr : red (unlab_rules Decr) << @eq term.

  Lemma rt_red_Frs_Decr : red (unlab_rules Decr) # << @eq term.

  Lemma red_mod_Frs_Decr : forall E,
    red (unlab_rules (union Decr (lab_rules E))) << red E %.

  Lemma rt_red_mod_Frs_Decr : forall E,
    red (unlab_rules (union Decr (lab_rules E))) # << red E #.

main theorem

  Variable Dge : relation I. Infix ">=D" := Dge (at level 50).

  Let Ige := IR I Dge. Infix ">=I" := Ige (at level 70).

  Variable pi_mon : forall f, Vmonotone (pi f) Dge (@Lge f).
  Variable I_mon : forall f, Vmonotone1 (fint I f) Dge.

  Section red.

    Variable R : set rule. Notation R' := (lab_rules R).

    Variable ge_compat : forall l r, R (mkRule l r) -> l >=I r.

    Lemma hd_red_lab : forall v t u,
      hd_red R t u -> hd_red_mod Decr R' (lab v t) (lab v u).

    Lemma red_lab : forall v t u,
      red R t u -> red_mod Decr R' (lab v t) (lab v u).

    Lemma rt_red_lab : forall v t u,
      red R # t u -> red_mod Decr R' # (lab v t) (lab v u).

    Lemma WF_red_lab : WF (red R) <-> WF (red_mod Decr R').

  End red.

rewriting modulo

  Section red_mod.

    Variables E R : set rule.

    Variable ge_compatE : forall l r, E (mkRule l r) -> l >=I r.
    Variable ge_compatR : forall l r, R (mkRule l r) -> l >=I r.

    Notation E' := (lab_rules E). Notation R' := (lab_rules R).

    Lemma red_mod_lab : forall v t u,
      red_mod E R t u -> red_mod (union Decr E') R' (lab v t) (lab v u).

    Lemma hd_red_mod_lab : forall v t u,
      hd_red_mod E R t u -> hd_red_mod (union Decr E') R' (lab v t) (lab v u).

    Lemma WF_red_mod_lab : WF (red_mod E R) <-> WF (red_mod (union Decr E') R').

    Lemma WF_hd_red_mod_lab :
      WF (hd_red_mod E R) <-> WF (hd_red_mod (union Decr E') R').

  End red_mod.

enumeration of labelled rules for a finite domain

  Section enum.

    Variable Is : list I.
    Variable Is_ok : forall x : I, In x Is.

    Fixpoint enum_tuple n : list (vector I n) :=
      match n with
        | 0 => cons Vnil nil
        | S p =>
          flat_map (fun ds => map (fun d => Vcons d ds) Is) (enum_tuple p)
      end.

    Lemma enum_tuple_complete : forall n (ds : vector I n),
      In ds (enum_tuple n).


    Definition enum R :=
      flat_map (fun ds => map (lab_rule (val_of_vec I ds)) R)
      (enum_tuple (S (maxvar_rules R))).

    Lemma enum_correct : forall R a, In a (enum R) -> lab_rules (of_list R) a.

    Lemma enum_complete : forall R a, lab_rules (of_list R) a -> In a (enum R).

    Infix "[=]" := equiv.

    Lemma lab_rules_enum : forall R, lab_rules (of_list R) [=] of_list (enum R).


enumeration of labelled symbols

    Variable Fs : list Sig.
    Variable Fs_ok : forall x, In x Fs.

    Variable Ls : forall f, list (L f).
    Variable Ls_ok : forall f (x : L f), In x (Ls f).

    Definition Fs_lab := flat_map (fun f => map (@mk f) (Ls f)) Fs.

    Lemma Fs_lab_ok : forall f : Sig', In f Fs_lab.

enumeration of Decr rules

    Variable L2s : forall f, list (L f * L f).
    Variable L2s_ok : forall f (x y : L f), x >L y <-> In (x,y) (L2s f).

    Definition enum_Decr := flat_map (fun f =>
      map (fun x : L f * L f => let (a,b) := x in decr a b) (L2s f)) Fs.

    Notation D' := enum_Decr.

    Lemma enum_Decr_correct : forall x, In x D' -> Decr x.

    Lemma enum_Decr_complete : forall x, Decr x -> In x D'.

    Lemma Rules_enum_Decr : of_list D' [=] Decr.

main theorems (finite versions)

    Import ATrs. Notation rules := (rules Sig).

    Variable bge : term -> term -> bool.
    Variable bge_ok : rel_of_bool bge << Ige.

    Section bge.

      Variable R : rules.
      Variable bge_compat : forallb (brule bge) R = true.

      Lemma ge_compat : forall l r, In (mkRule l r) R -> l >=I r.

    End bge.


    Section red_mod.

      Variables E R : rules.

      Notation E' := (enum E). Notation R' := (enum R).

      Variable bge_compatE : forallb (brule bge) E = true.
      Variable bge_compatR : forallb (brule bge) R = true.

      Notation ge_compatE := (ge_compat bge_compatE).
      Notation ge_compatR := (ge_compat bge_compatR).

      Lemma WF_red_lab_fin : WF (red R) <-> WF (red_mod D' R').

      Import List.

      Lemma WF_red_mod_lab_fin :
        WF (red_mod E R) <-> WF (red_mod (D' ++ E') R').

      Lemma WF_hd_red_mod_lab_fin :
        WF (hd_red_mod E R) <-> WF (hd_red_mod (D' ++ E') R').

    End red_mod.

    Lemma WF_red_unlab_fin : forall R,
      WF (red (unlab_rules_fin R)) -> WF (red R).

    Lemma WF_red_mod_unlab_fin : forall E R,
      WF (red_mod (unlab_rules_fin E) (unlab_rules_fin R)) -> WF (red_mod E R).

    Lemma WF_hd_red_mod_unlab_fin : forall E R,
      WF (hd_red_mod (unlab_rules_fin E) (unlab_rules_fin R))
      -> WF (hd_red_mod E R).

  End enum.

End S.


basic module type for semantic labellings

Module Type Base.

  Parameter Sig : Signature.

  Parameter L : Sig -> Type.
  Parameter beq : forall f g, L f -> L g -> bool.
  Parameter beq_ok : forall f (l m : L f), beq l m = true <-> l = m.

  Parameter I : interpretation Sig.

  Parameter pi : forall f : Sig, vector I (arity f) -> L f.

End Base.

module type for semantic labellings with unordered labels

Module Type SemLab.

  Include Base.

  Parameter beqI : term Sig -> term Sig -> bool.
  Parameter beqI_ok : rel_of_bool beqI << IR I (@eq I).

End SemLab.

module type for semantic labellings with ordered labels

Module Type OrdSemLab.

  Include SemLab.

  Parameter Dge : relation I.
  Parameter bge : term Sig -> term Sig -> bool.
  Parameter bge_ok : rel_of_bool bge << IR I Dge.
  Parameter I_mon : forall f, Vmonotone1 (fint I f) Dge.

  Notation "t '>=I' u" := (IR I Dge t u) (at level 70).

  Parameter Lgt : forall f, relation (L f).

  Infix ">L" := Lgt (at level 50).

  Parameter pi_mon : forall f, Vmonotone (pi f) Dge (@Lgt f%).

End OrdSemLab.

functor providing equality-ordered labels

Module Ord (SL : SemLab) <: OrdSemLab.

  Include SL.

  Definition Dge := @eq I.
  Definition bge := beqI.
  Definition bge_ok := beqI_ok.

  Lemma I_mon : forall f, Vmonotone1 (fint I f) Dge.

  Definition Lgt (f : Sig) (_ _ : L f) := False.

  Lemma Lge_is_eq : forall f a b, (@Lgt f%) a b <-> a = b.

  Lemma pi_mon : forall f, Vmonotone (pi f) Dge (@Lgt f%).

  Notation "t '>=I' u" := (IR I Dge t u) (at level 70).

  Notation Sig' := (lab_sig Sig beq_ok).

  Lemma Decr_empty : Decr beq_ok Lgt [=] empty.

End Ord.

module type for finite semantic labellings with unordered labels

Module Type FinSemLab.

  Include SemLab.

  Parameter Fs : list Sig.
  Parameter Fs_ok : forall x : Sig, In x Fs.

  Parameter Is : list I.
  Parameter Is_ok : forall x : I, In x Is.

  Parameter Ls : forall f, list (L f).
  Parameter Ls_ok : forall f (x : L f), In x (Ls f).

End FinSemLab.

module type for finite semantic labellings with ordered labels

Module Type FinOrdSemLab.

  Include OrdSemLab.

  Parameter Fs : list Sig.
  Parameter Fs_ok : forall x : Sig, In x Fs.

  Parameter Is : list I.
  Parameter Is_ok : forall x : I, In x Is.

  Parameter Ls : forall f, list (L f).
  Parameter Ls_ok : forall f (x : L f), In x (Ls f).

  Parameter L2s : forall f, list (L f * L f).
  Parameter L2s_ok : forall f (x y : L f), x >L y <-> In (x,y) (L2s f).

End FinOrdSemLab.

functor providing equality-ordered labels

Module FinOrd (Import FSL : FinSemLab) <: FinOrdSemLab.

  Include (Ord FSL).

  Definition Fs := Fs.
  Definition Fs_ok := Fs_ok.

  Definition Is := Is.
  Definition Is_ok := Is_ok.

  Definition Ls := Ls.
  Definition Ls_ok := Ls_ok.

  Definition L2s : forall f, list (L f * L f) := fun _ => nil.

  Lemma L2s_ok : forall f (x y : L f), Lgt x y <-> In (x,y) (L2s f).

  Lemma enum_Decr_empty : enum_Decr beq_ok Fs L2s = nil.

End FinOrd.

functor providing the properties of a semantic labelling with ordered labels

Import ARules.

Module OrdSemLabProps (Import OSL : OrdSemLab).

  Notation Decr := (Decr beq_ok Lgt).
  Notation lab_rules := (lab_rules beq_ok pi).

  Section props.

    Variables E R : set (rule Sig).

    Variable ge_compatE : forall l r, E (mkRule l r) -> l >=I r.
    Variable ge_compatR : forall l r, R (mkRule l r) -> l >=I r.

    Lemma WF_red_mod_lab : WF (red_mod E R)
      <-> WF (red_mod (union Decr (lab_rules E)) (lab_rules R)).

    Lemma WF_hd_red_mod_lab : WF (hd_red_mod E R)
      <-> WF (hd_red_mod (union Decr (lab_rules E)) (lab_rules R)).

    Lemma WF_red_lab : WF (red R) <-> WF (red_mod Decr (lab_rules R)).

  End props.

End OrdSemLabProps.

functor providing the properties of a semantic labelling with unordered labels

Module SemLabProps (SL : SemLab).

  Module Import OSL := Ord SL.

  Module Import Props := OrdSemLabProps OSL.

  Section props.

    Variables E R : set (rule Sig).

    Variable ge_compatE : forall l r, E (mkRule l r) -> l >=I r.
    Variable ge_compatR : forall l r, R (mkRule l r) -> l >=I r.

    Lemma WF_red_mod_lab : WF (red_mod E R)
      <-> WF (red_mod (lab_rules E) (lab_rules R)).

    Lemma WF_hd_red_mod_lab : WF (hd_red_mod E R)
      <-> WF (hd_red_mod (lab_rules E) (lab_rules R)).

    Lemma WF_red_lab : WF (red R) <-> WF (red (lab_rules R)).

  End props.

End SemLabProps.

functor providing the properties of a finite semantic labelling with ordered labels

Import ATrs. Infix "++" := app.
Module FinOrdSemLabProps (Import FOSL : FinOrdSemLab).

  Module LabSig.

    Definition Sig := lab_sig Sig beq_ok.
    Definition Fs := Fs_lab Fs Ls.
    Definition Fs_ok := Fs_lab_ok beq_ok Fs_ok Ls_ok.

    Notation unlab_rules := (unlab_rules_fin Sig beq_ok).

    Ltac unlab :=
      match goal with
        | |- WF (red_mod _ _) => apply (WF_red_mod_unlab_fin beq_ok)
        | |- WF (hd_red_mod _ _) => apply (WF_hd_red_mod_unlab_fin beq_ok)
        | |- WF (red _) => apply (WF_red_unlab_fin beq_ok)
      end.

  End LabSig.

  Notation Decr := (enum_Decr beq_ok Fs L2s).
  Notation lab_rules := (enum beq_ok pi Is).

  Section props.

    Variables E R : rules Sig.

    Variable bge_compatE : forallb (brule bge) E = true.
    Variable bge_compatR : forallb (brule bge) R = true.

    Lemma WF_red_mod_lab : WF (red_mod E R)
      <-> WF (red_mod (Decr ++ lab_rules E) (lab_rules R)).

    Lemma WF_hd_red_mod_lab : WF (hd_red_mod E R)
      <-> WF (hd_red_mod (Decr ++ lab_rules E) (lab_rules R)).

    Lemma WF_red_lab : WF (red R) <-> WF (red_mod Decr (lab_rules R)).

  End props.

  Ltac semlab :=
    match goal with
      | |- WF (red_mod _ _) => rewrite WF_red_mod_lab;
        [ idtac
        | check_eq || fail 10 "some relative rule is not in the model"
        | check_eq || fail 10 "some rule is not in the model"]
      | |- WF (hd_red_mod _ _) => rewrite WF_hd_red_mod_lab;
        [ idtac
        | check_eq || fail 10 "some relative rule is not in the model"]
      | |- WF (red _) => rewrite WF_red_lab;
        [ idtac
        | check_eq || fail 10 "some rule is not in the model"]
    end.

End FinOrdSemLabProps.

functor providing the properties of a finite semantic labelling with unordered labels

Module FinSemLabProps (FSL : FinSemLab).

  Module Import FOSL := FinOrd FSL.

  Module Import Props := FinOrdSemLabProps FOSL.

  Module LabSig := LabSig.

  Import FSL.

  Section props.

    Variables E R : rules Sig.

    Variable bge_compatE : forallb (brule bge) E = true.
    Variable bge_compatR : forallb (brule bge) R = true.

    Lemma WF_red_mod_lab : WF (red_mod E R)
      <-> WF (red_mod (lab_rules E) (lab_rules R)).

    Lemma WF_hd_red_mod_lab : WF (hd_red_mod E R)
      <-> WF (hd_red_mod (lab_rules E) (lab_rules R)).

    Lemma WF_red_lab : WF (red R) <-> WF (red (lab_rules R)).

  End props.

  Ltac semlab :=
    match goal with
      | |- WF (red_mod _ _) => rewrite WF_red_mod_lab;
        [ idtac
        | check_eq || fail 10 "some relative rule is not in the model"
        | check_eq || fail 10 "some rule is not in the model"]
      | |- WF (hd_red_mod _ _) => rewrite WF_hd_red_mod_lab;
        [ idtac
        | check_eq || fail 10 "some relative rule is not in the model"]
      | |- WF (red _) => rewrite WF_red_lab;
        [idtac
        | check_eq || fail 10 "some rule is not in the model"]
    end.

End FinSemLabProps.