proposition: Lemma matching_is_sound : forall t1 t2 Wt1 Wt2 sigma, In sigma (matching t1 t2 Wt1 Wt2) -> apply_cf_subst sigma t1 = t2.
proof: Proof. intros t1 t2 Wt1 Wt2 sigma; unfold matching. intro In_wpb. cut (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 _ => sigma = clean_sol (existential_vars pb) (extract_solution (solved_part pb) (partly_solved_part pb)) end). clear In_wpb; intro In_wpb; elim In_wpb; clear In_wpb; intros wpb In_wpb; elim In_wpb; clear In_wpb; intros In_wpb Is_sol; generalize (matching_step2_is_sound t1 t2 Wt1 Wt2 wpb); destruct wpb; intro H; generalize (H In_wpb); clear H; intro H; rewrite Is_sol; rewrite <- H; clear Is_sol H; generalize (extract_solution (solved_part pb) (partly_solved_part pb)); cut (forall v, occurs_in_term v t1 -> ~ In v (existential_vars pb)). generalize (existential_vars pb); clear sigma pb w In_wpb; intros l; pattern t1; apply term_rec3. intros v not_occurs sigma; generalize v not_occurs; clear v not_occurs; induction sigma. unfold clean_sol; simpl; trivial. intros v not_occurs; destruct a; simpl. generalize (X.eq_bool_ok v a); case (X.eq_bool v a); [intro v_eq_a | intro v_diff_a]. subst v; assert (a_not_in_l := not_occurs a (eq_refl _)). generalize (mem_bool_ok _ _ X.eq_bool_ok a l); case (mem_bool X.eq_bool a l). intro a_mem_l; absurd (In a l); trivial. apply (mem_impl_in (@eq variable)); trivial. intros _; simpl; generalize (X.eq_bool_ok a a); case (X.eq_bool a a); [intros _; trivial | intro a_diff_a; apply False_rect; apply a_diff_a; reflexivity]. generalize (mem_bool_ok _ _ X.eq_bool_ok a l); case (mem_bool X.eq_bool a l). intro a_mem_l; simpl in IHsigma; apply IHsigma; trivial. intro a_not_mem_l; simpl; generalize (X.eq_bool_ok v a); case (X.eq_bool v a); [intro v_eq_a | intros _]. absurd (v=a); trivial. simpl in IHsigma; apply IHsigma; trivial. intros f l0 IH not_occurs sigma; cut (map (apply_cf_subst (clean_sol l sigma)) l0 = map (apply_cf_subst sigma) l0). intro H; simpl; rewrite H; trivial. induction l0. trivial. simpl map; rewrite (IH a). rewrite (IHl0); trivial. intros; apply IH; trivial; right; trivial. intros; apply not_occurs; right; trivial. left; trivial. intros; apply not_occurs; trivial; left; 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); trivial. intros lpb wpb In_wpb'; elim In_wpb'; clear In_wpb'; intro In_wpb'. subst wpb; unfold init_pb; simpl; split. unfold not; trivial. left; left; trivial. contradiction. generalize (wf_solve_loop (W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2) :: nil)) In_wpb; clear In_wpb; induction l; [contradiction | simpl map; intro In_wpb; elim In_wpb; clear In_wpb; intro In_wpb; [destruct a; exists (W pb w); split; trivial; [ left | apply sym_eq ]; trivial |elim (IHl In_wpb); clear In_wpb; intros wpb H; elim H; clear H; intros In_wpb H; exists wpb; split; trivial; 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)