# Library CoLoR.Term.WithArity.AUnif

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2008-01-22
syntactic unification

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

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

Ltac case_beq_symb := ASignature.case_beq_symb Sig.

unification problem

Definition eqn := ((term * term)%type).
Definition eqns := (list eqn).

Definition eqn_sub s (e : eqn) := (sub s (fst e), sub s (snd e)).

Definition solved_eqn := ((variable * term)%type).
Definition solved_eqns := (list solved_eqn).

Definition problem := (option ((solved_eqns * eqns)%type)).

Definition solved (p : problem) :=
match p with
| None
| Some (_, nil) => true
| _ => false
end.

Definition successfull (p : problem) :=
match p with
| Some (_, nil) => true
| _ => false
end.

Lemma successfull_solved : forall p, successfull p = true -> solved p = true.

variables of a list of equations

Definition vars_eqn (e : eqn) := union (vars (fst e)) (vars (snd e)).

Fixpoint vars_eqns l :=
match l with
| nil => empty
| e :: l' => union (vars_eqn e) (vars_eqns l')
end.

Lemma vars_eqns_app : forall l m,
vars_eqns (l ++ m) [=] union (vars_eqns l) (vars_eqns m).

Lemma vars_eqns_combine : forall n (us vs : terms n),
vars_eqns (combine (list_of_vec vs) (list_of_vec us))
[=] union (vars_vec vs) (vars_vec us).

Lemma mem_vars_sub_single : forall n (u : term) x v,
mem n (vars u) = false -> mem n (vars v) = false ->
mem n (vars (sub (single x v) u)) = false.

Lemma mem_vars_sub_single' : forall n (u v : term),
mem n (vars v) = false -> mem n (vars (sub (single n v) u)) = false.

Lemma vars_eqn_sub : forall x v e,
vars_eqn (eqn_sub (single x v) e) [=]
if mem x (vars_eqn e) then union (vars v) (remove x (vars_eqn e))
else vars_eqn e.

Lemma vars_eqns_subs : forall x v l,
vars_eqns (map (eqn_sub (single x v)) l) [=]
if mem x (vars_eqns l) then union (vars v) (remove x (vars_eqns l))
else vars_eqns l.

well-formed unification problems

Definition notin_eqn x (e : eqn) :=
mem x (vars (fst e)) = false /\ mem x (vars (snd e)) = false.

Definition notin_solved_eqn x (e : solved_eqn) :=
x <> fst e /\ mem x (vars (snd e)) = false.

Definition notin_vars_solved_eqn (v : term) (e : solved_eqn) :=
mem (fst e) (vars v) = false.

Fixpoint solved_eqns_wf (l : solved_eqns) :=
match l with
| nil => True
| (x, v) :: l' => mem x (vars v) = false
/\ lforall (notin_solved_eqn x) l' /\ solved_eqns_wf l'
/\ lforall (notin_vars_solved_eqn v) l'
end.

Definition notin l2 (e : solved_eqn) := lforall (notin_eqn (fst e)) l2.

Definition problem_wf (p : problem) :=
match p with
| Some (l1, l2) => solved_eqns_wf l1 /\ lforall (notin l2) l1
| _ => True
end.

Definition solved_eqn_sub s (e : solved_eqn) := (fst e, sub s (snd e)).

properties of well-formed problems

Lemma lforall_notin_solved_eqn_1 : forall n t, mem n (vars t) = false ->
forall l' l, lforall (notin ((t, Var n) :: l')) l ->
lforall (notin_solved_eqn n) (map (solved_eqn_sub (single n t)) l).

Lemma lforall_notin_solved_eqn_1' : forall n t, mem n (vars t) = false ->
forall l' l, lforall (notin ((Var n, t) :: l')) l ->
lforall (notin_solved_eqn n) (map (solved_eqn_sub (single n t)) l).

Lemma lforall_notin_solved_eqn_2 : forall n t, mem n (vars t) = false ->
forall x l, lforall (notin_solved_eqn n) l ->
lforall (notin_solved_eqn n) (map (solved_eqn_sub (single x t)) l).

Lemma lforall_notin_vars_solved_eqn_1 : forall n t0 t1 l' l,
lforall (notin ((Var n, t0) :: l')) l ->
lforall (notin_vars_solved_eqn t1) l ->
lforall (notin_vars_solved_eqn (sub (single n t0) t1))
(map (solved_eqn_sub (single n t0)) l).

Lemma lforall_notin_vars_solved_eqn_1' : forall n t0 t1 l' l,
lforall (notin ((t0, Var n) :: l')) l ->
lforall (notin_vars_solved_eqn t1) l ->
lforall (notin_vars_solved_eqn (sub (single n t0) t1))
(map (solved_eqn_sub (single n t0)) l).

Lemma lforall_notin_vars_solved_eqn_2 : forall n u l' l,
lforall (notin ((Var n, u) :: l')) l ->
lforall (notin_vars_solved_eqn u) (map (solved_eqn_sub (single n u)) l).

Lemma lforall_notin_vars_solved_eqn_2' : forall n u l' l,
lforall (notin ((u, Var n) :: l')) l ->
lforall (notin_vars_solved_eqn u) (map (solved_eqn_sub (single n u)) l).

Lemma solved_eqns_wf_map : forall n t, mem n (vars t) = false ->
forall l' l, solved_eqns_wf l -> lforall (notin ((Var n, t) :: l')) l ->
solved_eqns_wf (map (solved_eqn_sub (single n t)) l).

Lemma solved_eqns_wf_map' : forall n t, mem n (vars t) = false ->
forall l' l, solved_eqns_wf l -> lforall (notin ((t, Var n) :: l')) l ->
solved_eqns_wf (map (solved_eqn_sub (single n t)) l).

Lemma notin_map : forall x t, mem x (vars t) = false ->
forall l, notin (map (eqn_sub (single x t)) l) (x, t).

Lemma lforall_notin_eqn : forall x t, mem x (vars t) = false ->
forall n l, lforall (notin_eqn x) l ->
lforall (notin_eqn x) (map (eqn_sub (single n t)) l).

Lemma lforall_notin_r : forall x t l' l,
lforall (notin ((t, Var x) :: l')) l ->
lforall (notin (map (eqn_sub (single x t)) l'))
(map (solved_eqn_sub (single x t)) l).

Lemma lforall_notin_l : forall x t l' l,
lforall (notin ((Var x, t) :: l')) l ->
lforall (notin (map (eqn_sub (single x t)) l'))
(map (solved_eqn_sub (single x t)) l).

Lemma lforall_notin_eqn_combine : forall x n (v1 v2 : terms n),
mem x (vars_vec v1) = false -> mem x (vars_vec v2) = false ->
lforall (notin_eqn x) (combine (list_of_vec v1) (list_of_vec v2)).

step function

Notation beq_symb := (@beq_symb Sig).

Definition step (p : problem) :=
match p with
| Some (l1, e :: l2) =>
match e with
| (v, Var x) =>
if beq_term v (Var x) then Some (l1, l2)
else if mem x (vars v) then None
else Some ((x, v) :: List.map (solved_eqn_sub (single x v)) l1,
List.map (eqn_sub (single x v)) l2)
| (Var x, v) =>
if beq_term v (Var x) then Some (l1, l2)
else if mem x (vars v) then None
else Some ((x, v) :: List.map (solved_eqn_sub (single x v)) l1,
List.map (eqn_sub (single x v)) l2)
| (Fun f vs, Fun g us) =>
if beq_symb f g then
Some (l1, List.combine (list_of_vec vs) (list_of_vec us) ++ l2)
else None
end
| _ => p
end.

Fixpoint iter_step k (p : problem) :=
match k with
| 0 => p
| S k' => step (iter_step k' p)
end.

basic properties

Lemma iter_step_commut : forall k (p : problem),
iter_step k (step p) = step (iter_step k p).

Lemma successfull_elim : forall k p, successfull (iter_step k p) = true ->
exists l, iter_step k p = Some (l, nil).

Lemma successfull_preserved : forall k p,
successfull (iter_step k p) = true ->
forall l, l > k -> successfull (iter_step l p) = true.

Lemma unsuccessfull_preserved : forall k p,
iter_step k p = None -> forall l, l > k -> iter_step l p = None.

Lemma successfull_inv : forall k p,
successfull (iter_step k p) = true ->
forall l, l < k -> iter_step l p <> None.

size-based multiset ordering on equations

Notation nb_symb_occs := (@nb_symb_occs Sig).

Definition size e := nb_symb_occs (fst e) + nb_symb_occs (snd e).

Definition sizes l := list2multiset (List.map size l).

Definition sizes_lt l1 l2 := MultisetLt gt (sizes l1) (sizes l2).

Lemma wf_sizes_lt : well_founded sizes_lt.

number of distinct variables in equations
wellfounded ordering on equations

Definition lt : relation (eqns * eqns) :=
transp (lex (transp nb_vars_lt) nb_vars_eq (transp sizes_lt)).

Lemma wf_lt : well_founded lt.

Definition Lt l1 l2 := lt (l1, l1) (l2, l2).

Lemma wf_Lt : well_founded Lt.

Lemma Lt_eqns_subs_l : forall x v l, mem x (vars v) = false ->
Lt (map (eqn_sub (single x v)) l) ((Var x, v) :: l).

Lemma Lt_eqns_subs_r : forall x v l, mem x (vars v) = false ->
Lt (map (eqn_sub (single x v)) l) ((v, Var x) :: l).

Lemma Lt_cons : forall x l, Lt l (x :: l).

Lemma Lt_combine : forall f vs g us l, beq_symb f g = true ->
Lt (combine (list_of_vec vs) (list_of_vec us) ++ l)
((Fun f vs, Fun g us) :: l).

Definition Lt' (p1 p2 : problem) :=
match p1, p2 with
| None, Some _ => True
| Some (_, l1), Some (_, l2) => Lt l1 l2
| _, _ => False
end.

Lemma wf_Lt' : well_founded Lt'.

termination of iter_step

Lemma Lt_step : forall p, solved p = false -> Lt' (step p) p.

Lemma solved_inv : forall p, solved (step p) = false -> solved p = false.

Lemma wf_iter_step : forall p, exists k, solved (iter_step k p) = true.

the step function preserves well-formedness

Lemma step_wf : forall p, problem_wf p -> problem_wf (step p).
Opaque vars. Transparent vars.

Lemma iter_step_wf : forall p k, problem_wf p -> problem_wf (iter_step k p).

solutions of an unification problem

Definition is_sol_eqn s (e : eqn) := sub s (fst e) = sub s (snd e).
Definition is_sol_solved_eqn s (e : solved_eqn) := s (fst e) = sub s (snd e).

Definition is_sol_eqns s := lforall (is_sol_eqn s).
Definition is_sol_solved_eqns s := lforall (is_sol_solved_eqn s).

Definition is_sol s p :=
match p with
| None => False
| Some (l1, l2) => is_sol_solved_eqns s l1 /\ is_sol_eqns s l2
end.

Lemma is_sol_eqn_sub : forall s s' e,
is_sol_eqn s e -> is_sol_eqn (sub_comp s' s) e.

Lemma is_sol_solved_eqns_sub : forall s s' l,
is_sol_solved_eqns s l -> is_sol_solved_eqns (sub_comp s' s) l.

Lemma is_sol_sub : forall s s' p, is_sol s p -> is_sol (sub_comp s' s) p.

the step function preserves solutions

Lemma is_sol_solved_eqns_map : forall s n u, s n = sub s u ->
forall l, is_sol_solved_eqns s (map (solved_eqn_sub (single n u)) l)
<-> is_sol_solved_eqns s l.

Lemma is_sol_eqns_map : forall s x u, s x = sub s u ->
forall l, is_sol_eqns s (map (eqn_sub (single x u)) l) <-> is_sol_eqns s l.

Lemma lforall_is_sol_solved_eqn : forall s x u, s x = sub s u -> forall l,
lforall (is_sol_solved_eqn s) (map (solved_eqn_sub (single x u)) l)
<-> lforall (is_sol_solved_eqn s) l.

Lemma lforall_is_sol_eqn_combine : forall s n (v v0 : terms n),
lforall (is_sol_eqn s) (combine (list_of_vec v) (list_of_vec v0))
<-> Vmap (sub s) v = Vmap (sub s) v0.

Lemma step_correct : forall s p, is_sol s p <-> is_sol s (step p).
Opaque vars. Transparent vars.

Lemma iter_step_correct : forall s p k,
is_sol s p <-> is_sol s (iter_step k p).

extension of a substitution

Lemma is_sol_solved_eqns_extend : forall s n v l,
lforall (notin_solved_eqn n) l ->
is_sol_solved_eqns s l -> is_sol_solved_eqns (extend s n v) l.

Lemma is_sol_eqn_extend : forall s x (v : term) e,
is_sol_eqn s (eqn_sub (single x v) e) <->
is_sol_eqn (extend s x (sub s v)) e.

Lemma is_sol_eqns_extend : forall s x (v : term) l,
is_sol_eqns s (map (eqn_sub (single x v)) l) <->
is_sol_eqns (extend s x (sub s v)) l.

substitution corresponding to solved equations

Fixpoint subst_of_solved_eqns (l : solved_eqns) :=
match l with
| (x, v) :: l' => extend (subst_of_solved_eqns l') x v
| nil => id Sig
end.

Fixpoint dom (l : solved_eqns) :=
match l with
| (x, _) :: l' => add x (dom l')
| nil => empty
end.

Lemma dom_subst_of_solved_eqns : forall x l,
mem x (dom l) = false -> subst_of_solved_eqns l x = Var x.

Lemma lforall_notin_vars_solved_eqn_dom : forall x u l,
lforall (notin_vars_solved_eqn u) l ->
mem x (vars u) = true -> mem x (dom l) = false.

Lemma lforall_notin_vars_solved_eqn_mem : forall x u l,
lforall (notin_vars_solved_eqn u) l ->
mem x (dom l) = true -> mem x (vars u) = false.

Lemma sub_eq' : forall s1 s2 (t : term),
(forall x, mem x (vars t) = true -> s1 x = s2 x) -> sub s1 t = sub s2 t.

Lemma sub_eq_id' : forall s (t : term),
(forall x, mem x (vars t) = true -> s x = Var x) -> sub s t = t.

Lemma lforall_notin_solved_eqn_mem : forall n x l,
lforall (notin_solved_eqn n) l -> beq_nat x n = false ->
mem n (vars (subst_of_solved_eqns l x)) = false.

Lemma subst_of_solved_eqns_correct : forall l, solved_eqns_wf l ->
is_sol_solved_eqns (subst_of_solved_eqns l) l.

Lemma subst_of_solved_eqns_correct_problem : forall p l k, problem_wf p ->
iter_step k p = Some (l, nil) -> is_sol (subst_of_solved_eqns l) p.

Lemma successfull_is_sol : forall k p, problem_wf p ->
successfull (iter_step k p) = true -> exists s, is_sol s p.

most generality

Definition theta l (s : substitution) y :=
if mem y (dom l) then Var y else s y.

Lemma subst_of_solved_eqns_most_general :
forall s l, solved_eqns_wf l -> is_sol_solved_eqns s l ->
forall x, s x = sub (theta l s) (subst_of_solved_eqns l x).

Lemma iter_step_None :
forall p k, iter_step k p = None -> forall s, ~is_sol s p.

Lemma iter_step_solved_eqn_wf : forall p l k, problem_wf p ->
iter_step k p = Some (l, nil) -> solved_eqns_wf l.

Lemma iter_step_Some : forall p l k, problem_wf p ->
iter_step k p = Some (l, nil) -> is_sol (subst_of_solved_eqns l) p.

Lemma iter_step_most_general : forall p l k, problem_wf p ->
iter_step k p = Some (l, nil) -> forall s, is_sol s p ->
forall x, s x = sub (theta l s) (subst_of_solved_eqns l x).

Lemma iter_step_complete : forall p, problem_wf p ->
(exists s, is_sol s p) -> exists k, successfull (iter_step k p) = true.

Lemma iter_step_complete2 : forall p, problem_wf p ->
(forall s, ~is_sol s p) -> exists k, iter_step k p = None.

unifiability of two terms

Definition mk_problem u v : problem := Some (nil, (u,v)::nil).

Lemma wf_mk_problem : forall u v, problem_wf (mk_problem u v).

Definition unifiable u v := exists s, is_sol s (mk_problem u v).

Notation In := List.In.
Notation In_dec := (List.In_dec eq_nat_dec).
Notation vars := (@ATerm.vars Sig).

Lemma sub_eq_is_sol : forall s1 t1 s2 t2,
(forall x, In x (vars t1) -> In x (vars t2) -> False) ->
sub s1 t1 = sub s2 t2 -> unifiable t1 t2.

End S.