Library ac_matching.matching_sound
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_well_formed.
Module Type S.
Declare Module Import WFMMatching : matching_well_formed.S.
Import WFMMatching.
Import WFMatching.
Import Matching.
Import Cf_eq_ac.
Import Ac.
Import EqTh.
Import T.
Axiom solve_is_sound :
forall pb sigma, well_formed_pb pb ->
forall pb', In pb' (solve pb) -> is_sol pb' sigma -> is_sol pb sigma.
End S.
Module Make (WFMMatching1 : matching_well_formed.S) :
S with Module WFMMatching := WFMMatching1.
Module Import WFMMatching := WFMMatching1.
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 add_a_subterm :
forall f l l' t, arity f = AC -> (well_formed_cf (Term f (l ++ t :: l'))) ->
permut (flatten f (build f (l ++ l') :: t :: nil)) (l ++ t :: l').
Proof.
intros f l l' t Af W.
assert (Al_t : match t with | Var _ => True | Term g ll => f <> g end).
apply (well_formed_cf_alien Af W); apply in_or_app; right; left; trivial.
replace (build f (l ++ l') :: t :: nil) with ((build f (l ++ l') :: nil) ++ (t :: nil)); trivial.
rewrite flatten_app; replace (flatten f (t :: nil)) with (t :: nil).
setoid_rewrite <- permut_add_inside.
reflexivity.
rewrite <- app_nil_end;
apply flatten_build_inside with t; trivial.
simpl; destruct t as [ v | g ll]; [auto | idtac];
destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g); trivial | auto].
Qed.
Lemma add_a_subterm_subst :
forall f l1 l2' l2'' t sigma, arity f = AC ->
well_formed_cf (Term f (l2' ++ t :: l2'')) ->
apply_cf_subst sigma (build f l1) = build f (l2' ++ l2'') ->
permut (flatten f (t :: (map (apply_cf_subst sigma) l1))) (l2' ++ t :: l2'').
Proof.
intros f l1 l2' l2'' t sigma Af Wt2 t1_sigma.
assert (Al_t : match t with | Var _ => True | Term g ll => f <> g end).
apply (well_formed_cf_alien Af Wt2); apply in_or_app; right; left; trivial.
simpl; destruct t as [ v | g ll].
setoid_rewrite <- permut_cons_inside.
reflexivity.
refine (permut_trans (flatten_apply_cf_subst sigma l1 Af) _);
rewrite t1_sigma; apply flatten_build_inside with (Var v); trivial.
destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g); trivial | auto].
setoid_rewrite <- permut_cons_inside.
reflexivity.
refine (permut_trans (flatten_apply_cf_subst sigma l1 Af) _);
rewrite t1_sigma; apply flatten_build_inside with (Term g ll); trivial.
Qed.
Lemma solve_is_sound :
forall pb sigma, well_formed_pb pb ->
forall pb', In pb' (solve pb) -> is_sol pb' sigma -> is_sol pb sigma.
Proof.
intros pb; assert (R := add_new_var_to_rough_sol pb);
unfold is_sol, solve, well_formed_pb in R;
unfold is_sol, solve, well_formed_pb;
intros sigma [W1 [W2 [W3 [W4 [W5 W6]]]]] pb' In_pb';
assert (U_pb : forall pb', pb' = pb -> unsolved_part pb' = unsolved_part pb).
intros; subst; trivial.
destruct (unsolved_part pb) as [ | [[v1 | f1 l1] t2] l];
generalize (U_pb pb (refl_equal _)); clear U_pb; intro U_pb.
contradiction.
assert (F : forall v, v=v1 -> find eq_variable_dec v (solved_part pb) =
find eq_variable_dec v1 (solved_part pb)). intros; subst; trivial.
destruct (find eq_variable_dec v1 (solved_part pb)) as [t1 | ];
generalize (F v1 (refl_equal _)); clear F; intro F.
destruct (eq_term_dec t1 t2) as [t1_eq_t2 | _]; [idtac | contradiction];
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst t2 pb'.
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol; do 2 (split; trivial).
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | apply H1; trivial];
injection st_eq; intros; subst; generalize (H3 v1); simpl solved_part; rewrite F; trivial.
intuition.
generalize (W3 v1);
assert (F' : forall v, v=v1 -> find eq_variable_dec v (partly_solved_part pb) =
find eq_variable_dec v1 (partly_solved_part pb)). intros; subst; trivial.
destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [p1 | ];
generalize (F' v1 (refl_equal _)); clear F'; intro F'.
destruct t2 as [ v2 | f2 l2]; [contradiction | idtac];
destruct (eq_symbol_dec (head_symb p1) f2) as [f1_eq_f2 | ]; [idtac | contradiction];
rewrite f1_eq_f2; destruct_arity f2 n2 Af2; [ idtac | contradiction | contradiction].
intros _; generalize (in_remove _ eq_term_dec (closed_term p1) l2);
destruct (remove _ eq_term_dec (closed_term p1) l2) as [ l2''' |]; [idtac | contradiction].
intros [cp1 [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst l2''';
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction].
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol;
split; [split | idtac]; subst pb'; trivial.
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | apply H1; subst; right; trivial];
injection st_eq; intros; subst;
generalize (H2 v1); simpl partly_solved_part; rewrite F'; intro H; rewrite H;
apply (f_equal (fun l => Term (head_symb p1) l)); apply sort_is_unique.
apply quick_sorted.
apply well_formed_cf_sorted with (head_symb p1); trivial;
refine (proj2 _ (A:= well_formed_cf (Var v1))); apply W1; left; trivial.
apply quick_permut_bis;
rewrite (H1 (Var (new_var p1)) (build (head_symb p1) (l2' ++ l2''))); [idtac | left; trivial];
apply add_a_subterm; trivial;
refine (proj2 _ (A:= well_formed_cf (Var v1))); apply W1; left; trivial.
split; trivial.
intros _; generalize In_pb'; clear In_pb'; intros [pb'_eq | ]; [subst pb' | contradiction].
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol;
split; [split; [idtac | split] | idtac].
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | apply H1; trivial].
injection st_eq; intros; subst; generalize (H3 v1); simpl;
destruct (eq_variable_dec v1 v1) as [ _ | v1_diff_v1]; [idtac | absurd (v1 = v1)]; trivial.
apply H2.
intro v; generalize (H3 v); simpl;
destruct (eq_variable_dec v v1) as [v_eq_v1 | v_diff_v1]; [ subst; rewrite F | idtac]; trivial.
apply H4.
destruct t2 as [ v2 | f2 l2 ]; [contradiction | idtac];
destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | _]; [idtac | contradiction].
subst f2; destruct_arity f1 n1 Af1.
destruct (le_gt_dec (length l1) (length l2)) as [_ | _]; [idtac | contradiction].
unfold ac_elementary_solve in *.
assert (W_t1 : well_formed_cf (Term f1 l1)).
refine (proj1 _ (B:= (well_formed_cf (Term f1 l2)))); apply W1; left; trivial.
assert (W_t2 : well_formed_cf (Term f1 l2)).
apply (proj2 (A:= (well_formed_cf (Term f1 l1)))); apply W1; left; trivial.
destruct l1 as [ | t1 l1].
absurd (2 <= @length term nil); auto with arith;
apply well_formed_cf_length with f1; trivial.
destruct t1 as [v1 | g1 ll1].
assert (F : forall v, v=v1 -> find eq_variable_dec v (solved_part pb) =
find eq_variable_dec v1 (solved_part pb)). intros; subst; trivial.
generalize (W2 v1);
destruct (find eq_variable_dec v1 (solved_part pb)) as [s1 | ];
generalize (F v1 (refl_equal _)); clear F; intro F.
intro W_s1; unfold ac_elementary_solve_term_var_with_val_term in *.
generalize (in_remove _ eq_term_dec s1 l2);
destruct (remove _ eq_term_dec s1 l2) as [ l2''' |].
intros [cp1 [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst l2''';
inversion_clear In_pb' as [pb'_eq_ | ]; [subst pb' | contradiction].
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol;
split; [split; [idtac | split] | idtac]; trivial.
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | subst; apply H1; right; trivial];
injection st_eq; intros; subst.
replace (apply_cf_subst sigma' (Term f1 (Var v1 :: l1))) with
(Term f1 (quicksort (flatten f1 (cp1 :: map (apply_cf_subst sigma') l1)))).
apply (f_equal (fun l => Term f1 l)).
apply sort_is_unique.
apply quick_sorted.
apply well_formed_cf_sorted with f1; trivial.
apply quick_permut_bis.
apply add_a_subterm_subst; trivial; apply H1; left; trivial.
generalize (H3 v1); simpl; rewrite F; rewrite Af1; intro H3_v1; rewrite H3_v1; trivial.
intros _; destruct s1 as [| g1 ll1]; [contradiction | idtac ];
destruct (eq_symbol_dec f1 g1) as [f1_eq_g1 | _]; [idtac | contradiction].
assert (S_ll1 : is_sorted ll1).
apply well_formed_cf_sorted with g1; subst; trivial.
assert (S_l2 : is_sorted l2).
apply well_formed_cf_sorted with f1; trivial.
generalize (in_remove_list S_ll1 S_l2); unfold EDS.A, DOS.A in *;
destruct (remove_list ll1 l2) as [l2' | ]; [idtac | contradiction ].
unfold EDS.A, DOS.A in *; destruct (le_gt_dec (length l1) (length l2')) as [L_l1_l2' |]; [idtac | contradiction].
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction].
intros P [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol; subst pb' g1;
split; [split; [idtac | split] | idtac]; trivial.
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | subst; apply H1; right; trivial];
injection st_eq; intros; subst;
replace (apply_cf_subst sigma' (Term f1 (Var v1 :: l1))) with
(Term f1 (quicksort (flatten f1 ((Term f1 ll1) :: map (apply_cf_subst sigma') l1)))).
apply (f_equal (fun l => Term f1 l)).
apply sort_is_unique.
apply quick_sorted.
apply well_formed_cf_sorted with f1; trivial.
apply quick_permut_bis;
simpl; destruct (eq_symbol_dec f1 f1) as [_ | f1_diff_f1]; [idtac | absurd (f1 = f1); trivial].
transitivity (ll1 ++ l2'); trivial.
setoid_rewrite <- permut_app1.
setoid_rewrite (flatten_apply_cf_subst sigma' l1 Af1);
rewrite (H1 (build f1 l1) (build f1 l2')); [idtac | left; trivial]; apply flatten_build; trivial.
intros t In_t; apply well_formed_cf_alien with l2; trivial;
setoid_rewrite <- (list_permut.in_permut_in P); apply in_or_app; right; trivial.
generalize (H3 v1); simpl; rewrite F; rewrite Af1; intro H3_v1; rewrite H3_v1; trivial.
intros _; generalize (W3 v1);
assert (F' : forall v, v=v1 -> find eq_variable_dec v (partly_solved_part pb) =
find eq_variable_dec v1 (partly_solved_part pb)). intros; subst; trivial.
destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [p1 | ];
generalize (F' v1 (refl_equal _)); clear F'; intro F'.
unfold ac_elementary_solve_term_var_with_part_val_term in *.
destruct (eq_symbol_dec f1 (head_symb p1)) as [f1_eq_hd_p1 | f1_diff_hd_p1].
generalize (in_remove _ eq_term_dec (closed_term p1) l2);
destruct (remove _ eq_term_dec (closed_term p1) l2) as [l2''' | ]; [idtac | contradiction].
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction].
intros [cp1 [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro l2'''_eq; subst pb'.
intros _ [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol;
split; [split; [idtac | split] | idtac]; trivial.
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | subst; apply H1; right; trivial];
injection st_eq; intros; subst s t; clear st_eq.
assert (v1_sigma'_eq : apply_cf_subst sigma' (Var v1) =
Term f1 (quicksort (flatten f1 (apply_cf_subst sigma' (Var (new_var p1)) ::
closed_term p1 :: nil)))).
generalize (H2 v1); simpl; rewrite F'; subst f1; trivial.
assert (l1_sigma'_eq :=
(H1 (build f1 (Var (new_var p1) :: l1)) (build f1 l2''') (or_introl _ (refl_equal _)))).
replace (apply_cf_subst sigma' (Term f1 (Var v1 :: l1))) with
(Term f1 (quicksort (flatten f1 (((apply_cf_subst sigma' (Var v1)) :: nil) ++
map (apply_cf_subst sigma') l1))));
[ idtac | simpl; rewrite Af1; trivial];
apply (f_equal (fun l => Term f1 l)).
apply sort_is_unique.
apply quick_sorted.
apply well_formed_cf_sorted with f1; trivial.
replace (build f1 (Var (new_var p1) :: l1)) with
(Term f1 (quicksort (Var (new_var p1) :: l1))) in l1_sigma'_eq.
simpl in l1_sigma'_eq; rewrite Af1 in l1_sigma'_eq.
transitivity (closed_term p1 :: l2''');
[idtac | subst l2; setoid_rewrite <- permut_cons_inside; auto].
assert (build_f1_l2'''_eq : build f1 l2''' = Term f1 (quicksort l2''')).
destruct l2''' as [ | u2 [ | u2' l2''']];
[simpl; rewrite quicksort_equation; trivial | idtac | trivial].
assert (Al_u2 : match u2 with | Var _ => True | Term g _ => f1 <> g end).
apply (well_formed_cf_alien Af1 W_t2).
subst l2; assert (u2_in_l2'_l2'' : In u2 (l2' ++ l2'')). rewrite <- l2'''_eq; left; trivial.
destruct (in_app_or _ _ _ u2_in_l2'_l2''); apply in_or_app; [left | right; right]; trivial.
simpl in l1_sigma'_eq; destruct u2 as [ | g2];
[discriminate | injection l1_sigma'_eq; intros; subst g2; absurd (f1 = f1); trivial].
replace (build f1 l2''') with (Term f1 (quicksort l2''')) in l1_sigma'_eq; trivial.
assert (P : permut (flatten f1 (map (apply_cf_subst sigma') (Var (new_var p1) :: l1)))
l2''').
apply permut_sym; transitivity (quicksort l2''').
apply quick_permut.
injection l1_sigma'_eq; intros H''; rewrite <- H''; clear H'';
apply quick_permut_bis.
apply list_permut_flatten.
apply list_permut.permut_map with (@eq term).
intros; subst; reflexivity.
apply quick_permut_bis; auto.
apply quick_permut_bis.
transitivity (closed_term p1 :: (flatten f1 (map (apply_cf_subst sigma') (Var (new_var p1) :: l1))));
[idtac | setoid_rewrite <- permut_cons; trivial].
rewrite v1_sigma'_eq; rewrite flatten_app;
replace (map (apply_cf_subst sigma') (Var (new_var p1) :: l1)) with
(apply_cf_subst sigma' (Var (new_var p1)) :: map (apply_cf_subst sigma') l1); trivial.
generalize (map (apply_cf_subst sigma') l1) (apply_cf_subst sigma' (Var (new_var p1)));
intros l1_sigma' t; replace (t :: l1_sigma') with ((t :: nil) ++ l1_sigma'); trivial;
rewrite flatten_app; rewrite app_comm_cons; setoid_rewrite <- permut_app2.
assert (Al_ct : match closed_term p1 with | Var _ => True | Term g _ => f1 <> g end).
generalize (W3 v1); rewrite F'; rewrite <- f1_eq_hd_p1; rewrite Af1; intuition.
pattern (quicksort (flatten f1 (t :: closed_term p1 :: nil))); simpl flatten at 1;
destruct (eq_symbol_dec f1 f1) as [ _ | f1_diff_f1]; [idtac | absurd (f1 = f1); trivial].
rewrite <- app_nil_end; apply quick_permut_bis.
replace (flatten f1 (t :: closed_term p1 :: nil)) with
(flatten f1 (t :: nil) ++ flatten f1 (closed_term p1 :: nil)).
simpl flatten at 2.
destruct (closed_term p1) as [v | g ll];
[idtac | destruct (eq_symbol_dec f1 g) as [f_eq_g1 | _]; [absurd (f1 = g); trivial | idtac ]];
apply permut_sym; setoid_rewrite <- permut_cons_inside.
reflexivity.
rewrite <- app_nil_end; reflexivity.
reflexivity.
rewrite <- app_nil_end; reflexivity.
rewrite <- flatten_app; simpl; reflexivity.
reflexivity.
subst; auto.
rewrite build_eq_Term; trivial; simpl;
generalize (well_formed_cf_length Af1 W_t1); simpl; trivial.
intros W3_v1;
pattern pb';
refine
(prop_map_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb');
clear pb' In_pb'; intros [ | g2 ll2] In_t2; trivial;
destruct (eq_symbol_dec g2 (head_symb p1)) as [g2_eq_hd_p1 | g2_diff_hd_p1]; trivial.
generalize (in_remove _ eq_term_dec (closed_term p1) ll2);
destruct (remove _ eq_term_dec (closed_term p1) ll2) as [ll2''' | ]; trivial;
intros [cp1 [ll2' [ll2'' [ H' [ll2_eq ll2'''_eq]]]]].
injection ll2'''_eq; clear ll2'''_eq; intro ll2'''_eq;
generalize (in_remove _ eq_term_dec (Term g2 ll2) l2);
destruct (remove _ eq_term_dec (Term g2 ll2) l2) as [l2''' | ]; trivial.
intros [cp1' [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro l2'''_eq;
assert (Ag2 : arity g2 = AC).
rewrite <- g2_eq_hd_p1 in W3_v1; destruct (arity g2); [trivial | contradiction | contradiction].
assert (W_g2_ll2 : well_formed_cf (Term g2 ll2)).
apply well_formed_cf_subterms with f1 l2; trivial.
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol;
split; [split; [idtac | split] | idtac]; trivial.
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | subst; apply H1; right; right; trivial];
injection st_eq; intros; subst s t; clear st_eq.
assert (v1_sigma'_eq : apply_cf_subst sigma' (Var v1) =
Term (head_symb p1)
(quicksort (flatten (head_symb p1) (apply_cf_subst sigma' (Var (new_var p1)) ::
closed_term p1 :: nil)))).
generalize (H2 v1); simpl; rewrite F'; trivial.
assert (l1_sigma'_eq :=
(H1 (build f1 l1) (build f1 l2''') ((or_intror _ (or_introl _ (refl_equal _)))))).
replace (apply_cf_subst sigma' (Term f1 (Var v1 :: l1)))
with (Term f1 (quicksort (flatten f1 (((apply_cf_subst sigma' (Var v1)) :: nil) ++ map (apply_cf_subst sigma') l1))));
[ idtac | simpl; rewrite Af1; trivial];
apply (f_equal (fun l => Term f1 l)).
apply sort_is_unique.
apply quick_sorted.
apply well_formed_cf_sorted with f1; trivial.
apply quick_permut_bis; rewrite flatten_app.
transitivity
(flatten f1 (apply_cf_subst sigma' (Var v1) :: nil) ++
(flatten f1 (build f1 l2''' :: nil))).
setoid_rewrite <- permut_app1; rewrite <- l1_sigma'_eq;
apply flatten_apply_cf_subst; trivial.
transitivity (flatten f1 (apply_cf_subst sigma' (Var v1) :: nil) ++ l2''').
setoid_rewrite <- permut_app1; apply flatten_build; trivial;
intros t In_t; apply (well_formed_cf_alien Af1 W_t2); subst l2 l2''';
generalize (in_app_or _ _ _ In_t); clear In_t; intros [In_t | In_t];
apply in_or_app; [left | right; right]; trivial.
subst l2 l2''' cp1'.
replace (l2' ++ Term g2 ll2 :: l2'') with ((l2' ++ Term g2 ll2 :: nil) ++ l2'').
rewrite <- app_ass; setoid_rewrite <- permut_app2.
refine (permut_trans _ (list_permut_app_app _ _));
setoid_rewrite <- permut_app2.
assert (new_var_p1_sigma'_eq :=
(H1 (Var (new_var p1)) (build g2 ll2''') (or_introl _ (refl_equal _)))).
rewrite v1_sigma'_eq; rewrite new_var_p1_sigma'_eq; rewrite <- g2_eq_hd_p1;
transitivity
(Term g2
(quicksort
(flatten g2 (build g2 ll2''' :: closed_term p1 :: nil)))
:: nil).
simpl; destruct (eq_symbol_dec f1 g2) as [f1_eq_g2 | _];
[absurd (f1 = g2); subst; trivial | auto].
replace ll2 with (quicksort (flatten g2 (build g2 ll2''' :: closed_term p1 :: nil))); auto;
apply sort_is_unique.
apply quick_sorted.
apply well_formed_cf_sorted with g2; trivial.
apply quick_permut_bis;
replace (build g2 ll2''' :: closed_term p1 :: nil) with
((build g2 ll2''' :: nil) ++ (closed_term p1 :: nil)); trivial;
rewrite flatten_app.
transitivity (ll2''' ++ flatten g2 (closed_term p1 :: nil)).
setoid_rewrite <- permut_app2; apply flatten_build; trivial.
intros t In_t; apply well_formed_cf_alien with ll2; trivial;
subst ll2 ll2'''; generalize (in_app_or _ _ _ In_t); clear In_t; intros [In_t | In_t];
apply in_or_app; [left | right; right]; trivial.
replace (flatten g2 (closed_term p1 :: nil)) with (closed_term p1 :: nil).
subst ll2 ll2'''; simpl; setoid_rewrite <- permut_add_inside.
subst; reflexivity.
rewrite <- app_nil_end; auto.
simpl; destruct (arity (head_symb p1)) as [ | | ]; [idtac | contradiction | contradiction].
generalize (well_formed_cf_alien Ag2 W_g2_ll2 cp1); subst.
destruct (closed_term p1) as [ | g1]; trivial.
destruct (eq_symbol_dec (head_symb p1) g1) as [g2_eq_g1 | ]; trivial.
intro H; absurd (head_symb p1 = g1); trivial.
apply H; apply in_or_app; right; trivial.
left; trivial.
rewrite app_ass; simpl; trivial.
intros _; unfold ac_elementary_solve_term_var_without_val_term in *.
pattern pb';
refine
(prop_map12_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb');
clear pb' In_pb';
intros t2 In_t2; generalize (in_remove _ eq_term_dec t2 l2);
destruct (remove _ eq_term_dec t2 l2) as [l2''' | ]; trivial;
intros [cp1' [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro l2'''_eq;
assert (Common :
(exists sigma' : substitution,
is_rough_sol
(mk_pb (existential_vars pb) ((build f1 l1, build f1 l2''') :: l)
((v1, t2) :: solved_part pb) (partly_solved_part pb)) sigma' /\
(forall v : variable,
In v
(existential_vars
(mk_pb (existential_vars pb) ((build f1 l1, build f1 l2''') :: l)
((v1, t2) :: solved_part pb) (partly_solved_part pb))) \/
apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v))) ->
exists sigma' : substitution,
is_rough_sol pb sigma' /\
(forall v : variable,
In v (existential_vars pb) \/
apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v))).
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma'; unfold is_rough_sol;
split; [split; [idtac | split] | idtac]; trivial.
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | subst; apply H1; right; trivial];
injection st_eq; intros; subst s t; clear st_eq.
assert (v1_sigma'_eq : apply_cf_subst sigma' (Var v1) = t2).
generalize (H3 v1); simpl.
destruct (eq_variable_dec v1 v1) as [ _ | v1_diff_v1]; [idtac | absurd (v1 = v1)] ; trivial.
assert (l1_sigma'_eq := H1 (build f1 l1) (build f1 l2''') (or_introl _ (refl_equal _))).
replace (apply_cf_subst sigma' (Term f1 (Var v1 :: l1)))
with (Term f1 (quicksort (flatten f1 ((t2 :: nil) ++ map (apply_cf_subst sigma') l1))));
[ idtac | rewrite <- v1_sigma'_eq; simpl; rewrite Af1; trivial];
apply (f_equal (fun l => Term f1 l));
apply sort_is_unique;
[ apply quick_sorted | apply (well_formed_cf_sorted Af1 W_t2) | idtac];
apply quick_permut_bis; rewrite flatten_app;
assert (Ft2 : flatten f1 (t2 :: nil) = t2 :: nil).
generalize (well_formed_cf_alien Af1 W_t2 _ In_t2); intro;
destruct t2 as [ | g2]; trivial; simpl;
destruct (eq_symbol_dec f1 g2) as [f1_eq_g2 | _]; [absurd (f1 = g2); trivial | auto].
rewrite Ft2; subst l2; simpl; setoid_rewrite <- permut_cons_inside.
subst; reflexivity.
setoid_rewrite (flatten_apply_cf_subst sigma' l1 Af1); rewrite l1_sigma'_eq;
subst; apply flatten_build; trivial;
intros t In_t; apply (well_formed_cf_alien Af1 W_t2);
generalize (in_app_or _ _ _ In_t); clear In_t; intros [In_t | In_t];
apply in_or_app; [left | right; right]; trivial.
intro v; generalize (H3 v); simpl;
destruct (eq_variable_dec v v1) as [v_eq_v1 | _]; [subst; rewrite F | idtac]; trivial.
unfold EDS.A, DOS.A in *; destruct (le_gt_dec (length l2) (length l1 + 1)) as [_ | _]; trivial;
split; trivial; clear Common.
intros [sigma' [[H1 [H2 H3]] H4]];
exists ((fresh_var pb, apply_cf_subst sigma (Var (fresh_var pb))) :: sigma'); split.
apply R; [intuition | idtac].
split; [idtac | split] ; trivial.
rewrite U_pb; intros s t [st_eq | In_st]; [idtac | subst; apply H1; right; trivial];
injection st_eq; intros; subst s t; clear st_eq.
simpl; rewrite Af1; apply (f_equal (fun l => Term f1 l));
apply sort_is_unique; [ apply quick_sorted | apply (well_formed_cf_sorted Af1 W_t2) | idtac];
apply quick_permut_bis;
generalize (H2 v1); unfold partly_solved_part; simpl find;
destruct (eq_variable_dec v1 v1) as [ _ | v1_diff_v1]; [idtac | absurd (v1 = v1); trivial];
intro H2_v1; fold (apply_cf_subst sigma' (Var v1)); rewrite H2_v1; clear H2_v1;
simpl head_symb; simpl new_var; simpl closed_term;
destruct (eq_symbol_dec f1 f1) as [ _ | f1_diff_f1]; [idtac | absurd (f1 = f1); trivial].
transitivity
(flatten f1 (apply_cf_subst sigma' (Var (fresh_var pb)) :: t2 :: nil) ++
flatten f1 (map (apply_cf_subst sigma') l1));
[setoid_rewrite <- permut_app2; apply quick_permut_bis; auto | idtac].
replace (apply_cf_subst sigma' (Var (fresh_var pb)) :: t2 :: nil) with
((apply_cf_subst sigma' (Var (fresh_var pb)) :: nil) ++ (t2 :: nil)); trivial.
subst l2 l2''' cp1'; setoid_rewrite <- (add_a_subterm _ _ _ _ Af1 W_t2);
replace (build f1 (l2' ++ l2'') :: t2 :: nil) with ((build f1 (l2' ++ l2'') :: nil) ++ (t2 :: nil)); trivial.
do 2 rewrite flatten_app; replace (flatten f1 (t2 :: nil)) with (t2 :: nil);
[idtac | destruct t2 as [ | g2]; simpl; trivial;
destruct (eq_symbol_dec f1 g2) as [f1_eq_g2 | ]; trivial;
absurd (f1 = g2); trivial; apply (well_formed_cf_alien Af1 W_t2 _ In_t2)].
rewrite app_ass; rewrite <- app_comm_cons.
setoid_rewrite <- permut_add_inside.
reflexivity.
rewrite <- app_ass; do 2 rewrite <- app_nil_end.
apply permut_sym;
rewrite <- (H1 (build f1 (Var (fresh_var pb) :: l1)) (build f1 (l2' ++ l2'')) (or_introl _ (refl_equal _))).
rewrite build_eq_Term; [idtac | generalize (well_formed_cf_length Af1 W_t1); simpl; trivial].
simpl; rewrite Af1; destruct (eq_symbol_dec f1 f1) as [ _ | f1_diff_f1]; [idtac | absurd (f1 = f1); trivial].
rewrite <- app_nil_end; apply quick_permut_bis.
transitivity (flatten f1 (map (apply_cf_subst sigma') (Var (fresh_var pb) :: l1))).
apply list_permut_flatten.
apply list_permut.permut_map with (@eq term).
intros; subst; reflexivity.
apply quick_permut_bis; auto.
simpl; destruct (find eq_variable_dec (fresh_var pb) sigma') as [ [ | g ] | ].
intros; apply permut_refl.
destruct (eq_symbol_dec f1 g) as [_ | _].
intros; rewrite <- app_nil_end; apply permut_refl.
intros; apply permut_refl.
apply permut_refl.
intros v; generalize (H2 v); simpl partly_solved_part; simpl find;
destruct (eq_variable_dec v v1) as [v_eq_v1 | _]; [ subst v; rewrite F' | idtac ]; trivial.
intros v; generalize (H4 v); simpl existential_vars;
intros [[v_eq | In_v] | v_sigma_eq].
right; rewrite v_eq; simpl; destruct (eq_variable_dec v v) as [_ | v_diff_v];
[ idtac | absurd (v=v) ]; trivial.
left; trivial.
right; simpl; destruct (eq_variable_dec v (fresh_var pb)); intros; subst; trivial.
unfold ac_elementary_solve_term_term_term in *.
pattern pb';
refine
(prop_map_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb');
clear pb' In_pb'; intros [ | g2 ll2] In_t2; trivial;
destruct (eq_symbol_dec g1 g2) as [g1_eq_g2 | g1_diff_g2]; trivial.
generalize (in_remove _ eq_term_dec (Term g2 ll2) l2);
destruct (remove _ eq_term_dec (Term g2 ll2) l2) as [l2''' | ]; trivial;
intros [cp1' [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro l2'''_eq;
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma';
split; [split; [idtac | split] | idtac]; trivial.
rewrite U_pb; intros s t [st_eq | In_st].
injection st_eq; intros; subst.
replace (apply_cf_subst sigma' (Term f1 (Term g2 ll1 :: l1))) with
(Term f1 (quicksort (flatten f1 (apply_cf_subst sigma' (Term g2 ll1) :: nil) ++
flatten f1 (map (apply_cf_subst sigma') l1))));
[idtac | rewrite <- flatten_app; simpl; rewrite Af1; trivial].
apply (f_equal (fun l => Term f1 l)).
apply sort_is_unique;
[apply quick_sorted | apply well_formed_cf_sorted with f1; trivial | idtac].
apply quick_permut_bis.
rewrite (H1 _ _ (or_introl _ (refl_equal _))); rewrite <- flatten_app;
rewrite <- app_comm_cons; simpl (app (A:=term) nil); cbv beta.
apply add_a_subterm_subst; trivial.
apply H1; right; left; trivial.
apply H1; right; right; trivial.
destruct l1 as [ | u1 [ | u2 [ | u3 l1]]]; [contradiction | contradiction | idtac | contradiction].
destruct l2 as [ | v1 [ | v2 [ | v3 l2]]]; [contradiction | contradiction | idtac | contradiction].
inversion_clear In_pb' as [pb'_eq_ | In_pb''];
[idtac | inversion_clear In_pb'' as [pb''_eq_ | ]; [idtac | contradiction]];
subst; simpl unsolved_part.
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma';
split; [split; [idtac | split] | idtac]; trivial;
rewrite U_pb; intros s t [st_eq | In_st].
injection st_eq; intros; subst; simpl; rewrite Af1;
rewrite (H1 _ _ (or_introl _ (refl_equal _)));
rewrite (H1 _ _ (or_intror _ (or_introl _ (refl_equal _))));
apply (f_equal (fun l => Term f1 l));
assert (W_t2 := proj2 (W1 _ _ (or_introl _ (refl_equal _))));
simpl in W_t2; rewrite Af1 in W_t2;
apply sort_is_unique; [apply quick_sorted | intuition | apply quick_permut_bis; auto].
apply H1; right; right; trivial.
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma';
split; [split; [idtac | split] | idtac]; trivial;
rewrite U_pb; intros s t [st_eq | In_st].
injection st_eq; intros; subst; simpl; rewrite Af1;
rewrite (H1 _ _ (or_introl _ (refl_equal _)));
rewrite (H1 _ _ (or_intror _ (or_introl _ (refl_equal _))));
apply (f_equal (fun l => Term f1 l));
assert (W_t2 := proj2 (W1 _ _ (or_introl _ (refl_equal _))));
simpl in W_t2; rewrite Af1 in W_t2;
apply sort_is_unique; [apply quick_sorted | intuition | idtac].
apply quick_permut_bis.
apply (@list_permut.Pcons _ term (@eq term) v2 v2 (v1 :: nil) (v1 :: nil) nil); auto.
apply H1; right; right; trivial.
intros [sigma' [[H1 [H2 H3]] H4]]; exists sigma';
split; [split; [idtac | split] | idtac].
assert
(In_t1t2 : forall t1 t2 l1 l2 l, In (t1,t2) l ->
match
fold_left2
(fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l l1 l2
with
| Some new_list_of_equations =>
In (t1,t2) new_list_of_equations
| None => True
end).
clear l l1 l2 R W1 U_pb In_pb';
intros t1 t2; induction l1 as [ | a1 l1]; intros l2 l In_l; destruct l2; simpl; trivial;
apply IHl1; right; trivial.
rewrite U_pb; intros s t [st_eq | In_st].
injection st_eq; clear st_eq;
intros; subst; simpl; rewrite Af1; apply (f_equal (fun l => Term f1 l)).
assert (L12 : length l1 = length l2).
apply trans_eq with n1; [idtac | apply sym_eq];
generalize (W1 (Term f1 l1) (Term f1 l2) (or_introl _ (refl_equal _)));
intros [[_ W_t1] [_ W_t2]]; [rewrite Af1 in W_t1 | rewrite Af1 in W_t2]; trivial.
generalize l l2 In_pb' L12 H1; clear U_pb R W1 W2 W3 l l2 In_pb' L12 H1.
induction l1 as [ | t1 l1]; destruct l2 as [ | t2 l2].
intros [In_pb' | In_pb'] _; [idtac | contradiction]; trivial.
intros _ L12; simpl L12; discriminate.
intros _ L12; simpl L12; discriminate.
intros In_pb' L12 H1; simpl in L12; generalize (eq_add_S _ _ L12); clear L12; intro L12.
generalize (IHl1 _ _ In_pb' L12); clear IHl1; intro IHl1;
generalize (In_t1t2 _ _ l1 l2 ((t1,t2) :: l) (or_introl _ (refl_equal _))); clear In_t1t2;
intro In_t1t2.
simpl in In_pb';
destruct (fold_left2
(fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) ((t1,t2) :: l) l1 l2) as [new_list_of_equations | ];
[idtac | contradiction].
generalize In_pb'; clear In_pb'; intros [pb'_eq | In_pb']; [idtac | contradiction].
simpl; rewrite (IHl1 H1); injection pb'_eq; intros; subst; rewrite (H1 _ _ In_t1t2); trivial.
rewrite (H1 s t); trivial.
generalize (In_t1t2 _ _ l1 l2 _ In_st).
destruct (fold_left2
(fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l l1 l2);
[idtac | contradiction].
generalize In_pb'; clear In_pb'; intros [pb'_eq | In_pb']; [idtac | contradiction].
subst; simpl; trivial.
destruct (fold_left2
(fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l l1 l2);
[idtac | contradiction].
generalize In_pb'; clear In_pb'; intros [pb'_eq | In_pb']; [idtac | contradiction].
intro v; subst; apply H2; trivial.
destruct (fold_left2
(fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l l1 l2);
[idtac | contradiction].
generalize In_pb'; clear In_pb'; intros [pb'_eq | In_pb']; [idtac | contradiction].
intro v; subst; apply H3; trivial.
destruct (fold_left2
(fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l l1 l2);
[idtac | contradiction].
generalize In_pb'; clear In_pb'; intros [pb'_eq | In_pb']; [idtac | contradiction].
intro v; subst; apply H4; trivial.
Qed.
End Make.