# Library ac_matching.ac

``` Add LoadPath "basis". Add LoadPath "list_extensions". Add LoadPath "term_algebra". Add LoadPath "term_orderings". Require Import Relations. Require Import List. Require Import closure. Require Import more_list. Require Import list_permut. Require Import list_sort. Require Import Arith. Require Import term. Require Import term_o. Require Import equational_theory. Set Implicit Arguments. Module Type S.   Declare Module Import EqTh : equational_theory.EqTh.   Import T.   Import F.   Declare Module TO : ordered_set.S with Definition A := term.   Declare Module Import Sort : list_sort.Sort with Module DOS := TO.   Import LPermut. ```

## Definition of AC.

``` Inductive ac_one_step_at_top : term -> term -> Prop :=   | a_axiom :       forall (f:symbol) (t1 t2 t3:term),         arity f = AC ->         ac_one_step_at_top           (Term f ((Term f (t1 :: t2 :: nil)) :: t3 :: nil))           (Term f (t1 :: ((Term f (t2 :: t3 :: nil)) :: nil)))   | c_axiom :       forall (f:symbol) (t1 t2:term),         arity f = C \/ arity f = AC ->         ac_one_step_at_top (Term f (t1 :: t2 :: nil))           (Term f (t2 :: t1 :: nil)). Hint Constructors ac_one_step_at_top. Definition ac := th_eq ac_one_step_at_top. Fixpoint flatten (f : symbol) (l : list term) : list term :=   match l with   | nil => nil   | (Var _ as t) :: tl => t :: (flatten f tl)   | (Term g ll as t) :: tl =>            if eq_symbol_dec f g            then ll ++ (flatten f tl)            else t :: (flatten f tl)    end. Fixpoint canonical_form (t : term) : term :=   match t with   | Var _ => t   | Term f l =>     Term f       (match arity f with       | Free _ => map canonical_form l       | C => quicksort (map canonical_form l)       | AC => quicksort (flatten f (map canonical_form l))       end) end.  Fixpoint well_formed_cf (t:term) : Prop :=   match t with   | Var _ => True   | Term f l =>      let wf_cf_list :=        (fix wf_cf_list (l:list term) : Prop :=        match l with        | nil => True        | h :: tl => well_formed_cf h /\ wf_cf_list tl        end) in        wf_cf_list l /\      (match arity f with      | Free n => length l = n      | C => length l = 2 /\ is_sorted l      | AC => length l >= 2 /\              is_sorted l /\              (forall s, In s l -> match s with                                   | Var _ => True                                   | Term g _ => f<>g                                   end)      end)   end. Definition build (f : symbol) l :=   match l with   | t :: nil => t   | _ => Term f (quicksort l)   end. Definition well_formed_cf_subst sigma :=   forall v, match find eq_variable_dec v sigma with             | None => True             | Some t => well_formed_cf t             end.  Fixpoint apply_cf_subst (sigma : substitution) (t : term) {struct t} : term :=   match t with   | Var v =>     match find eq_variable_dec v sigma with     | None => t     | Some v_sigma => v_sigma     end   | Term f l =>      let l_sigma :=        match arity f with        | AC => quicksort (flatten f (map (apply_cf_subst sigma) l))        | C => quicksort (map (apply_cf_subst sigma) l)        | Free _ => map (apply_cf_subst sigma) l      end in    Term f l_sigma  end.  Fixpoint ac_size (t:term) : nat :=   match t with   | Var v => 1   | Term f l =>        let ac_size_list :=          (fix ac_size_list (l : list term) {struct l} : nat :=             match l with             | nil => 0             | t :: lt => ac_size t + ac_size_list lt             end) in      (match arity f with       | AC => (length l) - 1       | C => 1       | Free _ => 1       end) + ac_size_list l    end.  Axiom l_assoc :   forall f t1 t2 t3, arity f = AC ->   ac (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil))        (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil)). Axiom r_assoc :   forall f t1 t2 t3, arity f = AC ->   ac (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil))        (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil)). Axiom comm :   forall f t1 t2, arity f = C \/ arity f = AC ->   ac (Term f (t1 :: t2 :: nil)) (Term f (t2 :: t1 :: nil)). Axiom ac_top_eq :   forall t1 t2, ac t1 t2 ->   match t1, t2 with    | Var x1, Var x2 => x1 = x2    | Term _ _, Var _ => False    | Var _, Term _ _ => False    | Term f1 _, Term f2 _ => f1 = f2    end. Axiom well_formed_cf_unfold : forall t,  well_formed_cf t -> match t with                     | Var _ => True                     | Term f l =>                       (forall u, In u l -> well_formed_cf u) /\                       (match arity f with                        | AC => length l >= 2 /\ is_sorted l /\                                (forall u, In u l -> match u with                                                     | Var _ => True                                                     | Term g _ => f <> g                                                     end)                        | C => length l = 2 /\ is_sorted l                        | Free n => length l = n                        end)                        end. Axiom well_formed_cf_subterms :  forall f l, well_formed_cf (Term f l) -> (forall t, In t l -> well_formed_cf t). Axiom well_formed_cf_length :  forall f l, arity f = AC -> well_formed_cf (Term f l) -> 2 <= length l. Axiom well_formed_cf_sorted :  forall f l, arity f = AC -> well_formed_cf (Term f l) -> is_sorted l. Axiom well_formed_cf_alien :  forall f l, arity f = AC -> well_formed_cf (Term f l) ->  (forall t, In t l -> match t with                           | Var _ => True                           | Term g _ => f <> g                           end).  Axiom flatten_app :   forall f l1 l2, flatten f (l1 ++ l2) = (flatten f l1) ++ (flatten f l2). Axiom list_permut_flatten :   forall f l1 l2, permut l1 l2 -> permut (flatten f l1) (flatten f l2). Axiom length_flatten_bis : forall f, arity f = AC ->   forall l, (forall t, In t l -> well_formed_cf t) ->  (length l) <= length (flatten f l). Axiom flatten_cf :  forall f t1 t2, arity f = AC -> well_formed_cf t1 -> well_formed_cf t2 ->  permut (flatten f (t1 :: nil)) (flatten f (t2 :: nil)) ->  t1 = t2.  Axiom flatten_cf_cf :  forall f t1 t2, arity f = AC -> well_formed t1 -> well_formed t2 ->  permut (flatten f (canonical_form t1 :: nil))  (flatten f (canonical_form t2 :: nil)) ->  canonical_form t1 = canonical_form t2. Axiom build_eq_Term : forall f l, 2 <= length l -> build f l = Term f (quicksort l). Axiom well_formed_cf_build :  forall f l, arity f = AC ->  1 <= length l ->  (forall t, In t l -> well_formed_cf t) ->  (forall t, In t l -> match t with | Var _ => True | Term g _ => f <> g end) ->  well_formed_cf (build f l). Axiom well_formed_cf_build_cons :  forall f t l, arity f = AC ->  well_formed_cf (Term f (t :: l)) -> well_formed_cf (build f l). Axiom well_formed_cf_build_inside : forall f t l1 l2, arity f = AC ->  well_formed_cf (Term f (l1 ++ t :: l2)) -> well_formed_cf (build f (l1 ++ l2)). Axiom flatten_build :  forall f l, arity f = AC ->  (forall t, In t l -> match t with | Var _ => True | Term g _ => f <> g end) ->  permut (flatten f ((build f l) :: nil)) l. Axiom flatten_build_cons :  forall f t l, arity f = AC -> well_formed_cf (Term f (t :: l)) ->  permut (flatten f ((build f l) :: nil)) l. Axiom flatten_build_inside :  forall f t l1 l2, arity f = AC ->  well_formed_cf (Term f (l1 ++ t :: l2)) ->  permut (flatten f ((build f (l1 ++ l2)) :: nil)) (l1 ++ l2). Axiom flatten_apply_cf_subst :  forall sigma f l, arity f = AC ->   permut (flatten f (map (apply_cf_subst sigma) l))   (flatten f (apply_cf_subst sigma (build f l) :: nil)). Axiom well_formed_cf_apply_subst :   forall sigma, well_formed_cf_subst sigma ->   forall t, well_formed_cf t -> well_formed_cf (apply_cf_subst sigma t). Axiom length_flatten_ter : forall f sigma, arity f = AC -> well_formed_cf_subst sigma ->   forall l, (forall t, In t l -> well_formed_cf t) ->   length l <= length (flatten f (map (apply_cf_subst sigma) l)). Axiom ac_cf_eq : forall t1 t2, ac t1 t2 -> canonical_form t1 = canonical_form t2. Axiom ac_size_eq : forall t1 t2, ac t1 t2 -> size t1 = size t2. Axiom ac_size_unfold :   forall t,   ac_size t = match t with               | Var _ => 1               | Term f l =>                 (match arity f with                 | AC => (length l) - 1                 | C => 1                 | Free _ => 1                 end) + list_size ac_size l                end.  Axiom size_size_aux3 :  forall f t, arity f = AC -> well_formed t ->  1 <= length (A:=term) (flatten f (canonical_form t :: nil)). Axiom size_size :  forall t, well_formed t -> size t = ac_size (canonical_form t). Axiom ac_size_ge_one : forall t, well_formed_cf t -> 1 <= ac_size t. End S. Module Make (T1: term.Term) (OF1 : ordered_set.S with Definition A := T1.symbol) (OX1 : ordered_set.S with Definition A := T1.variable) : S with Module EqTh.T := T1. Module T := T1. Module Import EqTh := equational_theory.Make (T). Import T. Import F. Import X. ```

## Definition of AC.

``` Inductive ac_one_step_at_top : term -> term -> Prop :=   | a_axiom :       forall (f:symbol) (t1 t2 t3:term),         arity f = AC ->         ac_one_step_at_top           (Term f ((Term f (t1 :: t2 :: nil)) :: t3 :: nil))           (Term f (t1 :: ((Term f (t2 :: t3 :: nil)) :: nil)))   | c_axiom :       forall (f:symbol) (t1 t2:term),         arity f = C \/ arity f = AC ->         ac_one_step_at_top (Term f (t1 :: t2 :: nil))           (Term f (t2 :: t1 :: nil)). Hint Constructors ac_one_step_at_top. Definition ac := th_eq ac_one_step_at_top. Lemma no_need_of_instance :   forall t1 t2, axiom (sym_refl ac_one_step_at_top) t1 t2 ->                      (sym_refl ac_one_step_at_top) t1 t2. Proof. unfold sym_refl; intros t1 t2 H. inversion_clear H as [ u1 u2 sigma H']; destruct H' as [H' | [H' | H']]. inversion_clear H'. left; simpl; apply a_axiom; trivial. left; simpl; apply c_axiom; trivial. inversion_clear H'. right; left; simpl; apply a_axiom; trivial. right; left; simpl; apply c_axiom; trivial. right; right; subst; trivial. Qed. Lemma l_assoc :   forall f t1 t2 t3, arity f = AC ->   ac (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil))        (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil)). Proof. intros f t1 t2 t3 Af. unfold ac, th_eq, rwr; apply t_step; apply at_top. rewrite <- (empty_subst_is_id (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil))). rewrite <- (empty_subst_is_id (Term f (t1 :: Term f (t2 :: t3 :: nil) :: nil))). apply instance. left; apply a_axiom; trivial. Qed. Lemma r_assoc :   forall f t1 t2 t3, arity f = AC ->   ac (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil))        (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil)). Proof. intros f t1 t2 t3 Af. unfold ac, th_eq, rwr; apply t_step; apply at_top. rewrite <- (empty_subst_is_id (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil))). rewrite <- (empty_subst_is_id (Term f (t1 :: Term f (t2 :: t3 :: nil) :: nil))). apply instance. right; left; apply a_axiom; trivial. Qed. Lemma comm :   forall f t1 t2, arity f = C \/ arity f = AC ->   ac (Term f (t1 :: t2 :: nil)) (Term f (t2 :: t1 :: nil)). Proof. intros f t1 t2 Af. unfold ac, th_eq, rwr; apply t_step; apply at_top. rewrite <- (empty_subst_is_id (Term f (t1 :: t2 :: nil))). rewrite <- (empty_subst_is_id (Term f (t2 :: t1 :: nil))). apply instance. left; apply c_axiom; trivial. Qed. Lemma ac_one_step_at_top_top_eq :   forall t1 t2, (sym_refl ac_one_step_at_top) t1 t2 ->    match t1, t2 with    | Var x1, Var x2 => x1 = x2    | Term _ _, Var _ => False    | Var _, Term _ _ => False    | Term f1 _, Term f2 _ => f1 = f2    end. Proof. unfold sym_refl; intros t1 t2 [Ac | [Ac | t1_eq_t2]]. inversion_clear Ac; simpl; trivial. inversion_clear Ac; simpl; trivial. subst t2; destruct t1; trivial. Qed. Lemma ac_one_step_top_eq :   forall t1 t2 : term, one_step (sym_refl ac_one_step_at_top) t1 t2 ->   match t1, t2 with    | Var x1, Var x2 => x1 = x2    | Term _ _, Var _ => False    | Var _, Term _ _ => False    | Term f1 _, Term f2 _ => f1 = f2    end. Proof. intros t1 t2 Ac; inversion Ac; trivial. apply ac_one_step_at_top_top_eq; apply no_need_of_instance; trivial. Qed. Lemma ac_top_eq :   forall t1 t2, ac t1 t2 ->   match t1, t2 with    | Var x1, Var x2 => x1 = x2    | Term _ _, Var _ => False    | Var _, Term _ _ => False    | Term f1 _, Term f2 _ => f1 = f2    end. Proof. intros t1 t2 Ac; induction Ac as [t1 t2 H | t1 t2 t3 H H']. inversion H as [ H1 H2 H' H4 H5 | f l1 l2 H' H1 H2]; subst. inversion H' as [u1 u2 sigma H'' H5 H6]; subst. destruct H'' as [H'' | [ H'' | H'']]. inversion H''; subst; simpl; trivial. inversion H''; subst; simpl; trivial. subst u2; destruct (apply_subst sigma u1); trivial. trivial. assert (H'' := ac_one_step_top_eq H). destruct t1 as [ v1 | f1 l1 ]; destruct t2 as [ v2 | f2 l2 ]; destruct t3 as [ v3 | f3 l3 ]; trivial. apply trans_eq with v2; trivial. contradiction. contradiction. apply trans_eq with f2; trivial. Qed. Module TO := term_o.Make (T1) (OF1) (OX1). Module Import Sort := list_sort.Make (TO). Import LPermut. Fixpoint flatten (f : symbol) (l : list term) : list term :=   match l with   | nil => nil   | (Var _ as t) :: tl => t :: (flatten f tl)   | (Term g ll as t) :: tl =>            if eq_symbol_dec f g            then ll ++ (flatten f tl)            else t :: (flatten f tl)    end. Fixpoint canonical_form (t : term) : term :=   match t with   | Var _ => t   | Term f l =>     Term f       (match arity f with       | Free _ => map canonical_form l       | C => quicksort (map canonical_form l)       | AC => quicksort (flatten f (map canonical_form l))       end) end. Fixpoint well_formed_cf (t:term) : Prop :=   match t with   | Var _ => True   | Term f l =>      let wf_cf_list :=        (fix wf_cf_list (l:list term) : Prop :=        match l with        | nil => True        | h :: tl => well_formed_cf h /\ wf_cf_list tl        end) in        wf_cf_list l /\      (match arity f with      | Free n => length l = n      | C => length l = 2 /\ is_sorted l      | AC => length l >= 2 /\              is_sorted l /\              (forall s, In s l -> match s with                                   | Var _ => True                                   | Term g _ => f<>g                                   end)      end)   end. Lemma well_formed_cf_unfold : forall t,  well_formed_cf t -> match t with                     | Var _ => True                     | Term f l =>                       (forall u, In u l -> well_formed_cf u) /\                       (match arity f with                        | AC => length l >= 2 /\ is_sorted l /\                                (forall u, In u l -> match u with                                                     | Var _ => True                                                     | Term g _ => f <> g                                                     end)                        | C => length l = 2 /\ is_sorted l                        | Free n => length l = n                        end)                        end. Proof. intro t; destruct t as [v | f l]; simpl; trivial; intros [Wl Ll]; split; trivial. clear Ll; induction l as [ | t l]. contradiction. intros u [u_eq_t | In_u]; subst; intuition. Qed. Lemma well_formed_cf_subterms :  forall f l, well_formed_cf (Term f l) -> (forall t, In t l -> well_formed_cf t). Proof. intros f l W; elim (well_formed_cf_unfold _ W); trivial. Qed. Lemma well_formed_cf_length :  forall f l, arity f = AC -> well_formed_cf (Term f l) -> 2 <= length l. Proof. intros f l Af [_ Ll]; rewrite Af in Ll; intuition. Qed. Lemma well_formed_cf_sorted :  forall f l, arity f = AC -> well_formed_cf (Term f l) -> is_sorted l. Proof. intros f l Af [_ Ll]; rewrite Af in Ll; intuition. Qed. Lemma well_formed_cf_alien :  forall f l, arity f = AC -> well_formed_cf (Term f l) ->  (forall t, In t l -> match t with                           | Var _ => True                           | Term g _ => f <> g                           end). Proof. intros f l Af [_ Ll]; rewrite Af in Ll; intuition. Qed. Lemma well_formed_cf_fold : forall t, (match t with                     | Var _ => True                     | Term f l =>                       (forall u, In u l -> well_formed_cf u) /\                       (match arity f with                        | AC => length l >= 2 /\ is_sorted l /\                                (forall u, In u l -> match u with                                                     | Var _ => True                                                     | Term g _ => f <> g                                                     end)                        | C => length l = 2 /\ is_sorted l                        | Free n => length l = n                        end)                        end) -> well_formed_cf t. Proof. intro t; destruct t as [v | f l]; trivial. intros [Wl Hl]; split; trivial; clear Hl; induction l as [ | t l]; intuition; apply IHl; intros; apply Wl; right; trivial. Qed. Lemma flatten_app :   forall f l1 l2, flatten f (l1 ++ l2) = (flatten f l1) ++ (flatten f l2). Proof. intros f l1; induction l1 as [ | [v1 | g1 ll1]]; simpl; trivial. intros l2; rewrite IHl1; trivial. intros l2; rewrite IHl1; destruct (eq_symbol_dec f g1) as [f_eq_g1 | f_diff_g1]. rewrite app_ass; trivial. simpl; trivial. Qed. Lemma list_permut_flatten :   forall f l1 l2, permut l1 l2 -> permut (flatten f l1) (flatten f l2). Proof. intros f l1; induction l1 as [ | t1 l1]; intros l2 P. rewrite (permut_nil (permut_sym P)); apply permut_refl. assert (In_t1 : mem t1 l2). setoid_rewrite <- P; left; reflexivity. destruct (mem_split_set _ _ In_t1) as [t1' [l2' [l2'' [t1_eq_t1' H]]]]; simpl in t1_eq_t1'; simpl in H; subst l2; assert (P' : permut (flatten f l1) (flatten f (l2' ++ l2''))). apply IHl1. setoid_rewrite <- permut_cons_inside in P; trivial. unfold EDS.eq_A, Sort.EDS.eq_A in t1_eq_t1'; subst t1'. rewrite flatten_app; simpl; destruct t1 as [v1 | f1 ll1]. setoid_rewrite <- permut_cons_inside. reflexivity. rewrite <- flatten_app; trivial. destruct (eq_symbol_dec f f1) as [f_eq_f1 | f_diff_f1]; subst. transitivity (ll1 ++ flatten f1 (l2' ++ l2'')). setoid_rewrite <- permut_app1; trivial. rewrite flatten_app; do 2 rewrite <- app_ass; setoid_rewrite <- permut_app2; apply list_permut_app_app. setoid_rewrite <- permut_cons_inside. reflexivity. rewrite <- flatten_app; trivial. Qed. Lemma well_formed_cf_is_well_formed_cf :  forall cf, well_formed_cf cf -> exists t, well_formed t /\ cf = canonical_form t. Proof. intros cf Wcf; generalize (well_formed_cf_unfold _ Wcf); pattern cf; apply term_rec3; clear cf Wcf. intros v _; exists (Var v); simpl; split; trivial. intros f l Hrec [Wl Ll]; assert (Wl' : forall u, In u l -> exists s, well_formed s /\ u = canonical_form s). intros u In_u; apply Hrec; trivial; apply well_formed_cf_unfold; apply Wl; trivial. destruct_arity f n Af. generalize Ll; clear Ll; intros [Ll [Sl Al]]; induction l as [ | t1 l]. absurd (0 >= 2); trivial; unfold ge; auto with arith. destruct l as [ | t2 l]. absurd (1 >= 2); trivial; unfold ge; auto with arith. elim (Wl' t1). intros u1 [Wu1 Hu1] . elim (Wl' t2). intros u2 [Wu2 Hu2] . assert (At1 : match t1 with Var _ => True | Term g _ => f <> g end). apply Al; left; trivial. assert (At2 : match t2 with Var _ => True | Term g _ => f <> g end). apply Al; right; left; trivial. destruct l as [ | t3 l]. exists (Term f (u2 :: u1 :: nil)); split. apply well_formed_fold; rewrite Af; split; trivial. intros u In_u; elim In_u; clear In_u; intro In_u; try subst u; trivial; elim In_u; clear In_u; intro In_u; try subst u; trivial; contradiction. simpl; rewrite Af; rewrite <- Hu1; rewrite <- Hu2. destruct t1 as [v1 | g1 ll1]; destruct t2 as [v2 | g2 ll2]. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Var v2 :: nil) (Var v1 :: nil)). destruct (eq_symbol_dec f g2) as [f_eq_g2 | f_diff_g2]. absurd (f=g2); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Term g2 ll2 :: nil) (Var v1 :: nil)). destruct (eq_symbol_dec f g1) as [f_eq_g1 | f_diff_g1]. absurd (f=g1); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Var v2 :: nil) (Term g1 ll1 :: nil)). destruct (eq_symbol_dec f g2) as [f_eq_g2 | f_diff_g2]. absurd (f=g2); trivial. destruct (eq_symbol_dec f g1) as [f_eq_g1 | f_diff_g1]. absurd (f=g1); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply (list_permut_app_app (Term g2 ll2 :: nil) (Term g1 ll1 :: nil)). elim IHl. intros s2 [Ws2 Hs2]; exists (Term f (s2 :: u1 :: nil)); split. apply well_formed_fold; rewrite Af; split; trivial. intros u In_u; elim In_u; clear In_u; intro In_u; try subst u; trivial; elim In_u; clear In_u; intro In_u; try subst u; trivial; contradiction. simpl; rewrite Af; rewrite <- Hu1; rewrite <- Hs2. destruct (eq_symbol_dec f f) as [ f_eq_f | f_diff_f ]. destruct t1 as [v1 | g1 ll1]. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply permut_sym; setoid_rewrite <- permut_cons_inside. reflexivity. rewrite <- app_nil_end; apply permut_refl. destruct (eq_symbol_dec f g1) as [f_eq_g1 | f_diff_g1]. absurd (f=g1); trivial. apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial. apply quick_sorted. apply permut_sym; apply quick_permut_bis; apply permut_sym; setoid_rewrite <- permut_cons_inside. reflexivity. rewrite <- app_nil_end; apply permut_refl. absurd (f=f); trivial. intros; apply Hrec; trivial; right; trivial. intros; apply Wl; right; trivial. intros; apply Wl'; right; trivial. simpl; auto with arith. apply sorted_tl_sorted with t1; trivial. intros; apply Al; right; trivial. right; left; trivial. left; trivial. generalize Ll; clear Ll; intros [Ll Sl]; destruct l as [ | t1 l]. absurd (0 = 2); auto with arith. destruct l as [ | t2 l]. absurd (1 = 2); auto with arith. destruct l as [ | t3 l]. elim (Wl' t1). intros u1 [Wu1 Hu1] . elim (Wl' t2). intros u2 [Wu2 Hu2] . exists (Term f (u1 :: u2 :: nil)); split. apply well_formed_fold; rewrite Af; split; trivial. intros u In_u; elim In_u; clear In_u; intro In_u; try subst u; trivial; elim In_u; clear In_u; intro In_u; try subst u; trivial; contradiction. simpl; rewrite Af; subst; apply (f_equal (fun l => Term f l)); apply sort_is_unique; trivial; [ apply quick_sorted | apply quick_permut ]. right; left; trivial. left; trivial. absurd (S(S(S(length l))) = 2); auto. assert (H : exists l', (forall s, In s l' -> well_formed s) /\                                map canonical_form l' = l). generalize l Wl'; clear l Hrec Wl Wl' Ll; induction l as [ | t l]. intros _; exists (nil (A := term)); split; trivial; contradiction. intros Wl; elim IHl. intros l' [Wl' Hl']; elim (Wl t). intros t' [Wt' Ht']; exists (t' :: l'); split; trivial. intros s [ s_eq_t' | In_s]; try subst s; trivial; apply Wl'; trivial. simpl; subst; trivial. left; trivial. intros; apply Wl; right; trivial. elim H; clear H; intros l' [Wl'' Hl']; exists (Term f l'); split. apply well_formed_fold; rewrite Af; subst; rewrite length_map; split; trivial. simpl; rewrite Af; subst; trivial. Qed. Lemma length_flatten_bis : forall f, arity f = AC ->   forall l, (forall t, In t l -> well_formed_cf t) ->  (length l) <= length (flatten f l). Proof. intros f Af l Wl; induction l as [ | t l]. simpl; auto with arith. simpl; destruct t as [v | g ll]. simpl; apply le_n_S; apply IHl; intros; apply Wl; right; trivial. destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]. rewrite length_app; replace (S (length l)) with (1 + length l); trivial; apply plus_le_compat. assert (Wt : well_formed_cf (Term g ll)). apply Wl; left; trivial. unfold well_formed_cf in Wt; subst g; rewrite Af in Wt; destruct Wt as [_ [Lll _]]; auto with arith. apply IHl; intros; apply Wl; right; trivial. simpl; apply le_n_S; apply IHl; intros; apply Wl; right; trivial. Qed. Lemma length_flatten :   forall f, forall l, arity f = AC -> (forall u, In u l -> well_formed u) ->   length l <= length (flatten f (map canonical_form l)). Proof. intros f l; pattern l; apply (list_rec3 size); clear l; induction n; destruct l as [ | t l]. simpl; trivial. simpl; intro S_l; absurd (1 <= 0); auto with arith; apply le_trans with (size t + list_size size l); trivial; apply le_plus_trans; apply size_ge_one. simpl; trivial. intros Sl Af Wl; replace (t :: l) with ((t :: nil) ++ l); trivial; rewrite map_app; rewrite flatten_app; do 2 rewrite length_app; apply plus_le_compat. assert (Wt : well_formed t). apply Wl; left; trivial. destruct t as [v | g ll]; simpl; auto with arith. destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]; subst. rewrite <- app_nil_end; rewrite Af; rewrite length_quicksort; apply le_trans with (length ll). elim (well_formed_unfold _ Wt); rewrite Af; intros _ Lll; rewrite Lll; auto with arith. apply IHn; trivial. apply le_S_n; apply le_trans with (size (Term g ll) + list_size size l); trivial; rewrite size_unfold; simpl; apply le_n_S; apply le_plus_l. elim (well_formed_unfold _ Wt); rewrite Af; trivial. apply le_n. apply IHn; trivial. apply plus_le_reg_l with 1; apply le_trans with (size t + list_size size l); trivial; apply plus_le_compat_r; apply size_ge_one. intros; apply Wl; right; trivial. Qed. Lemma well_formed_cf_is_well_formed_cf_conv :  forall cf, (exists t, well_formed t /\ cf = canonical_form t) -> well_formed_cf cf. Proof. intros cf [t [Wt Ct]]; subst; generalize Wt; clear Wt. pattern t; apply term_rec2; clear t; induction n as [ | n ]; intros t St Wt. absurd (1 <= 0); auto with arith; apply le_trans with (size t); trivial; apply size_ge_one. apply well_formed_cf_fold; destruct t as [ v | f l ]; trivial. generalize (well_formed_unfold _ Wt); simpl; intros [Wl L]. assert (Wl' : forall t, In t (map canonical_form l) -> well_formed_cf t). clear Wt L; rewrite size_unfold in St; induction l as [ | t1 l ]. contradiction. intros t In_t; elim In_t; clear In_t; intro In_t; subst. apply IHn; [ apply le_trans with (list_size size (t1 :: l)); simpl; auto with arith | apply Wl; left; trivial ]. apply IHl; trivial; [ apply le_trans with (1 + list_size size (t1 :: l)); simpl; auto with arith | intros; apply Wl; right; trivial]. destruct_arity f a Af. split; [idtac | split; [idtac | split]]. intros u In_u; setoid_rewrite <- in_quick_in in In_u. generalize (map canonical_form l) Wl' In_u; clear l St Wt Wl L Wl' In_u; intro l; induction l as [ | t l ]; intros Wl In_u. contradiction. assert (H:=flatten_app f (t :: nil) l); simpl app in H; rewrite H in In_u; clear H; elim (in_app_or _ _ _ In_u); clear In_u; intro In_u. assert (Wt : well_formed_cf t). apply Wl; left; trivial. destruct t as [v | g h]. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]; subst. rewrite <- app_nil_end in In_u; apply (well_formed_cf_subterms Wt); trivial. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. apply IHl; trivial; intros; apply Wl; right; trivial. rewrite length_quicksort; rewrite <- L; unfold ge; apply length_flatten; trivial. apply quick_sorted. intros u In_u; setoid_rewrite <- in_quick_in in In_u. generalize (map canonical_form l) In_u Wl'; clear l St Wt Wl L Wl' In_u; intro l; pattern l; apply (list_rec3 size); clear l; induction n0 as [ | m]; destruct l as [ | t l ]. contradiction. intro H; absurd (1 <= 0); auto with arith; apply le_trans with (list_size size (t :: l)); trivial; apply le_trans with (size t); simpl; auto with arith; apply size_ge_one. contradiction. assert (H:=flatten_app f (t :: nil) l); simpl app in H; rewrite H; clear H. intros Sl In_u Wl; elim (in_app_or _ _ _ In_u); clear In_u; intro In_u. assert (Wt : well_formed_cf t). apply Wl; left; trivial. destruct t as [ v | g ll ]. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]. subst g; rewrite <- app_nil_end in In_u; apply well_formed_cf_alien with ll; trivial. elim In_u; clear In_u; intro In_u; subst; trivial; contradiction. apply (IHm l); trivial. apply le_S_n; apply le_trans with (1 + list_size size l); auto with arith; apply le_trans with (size t + list_size size l); trivial; apply plus_le_compat_r; apply size_ge_one. intros; apply Wl; right; trivial. split; [idtac | split]. intros u In_u; setoid_rewrite <- in_quick_in in In_u. apply Wl'; trivial. rewrite length_quicksort; rewrite length_map; trivial. apply quick_sorted. split; trivial; rewrite length_map; trivial. Qed. Lemma flatten_cf :  forall f t1 t2, arity f = AC -> well_formed_cf t1 -> well_formed_cf t2 ->  permut (flatten f (t1 :: nil)) (flatten f (t2 :: nil)) -> t1 = t2. Proof. intros f t1 t2 Af Wt1 Wt2; destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]. simpl; intros; apply permut_length_1; trivial. simpl; destruct (eq_symbol_dec f f2) as [f_eq_f2 | f_diff_f2]; subst. rewrite <- app_nil_end; intro P; absurd (2 <= 1); auto with arith. generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite L; auto with arith; apply well_formed_cf_length with f2; trivial. intro P; apply permut_length_1; trivial. simpl; destruct (eq_symbol_dec f f1) as [f_eq_f1 | f_diff_f1]; subst. rewrite <- app_nil_end; intro P; absurd (2 <= 1); auto with arith. generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite <- L; auto with arith; apply well_formed_cf_length with f1; trivial. intro P; apply permut_length_1; trivial. simpl; destruct (eq_symbol_dec f f1) as [f_eq_f1 | f_diff_f1]; destruct (eq_symbol_dec f f2) as [f_eq_f2 | f_diff_f2]; intro P. subst f1 f2; apply (f_equal (fun l => Term f l)); do 2 rewrite <- app_nil_end in P; apply sort_is_unique; trivial; apply well_formed_cf_sorted with f; trivial. subst f; absurd (2 <= 1); auto with arith. rewrite <- app_nil_end in P; generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite <- L; auto with arith; apply well_formed_cf_length with f1; trivial. subst f; absurd (2 <= 1); auto with arith. rewrite <- app_nil_end in P; generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite L; auto with arith; apply well_formed_cf_length with f2; trivial. apply permut_length_1; trivial. Qed. Lemma flatten_cf_cf :  forall f t1 t2, arity f = AC -> well_formed t1 -> well_formed t2 ->  permut (flatten f (canonical_form t1 :: nil))  (flatten f (canonical_form t2 :: nil)) ->  canonical_form t1 = canonical_form t2. Proof. intros f t1 t2 Af Wt1 Wt2 P; apply flatten_cf with f; trivial. apply well_formed_cf_is_well_formed_cf_conv; exists t1; split; trivial. apply well_formed_cf_is_well_formed_cf_conv; exists t2; split; trivial. Qed. Definition build (f : symbol) l :=   match l with   | t :: nil => t   | _ => Term f (quicksort l)   end. Lemma build_eq_Term : forall f l, 2 <= length l -> build f l = Term f (quicksort l). Proof. intros f l Ll; destruct l as [ | u [ | v l]]; simpl; trivial. simpl in Ll; absurd (2 <= 1); auto with arith. Qed. Lemma well_formed_cf_build :  forall f l, arity f = AC ->  1 <= length l ->  (forall t, In t l -> well_formed_cf t) ->  (forall t, In t l -> match t with | Var _ => True | Term g _ => f <> g end) ->  well_formed_cf (build f l). Proof. intros f l Af Ll Wl Al; destruct l as [ | t1 [ | t2 l]]. simpl in Ll; absurd (1 <= 0); trivial; auto with arith. apply Wl; left; trivial. rewrite build_eq_Term; [idtac | simpl; auto with arith]. apply well_formed_cf_fold; split. intros u In_u; setoid_rewrite <- in_quick_in in In_u. apply Wl; trivial. rewrite Af; split; [idtac | split]. rewrite length_quicksort; simpl; auto with arith. apply quick_sorted. intros u In_u; setoid_rewrite <- in_quick_in in In_u. apply Al; trivial. Qed. Lemma well_formed_cf_build_cons :  forall f t l, arity f = AC ->  well_formed_cf (Term f (t :: l)) -> well_formed_cf (build f l). Proof. intros f t l Af W; apply well_formed_cf_build; trivial. apply le_S_n; replace (S (length l)) with (length (t :: l)); trivial; apply well_formed_cf_length with f; trivial. intros; apply (well_formed_cf_subterms W); right; trivial. intros; apply (well_formed_cf_alien Af W); right; trivial. Qed. Lemma well_formed_cf_build_inside : forall f t l1 l2, arity f = AC ->  well_formed_cf (Term f (l1 ++ t :: l2)) -> well_formed_cf (build f (l1 ++ l2)). Proof. intros f t l1 l2 Af W; assert (H : forall u, In u (l1 ++ l2) -> In u (l1 ++ t :: l2)). intros u In_u; elim (in_app_or _ _ _ In_u); clear In_u; intro In_u; apply in_or_app; [ left | right; right ]; trivial. apply well_formed_cf_build; trivial. apply le_S_n; replace (S (length (l1 ++ l2))) with (length (l1 ++ t :: l2)). apply well_formed_cf_length with f; trivial. do 2 rewrite length_app; rewrite plus_comm; simpl; rewrite plus_comm; trivial. intros u In_u; apply (well_formed_cf_subterms W); apply H; trivial. intros u In_u; apply (well_formed_cf_alien Af W); apply H; trivial. Qed. Lemma flatten_build :  forall f l, arity f = AC ->  (forall t, In t l -> match t with | Var _ => True | Term g _ => f <> g end) ->  permut (flatten f ((build f l) :: nil)) l. Proof. intros f [ | t1 [ | t2 l]] Af Al. simpl; destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [ auto | absurd (f=f); trivial ]. assert (Al_t1 := Al _ (or_introl _ (refl_equal _))). simpl; destruct t1 as [ | g]; [auto | idtac]. destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g); trivial | auto]. simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [idtac | absurd (f=f); trivial]. rewrite <- app_nil_end; apply quick_permut_bis; auto. Qed. Lemma flatten_build_cons :  forall f t l, arity f = AC -> well_formed_cf (Term f (t :: l)) ->  permut (flatten f ((build f l) :: nil)) l. Proof. intros f t l Af W; apply flatten_build; trivial. intros; apply (well_formed_cf_alien Af W); right; trivial. Qed. Lemma flatten_build_inside :  forall f t l1 l2, arity f = AC ->  well_formed_cf (Term f (l1 ++ t :: l2)) ->  permut (flatten f ((build f (l1 ++ l2)) :: nil)) (l1 ++ l2). Proof. intros f t l1 l2 Af W; apply flatten_build; trivial. intros u In_u; apply (well_formed_cf_alien Af W); elim (in_app_or _ _ _ In_u); clear In_u; intro In_u; apply in_or_app; [left | right; right]; trivial. Qed. ```

## Substitutions modulo AC

``` Definition is_subst_canonical_form sigma sigma_cf :=   forall v, match find eq_variable_dec v sigma with     | None => find eq_variable_dec v sigma_cf = None     | Some v_sigma =>         find eq_variable_dec v sigma_cf = Some (canonical_form v_sigma)   end. Lemma is_subst_cf_is_subst_cf :   forall sigma, is_subst_canonical_form sigma (map_subst (fun _ t => canonical_form t) sigma). Proof. intros sigma; unfold is_subst_canonical_form. intro v; rewrite subst_comp_is_subst_comp_aux1. destruct (find eq_variable_dec v sigma); trivial. Qed. Definition well_formed_cf_subst sigma :=   forall v, match find eq_variable_dec v sigma with             | None => True             | Some t => well_formed_cf t             end. Lemma well_formed_cf_subst_is_well_formed_cf_subst_aux :  forall sigma, well_formed_cf_subst sigma ->  (forall v, nb_occ eq_variable_dec v sigma <= 1) ->   exists sigma', well_formed_subst sigma' /\   is_subst_canonical_form sigma' sigma. Proof. unfold well_formed_cf_subst, is_subst_canonical_form; intros sigma Wsigma Nb_occ_sigma; induction sigma as [ | [v1 t1] sigma]. exists (nil : substitution); split; trivial; intro v; simpl; trivial. elim IHsigma. intros sigma' [Wsigma' Hsigma']; assert (Wt1 : well_formed_cf t1). generalize (Wsigma v1); simpl; destruct (eq_variable_dec v1 v1) as [ _ | v1_diff_v1]; trivial; absurd (v1=v1); trivial. elim (well_formed_cf_is_well_formed_cf _ Wt1); intros u1 [Wu1 Hu1]; exists ((v1,u1)::sigma'); split; intro v; simpl; destruct (eq_variable_dec v v1) as [ _ | _ ]; trivial. apply Wsigma'. subst; trivial. apply Hsigma'. intro v; generalize (Wsigma v) (Nb_occ_sigma v); simpl; destruct (eq_variable_dec v v1) as [ v_eq_v1 | _ ]; trivial; generalize (some_nb_occ_Sn eq_variable_dec v sigma); destruct (find eq_variable_dec v sigma) as [ b | ]; trivial; intro H; generalize (H _ (refl_equal _)); clear H; intros H _ H'; destruct (nb_occ eq_variable_dec v sigma) as [ | o]; [ absurd (1 <= 0) | absurd (S(S o) <= 1) ]; auto with arith. intro v; generalize (Nb_occ_sigma v); simpl; destruct (eq_variable_dec v v1) as [ _ | _ ]; trivial; auto with arith. Qed. Lemma well_formed_cf_subst_is_well_formed_cf_subst :  forall sigma, well_formed_cf_subst sigma ->   exists sigma', well_formed_subst sigma' /\                         is_subst_canonical_form sigma' sigma. Proof. intros sigma Wsigma; elim (reduce_assoc_list eq_variable_dec sigma); intros sigma1 [Nb_occ H]; elim (well_formed_cf_subst_is_well_formed_cf_subst_aux (sigma := sigma1)); trivial. intros sigma' [Wsigma' H']; exists sigma'; split; trivial; intro v; rewrite H; apply H'. intro v; rewrite <- H; apply Wsigma. Qed. Fixpoint apply_cf_subst (sigma : substitution) (t : term) {struct t} : term :=   match t with   | Var v =>     match find eq_variable_dec v sigma with     | None => t     | Some v_sigma => v_sigma     end   | Term f l =>      let l_sigma :=        match arity f with        | AC => quicksort (flatten f (map (apply_cf_subst sigma) l))        | C => quicksort (map (apply_cf_subst sigma) l)        | Free _ => map (apply_cf_subst sigma) l      end in    Term f l_sigma  end. Lemma flatten_apply_cf_subst :  forall sigma f l, arity f = AC ->   permut (flatten f (map (apply_cf_subst sigma) l))   (flatten f (apply_cf_subst sigma (build f l) :: nil)). Proof. intros sigma f l Af; induction l as [ | t1 l]. simpl; destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [ rewrite Af; repeat rewrite quicksort_equation; simpl; auto | absurd (f=f); trivial ]. destruct l as [ | t2 l]; auto. simpl; rewrite Af; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [idtac | absurd (f = f); trivial]. rewrite <- app_nil_end; apply permut_sym; apply quick_permut_bis; transitivity (flatten f (map (apply_cf_subst sigma) (t1 :: t2 :: l))); auto; apply list_permut_flatten. apply permut_map with (@eq term). intros; subst; reflexivity. apply permut_sym; apply quick_permut. Qed. 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. intros sigma sigma_cf H t; pattern t; apply term_rec3; clear t. intro v; generalize (H v); simpl; destruct (find eq_variable_dec 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))). setoid_rewrite <- permut_app1; apply IHl. setoid_rewrite <- permut_app2. destruct t as [ v | g ll]; simpl; auto. destruct (eq_symbol_dec f g) as [ f_eq_g | f_diff_g ]. subst g; rewrite Af; do 2 rewrite <- app_nil_end; apply permut_sym; apply quick_permut. simpl; destruct (eq_symbol_dec f g) as [ f_eq_g | _ ]; auto; absurd (f=g); trivial. 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. Theorem well_formed_cf_apply_subst :   forall sigma, well_formed_cf_subst sigma ->   forall t, well_formed_cf t -> well_formed_cf (apply_cf_subst sigma t). Proof. intros sigma Wsigma t Wt; elim (well_formed_cf_is_well_formed_cf _ Wt); intros u [Wu Hu]; subst; elim (well_formed_cf_subst_is_well_formed_cf_subst Wsigma); intros tau [Wtau Htau]; rewrite apply_cf_subst_is_sound with tau sigma u; trivial; apply well_formed_cf_is_well_formed_cf_conv; exists (apply_subst tau u); split; trivial; apply well_formed_apply_subst; trivial. Qed. Lemma length_flatten_ter : forall f sigma, arity f = AC -> well_formed_cf_subst sigma ->   forall l, (forall t, In t l -> well_formed_cf t) ->   length l <= length (flatten f (map (apply_cf_subst sigma) l)). Proof. intros f sigma Af Wsigma l Wl; induction l as [ | t l]; trivial. replace (t::l) with ((t::nil) ++ l); trivial; rewrite map_app; rewrite flatten_app; do 2 rewrite length_app; apply plus_le_compat. assert (Wtsigma : well_formed_cf (apply_cf_subst sigma t)). apply well_formed_cf_apply_subst; trivial; apply Wl; left; trivial. simpl map; destruct (apply_cf_subst sigma t) as [ v | g ll ]; simpl; trivial; destruct (eq_symbol_dec f g) as [f_eq_g | _]; subst; trivial; rewrite <- app_nil_end; apply le_trans with 2; auto with arith; apply well_formed_cf_length with g; trivial. apply IHl; intros; apply Wl; right; trivial. Qed. ```

## Canonical forms and equality modulo AC

``` Lemma ac_one_step_at_top_cf_eq :   forall t1 t2, ac_one_step_at_top t1 t2 -> canonical_form t1 = canonical_form t2. Proof. assert (P12 : forall t1 t2, permut (t1 :: t2 :: nil) (t2 :: t1 :: nil)). intros t1 t2; replace (t1 :: t2 :: nil) with ((t1 :: nil) ++ (t2 :: nil)); trivial; replace (t2 :: t1 :: nil) with ((t2 :: nil) ++ (t1 :: nil)); trivial; apply list_permut_app_app. assert (Ccase : forall f, arity f = C \/ arity f = AC -> forall t1 t2, canonical_form (Term f (t1 :: t2 :: nil)) = canonical_form (Term f (t2 :: t1 :: nil))). intros f [Af | Af] t1 t2; simpl; rewrite Af; apply (f_equal (fun l => Term f l)); apply sort_is_unique; try apply quick_sorted; do 2 (apply quick_permut_bis; apply permut_sym). apply P12. destruct (canonical_form t1) as [v1 | f1 ll1]; destruct (canonical_form t2) as [v2 | f2 ll2]. apply P12. destruct (eq_symbol_dec f f2) as [_ | _]; [ setoid_rewrite <- permut_cons_inside; auto | apply P12 ]. reflexivity. destruct (eq_symbol_dec f f1) as [_ | _]; [ apply permut_sym; setoid_rewrite <- permut_cons_inside; auto | apply P12 ]. reflexivity. destruct (eq_symbol_dec f f1) as [_ | _]; destruct (eq_symbol_dec f f2) as [_ | _]. do 2 rewrite <- app_nil_end; apply list_permut_app_app. apply permut_sym; setoid_rewrite <- permut_cons_inside; auto. reflexivity. setoid_rewrite <- permut_cons_inside; auto. reflexivity. apply P12. assert (ACcase : forall f, arity f = AC -> forall t1 t2 t3, canonical_form (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil)) = canonical_form (Term f (t1 :: Term f (t2 :: t3 :: nil) :: nil))). intros f Af t1 t2 t3; simpl; rewrite Af; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [idtac | absurd (f=f); trivial]. apply (f_equal (fun l => Term f l)); apply sort_is_unique. apply quick_sorted. apply quick_sorted. do 2 (apply quick_permut_bis; apply permut_sym). generalize (canonical_form t1) (canonical_form t2) (canonical_form t3); clear t1 t2 t3; intros t1 t2 t3; rewrite <- app_nil_end. transitivity ((flatten f (t1 :: t2 :: nil)) ++ (flatten f (t3 :: nil))). setoid_rewrite <- permut_app2. apply permut_sym; apply quick_permut. transitivity ((flatten f (t1 :: nil)) ++ (flatten f (t2 :: t3 :: nil))). do 2 rewrite <- flatten_app; simpl app; apply permut_refl. destruct t1 as [v1 | g1 ll1]. simpl; setoid_rewrite <- permut_cons. reflexivity. apply quick_permut. simpl; destruct (eq_symbol_dec f g1) as [ _ | _ ]. rewrite <- app_nil_end; setoid_rewrite <- permut_app1; apply quick_permut. simpl; setoid_rewrite <- permut_cons. reflexivity. apply quick_permut. intros t1 t2 H; destruct H; auto; apply sym_eq; auto. Qed. Lemma sym_refl_ac_one_step_at_top_cf_eq :   forall t1 t2, (sym_refl ac_one_step_at_top) t1 t2 -> canonical_form t1 = canonical_form t2. Proof. intros t1 t2; unfold sym_refl; intros [H | [H | H]]. apply ac_one_step_at_top_cf_eq; trivial. apply sym_eq; apply ac_one_step_at_top_cf_eq; trivial. subst; trivial. Qed. Lemma ac_one_step_cf_eq :   forall t1 t2, one_step (sym_refl ac_one_step_at_top) t1 t2 -> canonical_form t1 = canonical_form t2. Proof. intros t1; pattern t1; apply term_rec3; clear t1. intros v1 t2 H; inversion_clear H as [H1 H2 H' | f l1 l2 H']. apply sym_refl_ac_one_step_at_top_cf_eq; apply no_need_of_instance; trivial. intros f l1 IHl1 t2 H; inversion_clear H as [ H1 H2 Hroot | H1 H2 l2 Hsub]. apply sym_refl_ac_one_step_at_top_cf_eq; apply no_need_of_instance; trivial. assert (H : map canonical_form l1 = map canonical_form l2). generalize l2 Hsub; clear l2 Hsub; induction l1 as [ | t1 l1]; intros l2 Hsub; inversion_clear Hsub. simpl; apply (f_equal (fun t => t :: map canonical_form l1)); apply IHl1; trivial; left; trivial. simpl; apply (f_equal (fun l => canonical_form t1 :: l)); apply IHl0; trivial; intros; apply IHl1; trivial; right; trivial. simpl; rewrite H; trivial. Qed. Theorem ac_cf_eq :   forall t1 t2, ac t1 t2 -> canonical_form t1 = canonical_form t2. Proof. unfold ac, th_eq; intros t1 t2 H. refine (rwr_inv _ _ _ _ (@trans_eq term) _ _ _ H). clear t1 t2 H; intros t1 t2 H; apply ac_one_step_cf_eq; trivial. Qed. Lemma ac_one_step_at_top_size_eq :   forall t1 t2, ac_one_step_at_top t1 t2 -> size t1 = size t2. Proof. intros t1 t2 H; destruct H; simpl; repeat rewrite plus_0_r; auto with arith; rewrite (plus_comm (size t1) (S (size t2 + size t3))); simpl; apply (f_equal (fun n => S (S n))); rewrite <- (plus_assoc (size t1) (size t2) (size t3)); apply plus_comm. Qed. Lemma sym_refl_ac_one_step_at_top_size_eq :   forall t1 t2, (sym_refl ac_one_step_at_top) t1 t2 -> size t1 = size t2. Proof. intros t1 t2; unfold sym_refl; intros [H | [H | H]]. apply ac_one_step_at_top_size_eq; trivial. apply sym_eq; apply ac_one_step_at_top_size_eq; trivial. subst; trivial. Qed. Lemma ac_one_step_size_eq :   forall t1 t2, one_step (sym_refl ac_one_step_at_top) t1 t2 -> size t1 = size t2. Proof. intros t1; pattern t1; apply term_rec3; clear t1. intros v1 t2 H; inversion_clear H as [H1 H2 H' | f l1 l2 H']. apply sym_refl_ac_one_step_at_top_size_eq; apply no_need_of_instance; trivial. intros f l1 IHl1 t2 H; inversion_clear H as [ H1 H2 Hroot | H1 H2 l2 Hsub]. apply sym_refl_ac_one_step_at_top_size_eq; apply no_need_of_instance; trivial. assert (H : list_size size l1 = list_size size l2). generalize l2 Hsub; clear l2 Hsub; induction l1 as [ | t1 l1]; intros l2 Hsub; inversion_clear Hsub. simpl; apply (f_equal (fun n => n + list_size size l1)); apply IHl1; trivial; left; trivial. simpl; apply (f_equal (fun n => size t1 + n)); apply IHl0; trivial; intros; apply IHl1; trivial; right; trivial. do 2 rewrite size_unfold; rewrite H; trivial. Qed. Lemma ac_size_eq :   forall t1 t2, ac t1 t2 -> size t1 = size t2. Proof. intros t1 t2 H; refine (rwr_inv _ _ _ _ (@trans_eq nat) _ _ _ H). intros; apply ac_one_step_size_eq; trivial. Qed. Fixpoint ac_size (t:term) : nat :=   match t with   | Var v => 1   | Term f l =>        let ac_size_list :=          (fix ac_size_list (l : list term) {struct l} : nat :=             match l with             | nil => 0             | t :: lt => ac_size t + ac_size_list lt             end) in      (match arity f with       | AC => (length l) - 1       | C => 1       | Free _ => 1       end) + ac_size_list l    end. Lemma ac_size_unfold :   forall t,   ac_size t = match t with               | Var _ => 1               | Term f l =>                 (match arity f with                 | AC => (length l) - 1                 | C => 1                 | Free _ => 1                 end) + list_size ac_size l                end. Proof. intro t; destruct t as [v | f l]; trivial; simpl. apply (f_equal (fun n => (match arity f with                                         | AC => length l - 1                                         | C => 1                                         | Free _ => 1                                         end) + n)); induction l as [ | t l]; trivial. simpl; rewrite <- IHl; generalize (ac_size t); clear f t IHl; induction l as [ | t l]; simpl; trivial; intro n; rewrite (IHl (n + ac_size t)); rewrite (IHl (ac_size t)); auto with arith. Qed. Lemma size_size_aux2 :  forall f t, arity f = AC -> well_formed t ->  ac_size (canonical_form t) =  list_size ac_size (flatten f (canonical_form t :: nil)) +  (length (flatten f (canonical_form t :: nil))) - 1. Proof. intros f t Af Wt; assert (Wu : well_formed_cf (canonical_form t)). apply well_formed_cf_is_well_formed_cf_conv; exists t; split; trivial. generalize (canonical_form t) Wu; clear t Wt Wu; intros u Wu. destruct u as [v | g l]; trivial; simpl. destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]. subst g; rewrite Af; rewrite <- app_nil_end; generalize (well_formed_cf_length Af Wu); intro Ll; destruct (length l) as [ | n]. absurd (2 <= 0); auto with arith. rewrite (plus_comm (list_size ac_size l)); simpl; do 2 rewrite <- minus_n_O; trivial. simpl; rewrite (list_size_fold ac_size); trivial. simpl; rewrite plus_0_r; apply sym_eq; rewrite plus_comm; simpl; rewrite <- minus_n_O; trivial. Qed. Lemma size_size_aux3 :  forall f t, arity f = AC -> well_formed t ->  1 <= length (A:=term) (flatten f (canonical_form t :: nil)). Proof. intros f t Ar Wt; apply (length_flatten (t :: nil) Ar); intros u In_u; elim In_u; clear In_u; intro In_u. subst u; trivial. contradiction. Qed. Lemma size_size :  forall t, well_formed t -> size t = ac_size (canonical_form t). Proof. intros t; pattern t; apply term_rec3; clear t. intros v _; trivial. intros f l H Wt; destruct (well_formed_unfold _ Wt) as [Wl Ll]. assert (Hl : forall t, In t l -> size t = ac_size (canonical_form t)). intros; apply H; trivial; apply Wl; trivial. clear H Wt; assert (Hl' : list_size size l = list_size ac_size (map canonical_form l)). clear Ll; induction l as [ | t l]; trivial. simpl; rewrite (Hl t (or_introl _ (refl_equal _))); rewrite IHl; trivial. intros; apply Wl; right; trivial. intros; apply Hl; right; trivial. simpl; rewrite (list_size_fold size); rewrite (list_size_fold ac_size); destruct_arity f n Af. assert (Dummy : DOS.A = term). apply refl_equal. rewrite length_quicksort. assert (Dummy2 : forall l, @length DOS.A l = @length term l). intro k; apply refl_equal. rewrite Dummy2. replace (list_size ac_size (quicksort (flatten f (map canonical_form l)))) with (list_size ac_size (flatten f (map canonical_form l))). destruct l as [ | t1 [ | t2 [ | t3 l]]]; [absurd (0 = 2) | absurd (1 = 2) | idtac | absurd (S(S(S(length l))) = 2)]; auto with arith. simpl map; simpl list_size; rewrite plus_0_r; rewrite (Hl t1 (or_introl _ (refl_equal _))); rewrite (Hl t2 (or_intror _ (or_introl _ (refl_equal _)))). assert (W1 : well_formed_cf (canonical_form t1)). apply well_formed_cf_is_well_formed_cf_conv; exists t1; split; trivial; apply Wl; left; trivial. assert (W2 : well_formed_cf (canonical_form t2)). apply well_formed_cf_is_well_formed_cf_conv; exists t2; split; trivial; apply Wl; right; left; trivial. destruct (canonical_form t1) as [v1 | f1 ll1]; destruct (canonical_form t2) as [v2 | f2 ll2]; trivial. simpl flatten; destruct (eq_symbol_dec f f2) as [f_eq_f2 | f_diff_f2]. simpl; rewrite <- app_nil_end; simpl; subst f2; rewrite Af. rewrite (list_size_fold ac_size); rewrite <- minus_n_O. generalize (well_formed_cf_length Af W2). intro Lll2; destruct (length ll2) as [ | n2]. absurd (2 <= 0); auto with arith. simpl; rewrite <- minus_n_O; apply sym_eq; rewrite plus_comm; simpl; rewrite plus_comm; trivial. simpl; rewrite plus_0_r; trivial. simpl flatten; destruct (eq_symbol_dec f f1) as [f_eq_f1 | f_diff_f1]. simpl; subst f1; rewrite Af; rewrite (list_size_fold ac_size). generalize (well_formed_cf_length Af W1); intro Lll1; rewrite length_app; destruct (length ll1) as [ | n1]. absurd (2 <= 0); auto with arith. rewrite list_size_app; simpl; do 2 rewrite <- minus_n_O; rewrite (plus_comm n1 1); simpl; rewrite plus_assoc; trivial. trivial. replace (flatten f (Term f1 ll1 :: Term f2 ll2 :: nil)) with    ((flatten f (Term f1 ll1 :: nil)) ++ (flatten f (Term f2 ll2 :: nil))). rewrite length_app. simpl; destruct (eq_symbol_dec f f1) as [f_eq_f1 | f_diff_f1]; destruct (eq_symbol_dec f f2) as [f_eq_f2 | f_diff_f2]. do 2 rewrite <- app_nil_end; subst f1 f2; rewrite Af; do 2 rewrite (list_size_fold ac_size); rewrite list_size_app. unfold DOS.A in *; generalize (well_formed_cf_length Af W1); intro Lll1; destruct (length ll1) as [ | n1]. absurd (2 <= 0); auto with arith. unfold DOS.A in *; generalize (well_formed_cf_length Af W2); intro Lll2; destruct (length ll2) as [ | n2]. absurd (2 <= 0); auto with arith. simpl; do 3 rewrite <- minus_n_O; rewrite (plus_comm n1 (S n2)); simpl; rewrite (plus_comm n2 n1); do 2 rewrite <- plus_assoc; apply (f_equal (fun n => S (n1 + n))); rewrite plus_comm; rewrite <- plus_assoc; apply (f_equal (fun n => n2 + n)); apply plus_comm. subst f1; rewrite Af; rewrite <- app_nil_end; rewrite list_size_app; simpl; do 2 rewrite (list_size_fold ac_size); simpl; rewrite plus_0_r; rewrite (plus_comm (length ll1) 1); simpl; rewrite <- minus_n_O; unfold DOS.A in *; generalize (well_formed_cf_length Af W1); intro Lll1; destruct (length ll1) as [ | n1]. absurd (2 <= 0); auto with arith. simpl; rewrite <- minus_n_O; rewrite <- plus_assoc; trivial. subst f2; rewrite Af; rewrite <- app_nil_end. do 2 rewrite (list_size_fold ac_size). unfold DOS.A in *; generalize (well_formed_cf_length Af W2); intro Lll2; destruct (length ll2) as [ | n2]. absurd (2 <= 0); auto with arith. simpl minus; rewrite <- minus_n_O; simpl plus; do 3 rewrite plus_assoc; apply (f_equal (fun n => S (n + list_size ac_size ll2))). rewrite plus_comm; rewrite plus_assoc; rewrite (list_size_fold ac_size); trivial. simpl; rewrite plus_0_r; trivial. rewrite <- flatten_app; simpl app; trivial. apply permut_size with (@eq term). intros; subst; trivial. apply quick_permut. rewrite Hl'; simpl; apply (f_equal S). apply permut_size with (@eq term). intros; subst; trivial. apply quick_permut. rewrite Hl'; simpl; trivial. Qed. Lemma ac_size_ge_one :   forall t, well_formed_cf t -> 1 <= ac_size t. Proof. intros t Wt; elim (well_formed_cf_is_well_formed_cf _ Wt); intros u [Wu Hu]; subst; rewrite <- size_size; trivial; apply size_ge_one. Qed. End Make. ```