# 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. ```