proposition: Lemma matching_is_complete : forall t1 t2 Wt1 Wt2 sigma, well_formed_cf_subst sigma -> apply_cf_subst sigma t1 = t2 -> (exists sigma', In sigma' (matching t1 t2 Wt1 Wt2) /\ (forall v, occurs_in_term v t1 -> apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v))).
proof: Proof. intros t1 t2 Wt1 Wt2 sigma W_sigma Is_sol; elim (matching_step2_is_complete t1 t2 Wt1 Wt2 sigma W_sigma Is_sol). intros wpb H; elim H; clear H; intros In_wpb Is_sol'; destruct wpb. unfold matching. exists (clean_sol (existential_vars pb) (extract_solution (solved_part pb) (partly_solved_part pb))); split. generalize In_wpb; clear In_wpb; induction (wf_solve_loop (W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2) :: nil)). contradiction. intro In_wpb; elim In_wpb; clear In_wpb; intro In_wpb. subst a; left; trivial. right; apply IHl; trivial. intros v O; cut (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). intro H; elim (variable_preservation v _ H (W pb w) In_wpb); clear H; intros E' O'. rewrite Is_sol'; trivial. generalize (extract_solution (solved_part pb) (partly_solved_part pb)). clear t1 t2 Wt1 Wt2 sigma W_sigma Is_sol w In_wpb Is_sol' O O'; intro sigma; induction sigma. simpl; trivial. destruct a; simpl. generalize (mem_bool_ok _ _ X.eq_bool_ok a (existential_vars pb)); case (mem_bool X.eq_bool a (existential_vars pb)). intro a_mem_ex; generalize (X.eq_bool_ok v a); case (X.eq_bool v a); [intro v_eq_a; subst a | intro v_diff_a]. absurd (In v (existential_vars pb)); trivial. apply mem_impl_in with (@eq _). intros; assumption. assumption. simpl in IHsigma; rewrite IHsigma; trivial. intro a_not_mem_ex; simpl; generalize (X.eq_bool_ok v a); case (X.eq_bool v a); [intro v_eq_a; subst a; trivial | intro v_diff_a]. simpl in IHsigma; rewrite IHsigma; trivial. 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. 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)