proposition: Lemma coalesce1_decreases : forall x y l sigma x_val, x <> y -> find X.eq_bool x sigma = Some x_val -> lt_pb (mk_pb ((x, Var y) :: map_subst (fun (_ : variable) (v_sigma : term) => apply_subst ((x, Var y) :: nil) v_sigma) sigma) ((Var y, apply_subst ((x, Var y) :: nil) x_val) :: map (fun uv : term * term => let (u, v) := uv in (apply_subst ((x, Var y) :: nil) u, apply_subst ((x, Var y) :: nil) v)) l)) (mk_pb sigma ((Var x, Var y) :: l)).
proof: Proof. intros x y l sigma x_val x_diff_y x_sigma; assert (Hx := find_map_subst x x (Var y) sigma); rewrite x_sigma in Hx. unfold lt_pb, measure_for_unif_pb; apply lex_lt. unfold phi1; apply VSet.subset_cardinal_not_eq_not_eq_set with x. apply VSet.subset_filter. assert (Hy : VSet.mem y (VSet.union (VSet.union (VSet.union (VSet.singleton x) (VSet.singleton y)) (set_of_variables_in_unsolved_part l)) (VSet.union (domain_of_subst sigma) (set_of_variables_in_range_of_subst sigma)))). do 2 apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. simpl; apply VSet.subset_subset_union. apply VSet.subset_subset_union. apply VSet.subset_subset_union. intros z [z_eq_y | z_in_nil]. unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst; apply Hy. contradiction. intros z z_in_x_val'; generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y; subst; apply Hy | intro z_diff_y]. do 2 apply VSet.union_2; apply solved_var_inc_occ_in_subst with x x_val; trivial; apply solved_var_inc_term with x y; trivial. intros z z_in_l'; generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y; subst; apply Hy | intro z_diff_y]. apply VSet.union_1; apply VSet.union_2; clear Hy. apply solved_var_inc_list with x y; trivial. apply VSet.subset_subset_union. intros z z_in_x_dom_sig; destruct (VSet.add_12 _ _ _ z_in_x_dom_sig) as [z_eq_x | z_in_dom_sig]. do 3 apply VSet.union_1; left; subst; trivial. apply VSet.union_2; apply VSet.union_1; rewrite domain_of_subst_map_subst in z_in_dom_sig; trivial. apply VSet.subset_subset_union. intros z [z_eq_y | z_in_nil]. unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst z; apply Hy. contradiction. intros z z_in_sigma'; generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y; subst; apply Hy | intro z_diff_y]. do 2 apply VSet.union_2; apply (solved_var_inc_subst _ _ _ _ z_diff_y z_in_sigma'). intros z; do 2 (rewrite Dummy_bool; rewrite not_solved_var); simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. intros _; rewrite x_sigma; left; do 2 apply VSet.union_1; left; reflexivity. assert (Hz := find_map_subst z x (Var y) sigma). case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma| intro z_sigma]; rewrite z_sigma in Hz; rewrite Hz; trivial. simpl; generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. intros _; left; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. intros [z_in_y_x_val'_l' | z_in_y_sigma']. destruct_set z_in_y_x_val'_l' z_in_y_x_val' z_in_l'. destruct_set z_in_y_x_val' z_in_y z_in_x_val'. left; apply VSet.union_1; apply VSet.union_2; trivial. right; apply solved_var_inc_occ_in_subst with x x_val; trivial. apply solved_var_inc_term with x y; trivial. left; apply VSet.union_2. apply solved_var_inc_list with x y; trivial. destruct_set z_in_y_sigma' z_in_y z_in_sigma'. left; apply VSet.union_1; apply VSet.union_2; trivial. right; apply solved_var_inc_subst with x y; trivial. intro H; generalize (VSet.filter_2 _ _ _ _ H); clear H; intros [_ H]. rewrite Dummy_bool in H; rewrite not_solved_var in H; simpl in H; revert H. generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _ | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. intros [H | H]. destruct_set H x_in_y_x_val' x_in_l'. destruct_set x_in_y_x_val' x_in_y x_in_x_val'. destruct x_in_y as [x_eq_y | x_in_nil]; [idtac | contradiction]. apply x_diff_y; subst; trivial. apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_x_val'). apply (solved_var_inc_not_mem_list _ _ _ x_diff_y x_in_l'). destruct_set H x_in_y x_in_sigma'. destruct x_in_y as [x_eq_y | x_in_nil]; [idtac | contradiction]. apply x_diff_y; subst; trivial. apply (solved_var_inc_not_mem_subst _ _ _ x_diff_y x_in_sigma'). apply VSet.filter_1. simpl unsolved_part; unfold set_of_variables_in_unsolved_part; do 3 apply VSet.union_1; left; reflexivity. rewrite Dummy_bool; rewrite not_solved_var; simpl; rewrite x_sigma. left; do 2 apply VSet.union_1; left; reflexivity. Defined.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)