proposition: Lemma remove_several_subterms : forall sigma f 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) = t -> apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 -> match t with | Var _ => True | Term g l0 => if F.Symb.eq_bool f g then match remove_list l0 l2 with | None => False | Some l3 => if le_gt_dec (length l1) (length l3) then apply_cf_subst sigma (build f l1) = build f l3 else False end else True end.
proof: Proof. intros sigma f v l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma; 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; subst g | intros _; trivial]. assert (W_v : well_formed_cf (Var v)). simpl; trivial. assert (W_v_sigma := well_formed_cf_apply_subst W_sigma _ W_v); rewrite v_sigma in W_v_sigma. generalize (in_remove_list (well_formed_cf_sorted Ar W_v_sigma) (well_formed_cf_sorted Ar Wt2)). destruct (remove_list ll l2) as [l2' | ]. intro P; elim (le_gt_dec (length l1) (length l2')); intro L. assert (Al_l2' : forall t, In t l2' -> match t with Var _ => True | Term g _ => f <> g end). intros t In_t; apply (well_formed_cf_alien Ar Wt2). rewrite <- (list_permut.in_permut_in P). apply in_or_app; right; trivial. apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build_cons with (Var v); trivial. apply well_formed_cf_build; trivial. apply Nat.le_trans with (length l1); trivial. apply le_S_n; generalize (well_formed_cf_length Ar Wt1); trivial. intros t In_t; apply (well_formed_cf_subterms Wt2). rewrite <- (list_permut.in_permut_in P); apply in_or_app; right; trivial. rewrite <- (flatten_apply_cf_subst sigma l1 Ar); rewrite (flatten_build l2' Ar Al_l2'). rewrite (permut_app1 ll). transitivity l2. simpl in t1_sigma; rewrite Ar in t1_sigma. inversion_clear t1_sigma. simpl in v_sigma; rewrite v_sigma. generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. apply quick_permut. symmetry; trivial. generalize (proj1 (Nat.add_lt_mono_l _ _ (length ll)) L). rewrite <- length_app; assert (L' := list_permut.permut_length P). setoid_rewrite L'; clear L'. simpl in t1_sigma; rewrite Ar in t1_sigma. inversion_clear t1_sigma; rewrite length_quicksort; simpl in v_sigma; rewrite v_sigma; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite length_app; intro L'; assert (L'' := (proj2 (Nat.add_lt_mono_l _ _ (length ll)) L')); clear L L'. absurd (length l1 < length l1); auto with arith. refine (Nat.le_lt_trans _ _ _ _ L''). rewrite <- (length_map (apply_cf_subst sigma)). apply length_flatten_bis; trivial. intros t' t'_in_map_l1; rewrite in_map_iff in t'_in_map_l1; destruct t'_in_map_l1 as [t [Wt t_sigma]]. subst; apply well_formed_cf_apply_subst; trivial. apply (well_formed_cf_subterms Wt1); right; trivial. intro P; apply (P (flatten f (map (apply_cf_subst sigma) l1))); simpl in v_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma; rewrite v_sigma in t1_sigma; inversion_clear t1_sigma. simpl; trivial; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. apply quick_permut; auto. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching_sound)