proposition: Lemma matching_step2_is_complete : forall t1 t2 Wt1 Wt2 sigma, well_formed_cf_subst sigma -> apply_cf_subst sigma t1 = t2 -> (exists wpb, In wpb (wf_solve_loop ((W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2)) :: nil)) /\ match wpb with | W pb _ => forall v, occurs_in_term v t1 -> apply_cf_subst sigma (Var v) = apply_cf_subst (extract_solution (solved_part pb) (partly_solved_part pb)) (Var v) end).
proof: Proof. intros t1 t2 Wt1 Wt2 sigma Wsigma Is_sol; elim (matching_step1_is_complete t1 t2 Wt1 Wt2 sigma Wsigma Is_sol). clear Is_sol; intros [pb w_pb] [Is_sol pb_in_loop]. destruct Is_sol as [sigma' [[Is_sol'_usp [Is_sol'_psp Is_sol'_sp]] [sigma_eq_sigma' Wsigma']]]. exists (W pb w_pb); split; [trivial | idtac]. intros v O. assert (H : let lpb:= (W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2) :: nil) in forall wpb, In wpb lpb -> match wpb with | W pb' _ => ~ In v (existential_vars pb') /\ occurs_in_pb v pb' end). intros lpb wpb In_wpb'; elim In_wpb'; clear In_wpb'; intro In_wpb'. subst wpb; split; simpl. unfold not; trivial. unfold init_pb; left; simpl; left; trivial. contradiction. elim (variable_preservation v _ H (W pb w_pb) pb_in_loop); clear H; intros E' O'. assert (usp_eq_nil := wf_solve_loop_end _ _ pb_in_loop); destruct pb as [ex usp sp psp]; simpl unsolved_part in *; subst usp. clear Is_sol'_usp; clear pb_in_loop; elim w_pb; intros _ w; elim w; clear w. intros _ w; elim w; clear w. intros _ w; elim w; clear w. intros nb_occ_v w; elim w; clear w. intros well_sorted new_var_occ. simpl partly_solved_part in *; simpl solved_part in *; simpl existential_vars in *. elim (sigma_eq_sigma' v); intro E_v. absurd (In v ex); trivial. rewrite E_v; clear sigma Wsigma sigma_eq_sigma' E_v O. elim O'; clear O'; intro O'. contradiction. elim O'; clear O'; intro O'; simpl in O'. generalize sp Is_sol'_psp Is_sol'_sp nb_occ_v well_sorted new_var_occ O' (extract_solution_in_partly_solved_part sp psp ex nb_occ_v well_sorted new_var_occ); clear sp w_pb Is_sol'_psp Is_sol'_sp nb_occ_v well_sorted new_var_occ O' E'; induction psp. contradiction. intros sp Is_sol'_psp Is_sol'_sp nb_occ_v well_sorted new_var_occ; destruct a; generalize (Is_sol'_psp v); simpl find. generalize (X.eq_bool_ok v a); case (X.eq_bool v a); [intros v_eq_a H _; subst a | intro v_diff_a]. rewrite H; rewrite extract_solution_unfold; rewrite (extract_solution_in_solved_part ((v, (Term (head_symb p) (quicksort (flatten (head_symb p) (apply_cf_subst sp (Var (new_var p)) :: closed_term p :: nil))))) :: sp) psp v (Term (head_symb p) (quicksort (flatten (head_symb p) (apply_cf_subst sp (Var (new_var p)) :: closed_term p :: nil))))). intros _; 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 ((v,p) :: psp)) (eq_refl _) well_sorted new_var_occ) (Is_sol'_sp (new_var p)); simpl. destruct (find X.eq_bool (new_var p) sp); trivial; contradiction. generalize (nb_occ_v v); 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]. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. simpl find; generalize (X.eq_bool_ok v v); case (X.eq_bool v v); [intros _; trivial | intro v_diff_v; apply False_rect; apply v_diff_v; reflexivity]. intros; rewrite extract_solution_unfold. apply IHpsp; trivial. intros; generalize (Is_sol'_psp v0) (nb_occ_v v0); simpl nb_occ; simpl find. generalize (X.eq_bool_ok v0 a); case (X.eq_bool v0 a); [intro v0_eq_a; subst v0 | intro v0_diff_a]. generalize (some_nb_occ_Sn X.eq_bool a psp); destruct (find X.eq_bool a psp); trivial. intro H1; generalize (H1 p0 (eq_refl _)); clear H1; intro H1; destruct (nb_occ X.eq_bool a psp). absurd (1 <= 0); auto with arith. intros _ H2; rewrite Nat.add_comm in H2; simpl in H2; absurd (S(S(n + nb_occ X.eq_bool a sp)) <= 1); auto with arith. trivial. intro v1; generalize (Is_sol'_psp v1); pattern (apply_cf_subst sp (Var (new_var p)) :: closed_term p :: nil); unfold find. generalize (X.eq_bool_ok v1 a); case (X.eq_bool v1 a); [intro v1_eq_a; subst v1 | intro v1_diff_a]. intro H1; rewrite H1; 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 ((a, p) :: psp)) (eq_refl _) well_sorted new_var_occ); intro H4; simpl in H4. generalize (Is_sol'_sp (new_var p)). simpl; destruct (find X.eq_bool (new_var p) sp); trivial; contradiction. intros _; apply Is_sol'_sp. intro v1; generalize (nb_occ_v v1); simpl. generalize (X.eq_bool_ok v1 a); case (X.eq_bool v1 a); [intro v1_eq_a; subst v1 | intro v1_diff_a; trivial]. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. elim well_sorted; intros _ H1; elim H1; trivial. intros v1; generalize (nb_occ_v v1) (new_var_occ v1); simpl find; intro H'; simpl in H'; generalize H'; clear H'. generalize (X.eq_bool_ok v1 a); case (X.eq_bool v1 a); [intro v1_eq_a; subst v1 | intro v1_diff_a]. intros H'; generalize (some_nb_occ_Sn X.eq_bool a psp). destruct (find X.eq_bool a psp). intro H1; generalize (H1 p0 (eq_refl _)); clear H1; intro H1. destruct (nb_occ X.eq_bool a psp). absurd (1 <= 0); auto with arith. rewrite Nat.add_comm in H'; simpl in H'; absurd (S(S(n + nb_occ X.eq_bool a sp)) <= 1); auto with arith. intros; discriminate. intros H' H1 p0 H2; elim (H1 p0 H2); clear H1; intro H1. contradiction. revert H1; simpl. generalize (X.eq_bool_ok (new_var p0) a); case (X.eq_bool (new_var p0) a); [intro new_var_p0_eq_a | intro new_var_p0_diff_a]. intros _; right; right; simpl. generalize (X.eq_bool_ok (new_var p0) a); case (X.eq_bool (new_var p0) a); [intros _; trivial | intro new_var_p0_diff_a]. absurd (new_var p0 = a); assumption. case_eq (find X.eq_bool (new_var p0) psp). intros p1 F _; right; left; simpl; rewrite F; trivial. intros F; case_eq (find X.eq_bool (new_var p0) sp). intros t F' _; right; right; simpl. generalize (X.eq_bool_ok (new_var p0) a); case (X.eq_bool (new_var p0) a); [intros new_var_p0_eq_a | intros _]. exact I. rewrite F'; exact I. intros F' [Abs | Abs]; contradiction. intros v1 p1 F1. refine (extract_solution_in_partly_solved_part _ _ ex _ _ _ _ _ F1). intros v2; generalize (nb_occ_v v2); simpl. generalize (X.eq_bool_ok v2 a); case (X.eq_bool v2 a); [intro v2_eq_a; subst v2 | intro v2_diff_a; trivial]. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. elim well_sorted; intros _ H2; elim H2; trivial. intros v2; generalize (nb_occ_v v2) (new_var_occ v2); simpl find; intro H'; simpl in H'; generalize H'; clear H'. generalize (X.eq_bool_ok v2 a); case (X.eq_bool v2 a); [intro v2_eq_a; subst v2 | intro v2_diff_a]. intros H'; generalize (some_nb_occ_Sn X.eq_bool a psp). destruct (find X.eq_bool a psp). intro H1; generalize (H1 p0 (eq_refl _)); clear H1; intro H1. destruct (nb_occ X.eq_bool a psp). absurd (1 <= 0); auto with arith. rewrite Nat.add_comm in H'; simpl in H'; absurd (S(S(n + nb_occ X.eq_bool a sp)) <= 1); auto with arith. intros; discriminate. intros H' H1 p0 H2; elim (H1 p0 H2); clear H1; intro H1. contradiction. elim H1; clear H1; simpl find. generalize (X.eq_bool_ok (new_var p0) a); case (X.eq_bool (new_var p0) a); [intro new_var_p0_eq_a | intro new_var_p0_diff_a]. right; right; simpl. generalize (X.eq_bool_ok (new_var p0) a); case (X.eq_bool (new_var p0) a); [intros _; trivial | intro new_var_p0_diff_a]. absurd (new_var p0 = a); assumption. right; left; simpl; trivial. right; right; simpl; case (X.eq_bool (new_var p0) a); trivial. generalize (Is_sol'_sp v) (extract_solution_in_solved_part sp psp v); destruct (find X.eq_bool v sp). intros H0 H; generalize (H t (nb_occ_v v) (eq_refl _)); clear H; intro H; rewrite H; rewrite H0; trivial. contradiction. 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)