proposition: Lemma matching_step2_is_sound : forall t1 t2 Wt1 Wt2 wpb, match wpb with | W pb _ => In wpb (wf_solve_loop ((W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2)) :: nil)) -> let sigma := extract_solution (solved_part pb) (partly_solved_part pb) in apply_cf_subst sigma t1 = t2 end.
proof: Proof. intros t1 t2 Wt1 Wt2 [pb w_pb]; intros pb_in_loop; refine (matching_step1_is_sound t1 t2 Wt1 Wt2 _ _ _ pb_in_loop). simpl; unfold is_sol; exists (extract_solution (solved_part pb) (partly_solved_part pb)); split; [idtac | intro; right; trivial]. assert (usp_eq_nil := wf_solve_loop_end _ _ pb_in_loop); destruct pb as [ex usp sp psp]; simpl unsolved_part in usp_eq_nil; subst usp. unfold is_rough_sol; split; [idtac | split]. contradiction. elim w_pb; intros _ [ _ [ _ [nb_occ_v [well_sorted new_var_occ]]]]. simpl partly_solved_part in *; simpl solved_part in *. intro v; generalize (extract_solution_in_partly_solved_part sp psp ex nb_occ_v well_sorted new_var_occ v). destruct (find X.eq_bool v psp) as [v_pval | ]; [idtac | trivial]. intro H; apply H; trivial. elim w_pb; intros _ [ _ [ _ [nb_occ_v _]]]. simpl partly_solved_part in *; simpl solved_part in *. intro v; generalize (extract_solution_in_solved_part sp psp v); destruct (find X.eq_bool v sp) as [v_val | ]; [idtac | trivial]. intro H; rewrite (H v_val); 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)