proposition: Lemma extract_solution_in_partly_solved_part : forall solved_part partly_solved_part ex, (forall v, nb_occ X.eq_bool v solved_part + nb_occ X.eq_bool v partly_solved_part <= 1) -> well_sorted_partly_solved_part partly_solved_part -> (forall v p, find X.eq_bool v partly_solved_part = Some p -> occurs_in_pb (new_var p) (mk_pb ex nil solved_part partly_solved_part)) -> forall v p, find X.eq_bool v partly_solved_part = Some p -> apply_cf_subst (extract_solution solved_part partly_solved_part) (Var v) = Term (head_symb p) (quicksort (flatten (head_symb p) ((apply_cf_subst (extract_solution solved_part partly_solved_part) (Var (new_var p))) :: (closed_term p) :: nil))).
proof: Proof. intros sp psp; generalize sp; clear sp; induction psp as [ | [x s] psp]; intros sp ex only_one_occ well_sorted new_var_occ y p y_psp. discriminate. simpl in y_psp; rewrite extract_solution_unfold. revert y_psp; generalize (X.eq_bool_ok y x); case (X.eq_bool y x); [intros y_eq_x y_psp | intros y_diff_x y_psp]. injection y_psp; intros; subst. assert (H := (extract_solution_in_solved_part ((x, (Term (head_symb p) (quicksort (flatten (head_symb p) (apply_cf_subst sp (Var (new_var p)) :: closed_term p :: nil))))) :: sp) psp x (Term (head_symb p) (quicksort (flatten (head_symb p) (apply_cf_subst sp (Var (new_var p)) :: closed_term p :: nil)))))). refine (trans_eq (H _ _) _); clear H y_psp. generalize (only_one_occ x); simpl; 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]. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; subst; trivial. simpl; 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]. reflexivity. apply (f_equal (fun t => Term (head_symb p) (quicksort (flatten (head_symb p) (t :: closed_term p :: nil))))). generalize (new_var_occ_in_solved_part (mk_pb ex nil sp ((x,p) :: psp)) (eq_refl _) well_sorted new_var_occ). simpl partly_solved_part; simpl solved_part. replace (apply_cf_subst sp (Var (new_var p))) with (match find eq_var_bool (new_var p) sp with | Some new_var_p_val => new_var_p_val | None => Var (new_var p) end) by reflexivity. case_eq (find X.eq_bool (new_var p) sp); [intros new_var_p_val F _ | intros F]; [idtac | contradiction]. assert (H:= (extract_solution_in_solved_part ((x, (Term (head_symb p) (quicksort (flatten (head_symb p) (apply_cf_subst sp (Var (new_var p)) :: closed_term p :: nil))))) :: sp) psp (new_var p) new_var_p_val)). rewrite <- H at 1. simpl apply_cf_subst at 2; rewrite F; reflexivity. generalize (only_one_occ (new_var p)); simpl; generalize (X.eq_bool_ok (new_var p) x); case (X.eq_bool (new_var p) x); [intro new_var_p_eq_x | intro new_var_p_diff_x]. destruct well_sorted as [x_diff_new_var_p _]; absurd (x = new_var p); trivial; apply sym_eq; trivial. trivial. simpl; generalize (X.eq_bool_ok (new_var p) x); case (X.eq_bool (new_var p) x); [intro new_var_p_eq_x | intro new_var_p_diff_x]. destruct well_sorted as [x_diff_new_var_p _]; absurd (x = new_var p); trivial; apply sym_eq; trivial. trivial. refine (IHpsp _ ex _ _ _ y p y_psp). intros z; generalize (only_one_occ z); simpl; generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x | intro z_diff_x]; trivial. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. inversion well_sorted; intuition. intros z z_val z_psp; generalize (new_var_occ z) (only_one_occ z) (some_nb_occ_Sn X.eq_bool z psp z_psp); simpl find; simpl nb_occ; generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x | intro z_diff_x]. intros _; subst z; destruct (nb_occ X.eq_bool x psp) as [ | n]. intros; absurd (1 <= 0); auto with arith. rewrite Nat.add_comm; simpl plus; intros; absurd (S (S (n + nb_occ X.eq_bool x sp)) <= 1); auto with arith. intros H _ _; generalize (H z_val z_psp). unfold occurs_in_pb; simpl; intros [occ_in_usp | [occ_in_psp | occ_in_sp]]. contradiction. right; revert occ_in_psp. case (X.eq_bool (new_var z_val) x); [right | left]; trivial. case (X.eq_bool (new_var z_val) x); right; right; trivial. 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)