Library ac_matching.matching_complete
Add LoadPath "basis".
Add LoadPath "list_extensions".
Add LoadPath "term_algebra".
Add LoadPath "term_orderings".
Require Import Arith.
Require Import List.
Require Import more_list.
Require Import list_sort.
Require Import term.
Require Import ac.
Require Import cf_eq_ac.
Require Import matching_sound.
Module Type S.
Declare Module Import SMatching : matching_sound.S.
Import WFMMatching.
Import WFMatching.
Import Matching.
Import Cf_eq_ac.
Import Ac.
Import EqTh.
Import T.
Axiom solve_is_complete :
forall pb, well_formed_pb pb -> forall sigma, is_well_formed_sol pb sigma ->
match pb.(unsolved_part) with
| nil => True
| _ :: _ => exists pb', In pb' (solve pb) /\ is_well_formed_sol pb' sigma
end.
End S.
Module Make (SMatching1 : matching_sound.S) :
S with Module SMatching := SMatching1.
Module Import SMatching := SMatching1.
Import WFMMatching.
Import WFMatching.
Import Matching.
Import Cf_eq_ac.
Import Ac.
Import EqTh.
Import T.
Import F.
Import X.
Import Sort.
Import LPermut.
Lemma remove_a_subterm :
forall sigma f v l1 t l2, arity f = AC -> well_formed_cf_subst sigma ->
well_formed_cf (Term f (Var v :: l1)) ->
well_formed_cf (Term f l2) ->
apply_cf_subst sigma (Var v) = t ->
apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 ->
match remove _ eq_term_dec t l2 with
| None =>
match t with
| Var _ => False
| Term g _ => f=g
end
| Some rmv => apply_cf_subst sigma (build f l1) = build f rmv
end.
Proof.
intros sigma f v l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma;
generalize (in_remove _ eq_term_dec t l2);
destruct (remove _ eq_term_dec t l2) as [l2''' | ].
intros [cp1 [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]]; subst cp1.
injection l2'''_eq; clear l2'''_eq; intro; subst l2 l2''';
apply flatten_cf with f; trivial.
apply well_formed_cf_apply_subst; trivial;
apply well_formed_cf_build_cons with (Var v); trivial.
apply well_formed_cf_build_inside with t; trivial.
setoid_rewrite <- (flatten_apply_cf_subst sigma l1 Ar);
setoid_rewrite (flatten_build (l2' ++ l2'') Ar).
intros s s_in_l2'_l2'';
destruct (in_app_or _ _ _ s_in_l2'_l2'') as [s_in_l2' | s_in_l2''];
apply (well_formed_cf_alien Ar Wt2); apply in_or_app; [left | right; right]; trivial.
setoid_rewrite (permut_app1 (t :: nil)).
transitivity (l2' ++ t :: l2'').
simpl in t1_sigma; rewrite Ar in t1_sigma;
simpl in v_sigma; rewrite v_sigma in t1_sigma; inversion_clear t1_sigma;
apply permut_sym; apply quick_permut_bis.
destruct t as [ x | g ll].
apply permut_refl.
destruct (eq_symbol_dec f g) as [f_eq_g | _].
absurd (f=g); trivial.
apply (well_formed_cf_alien Ar Wt2 (Term g ll)).
apply in_or_app; right; left; trivial.
apply permut_refl.
simpl; apply permut_sym; setoid_rewrite <- permut_cons_inside; auto.
reflexivity.
intros t_not_in_l2;
simpl in t1_sigma; rewrite Ar in t1_sigma;
simpl in v_sigma; rewrite v_sigma in t1_sigma;
inversion t1_sigma.
destruct t as [x | g ll].
apply (t_not_in_l2 (Var x)); subst l2; trivial.
setoid_rewrite <- (list_permut.in_permut_in (quick_permut (Var x :: flatten f (map (apply_cf_subst sigma) l1)))); left; trivial.
destruct (eq_symbol_dec f g); trivial.
absurd (In (Term g ll) l2); trivial.
intro H; apply (t_not_in_l2 (Term g ll)); trivial.
subst l2;
setoid_rewrite <- (list_permut.in_permut_in (quick_permut (Term g ll :: flatten f (map (apply_cf_subst sigma) l1)))).
left; trivial.
Qed.
Lemma remove_several_subterms :
forall sigma f v l1 t l2, arity f = AC -> well_formed_cf_subst sigma ->
well_formed_cf (Term f (Var v :: l1)) ->
well_formed_cf (Term f l2) ->
apply_cf_subst sigma (Var v) = t ->
apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 ->
match t with
| Var _ => True
| Term g l0 =>
if eq_symbol_dec f g
then
match remove_list l0 l2 with
| None => False
| Some l3 =>
if le_gt_dec (length l1) (length l3)
then apply_cf_subst sigma (build f l1) = build f l3
else False
end
else True
end.
Proof.
intros sigma f v l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma;
destruct t as [ x | g ll]; trivial.
destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]; [subst g | trivial].
assert (W_v : well_formed_cf (Var v)). simpl; trivial.
assert (W_v_sigma := well_formed_cf_apply_subst W_sigma _ W_v);
rewrite v_sigma in W_v_sigma.
generalize (in_remove_list (well_formed_cf_sorted Ar W_v_sigma)
(well_formed_cf_sorted Ar Wt2)).
unfold EDS.A, DOS.A in *;
destruct (remove_list ll l2) as [l2' | ].
unfold EDS.A, DOS.A in *; intro P; elim (le_gt_dec (length l1) (length l2')); intro L.
assert (Al_l2' : forall t, In t l2' -> match t with Var _ => True | Term g _ => f <> g end).
intros t In_t; apply (well_formed_cf_alien Ar Wt2).
setoid_rewrite <- (list_permut.in_permut_in P).
apply in_or_app; right; trivial.
apply flatten_cf with f; trivial.
apply well_formed_cf_apply_subst; trivial;
apply well_formed_cf_build_cons with (Var v); trivial.
apply well_formed_cf_build; trivial.
apply le_trans with (length l1); trivial.
apply le_S_n; generalize (well_formed_cf_length Ar Wt1); trivial.
intros t In_t; apply (well_formed_cf_subterms Wt2).
setoid_rewrite <- (list_permut.in_permut_in P);
apply in_or_app; right; trivial.
setoid_rewrite <- (flatten_apply_cf_subst sigma l1 Ar);
setoid_rewrite (flatten_build l2' Ar Al_l2').
setoid_rewrite (permut_app1 ll).
transitivity l2.
simpl in t1_sigma; rewrite Ar in t1_sigma.
inversion_clear t1_sigma.
simpl in v_sigma; rewrite v_sigma.
destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial].
apply quick_permut.
symmetry; trivial.
generalize (plus_lt_compat_l _ _ (length ll) L).
rewrite <- length_app; assert (L' := list_permut.permut_length P); unfold EDS.A, DOS.A in *;
rewrite L'; clear L'.
simpl in t1_sigma; rewrite Ar in t1_sigma.
inversion_clear t1_sigma; rewrite length_quicksort;
simpl in v_sigma; rewrite v_sigma;
destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial].
rewrite length_app; intro L'; assert (L'' := plus_lt_reg_l _ _ (length ll) L'); clear L L'.
absurd (length l1 < length l1); auto with arith.
refine (le_lt_trans _ _ _ _ L'').
rewrite <- (length_map (apply_cf_subst sigma)).
apply length_flatten_bis; trivial.
intros t' t'_in_map_l1; setoid_rewrite in_map_iff in t'_in_map_l1;
destruct t'_in_map_l1 as [t [Wt t_sigma]].
subst; apply well_formed_cf_apply_subst; trivial.
apply (well_formed_cf_subterms Wt1); right; trivial.
intro P; apply (P (flatten f (map (apply_cf_subst sigma) l1)));
simpl in v_sigma; simpl in t1_sigma;
rewrite Ar in t1_sigma; rewrite v_sigma in t1_sigma;
inversion_clear t1_sigma.
simpl; trivial;
destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [idtac | absurd (f=f); trivial].
apply quick_permut; auto.
Qed.
Lemma remove_several_subterms_bis :
forall sigma f v v' l1 t l2, arity f = AC -> well_formed_cf_subst sigma ->
well_formed_cf (Term f (Var v :: l1)) ->
well_formed_cf (Term f l2) ->
apply_cf_subst sigma (Var v) =
Term f (quicksort (flatten f (apply_cf_subst sigma (Var v') :: t :: nil))) ->
apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 ->
match t with | Var _ => True | Term g _ => f<>g end ->
match remove _ eq_term_dec t l2 with
| None => False
| Some l3 => apply_cf_subst sigma (build f (Var v' :: l1)) = build f l3
end.
Proof.
intros sigma f v v' l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma.
generalize (in_remove _ eq_term_dec t l2);
destruct (remove _ eq_term_dec t l2) as [l2''' | ].
intros [cp1' [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]] Al_t.
injection l2'''_eq; clear l2'''_eq; intro l2'''_eq;
apply flatten_cf with f; trivial.
apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build; trivial.
simpl; auto with arith.
intros s [s_eq_v' | s_in_l1]; [subst; simpl | apply (well_formed_cf_subterms Wt1); right]; trivial.
intros s [s_eq_v' | s_in_l1]; [subst; simpl | apply (well_formed_cf_alien Ar Wt1); right]; trivial.
subst l2 l2'''; apply well_formed_cf_build_inside with t; subst; trivial.
setoid_rewrite <- (flatten_apply_cf_subst sigma (Var v' :: l1) Ar);
setoid_rewrite (flatten_build l2''' Ar).
subst l2 l2'''; intros s s_in_l2'_l2'';
destruct (in_app_or _ _ _ s_in_l2'_l2'') as [s_in_l2' | s_in_l2''];
apply (well_formed_cf_alien Ar Wt2); apply in_or_app; [left | right; right]; trivial.
setoid_rewrite (@permut_cons t t).
reflexivity.
transitivity (l2' ++ t :: l2'').
pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma.
pattern (Var v') in v_sigma;
simpl apply_cf_subst in v_sigma.
rewrite v_sigma in t1_sigma; clear v_sigma.
destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial].
assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l'').
intros l' l'' H'; injection H'; intros; subst; trivial.
subst l2 cp1'; rewrite <- (Inj _ _ t1_sigma); clear Inj.
apply permut_sym; apply quick_permut_bis.
transitivity
(flatten f (apply_cf_subst sigma (Var v') :: t :: nil) ++
flatten f (map (apply_cf_subst sigma) l1)).
setoid_rewrite <- permut_app2; apply quick_permut_bis; auto.
replace (flatten f (map (apply_cf_subst sigma) (Var v' :: l1))) with
((flatten f (apply_cf_subst sigma (Var v') :: nil)) ++
flatten f (map (apply_cf_subst sigma) l1));
[ rewrite app_comm_cons | rewrite <- flatten_app; trivial].
setoid_rewrite <- permut_app2.
replace (flatten f (apply_cf_subst sigma (Var v') :: t :: nil)) with
((flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil)));
[idtac | rewrite <- flatten_app; simpl app; trivial].
replace (flatten f (t :: nil)) with (t :: nil).
apply permut_sym; setoid_rewrite <- permut_cons_inside.
reflexivity.
rewrite <- app_nil_end; auto.
simpl; destruct t as [x | g ll]; trivial.
destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g) | idtac]; trivial.
apply permut_sym; setoid_rewrite <- permut_cons_inside; subst; auto.
reflexivity.
intros Not_in Al_t;
pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma.
pattern (Var v') in v_sigma;
simpl apply_cf_subst in v_sigma.
rewrite v_sigma in t1_sigma; clear v_sigma.
destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial].
assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l'').
intros l' l'' H'; injection H'; intros; subst; trivial.
rewrite <- (Inj _ _ t1_sigma) in Not_in; clear Inj.
apply (Not_in _ (refl_equal _)).
setoid_rewrite <- in_quick_in.
apply in_or_app; left.
setoid_rewrite <- in_quick_in.
replace (flatten f (apply_cf_subst sigma (Var v') :: t :: nil)) with
(flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil)).
apply in_or_app; right; destruct t as [x | g ll]; simpl.
left; trivial.
destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g) | left ]; trivial.
rewrite <- flatten_app; simpl app; trivial.
Qed.
Lemma remove_several_subterms_bis_nil :
forall sigma f v v' t l2, arity f = AC -> well_formed_cf_subst sigma ->
well_formed_cf (Term f l2) ->
apply_cf_subst sigma (Var v) =
Term f (quicksort (flatten f (apply_cf_subst sigma (Var v') :: t :: nil))) ->
apply_cf_subst sigma (Var v) = Term f l2 ->
match t with | Var _ => True | Term g _ => f<>g end ->
match remove _ eq_term_dec t l2 with
| None => False
| Some l3 => apply_cf_subst sigma (Var v') = build f l3
end.
Proof.
intros sigma f v v' t l2 Ar W_sigma Wt2 v_sigma t1_sigma Al_t;
generalize (in_remove _ eq_term_dec t l2);
destruct (remove _ eq_term_dec t l2) as [l2''' | ].
intros [cp1 [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro l2'''_eq;
subst l2 l2'''; apply flatten_cf with f; trivial.
apply well_formed_cf_apply_subst; trivial; simpl; trivial.
apply well_formed_cf_build_inside with t; subst; trivial.
apply permut_trans with (l2' ++ l2'').
setoid_rewrite (@permut_cons t t).
reflexivity.
apply permut_trans with (l2' ++ t :: l2'').
assert (H:= trans_eq (sym_eq v_sigma) t1_sigma).
assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l'').
intros l' l'' H''; injection H''; intros; subst; trivial.
subst cp1; rewrite <- (Inj _ _ H); clear Inj.
apply permut_sym; apply quick_permut_bis.
apply permut_trans with
(flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil)).
rewrite <- flatten_app; simpl app; apply permut_refl.
refine (permut_trans (list_permut_app_app _ _) _).
simpl; destruct t as [ x | g ll ]; [apply permut_refl | idtac].
destruct (eq_symbol_dec f g) as [f_eq_g | _];
[absurd (f=g); trivial | apply permut_refl ].
apply permut_sym; setoid_rewrite <- permut_cons_inside; reflexivity.
apply permut_sym; apply flatten_build_inside with t; subst cp1; trivial.
intros Not_in; apply (Not_in _ (refl_equal _)).
assert (H := trans_eq (sym_eq v_sigma) t1_sigma).
assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l'').
intros l' l'' H'; injection H'; intros; subst; trivial.
rewrite <- (Inj _ _ H); clear Inj.
setoid_rewrite <- in_quick_in.
assert (H':= flatten_app f (apply_cf_subst sigma (Var v') :: nil) (t :: nil)).
simpl in H'; simpl; rewrite H'; apply in_or_app; right.
destruct t as [ x | g ll ]; simpl; [left; trivial | idtac].
destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g) | left ]; trivial.
Qed.
Lemma solve_is_complete :
forall pb, well_formed_pb pb -> forall sigma, is_well_formed_sol pb sigma ->
match pb.(unsolved_part) with
| nil => True
| _ :: _ => exists pb', In pb' (solve pb) /\ is_well_formed_sol pb' sigma
end.
Proof.
cut (forall f g, f=g -> arity f = arity g).
intros Ar pb W; unfold well_formed_pb in W; elim W; clear W;
intros W1_pb W; elim W; clear W;
intros W2_pb W; elim W; clear W;
intros W3_pb W4_pb sigma' S'; unfold is_well_formed_sol, solve;
elim S'; clear S';
intros sigma S'; elim S'; clear S';
intros R S';
cut (forall t:term, is_rough_sol pb (((fresh_var pb), t) :: sigma)).
unfold is_rough_sol;
intro R'; elim S'; clear S';
intros S' W_sigma; elim R; clear R;
intros S1 S2; elim S2; clear S2;
intros S2 S3;
generalize (fresh_var_spec pb); unfold occurs_in_pb;
intro Fresh_var;
destruct pb.(unsolved_part); trivial.
destruct p; rename t into t1; rename t0 into t2; elim (W1_pb t1 t2).
intros Wt1 Wt2;
generalize (S1 t1 t2 (or_introl _ (refl_equal _))); intro t1_sigma;
destruct t1 as [v | f1 l1].
cut (forall v', v'=v -> find eq_variable_dec v' (solved_part pb) =
find eq_variable_dec v (solved_part pb)).
case (find eq_variable_dec v pb.(solved_part)).
intros x_val F; generalize (F v (refl_equal _)); clear F;
intro F; elim (eq_term_dec x_val t2).
intro; subst x_val;
exists (mk_pb (existential_vars pb) l (solved_part pb)
(partly_solved_part pb)); split.
left; trivial.
exists sigma; intuition.
intro; absurd (x_val = t2); trivial.
generalize (S3 v); rewrite F; rewrite t1_sigma; intro; apply sym_eq; trivial.
intros F; generalize (F v (refl_equal _)); clear F; intro F;
cut (forall v', v'=v -> find eq_variable_dec v' (partly_solved_part pb) =
find eq_variable_dec v (partly_solved_part pb)).
case (find eq_variable_dec v pb.(partly_solved_part)).
intros pst F'; generalize (F' v (refl_equal _)); clear F';
intro F'; destruct t2 as [v2 | f2 l2].
generalize (S2 v); rewrite F'; intro E; rewrite t1_sigma in E; inversion E.
generalize (S2 v); rewrite F'; intro t1_sigma';
rewrite t1_sigma in t1_sigma';
generalize (W3_pb v); rewrite F';
intro Act; elim (eq_symbol_dec (head_symb pst) f2).
intro H; generalize (Ar _ _ (sym_eq H));
destruct (arity (head_symb pst)).
elim Act; clear Act; intros Wct Act Af2;
rewrite H in t1_sigma'; rewrite H in Act;
generalize (remove_several_subterms_bis_nil
sigma f2 v (new_var pst) (closed_term pst) l2 Af2 W_sigma Wt2
(trans_eq t1_sigma t1_sigma') t1_sigma Act);
destruct (remove _ eq_term_dec (closed_term pst) l2) as [ l2' | ].
intro t_sigma;
exists (mk_pb (existential_vars pb) ((Var (new_var pst), build f2 l2') :: l)
(solved_part pb) (partly_solved_part pb)); split.
left; trivial.
exists sigma.
split.
split.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion In_t1t2; trivial.
apply S1; right; trivial.
split; trivial.
split; trivial.
contradiction.
contradiction.
contradiction.
intro; inversion t1_sigma';
absurd (head_symb pst = f2); trivial; apply sym_eq; trivial.
intro F'; generalize (F' v (refl_equal _)); clear F';
intro F';
exists (mk_pb (existential_vars pb) l ((v, t2) :: (solved_part pb))
(partly_solved_part pb)); split.
left; trivial.
exists sigma; intuition.
simpl solved_part; simpl find;
elim (eq_variable_dec v0 v); intro v0_eq_v.
subst v0; trivial.
apply (S3 v0).
intros; subst v; trivial.
intros; subst v; trivial.
destruct t2 as [v' | f2 l2].
inversion t1_sigma.
destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2].
subst f2; generalize (Ar f1); case (arity f1).
intro Af; generalize (Af f1 (refl_equal _)); clear Af;
intro Af; generalize (sym_eq Af); clear Af; intro Af;
elim (le_gt_dec (length l1) (length l2)).
intros Ll2; unfold ac_elementary_solve; destruct l1.
absurd (2<=0); auto with arith; apply (well_formed_cf_length Af Wt1).
destruct t as [v | f k].
cut (forall v', v=v' -> find eq_variable_dec v' (solved_part pb) =
find eq_variable_dec v (solved_part pb)).
case (find eq_variable_dec v (solved_part pb)).
intros pst F; generalize (F v (refl_equal _)); clear F; intro F.
unfold ac_elementary_solve_term_var_with_val_term;
generalize (S3 v); rewrite F; intro v_sigma;
generalize
(remove_a_subterm
sigma f1 v l1 pst l2 Af W_sigma Wt1 Wt2 v_sigma t1_sigma)
(remove_several_subterms
sigma f1 v l1 pst l2 Af W_sigma Wt1 Wt2 v_sigma t1_sigma);
destruct (remove _ eq_term_dec pst l2).
intros t_sigma _;
exists (mk_pb (existential_vars pb) ((build f1 l1, build f1 l0) :: l)
(solved_part pb) (partly_solved_part pb)); split.
left; trivial.
exists sigma; split.
split.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; apply t_sigma; trivial.
apply S1; right; trivial.
split; trivial.
split; trivial.
destruct pst as [v' | f k].
contradiction.
intro; destruct (eq_symbol_dec f1 f) as [f1_eq_f | f1_diff_f].
subst f; destruct (remove_list k l2) as [k2' | ].
unfold EDS.A, DOS.A in *; elim (le_gt_dec (length l1) (length k2')).
intros _ t_sigma;
exists (mk_pb (existential_vars pb) ((build f1 l1, build f1 k2') :: l)
(solved_part pb) (partly_solved_part pb)); split.
left; trivial.
exists sigma; split.
split.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
apply S1; right; trivial.
split; trivial.
split; trivial.
contradiction.
contradiction.
intro; absurd (f1=f); trivial.
intro F; generalize (F v (refl_equal _)); clear F; intro F;
cut (forall v', v=v' -> find eq_variable_dec v' (partly_solved_part pb) =
find eq_variable_dec v (partly_solved_part pb)).
destruct (find eq_variable_dec v (partly_solved_part pb)).
intro F'; generalize (F' v (refl_equal _)); clear F'; intro F';
unfold ac_elementary_solve_term_var_with_part_val_term;
generalize (S2 v); rewrite F'; intro v_sigma;
generalize (W3_pb v); rewrite F';
elim (eq_symbol_dec f1 (head_symb p)).
intro f_eq_head_p; rewrite <- f_eq_head_p; rewrite Af;
rewrite <- f_eq_head_p in v_sigma;
intro Act; elim Act; clear Act;
intros Wct Act;
generalize (remove_several_subterms_bis
sigma f1 v (new_var p) l1 (closed_term p) l2 Af W_sigma Wt1 Wt2
v_sigma t1_sigma Act).
destruct (remove _ eq_term_dec (closed_term p) l2).
intro t_sigma;
exists (mk_pb (existential_vars pb)
((build f1 (Var (new_var p) :: l1), build f1 l0) :: l)
(solved_part pb) (partly_solved_part pb)); split.
left; trivial.
exists sigma; split.
split.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
apply S1; right; trivial.
split; trivial.
split; trivial.
contradiction.
intros f_diff_head_p Act;
apply (exists_map_without_repetition eq_term_dec
(fun pb' =>
( exists sigma'0 : substitution,
((forall t1 t2:term,
In (t1, t2) (unsolved_part pb') -> apply_cf_subst sigma'0 t1 = t2) /\
(forall v0:variable,
match find eq_variable_dec v0 (partly_solved_part pb') with
| Some pst =>
apply_cf_subst sigma'0 (Var v0) =
Term (head_symb pst)
(quicksort
(flatten (head_symb pst)
(apply_cf_subst sigma'0 (Var (new_var pst))
:: closed_term pst :: nil)))
| None => True
end) /\
(forall v0:variable,
match find eq_variable_dec v0 (solved_part pb') with
| Some t => apply_cf_subst sigma'0 (Var v0) = t
| None => True
end)) /\
(forall v0:variable,
In v0 (existential_vars pb') \/
apply_cf_subst sigma' (Var v0) = apply_cf_subst sigma'0 (Var v0)) /\
(well_formed_cf_subst sigma'0))));
exists (apply_cf_subst sigma (Var v)); split.
simpl in t1_sigma; rewrite Af in t1_sigma;
inversion_clear t1_sigma;
replace (match find eq_variable_dec v sigma with
| Some v_sigma => v_sigma
| None => Var v
end) with (apply_cf_subst sigma (Var v)); trivial;
rewrite v_sigma;
elim (eq_symbol_dec f1 (head_symb p)).
intro; absurd (f1 = head_symb p); trivial.
intros _; setoid_rewrite <- in_quick_in; left; trivial.
rewrite v_sigma;
elim (eq_symbol_dec (head_symb p) (head_symb p)).
intros _; generalize (Ar (head_symb p)); destruct (arity (head_symb p)).
elim Act; clear Act;
intros Wct Act Ahsp;
generalize (Ahsp (head_symb p) (refl_equal _)); clear Ahsp;
intro Ahsp; generalize (sym_eq Ahsp); clear Ahsp;
intro Ahsp;
cut (well_formed_cf
(Term (head_symb p)
(quicksort
(flatten (head_symb p)
(apply_cf_subst sigma (Var (new_var p)) :: closed_term p :: nil))))).
intro W;
generalize (remove_several_subterms_bis_nil sigma (head_symb p)
v (new_var p) (closed_term p) (quicksort (flatten (head_symb p)
(apply_cf_subst sigma (Var (new_var p)) :: closed_term p :: nil)))
Ahsp W_sigma W v_sigma v_sigma Act).
destruct (remove _ eq_term_dec (closed_term p)
(quicksort
(flatten (head_symb p)
(apply_cf_subst sigma (Var (new_var p)) :: closed_term p :: nil)))).
intro v'_sigma;
generalize (remove_a_subterm sigma f1 v l1
(apply_cf_subst sigma (Var v)) l2 Af W_sigma Wt1 Wt2 (refl_equal _) t1_sigma).
rewrite <- v_sigma;
destruct (remove _ eq_term_dec (apply_cf_subst sigma (Var v)) l2).
intro t_sigma; exists sigma; split.
split.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
apply S1; right; trivial.
split; trivial.
split; trivial.
rewrite v_sigma; intro; apply f_diff_head_p; trivial.
trivial.
rewrite <- v_sigma; apply well_formed_cf_apply_subst; trivial;
simpl; trivial.
contradiction.
contradiction.
intro H; apply H; trivial.
intro F'; generalize (F' v (refl_equal _)); clear F'; intro F';
unfold ac_elementary_solve_term_var_without_val_term.
apply (exists_map12_without_repetition eq_term_dec
(fun pb' =>
( exists sigma'0 : substitution,
((forall t1 t2:term,
In (t1, t2) (unsolved_part pb') -> apply_cf_subst sigma'0 t1 = t2) /\
(forall v0:variable,
match find eq_variable_dec v0 (partly_solved_part pb') with
| Some pst =>
apply_cf_subst sigma'0 (Var v0) =
Term (head_symb pst)
(quicksort
(flatten (head_symb pst)
(apply_cf_subst sigma'0 (Var (new_var pst))
:: closed_term pst :: nil)))
| None => True
end) /\
(forall v0:variable,
match find eq_variable_dec v0 (solved_part pb') with
| Some t => apply_cf_subst sigma'0 (Var v0) = t
| None => True
end)) /\
(forall v0:variable,
In v0 (existential_vars pb') \/
apply_cf_subst sigma' (Var v0)= apply_cf_subst sigma'0 (Var v0)) /\
well_formed_cf_subst sigma'0))
(fun t => match remove _ eq_term_dec t l2 with
| Some rmv =>
if le_gt_dec (length l2) (length l1 + 1)
then
(Some
(mk_pb (existential_vars pb)
((build f1 l1, build f1 rmv) :: l)
((v, t) :: (solved_part pb))
(partly_solved_part pb)), None)
else
(Some
(mk_pb (existential_vars pb)
((build f1 l1, build f1 rmv) :: l)
((v, t) :: (solved_part pb))
(partly_solved_part pb)),
Some
(mk_pb (fresh_var pb :: existential_vars pb)
((build f1 (Var (fresh_var pb) :: l1), build f1 rmv)
:: l) (solved_part pb)
((v, (mk_pst f1 (fresh_var pb) t)) ::
(partly_solved_part pb))))
| None => (None, None)
end) l2).
elim (le_gt_dec (length l2) (length l1 + 1)); intro L.
exists (apply_cf_subst sigma (Var v));
cut (match apply_cf_subst sigma (Var v) with
| Var _ => True
| Term g _ => f1<>g end).
intro Axsigma;
generalize (remove_a_subterm sigma f1 v l1 (apply_cf_subst sigma (Var v)) l2
Af W_sigma Wt1 Wt2 (refl_equal _) t1_sigma).
generalize (in_remove _ eq_term_dec (apply_cf_subst sigma (Var v)) l2);
destruct (remove _ eq_term_dec (apply_cf_subst sigma (Var v)) l2).
intros [t [l' [l'' [v_sigma_eq_t [l2_eq H]]]]] H'; split.
subst; apply in_or_app; right; left; trivial.
exists sigma; split.
split.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
apply S1; right; trivial.
split; trivial.
intro v0; simpl; elim (eq_variable_dec v0 v).
intro; subst v0; trivial.
intros _; generalize (S3 v0); simpl; trivial.
destruct (apply_cf_subst sigma (Var v)).
split; trivial.
split; trivial.
intros; destruct (apply_cf_subst sigma (Var v)).
contradiction.
absurd (f1=a); trivial.
assert (L' : 1 + length l1 = length l2).
apply le_antisym; [simpl in Ll2; trivial | rewrite plus_comm; trivial].
pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Af in t1_sigma.
assert (Inj : forall l' l'', Term f1 l' = Term f1 l'' -> l' = l'').
intros l' l'' H'; injection H'; intros; subst; trivial.
rewrite <- (Inj _ _ t1_sigma) in L'; clear Inj.
rewrite length_quicksort in L'; simpl.
assert (Wv_sigma : well_formed_cf (apply_cf_subst sigma (Var v))).
apply well_formed_cf_apply_subst; simpl; trivial.
simpl in Wv_sigma;
destruct (find eq_variable_dec v sigma) as [ [ | g ll ] | ]; trivial.
destruct (eq_symbol_dec f1 g) as [f1_eq_g | ]; trivial.
subst g; assert (L'' := well_formed_cf_length Af Wv_sigma).
rewrite length_app in L'.
assert (L''' := plus_le_compat_r _ _ (length (flatten f1 (map (apply_cf_subst sigma) l1))) L'').
rewrite <- L' in L'''.
assert (Wl1 : forall t, In t (map (apply_cf_subst sigma) l1) -> well_formed_cf t).
intros t' t'_in_map_l1; setoid_rewrite in_map_iff in t'_in_map_l1;
destruct t'_in_map_l1 as [t [Wt t_sigma]].
subst; apply well_formed_cf_apply_subst; trivial.
apply (well_formed_cf_subterms Wt1); right; trivial.
assert (L4 := length_flatten_bis Af _ Wl1); rewrite length_map in L4.
generalize (le_trans _ _ _ (plus_le_compat_l _ _ 2 L4) L''').
intro; absurd (2 + length l1 <= 1 + length l1); auto with arith.
cut (forall v', v'=v -> apply_cf_subst sigma (Var v') = apply_cf_subst sigma (Var v)).
destruct (apply_cf_subst sigma (Var v)).
intro v_sigma; generalize (v_sigma v (refl_equal _)); clear v_sigma;
intro v_sigma;
exists (Var a);
generalize (in_remove _ eq_term_dec (Var a) l2)
(remove_a_subterm sigma f1 v l1 (Var a) l2 Af
W_sigma Wt1 Wt2 v_sigma t1_sigma);
destruct (remove _ eq_term_dec (Var a) l2).
intros [t [l' [l'' [v_sigma_eq_t [l2_eq H]]]]] H'; split.
subst; apply in_or_app; right; left; trivial.
left; exists sigma; repeat split; trivial.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
apply S1; right; trivial.
simpl; intros v1; elim (eq_variable_dec v1 v).
intro; subst v1; simpl in v_sigma; trivial.
intros _; generalize (S3 v1); simpl; trivial.
contradiction.
intro v_sigma; generalize (v_sigma v (refl_equal _)); clear v_sigma;
intro v_sigma; elim (eq_symbol_dec f1 a).
intro; subst a; cut (well_formed_cf (Term f1 l0)).
intro W; destruct l0.
absurd (2<=0); auto with arith; apply (well_formed_cf_length Af W).
generalize ((well_formed_cf_alien Af W) t (or_introl _ (refl_equal _)));
intro At;
cut (well_formed_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)).
intro W_sigma0;
cut (apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma) (Var v) =
Term f1
(quicksort
(flatten f1
(apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)
(Var (fresh_var pb)) :: t :: nil)))).
intro v_sigma0;
cut (apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)
(Term f1 (Var v :: l1)) = Term f1 l2).
intro t1_sigma0;
generalize (in_remove _ eq_term_dec t l2)
(remove_several_subterms_bis
(((fresh_var pb), (build f1 l0)) :: sigma) f1 v (fresh_var pb) l1
t l2 Af W_sigma0 Wt1 Wt2 v_sigma0 t1_sigma0 At).
intros H1 H'; exists t.
destruct (remove _ eq_term_dec t l2).
destruct H1 as [t' [l' [l'' [v_sigma_eq_t' [l2_eq H]]]]]; subst t'; split.
subst; apply in_or_app; right; left; trivial.
right; exists (((fresh_var pb), (build f1 l0)) :: sigma);
elim (R' (build f1 l0)); clear R';
intros R1 R2; elim R2; clear R2;
intros R2 R3; split.
split.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
apply R1; right; trivial.
split; trivial.
simpl; intro v0; elim (eq_variable_dec v0 v).
intro; subst v0; apply v_sigma0.
generalize (R2 v0); simpl; trivial.
split; trivial.
simpl; intro v0; elim (eq_variable_dec v0 (fresh_var pb)).
intro; subst v0; left; left; trivial.
intros _; elim (S' v0); intro; [ left; right | right ]; trivial.
contradiction.
elim (R' (build f1 l0)); intros R1 _; apply R1; left; trivial.
apply trans_eq with (apply_cf_subst sigma (Var v)).
simpl; cut (v <> (fresh_var pb)).
intro v_diff_fresh; elim (eq_variable_dec v (fresh_var pb)).
intro; absurd (v=fresh_var pb); trivial.
intro; trivial.
unfold not; intro; apply Fresh_var; left;
unfold occurs_in_term_list; simpl; left; left; apply sym_eq; trivial.
rewrite v_sigma.
apply (f_equal (fun l => Term f1 l));
apply sort_is_unique.
apply (well_formed_cf_sorted Af W).
apply quick_sorted.
apply permut_sym; apply quick_permut_bis.
replace (apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)
(Var (fresh_var pb))) with (build f1 l0).
replace (flatten f1 (build f1 l0 :: t :: nil)) with (flatten f1 (build f1 l0 :: nil) ++ flatten f1 (t :: nil));
[idtac | rewrite <- flatten_app; simpl app; trivial].
refine (permut_trans (list_permut_app_app _ _) _).
apply permut_trans with (t :: flatten f1 (build f1 l0 :: nil)).
simpl; destruct t as [ | g ll]; [apply permut_refl | idtac].
destruct (eq_symbol_dec f1 g) as [f1_eq_g | _]; [absurd (f1=g); trivial | apply permut_refl].
setoid_rewrite <- permut_cons.
reflexivity.
apply flatten_build_cons with t; trivial.
simpl; elim (eq_variable_dec (fresh_var pb) (fresh_var pb)).
intros _; trivial.
intro; absurd (fresh_var pb = fresh_var pb); trivial.
unfold well_formed_cf_subst; simpl;
intro v0; elim (eq_variable_dec v0 (fresh_var pb)); intro v0_eq_fresh_var_pb.
apply (well_formed_cf_build_cons Af W).
apply W_sigma.
unfold well_formed_cf_subst in W_sigma;
generalize (W_sigma v); simpl in v_sigma; destruct (find eq_variable_dec v sigma).
subst t; trivial.
absurd (Var v = Term f1 l0); trivial; discriminate.
intro f_diff_s; exists (Term a l0);
generalize (in_remove _ eq_term_dec (Term a l0) l2)
(remove_a_subterm sigma f1 v l1 (Term a l0) l2 Af W_sigma Wt1 Wt2
v_sigma t1_sigma).
intros H1 H'; destruct (remove _ eq_term_dec (Term a l0) l2).
destruct H1 as [t' [l' [l'' [v_sigma_eq_t' [l2_eq H]]]]]; subst t'; split.
subst; apply in_or_app; right; left; trivial.
left; exists sigma; repeat split; trivial.
intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
inversion_clear In_t1t2; trivial.
apply S1; right; trivial.
simpl; intros v1; elim (eq_variable_dec v1 v).
intro; subst v1; simpl in v_sigma; trivial.
intros _; generalize (S3 v1); simpl; trivial.
absurd (f1=a); trivial.
intros; subst v; trivial.
intros; subst v; trivial.
intros; subst v; trivial.
unfold ac_elementary_solve_term_term_term.
apply (exists_map_without_repetition eq_term_dec
(fun pb' =>
(exists sigma'0 : substitution,
((forall t1 t2:term,
In (t1, t2) (unsolved_part pb') -> apply_cf_subst sigma'0 t1 = t2) /\
(forall v:variable,
match find eq_variable_dec v (partly_solved_part pb') with
| Some pst =>
apply_cf_subst sigma'0 (Var v) =
Term (head_symb pst)
(quicksort
(flatten (head_symb pst)
(apply_cf_subst sigma'0 (Var (new_var pst))
:: closed_term pst :: nil)))
| None => True
end) /\
(forall v:variable,
match find eq_variable_dec v (solved_part pb') with
| Some t => apply_cf_subst sigma'0 (Var v) = t
| None => True
end)) /\
(forall v:variable,
In v (existential_vars pb') \/
apply_cf_subst sigma' (Var v) = apply_cf_subst sigma'0 (Var v)) /\
(well_formed_cf_subst sigma'0)))).
exists (apply_cf_subst sigma (Term f k)).
assert (f_diff_s := well_formed_cf_alien Af Wt1 _ (or_introl _ (refl_equal _))).
simpl in f_diff_s.
assert (s_l0_in_l2 : In (apply_cf_subst sigma (Term f k)) l2).
generalize (S1 _ _ (or_introl _ (refl_equal _))); simpl; rewrite Af;
destruct (eq_symbol_dec f1 f) as [f1_eq_f | _]; [absurd (f1=f); trivial | idtac].
intro H; injection H; intros; subst l2.
setoid_rewrite <- in_quick_in; left; trivial.
split; [trivial | idtac].
generalize (in_remove _ eq_term_dec (apply_cf_subst sigma (Term f k)) l2);
destruct (remove _ eq_term_dec (apply_cf_subst sigma (Term f k)) l2) as
[l2''' | ]; [idtac | intro; absurd (In (apply_cf_subst sigma (Term f k)) l2); trivial].
intros [a' [l2' [l2'' [H [l2_eq l2'''_eq]]]]]; subst a';
injection l2'''_eq; clear l2'''_eq; intro; subst l2 l2''';
simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f];
[idtac | absurd (f = f); trivial].
exists sigma; repeat split; trivial.
simpl unsolved_part; intros t1 t2 [In_t1t2 | [In_t1t2 | In_t1t2]].
injection In_t1t2; intros; subst.
apply flatten_cf with f1; trivial.
apply well_formed_cf_apply_subst; trivial;
apply (well_formed_cf_subterms Wt1); left; trivial.
apply (well_formed_cf_apply_subst W_sigma (Term f k)).
apply (well_formed_cf_subterms Wt1); left; trivial.
apply permut_refl.
injection In_t1t2; intros; subst.
apply flatten_cf with f1; trivial.
apply well_formed_cf_apply_subst; trivial;
apply well_formed_cf_build_cons with (Term f k); trivial.
apply well_formed_cf_build_inside with (apply_cf_subst sigma (Term f k)); trivial.
setoid_rewrite <- (flatten_apply_cf_subst sigma l1 Af);
setoid_rewrite (flatten_build (l2' ++ l2'') Af).
intros t t_in_l2'_l2'';
destruct (in_app_or _ _ _ t_in_l2'_l2'') as [t_in_l2' | t_in_l2''];
apply (well_formed_cf_alien Af Wt2); apply in_or_app; [left | right; right]; trivial.
setoid_rewrite (@permut_cons (apply_cf_subst sigma (Term f k))
(apply_cf_subst sigma (Term f k))).
reflexivity.
transitivity (l2' ++ apply_cf_subst sigma (Term f k) :: l2'').
simpl in t1_sigma; rewrite Af in t1_sigma;
simpl; inversion_clear t1_sigma;
apply permut_sym; apply quick_permut_bis;
elim (eq_symbol_dec f1 f).
intro; absurd (f1=f); trivial.
intros _; auto.
apply permut_sym; setoid_rewrite <- permut_cons_inside; auto.
reflexivity.
apply S1; right; trivial.
apply H; trivial.
intro L; absurd (length l1 > length l2); trivial;
unfold gt; apply le_not_lt;
simpl in t1_sigma; rewrite Af in t1_sigma; inversion_clear t1_sigma;
rewrite length_quicksort;
apply length_flatten_ter; trivial.
intros; apply (well_formed_cf_subterms Wt1); trivial.
intro Af; generalize (Af f1 (refl_equal _)); clear Af; intro Af;
generalize (sym_eq Af); clear Af; intro Af.
elim Wt1; intros _ H; rewrite Af in H; elim H; clear H;
intros Ll1 _;
elim Wt2; intros _ H; rewrite Af in H; elim H; clear H;
intros Ll2 _; destruct l1.
simpl in Ll1; absurd (0=2); trivial.
destruct l1.
simpl in Ll1; absurd (1=2); trivial.
destruct l1.
destruct l2.
simpl in Ll2; absurd (0=2); trivial.
destruct l2.
simpl in Ll2; absurd (1=2); trivial.
destruct l2.
simpl in t1_sigma; rewrite Af in t1_sigma; inversion t1_sigma;
generalize (quick_permut
(apply_cf_subst sigma t :: apply_cf_subst sigma t0 :: nil));
rewrite H0; intro P;
elim (list_permut.permut_length_2 P); clear P;
intro P; elim P; clear P; intros t_sigma t0_sigma.
exists (mk_pb (existential_vars pb) ((t, t1) :: (t0, t2) :: l) (solved_part pb)
(partly_solved_part pb)); split.
left; trivial.
exists sigma; repeat split; trivial.
intros t3 t4 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
injection In_t1t2; intros; subst t3 t4; trivial.
elim In_t1t2; clear In_t1t2; intro In_t1t2.
injection In_t1t2; intros; subst t3 t4; trivial.
apply S1; right; trivial.
exists (mk_pb (existential_vars pb) ((t, t2) :: (t0, t1) :: l)
(solved_part pb) (partly_solved_part pb)); split.
right; left; trivial.
exists sigma; repeat split; trivial.
intros t3 t4 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2.
injection In_t1t2; intros; subst t3 t4; trivial.
elim In_t1t2; clear In_t1t2; intro In_t1t2.
injection In_t1t2; intros; subst t3 t4; trivial.
apply S1; right; trivial.
simpl in Ll2; discriminate.
simpl in Ll1; discriminate.
intros n Af; generalize (Af f1 (refl_equal _)); clear Af; intro Af;
generalize (sym_eq Af); clear Af; intro Af;
simpl in t1_sigma; rewrite Af in t1_sigma;
inversion t1_sigma.
generalize (length_map (apply_cf_subst sigma) l1); rewrite H0;
intro L;
cut (forall t1 t2, In (t1,t2) l -> apply_cf_subst sigma t1 = t2).
subst l2; clear L Fresh_var R' W1_pb S1 Wt1 Wt2 t1_sigma;
intros S1.
cut (match
fold_left2
(fun (current_list_of_eqs : list _) t1 t2 => (t1,t2) :: current_list_of_eqs)
l l1 (map (apply_cf_subst sigma) l1) with
| None => False
| Some new_list_of_equations =>
(forall t1 t2, In (t1,t2) new_list_of_equations ->
apply_cf_subst sigma t1 = t2)
end).
destruct (fold_left2 (fun (current_list_of_eqs : list _) t1 t2 =>
(t1,t2) :: current_list_of_eqs)
l l1 (map (apply_cf_subst sigma) l1)).
clear S1; intro S1;
exists (mk_pb (existential_vars pb) l0 (solved_part pb)
(partly_solved_part pb)); split.
left; trivial.
exists sigma; intuition.
contradiction.
generalize S1; clear S1; generalize l; induction l1; simpl; trivial.
intros l0 S1.
apply (IHl1 ((a, apply_cf_subst sigma a) :: l0));
intros t1 t2 I; elim I; clear I; intro I.
inversion I; trivial.
apply S1; trivial.
intros; apply S1; right; trivial.
absurd (f1=f2); trivial.
simpl in t1_sigma; injection t1_sigma; trivial.
left; trivial.
intro t; apply add_new_var_to_rough_sol; trivial.
do 3 (split; trivial).
intro f; intros; subst f; trivial.
Qed.
End Make.