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.