proposition: Lemma rep_var_is_complete : forall x sigma, let sigma' := (x, apply_subst sigma (Var x)) :: (map (fun xt => (fst xt, apply_subst ((x, apply_subst sigma (Var x)) :: nil) (snd xt))) sigma) in forall tau, is_a_solution (mk_pb sigma nil) tau <-> is_a_solution (mk_pb sigma' nil) tau.
proof: Proof. intros x sigma sigma'; subst sigma'; induction sigma as [ | [y y_val] sigma]; intros tau; unfold is_a_solution. simpl; split. intros; split. intros; contradiction. simpl; intros v. generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v; reflexivity | trivial]. intros _; split. intros; contradiction. trivial. split. intros [_ Hsol]; split. intros; contradiction. assert (Hsol_x := Hsol x); simpl in Hsol_x. intro v; assert (Hsol_v := Hsol v); simpl in Hsol_v. assert (F := find_map X.eq_bool (apply_subst ((x, (apply_subst ((y,y_val) :: sigma) (Var x))) :: nil)) v sigma). simpl; simpl in F; revert F Hsol_x. generalize (X.eq_bool_ok x y); case (X.eq_bool x y); [intro x_eq_y; subst y | intro x_diff_y]. revert Hsol_v; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v; trivial | intro v_diff_x]. destruct (find X.eq_bool v sigma) as [v_val | ]; intros Hsol_v F Hsol_x; rewrite F; trivial. rewrite Hsol_v; rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars; intros z z_in_v_val. rewrite subst_comp_is_subst_comp; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intros _]; trivial. generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v; trivial | intro v_diff_x]. revert Hsol_v; generalize (X.eq_bool_ok x y); case (X.eq_bool x y); [intro x_eq_y; absurd (x = y); trivial | intros _]. case (find X.eq_bool x sigma); trivial. revert Hsol_v; generalize (X.eq_bool_ok v y); case (X.eq_bool v y); [intro v_eq_y; subst v | intro v_diff_y]; intros Hsol_v F Hsol_x. rewrite Hsol_v; rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars; intros v v_in_y_val. rewrite subst_comp_is_subst_comp; simpl. generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v | intros _; trivial]. destruct (find X.eq_bool x sigma) as [x_val | ]; trivial. destruct (find X.eq_bool v sigma) as [v_val | ]; rewrite F; trivial. rewrite Hsol_v; rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars; intros z z_in_y_val. rewrite subst_comp_is_subst_comp; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intros _]; trivial. destruct (find X.eq_bool x sigma) as [x_val | ]; trivial. simpl; intros [_ Hsol]; split. intros; contradiction. intro v; generalize (Hsol x) (Hsol v); clear Hsol. generalize (find_map X.eq_bool (apply_subst ((x, (apply_subst ((y,y_val) :: sigma) (Var x))) :: nil)) v sigma). simpl; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _ | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. generalize (X.eq_bool_ok x y); case (X.eq_bool x y); [intro x_eq_y; subst y | intros x_diff_y]. generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v; trivial | intro v_diff_x]. case_eq (find X.eq_bool v sigma); [intros v_val v_sigma | intro v_sigma]; intros Hsol_v Hsol_x F; trivial. rewrite Hsol_v in F; rewrite F. rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars. intros z z_in_v_val. rewrite subst_comp_is_subst_comp; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intros _]; trivial. rewrite Hsol_x; trivial. generalize (X.eq_bool_ok v y); case (X.eq_bool v y); [intro v_eq_y; subst v | intro v_diff_y]. generalize (X.eq_bool_ok y x); case (X.eq_bool y x); [intro y_eq_x; absurd (x = y); subst; trivial | intro y_diff_x]. intros F Hsol_x Hsol_v. rewrite Hsol_v; rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars. intros z z_in_y_val. rewrite subst_comp_is_subst_comp; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intros _]; trivial. rewrite Hsol_x; trivial. generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v | intro v_diff_x]; intros F Hsol_x Hsol_v. rewrite Hsol_v; destruct (find X.eq_bool x sigma) as [x_val | ]; trivial. destruct (find X.eq_bool v sigma) as [v_val | ]; rewrite F in Hsol_v. rewrite Hsol_v. rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars. intros z z_in_v_val. rewrite subst_comp_is_subst_comp; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intros _]; trivial. rewrite Hsol_x; trivial. trivial. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)