# 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.

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.