# Library ac_matching.matching_well_founded

``` Add LoadPath "basis". 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. Module Type S. Declare Module Import Matching : matching.S. Import Cf_eq_ac. Import Ac. Import EqTh. Import T. Definition pb_weight pb :=   list_size     (fun t1_t2 : term * term =>        match t1_t2 with | (t1,t2) => ac_size t1 + ac_size t2 end)      (unsolved_part pb). Axiom well_founded_solve :   forall pb, well_formed_pb pb ->   forall pb', In pb' (solve pb) -> pb_weight pb' < pb_weight pb. End S. Module Make (Matching1 : matching.S) : S with Module Matching := Matching1. Module Import Matching := Matching1. Import Cf_eq_ac. Import Ac. Import EqTh. Import T. Import F. Import X. Import Sort. Import LPermut. Lemma ac_size_build_eq :   forall f l, arity f = AC ->   ac_size (build f l) = (length l - 1) + list_size ac_size l. Proof. intros f l Af; unfold build; simpl; destruct l as [ | t1 l]. rewrite quicksort_equation; simpl; rewrite Af; trivial. destruct l as [ | t2 l]. simpl; auto with arith. rewrite ac_size_unfold; rewrite Af; rewrite length_quicksort; apply (f_equal (fun n => length (t1 :: t2 :: l) -1 + n)); apply list_permut.permut_size with (@eq term). intros; subst; trivial. apply quick_permut_bis; auto. Qed. Lemma ac_size_build_lt_args :   forall f l1 l2 t1, arity f = AC -> well_formed_cf (Term f (l1 ++ t1 :: l2)) ->   ac_size (build f (l1 ++ l2)) + ac_size t1 < ac_size (Term f (l1 ++ t1 :: l2)). Proof. intros f l1 l2 t1 Ar W; pattern (ac_size (Term f (l1 ++ t1 :: l2))); rewrite ac_size_unfold. rewrite ac_size_build_eq; trivial. do 2 rewrite length_app; do 2 rewrite list_size_app; simpl; rewrite <- plus_assoc; apply plus_lt_le_compat. rewrite (plus_comm (length l1) (S (length l2))); simpl; rewrite <- minus_n_O; rewrite (plus_comm (length l2)); elim W; clear W; rewrite Ar; intros _ W; elim W; clear W; intros L _; rewrite length_app in L; simpl in L; rewrite plus_comm in L; simpl in L; rewrite plus_comm in L; destruct (length l1 + length l2). absurd (1 >= 2); trivial; unfold ge; auto with arith. auto with arith. rewrite <- plus_assoc; apply plus_le_compat_l; rewrite plus_comm; auto with arith. Qed. Lemma ac_size_build_lt :   forall f l1 l2 t1, arity f = AC -> well_formed_cf (Term f (l1 ++ t1 :: l2)) ->   ac_size (build f (l1 ++ l2)) < ac_size (Term f (l1 ++ t1 :: l2)). Proof. intros f l1 l2 t1 Ar W. apply lt_le_trans with (ac_size (build f (l1 ++ l2)) + ac_size t1). rewrite (plus_n_O (ac_size (build f (l1 ++ l2)))); rewrite <- plus_assoc; apply plus_lt_compat_l; simpl; unfold lt; apply ac_size_ge_one; elim (well_formed_cf_unfold _ W); intros Wl _; apply Wl; apply in_or_app; right; left; trivial. apply lt_le_weak; apply ac_size_build_lt_args; trivial. Qed. Definition pb_weight pb :=   list_size     (fun t1_t2 : term * term =>        match t1_t2 with | (t1,t2) => ac_size t1 + ac_size t2 end)      (unsolved_part pb). Theorem well_founded_solve :   forall pb, well_formed_pb pb ->   forall pb', In pb' (solve pb) -> pb_weight pb' < pb_weight pb. Proof. unfold pb_weight, solve, well_formed_pb;  intros pb [W1 [W2 [W3 _]]] pb' In_pb'; destruct (unsolved_part pb) as [ | [[v1 | f1 l1] t2] l]. contradiction. destruct (find eq_variable_dec v1 (solved_part pb)) as [t1 | ]. destruct (eq_term_dec t1 t2) as [t1_eq_t2 | _]; [idtac | contradiction]; inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst; simpl; auto with arith. generalize (W3 v1); destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [ p1 |]. 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 _; assert (In_l2 := in_remove _ eq_term_dec (closed_term p1) l2). destruct (remove _ eq_term_dec (closed_term p1) l2) as [ l2''' |]; [idtac | contradiction]. destruct In_l2 as [cp1 [l2' [l2'' [H [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro l2'''_eq; rewrite <- H in l2_eq; clear H; subst l2; inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]. subst; simpl unsolved_part; apply list_size_tl_compat; apply plus_le_lt_compat; auto with arith. apply ac_size_build_lt; [ rewrite Af2 | apply (proj2 (A:=well_formed_cf (Var v1))); apply W1; left] ; trivial. inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]. intros _; subst; simpl unsolved_part; simpl; auto with arith. destruct t2 as [ v2 | f2 l2 ]; [contradiction | idtac]; destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | _]; [subst f2| contradiction]. 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]. generalize (W2 v1); destruct (find eq_variable_dec v1 (solved_part pb)) as [s1 | ]. 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 l2'''_eq; rewrite <- H in l2_eq; clear H; subst l2'''; inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]. generalize (W1 (Term f1 (Var v1 :: l1)) (Term f1 l2) (or_introl _ (refl_equal _))); intros [Wt1 Wt2]; subst; unfold unsolved_part; apply list_size_tl_compat; apply plus_lt_compat; [replace (Var v1 :: l1) with (nil ++ Var v1 :: l1); trivial; replace (build f1 l1) with (build f1 (nil ++ l1)); trivial | idtac]; apply ac_size_build_lt; trivial. intros _; destruct s1 as [| g1 ll1]; [contradiction | idtac ]; destruct (eq_symbol_dec f1 g1) as [f1_eq_g1 | _]; [idtac | contradiction]. subst g1; assert (S_ll1 := well_formed_cf_sorted Af1 W_s1). assert (S_l2 := well_formed_cf_sorted Af1 W_t2). generalize (in_remove_list S_ll1 S_l2); destruct (remove_list ll1 l2) as [l2' | ]; [idtac | contradiction ]. unfold 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]. intro P; subst; simpl unsolved_part; apply list_size_tl_compat; apply plus_lt_le_compat. replace (Var v1 :: l1) with (nil ++ Var v1 :: l1); trivial; replace (build f1 l1) with (build f1 (nil ++ l1)); trivial; apply ac_size_build_lt; trivial. rewrite ac_size_build_eq; trivial; rewrite ac_size_unfold; rewrite Af1; apply plus_le_compat. generalize (list_permut.permut_length P); intro H; unfold EDS.A, DOS.A in *; rewrite <- H; rewrite length_app; destruct (length l2'); simpl; auto with arith; rewrite plus_comm; simpl; do 2 rewrite <- minus_n_O; auto with arith. assert (Dummy : forall a a' : term,   In a (ll1 ++ l2') -> In a' l2 -> a = a' -> ac_size a = ac_size a'). intros; subst; trivial. generalize (list_permut.permut_size ac_size ac_size Dummy P); intro H; unfold EDS.A, DOS.A in *; rewrite <- H; rewrite list_size_app; auto with arith. intros _; generalize (W3 v1); destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [p1 | ]. 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]. destruct 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; rewrite <- H in l2_eq; clear H; subst; simpl unsolved_part; rewrite Af1; intros. apply list_size_tl_compat; apply plus_le_lt_compat. destruct l1 as [ | s1 l1]; [simpl; auto with arith | idtac]. do 2 rewrite ac_size_unfold; rewrite Af1; rewrite length_quicksort; simpl; apply le_n_S; apply plus_le_compat_l. assert (H'' := @list_permut.permut_size _ term (@eq term) ac_size ac_size (quicksort (Var (new_var p1) :: s1 :: l1))   ((Var (new_var p1) :: s1 :: l1))). unfold EDS.A, DOS.A in *; rewrite H''. apply le_n. intros; subst; trivial. apply quick_permut_bis; reflexivity. apply ac_size_build_lt; 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; subst cp1 ll2'''; 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; subst l2'''; simpl unsolved_part; unfold list_size; rewrite plus_assoc; apply plus_lt_compat_r; replace (ac_size (Var (new_var p1))) with (ac_size (Var v1)); trivial; rewrite (plus_comm (ac_size (Var v1))); rewrite <- plus_assoc; rewrite (plus_assoc (ac_size (Var v1))); rewrite plus_comm; rewrite <- plus_assoc; apply plus_lt_compat. rewrite plus_comm; replace (build f1 l1) with (build f1 (nil ++ l1)); trivial; replace (Var v1 :: l1) with (nil ++ Var v1 :: l1); trivial; apply ac_size_build_lt_args; trivial. apply lt_trans with (ac_size (build f1 (l2' ++ l2'')) + ac_size (Term g2 ll2)). apply plus_lt_compat_l; subst; apply ac_size_build_lt. destruct (arity (head_symb p1)); [trivial | contradiction | contradiction]. apply (well_formed_cf_subterms W_t2); trivial. subst; apply ac_size_build_lt_args; 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; subst l2'''; assert (Common_ineq : list_size   (fun t1_t2 : term * term =>    let (t1, t3) := t1_t2 in ac_size t1 + ac_size t3)   (unsolved_part      (mk_pb (existential_vars pb) ((build f1 l1, build f1 (l2' ++ l2'')) :: l)         ((v1, t2) :: solved_part pb) (partly_solved_part pb))) < list_size   (fun t1_t2 : term * term =>    let (t1, t3) := t1_t2 in ac_size t1 + ac_size t3)   ((Term f1 (Var v1 :: l1), Term f1 l2) :: l)). simpl unsolved_part; apply list_size_tl_compat; apply plus_le_lt_compat. simpl; rewrite Af1; rewrite <- minus_n_O; rewrite (list_size_fold ac_size); rewrite ac_size_build_eq; trivial; apply plus_le_compat; auto with arith; apply le_minus. subst; apply ac_size_build_lt; trivial. unfold EDS.A, DOS.A in *; destruct (le_gt_dec (length l2) (length l1 + 1)) as [_ | _]; trivial; split; trivial; clear Common_ineq. simpl unsolved_part; apply list_size_tl_compat; apply plus_le_lt_compat. destruct l1 as [| t1' l1]; [simpl; auto with arith | idtac]; simpl; rewrite Af1; rewrite length_quicksort; simpl; do 2 rewrite (list_size_fold ac_size); simpl; assert (H' := @list_permut.permut_size _ term (@eq term) ac_size ac_size (Var (fresh_var pb) :: t1' :: l1) (quicksort (Var (fresh_var pb) :: t1' :: l1))). unfold EDS.A, DOS.A in *; rewrite <- H'. simpl; apply le_n. intros; subst; trivial. apply quick_permut. subst l2; apply ac_size_build_lt; 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; subst l2'''; simpl unsolved_part; unfold list_size; do 2 rewrite plus_assoc; apply plus_lt_compat_r. rewrite <- plus_assoc; rewrite (plus_comm (ac_size (Term g1 ll1))); rewrite <- plus_assoc; rewrite (plus_assoc (ac_size (Term g1 ll1))); rewrite plus_comm; rewrite <- plus_assoc; apply plus_lt_compat. rewrite plus_comm; replace (build f1 l1) with (build f1 (nil ++ l1)); trivial; replace (Term g1 ll1 :: l1) with (nil ++ Term g1 ll1 :: l1); trivial; apply ac_size_build_lt_args; trivial. subst l2 cp1; apply ac_size_build_lt_args; 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; simpl list_size; rewrite Af1; do 2 rewrite plus_assoc; apply plus_lt_compat_r; do 2 rewrite plus_0_r. do 2 rewrite plus_assoc; apply plus_lt_compat_r; simpl; unfold lt; apply le_n_S; do 3 rewrite <- plus_assoc; apply plus_le_compat_l; rewrite plus_comm; apply plus_le_compat_l; simpl; apply le_S; apply le_n. simpl; unfold lt; apply le_n_S; do 3 rewrite <- plus_assoc; apply plus_le_compat_l; rewrite plus_comm; rewrite <- plus_assoc; apply plus_le_compat_l; apply le_S; apply le_n. 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; clear W1 W2 W3 l l2 In_pb' L12. induction l1 as [ | t1 l1]; destruct l2 as [ | t2 l2]. intros [In_pb' | In_pb'] _; [idtac | contradiction]; subst pb'; simpl; rewrite Af1; rewrite <- plus_n_O; simpl; auto with arith. intros _ L12; simpl L12; discriminate. intros _ L12; simpl L12; discriminate. intros In_pb' L12; simpl in L12; generalize (eq_add_S _ _ L12); clear L12; intro L12. generalize (IHl1 _ _ In_pb' L12). intro H; apply lt_le_trans with (list_size   (fun t1_t2 : term * term =>    let (t1, t2) := t1_t2 in ac_size t1 + ac_size t2)   ((Term f1 l1, Term f1 l2) :: (t1, t2) :: l)); trivial. simpl; rewrite Af1; do 2 rewrite (list_size_fold ac_size); simpl; apply le_n_S. rewrite plus_assoc; apply plus_le_compat_r. rewrite plus_comm; do 2 rewrite <- plus_assoc; apply plus_le_compat_l. rewrite plus_comm; rewrite <- plus_assoc; apply plus_le_compat_l. simpl; rewrite plus_comm; trivial. Qed. End Make. ```