proposition: Lemma new_var_occ_in_solved_part : forall pb, unsolved_part pb = nil -> well_sorted_partly_solved_part (partly_solved_part pb) -> (forall v p, find X.eq_bool v (partly_solved_part pb) = Some p -> occurs_in_pb (new_var p) pb) -> match partly_solved_part pb with | nil => True | (v,p) :: _ => match find X.eq_bool (new_var p) (solved_part pb) with | Some _ => True | None => False end end.
proof: Proof. intros [starting_vars usp sp [ | [v ps] psp]] U well_sorted new_var_occ. trivial. generalize (new_var_occ v ps); simpl. generalize (X.eq_bool_ok v v); case (X.eq_bool v v); [intros _ | intro v_diff_v; apply False_rect; apply v_diff_v; reflexivity]. intro new_var_ps_occ; generalize (new_var_ps_occ (eq_refl _)); clear new_var_ps_occ; unfold occurs_in_pb; simpl in U; subst usp; simpl; intros [F | new_var_ps_occ]; [contradiction | idtac]. generalize (some_nb_occ_Sn X.eq_bool (new_var ps) psp); destruct (find X.eq_bool (new_var ps) psp) as [new_var_ps_val | ]. intro F; generalize (F new_var_ps_val (eq_refl _)); clear F; intros F; simpl in well_sorted; destruct well_sorted as [_ [H _]]; assert (new_var_diff_new_var := H _ F); absurd (new_var ps = new_var ps); trivial. revert new_var_ps_occ; generalize (X.eq_bool_ok (new_var ps) v); case (X.eq_bool (new_var ps) v); [intro new_var_ps_eq_v | intro new_var_ps_diff_v]. absurd (v = new_var ps); [destruct well_sorted | apply sym_eq]; trivial. intuition. Qed.
imports: Coq(Arith List Wellfounded Wf_nat) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory ac matching dickson matching_well_formed matching_well_founded matching_sound matching_complete dickson)