proposition: Lemma coalesce2_decreases : forall x y l sigma, x <> y -> find X.eq_bool x sigma = None -> lt_pb (mk_pb ((x, Var y) :: map_subst (fun (_ : variable) (v_sigma : term) => apply_subst ((x, Var y) :: nil) v_sigma) sigma) (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_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. simpl unsolved_part; simpl solved_part; simpl set_of_variables_in_unsolved_part; simpl domain_of_subst; apply VSet.subset_filter. apply VSet.subset_subset_union. intros z z_in_l'; generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. do 2 apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. apply VSet.union_1; apply VSet.union_2; apply solved_var_inc_list with x y; trivial. apply VSet.subset_subset_union. rewrite domain_of_subst_map_subst. 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; trivial. intros z z_in_y_sigma'; destruct_set z_in_y_sigma' z_in_y z_in_sigma'. do 2 apply VSet.union_1; apply VSet.union_2; trivial. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. do 2 apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. do 2 apply VSet.union_2; apply (solved_var_inc_subst _ _ _ _ z_diff_y z_in_sigma'). intros z; do 2 rewrite Dummy_bool; do 2 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]. rewrite x_sigma; trivial. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intro z_sigma; trivial]. assert (Hz := find_map_subst z x (Var y) sigma); rewrite z_sigma in Hz; rewrite Hz. intros [z_in_l' | z_in_y_sigma']. left; generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. 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. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. left; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. right; apply solved_var_inc_subst with x y; trivial. intro H; destruct (VSet.filter_2 _ _ _ _ H) as [_ H1]; clear H. rewrite Dummy_bool in H1; rewrite not_solved_var in H1; simpl in H1; revert H1. 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 [x_in_l' | x_in_y_sigma']. revert x_in_l'; apply solved_var_inc_not_mem_list; trivial. destruct_set x_in_y_sigma' x_in_y x_in_sigma'. apply x_diff_y; destruct x_in_y as [x_eq_y | x_in_nil]; [subst; trivial | contradiction]. apply solved_var_inc_not_mem_subst with x y sigma; trivial. apply VSet.filter_1. simpl 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; trivial. 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)