Library ac_matching.cf_eq_ac
Add LoadPath "basis".
Add LoadPath "list_extensions".
Add LoadPath "term_algebra".
Add LoadPath "term_orderings".
Require Import Arith.
Require Import List.
Require Import closure.
Require Import more_list.
Require Import list_sort.
Require Import term.
Require Import ac.
Set Implicit Arguments.
Module Type S.
Declare Module Import Ac : ac.S.
Import Ac.EqTh.T.
Axiom cf_eq_ac :
forall t1 t2, well_formed t1 -> well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2.
End S.
Module Make (Ac1 : ac.S) <: S with Module Ac := Ac1.
Module Import Ac := Ac1.
Import EqTh.
Import Sort.
Import LPermut.
Import T.
Import F.
Import X.
Lemma split_cf :
forall f, arity f = AC -> forall t u1 u2, well_formed t ->
permut (flatten f (canonical_form t :: nil)) (u1 ++ u2) ->
u1 = nil \/
u2 = nil \/
(exists t1, exists t2,
well_formed t1 /\ well_formed t2 /\
ac t (Term f (t1 :: t2 :: nil)) /\
permut (flatten f (canonical_form t1 :: nil)) u1 /\
permut (flatten f (canonical_form t2 :: nil)) u2).
Proof.
intros f Af t; pattern t; apply term_rec3; clear t.
intros v l1 l2 _ P; simpl in P;
destruct l1 as [ | t1 l1]; [left; trivial | idtac];
destruct l2 as [ | t2 l2]; [right; left; trivial | idtac];
generalize (list_permut.permut_length P); rewrite length_app; simpl;
rewrite plus_comm; intro; discriminate.
intros g l IHl l1 l2 Wt P'; simpl in P';
destruct (eq_symbol_dec f g) as [f_eq_s | f_diff_g].
subst; rewrite Af in P'; rewrite <- app_nil_end in P'.
assert (P : permut (flatten g (map canonical_form l)) (l1 ++ l2)).
setoid_rewrite <- P'; apply quick_permut.
clear P'; elim (well_formed_unfold _ Wt); rewrite Af; intros Wl Ll;
destruct l as [ | t1 l]; [absurd (0=2); auto with arith | idtac];
destruct l as [ | t2 l]; [absurd (1=2); auto with arith | idtac];
destruct l as [ | t3 l]; [idtac | absurd (S(S(S(length l)))=2); auto with arith];
replace (map canonical_form (t1 :: t2 :: nil)) with
((canonical_form t1 :: nil) ++ canonical_form t2 :: nil) in P; trivial;
rewrite flatten_app in P;
assert (Wt1 := Wl t1 (or_introl _ (refl_equal t1)));
assert (Wt2 := Wl t2 (or_intror _ (or_introl _ (refl_equal t2))));
elim (ac_syntactic _ _ _ _ P); intros k1 [k2 [k3 [k4 [P2 [P1 [P3 P4]]]]]].
generalize (IHl t1 (or_introl _ (refl_equal _)) k3 k4 Wt1 P1);
intros [Hk3 | [Hk4 | [t11 [t12 [Wt11 [Wt12 [H1 [Q11 Q12]]]]]]]];
generalize (IHl t2 (or_intror _ (or_introl _ (refl_equal _))) k1 k2 Wt2 P2);
intros [Hk1 | [Hk2 | [t21 [t22 [Wt21 [Wt22 [H2 [Q21 Q22]]]]]]]].
subst; right; left; apply list_permut.permut_nil with term (@eq term); trivial.
subst; right; right; exists t1; exists t2; intuition.
unfold ac; apply th_refl.
setoid_rewrite P1; apply permut_sym; trivial.
setoid_rewrite P3; trivial.
subst; right; right; exists (Term g (t1 :: t22 :: nil)); exists t21; intuition.
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t1 | [u_eq_t2 | In_u_nil]]; subst; trivial; contradiction.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term g (t1 :: (Term g (t21 :: t22 :: nil) :: nil))).
apply general_context; simpl; right; left; split; trivial.
left; split; simpl; trivial.
apply trans_clos_is_trans with (Term g (t1 :: Term g (t22 :: t21 :: nil) :: nil)).
apply general_context; simpl; right; left; trivial.
split; simpl; trivial; left; split; trivial.
apply comm; right; trivial.
apply r_assoc; trivial.
setoid_rewrite P4; setoid_rewrite <- P1; setoid_rewrite <- Q22;
rewrite <- flatten_app;
transitivity (flatten g ((canonical_form t1 :: nil) ++ canonical_form t22 :: nil)).
simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g];
[idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end;
apply quick_permut_bis; apply permut_refl.
apply list_permut_flatten; apply list_permut_app_app.
setoid_rewrite P3; rewrite <- app_nil_end; trivial.
right; right; exists t2; exists t1; subst; intuition.
apply comm; right; trivial.
setoid_rewrite P4; setoid_rewrite P2; rewrite <- app_nil_end; apply permut_refl.
setoid_rewrite P1; setoid_rewrite P3; rewrite <- app_nil_end; apply permut_refl.
subst; left; apply list_permut.permut_nil with term (@eq term); trivial.
subst; right; right; exists t22; exists (Term g (t1 :: t21 :: nil)); intuition.
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t1 | [u_eq_t21 | In_u_nil]]; subst; trivial; contradiction.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term g (t1 :: (Term g (t21 :: t22 :: nil) :: nil))).
apply general_context; simpl; right; left; split; trivial.
left; split; simpl; trivial.
apply trans_clos_is_trans with (Term g (Term g (t1 :: t21 :: nil) :: t22 :: nil)).
apply r_assoc; trivial.
apply comm; right; trivial.
setoid_rewrite P4; setoid_rewrite <- Q22; rewrite <- app_nil_end; auto.
transitivity (flatten g ((canonical_form t1 :: nil) ++ canonical_form t21 :: nil)).
simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g];
[idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end;
apply quick_permut_bis; apply permut_refl.
setoid_rewrite P3;
rewrite <- app_nil_end in P1; setoid_rewrite <- P1;
setoid_rewrite <- Q21;
rewrite flatten_app; apply list_permut_app_app.
subst; right; right; exists (Term g (t12 :: t2 :: nil)); exists t11; intuition.
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t12 | [u_eq_t2 | In_u_nil]]; subst; trivial; contradiction.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term g (Term g (t11 :: t12 :: nil) :: t2 :: nil)).
apply general_context; simpl; left; split; trivial.
apply trans_clos_is_trans with (Term g (t11 :: (Term g (t12 :: t2 :: nil)) :: nil)).
apply l_assoc; trivial.
apply comm; right; trivial.
setoid_rewrite P4; setoid_rewrite <- P2; setoid_rewrite <- Q12;
transitivity (flatten g ((canonical_form t12 :: nil) ++ canonical_form t2 :: nil)).
simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g];
[idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end;
apply quick_permut_bis; apply permut_refl.
rewrite flatten_app; apply list_permut_app_app.
setoid_rewrite P3; trivial.
subst; right; right; exists t12; exists (Term g (t11 :: t2 :: nil)); intuition.
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t11 | [u_eq_t2 | In_u_nil]]; subst; trivial; contradiction.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term g (Term g (t11 :: t12 :: nil) :: t2 :: nil)).
apply general_context; simpl; left; split; trivial.
apply trans_clos_is_trans with (Term g (Term g (t12 :: t11 :: nil) :: t2 :: nil)).
apply general_context; simpl; left; split; trivial; apply comm; right; trivial.
apply l_assoc; trivial.
setoid_rewrite P4; auto.
setoid_rewrite P3;
rewrite <- app_nil_end in P2; setoid_rewrite <- P2;
setoid_rewrite <- Q11;
transitivity (flatten g ((canonical_form t11 :: nil) ++ canonical_form t2 :: nil)).
simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g];
[idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end;
apply quick_permut_bis; apply permut_refl.
rewrite flatten_app; apply list_permut_app_app.
right; right; exists (Term g (t12 :: t22 :: nil)); exists (Term g (t11 :: t21 :: nil));
intuition.
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t12 | [u_eq_t22 | In_u_nil]]; subst; trivial; contradiction.
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t11 | [u_eq_t21 | In_u_nil]]; subst; trivial; contradiction.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with
(Term g (Term g (t11 :: t12 :: nil) :: (Term g (t21 :: t22 :: nil)) :: nil)).
apply general_context; simpl; right; right; split; trivial.
left; split; trivial.
apply trans_clos_is_trans with
(Term g (t11 :: (Term g (t12 :: (Term g (t21 :: t22 :: nil)) :: nil)) :: nil)).
apply l_assoc; trivial.
apply trans_clos_is_trans with
(Term g (t11 :: (Term g (Term g (t12 :: t21 :: nil) :: t22 :: nil)) :: nil)).
apply general_context; simpl; right; left; split; trivial.
left; split; trivial.
apply r_assoc; trivial.
apply trans_clos_is_trans with
(Term g (t11 :: (Term g (Term g (t21 :: t12 :: nil) :: t22 :: nil)) :: nil)).
apply general_context; simpl; right; left; split; trivial.
left; split; trivial.
apply general_context; simpl; left; split; trivial.
apply comm; trivial; right; trivial.
apply trans_clos_is_trans with
(Term g (t11 :: (Term g (t21 :: (Term g (t12 :: t22 :: nil)) :: nil)) :: nil)).
apply general_context; simpl; right; left; split; trivial.
left; split; trivial.
apply l_assoc; trivial.
apply trans_clos_is_trans with
(Term g (Term g (t11:: t21 :: nil) :: Term g (t12 :: t22 :: nil) :: nil)).
apply r_assoc; trivial.
apply comm; right; trivial.
setoid_rewrite P4; setoid_rewrite <- Q12; setoid_rewrite <- Q22.
transitivity (flatten g (canonical_form t12 :: nil) ++ flatten g (canonical_form t22 :: nil)).
rewrite <- flatten_app;
simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g];
[idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end;
apply quick_permut_bis; apply permut_refl.
apply list_permut_app_app.
setoid_rewrite P3; setoid_rewrite <- Q11; setoid_rewrite <- Q21.
transitivity (flatten g (canonical_form t11 :: nil) ++ flatten g (canonical_form t21 :: nil)).
rewrite <- flatten_app;
simpl; destruct (eq_symbol_dec g g) as [ _ | g_diff_g];
[idtac | absurd (g=g); trivial]; rewrite Af; rewrite <- app_nil_end;
apply quick_permut_bis; apply permut_refl.
apply list_permut_app_app.
assert ( Ll := list_permut.permut_length P'); clear P';
destruct l1 as [ | t1 l1]; [left; trivial | idtac];
destruct l2 as [ | t2 l2]; [right; left; trivial | idtac];
rewrite length_app in Ll; simpl in Ll; rewrite plus_comm in Ll; simpl in Ll;
discriminate.
Qed.
Lemma syntactic_dec :
forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->
well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2) ->
forall f, arity f = AC -> forall a1 a2 a3 a4,
size a1 <= n -> well_formed a1 ->
size a2 <= n -> well_formed a2 ->
well_formed a3 -> well_formed a4 ->
forall k1 k4,
permut (flatten f (canonical_form a1 :: nil)) k1 ->
permut (flatten f (canonical_form a2 :: nil)) k4 ->
permut (flatten f (canonical_form a3 :: nil)) k1->
permut (flatten f (canonical_form a4 :: nil)) k4 ->
ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil)).
Proof.
intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Wa3 Wa4
k1 k4 P1 P2 P3 P4;
unfold ac, th_eq; apply general_context; simpl.
right; right; split.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P1; setoid_rewrite P3; auto.
left; split; trivial.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P2; setoid_rewrite P4; auto.
Qed.
Lemma commutativity :
forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->
well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2) ->
forall f, arity f = AC -> forall a1 a2 a3 a4,
size a1 <= n -> well_formed a1 ->
size a2 <= n -> well_formed a2 ->
well_formed a3 -> well_formed a4 ->
forall k2 k3,
permut (flatten f (canonical_form a1 :: nil)) k2 ->
permut (flatten f (canonical_form a2 :: nil)) k3 ->
permut (flatten f (canonical_form a3 :: nil)) k3 ->
permut (flatten f (canonical_form a4 :: nil)) k2 ->
ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil)).
Proof.
intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Wa3 Wa4
k2 k3 P1 P2 P3 P4;
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f (a2 :: a1 :: nil)).
apply comm; right; trivial.
apply general_context; simpl; right; right; split.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P2; setoid_rewrite P3; auto.
left; split; trivial.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P1; setoid_rewrite P4; auto.
Qed.
Lemma associativity :
forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->
well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2) ->
forall f, arity f = AC -> forall a1 a2 a3 a4,
size a1 <= n -> well_formed a1 ->
size a2 <= n -> well_formed a2 ->
size a3 <= n -> well_formed a3 ->
size a4 <= n -> well_formed a4 ->
forall k1 k2 k4, k1 = nil \/ k2 = nil \/ k4 = nil \/
(permut (flatten f (canonical_form a1 :: nil)) (k1 ++ k2) ->
permut (flatten f (canonical_form a2 :: nil)) k4 ->
permut (flatten f (canonical_form a3 :: nil)) k1 ->
permut (flatten f (canonical_form a4 :: nil)) (k2 ++ k4) ->
ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))).
Proof.
intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k1 k2 k4.
destruct k1 as [ | h1 k1]; [left; trivial | right];
destruct k2 as [ | h2 k2]; [left; trivial | right];
destruct k4 as [ | h4 k4]; [left; trivial | right]; intros P1 P2 P3 P4;
generalize (split_cf Af _ _ _ Wa1 P1);
intros [Hk1 | [Hk2 | [t1 [t2 [Wt1 [Wt2 [H1 [Q1 Q2]]]]]]]];
generalize (split_cf Af _ _ _ Wa4 P4);
intros [Hk2' | [Hk4 | [t2' [t4 [Wt2' [Wt4 [H2 [Q2' Q4]]]]]]]];
subst; try discriminate.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f ((Term f (t1 :: t2 :: nil)) :: t4 :: nil)).
apply general_context; simpl; right; right; split; trivial.
left; split; trivial.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P2; setoid_rewrite Q4; auto.
apply trans_clos_is_trans with (Term f (t1 :: (Term f (t2 :: t4 :: nil)) :: nil)).
apply l_assoc; trivial.
assert (Wt24 : well_formed (Term f (t2 :: t4 :: nil))).
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t2 | [u_eq_t4 | In_u_nil]]; subst; trivial; contradiction.
apply th_sym; unfold th_eq;
apply general_context; simpl; right; right; split.
apply IH; trivial; apply flatten_cf_cf with f; trivial.
setoid_rewrite P3; setoid_rewrite Q1; auto.
left; split; trivial.
apply IH; trivial; apply flatten_cf_cf with f; trivial.
setoid_rewrite P4; setoid_rewrite <- Q2; setoid_rewrite <- Q4.
rewrite <- flatten_app; simpl;
destruct (eq_symbol_dec f f) as [ _ | f_diff_f];
[rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial];
apply quick_permut.
Qed.
Lemma swap_left :
forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->
well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2) ->
forall f, arity f = AC -> forall a1 a2 a3 a4,
size a1 <= n -> well_formed a1 ->
size a2 <= n -> well_formed a2 ->
size a3 <= n -> well_formed a3 ->
size a4 <= n -> well_formed a4 ->
forall k2 k3 k4, k2 = nil \/ k3 = nil \/ k4 = nil \/
(permut (flatten f (canonical_form a1 :: nil)) k2 ->
permut (flatten f (canonical_form a2 :: nil)) (k3 ++ k4) ->
permut (flatten f (canonical_form a3 :: nil)) k3 ->
permut (flatten f (canonical_form a4 :: nil)) (k2 ++ k4) ->
ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))).
Proof.
intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k2 k3 k4.
destruct k2 as [ | h2 k2]; [left; trivial | right];
destruct k3 as [ | h3 k3]; [left; trivial | right];
destruct k4 as [ | h4 k4]; [left; trivial | right]; intros P1 P2 P3 P4;
generalize (split_cf Af _ _ _ Wa2 P2);
intros [Hk1 | [Hk2 | [t3 [t4 [Wt3 [Wt4 [H2 [Q3 Q4]]]]]]]];
generalize (split_cf Af _ _ _ Wa4 P4);
intros [Hk2' | [Hk4 | [t2' [t4' [Wt2' [Wt4' [H4 [Q2' Q4']]]]]]]];
subst; try discriminate.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f (t2' :: (Term f (t3 :: t4 :: nil)) :: nil)).
apply general_context; simpl; right; right; split.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P1; setoid_rewrite Q2'; auto.
left; split; trivial.
apply trans_clos_is_trans with (Term f ((Term f (t2' :: t3 :: nil)) :: t4 :: nil)).
apply r_assoc; trivial.
apply trans_clos_is_trans with (Term f ((Term f (t3 :: t2' :: nil)) :: t4 :: nil)).
apply general_context; simpl; left; split; trivial.
apply comm; trivial; right; trivial.
apply trans_clos_is_trans with (Term f (t3 :: (Term f (t2' :: t4 :: nil)) :: nil)).
apply l_assoc; trivial.
assert (Wt24 : well_formed (Term f (t2' :: t4 :: nil))).
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t2' | [u_eq_t4 | In_u_nil]]; subst; trivial; contradiction.
apply th_sym; unfold th_eq; apply general_context; simpl; right; right; split.
apply IH; trivial; apply flatten_cf_cf with f; trivial.
setoid_rewrite P3; setoid_rewrite Q3; auto.
left; split; trivial; apply IH; trivial; apply flatten_cf_cf with f; trivial.
setoid_rewrite P4; setoid_rewrite <- Q2'; setoid_rewrite <- Q4;
rewrite <- flatten_app; simpl;
destruct (eq_symbol_dec f f) as [ _ | f_diff_f];
[rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial];
apply quick_permut.
Qed.
Lemma swap_right :
forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->
well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2) ->
forall f, arity f = AC -> forall a1 a2 a3 a4,
size a1 <= n -> well_formed a1 ->
size a2 <= n -> well_formed a2 ->
size a3 <= n -> well_formed a3 ->
size a4 <= n -> well_formed a4 ->
forall k1 k2 k3, k1 = nil \/ k2 = nil \/ k3 = nil \/
(permut (flatten f (canonical_form a1 :: nil)) (k1 ++ k2) ->
permut (flatten f (canonical_form a2 :: nil)) k3 ->
permut (flatten f (canonical_form a3 :: nil)) (k1 ++ k3) ->
permut (flatten f (canonical_form a4 :: nil)) k2 ->
ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))).
Proof.
intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k1 k2 k3.
destruct k1 as [ | h1 k1]; [left; trivial | right];
destruct k2 as [ | h2 k2]; [left; trivial | right];
destruct k3 as [ | h3 k3]; [left; trivial | right]; intros P1 P2 P3 P4;
generalize (split_cf Af _ _ _ Wa1 P1);
intros [Hk1 | [Hk2 | [t1 [t2 [Wt1 [Wt2 [H1 [Q1 Q2]]]]]]]];
generalize (split_cf Af _ _ _ Wa3 P3);
intros [Hk1' | [Hk3 | [t1' [t3 [Wt1' [Wt3 [H3 [Q1' Q3]]]]]]]];
subst; try discriminate.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f ((Term f (t1 :: t2 :: nil)) :: t3 :: nil)).
apply general_context; simpl; right; right; split; trivial.
left; split; trivial.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P2; setoid_rewrite Q3; auto.
apply trans_clos_is_trans with (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil)).
apply l_assoc; trivial.
apply trans_clos_is_trans with (Term f (t1 :: (Term f (t3 :: t2 :: nil)) :: nil)).
apply general_context; simpl; right; left; split; trivial.
left; split; trivial; apply comm; right; trivial.
apply trans_clos_is_trans with (Term f ((Term f (t1 :: t3 :: nil)) :: t2 :: nil)).
apply r_assoc; trivial.
assert (Wt13 : well_formed (Term f (t1 :: t3 :: nil))).
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t1 | [u_eq_t3 | In_u_nil]]; subst; trivial; contradiction.
apply th_sym; unfold th_eq; apply general_context; simpl; right; right; split.
apply IH; trivial; apply flatten_cf_cf with f; trivial.
setoid_rewrite P3; setoid_rewrite <- Q1; setoid_rewrite <- Q3.
rewrite <- flatten_app; simpl;
destruct (eq_symbol_dec f f) as [ _ | f_diff_f];
[rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial];
apply quick_permut.
left; split; trivial.
apply IH; trivial; apply flatten_cf_cf with f; trivial.
setoid_rewrite P4; setoid_rewrite Q2; auto.
Qed.
Lemma middle_commutativity :
forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 ->
well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2) ->
forall f, arity f = AC -> forall a1 a2 a3 a4,
size a1 <= n -> well_formed a1 ->
size a2 <= n -> well_formed a2 ->
size a3 <= n -> well_formed a3 ->
size a4 <= n -> well_formed a4 ->
forall k1 k2 k3 k4, k1 = nil \/ k2 = nil \/ k3 = nil \/ k4 = nil \/
(permut (flatten f (canonical_form a1 :: nil)) (k1 ++ k2) ->
permut (flatten f (canonical_form a2 :: nil)) (k3 ++ k4) ->
permut (flatten f (canonical_form a3 :: nil)) (k1 ++ k3) ->
permut (flatten f (canonical_form a4 :: nil)) (k2 ++ k4) ->
ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil))).
Proof.
intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 k1 k2 k3 k4.
destruct k1 as [ | h1 k1]; [left; trivial | right];
destruct k2 as [ | h2 k2]; [left; trivial | right];
destruct k3 as [ | h3 k3]; [left; trivial | right];
destruct k4 as [ | h4 k4]; [left; trivial | right]; intros P1 P2 P3 P4;
generalize (split_cf Af _ _ _ Wa1 P1);
intros [Hk1 | [Hk2 | [t1 [t2 [Wt1 [Wt2 [H1 [Q1 Q2]]]]]]]];
generalize (split_cf Af _ _ _ Wa2 P2);
intros [Hk3 | [Hk4 | [t3 [t4 [Wt3 [Wt4 [H2 [Q3 Q4]]]]]]]];
generalize (split_cf Af _ _ _ Wa3 P3);
intros [Hk1' | [Hk3' | [t1' [t3' [Wt1' [Wt3' [H3 [Q1' Q3']]]]]]]];
generalize (split_cf Af _ _ _ Wa4 P4);
intros [Hk2' | [Hk4' | [t2' [t4' [Wt2' [Wt4' [H4 [Q2' Q4']]]]]]]];
subst; try discriminate.
unfold ac, th_eq, rwr; apply trans_clos_is_trans with
(Term f ((Term f (t1 :: t2 :: nil)) :: (Term f (t3 :: t4 :: nil)) :: nil)).
apply general_context; simpl; right; right; split; trivial.
left; split; trivial.
apply trans_clos_is_trans with
(Term f (t1 :: (Term f (t2 :: (Term f (t3 :: t4 :: nil)) :: nil)) :: nil)).
apply l_assoc; trivial.
apply trans_clos_is_trans with
(Term f (t1 :: (Term f ((Term f (t2 :: t3 :: nil)) :: t4 :: nil)) :: nil)).
apply general_context; simpl; right; left; split; trivial.
left; split; trivial.
apply r_assoc; trivial.
apply trans_clos_is_trans with
(Term f (t1 :: (Term f ((Term f (t3 :: t2 :: nil)) :: t4 :: nil)) :: nil)).
apply general_context; simpl; right; left; split; trivial.
left; split; trivial.
apply general_context; simpl; left; split; trivial.
apply comm; right; trivial.
apply trans_clos_is_trans with
(Term f (t1 :: (Term f (t3 :: (Term f (t2 :: t4 :: nil)) :: nil)) :: nil)).
apply general_context; simpl; right; left; split; trivial.
left; split; trivial.
apply l_assoc; trivial.
apply trans_clos_is_trans with
(Term f ((Term f (t1 :: t3 :: nil)) :: (Term f (t2 :: t4 :: nil)) :: nil)).
apply r_assoc; trivial.
apply th_sym; unfold th_eq; apply general_context; simpl; right; right; split.
assert (Wt13 : well_formed (Term f (t1 :: t3 :: nil))).
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t1 | [u_eq_t3 | In_u_nil]]; subst; trivial; contradiction.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P3; setoid_rewrite <- Q1; setoid_rewrite <- Q3.
rewrite <- flatten_app; simpl;
destruct (eq_symbol_dec f f) as [ _ | f_diff_f];
[rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial];
apply quick_permut.
assert (Wt24 : well_formed (Term f (t2 :: t4 :: nil))).
apply well_formed_fold; rewrite Af; split; trivial;
intros u [u_eq_t2 | [u_eq_t4 | In_u_nil]]; subst; trivial; contradiction.
left; split; trivial.
apply IH; trivial; apply flatten_cf_cf with f; trivial;
setoid_rewrite P4; setoid_rewrite <- Q2; setoid_rewrite <- Q4.
rewrite <- flatten_app; simpl;
destruct (eq_symbol_dec f f) as [ _ | f_diff_f];
[rewrite Af; rewrite <- app_nil_end | absurd (f=f); trivial];
apply quick_permut.
Qed.
Add Morphism (length (A:=term))
with signature permut ==> (@eq nat)
as length_morph.
Proof.
apply list_permut.permut_length.
Qed.
Theorem cf_eq_ac :
forall t1 t2, well_formed t1 -> well_formed t2 ->
canonical_form t1 = canonical_form t2 -> ac t1 t2.
Proof.
intro t1; pattern t1; apply term_rec2; clear t1; induction n as [ | n].
intros t1 St1; absurd (1 <= 0); auto with arith;
apply le_trans with (size t1); trivial; apply size_ge_one.
intros [v1 | f1 l1] St1 [v2 | f l2] Wt1 Wt2 H;
[simpl in H; rewrite H; unfold ac; apply th_refl | discriminate | discriminate | idtac].
assert (St2 : size (Term f l2) <= S n).
rewrite size_size; trivial; rewrite <- H; rewrite <- size_size; trivial.
simpl in H; injection H; clear H;
intros H f1_eq_f; subst f1; destruct_arity f m Af.
generalize (well_formed_unfold _ Wt1); rewrite Af; intros [Wl1 Ll1];
generalize (well_formed_unfold _ Wt2); rewrite Af; intros [Wl2 Ll2];
destruct l1 as [ | a1 l1]; [absurd (0=2); auto with arith | idtac];
destruct l1 as [ | a2 l1]; [absurd (1=2); auto with arith | idtac];
destruct l1 as [ | a3 l1]; [clear Ll1 | absurd (S(S(S(length l1)))=2); auto with arith];
destruct l2 as [ | a3 l2]; [absurd (0=2); auto with arith | idtac];
destruct l2 as [ | a4 l2]; [absurd (1=2); auto with arith | idtac];
destruct l2 as [ | a5 l2]; [clear Ll2 | absurd (S(S(S(length l2)))=2); auto with arith];
assert (Wa1 := Wl1 a1 (or_introl _ (refl_equal _)));
assert (Wa2 := Wl1 a2 (or_intror _ (or_introl _ (refl_equal _))));
assert (Wa3 := Wl2 a3 (or_introl _ (refl_equal _)));
assert (Wa4 := Wl2 a4 (or_intror _ (or_introl _ (refl_equal _))));
simpl in St1; rewrite plus_0_r in St1;
simpl in St2; rewrite plus_0_r in St2.
assert (Sa1 : size a1 <= n).
apply le_trans with (size a1 + size a2); auto with arith.
assert (Sa2 : size a2 <= n).
apply le_trans with (size a1 + size a2); auto with arith.
assert (Sa3 : size a3 <= n).
apply le_trans with (size a3 + size a4); auto with arith.
assert (Sa4 : size a4 <= n).
apply le_trans with (size a3 + size a4); auto with arith.
elim (ac_syntactic
(flatten f (canonical_form a1 :: nil))
(flatten f (canonical_form a2 :: nil))
(flatten f (canonical_form a3 :: nil))
(flatten f (canonical_form a4 :: nil))).
intros k1 [k2 [k3 [k4 [P1 [P2 [P3 P4]]]]]].
destruct k1 as [ | h1 k1]; destruct k4 as [ | h4 k4].
apply commutativity with n k2 k3; trivial;
[rewrite <- app_nil_end in P2 | rewrite <- app_nil_end in P4]; trivial.
generalize (swap_left IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4
k2 k3 (h4 :: k4));
intros [Hk2 | [Hk3 | [Hk4 | H']]]; subst.
generalize (size_size_aux3 _ Af Wa1); setoid_rewrite P1; intro;
absurd (1 <= 0); auto with arith.
generalize (size_size_aux3 _ Af Wa3); setoid_rewrite P3; intro;
absurd (1 <= 0); auto with arith.
discriminate.
apply H'; trivial.
generalize (swap_right IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4
(h1 :: k1) k2 k3);
intros [Hk1 | [Hk2 | [Hk3 | H']]]; subst.
discriminate.
generalize (size_size_aux3 _ Af Wa4); setoid_rewrite P4; intro;
absurd (1 <= 0); auto with arith.
generalize (size_size_aux3 _ Af Wa2); setoid_rewrite P2; intro;
absurd (1 <= 0); auto with arith.
rewrite <- app_nil_end in P2; rewrite <- app_nil_end in P4;
apply H'; trivial.
destruct k2 as [ | h2 k2]; destruct k3 as [ | h3 k3].
apply (syntactic_dec IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Wa3 Wa4 P1 P2 P3 P4).
generalize (associativity IHn Af _ _ _ _ Sa3 Wa3 Sa4 Wa4 Sa1 Wa1 Sa2 Wa2
(h1::k1) (h3 :: k3) (h4::k4));
intros [Hk1 | [Hk3 | [Hk4 | H']]]; subst.
discriminate.
discriminate.
discriminate.
rewrite <- app_nil_end in P1; unfold ac; apply th_sym; apply H'; trivial.
generalize (associativity IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4 (h1::k1) (h2 :: k2) (h4::k4)).
intros [Hk1 | [Hk2 | [Hk4 | H']]]; subst.
discriminate.
discriminate.
discriminate.
rewrite <- app_nil_end in P3; unfold ac; apply H'; trivial.
generalize (middle_commutativity IHn Af _ _ _ _ Sa1 Wa1 Sa2 Wa2 Sa3 Wa3 Sa4 Wa4
(h1 :: k1) (h2 :: k2) (h3 :: k3) (h4 :: k4));
intros [Hk1 | [Hk2 | [Hk3 | [Hk4 | H']]]].
discriminate.
discriminate.
discriminate.
discriminate.
apply H'; trivial.
simpl map in H; refine (permut_trans (list_permut_app_app _ _) _);
refine (permut_trans _ (list_permut_app_app _ _));
do 2 rewrite <- flatten_app;
refine (permut_trans (quick_permut _) _).
simpl app; rewrite H; apply quick_permut_bis; apply permut_refl.
generalize (well_formed_unfold _ Wt1); rewrite Af; intros [Wl1 Ll1];
generalize (well_formed_unfold _ Wt2); rewrite Af; intros [Wl2 Ll2];
destruct l1 as [ | a1 l1]; [absurd (0=2); auto with arith | idtac];
destruct l1 as [ | a2 l1]; [absurd (1=2); auto with arith | idtac];
destruct l1 as [ | a3 l1]; [clear Ll1 | absurd (S(S(S(length l1)))=2); auto with arith];
destruct l2 as [ | a3 l2]; [absurd (0=2); auto with arith | idtac];
destruct l2 as [ | a4 l2]; [absurd (1=2); auto with arith | idtac];
destruct l2 as [ | a5 l2]; [clear Ll2 | absurd (S(S(S(length l2)))=2); auto with arith];
assert (Wa1 := Wl1 a1 (or_introl _ (refl_equal _)));
assert (Wa2 := Wl1 a2 (or_intror _ (or_introl _ (refl_equal _))));
assert (Wa3 := Wl2 a3 (or_introl _ (refl_equal _)));
assert (Wa4 := Wl2 a4 (or_intror _ (or_introl _ (refl_equal _))));
simpl in St1; rewrite plus_0_r in St1;
simpl in St2; rewrite plus_0_r in St2.
assert (Sa1 : size a1 <= n).
apply le_trans with (size a1 + size a2); auto with arith.
assert (Sa2 : size a2 <= n).
apply le_trans with (size a1 + size a2); auto with arith.
assert (Sa3 : size a3 <= n).
apply le_trans with (size a3 + size a4); auto with arith.
assert (Sa4 : size a4 <= n).
apply le_trans with (size a3 + size a4); auto with arith.
elim (@list_permut.permut_length_2 _ term (@eq term) (canonical_form a1) (canonical_form a2)
(canonical_form a3) (canonical_form a4)).
intros [D1 D2]; unfold ac, th_eq; apply general_context; simpl.
right; right; split.
apply IHn; trivial.
left; split; trivial; apply IHn; trivial.
intros [C1 C2]; unfold ac, th_eq, rwr; apply trans_clos_is_trans with (Term f (a2 :: a1 :: nil)).
apply comm; left; trivial.
apply general_context; simpl; right; right; split.
apply IHn; trivial; apply sym_eq; trivial.
left; split; trivial; apply IHn; trivial.
apply permut_trans with (quicksort (map canonical_form (a1 :: a2 :: nil)));
[ apply quick_permut | rewrite H; apply quick_permut_bis; auto ].
unfold ac, th_eq;
destruct (list_eq_dec eq_term_dec l1 l2) as [l1_eq_l2 | l1_diff_l2].
subst; apply th_refl.
apply general_context;
generalize (well_formed_unfold _ Wt1); intros [Wl1 _];
generalize (well_formed_unfold _ Wt2); intros [Wl2 _].
assert (Sl1 : forall t1, In t1 l1 -> size t1 <= n).
intros t1 In_t1; apply le_S_n; apply lt_le_trans with (size (Term f l1)); trivial;
apply size_direct_subterm; trivial.
generalize l2 H Wl2 l1_diff_l2; clear St1 Wt1 l2 Wt2 St2 H Wl2 l1_diff_l2;
induction l1 as [ | t1 l1]; intros l2 H Wl2; destruct l2 as [ | t2 l2]; simpl; trivial.
intro H'; apply H'; trivial.
discriminate.
discriminate.
intro H'; destruct (list_eq_dec eq_term_dec l1 l2) as [l1_eq_l2 | l1_diff_l2'].
left; split; trivial; apply IHn.
apply Sl1; left; trivial.
apply Wl1; left; trivial.
apply Wl2; left; trivial.
inversion H; trivial.
right; right; split.
apply IHn.
apply Sl1; left; trivial.
apply Wl1; left; trivial.
apply Wl2; left; trivial.
inversion H; trivial.
apply IHl1; trivial.
intros; apply Wl1; right; trivial.
intros; apply Sl1; right; trivial.
inversion H; trivial.
intros; apply Wl2; right; trivial.
Qed.
End Make.