proposition: Lemma variable_preservation : forall v lpb, (forall wpb, In wpb lpb -> match wpb with | W pb _ => (~ In v (existential_vars pb)) /\ (occurs_in_pb v pb) end) -> (forall wpb', In wpb' (wf_solve_loop lpb) -> match wpb' with | W pb' _ => (~ In v (existential_vars pb')) /\ (occurs_in_pb v pb') end).
proof: Proof. intros x lpb; refine (well_founded_ind well_founded_o_lpb (fun lpb => (forall wpb : well_formed_matching_problem, In wpb lpb -> match wpb with | W pb _ => ~ In x (existential_vars pb) /\ occurs_in_pb x pb end) -> forall wpb' : well_formed_matching_problem, In wpb' (wf_solve_loop lpb) -> match wpb' with | W pb' _ => ~ In x (existential_vars pb') /\ occurs_in_pb x pb' end) _ _). clear lpb; intros lpb IH P_lpb wpb; destruct lpb as [ | [pb w_pb] lpb]. rewrite wf_solve_nil; contradiction. rewrite wf_solve_cons; destruct pb as [ex [ | [s t] usp] sp psp]; simpl unsolved_part; cbv iota. intros [wpb_eq_w_pb | wpb_in_loop_lpb]. subst wpb; apply (P_lpb (W (mk_pb ex nil sp psp) w_pb)); trivial; left; trivial. refine (IH lpb (F_wf_solve_dec1 _ _) _ wpb wpb_in_loop_lpb); intros; apply P_lpb; right; trivial. intro wpb_in_loop; refine (IH (wf_solve (W (mk_pb ex ((s, t) :: usp) sp psp) w_pb) ++ lpb) (F_wf_solve_dec2 _ _) _ wpb wpb_in_loop). clear wpb wpb_in_loop; intros wpb wpb_in_loop. destruct (in_app_or _ _ _ wpb_in_loop) as [wpb_in_solve_pb | wpb_in_loop_lpb]; clear wpb_in_loop; [ idtac | apply P_lpb; right; trivial]. generalize (P_lpb _ (or_introl _ (eq_refl _))); simpl existential_vars; intros [NE O]. destruct wpb as [pb' w_pb']; generalize (wf_projection _ _ _ _ wpb_in_solve_pb). clear lpb IH P_lpb; unfold solve; simpl unsolved_part; simpl solved_part; cbv iota beta. destruct s as [ v | f1 l1]. case_eq (find X.eq_bool v sp); [intros v_val v_sp| intro v_sp]. generalize (T.eq_bool_ok v_val t); case (T.eq_bool v_val t); [intro v_val_eq_t | intros; contradiction]. simpl existential_vars; simpl partly_solved_part; intros [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | contradiction]. split; [trivial | idtac]. destruct O as [ O | O ]; [idtac | right; trivial]. simpl unsolved_part in O; elim O; clear O; intro O. simpl in O; subst v; right; right; simpl; rewrite v_sp; trivial. left; trivial. simpl partly_solved_part; case_eq (find X.eq_bool v psp); [intros v_pval v_psp | intro v_psp]. destruct t as [ | f2 l2]; [intro; contradiction | idtac]. generalize (F.Symb.eq_bool_ok (head_symb v_pval) f2); case (F.Symb.eq_bool (head_symb v_pval) f2); [intro top_v_pval_eq_f2 | intros; contradiction]. destruct (remove T.eq_bool (closed_term v_pval) l2); [idtac | intros; contradiction]. intros [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | contradiction]. simpl existential_vars; split; [trivial | idtac]. destruct O as [ O | [ O | O ]]. simpl unsolved_part in O; elim O; clear O; intro O. simpl in O; subst v; right; left; simpl; rewrite v_psp; trivial. left; right; trivial. right; trivial. left; trivial. right; right; trivial. intros [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | intros; contradiction]. simpl existential_vars; split; [trivial | idtac]. destruct O as [ [O | O] | [ O | O ]]. simpl in O; subst v; right; right; simpl; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; exact I | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. left; trivial. right; left; trivial. right; right; simpl; case (X.eq_bool x v); trivial. destruct t as [ | f2 l2]; [intros; contradiction | idtac]. generalize (F.Symb.eq_bool_ok f1 f2); case (F.Symb.eq_bool f1 f2); [intro f1_eq_f2 | intros; contradiction]. subst f2; case_eq (arity f1); [ intro Af1| intro Af1 | intros n Af1]. destruct (le_gt_dec (length l1) (length l2)) as [L | L]; [idtac | intros; contradiction]. simpl; destruct l1 as [ | [v1 | g1 ll1] l1]. intros [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | intros; contradiction]. split. trivial. destruct O as [ [O | O] | O]; [contradiction | left; trivial | right; trivial]. simpl solved_part; case_eq (find X.eq_bool v1 sp); [intros v1_val v1_sp | intro v1_sp]. unfold ac_elementary_solve_term_var_with_val_term; simpl. destruct (remove T.eq_bool v1_val l2) as [l2' | ]. intros [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | intros; contradiction]. split; [trivial | idtac]. destruct O as [ [[O | O] | O] | O]; [idtac | idtac | idtac | right; trivial]. simpl in O. subst x; right; right; simpl; rewrite v1_sp; trivial. left; left; destruct l1 as [ | s1 [ | t1 l1]]; [contradiction | intuition | simpl]. apply list_permut_occurs_in_term_list with (s1 :: t1 :: l1); trivial; apply quick_permut. left; right; trivial. destruct v1_val as [ | g ll]; [intros; contradiction | idtac]. generalize (F.Symb.eq_bool_ok f1 g); case (F.Symb.eq_bool f1 g); [intros f1_eq_g; subst g | intros f1_diff_g; contradiction]. destruct (remove_list ll l2) as [l2' | ]; [idtac | intros; contradiction]. unfold EDS.A, DOS.A in *; destruct (le_gt_dec (length l1) (length l2')) as [L' | L']; [idtac | intros; contradiction]. intros [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | intros; contradiction]. split; [trivial | idtac]. destruct O as [ [[O | O] | O] | O]; [idtac | idtac | idtac | right; trivial]. simpl in O. subst x; right; right; simpl; rewrite v1_sp; trivial. left; left; destruct l1 as [ | s1 [ | t1 l1]]; [contradiction | intuition | simpl]. apply list_permut_occurs_in_term_list with (s1 :: t1 :: l1); trivial; apply quick_permut. left; right; trivial. case_eq (find X.eq_bool v1 psp); [intros v1_pval v1_psp| intro v1_psp]. unfold ac_elementary_solve_term_var_with_part_val_term. generalize (F.Symb.eq_bool_ok f1 (head_symb v1_pval)); case (F.Symb.eq_bool f1 (head_symb v1_pval)); [intro f1_eq_top_v1_pval | intro f1_diff_top_v1_pval]. destruct (remove T.eq_bool (closed_term v1_pval) l2) as [l2' | ]; [idtac | intros; contradiction]. intros [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | intros; contradiction]. split; [trivial | idtac]. destruct O as [ [ [ O | O] | O] | O ]; [idtac | idtac | idtac | right; trivial]. simpl in O. subst x; right; left; simpl; rewrite v1_psp; trivial. left; left; destruct l1 as [ | t1 l1]; [contradiction | idtac]. simpl; apply list_permut_occurs_in_term_list with ((Var (new_var v1_pval)) :: t1 :: l1); [ apply quick_permut | right; trivial ]. left; right; trivial. intro pb'_in_lpb; pattern pb'; refine (prop_map_without_repetition _ T.eq_bool_ok _ _ _ _ _ pb'_in_lpb); clear pb' w_pb' pb'_in_lpb wpb_in_solve_pb; intros t2 t2_in_l2; destruct t2 as [ | g2 ll2 ]; [trivial | idtac]. generalize (F.Symb.eq_bool_ok g2 (head_symb v1_pval)); case (F.Symb.eq_bool g2 (head_symb v1_pval)); [intros g2_eq_top_v1_pval | intros; trivial]. destruct (remove T.eq_bool (closed_term v1_pval) ll2) as [ll2' | ]; [idtac | trivial]. destruct (remove T.eq_bool (Term g2 ll2) l2) as [l2' | ]; [idtac | trivial]. split; [trivial | idtac]. destruct O as [ [[O | O] | O] | O]; [idtac | idtac | idtac | right; trivial]. simpl in O. subst x; right; left; simpl; rewrite v1_psp; trivial. left; right; left; destruct l1 as [ | s1 [ | t1 l1]]; [contradiction | intuition | idtac]. simpl; apply list_permut_occurs_in_term_list with (s1 :: t1 :: l1); trivial; apply quick_permut. left; right; right; trivial. unfold ac_elementary_solve_term_var_without_val_term; simpl. intro pb'_in_lpb; pattern pb'; refine (prop_map12_without_repetition _ T.eq_bool_ok _ _ _ _ _ pb'_in_lpb); clear pb' w_pb' pb'_in_lpb wpb_in_solve_pb; intros t2 t2_in_l2. destruct (remove T.eq_bool t2 l2) as [l2' | ]; [idtac | trivial]. unfold EDS.A, DOS.A in *; destruct (le_gt_dec (length l2) (length l1 + 1)) as [L' | L']. split; [trivial | idtac]. destruct O as [ [[O | O] | O] | [ O | O]]. right; right; simpl in O; subst x; simpl; generalize (X.eq_bool_ok v1 v1); case (X.eq_bool v1 v1); [intros _; trivial | intro v1_diff_v1; apply False_rect; apply v1_diff_v1; reflexivity]. left; left; destruct l1 as [ | s1 [ | t1 l1]]; [contradiction | intuition | idtac]. simpl; apply list_permut_occurs_in_term_list with (s1 :: t1 :: l1); trivial; apply quick_permut. left; right; trivial. right; left; trivial. right; right; simpl; case (X.eq_bool x v1); trivial. split; split; [trivial | idtac | idtac | idtac]. destruct O as [ [[O | O] | O] | [ O | O ]]. right; right; simpl in O; subst x; simpl; generalize (X.eq_bool_ok v1 v1); case (X.eq_bool v1 v1); [trivial | intro v1_diff_v1; apply False_rect; apply v1_diff_v1; reflexivity]. left; left; destruct l1 as [ | s1 [ | t1 l1]]; [contradiction | intuition | idtac]. simpl; apply list_permut_occurs_in_term_list with (s1 :: t1 :: l1); trivial; apply quick_permut. left; right; trivial. right; left; trivial. right; right; simpl; case (X.eq_bool x v1); trivial. simpl; intros [x_is_fresh | H]; [subst x; apply (fresh_var_spec _ O) | apply NE; trivial]. destruct l1 as [ | t1 l1]; destruct O as [ [[O | O] | O] | [ O | O ]]. simpl in O; subst x; simpl. right; left; simpl; generalize (X.eq_bool_ok v1 v1); case (X.eq_bool v1 v1); [trivial | intro v1_diff_v1; apply False_rect; apply v1_diff_v1; reflexivity]. contradiction. left; right; simpl; trivial. right; left; simpl; case (X.eq_bool x v1); trivial. right; right; trivial. right; left; simpl in O; subst x; simpl; generalize (X.eq_bool_ok v1 v1); case (X.eq_bool v1 v1); [trivial | intro v1_diff_v1; apply False_rect; apply v1_diff_v1; reflexivity]. left; left; simpl; apply list_permut_occurs_in_term_list with (Var (fresh_var (mk_pb ex ((Term f1 (Var v1 :: t1 :: l1), Term f1 l2) :: usp) sp psp)) :: t1 :: l1); [ apply quick_permut | right; trivial ]. left; right; trivial. right; left; simpl; case (X.eq_bool x v1); trivial. right; right; trivial. unfold ac_elementary_solve_term_term_term; intro pb'_in_lpb; pattern pb'; refine (prop_map_without_repetition _ T.eq_bool_ok _ _ _ _ _ pb'_in_lpb); clear pb' w_pb' pb'_in_lpb wpb_in_solve_pb; intros t2 t2_in_l2. destruct t2 as [ | g2 ll2 ]; [trivial | idtac]. generalize (F.Symb.eq_bool_ok g1 g2); case (F.Symb.eq_bool g1 g2); [intro g1_eq_g2 | intros _; trivial]. destruct (remove T.eq_bool (Term g2 ll2) l2) as [l2' | ]; [idtac | trivial]. split; [trivial | idtac]. destruct O as [ [[O | O] | O] | O]; [idtac | idtac | idtac | right; trivial]. left; left; trivial. left; right; left; destruct l1 as [ | s1 [ | t1 l1]]; [contradiction | intuition | idtac]. simpl; apply list_permut_occurs_in_term_list with (s1 :: t1 :: l1); trivial; apply quick_permut. left; right; right; trivial. destruct l1 as [ | s1 [ | t1 [ | u1 l1]]]; [intros; contradiction | intros; contradiction | idtac | intros; contradiction]. destruct l2 as [ | s2 [ | t2 [ | u2 l2]]]; [intros; contradiction | intros; contradiction | idtac | intros; contradiction]. intros [pb'_in_pb1 | [pb'_in_pb2 | pb'_in_nil]]; [subst pb' | subst pb' | contradiction]. split; trivial. destruct O as [ [[O | [O | O]] | O] | O ]; [idtac | idtac | idtac | idtac | right; trivial]. left; left; trivial. left; right; left; trivial. contradiction. left; right; right; trivial. split; trivial. destruct O as [ [[O | [O | O]] | O] | O ]; [idtac | idtac | idtac | idtac | right; trivial]. left; left; trivial. left; right; left; trivial. contradiction. left; right; right; trivial. generalize l1 l2 usp O; clear l1 l2 usp O w_pb wpb_in_solve_pb; induction l1 as [ | t1 l1]; destruct l2 as [ | t2 l2]; simpl. intros usp O [pb'_eq_pb1 | pb'_in_nil]; [subst pb' | contradiction]. split; [trivial | idtac]. destruct O as [ [O | O] | O ]; [idtac | idtac | right; trivial]. contradiction. left; trivial. contradiction. contradiction. intros usp O; simpl. assert (O' : occurs_in_pb x (mk_pb ex ((Term f1 l1, Term f1 l2) :: (t1,t2) :: usp) sp psp)). destruct O as [ [[O | O] | O] | O ]; [idtac | idtac | idtac | right; trivial ]. left; right; left; trivial. left; left; trivial. left; right; right; trivial. assert (H:= IHl1 l2 ((t1,t2) :: usp) O'). destruct (fold_left2 (fun (current_list_of_eqs : list (term * term)) (t3 t4 : term) => (t3, t4) :: current_list_of_eqs) ((t1, t2) :: usp) l1 l2) as [ | ]; [idtac | intros; contradiction]. intros pb'_in; generalize (H pb'_in); 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)