proposition: Lemma remove_several_subterms_bis : forall sigma f v v' l1 t l2, arity f = AC -> well_formed_cf_subst sigma -> well_formed_cf (Term f (Var v :: l1)) -> well_formed_cf (Term f l2) -> apply_cf_subst sigma (Var v) = Term f (quicksort (flatten f (apply_cf_subst sigma (Var v') :: t :: nil))) -> apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 -> match t with | Var _ => True | Term g _ => f<>g end -> match remove T.eq_bool t l2 with | None => False | Some l3 => apply_cf_subst sigma (build f (Var v' :: l1)) = build f l3 end.
proof: Proof. intros sigma f v v' l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma. generalize (in_remove _ _ T.eq_bool_ok t l2); destruct (remove T.eq_bool t l2) as [l2''' | ]. intros [cp1' [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]] Al_t. injection l2'''_eq; clear l2'''_eq; intro l2'''_eq; apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build; trivial. simpl; auto with arith. intros s [s_eq_v' | s_in_l1]; [subst; simpl | apply (well_formed_cf_subterms Wt1); right]; trivial. intros s [s_eq_v' | s_in_l1]; [subst; simpl | apply (well_formed_cf_alien Ar Wt1); right]; trivial. subst l2 l2'''; apply well_formed_cf_build_inside with t; subst; trivial. rewrite <- (flatten_apply_cf_subst sigma (Var v' :: l1) Ar); rewrite (flatten_build l2''' Ar); subst l2 l2''' cp1'. rewrite (@permut_cons_inside t t) by reflexivity. pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma. pattern (Var v') in v_sigma; unfold apply_cf_subst in v_sigma. rewrite v_sigma in t1_sigma; clear v_sigma. revert t1_sigma; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ t1_sigma | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H'; injection H'; intros; subst; trivial. setoid_rewrite <- (Inj _ _ t1_sigma); clear Inj. apply permut_sym; apply quick_permut_bis. transitivity (flatten f (apply_cf_subst sigma (Var v') :: t :: nil) ++ flatten f (map (apply_cf_subst sigma) l1)). rewrite <- permut_app2; apply quick_permut_bis; auto. replace (flatten f (map (apply_cf_subst sigma) (Var v' :: l1))) with ((flatten f (apply_cf_subst sigma (Var v') :: nil)) ++ flatten f (map (apply_cf_subst sigma) l1)); [ rewrite app_comm_cons | rewrite <- flatten_app; trivial]. rewrite <- permut_app2. replace (flatten f (apply_cf_subst sigma (Var v') :: t :: nil)) with ((flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil))); [idtac | rewrite <- flatten_app; simpl app; trivial]. replace (flatten f (t :: nil)) with (t :: nil). apply permut_sym; rewrite <- permut_cons_inside. rewrite <- app_nil_end; auto. reflexivity. simpl; destruct t as [x | g ll]; trivial. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; absurd (f = g); trivial | intros _; trivial]. intros s s_in_l2'_l2''; destruct (in_app_or _ _ _ s_in_l2'_l2'') as [s_in_l2' | s_in_l2'']; apply (well_formed_cf_alien Ar Wt2); apply in_or_app; [left | right; right]; trivial. intros Not_in Al_t; pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma. pattern (Var v') in v_sigma; unfold apply_cf_subst in v_sigma. rewrite v_sigma in t1_sigma; clear v_sigma. revert t1_sigma; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ t1_sigma | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H'; injection H'; intros; subst; trivial. rewrite <- (Inj _ _ t1_sigma) in Not_in; clear Inj. apply Not_in. apply in_impl_mem. reflexivity. rewrite <- in_quick_in. apply in_or_app; left. rewrite <- in_quick_in. replace (flatten f (match find eq_var_bool v' sigma with | Some v_sigma => v_sigma | None => Var v' end :: t :: nil)) with (flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil)). apply in_or_app; right; destruct t as [x | g ll]; simpl. left; trivial. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; absurd (f = g); trivial | intros _; left; trivial]. rewrite <- flatten_app; simpl app; trivial. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching_sound)