proposition: Lemma total_acc_inst_inv : forall c sigma tau, is_a_total_oc_ordering sigma c = true -> (is_a_solution (mk_pb (acc_inst c sigma) nil) tau <-> is_a_solution (mk_pb sigma nil) tau).
proof: Proof. intro c; induction c as [ | v c]; intros sigma tau Hoc. simpl; intuition. assert (equiv_sol : forall rho rho' sol, (forall v, find X.eq_bool v rho = find X.eq_bool v rho') -> is_a_solution (mk_pb rho nil) sol -> is_a_solution (mk_pb rho' nil) sol). intros rho rho' sol r_eq_r' [_ Sol']; split. intros; contradiction. intro x; assert (Solx := Sol' x); simpl in Solx; simpl; rewrite r_eq_r' in Solx; trivial. assert (Hoc' : is_a_total_oc_ordering (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, apply_subst sigma (Var v)) :: nil) t) sigma) c = true). simpl in Hoc. destruct (var_in_term v match find X.eq_bool v sigma with | Some v_sigma => v_sigma | None => Var v end); [discriminate | idtac]. case_eq (list_exists (fun z : variable => var_in_term z match find X.eq_bool v sigma with | Some v_sigma => v_sigma | None => Var v end) c); intro Hoc'; rewrite Hoc' in Hoc; [discriminate | simpl in Hoc]. apply tail_total_ordering; trivial. simpl; split; intro Sol. rewrite (IHc _ tau Hoc') in Sol. rewrite (rep_var_is_complete v). refine (equiv_sol _ _ _ _ Sol). intros x; assert (F := find_map_subst x v (apply_subst sigma (Var v)) sigma). assert (F' := find_map X.eq_bool (apply_subst ((v, apply_subst sigma (Var v)) :: nil)) x sigma). simpl; generalize (X.eq_bool_ok x v); case (X.eq_bool x v); [intro v_eq_x; subst x | intro v_diff_x]. simpl in F; case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma; rewrite v_sigma in F; rewrite F. apply f_equal; rewrite <- (empty_subst_is_id v_val) at 3. rewrite <- subst_eq_vars. intros x x_in_v_val; simpl. generalize (X.eq_bool_ok x v); case (X.eq_bool x v); [intro v_eq_x; subst x | intros _; reflexivity]. rewrite <- var_in_term_is_sound in x_in_v_val. simpl in Hoc; rewrite v_sigma in Hoc; rewrite x_in_v_val in Hoc; discriminate. simpl in Hoc; rewrite v_sigma in Hoc; simpl in Hoc; revert Hoc. generalize (X.eq_bool_ok v v); case (X.eq_bool v v); [intros _ | intro v_diff_v]; [intros; discriminate | absurd (v = v); trivial]. simpl in F; simpl in F'; case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma; rewrite x_sigma in F; rewrite F; rewrite x_sigma in F'; rewrite F'; trivial. rewrite IHc; trivial. rewrite (rep_var_is_complete v) in Sol. refine (equiv_sol _ _ _ _ Sol). intros x; assert (F := find_map_subst x v (apply_subst sigma (Var v)) sigma). assert (F' := find_map X.eq_bool (apply_subst ((v, apply_subst sigma (Var v)) :: nil)) x sigma). simpl; generalize (X.eq_bool_ok x v); case (X.eq_bool x v); [intro v_eq_x; subst x | intros x_diff_v]. simpl in F; case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma; rewrite v_sigma in F; rewrite F. symmetry; apply f_equal; rewrite <- (empty_subst_is_id v_val) at 3. rewrite <- subst_eq_vars. intros x x_in_v_val; simpl. generalize (X.eq_bool_ok x v); case (X.eq_bool x v); [intro v_eq_x; subst x | intros x_diff_v]. rewrite <- var_in_term_is_sound in x_in_v_val. simpl in Hoc; rewrite v_sigma in Hoc; rewrite x_in_v_val in Hoc; discriminate. trivial. simpl in Hoc; rewrite v_sigma in Hoc; simpl in Hoc; revert Hoc. generalize (X.eq_bool_ok v v); case (X.eq_bool v v); [intros _ | intro v_diff_v]; [intros; discriminate | absurd (v = v); trivial]. simpl in F; simpl in F'; case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma; rewrite x_sigma in F; rewrite F; rewrite x_sigma in F'; rewrite F'; 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)