Library unification.free_unif
Add LoadPath "basis".
Add LoadPath "list_extensions".
Add LoadPath "term_algebra".
Add LoadPath "term_orderings".
Add LoadPath "ac_matching".
Require Import Arith.
Require Import Wf_nat.
Require Import Wellfounded.
Require Import Max.
Require Import Min.
Require Import Bool_nat.
Require Import List.
Require Import Multiset.
Require Import closure.
Require Import more_list.
Require Import list_permut.
Require Import list_sort.
Require Import dickson.
Require Import Relations.
Require Import term.
Module Make (T1: term.Term)
(OF1 : ordered_set.S with Definition A := T1.symbol)
(OX1 : ordered_set.S with Definition A := T1.variable).
Module Import T := T1.
Module Term_eq_dec : decidable_set.S with Definition A:= term
with Definition eq_dec := eq_term_dec.
Definition A := term.
Definition eq_dec := eq_term_dec.
End Term_eq_dec.
Import F.
Import X.
Inductive exc (A : Set) : Set :=
| Normal : A -> exc A
| Not_appliable : A -> exc A
| No_solution : exc A.
Definition bind (A : Set) (f : A -> exc A) (x : exc A) : (exc A) :=
match x with
| Normal a => f a
| Not_appliable a => Not_appliable A a
| No_solution => @No_solution A
end.
Record unification_problem : Set :=
mk_pb
{
solved_part : substitution;
unsolved_part : list (term * term)
}.
Definition combine (A : Set) (l : list (A * A)) (l1 l2 : list A) : length l1 = length l2 -> list (A*A).
Proof.
intros B l l1; induction l1 as [ | h1 t1];
intros l2 L; destruct l2 as [ | h2 t2].
exact l.
discriminate.
discriminate.
refine ((h1,h2) :: (IHt1 t2) (plus_reg_l _ _ 1 L)).
Defined.
Lemma combine_proof :
forall A l l1 l2 (L : length l1 = length l2) (L' : length l1 = length l2),
combine A l l1 l2 L = combine A l l1 l2 L'.
Proof.
intros B l l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] L L'.
trivial.
discriminate.
discriminate.
simpl; apply (f_equal (fun l => (t1, t2) :: l)); refine (IHl1 l2 _ _).
Qed.
Lemma combine_nil : forall A l (L : length nil = length nil), combine A l nil nil L = l.
Proof.
trivial.
Qed.
Lemma combine_cons :
forall A l h1 l1 h2 l2 (L : length l1 = length l2) (L' : length (h1 :: l1) = length (h2 :: l2)),
combine A l (h1 :: l1) (h2 :: l2) L' = (h1,h2) :: combine A l l1 l2 L.
Proof.
intros B l h1 l1 h2 l2 L L'; simpl;
apply (f_equal (fun l => (h1, h2) :: l));
refine (combine_proof B l l1 l2 _ _).
Qed.
Function decomposition_step (pb : unification_problem) : exc unification_problem :=
match pb.(unsolved_part) with
| nil => @Not_appliable _ pb
| (s,t) :: l =>
if (eq_term_dec s t : sumbool _ _)
then Normal _ (mk_pb pb.(solved_part) l)
else
match s, t with
| Var x, Var y =>
let x_maps_to_y := (x, t) :: nil in
let solved_part' :=
map_subst (fun _ v_sigma => apply_subst ((x,t) :: nil) v_sigma)
pb.(solved_part) in
let l' := map (fun uv =>
match uv with
| (u, v) => (apply_subst ((x,t) :: nil) u,
apply_subst ((x,t) :: nil) v)
end) l in
match find eq_variable_dec x solved_part' with
| Some x_val => Normal _ (mk_pb ((x, t) :: solved_part') ((t, x_val) :: l'))
| None => Normal _ (mk_pb ((x, t) :: solved_part') l')
end
| Var x, (Term _ _ as u) =>
match find eq_variable_dec x pb.(solved_part) with
| None => Normal _ (mk_pb ((x,u) :: pb.(solved_part)) l)
| Some x_val =>
if lt_ge_dec (T.size u) (T.size x_val)
then Normal _ (mk_pb ((x,u) :: pb.(solved_part)) ((x_val,u) :: l))
else Normal _ (mk_pb pb.(solved_part) ((x_val,u) :: l))
end
| (Term _ _ as u), Var x =>
match find eq_variable_dec x pb.(solved_part) with
| None => Normal _ (mk_pb ((x,u) :: pb.(solved_part)) l)
| Some x_val =>
if lt_ge_dec (T.size u) (T.size x_val)
then Normal _ (mk_pb ((x,u) :: pb.(solved_part)) ((x_val,u) :: l))
else Normal _ (mk_pb pb.(solved_part) ((x_val,u) :: l))
end
| Term f l1, Term g l2 =>
if eq_symbol_dec f g
then
match eq_nat_dec (length l1) (length l2) with
| left L => Normal _ (mk_pb pb.(solved_part) (combine _ l l1 l2 L))
| right _ => @No_solution _
end
else @No_solution _
end
end.
Definition is_a_solution pb theta :=
(forall s t, In (s,t) pb.(unsolved_part) -> apply_subst theta s = apply_subst theta t)
/\
(forall x, match find eq_variable_dec x pb.(solved_part) with
| Some x_val => apply_subst theta (Var x) = apply_subst theta x_val
| None => True
end).
Module DecVar := decidable_set.Convert (X).
Module VSet <: list_set.S with Definition EDS.A := variable :=
list_set.Make (DecVar).
Ltac unfold_types :=
unfold VSet.LP.EDS.A, DecVar.A, variable in *.
Ltac destruct_set S S1 S2 :=
destruct (VSet.union_12 _ _ _ S) as [S1 | S2]; clear S.
Fixpoint set_of_variables (t : term) : VSet.t :=
match t with
| Var v => VSet.singleton v
| Term _ l =>
let set_of_variables_list :=
(fix set_of_variables_list (l : list term) {struct l} : VSet.t :=
match l with
| nil => VSet.empty
| t :: lt => VSet.union (set_of_variables t) (set_of_variables_list lt)
end) in
set_of_variables_list l
end.
Fixpoint set_of_variables_list (l : list term) : VSet.t :=
match l with
| nil => VSet.empty
| t :: lt => VSet.union (set_of_variables t) (set_of_variables_list lt)
end.
Fixpoint set_of_variables_in_unsolved_part (l : list (term * term)) : VSet.t :=
match l with
| nil => VSet.empty
| (s,t) :: l => VSet.union (VSet.union (set_of_variables s) (set_of_variables t))
(set_of_variables_in_unsolved_part l)
end.
Fixpoint domain_of_subst (sigma : substitution) : VSet.t :=
match sigma with
| nil => VSet.empty
| (x,_) :: sigma => VSet.add x (domain_of_subst sigma)
end.
Fixpoint set_of_variables_in_range_of_subst (sigma : substitution) : VSet.t :=
match sigma with
| nil => VSet.empty
| (_,t) :: sigma => VSet.union (set_of_variables t)
(set_of_variables_in_range_of_subst sigma)
end.
Lemma apply_subst_outside_dom :
forall sigma t, VSet.eq_set (VSet.inter (domain_of_subst sigma) (set_of_variables t))
VSet.empty ->
apply_subst sigma t = t.
Proof.
intros sigma t; pattern t; apply term_rec3; clear t.
intros v; induction sigma as [ | [x t] sigma]; trivial.
intro; simpl; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst v; assert (H' : VSet.mem x VSet.empty).
setoid_rewrite <- (H x); apply VSet.inter_12;
[ simpl; apply VSet.add_1 | left; reflexivity].
contradiction.
apply IHsigma; intro z; split; [intro z_in_x_dom_sig | intro z_in_empty].
setoid_rewrite <- (H z); apply VSet.inter_12.
simpl; apply VSet.add_2; apply (VSet.inter_1 _ _ _ z_in_x_dom_sig).
apply (VSet.inter_2 _ _ _ z_in_x_dom_sig).
contradiction.
intros f l IH H; simpl; simpl in H; apply (f_equal (fun l => Term f l)); induction l as [ | s l].
trivial.
simpl; rewrite (IH s); [rewrite IHl; trivial | left; trivial | idtac ].
intros; apply IH; trivial; right; trivial.
intro z; split; [intro z_in_dom_sig_l | intro z_in_empty].
setoid_rewrite <- (H z); apply VSet.inter_12.
simpl; apply (VSet.inter_1 _ _ _ z_in_dom_sig_l).
apply VSet.union_2; apply (VSet.inter_2 _ _ _ z_in_dom_sig_l).
contradiction.
intro z; split; [intro z_in_dom_sig_s | intro z_in_empty].
setoid_rewrite <- (H z); apply VSet.inter_12.
simpl; apply (VSet.inter_1 _ _ _ z_in_dom_sig_s).
apply VSet.union_1; apply (VSet.inter_2 _ _ _ z_in_dom_sig_s).
contradiction.
Qed.
Lemma occ_var_is_a_subterm_at_pos :
forall x t, VSet.mem x (set_of_variables t) ->
exists p, subterm_at_pos t p = Some (Var x).
Proof.
intros x t; pattern t; apply term_rec3; clear t.
intros v; simpl; intros [x_eq_v | x_in_nil]; [idtac | contradiction].
exists (@nil nat);
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A , DecVar.eq_A in *; subst; trivial.
intros f l IH x_in_l;
assert (H : exists s, exists i, In s l /\ nth_error l i = Some s
/\ VSet.mem x (set_of_variables s)).
clear IH; simpl in x_in_l; induction l as [ | t l]; [contradiction | idtac].
destruct_set x_in_l x_in_t x_in_l'.
exists t; exists 0; split; [left; trivial | split; trivial; simpl].
destruct (IHl x_in_l') as [s [i [s_in_l [s_eq_li x_in_s]]]]; exists s; exists (S i).
split; [right; trivial | split; trivial].
destruct H as [s [i [s_in_l [s_eq_li x_in_s]]]].
destruct (IH s s_in_l x_in_s) as [p H].
exists (i :: p); simpl; rewrite s_eq_li; rewrite H; trivial.
Qed.
Lemma find_map_subst :
forall x y t sigma,
match find eq_variable_dec x sigma with
| None =>
find eq_variable_dec x
(map_subst
(fun (_ : variable) v_sigma =>
apply_subst ((y, t) :: nil) v_sigma) sigma) = None
| Some x_val =>
find eq_variable_dec x
(map_subst
(fun (_ : variable) v_sigma =>
apply_subst ((y, t) :: nil) v_sigma) sigma) =
Some (apply_subst ((y, t) :: nil) x_val)
end.
Proof.
intros x y s sigma; generalize x y s; clear x y s;
induction sigma as [ | [z u] sigma]; intros x y s; simpl; trivial.
destruct (eq_variable_dec x z) as [x_eq_z | x_diff_z]; trivial.
apply IHsigma.
Qed.
Lemma decomposition_step_is_complete :
forall l sigma theta, is_a_solution (mk_pb sigma l) theta ->
match decomposition_step (mk_pb sigma l) with
| Normal pb' => is_a_solution pb' theta
| No_solution => False
| Not_appliable pb' => is_a_solution pb' theta
end.
Proof.
intros [ | [s t] l] sigma theta;
unfold decomposition_step; simpl unsolved_part; cbv iota beta; trivial.
destruct (eq_term_dec s t) as [s_eq_t | s_diff_t].
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma]; split; [intros; apply Hl; right | intros; apply Hsigma]; trivial.
destruct s as [ x | f l1 ]; destruct t as [ y | g l2 ].
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
assert (Hx := find_map_subst x x (Var y) sigma).
destruct (find eq_variable_dec x sigma) as [x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma;
simpl solved_part; rewrite Hx.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma];
assert (Htheta : forall t, apply_subst theta t = apply_subst theta (apply_subst ((x, Var y) :: nil) t)).
intro t; pattern t; apply term_rec3; clear t; [intros v | intros f l'].
simpl; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst v; apply (Hl (Var x) (Var y) (or_introl _ (refl_equal _))).
trivial.
intros IH; simpl; apply (f_equal (fun l => Term f l)); induction l' as [ | s' l']; trivial.
simpl; rewrite (IH s' (or_introl _ (refl_equal _))); rewrite IHl'; trivial;
intros; apply IH; right; trivial.
split.
intros s t H; destruct (in_inv H) as [s_t_eq_y_x_val' | s_t_in_l']; clear H.
assert (H':=Hsigma x); rewrite x_sigma in H';
injection s_t_eq_y_x_val'; clear s_t_eq_y_x_val'; intros; subst s t;
rewrite <- (Hl _ _ (or_introl _ (refl_equal _))); rewrite H'; apply Htheta.
setoid_rewrite in_map_iff in s_t_in_l'; destruct s_t_in_l' as [[s' t'] [H s'_t'_in_l]];
injection H; intros; subst; clear H; do 2 rewrite <- Htheta;
apply Hl; right; trivial.
trivial.
intro z; simpl; destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; apply (Hl (Var x) (Var y) (or_introl _ (refl_equal _))).
assert (z_sigma : forall z', z' = z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
assert (Hz := find_map_subst z x (Var y) sigma);
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma; rewrite Hz; trivial.
rewrite <- Htheta; generalize (Hsigma z); rewrite z_sigma; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma];
assert (Htheta : forall t, apply_subst theta t = apply_subst theta (apply_subst ((x, Var y) :: nil) t)).
intro t; pattern t; apply term_rec3; clear t; [intros v | intros f l'].
simpl; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst v; apply (Hl (Var x) (Var y) (or_introl _ (refl_equal _))).
trivial.
intros IH; simpl; apply (f_equal (fun l => Term f l)); induction l' as [ | s' l']; trivial.
simpl; rewrite (IH s' (or_introl _ (refl_equal _))); rewrite IHl'; trivial;
intros; apply IH; right; trivial.
split.
intros s t s_t_in_l'; setoid_rewrite in_map_iff in s_t_in_l';
destruct s_t_in_l' as [[s' t'] [H s'_t'_in_l]];
injection H; intros; subst; clear H; do 2 rewrite <- Htheta;
apply Hl; right; trivial.
intro z; simpl; destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; apply (Hl (Var x) (Var y) (or_introl _ (refl_equal _))).
assert (z_sigma : forall z', z' = z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
assert (Hz := find_map_subst z x (Var y) sigma);
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma; rewrite Hz; trivial.
rewrite <- Htheta; generalize (Hsigma z); rewrite z_sigma; trivial.
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
destruct (find eq_variable_dec x sigma) as [x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma;
intros [Hl Hsigma].
destruct (lt_ge_dec (T.size (Term g l2)) (T.size x_val)) as [L | L].
simpl; split.
intros s t [s_t_eq_x_val_g_l2 | s_t_in_l].
injection s_t_eq_x_val_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta (Var x)).
generalize (Hsigma x); rewrite x_sigma; intro; apply sym_eq; trivial.
apply Hl; left; trivial.
apply Hl; right; trivial.
intro z; destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; apply (Hl _ _ (or_introl _ (refl_equal _))).
apply (Hsigma z).
simpl; split.
intros s t [s_t_eq_x_val_g_l2 | s_t_in_l].
injection s_t_eq_x_val_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta (Var x)).
generalize (Hsigma x); rewrite x_sigma; intro; apply sym_eq; trivial.
apply Hl; left; trivial.
apply Hl; right; trivial.
intro z; apply (Hsigma z).
simpl; split.
intros s t s_t_in_l.
apply Hl; right; trivial.
intro z; destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; apply (Hl _ _ (or_introl _ (refl_equal _))).
apply (Hsigma z).
assert (y_sigma : forall y', y'=y ->
find eq_variable_dec y' sigma = find eq_variable_dec y sigma).
intros; subst; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
destruct (find eq_variable_dec y sigma) as [y_val | ];
generalize (y_sigma _ (refl_equal _)); clear y_sigma; intro y_sigma;
intros [Hl Hsigma].
destruct (lt_ge_dec (T.size (Term f l1)) (T.size y_val)) as [L | L].
simpl; split.
intros s t [s_t_eq_y_val_f_l1 | s_t_in_l].
injection s_t_eq_y_val_f_l1; intros; subst s t; apply trans_eq with (apply_subst theta (Var y)).
generalize (Hsigma y); rewrite y_sigma; intro; apply sym_eq; trivial.
apply sym_eq; apply Hl; left; trivial.
apply Hl; right; trivial.
intro z; destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
subst z; apply sym_eq; apply (Hl _ _ (or_introl _ (refl_equal _))).
apply (Hsigma z).
simpl; split.
intros s t [s_t_eq_y_val_f_l1 | s_t_in_l].
injection s_t_eq_y_val_f_l1; intros; subst s t; apply trans_eq with (apply_subst theta (Var y)).
generalize (Hsigma y); rewrite y_sigma; intro; apply sym_eq; trivial.
apply sym_eq; apply Hl; left; trivial.
apply Hl; right; trivial.
intro z; apply (Hsigma z).
simpl; split.
intros s t s_t_in_l.
apply Hl; right; trivial.
intro z; destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
subst z; apply sym_eq; apply (Hl _ _ (or_introl _ (refl_equal _))).
apply (Hsigma z).
destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g].
destruct (eq_nat_dec (length l1) (length l2)) as [ L | L ];
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma].
split; trivial.
assert (Hl' : forall s t, In (s,t) l -> apply_subst theta s = apply_subst theta t).
intros; apply Hl; right; trivial.
assert (Hl12 : map (apply_subst theta) l1 = map (apply_subst theta) l2).
generalize (Hl _ _ (or_introl _ (refl_equal _))); simpl;
intro H; injection H; intros; trivial.
clear Hsigma; generalize l2 l L Hl' Hl12; clear s_diff_t l2 l L Hl Hl' Hl12;
induction l1 as [ | s1 l1]; intros [ | s2 l2] l L Hl Hl12.
intros s t; simpl; intros s_t_in_l; apply Hl; trivial.
discriminate.
discriminate.
intros s t [s_t_eq_s1_s2 | s_t_in_l1_l2_l].
injection s_t_eq_s1_s2; simpl in Hl12; injection Hl12; intros; subst s t; trivial.
refine (IHl1 l2 l _ _ _ _ _ s_t_in_l1_l2_l); trivial; simpl in Hl12; injection Hl12; intros; trivial.
generalize (Hl _ _ (or_introl _ (refl_equal _))); simpl;
intro H; injection H; intros H' _; apply L;
rewrite <- (length_map (apply_subst theta)); rewrite H'; apply length_map.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl _]; apply f_diff_g.
generalize (Hl _ _ (or_introl _ (refl_equal _))); simpl;
intro H; injection H; intros _ H'; trivial.
Qed.
Lemma decomposition_step_is_sound :
forall l sigma theta,
match decomposition_step (mk_pb sigma l) with
| Normal pb' => is_a_solution pb' theta -> is_a_solution (mk_pb sigma l) theta
| No_solution => is_a_solution (mk_pb sigma l) theta -> False
| Not_appliable pb' => is_a_solution pb' theta -> is_a_solution (mk_pb sigma l) theta
end.
Proof.
intros [ | [s t] l] sigma theta;
unfold decomposition_step; simpl unsolved_part; cbv iota beta; trivial.
destruct (eq_term_dec s t) as [s_eq_t | s_diff_t].
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma]; split; [idtac | intros; apply Hsigma; trivial].
intros s' t' [s'_t'_eq_s_t | s'_t'_in_l]; [idtac | apply Hl; trivial].
injection s'_t'_eq_s_t; intros; subst s s' t'; trivial.
destruct s as [ x | f l1 ]; destruct t as [ y | g l2 ].
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
assert (Hx := find_map_subst x x (Var y) sigma).
destruct (find eq_variable_dec x sigma) as [x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma;
simpl solved_part; rewrite Hx.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma].
assert (x_theta_eq_y_theta : apply_subst theta (Var x) = apply_subst theta (Var y)).
generalize (Hsigma x); simpl;
destruct (eq_variable_dec x x) as [_ | x_diff_x]; [idtac | absurd (x=x)]; trivial.
assert (Htheta : forall t, apply_subst theta t = apply_subst theta (apply_subst ((x, Var y) :: nil) t)).
intro t; pattern t; apply term_rec3; clear t; [intros v | intros f l'].
simpl; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst v; trivial.
trivial.
intros IH; simpl; apply (f_equal (fun l => Term f l)); induction l' as [ | s' l']; trivial.
simpl; rewrite (IH s' (or_introl _ (refl_equal _))); rewrite IHl'; trivial;
intros; apply IH; right; trivial.
split.
intros s t [s_t_eq_x_y | s_t_in_l].
injection s_t_eq_x_y; intros; subst; trivial.
do 2 (apply sym_eq; rewrite Htheta).
apply Hl; right.
apply (in_map (B:= term*term)
(fun (uv : term * term) =>
let (u,v) := uv in
(apply_subst ((x,Var y) :: nil) u,
apply_subst ((x,Var y) :: nil) v)) _ _ s_t_in_l).
intro z; generalize (Hsigma z); simpl;
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; rewrite x_sigma; intro H; rewrite H;
apply sym_eq; rewrite Htheta; apply sym_eq; apply Hl; left; trivial.
assert (z_sigma : forall z', z' = z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
assert (Hz := find_map_subst z x (Var y) sigma);
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma; trivial.
rewrite Hz; intro H; rewrite H; rewrite <- Htheta; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma].
assert (x_theta_eq_y_theta : apply_subst theta (Var x) = apply_subst theta (Var y)).
generalize (Hsigma x); simpl;
destruct (eq_variable_dec x x) as [_ | x_diff_x]; [idtac | absurd (x=x)]; trivial.
assert (Htheta : forall t, apply_subst theta t = apply_subst theta (apply_subst ((x, Var y) :: nil) t)).
intro t; pattern t; apply term_rec3; clear t; [intros v | intros f l'].
simpl; destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
subst v; trivial.
trivial.
intros IH; simpl; apply (f_equal (fun l => Term f l)); induction l' as [ | s' l']; trivial.
simpl; rewrite (IH s' (or_introl _ (refl_equal _))); rewrite IHl'; trivial;
intros; apply IH; right; trivial.
split.
intros s t [s_t_eq_x_y | s_t_in_l].
injection s_t_eq_x_y; intros; subst; trivial.
do 2 (apply sym_eq; rewrite Htheta).
apply Hl;
apply (in_map (B:= term*term)
(fun (uv : term * term) =>
let (u,v) := uv in
(apply_subst ((x,Var y) :: nil) u,
apply_subst ((x,Var y) :: nil) v)) _ _ s_t_in_l).
intro z; generalize (Hsigma z); simpl;
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; rewrite x_sigma; trivial.
assert (z_sigma : forall z', z' = z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
assert (Hz := find_map_subst z x (Var y) sigma);
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma; trivial.
rewrite Hz; intro H; rewrite H; rewrite <- Htheta; trivial.
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
destruct (find eq_variable_dec x sigma) as [x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma.
destruct (lt_ge_dec (T.size (Term g l2)) (T.size x_val)) as [L | L];
intros [Hl Hsigma].
simpl; split.
intros s t [s_t_eq_x_g_l2 | s_t_in_l].
injection s_t_eq_x_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta x_val).
generalize (Hsigma x); simpl; rewrite x_sigma;
destruct (eq_variable_dec x x) as [ _ | x_diff_x]; [idtac | absurd (x=x); trivial].
intro H; rewrite H; apply sym_eq; apply Hl; left; trivial.
apply Hl; left; trivial.
apply Hl; right; trivial.
intro z; generalize (Hsigma z); simpl; destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; intro H; rewrite H; rewrite x_sigma.
apply sym_eq; apply Hl; left; trivial.
trivial.
simpl; split.
intros s t [s_t_eq_x_g_l2 | s_t_in_l].
injection s_t_eq_x_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta x_val).
generalize (Hsigma x); simpl; rewrite x_sigma; intro; trivial.
apply Hl; left; trivial.
apply Hl; right; trivial.
intro z; apply (Hsigma z).
simpl; intros [Hl Hsigma]; split.
intros s t [s_t_eq_x_g_l2 | s_t_in_l].
injection s_t_eq_x_g_l2; intros; subst s t;
generalize (Hsigma x); simpl;
destruct (eq_variable_dec x x) as [ _ | x_diff_x]; [idtac | absurd (x=x) ]; trivial.
apply Hl; trivial.
intro z; generalize (Hsigma z); simpl; destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; intro H; rewrite H; rewrite x_sigma; trivial.
trivial.
assert (y_sigma : forall y', y'=y ->
find eq_variable_dec y' sigma = find eq_variable_dec y sigma).
intros; subst; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
destruct (find eq_variable_dec y sigma) as [y_val | ];
generalize (y_sigma _ (refl_equal _)); clear y_sigma; intro y_sigma.
destruct (lt_ge_dec (T.size (Term f l1)) (T.size y_val)) as [L | L];
intros [Hl Hsigma].
simpl; split.
intros s t [s_t_eq_f_l1_y | s_t_in_l].
injection s_t_eq_f_l1_y; intros; subst s t; apply trans_eq with (apply_subst theta y_val).
apply sym_eq; apply Hl; left; trivial.
generalize (Hsigma y); simpl; rewrite y_sigma;
destruct (eq_variable_dec y y) as [ _ | y_diff_y]; [idtac | absurd (y=y); trivial].
intro H; rewrite H; apply Hl; left; trivial.
apply Hl; right; trivial.
intro z; generalize (Hsigma z); simpl; destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
subst z; intro H; rewrite H; rewrite y_sigma.
apply sym_eq; apply Hl; left; trivial.
trivial.
simpl; split.
intros s t [s_t_eq_f_l1_y | s_t_in_l].
injection s_t_eq_f_l1_y; intros; subst s t; apply trans_eq with (apply_subst theta y_val).
apply sym_eq; apply Hl; left; trivial.
generalize (Hsigma y); simpl; rewrite y_sigma; simpl; intro; apply sym_eq; trivial.
apply Hl; right; trivial.
intro z; apply (Hsigma z).
simpl; intros [Hl Hsigma]; split.
intros s t [s_t_eq_f_l1_y | s_t_in_l].
injection s_t_eq_f_l1_y; intros; subst s t;
generalize (Hsigma y); simpl;
destruct (eq_variable_dec y y) as [ _ | y_diff_y]; [idtac | absurd (y=y) ]; trivial.
simpl; intro; apply sym_eq; trivial.
apply Hl; trivial.
intro z; generalize (Hsigma z); simpl; destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
subst z; intro H; rewrite H; rewrite y_sigma; trivial.
trivial.
destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g].
destruct (eq_nat_dec (length l1) (length l2)) as [ L | L ].
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma].
split; trivial.
assert ((forall s t, In (s,t) l -> apply_subst theta s = apply_subst theta t) /\
map (apply_subst theta) l1 = map (apply_subst theta) l2).
generalize l2 l L Hl; clear l2 L l Hl s_diff_t; induction l1 as [ | s1 l1];
intros [ | s2 l2] l L Hl.
split; trivial; apply Hl; trivial.
discriminate.
discriminate.
simpl in L; injection L; intro L'.
assert (Hl' : forall s t : term, In (s, t) (combine term l l1 l2 L') ->
apply_subst theta s = apply_subst theta t).
intros s t H; apply Hl; simpl; right.
generalize l1 l2 l L L' H; clear H; intro k1;
induction k1 as [ | u1 k1]; intros [ | u2 k2] k K K' H;
trivial.
discriminate.
discriminate.
simpl; simpl in H; destruct H as [ H | H];
[left; trivial | right; refine (IHk1 k2 k _ _ H)].
split.
destruct (IHl1 l2 l L' Hl'); trivial.
simpl; rewrite (Hl s1 s2); [idtac | left; trivial].
apply (f_equal (fun l => apply_subst theta s2 :: l));
destruct (IHl1 l2 l L' Hl'); trivial.
intros s t [s_t_eq_f_l1_g_l2 | s_t_in_l].
injection s_t_eq_f_l1_g_l2; intros; subst; simpl; destruct H as [ _ H ]; rewrite H; subst; trivial.
destruct H as [ H _ ]; apply H; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma].
apply L; do 2 (apply sym_eq; rewrite <- (length_map (apply_subst theta)));
assert (Abs := Hl _ _ (or_introl _ (refl_equal _))); simpl in Abs; injection Abs;
intros H _; rewrite H; trivial.
unfold is_a_solution; simpl solved_part; simpl unsolved_part;
intros [Hl Hsigma].
apply f_diff_g; assert (Abs := Hl _ _ (or_introl _ (refl_equal _))); simpl in Abs; injection Abs;
intros _ H; rewrite H; trivial.
Qed.
Definition is_a_solved_var x pb :=
match find eq_variable_dec x pb.(solved_part) with
| None => False
| Some _ =>
~ VSet.mem x (set_of_variables_in_unsolved_part pb.(unsolved_part))
/\ ~ VSet.mem x (set_of_variables_in_range_of_subst pb.(solved_part))
end.
Lemma not_solved_var :
forall sigma l x, ~is_a_solved_var x (mk_pb sigma l) <->
(match find eq_variable_dec x sigma with
| None => True
| Some _ =>
VSet.mem x (set_of_variables_in_unsolved_part l)
\/ VSet.mem x (set_of_variables_in_range_of_subst sigma)
end).
Proof.
intros sigma l x; unfold is_a_solved_var;
simpl solved_part; simpl unsolved_part;
destruct (find eq_variable_dec x sigma) as [x_val | ]; split.
intros H; destruct (VSet.mem_dec x (set_of_variables_in_unsolved_part l))
as [x_in_l | x_not_in_l].
left; trivial.
destruct (VSet.mem_dec x (set_of_variables_in_range_of_subst sigma))
as [x_in_sigma | x_not_in_sigma].
right; trivial.
generalize (H (conj x_not_in_l x_not_in_sigma)); contradiction.
intros [x_in_l | x_in_sigma] [x_not_in_l x_not_in_sigma].
apply x_not_in_l; trivial.
apply x_not_in_sigma; trivial.
trivial.
intros _ H; trivial.
Qed.
Lemma is_a_solved_var_dec :
forall pb x, {is_a_solved_var x pb}+{~is_a_solved_var x pb}.
Proof.
intros [sigma l] x; unfold is_a_solved_var;
simpl solved_part; simpl unsolved_part;
destruct (find eq_variable_dec x sigma).
destruct (VSet.mem_dec x (set_of_variables_in_unsolved_part l))
as [ x_in_l | x_not_in_l ].
right; intros [ H _]; apply H; trivial.
destruct (VSet.mem_dec x (set_of_variables_in_range_of_subst sigma))
as [ x_in_sigma | x_not_in_sigma ].
right; intros [ _ H]; apply H; trivial.
left; split; trivial.
right; intro; trivial.
Qed.
Lemma is_a_not_solved_var_dec :
forall pb x, {~is_a_solved_var x pb}+{~~is_a_solved_var x pb}.
Proof.
intros pb x; destruct (is_a_solved_var_dec pb x) as [x_is_solved | x_is_not_solved].
right; intro x_is_not_solved; apply x_is_not_solved; trivial.
left; trivial.
Qed.
A measure on lists based on a measure on elements.
Module TermMul := dickson.Make(Term_eq_dec).
Fixpoint list_size_mul (A : Set) (siz : A -> nat) (l : list A) {struct l} : list nat :=
match l with
| nil => @nil nat
| h :: tl => (siz h) :: (list_size_mul A siz tl)
end.
Definition lt_mul : (relation (list nat)) :=
closure.trans_clos (NatMul.multiset_extension_step lt).
Definition size_of_unsolved_part pb :=
list_size_mul _
(fun s_t => match s_t with (s,t) => max (size s) (size t) end)
pb.(unsolved_part).
Definition size_of_solved_part pb :=
list_size_mul _
(fun x => match find eq_variable_dec x pb.(solved_part) with
Some x_val => size x_val
| None => 0
end)
(VSet.support (domain_of_subst pb.(solved_part))).
Definition nb_var_eq_of_unsolved_part pb :=
list_size (fun s_t => match s_t with (s,t) => match s, t with
| Var _, _ => 1
| _ , Var _ => 1
| _, _ => 0
end end)
pb.(unsolved_part).
Lemma VSet_compat :
forall pb e e', VSet.EDS.eq_A e e' ->
((fun v : variable => ~ is_a_solved_var v pb) e <->
(fun v : variable => ~ is_a_solved_var v pb) e').
Proof.
unfold VSet.EDS.eq_A, DecVar.eq_A.
intros; subst; split; intro; assumption.
Qed.
Definition phi1 pb :=
VSet.cardinal (VSet.filter (fun v : variable => ~is_a_solved_var v pb)
(is_a_not_solved_var_dec pb)
(VSet.union
(set_of_variables_in_unsolved_part pb.(unsolved_part))
(VSet.union
(domain_of_subst pb.(solved_part))
(set_of_variables_in_range_of_subst pb.(solved_part))))
(VSet_compat pb)).
Definition phi2 pb := size_of_solved_part pb ++ size_of_unsolved_part pb.
Definition phi3 pb := nb_var_eq_of_unsolved_part pb.
Definition measure_for_unif_pb pb := (phi1 pb, (phi2 pb, phi3 pb)).
Definition lt_ms :=
fun p123 q123 =>
match p123, q123 with
(p1,(p2,p3)), (q1,(q2,q3)) =>
if eq_nat_dec p1 q1
then
if (NatMul.LP.permut_dec p2 q2)
then p3 < q3
else lt_mul p2 q2
else p1 < q1
end.
Definition lt_pb pb pb' :=
lt_ms (measure_for_unif_pb pb) (measure_for_unif_pb pb').
Lemma lex_lt : forall p1 p2 p3 q1 q2 q3,
p1 < q1 -> lt_ms (p1,(p2,p3)) (q1,(q2,q3)).
Proof.
intros p1 p2 p3 q1 q2 q3 p1_lt_q1; unfold lt_ms.
destruct (eq_nat_dec p1 q1) as [p1_eq_q1 | p1_diff_q1]; trivial.
absurd (S p1 <= p1); subst; trivial; auto with arith.
Qed.
Lemma lex_le_lt : forall p1 p2 p3 q1 q2 q3,
p1 <= q1 -> lt_mul p2 q2 -> lt_ms (p1,(p2,p3)) (q1,(q2,q3)).
Proof.
intros p1 p2 p3 q1 q2 q3 p1_le_q1 p2_lt_q2; unfold lt_ms.
destruct (eq_nat_dec p1 q1) as [p1_eq_q1 | p1_diff_q1].
destruct (NatMul.LP.permut_dec p2 q2) as [p2_eq_q2 | p2_diff_q2]; trivial.
assert (lt_dec : forall n m, {n < m}+{~n<m}).
intros n m; destruct (le_lt_dec m n).
right; auto with arith.
left; trivial.
assert False.
destruct (@NatMul.multiset_closure lt lt_dec lt_trans _ _ p2_lt_q2)
as [pq2 [p2' [Pp2 [Pq2 [pq2_diff_nil [p2'_lt_q2' H]]]]]].
assert (p2'_eq_q2' : NatMul.LP.permut (NatMul.appendn pq2)
(NatMul.consn pq2)).
setoid_rewrite (NatMul.LP.permut_app2 p2').
transitivity p2.
symmetry; trivial.
transitivity q2; trivial.
destruct pq2 as [ | [a la] pq2].
apply pq2_diff_nil; trivial.
apply H with a.
intros; auto with arith.
simpl; left; reflexivity.
setoid_rewrite (NatMul.LP.mem_permut_mem a p2'_eq_q2'); simpl; left; trivial.
reflexivity.
contradiction.
destruct (lt_ge_dec p1 q1) as [p1_lt_q1 | p1_ge_q1]; trivial.
absurd (p1 = q1); trivial.
apply le_antisym; trivial.
Qed.
Lemma lex_le_meq_lt :
forall p1 p2 p3 q1 q2 q3,
p1 <= q1 -> NatMul.LP.permut p2 q2 -> p3 < q3 ->
lt_ms (p1,(p2,p3)) (q1,(q2,q3)).
Proof.
intros p1 p2 p3 q1 q2 q3 p1_le_q1 p2_eq_q2 p3_lt_q3; unfold lt_ms.
destruct (eq_nat_dec p1 q1) as [p1_eq_q1 | p1_diff_q1].
destruct (NatMul.LP.permut_dec p2 q2) as [_ | p2_diff_q2]; trivial.
absurd (NatMul.LP.permut p2 q2); trivial.
destruct (lt_ge_dec p1 q1) as [p1_lt_q1 | p1_ge_q1]; trivial.
absurd (p1 = q1); trivial.
apply le_antisym; trivial.
Qed.
Lemma wf_lt_ms : well_founded lt_ms.
unfold well_founded, lt_ms.
intros [p [q r]]; generalize q r; clear q r; pattern p.
refine (well_founded_ind lt_wf _ _ p).
clear p; intros p IHp q; unfold lt_mul.
pattern q; apply well_founded_ind with (list nat)
(trans_clos (NatMul.multiset_extension_step lt)).
apply closure.wf_trans; apply NatMul.dickson; apply Wf_nat.lt_wf.
clear q; intros q IHq r; pattern r;
refine (well_founded_ind Wf_nat.lt_wf _ _ r).
clear r; intros r IHr; apply Acc_intro.
intros [p' [q' r']]; destruct (eq_nat_dec p' p) as [p'_eq_p | p'_diff_p].
subst p'; destruct (NatMul.LP.permut_dec q' q) as [q'_eq_q | q'_diff_q].
intro r'_lt_r; assert (Acc_p_q_r' := IHr _ r'_lt_r).
apply Acc_intro; intros [p'' [q'' r'']].
destruct (eq_nat_dec p'' p) as [p''_eq_p | p''_diff_p].
subst p''; destruct (NatMul.LP.permut_dec q'' q') as [q''_eq_q' | q''_diff_q'].
intro r''_lt_r'; refine (Acc_inv Acc_p_q_r' _ _).
destruct (eq_nat_dec p p) as [ _ | p_diff_p]; [idtac | absurd (p=p); trivial].
destruct (NatMul.LP.permut_dec q'' q) as [q''_eq_q | q''_diff_q]; trivial.
absurd (NatMul.LP.permut q'' q); trivial.
transitivity q'; trivial.
intro q''_lt_q'; apply IHq.
generalize q q'_eq_q; clear q IHq IHr q'_eq_q Acc_p_q_r' q''_diff_q';
induction q''_lt_q' as [q'' q' q''_lt_q' | q'' q' q4 q''_lt_q' q'_lt_q4].
intros q q'_eq_q; apply closure.t_step;
apply NatMul.list_permut_multiset_extension_step_2 with q'; trivial.
intros q q4_eq_q; apply closure.t_trans with q'; trivial.
apply IHq'_lt_q4; trivial.
intro p''_lt_p; apply IHp; trivial.
intro q'_lt_q; apply IHq; trivial.
intro p'_lt_p; apply IHp; trivial.
Qed.
Lemma wf_lt_pb : well_founded lt_pb.
Proof.
unfold lt_pb;
apply (wf_inverse_image unification_problem _ lt_ms measure_for_unif_pb wf_lt_ms).
Qed.
Lemma remove_trivial_eq_decreases :
forall s l sigma, lt_pb (mk_pb sigma l) (mk_pb sigma ((s,s) :: l)).
Proof.
intros s l sigma;
unfold lt_pb, measure_for_unif_pb; apply lex_le_lt.
unfold phi1; apply VSet.cardinal_subset; apply VSet.subset_filter.
apply VSet.union_compat_subset_1.
simpl; intro v; apply VSet.union_2; trivial.
intro v; do 2 setoid_rewrite not_solved_var; simpl;
destruct (find eq_variable_dec v sigma) as [x_val | ]; [idtac | trivial].
intros [v_in_l | v_in_sigma].
left; apply VSet.union_2; trivial.
right; trivial.
unfold lt_mul, phi2, size_of_unsolved_part, size_of_solved_part; simpl.
apply closure.t_step;
refine (@NatMul.rmv_case lt _ _ (list_size_mul _
(fun x =>
match find eq_variable_dec x sigma with
| Some x_val => size x_val
| None => 0
end) (VSet.support (domain_of_subst sigma)) ++
list_size_mul (term * term)
(fun s_t : term * term =>
let (s0, t) := s_t in max (size s0) (size t)) l)
nil (max (size s) (size s)) _ _ _).
intros; contradiction.
reflexivity.
symmetry.
setoid_rewrite <- NatMul.LP.permut_cons_inside; reflexivity.
Qed.
Lemma domain_of_subst_map_subst :
forall sigma f, domain_of_subst (map_subst f sigma) = domain_of_subst sigma.
Proof.
intros sigma f;
induction sigma as [ | [x t] sigma]; simpl; trivial; rewrite IHsigma; trivial.
Qed.
Lemma solved_var_inc_not_mem :
forall x y t, x <> y ->
~ VSet.mem x (set_of_variables (apply_subst ((x, Var y) :: nil) t)).
Proof.
intros x y t x_diff_y; pattern t; apply T.term_rec3.
intros v; simpl;
destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x]; simpl; subst.
intros [x_eq_y | x_in_nil] ; [apply x_diff_y; subst; trivial | contradiction].
intros [x_eq_v | x_in_nil].
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst; apply v_diff_x; trivial.
contradiction.
intros f l IHl x_in_l'; simpl in x_in_l'; clear f; induction l as [ | s l]; trivial.
simpl in x_in_l'; destruct_set x_in_l' x_in_s' x_in_l''.
apply (IHl s); trivial; left; trivial.
apply IHl0; trivial.
intros; apply IHl; right; trivial.
Qed.
Lemma solved_var_inc_not_mem_list :
forall x y l, x <> y ->
~ VSet.mem x
(set_of_variables_in_unsolved_part
(map
(fun uv : term * term =>
let (u, v) := uv in
(apply_subst ((x, Var y) :: nil) u,
apply_subst ((x, Var y) :: nil) v)) l)).
Proof.
intros x y l x_diff_y x_in_l'; induction l as [ | [s t] l].
contradiction.
simpl set_of_variables_in_unsolved_part in x_in_l';
destruct_set x_in_l' x_in_s'_t' x_in_l''.
destruct_set x_in_s'_t' x_in_s' x_in_t'.
apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_s').
apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_t').
apply IHl; trivial.
Qed.
Lemma solved_var_inc_not_mem_subst :
forall x y sigma, x <> y ->
~VSet.mem x
(set_of_variables_in_range_of_subst
(map_subst
(fun (_ : variable) (v_sigma : term) =>
apply_subst ((x, Var y) :: nil) v_sigma) sigma)).
Proof.
intros x y sigma x_diff_y x_in_sigma'; induction sigma as [ | [v t] sigma].
contradiction.
simpl set_of_variables_in_range_of_subst in x_in_sigma';
destruct_set x_in_sigma' x_in_t' x_in_sigma''.
apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_t').
apply IHsigma; trivial.
Qed.
Lemma solved_var_inc_occ_in_subst :
forall x z x_val sigma, find eq_variable_dec x sigma = Some x_val ->
VSet.mem z (set_of_variables x_val) ->
VSet.mem z (set_of_variables_in_range_of_subst sigma).
Proof.
intros x z x_val sigma;
induction sigma as [ | [v t] sigma].
intro; discriminate.
intros x_sigma z_in_x_val;
simpl in x_sigma; destruct (eq_variable_dec x v) as [x_eq_v | x_diff_v].
simpl; apply VSet.union_1; injection x_sigma; intros; subst; trivial.
simpl; apply VSet.union_2; apply IHsigma; trivial.
Qed.
Lemma solved_var_inc_term :
forall x y z t, z <> y ->
VSet.mem z (set_of_variables (apply_subst ((x, Var y) :: nil) t)) ->
VSet.mem z (set_of_variables t).
Proof.
intros x y z t z_diff_y; pattern t; apply T.term_rec3.
intro v; simpl;
destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x]; simpl; subst; trivial.
intros [z_eq_y | z_in_nil].
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst z; absurd (y=y); trivial.
contradiction.
intros f l; simpl; fold set_of_variables_list; clear f;
induction l as [ | s l]; [trivial | idtac].
intros H_s_l z_in_s'_l'; destruct_set z_in_s'_l' z_in_s' z_in_l'.
simpl; apply VSet.union_1; apply H_s_l; trivial; left; trivial.
simpl; apply VSet.union_2; apply IHl; trivial.
intros; apply H_s_l; [right | idtac] ; trivial.
Qed.
Lemma solved_var_inc_list :
forall x y z l, z <> y ->
VSet.mem z
(set_of_variables_in_unsolved_part
(map
(fun uv : term * term =>
let (u, v) := uv in
(apply_subst ((x, Var y) :: nil) u,
apply_subst ((x, Var y) :: nil) v)) l)) ->
VSet.mem z (set_of_variables_in_unsolved_part l).
Proof.
intros x y z l z_diff_y z_in_l';
induction l as [ | [s t] l]; trivial; destruct_set z_in_l' z_in_s'_t' z_in_l''.
destruct_set z_in_s'_t' z_in_s' z_in_t'.
simpl set_of_variables_in_unsolved_part; do 2 apply VSet.union_1;
apply solved_var_inc_term with x y; trivial.
simpl set_of_variables_in_unsolved_part; apply VSet.union_1; apply VSet.union_2;
apply solved_var_inc_term with x y; trivial.
simpl set_of_variables_in_unsolved_part; apply VSet.union_2; apply IHl; trivial.
Qed.
Lemma solved_var_inc_subst :
forall x y z sigma, z <> y ->
VSet.mem z
(set_of_variables_in_range_of_subst
(map_subst
(fun (_ : variable) (v_sigma : term) =>
apply_subst ((x, Var y) :: nil) v_sigma) sigma)) ->
VSet.mem z (set_of_variables_in_range_of_subst sigma).
Proof.
intros x y z sigma z_diff_y z_in_sigma'; induction sigma as [ | [v t] sigma]; trivial.
destruct_set z_in_sigma' z_in_t' z_in_sigma''.
simpl set_of_variables_in_range_of_subst;
apply VSet.union_1; apply solved_var_inc_term with x y; trivial.
simpl set_of_variables_in_range_of_subst;
apply VSet.union_2; apply IHsigma; trivial.
Qed.
Lemma coalesce1_decreases :
forall x y l sigma x_val,
x <> y ->
find eq_variable_dec x sigma = Some x_val ->
lt_pb (mk_pb ((x, Var y)
:: map_subst
(fun (_ : variable) (v_sigma : term) =>
apply_subst ((x, Var y) :: nil) v_sigma) sigma)
((Var y, apply_subst ((x, Var y) :: nil) x_val)
:: map
(fun uv : term * term =>
let (u, v) := uv in
(apply_subst ((x, Var y) :: nil) u,
apply_subst ((x, Var y) :: nil) v)) l))
(mk_pb sigma ((Var x, Var y) :: l)).
Proof.
intros x y l sigma x_val x_diff_y x_sigma;
assert (Hx := find_map_subst x x (Var y) sigma); rewrite x_sigma in Hx.
unfold lt_pb, measure_for_unif_pb; apply lex_lt.
unfold phi1; apply VSet.subset_cardinal_not_eq_not_eq_set with x.
apply VSet.subset_filter.
assert (Hy : VSet.mem y (VSet.union
(VSet.union (VSet.union (VSet.singleton x) (VSet.singleton y))
(set_of_variables_in_unsolved_part l))
(VSet.union (domain_of_subst sigma)
(set_of_variables_in_range_of_subst sigma)))).
do 2 apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
simpl; apply VSet.subset_subset_union.
apply VSet.subset_subset_union.
apply VSet.subset_subset_union.
intros z [z_eq_y | z_in_nil].
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst; apply Hy.
contradiction.
intros z z_in_x_val';
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y]; [subst; apply Hy | idtac].
do 2 apply VSet.union_2;
apply solved_var_inc_occ_in_subst with x x_val; trivial;
apply solved_var_inc_term with x y; trivial.
intros z z_in_l';
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y]; [subst; apply Hy | idtac].
apply VSet.union_1; apply VSet.union_2; clear Hy.
apply solved_var_inc_list with x y; trivial.
apply VSet.subset_subset_union.
intros z z_in_x_dom_sig;
destruct (VSet.add_12 _ _ _ z_in_x_dom_sig) as [z_eq_x | z_in_dom_sig].
do 3 apply VSet.union_1; left; subst; trivial.
apply VSet.union_2; apply VSet.union_1;
rewrite domain_of_subst_map_subst in z_in_dom_sig; trivial.
apply VSet.subset_subset_union.
intros z [z_eq_y | z_in_nil].
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst z; apply Hy.
contradiction.
intros z z_in_sigma';
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y]; [subst z; apply Hy | idtac].
do 2 apply VSet.union_2; apply (solved_var_inc_subst _ _ _ _ z_diff_y z_in_sigma').
intros z;
do 2 setoid_rewrite not_solved_var; simpl.
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; intros _; rewrite x_sigma; left;
do 2 apply VSet.union_1; left; reflexivity.
assert (z_sigma : forall z', z' = z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
assert (Hz := find_map_subst z x (Var y) sigma).
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma;
unfold variable in *; rewrite Hz; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
intros _; left; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
intros [z_in_y_x_val'_l' | z_in_y_sigma'].
destruct_set z_in_y_x_val'_l' z_in_y_x_val' z_in_l'.
destruct_set z_in_y_x_val' z_in_y z_in_x_val'.
left; apply VSet.union_1; apply VSet.union_2; trivial.
right; apply solved_var_inc_occ_in_subst with x x_val; trivial.
apply solved_var_inc_term with x y; trivial.
left; apply VSet.union_2.
apply solved_var_inc_list with x y; trivial.
destruct_set z_in_y_sigma' z_in_y z_in_sigma'.
left; apply VSet.union_1; apply VSet.union_2; trivial.
right; apply solved_var_inc_subst with x y; trivial.
intro H; generalize (VSet.filter_2 _ _ _ _ _ H); clear H; intros [_ H]; apply H; clear H;
unfold is_a_solved_var; simpl.
destruct (eq_variable_dec x x) as [_ | x_diff_x]; [idtac | absurd (x=x); trivial]; split.
intro x_in_y_x_val'_l'; destruct_set x_in_y_x_val'_l' x_in_y_x_val' x_in_l'.
destruct_set x_in_y_x_val' x_in_y x_in_x_val'.
destruct x_in_y as [x_eq_y | x_in_nil]; [idtac | contradiction].
apply x_diff_y; subst; trivial.
apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_x_val').
apply (solved_var_inc_not_mem_list _ _ _ x_diff_y x_in_l').
intro x_in_y_sigma'; destruct_set x_in_y_sigma' x_in_y x_in_sigma'.
destruct x_in_y as [x_eq_y | x_in_nil]; [idtac | contradiction].
apply x_diff_y; subst; trivial.
apply (solved_var_inc_not_mem_subst _ _ _ x_diff_y x_in_sigma').
apply VSet.filter_1.
simpl unsolved_part; unfold set_of_variables_in_unsolved_part;
do 3 apply VSet.union_1; left; reflexivity.
setoid_rewrite not_solved_var; simpl; rewrite x_sigma.
left; do 2 apply VSet.union_1; left; reflexivity.
Qed.
Lemma coalesce2_decreases :
forall x y l sigma,
x <> y ->
find eq_variable_dec x sigma = None ->
lt_pb
(mk_pb
((x, Var y)
:: map_subst
(fun (_ : variable) (v_sigma : term) =>
apply_subst ((x, Var y) :: nil) v_sigma) sigma)
(map
(fun uv : term * term =>
let (u, v) := uv in
(apply_subst ((x, Var y) :: nil) u,
apply_subst ((x, Var y) :: nil) v)) l))
(mk_pb sigma ((Var x, Var y) :: l)).
Proof.
intros x y l sigma x_diff_y x_sigma;
assert (Hx := find_map_subst x x (Var y) sigma); rewrite x_sigma in Hx.
unfold lt_pb, measure_for_unif_pb; apply lex_lt.
unfold phi1; apply VSet.subset_cardinal_not_eq_not_eq_set with x.
simpl unsolved_part; simpl solved_part; simpl set_of_variables_in_unsolved_part;
simpl domain_of_subst; apply VSet.subset_filter.
apply VSet.subset_subset_union.
intros z z_in_l'; destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
do 2 apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply VSet.union_1; apply VSet.union_2;
apply solved_var_inc_list with x y; trivial.
apply VSet.subset_subset_union.
rewrite domain_of_subst_map_subst.
intros z z_in_x_dom_sig;
destruct (VSet.add_12 _ _ _ z_in_x_dom_sig) as [z_eq_x | z_in_dom_sig].
do 3 apply VSet.union_1; left; subst; trivial.
apply VSet.union_2; apply VSet.union_1; trivial.
intros z z_in_y_sigma'; destruct_set z_in_y_sigma' z_in_y z_in_sigma'.
do 2 apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
do 2 apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
do 2 apply VSet.union_2; apply (solved_var_inc_subst _ _ _ _ z_diff_y z_in_sigma').
intros z; do 2 setoid_rewrite not_solved_var.
assert (z_sigma : forall z', z' = z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
simpl; destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; rewrite z_sigma in x_sigma; discriminate.
assert (Hz := find_map_subst z x (Var y) sigma);
rewrite z_sigma in Hz; unfold variable in *; rewrite Hz.
intros [z_in_l' | z_in_y_sigma'].
left; destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply VSet.union_2; apply solved_var_inc_list with x y; trivial.
destruct_set z_in_y_sigma' z_in_y z_in_sigma'.
left; apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
left; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
right; apply solved_var_inc_subst with x y; trivial.
trivial.
intro H; destruct (VSet.filter_2 _ _ _ _ _ H) as [ _ H1 ]; apply H1; clear H H1.
unfold is_a_solved_var; simpl.
destruct (eq_variable_dec x x) as [ _ | x_diff_x ]; [idtac | absurd (x=x); trivial]; split.
apply solved_var_inc_not_mem_list; trivial.
intro x_in_y_sigma'; destruct_set x_in_y_sigma' x_in_y x_in_sigma'.
apply x_diff_y; destruct x_in_y as [x_eq_y | x_in_nil]; [subst; trivial | contradiction].
apply solved_var_inc_not_mem_subst with x y sigma; trivial.
apply VSet.filter_1.
simpl set_of_variables_in_unsolved_part;
do 3 apply VSet.union_1; left; reflexivity.
setoid_rewrite not_solved_var; simpl; rewrite x_sigma; trivial.
Qed.
Lemma list_size_mul_app:
forall (A : Set) (siz : A -> nat) l1 l2,
list_size_mul A siz (l1 ++ l2) = (list_size_mul A siz l1) ++ list_size_mul A siz l2.
Proof.
induction l1 as [ | a1 l1 ]; trivial.
intros; simpl; rewrite IHl1; trivial.
Qed.
Lemma merge1_decreases :
forall x g l2 l sigma x_val,
find eq_variable_dec x sigma = Some x_val ->
size (Term g l2) < size x_val ->
lt_pb (mk_pb ((x, Term g l2) :: sigma) ((x_val, Term g l2) :: l))
(mk_pb sigma ((Var x, Term g l2) :: l)).
Proof.
intros x g l2 l sigma x_val x_sigma L;
unfold lt_pb, measure_for_unif_pb; apply lex_le_meq_lt.
generalize (Term g l2) L; clear g l2 L; intros t2 L.
unfold phi1;
apply VSet.cardinal_subset; apply VSet.subset_filter.
apply VSet.subset_subset_union.
simpl; intros z z_in_x_val_t2_l; destruct_set z_in_x_val_t2_l z_in_x_val_t2 x_in_l.
destruct_set z_in_x_val_t2 z_in_x_val z_in_t2.
do 2 apply VSet.union_2; apply (solved_var_inc_occ_in_subst _ _ _ _ x_sigma z_in_x_val).
do 2 apply VSet.union_1; apply VSet.union_2; trivial.
apply VSet.union_1; apply VSet.union_2; trivial.
simpl; intros z z_in_x_dom_sig_t2_sigma;
destruct_set z_in_x_dom_sig_t2_sigma z_in_x_dom_sig z_in_t2_sigma.
destruct (VSet.add_12 _ _ _ z_in_x_dom_sig) as [z_in_x | z_in_dom_sig].
do 3 apply VSet.union_1; left; subst; trivial.
apply VSet.union_2; apply VSet.union_1; trivial.
destruct_set z_in_t2_sigma z_in_t2 z_in_sigma.
do 2 apply VSet.union_1; apply VSet.union_2; trivial.
do 2 apply VSet.union_2; trivial.
intros z; do 2 setoid_rewrite not_solved_var; simpl.
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; intros _; rewrite x_sigma; left;
do 2 apply VSet.union_1; left; subst; reflexivity.
assert (z_sigma : forall z', z' = z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma; trivial;
intros [ z_in_x_val_t2_l | z_in_t2_sigma].
destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l.
destruct_set z_in_x_val_t2 z_in_x_val z_in_t2.
right; apply (solved_var_inc_occ_in_subst x z x_val); trivial.
left; apply VSet.union_1; apply VSet.union_2; trivial.
left; apply VSet.union_2; trivial.
destruct_set z_in_t2_sigma z_in_t2 z_in_sigma.
left; apply VSet.union_1; apply VSet.union_2; trivial.
right; trivial.
generalize (Term g l2) L; clear g l2 L; intros t2 L.
assert (x_in_dom_sig : VSet.mem x (domain_of_subst sigma)).
unfold VSet.mem; induction sigma as [ | [y t] sigma].
discriminate.
simpl in x_sigma; destruct (eq_variable_dec x y) as [x_eq_y | x_diff_y].
subst y; simpl; apply VSet.add_1.
simpl; apply VSet.add_2;apply IHsigma; trivial.
destruct (VSet.LP.mem_split_set _ _ x_in_dom_sig)
as [x' [s1 [s2 [x_eq_x' dom_sig_eq_s1_x_s2]]]];
simpl in x_eq_x'; simpl in dom_sig_eq_s1_x_s2.
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst x'.
unfold phi2, size_of_solved_part, size_of_unsolved_part; simpl.
replace (VSet.add x (domain_of_subst sigma)) with (domain_of_subst sigma).
rewrite max_l; [idtac | auto with arith].
rewrite dom_sig_eq_s1_x_s2; do 2 rewrite list_size_mul_app.
simpl; destruct (eq_variable_dec x x) as [_ | x_diff_x]; [idtac | absurd (x=x); trivial].
rewrite x_sigma.
generalize (size_ge_one t2); unfold_types; destruct (size t2) as [ | n2];
[intro; absurd (1 <= 0); auto with arith | intros _ ].
rewrite <- ass_app; rewrite <- app_comm_cons;
setoid_rewrite <- NatMul.LP.permut_add_inside.
reflexivity.
rewrite <- ass_app; rewrite <- app_comm_cons; rewrite ass_app;
setoid_rewrite <- NatMul.LP.permut_add_inside.
reflexivity.
rewrite ass_app;
setoid_rewrite <- NatMul.LP.permut_app2.
do 2 rewrite <- list_size_mul_app.
assert (x_not_in_s1_s2 : ~VSet.LP.mem x (s1 ++ s2)).
assert (W := VSet.is_a_set (domain_of_subst sigma)).
rewrite dom_sig_eq_s1_x_s2 in W.
assert (P : VSet.LP.permut (x :: s1 ++ s2) (s1 ++ x :: s2)).
setoid_rewrite <- VSet.LP.permut_cons_inside; reflexivity.
assert (W'' := VSet.without_red_permut W (VSet.LP.permut_sym P)).
simpl in W''; destruct (VSet.LP.mem_dec x (s1 ++ s2));
[ contradiction | trivial ].
unfold_types; generalize (s1 ++ s2) x_not_in_s1_s2;
intros s x_not_in_s; induction s as [ | v s].
apply NatMul.LP.permut_refl.
simpl; destruct (eq_dec v x) as [v_eq_x | v_diff_x].
absurd (VSet.LP.mem x (v :: s)); trivial; subst; left; reflexivity.
setoid_rewrite <- NatMul.LP.permut_cons.
reflexivity.
apply IHs; intro; apply x_not_in_s; right; trivial.
unfold VSet.add.
destruct (VSet.mem_dec x (domain_of_subst sigma)); trivial.
absurd (VSet.mem x (domain_of_subst sigma)); trivial.
unfold phi3, nb_var_eq_of_unsolved_part; simpl.
destruct x_val as [v | f l1].
simpl in L; assert (L' := le_Sn_O _ (lt_S_n _ _ L)); contradiction.
auto with arith.
Qed.
Definition Inv_solved_part pb :=
forall x, match find eq_variable_dec x pb.(solved_part) with
| Some (Var _) => is_a_solved_var x pb
| _ => True
end.
Lemma merge2_decreases :
forall x g l2 l sigma x_val,
Inv_solved_part (mk_pb sigma ((Var x, Term g l2) :: l)) ->
find eq_variable_dec x sigma = Some x_val ->
size (Term g l2) >= size x_val ->
lt_pb (mk_pb sigma ((x_val, Term g l2) :: l)) (mk_pb sigma ((Var x, Term g l2) :: l)).
Proof.
intros x g l2 l sigma x_val Inv_pb x_sigma L;
assert (x_in_dom_sig : VSet.mem x (domain_of_subst sigma)).
clear Inv_pb; induction sigma as [ | [y t] sigma].
discriminate.
simpl in x_sigma; destruct (eq_variable_dec x y) as [x_eq_y | x_diff_y].
simpl; subst; apply VSet.add_1.
simpl; apply VSet.add_2; apply IHsigma; trivial.
unfold lt_pb, measure_for_unif_pb; apply lex_le_meq_lt.
generalize (Term g l2) L; clear g l2 L Inv_pb; intros t2 L.
unfold phi1;
apply VSet.cardinal_subset; apply VSet.subset_filter.
apply VSet.subset_subset_union.
simpl; intros z z_in_x_val_t2_l; destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l.
destruct_set z_in_x_val_t2 z_in_x_val z_in_t2.
do 2 apply VSet.union_2; refine (solved_var_inc_occ_in_subst _ _ _ _ x_sigma z_in_x_val).
do 2 apply VSet.union_1; apply VSet.union_2; trivial.
apply VSet.union_1; apply VSet.union_2; trivial.
apply VSet.subset_subset_union.
simpl; intros z z_in_dom_sig; apply VSet.union_2; apply VSet.union_1; trivial.
simpl; intros z z_in_sigma; do 2 apply VSet.union_2; trivial.
intros z; do 2 setoid_rewrite not_solved_var; simpl.
destruct (find eq_variable_dec z sigma) as [ z_val | ]; trivial.
intros [z_in_x_val_t2_l | z_in_sigma].
destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l.
destruct_set z_in_x_val_t2 z_in_x_val z_in_t2.
right; apply (solved_var_inc_occ_in_subst x z x_val); trivial.
left; apply VSet.union_1; apply VSet.union_2; trivial.
left; apply VSet.union_2; trivial.
right; trivial.
unfold phi2, size_of_unsolved_part, size_of_solved_part.
generalize (Term g l2) L; clear g l2 L Inv_pb; intros t2 L.
simpl; rewrite max_r; [idtac | unfold ge; trivial].
generalize (size_ge_one t2); destruct (size t2) as [ | n2];
[intro; absurd (1<=0); auto with arith | intros _].
apply NatMul.LP.permut_refl.
unfold phi3, nb_var_eq_of_unsolved_part; simpl.
generalize (Inv_pb x); simpl; rewrite x_sigma; unfold is_a_solved_var.
destruct x_val as [ v | f l'].
simpl; rewrite x_sigma; intros [ H _ ]; assert False.
apply H; do 2 apply VSet.union_1; left; reflexivity.
contradiction.
auto with arith.
Qed.
Lemma move_eq_decreases :
forall x g l2 l sigma,
find eq_variable_dec x sigma = None ->
lt_pb (mk_pb ((x, Term g l2) :: sigma) l) (mk_pb sigma ((Var x, Term g l2) :: l)).
Proof.
intros x g l2 l sigma x_sigma;
unfold lt_pb, measure_for_unif_pb; apply lex_le_meq_lt.
generalize (Term g l2); clear g l2; intro t2;
unfold phi1; apply VSet.cardinal_subset.
apply VSet.subset_filter.
simpl.
apply VSet.subset_subset_union.
intros z z_in_l; apply VSet.union_1; apply VSet.union_2; trivial.
apply VSet.subset_subset_union.
intros z z_in_x_dom_sig;
destruct (VSet.add_12 _ _ _ z_in_x_dom_sig) as [z_eq_x | z_in_dom_sig].
do 3 apply VSet.union_1; left; subst; trivial.
apply VSet.union_2; apply VSet.union_1; trivial.
apply VSet.subset_subset_union.
intros z z_in_t2; do 2 apply VSet.union_1; apply VSet.union_2; trivial.
intros z z_in_sigma; do 2 apply VSet.union_2; trivial.
intros z; do 2 setoid_rewrite not_solved_var; simpl;
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; rewrite x_sigma; trivial.
destruct (find eq_variable_dec z sigma) as [z_val | ]; trivial.
intros [z_in_l | z_in_t2_sigma].
left; apply VSet.union_2; trivial.
destruct_set z_in_t2_sigma z_in_t2 z_in_sigma.
left; apply VSet.union_1; apply VSet.union_2; trivial.
right; trivial.
unfold lt_mul, phi2, size_of_solved_part, size_of_unsolved_part.
generalize (Term g l2); intro t2; clear g l2.
assert (x_not_in_dom_sig : ~ VSet.LP.mem x (VSet.support (domain_of_subst sigma))).
induction sigma as [ | [y t] sigma].
intro; contradiction.
simpl in x_sigma; intro x_in_y_dom_sig;
destruct (VSet.add_12 _ _ _ x_in_y_dom_sig) as [x_eq_y | x_in_dom_sig];
clear x_in_y_dom_sig.
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst y.
destruct (eq_variable_dec x x) as [ _ | x_diff_x]; [discriminate | absurd (x=x); trivial].
apply IHsigma; trivial;
destruct (eq_variable_dec x y) as [ _ | _]; trivial; discriminate.
simpl; unfold VSet.add, VSet.mem_dec.
destruct (VSet.LP.mem_dec x (VSet.support (domain_of_subst sigma))) as
[x_in_dom_sig | x_not_in_dom_sig'].
absurd (VSet.LP.mem x (VSet.support (domain_of_subst sigma))); trivial.
simpl; destruct (eq_variable_dec x x) as [ _ | x_diff_x]; [idtac | absurd (x=x); trivial].
generalize (size_ge_one t2); destruct (size t2) as [ | n2];
[intro; absurd (1 <=0); auto with arith | intros _].
setoid_rewrite <- NatMul.LP.permut_cons_inside.
reflexivity.
setoid_rewrite <- NatMul.LP.permut_app2.
generalize (VSet.support (domain_of_subst sigma)) x_not_in_dom_sig;
intros s x_not_in_s; induction s as [ | y s].
apply NatMul.LP.permut_refl.
simpl; destruct (eq_dec y x) as [y_eq_x | y_diff_x].
absurd (VSet.LP.mem x (y :: s)); subst; trivial; left; reflexivity.
setoid_rewrite <- NatMul.LP.permut_cons.
reflexivity.
apply IHs; intro; apply x_not_in_s; right; trivial.
unfold phi3, nb_var_eq_of_unsolved_part; simpl; auto with arith.
Qed.
Lemma decomposition_decreases :
forall f l1 l2 l sigma (L : length l1 = length l2),
lt_pb (mk_pb sigma (combine term l l1 l2 L))
(mk_pb sigma ((Term f l1, Term f l2) :: l)).
Proof.
intros f l1 l2 l sigma L; unfold lt_pb, measure_for_unif_pb; apply lex_le_lt.
assert (H : forall z,
VSet.mem z (set_of_variables_in_unsolved_part (combine term l l1 l2 L)) ->
VSet.mem z (set_of_variables_in_unsolved_part ((Term f l1, Term f l2) :: l))).
generalize l2 L; clear l2 L; induction l1 as [ | t1 l1]; intros [ | t2 l2] L z.
simpl; intros; apply VSet.union_2; trivial.
discriminate.
discriminate.
simpl.
intros z_in_t1t2_l1l2l; destruct_set z_in_t1t2_l1l2l z_in_t1t2 z_in_l1l2l.
destruct_set z_in_t1t2 z_in_t1 z_in_t2.
do 3 apply VSet.union_1; trivial.
apply VSet.union_1; apply VSet.union_2; apply VSet.union_1; trivial.
assert (z_in_l1l2_l := IHl1 l2 _ z z_in_l1l2l); destruct_set z_in_l1l2_l z_in_l1l2 z_in_l.
destruct_set z_in_l1l2 z_in_l1 z_in_l2.
do 2 apply VSet.union_1; apply VSet.union_2; trivial.
apply VSet.union_1; do 2 apply VSet.union_2; trivial.
apply VSet.union_2; trivial.
unfold phi1; apply VSet.cardinal_subset; apply VSet.subset_filter.
apply VSet.subset_subset_union.
intros z z_in_l1_l2_l; generalize (H _ z_in_l1_l2_l); clear z_in_l1_l2_l; intro z_in_l1_l2_l.
destruct_set z_in_l1_l2_l z_in_l1_l2 z_in_l.
destruct_set z_in_l1_l2 z_in_l1 z_in_l2.
simpl; do 3 apply VSet.union_1; trivial.
simpl; do 2 apply VSet.union_1; apply VSet.union_2; trivial.
simpl; apply VSet.union_1; apply VSet.union_2; trivial.
apply VSet.subset_subset_union.
intros z z_in_dom_sig; apply VSet.union_2; apply VSet.union_1; trivial.
intros z z_in_sigma; do 2 apply VSet.union_2; trivial.
intro z; do 2 setoid_rewrite not_solved_var;
simpl; destruct (find eq_variable_dec z sigma) as [z_val | ]; trivial.
intros [H1 | H1].
left; apply H; trivial.
right; trivial.
unfold phi2, size_of_solved_part, size_of_unsolved_part; simpl.
unfold lt_mul; apply NatMul.context_trans_clos_multiset_extension_step_app1.
do 2 rewrite (list_size_fold size).
generalize l2 l L; clear l2 l L; induction l1 as [ | t1 l1];
intros [ | t2 l2] l L; try discriminate.
apply closure.t_step; simpl;
refine (@NatMul.rmv_case lt _ _
(list_size_mul (term * term)
(fun s_t : term * term => let (s, t) := s_t in max (size s) (size t)) l)
nil 1 _ _ _); try apply NatMul.LP.permut_refl.
intros; contradiction.
assert (L' := plus_reg_l (length l1) (length l2) 1 L).
rewrite (combine_cons term l t1 l1 t2 l2 L' L).
assert (H' := NatMul.context_trans_clos_multiset_extension_step_app1
(max (size t1) (size t2) :: nil) (IHl1 l2 l L')).
refine (closure.trans_clos_is_trans H' _); clear H'.
apply closure.t_step;
refine (@NatMul.rmv_case _ _ _ _
(max (size t1) (size t2) :: S (max (list_size size l1) (list_size size l2)) :: nil)
(S (max (size t1 + list_size size l1) (size t2 + list_size size l2))) _ _ _).
intros n [n_eq_max_t1_t2 | [n_eq_max_l1_l2 | n_in_nil]]; [idtac | idtac | intros; contradiction].
unfold NatMul.LP.EDS.eq_A in *;
subst n; apply (max_case2 (size t1) (size t2)); unfold lt; apply le_n_S.
refine (le_trans _ _ _ _ (le_max_l _ _)); auto with arith.
refine (le_trans _ _ _ _ (le_max_r _ _)); auto with arith.
unfold NatMul.LP.EDS.eq_A in *;
subst n; apply (max_case2 (list_size size l1) (list_size size l2)); unfold lt; apply le_n_S.
refine (le_trans _ _ _ _ (le_max_l _ _));
generalize (size_ge_one t1); destruct (size t1) as [ | n1];
[intro; absurd (1 <= 0) | intros _; simpl]; auto with arith.
refine (le_trans _ _ _ _ (le_max_r _ _));
generalize (size_ge_one t2); destruct (size t2) as [ | n2];
[intro; absurd (1 <= 0) | intros _; simpl]; auto with arith.
simpl; apply NatMul.LP.permut_refl.
apply NatMul.LP.permut_refl.
Qed.
Lemma inv_solved_part :
forall pb, Inv_solved_part pb ->
match decomposition_step pb with
| Normal pb' => Inv_solved_part pb'
| _ => True
end.
Proof.
intros [sigma [ | [s t] l]]; unfold Inv_solved_part, decomposition_step; simpl; trivial.
destruct (eq_term_dec s t) as [s_eq_t | s_diff_t]; simpl.
intros Inv_pb x; generalize (Inv_pb x); clear Inv_pb; unfold is_a_solved_var; simpl;
destruct (find eq_variable_dec x sigma) as [[ _ | _ _ ] | ]; trivial.
intros [x_not_in_s_t_l x_not_in_sigma]; split; trivial;
intro x_in_l; apply x_not_in_s_t_l; apply VSet.union_2; trivial.
destruct s as [x | f l1]; destruct t as [y | g l2].
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
destruct (find eq_variable_dec x sigma) as [ x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma;
assert (Hx := find_map_subst x x (Var y) sigma); rewrite x_sigma in Hx;
unfold solved_part; rewrite Hx; simpl.
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb; unfold is_a_solved_var; simpl;
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; rewrite x_sigma; intros _; unfold is_a_solved_var; simpl.
destruct (eq_variable_dec x x) as [ _ | x_diff_x]; [idtac | absurd (x=x); trivial];
unfold VSet.mem; split.
intro x_in_y_x_val'_l'; destruct_set x_in_y_x_val'_l' x_in_y_x_val' x_in_l'.
destruct_set x_in_y_x_val' x_in_y x_in_x_val'.
destruct x_in_y as [x_eq_y | x_in_nil]; [idtac | contradiction].
apply s_diff_t;
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst; trivial.
refine (solved_var_inc_not_mem _ _ _ _ x_in_x_val'); intro; apply s_diff_t; subst; trivial.
refine (solved_var_inc_not_mem_list _ _ _ _ x_in_l'); intro; apply s_diff_t; subst; trivial.
intro x_in_y_sigma'; destruct_set x_in_y_sigma' x_in_y x_in_sigma'.
destruct x_in_y as [x_eq_y | x_in_nil]; [idtac | contradiction].
apply s_diff_t;
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst; trivial.
refine (solved_var_inc_not_mem_subst _ _ _ _ x_in_sigma'); intro; apply s_diff_t; subst; trivial.
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros;
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
assert (Hz := find_map_subst z x (Var y) sigma); rewrite z_sigma in Hz;
rewrite Hz; destruct z_val as [v | f l']; simpl; trivial;
destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
intros [z_not_in_x_y_l z_not_in_sigma]; split.
unfold VSet.mem in *; intro z_in_y_x_val'_l'.
destruct_set z_in_y_x_val'_l' z_in_y_x_val' z_in_l'.
destruct_set z_in_y_x_val' z_in_y z_in_x_val'.
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial;
apply (solved_var_inc_occ_in_subst _ _ _ _ Hx z_in_x_val').
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_x_y_l; apply VSet.union_2; apply solved_var_inc_list with x y; trivial.
intro z_in_y_sigma; destruct_set z_in_y_sigma z_in_y z_in_sigma.
apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial.
intros [z_not_in_x_y_l z_not_in_sigma]; unfold VSet.mem in *; split.
intros z_in_y_x_val'_l'; destruct_set z_in_y_x_val'_l' z_in_y_x_val' z_in_l'.
destruct_set z_in_y_x_val' z_in_y z_in_x_val'.
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial;
apply (solved_var_inc_occ_in_subst _ _ _ _ Hx z_in_x_val').
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_x_y_l; apply VSet.union_2; apply solved_var_inc_list with x y; trivial.
intro z_in_y_sigma'; destruct_set z_in_y_sigma' z_in_y z_in_sigma'.
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial.
assert (Hz := find_map_subst z x (Var y) sigma);
rewrite z_sigma in Hz; rewrite Hz; trivial.
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb; unfold is_a_solved_var; simpl;
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x].
subst z; rewrite x_sigma; intros _; unfold is_a_solved_var; simpl.
unfold VSet.mem; split.
intro x_in_l';
refine (solved_var_inc_not_mem_list _ _ _ _ x_in_l'); intro; apply s_diff_t; subst; trivial.
intro x_in_y_sigma'; destruct_set x_in_y_sigma' x_in_y x_in_sigma'.
destruct x_in_y as [x_eq_y | x_in_nil]; [idtac | contradiction].
apply s_diff_t;
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst; trivial.
refine (solved_var_inc_not_mem_subst _ _ _ _ x_in_sigma'); intro; apply s_diff_t; subst; trivial.
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros;
unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *;
subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
assert (Hz := find_map_subst z x (Var y) sigma); rewrite z_sigma in Hz;
rewrite Hz; destruct z_val as [v | f l']; simpl; trivial;
destruct (eq_variable_dec v x) as [v_eq_x | v_diff_x].
intros [z_not_in_x_y_l z_not_in_sigma]; split.
unfold VSet.mem in *; intro z_in_l'.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_x_y_l; apply VSet.union_2; apply solved_var_inc_list with x y; trivial.
intro z_in_y_sigma; destruct_set z_in_y_sigma z_in_y z_in_sigma.
apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial.
intros [z_not_in_x_y_l z_not_in_sigma]; unfold VSet.mem in *; split.
intros z_in_l'; destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_x_y_l; apply VSet.union_2; apply solved_var_inc_list with x y; trivial.
intro z_in_y_sigma'; destruct_set z_in_y_sigma' z_in_y z_in_sigma'.
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; trivial.
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y].
apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity.
apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial.
assert (Hz := find_map_subst z x (Var y) sigma);
rewrite z_sigma in Hz; rewrite Hz; trivial.
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
destruct (find eq_variable_dec x sigma) as [ x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma.
destruct (lt_ge_dec (T.size (Term g l2)) (T.size x_val)) as [ L | L ].
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb;
unfold is_a_solved_var; simpl solved_part; simpl unsolved_part; simpl find;
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x]; trivial.
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
destruct z_val as [v | f l']; trivial.
intros [z_not_in_x_t2_l z_not_in_sigma];
split; [intro z_in_x_val_t2_l | intro z_in_t2_sigma].
destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l.
destruct_set z_in_x_val_t2 z_in_x_val z_in_t2.
apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with x x_val; trivial.
apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *;
apply VSet.union_1; apply VSet.union_2; trivial.
apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *; apply VSet.union_2; trivial.
destruct_set z_in_t2_sigma z_in_t2 z_in_sigma.
apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *;
apply VSet.union_1; apply VSet.union_2; trivial.
apply z_not_in_sigma; trivial.
trivial.
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb;
unfold is_a_solved_var; simpl solved_part; simpl unsolved_part; simpl find;
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
destruct z_val as [v | f l']; trivial.
intros [z_not_in_x_t2_l z_not_in_sigma];
split; [intro z_in_x_val_t2_l | intro z_in_t2_sigma].
destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l.
destruct_set z_in_x_val_t2 z_in_x_val z_in_t2.
apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with x x_val; trivial.
apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *;
apply VSet.union_1; apply VSet.union_2; trivial.
apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *; apply VSet.union_2; trivial.
apply z_not_in_sigma; trivial.
trivial.
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb;
unfold is_a_solved_var; simpl solved_part; simpl unsolved_part; simpl find;
destruct (eq_variable_dec z x) as [z_eq_x | z_diff_x]; trivial.
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
destruct z_val as [v | f l']; trivial.
intros [z_not_in_x_t2_l z_not_in_sigma];
split; [intro z_in_l | intro z_in_t2_sigma].
apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *; apply VSet.union_2; trivial.
destruct_set z_in_t2_sigma z_in_t2 z_in_sigma.
apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *;
apply VSet.union_1; apply VSet.union_2; trivial.
apply z_not_in_sigma; trivial.
trivial.
assert (y_sigma : forall y', y'=y ->
find eq_variable_dec y' sigma = find eq_variable_dec y sigma).
intros; subst; trivial.
destruct (find eq_variable_dec y sigma) as [ y_val | ];
generalize (y_sigma _ (refl_equal _)); clear y_sigma; intro y_sigma.
destruct (lt_ge_dec (T.size (Term f l1)) (T.size y_val)) as [ L | L ].
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb;
unfold is_a_solved_var; simpl solved_part; simpl unsolved_part; simpl find;
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y]; trivial.
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
destruct z_val as [v | f' l']; trivial.
intros [z_not_in_t1_y_l z_not_in_sigma];
split; [intro z_in_y_val_t1_l | intro z_in_t1_sigma].
destruct_set z_in_y_val_t1_l z_in_y_val_t1 z_in_l.
destruct_set z_in_y_val_t1 z_in_y_val z_in_t1.
apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with y y_val; trivial.
apply z_not_in_t1_y_l; simpl; unfold VSet.mem in *; do 2 apply VSet.union_1; trivial.
apply z_not_in_t1_y_l; simpl; unfold VSet.mem in *; apply VSet.union_2; trivial.
destruct_set z_in_t1_sigma z_in_t1 z_in_sigma.
apply z_not_in_t1_y_l; simpl; unfold VSet.mem in *; do 2 apply VSet.union_1; trivial.
apply z_not_in_sigma; trivial.
trivial.
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb;
unfold is_a_solved_var; simpl solved_part; simpl unsolved_part; simpl find;
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
destruct z_val as [v | f' l']; trivial.
intros [z_not_in_t1_y_l z_not_in_sigma];
split; [intro z_in_y_val_t1_l | intro z_in_t1_sigma].
destruct_set z_in_y_val_t1_l z_in_y_val_t1 z_in_l.
destruct_set z_in_y_val_t1 z_in_y_val z_in_t1.
apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with y y_val; trivial.
apply z_not_in_t1_y_l; simpl; unfold VSet.mem in *; do 2 apply VSet.union_1; trivial.
apply z_not_in_t1_y_l; simpl; unfold VSet.mem in *; apply VSet.union_2; trivial.
apply z_not_in_sigma; trivial.
trivial.
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb;
unfold is_a_solved_var; simpl solved_part; simpl unsolved_part; simpl find;
destruct (eq_variable_dec z y) as [z_eq_y | z_diff_y]; trivial.
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
destruct z_val as [v | f' l']; trivial.
intros [z_not_in_t1_y_l z_not_in_sigma];
split; [intro z_in_l | intro z_in_t1_sigma].
apply z_not_in_t1_y_l; simpl; unfold VSet.mem in *; apply VSet.union_2; trivial.
destruct_set z_in_t1_sigma z_in_t1 z_in_sigma.
apply z_not_in_t1_y_l; simpl; unfold VSet.mem in *; do 2 apply VSet.union_1; trivial.
apply z_not_in_sigma; trivial.
trivial.
destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g ].
destruct (eq_nat_dec (length l1) (length l2)) as [ L | L ]; trivial.
intros Inv_pb z; generalize (Inv_pb z); clear Inv_pb;
unfold is_a_solved_var; simpl solved_part; simpl unsolved_part;
assert (z_sigma : forall z', z'=z ->
find eq_variable_dec z' sigma = find eq_variable_dec z sigma).
intros; subst; trivial.
simpl; destruct (find eq_variable_dec z sigma) as [ z_val | ];
generalize (z_sigma _ (refl_equal _)); clear z_sigma; intro z_sigma.
destruct z_val as [v | h l']; simpl; trivial.
intros [z_not_in_t1_t2_l z_not_in_sigma]; split; [intro z_in_l1_l2_l | intro z_in_sigma].
simpl; unfold VSet.mem; apply z_not_in_t1_t2_l.
generalize l l2 L z_in_l1_l2_l; clear l L l2 z_not_in_t1_t2_l s_diff_t z_in_l1_l2_l;
induction l1 as [ | t1 l1]; intros l [ | t2 l2] L.
simpl; unfold VSet.mem; intros z_in_l; apply VSet.union_2; trivial.
discriminate.
discriminate.
intros z_in_t1_t2_l1_l2_l; destruct_set z_in_t1_t2_l1_l2_l z_in_t1_t2 z_in_l1_l2_l.
destruct_set z_in_t1_t2 z_in_t1 z_in_t2.
unfold VSet.mem in *; do 3 apply VSet.union_1; trivial.
unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; apply VSet.union_1; trivial.
assert (z_in_l1_l2_l' := IHl1 l l2 _ z_in_l1_l2_l); clear z_in_l1_l2_l.
destruct_set z_in_l1_l2_l' z_in_l1_l2 z_in_l.
destruct_set z_in_l1_l2 z_in_l1 z_in_l2.
unfold VSet.mem in *; do 2 apply VSet.union_1; apply VSet.union_2; trivial.
unfold VSet.mem in *; apply VSet.union_1; do 2 apply VSet.union_2; trivial.
unfold VSet.mem in *; apply VSet.union_2; trivial.
apply z_not_in_sigma; trivial.
trivial.
trivial.
Qed.
Lemma solved_var_swapp_eq :
forall x s t l sigma, is_a_solved_var x (mk_pb sigma ((s,t) :: l)) ->
is_a_solved_var x (mk_pb sigma ((t,s) :: l)).
Proof.
intros x s t l sigma; unfold is_a_solved_var; simpl;
destruct (find eq_variable_dec x sigma) as [x_val | ]; trivial.
intros [x_not_in_s_t_l x_not_in_sigma]; split; [intros x_in_t_s_l | intros x_in_sigma].
apply x_not_in_s_t_l; destruct_set x_in_t_s_l x_in_t_s x_in_l.
destruct_set x_in_t_s x_in_t x_in_s.
unfold VSet.mem; apply VSet.union_1; apply VSet.union_2; trivial.
unfold VSet.mem; do 2 apply VSet.union_1; trivial.
unfold VSet.mem; apply VSet.union_2; trivial.
apply x_not_in_sigma; trivial.
Qed.
Lemma measure_for_unif_pb_swapp_eq :
forall s t l sigma,
measure_for_unif_pb (mk_pb sigma ((s,t) :: l)) =
measure_for_unif_pb (mk_pb sigma ((t,s) :: l)).
Proof.
intros s t l sigma.
assert (Phi1 : phi1 (mk_pb sigma ((s,t) :: l)) = phi1 (mk_pb sigma ((t,s) :: l))).
unfold phi1; apply VSet.cardinal_eq_set.
assert (H : forall s t z, ~ is_a_solved_var z (mk_pb sigma ((s, t) :: l)) ->
~ is_a_solved_var z (mk_pb sigma ((t, s) :: l))).
clear s t; intros s t z H;
destruct (is_a_solved_var_dec (mk_pb sigma ((t,s) :: l)) z) as [z_solved | z_not_solved]; trivial.
absurd (is_a_solved_var z (mk_pb sigma ((s,t) :: l))); trivial;
apply solved_var_swapp_eq; trivial.
intros z; simpl solved_part; simpl unsolved_part; split; intro z_in_U;
destruct (VSet.filter_2 _ _ _ _ _ z_in_U) as [z_in_V z_unslvd]; clear z_in_U;
apply VSet.filter_1.
destruct_set z_in_V z_in_s_t_l z_in_sig.
destruct_set z_in_s_t_l z_in_s_t z_in_l.
destruct_set z_in_s_t z_in_s z_in_t.
simpl; unfold VSet.mem; do 2 apply VSet.union_1; apply VSet.union_2; trivial.
simpl; unfold VSet.mem; do 3 apply VSet.union_1; trivial.
simpl; unfold VSet.mem; apply VSet.union_1; apply VSet.union_2; trivial.
unfold VSet.mem; apply VSet.union_2; trivial.
apply H; trivial.
destruct_set z_in_V z_in_t_s_l z_in_sig.
destruct_set z_in_t_s_l z_in_t_s z_in_l.
destruct_set z_in_t_s z_in_t z_in_s.
simpl; unfold VSet.mem; do 2 apply VSet.union_1; apply VSet.union_2; trivial.
simpl; unfold VSet.mem; do 3 apply VSet.union_1; trivial.
simpl; unfold VSet.mem; apply VSet.union_1; apply VSet.union_2; trivial.
unfold VSet.mem; apply VSet.union_2; trivial.
apply H; trivial.
assert (Phi2 : phi2 (mk_pb sigma ((s,t) :: l)) = phi2 (mk_pb sigma ((t,s) :: l))).
unfold phi2, size_of_solved_part, size_of_unsolved_part; simpl;
rewrite max_comm; trivial.
assert (Phi3 : phi3 (mk_pb sigma ((s,t) :: l)) = phi3 (mk_pb sigma ((t,s) :: l))).
unfold phi3, nb_var_eq_of_unsolved_part; simpl;
destruct s; destruct t; trivial.
unfold measure_for_unif_pb; rewrite Phi1; rewrite Phi2; rewrite Phi3; trivial.
Qed.
Lemma decomposition_step_decreases :
forall pb, Inv_solved_part pb ->
match decomposition_step pb with
| Normal pb' => lt_pb pb' pb
| _ => True
end.
Proof.
intros [sigma [ | [s t] l]] Inv_pb; simpl; trivial.
unfold decomposition_step; simpl unsolved_part; cbv iota beta.
destruct (eq_term_dec s t) as [s_eq_t | s_diff_t].
subst s; apply remove_trivial_eq_decreases.
destruct s as [ x | f l1 ]; destruct t as [ y | g l2].
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
assert (Hx := find_map_subst x x (Var y) sigma).
destruct (find eq_variable_dec x sigma) as [x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma;
simpl solved_part; rewrite Hx.
apply coalesce1_decreases; trivial; intro; apply s_diff_t; subst; trivial.
apply coalesce2_decreases; trivial; intro; apply s_diff_t; subst; trivial.
simpl solved_part.
assert (x_sigma : forall x', x'=x ->
find eq_variable_dec x' sigma = find eq_variable_dec x sigma).
intros; subst; trivial.
destruct (find eq_variable_dec x sigma) as [x_val | ];
generalize (x_sigma _ (refl_equal _)); clear x_sigma; intro x_sigma.
destruct (lt_ge_dec (T.size (Term g l2)) (T.size x_val)) as [t2_lt_x_val | t2_ge_x_val].
apply merge1_decreases; trivial.
apply merge2_decreases; trivial.
apply move_eq_decreases; trivial.
simpl solved_part.
assert (y_sigma : forall y', y'=y ->
find eq_variable_dec y' sigma = find eq_variable_dec y sigma).
intros; subst; trivial.
simpl solved_part; destruct (find eq_variable_dec y sigma) as [y_val | ];
generalize (y_sigma _ (refl_equal _)); clear y_sigma; intro y_sigma.
destruct (lt_ge_dec (T.size (Term f l1)) (T.size y_val)) as [t1_lt_y_val | t1_ge_y_val].
unfold lt_pb; rewrite (measure_for_unif_pb_swapp_eq (Term f l1));
apply merge1_decreases; trivial.
unfold lt_pb; rewrite (measure_for_unif_pb_swapp_eq (Term f l1));
apply merge2_decreases; trivial.
unfold Inv_solved_part in *; simpl solved_part in *;
intros x; generalize (Inv_pb x);
destruct (find eq_variable_dec x sigma) as [[v | f' l'] | ]; trivial;
apply solved_var_swapp_eq.
unfold lt_pb; rewrite (measure_for_unif_pb_swapp_eq (Term f l1));
apply move_eq_decreases; trivial.
destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]; [idtac | trivial].
destruct (eq_nat_dec (length l1) (length l2)) as [ L | _ ]; trivial.
simpl solved_part; subst g; apply decomposition_decreases.
Qed.
Definition of a step of decomposition for the loop.
Definition Inv_solved_part_e e :=
match e with
| Normal pb => Inv_solved_part pb
| Not_appliable pb => pb.(unsolved_part) = nil
| No_solution => True
end.
Inductive exc_pb_ok : Set :=
| OK : forall (e : exc unification_problem), Inv_solved_part_e e -> exc_pb_ok.
Definition weight_exc_pb_ok e :=
match e with
| OK (Normal pb) _ => (2, measure_for_unif_pb pb)
| OK (Not_appliable pb) _ => (1, measure_for_unif_pb pb)
| OK No_solution _ => (0, (0,(nil,0)))
end.
Definition lt_weight_exc_pb_ok (w1 w2 : nat * (nat * (list nat * nat))) :=
match w1, w2 with
| (n1,m1), (n2,m2) =>
if eq_nat_dec n1 n2
then lt_ms m1 m2
else n1 < n2
end.
Definition lt_exc_pb_ok (u1 u2 : exc_pb_ok) :=
lt_weight_exc_pb_ok (weight_exc_pb_ok u1) (weight_exc_pb_ok u2).
Lemma wf_lt_exc_pb_ok : well_founded lt_exc_pb_ok.
Proof.
apply (wf_inverse_image (exc_pb_ok) _ lt_weight_exc_pb_ok weight_exc_pb_ok).
unfold well_founded, lt_weight_exc_pb_ok.
intros [n m]; generalize m; clear m; pattern n.
refine (well_founded_ind lt_wf _ _ n).
clear n; intros n IHn m; apply Acc_intro.
intros [n' m']; destruct (eq_nat_dec n' n) as [n'_eq_n | n'_diff_n];
[subst n' | intro n'_lt_n; apply IHn; trivial].
generalize m'; clear m';
pattern m; refine (well_founded_ind wf_lt_ms _ _ m); clear m.
intros m IHm m' m'_lt_m; apply Acc_intro.
intros [n'' m'']; destruct (eq_nat_dec n'' n) as [n''_eq_n | n''_diff_n].
subst n''; apply IHm; trivial.
intro n''_lt_n; apply IHn; trivial.
Qed.
Lemma inv_solved_part_e :
forall pb, Inv_solved_part pb \/ pb.(unsolved_part) = nil -> Inv_solved_part_e (decomposition_step pb).
Proof.
intros [sigma [ | [s t] l]] [Inv_pb | l_eq_nil].
simpl; trivial.
simpl; trivial.
generalize (inv_solved_part _ Inv_pb); unfold decomposition_step; simpl.
destruct (eq_term_dec s t); trivial.
destruct s as [x | f1 l1]; destruct t as [y | f2 l2].
case (find eq_variable_dec x
(map_subst
(fun (_ : variable) (v_sigma : term) =>
apply_subst ((x, Var y) :: nil) v_sigma) sigma)); trivial.
destruct (find eq_variable_dec x sigma) as [x_val | ]; trivial.
destruct (lt_ge_dec (T.size (Term f2 l2)) (T.size x_val)); trivial.
destruct (find eq_variable_dec y sigma) as [y_val | ]; trivial.
destruct (lt_ge_dec (T.size (Term f1 l1)) (T.size y_val)); trivial.
destruct (eq_symbol_dec f1 f2); trivial.
destruct (eq_nat_dec (length l1) (length l2)); trivial.
discriminate.
Qed.
Definition decomposition_step_e (e : exc_pb_ok) : exc_pb_ok.
intros [ [ pb | pb | ] Inv_pb ].
exact (OK (decomposition_step pb) (inv_solved_part_e _ (or_introl _ Inv_pb))).
exact (OK (Not_appliable _ pb) Inv_pb).
exact (OK (No_solution _) Inv_pb).
Defined.
Lemma decomposition_e_unfold_not_app :
forall pb Inv_pb,
decomposition_step_e (OK (Not_appliable _ pb) Inv_pb) = OK (Not_appliable _ pb) Inv_pb.
Proof.
intros; simpl; trivial.
Qed.
Lemma decomposition_e_unfold_no_sol :
forall Inv_pb,
decomposition_step_e (OK (No_solution _) Inv_pb) = OK (No_solution _) Inv_pb.
Proof.
intros; simpl; trivial.
Qed.
Lemma decomposition_e_unfold_normal :
forall pb Inv_pb,
decomposition_step_e (OK (Normal _ pb) Inv_pb) =
OK (decomposition_step pb) (inv_solved_part_e _ (or_introl _ Inv_pb)).
Proof.
intros pb Inv_pb; simpl; trivial.
Qed.
Lemma decomposition_step_decreases_e :
forall pb (Inv_pb : Inv_solved_part pb),
lt_exc_pb_ok (decomposition_step_e (OK (Normal _ pb) Inv_pb)) (OK (Normal _ pb) Inv_pb).
Proof.
intros pb Inv_pb; rewrite decomposition_e_unfold_normal.
unfold lt_exc_pb_ok, lt_weight_exc_pb_ok, lt_pb; simpl.
generalize (decomposition_step_decreases pb Inv_pb).
destruct (decomposition_step pb).
trivial.
intros _; destruct (eq_nat_dec 1 2); [discriminate | auto with arith].
intros _; destruct (eq_nat_dec 0 2); [discriminate | auto with arith].
Qed.
Definition F_decompose :
forall (u : exc_pb_ok),
(forall u' : exc_pb_ok , lt_exc_pb_ok u' u -> exc unification_problem) ->
exc unification_problem.
Proof.
intros [[pb | pb | ] Inv_pb] IH.
exact (IH _ (decomposition_step_decreases_e pb Inv_pb)).
exact (Not_appliable _ pb).
exact (No_solution _).
Defined.
Definition decompose : forall (u : exc_pb_ok), (exc unification_problem).
Proof.
intros u; exact (Fix wf_lt_exc_pb_ok (fun _ => exc unification_problem)
F_decompose u).
Defined.
Lemma decompose_unfold : forall u : exc_pb_ok,
decompose u = @F_decompose u (fun u' _ => decompose u').
Proof.
intros u; unfold decompose;
apply Fix_eq with (P:= (fun _: exc_pb_ok => exc unification_problem)); clear u.
intros [ [pb | pb | ] Inv_pb] f g H; simpl; [ rewrite H | idtac | idtac ]; trivial.
Qed.
Lemma decompose_nf :
forall e,
match decompose e with
| Normal _ => False
| Not_appliable (mk_pb sigma l) => l = nil
| No_solution => True
end.
Proof.
intros e; pattern e; apply (well_founded_ind wf_lt_exc_pb_ok); clear e.
intros [ [pb | pb | ] Inv_pb] IH; rewrite decompose_unfold; simpl.
apply IH; refine (decomposition_step_decreases_e _ Inv_pb).
simpl in Inv_pb; destruct pb; trivial.
trivial.
Qed.
Definition is_a_solution_e e sigma :=
match e with
| OK (Normal pb) _ => is_a_solution pb sigma
| OK (Not_appliable pb) _ => is_a_solution pb sigma
| OK No_solution _ => False
end.
Lemma decompose_is_sound :
forall e sigma,
match decompose e with
| Normal _ => False
| Not_appliable pb' => is_a_solution pb' sigma -> is_a_solution_e e sigma
| No_solution => True
end.
Proof.
intro e; pattern e; apply (well_founded_ind wf_lt_exc_pb_ok); clear e.
intros [[pb | pb | ] Inv_pb] IH theta;
rewrite decompose_unfold; unfold F_decompose; trivial.
assert (H := IH _ (decomposition_step_decreases_e _ Inv_pb) theta).
destruct pb as [sigma l].
destruct (decompose
(decomposition_step_e (OK (Normal unification_problem (mk_pb sigma l)) Inv_pb))).
contradiction.
intros sigma_is_sol; assert (H' := H sigma_is_sol); clear H; simpl in H'; simpl.
assert (H'' := decomposition_step_is_sound l sigma theta).
destruct (decomposition_step (mk_pb sigma l)); simpl.
apply H''; trivial.
apply H''; trivial.
contradiction.
trivial.
Qed.
Lemma decompose_is_complete :
forall e sigma, is_a_solution_e e sigma ->
match decompose e with
| Normal _ => False
| Not_appliable pb' => is_a_solution pb' sigma
| No_solution => False
end.
Proof.
intro e; pattern e; apply (well_founded_ind wf_lt_exc_pb_ok); clear e.
intros [[pb | pb | ] Inv_pb] IH theta theta_is_sol;
rewrite decompose_unfold; unfold F_decompose; trivial.
assert (H := IH _ (decomposition_step_decreases_e _ Inv_pb) theta).
destruct pb as [sigma l].
destruct (decompose
(decomposition_step_e (OK (Normal unification_problem (mk_pb sigma l)) Inv_pb)));
apply H; simpl; simpl in theta_is_sol;
apply decomposition_step_is_complete; trivial.
Qed.
Lemma inv_solved_part_init :
forall t1 t2, Inv_solved_part (mk_pb nil ((t1, t2) :: nil)).
Proof.
intros t1 t2; unfold Inv_solved_part; simpl; trivial.
Qed.
End Make.