proposition: Lemma wf_solve_is_complete : forall wpb sigma, is_wf_wf_sol wpb sigma -> match wpb with | W pb _ => match unsolved_part pb with | nil => True | _ :: _ => exists pb, In pb (wf_solve wpb) /\ is_wf_wf_sol pb sigma end end.
proof: Proof. destruct wpb; unfold is_wf_wf_sol; intros sigma Is_sol; generalize (solve_is_complete pb w sigma Is_sol); destruct (unsolved_part pb); trivial. unfold wf_solve. generalize (solve pb) (well_formed_solve pb w). induction l0; intros w0 H; simpl in H; elim H; clear H; intros pb' H; elim H; clear H. contradiction. intros In_pb' Is_sol'; elim In_pb'; clear In_pb'; intro In_pb'; simpl. exists (W a (w0 a (or_introl ((fix In (a0 : matching_problem) (l1 : list matching_problem) {struct l1} : Prop := match l1 with | nil => False | b :: m => b = a0 \/ In a0 m end) a l0) (eq_refl a)))); split; [ left | subst pb' ]; trivial. cut (exists pb' : matching_problem, In pb' l0 /\ is_well_formed_sol pb' sigma). intro H; elim (IHl0 (@tail_prop _ _ a l0 w0) H); clear H; intros pb0 H; elim H; clear H; intros In_pb0 Is_sol0; exists pb0; split; trivial; right; trivial. exists pb'; split; 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)