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.