proposition: Theorem apply_cf_subst_is_sound : forall sigma sigma_cf, is_subst_canonical_form sigma sigma_cf -> forall t, apply_cf_subst sigma_cf (canonical_form t) = canonical_form (apply_subst sigma t).
proof: Proof. intros sigma sigma_cf H t; pattern t; apply term_rec3; clear t. intro v; generalize (H v); simpl; destruct (find X.eq_bool v sigma) as [t | ]; intro H_v; rewrite H_v; trivial. intros f l IH; assert (IHl : map (apply_cf_subst sigma_cf) (map canonical_form l) = map canonical_form (map (apply_subst sigma) l)). induction l as [ | t l]; trivial. simpl map; rewrite IHl. rewrite IH; [ idtac | left ]; trivial. intros; apply IH; right; trivial. simpl; apply (f_equal (fun l => Term f l)). destruct_arity f a Af. apply sort_is_unique; [apply quick_sorted | apply quick_sorted | idtac]; apply quick_permut_bis; apply permut_sym; apply quick_permut_bis; transitivity (flatten f (map (apply_cf_subst sigma_cf) (flatten f (map canonical_form l)))). rewrite <- IHl; generalize (map canonical_form l); clear l IHl IH. intro l; induction l as [ | t l]; auto. replace (t :: l) with ((t :: nil) ++ l); trivial. rewrite map_app; do 2 rewrite flatten_app; rewrite map_app; rewrite flatten_app; transitivity (flatten f (map (apply_cf_subst sigma_cf) (t :: nil)) ++ flatten f (map (apply_cf_subst sigma_cf) (flatten f l))). rewrite <- permut_app1; apply IHl. rewrite <- permut_app2. destruct t as [ v | g ll]; simpl; auto. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g; subst g | intros f_diff_g]. rewrite Af; do 2 rewrite <- app_nil_end; apply permut_sym; apply quick_permut. simpl; generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g; subst g | intros _]. apply False_rect; apply f_diff_g; reflexivity. reflexivity. apply list_permut_flatten; apply permut_map with (@eq term). intros; subst; reflexivity. apply quick_permut. apply sort_is_unique; [apply quick_sorted | apply quick_sorted | idtac]; do 2 (apply quick_permut_bis; apply permut_sym); rewrite <- IHl. apply permut_map with (@eq term). intros; subst; reflexivity. apply quick_permut_bis; auto. trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)