Library CoLoR.Term.WithArity.AMatching

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Pierre-Yves Strub, 2009-04-09
  • Frederic Blanqui, 2009-11-02 (matches_dom)
Matching algorithm for ATerms.

Module VSF := AVariables.VarSetUtil.XSetFacts.
Module VS := AVariables.XSet.

Module VM := FMapAVL.Make (OrderedTypeEx.Nat_as_OT).
Module VMU := FMapUtil.Make VM.
Module VMF := VMU.XMapFacts.

Set Implicit Arguments.

Section Matching.
  Variable Sig : Signature.

  Notation term := (@ATerm.term Sig).
  Notation terms := (@vector term).
  Notation vars := (@AVariables.vars Sig).
  Notation vars_list := (@AVariables.vars_list Sig).
  Notation vars_vec := (@AVariables.vars_vec Sig _).

  Notation matching := (VM.t term) (only parsing).

  Notation beq_term := (@beq_term Sig).
  Notation beq_terms := (fun x y => beq_vec beq_term x y).

  Notation "x =X y" := (NatUtil.beq_nat x y) (at level 70, no associativity).
  Notation "f =S g" := (@beq_symb Sig f g) (at level 70, no associativity).
  Notation "t =T u" := (beq_term t u) (at level 70, no associativity).
  Notation "ts =V us" := (beq_terms ts us) (at level 70, no associativity).

  Local Hint Unfold is_true.

  Definition exmatch (m : matching) (x : variable) (t : term) :=
  match VM.find x m with
  | None => Some (VM.add x t m)
  | Some u => if t =T u then Some m else None
  end.

  Fixpoint matches_r (u t : term) (m : matching) : option matching :=
  match u, t with
  | Var y , _ => exmatch m y t
  | Fun g us, Fun f ts => if f =S g then Vfold2 m matches_r us ts else None
  | _ , _ => None
  end.

  Notation "\unopt_ ( x ) v" :=
    (match v with Some v' => v' | None => x end)
    (at level 8, v at level 36, x at level 50, format "\unopt_ ( x ) v").

  Definition subst_of_matching (m : matching) :=
    fun (x : variable) => \unopt_(Var x) (VM.find x m).

  Notation "\S ( θ )" := (subst_of_matching θ) (format "\S ( θ )").

  Definition matches (u t : term) :=
  match matches_r u t VM.empty with
  | None => None
  | Some m => Some \S(m)
  end.

  Notation "t ! θ" := (@sub Sig θ t) (at level 15).

  Lemma subst_of_matchingE :
    forall x m v, VM.find x m = Some v -> \S(m) x = v.

  Lemma vmap_eqb : forall x y, VMF.eqb x y = (x =X y).

Induction principle for matches_r when result is Some _
  Section MatchInd.
    Variable P : term -> term -> matching -> matching -> Prop.
    Variable Ps : forall nt nu,
      terms nt -> terms nu -> matching -> matching -> Prop.

    Hypothesis Hvar :
      forall x t θ θ', exmatch θ x t = Some θ' -> P (Var x) t θ θ'.

    Hypothesis Hfun :
      forall f g ts us θ θ',
           Vfold2 θ matches_r ts us = Some θ'
        -> Ps ts us θ θ'
        -> f = g
        -> P (Fun f ts) (Fun g us) θ θ'.

    Hypothesis Hnil :
      forall θ, Ps Vnil Vnil θ θ.

    Hypothesis Hcns :
      forall t nt (ts : terms nt) u nu (us : terms nu) θ θ' Ω,
           matches_r t u Ω = Some θ'
        -> P t u Ω θ'
        -> Vfold2 θ matches_r ts us = Some Ω
        -> Ps ts us θ Ω
        -> Ps (Vcons t ts) (Vcons u us) θ θ'.

    Notation "\matchesP" :=
      (forall u t θ θ', matches_r u t θ = Some θ' -> P u t θ θ').
    Notation "\matchesPs" :=
      (forall nu (us : terms nu) nt (ts : terms nt) θ θ',
        Vfold2 θ matches_r us ts = Some θ' -> Ps us ts θ θ').

    Lemma matches_some_ind : \matchesP /\ \matchesPs.
  End MatchInd.

  Section VarMin.
    Lemma exmatches_var_min :
      forall y t θ θ', exmatch θ y t = Some θ' ->
        forall x, VM.mem x θ' = VM.mem x θ || (y =X x).

    Notation "\matches_var_min" :=
      (forall u t θ θ', matches_r u t θ = Some θ' ->
        forall x, VM.mem x θ' = VM.mem x θ || VS.mem x (vars u)).

    Notation "\nmatches_var_min" :=
      (forall nu (us : terms nu) nt (ts : terms nt) θ θ',
        Vfold2 θ matches_r us ts = Some θ'
        -> forall x, VM.mem x θ' = VM.mem x θ || VS.mem x (vars_vec us)).

    Lemma matches_var_min_comb : \matches_var_min /\ \nmatches_var_min.

    Lemma matches_var_minP : \matches_var_min.

    Lemma nmatches_var_minP : \nmatches_var_min.
  End VarMin.

  Lemma matches_var_minadded :
    forall u t m m', matches_r u t m = Some m' ->
      forall x, VM.mem x m = false -> VM.mem x m' -> VS.mem x (vars u).

  Section MatchMon.
    Lemma exmatch_mon :
      forall θ θ' x t, exmatch θ x t = Some θ' ->
        forall y, VM.mem y θ -> VM.find y θ = VM.find y θ'.

    Notation "\matches_mon" :=
      (forall u t θ θ', matches_r u t θ = Some θ' ->
        forall x, VM.mem x θ -> VM.find x θ = VM.find x θ').

    Notation "\nmatches_mon" :=
      (forall nu (us : terms nu) nt (ts : terms nt) θ θ',
        Vfold2 θ matches_r us ts = Some θ'
        -> forall x, VM.mem x θ -> VM.find x θ = VM.find x θ').

    Lemma matches_mon_comb : \matches_mon /\ \nmatches_mon.

    Lemma matches_monP : \matches_mon.

    Lemma nmatches_monP : \nmatches_mon.
  End MatchMon.

  Lemma matches_submon :
    forall u t θ,
      u ! \S(θ) = t ->
      (forall x, VS.mem x (vars u) -> VM.mem x θ) ->
      forall u' t' θ', matches_r u' t' θ = Some θ' -> u ! \S(θ') = t.

  Lemma nmatches_submon :
    forall nu (us : terms nu) nt (ts : terms nt) θ,
      (Vmap (sub \S(θ)) us) =V ts ->
      (forall x, VS.mem x (vars_vec us) -> VM.mem x θ) ->
      forall u t θ', matches_r u t θ = Some θ' ->
        (Vmap (sub \S(θ')) us) =V ts.

  Section MatchCorrectness.
    Notation "\matches_correct" :=
      (forall u t θ θ', matches_r u t θ = Some θ' -> u ! \S(θ') = t).

    Notation "\nmatches_correct" :=
      (forall nu (us : terms nu) nt (ts : terms nt) θ θ',
        Vfold2 θ matches_r us ts = Some θ' -> (Vmap (sub \S(θ')) us) =V ts).

    Lemma matches_r_correct : \matches_correct /\ \nmatches_correct.

    Lemma matches_correct : forall u t θ, matches u t = Some θ -> u ! θ = t.
  End MatchCorrectness.

  Section MatchCompletness.
    Definition compose (m : matching) (θ : variable -> term) :=
      fun (x : variable) => \unopt_(θ x) (VM.find x m).

    Notation "m ⊕ θ" := (compose m θ) (at level 40, no associativity).

    Lemma composeI : forall x m θ, VM.find x m = None -> (m θ) x = θ x.

    Lemma composeE : forall x m v θ, VM.find x m = Some v -> (m θ) x = v.

    Notation "\matches_complete" :=
      (forall u t m, (exists θ, u ! (m θ) = t) -> matches_r u t m <> None).

    Notation "\nmatches_complete" :=
      (forall nu (us : terms nu) nt (ts : terms nt) m,
        (exists θ, (Vmap (sub (m θ)) us) =V ts) ->
        Vfold2 m matches_r us ts <> None).

    Lemma matches_extend_compatP :
      forall u t m m', matches_r u t m = Some m' ->
        forall θ, u ! (m θ) = t -> forall x, (m θ) x = (m' θ) x.

    Lemma nmatches_extend_compatP :
      forall nu (us : terms nu) nt (ts : terms nt) m m',
        Vfold2 m matches_r us ts = Some m' ->
        forall θ, Vmap (sub (m θ)) us =V ts ->
          forall x, (m θ) x = (m' θ) x.

    Lemma matches_r_complete : \matches_complete /\ \nmatches_complete.

    Lemma matches_complete :
      forall u t θ, u!θ = t -> matches u t <> None.

    Lemma matches_complete_ext :
      forall u t θ, u!θ = t ->
        exists Ω,
          ( matches u t = Some Ω
          /\ forall x, VS.mem x (vars u) -> θ x = Ω x).
  End MatchCompletness.


  Lemma matches_r_dom : forall u t m m' x, matches_r u t m = Some m' ->
    ~In x (ATerm.vars u) -> VM.mem x m' = VM.mem x m.

  Lemma matches_dom : forall u t s x,
    matches u t = Some s -> ~In x (ATerm.vars u) -> s x = Var x.

End Matching.