proposition: Lemma total_acc_inst_head : forall c v sigma, VSet.without_red (v :: c) -> is_a_total_oc_ordering sigma (v :: c) = true -> apply_subst (acc_inst (v :: c) sigma) (Var v) = apply_subst sigma (Var v).
proof: Proof. intro c; induction c as [ | v' c]; intros v sigma W Hoc. assert (F := find_map_subst v v (apply_subst sigma (Var v)) sigma); simpl in F. simpl; simpl in Hoc; case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma; rewrite v_sigma in Hoc; rewrite v_sigma in F; rewrite F; [idtac | reflexivity]. rewrite <- (empty_subst_is_id v_val) at 3. rewrite <- subst_eq_vars. intros y y_in_v_val; simpl. generalize (X.eq_bool_ok y v); case (X.eq_bool y v); [intro y_eq_v | intro y_diff_v; reflexivity]. subst y; rewrite <- var_in_term_is_sound in y_in_v_val; rewrite y_in_v_val in Hoc; discriminate. simpl; simpl in Hoc; case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma; rewrite v_sigma in Hoc. case_eq (var_in_term v v_val); intro v_in_v_val; rewrite v_in_v_val in Hoc; [discriminate | simpl in Hoc]. assert (Idem : apply_subst ((v,v_val) :: nil) v_val = v_val). rewrite <- (empty_subst_is_id v_val) at 3. rewrite <- subst_eq_vars. intros y y_in_v_val; simpl. generalize (X.eq_bool_ok y v); case (X.eq_bool y v); [intro y_eq_v | intro y_diff_v; reflexivity]. subst y; rewrite <- var_in_term_is_sound in y_in_v_val; rewrite y_in_v_val in v_in_v_val; discriminate. assert (F' := find_map_subst v' v (apply_subst sigma (Var v)) sigma); simpl in F'. rewrite v_sigma in F'. case_eq (find X.eq_bool v' sigma); [intro v'_val | idtac]; intro v'_sigma; rewrite v'_sigma in F'; rewrite F'. assert (Switch : forall y, find X.eq_bool y (map_subst (fun (_ : variable) (t : term) => apply_subst ((v', apply_subst ((v, v_val) :: nil) v'_val) :: nil) t) (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, v_val) :: nil) t) sigma)) = find X.eq_bool y (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, v_val) :: nil) t) (map_subst (fun (_ : variable) (t : term) => apply_subst ((v', apply_subst ((v, v_val) :: nil) v'_val) :: nil) t) sigma))). intro y. assert (Fy := find_map_subst y v v_val sigma). assert (Fy' := find_map_subst y v' (apply_subst ((v, v_val) :: nil) v'_val) (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, v_val) :: nil) t) sigma)). assert (Fy'' := find_map_subst y v' (apply_subst ((v, v_val) :: nil) v'_val) sigma). assert (Fy''' := find_map_subst y v v_val (map_subst (fun (_ : variable) (t : term) => apply_subst ((v', apply_subst ((v, v_val) :: nil) v'_val) :: nil) t) sigma)). case_eq (find X.eq_bool y sigma); [intro y_val | idtac]; intro y_sigma; unfold DecVar.A in *; rewrite y_sigma in Fy; rewrite Fy in Fy'; rewrite Fy'; rewrite y_sigma in Fy''; rewrite Fy'' in Fy'''; rewrite Fy'''; [apply f_equal | reflexivity]. do 2 rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars. intros z z_in_y_val; simpl. generalize (X.eq_bool_ok z v); case (X.eq_bool z v); [intro z_eq_v; subst z | intro z_diff_v]. generalize (X.eq_bool_ok v v'); case (X.eq_bool v v'); [intro v_eq_v'; subst v' | intro v_diff_v']. apply False_rect; unfold VSet.without_red in W; simpl in W; revert W. unfold DecVar.eq_bool; generalize (X.eq_bool_ok v v); case (X.eq_bool v v); [intros _; discriminate | intros v_diff_v _; apply v_diff_v; reflexivity]. rewrite <- (empty_subst_is_id v_val) at 3. rewrite <- subst_eq_vars. intros u u_in_v_val; simpl. generalize (X.eq_bool_ok u v'); case (X.eq_bool u v'); [intro u_eq_v'; subst v' | intros _; reflexivity]. rewrite <- var_in_term_is_sound in u_in_v_val; rewrite u_in_v_val in Hoc; destruct (var_in_term v v_val); simpl in Hoc; discriminate. simpl. generalize (X.eq_bool_ok v' v); case (X.eq_bool v' v); [intro v'_eq_v; absurd (v' = v); trivial | intros _]. revert W; unfold VSet.without_red; simpl; unfold DecVar.eq_bool. generalize (X.eq_bool_ok v v'); case (X.eq_bool v v'); [intro v_eq_v'; intros; discriminate | intro v_diff_v']. subst v'; intros _; assumption. destruct (X.eq_bool z v'); [idtac | reflexivity]. rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars. intros u u_in_val; simpl. generalize (X.eq_bool_ok u v); case (X.eq_bool u v); [intro u_eq_v; subst v | intros _; reflexivity]. rewrite Idem; reflexivity. rewrite (acc_inst_eq_subst c _ _ Switch); clear Switch. assert (IH := IHc v (map_subst (fun (_ : variable) (t : term) => apply_subst ((v', apply_subst ((v, v_val) :: nil) v'_val) :: nil) t) sigma) (VSet.without_red_remove v' (v :: nil) c W)). simpl in IH. assert (F := find_map_subst v v' (apply_subst ((v, v_val) :: nil) v'_val) sigma). unfold DecVar.A in *; rewrite v_sigma in F; rewrite F in IH. assert (Idem' : apply_subst ((v', apply_subst ((v, v_val) :: nil) v'_val) :: nil) v_val = v_val). rewrite <- (empty_subst_is_id v_val) at 3. rewrite <- subst_eq_vars. intros u u_in_v_val; simpl. generalize (X.eq_bool_ok u v'); case (X.eq_bool u v'); [intro u_eq_v'; subst v' | intros _; reflexivity]. rewrite <- var_in_term_is_sound in u_in_v_val; rewrite u_in_v_val in Hoc; discriminate. rewrite Idem' in IH; rewrite IH; trivial. clear IH; rewrite v_in_v_val; simpl. case_eq (var_in_term v' v_val); intro v'_in_v_val; rewrite v'_in_v_val in Hoc; [discriminate | simpl in Hoc]. rewrite v'_sigma in Hoc. case_eq (list_exists (fun z : variable => var_in_term z v_val) c); intro Hoc'; rewrite Hoc' in Hoc; [discriminate | simpl in Hoc]. case_eq (var_in_term v' v'_val); intro v'_in_v'_val; rewrite v'_in_v'_val in Hoc; [discriminate | simpl in Hoc]. case_eq (list_exists (fun z : variable => var_in_term z v'_val) c); intro Hoc''; rewrite Hoc'' in Hoc; [discriminate | simpl in Hoc]. apply tail_total_ordering; trivial. assert (H : list_exists (fun z : variable => var_in_term z (apply_subst ((v, v_val) :: nil) v'_val)) c <> true). intro H; rewrite list_exists_is_sound in H; destruct H as [z [z_in_c z_in_val]]. rewrite no_var_in_term_inv in z_in_val. discriminate. apply (list_exists_is_complete_false _ _ Hoc' _ z_in_c). apply (list_exists_is_complete_false _ _ Hoc'' _ z_in_c). destruct (list_exists (fun z : variable => var_in_term z (apply_subst ((v, v_val) :: nil) v'_val)) c); [absurd (true = true) | idtac]; trivial. rewrite v'_sigma in Hoc. destruct (var_in_term v' v_val); [discriminate | idtac]. destruct (list_exists (fun z : variable => var_in_term z v_val) c); [discriminate | idtac]. simpl in Hoc; revert Hoc. generalize (X.eq_bool_ok v' v'); case (X.eq_bool v' v'); [intros _; intros; discriminate | intro v'_diff_v'; apply False_rect; apply v'_diff_v'; reflexivity]. 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]. 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)