Module MyMultisets

Set Implicit Arguments.
Require Import Coq.Arith.Max.
Require Import CoLoR.Util.Multiset.MultisetTheory.
Require Import CoLoR.Util.Multiset.MultisetOrder.
Require Import CoLoR.Util.Multiset.MultisetList.
Require Import CoLoR.Util.Relation.RelExtras.
Require Import Setoid.
Require Import MyTactics.
Require Import Lexicographic.
Require Import WellFoundedInclusion.

This file defines multisets of coercion application descriptors and proves several facts about them. It then adapts a tactic, developed by Arthur Charguéraud, to help simplify and prove ordering assertions between multiset expressions.

This file serves as an auxiliary file for ValueReductionTerminates.

-------------------------------------------------------------------------

Coercion application descriptors.

A coercion application descriptor is a pair of the weight of the value to which the coercion is applied and the measure of the coercion.

Definition cadesc :=
(nat * nat)%type.

Descriptors are lexicographically ordered.

Definition lt :=
  lexprod (@eq nat) lt lt.

Definition gt :=
  transpose lt.

Lemma well_founded_lt:
  well_founded lt.

Proof.

eapply lexprod_wf; eauto using lt_wf.
Qed.

Lemma well_founded_gt:
well_founded (transpose gt).

Proof.

eapply well_founded_inclusion. eapply well_founded_lt. eauto.
Qed.

Definition ge d1 d2 :=
d1 = d2 \/ gt d1 d2.

-------------------------------------------------------------------------

This tactic makes some properties of max explicit.

Ltac maxx :=
  try match goal with |- context[max ?l ?r] =>
    generalize (le_max_l l r); generalize (le_max_r l r); intros ? ?
  end.

Prefixing omega with maxx helps it a little bit.

Ltac maxxomega :=
maxx; omega.

This tactic helps prove a goal of the form gt _ _.

Ltac gt :=
lexprod maxxomega maxxomega maxxomega maxxomega.

-------------------------------------------------------------------------

Little lemmas about the orderings gt and ge.

Lemma ge_intro:
  forall x1 x2 y,
  x1 >= x2 ->
  ge (x1, y) (x2, y).

Proof.

  intros.
  assert (h: x1 = x2 \/ x1 > x2). omega. destruct h.
  subst. left. reflexivity.
  right. left. omega.
Qed.

Lemma gt_ge_gt:
  forall x1 y1 x2 y2 x3 y3,
  gt (x2, y2) (x3, y3) ->
  ge (x1, y1) (x2, y2) ->
  gt (x1, y1) (x3, y3).

Proof.

  introv hgt2 [ heq | hgt1 ].
  congruence.
  dependent destruction hgt1; dependent destruction hgt2; gt.
Qed.

-------------------------------------------------------------------------

Multisets of coercion application descriptors.

The following code basically reproduces CoLoR.Util.Multiset.MultisetNat.

Package up the type of descriptors as a module.

Module CaDesc.
Definition A := cadesc.
End CaDesc.

Equip it with intensional equality to make it a setoid.

Module CaDescSet <: Eqset := Eqset_def CaDesc.

Prove that equality is decidable.

Module CaDescSet_dec.

Module Export Eq := CaDescSet.

Definition eqA_dec: forall x y : cadesc, {x = y} + {x <> y}.

Proof.

    intros (x1 & x2) (y1 & y2).
    generalize (eq_nat_dec x1 y1); intros [ ? | ? ]; [ subst | right; congruence ].
    generalize (eq_nat_dec x2 y2); intros [ ? | ? ]; [ subst | right; congruence ].
    auto.
  Qed.

End CaDescSet_dec.

Module MSetCore := MultisetList.MultisetList CaDescSet_dec.

Module Export MSetTheory := MultisetTheory.Multiset MSetCore.

Module Export MSetOrd := MultisetOrder.MultisetOrder MSetCore.

-------------------------------------------------------------------------

Hints.

Hint Resolve meq_refl.

Because CoLoR multisets have a concrete definition as lists, applications of union to empty sometimes reduce spontaneously. This seems undesirable, as one might wish to plug in a different implementation of multisets that does not have this property. To avoid this behavior, I make union opaque.

Global Opaque union.

Two useful tactics for reasoning about membership.

-------------------------------------------------------------------------

A lemma and tactic for exploiting membership in a singleton.

The statement is slightly specialized for the case where the elements of the multiset are pairs.

Lemma in_singleton:
  forall h1 m1 h2 m2,
  (h1, m1) in {{ (h2, m2) }} ->
  h1 = h2 /\ m1 = m2.

Proof.

intros. forwards: singleton_member_eqA. eassumption. unfold CaDescSet.eqA in *. split; congruence.
Qed.

Ltac in_singleton :=
  match goal with
  | h: (?h1, ?m1) in {{ (?h2, ?m2) }} |- _ =>
      unpack (in_singleton h); clear h; subst
  end.

-------------------------------------------------------------------------

Various lemmas.

Lemma union_comm_assoc:
forall x y z,
x + (y + z) =mul= y + (x + z).

Proof.

intros. do 2 rewrite union_assoc. rewrite (union_comm _ x). auto.
Qed.

Lemma union_empty_r:
forall m,
m + empty =mul= m.

Proof.

exact union_empty.
Qed.

Lemma union_empty_l:
forall m,
empty + m =mul= m.

Proof.

intros. rewrite union_comm. apply union_empty.
Qed.

Lemma eqmul_simplify_left:
  forall m n1 n2,
  n1 =mul= n2 ->
  m + n1 =mul= m + n2.

Proof.

introv h. rewrite h. auto.
Qed.

Lemma union_singleton_gt:
forall R s m,
MultisetGT R ({{s}} + m) m.

Proof.

  intros.
  apply MSetGT with (X := singleton s) (Y := empty) (Z := m).
  apply singleton_notempty.
  apply union_comm.
  rewrite union_empty_r. auto.
  introv h. false. eapply not_empty. eassumption. auto.
Qed.

For some reason, the morphisms in CoLoR.Util.Multiset.MultisetOrder are not directly accessible to us. Here is one, copied and pasted, complete with its horrible proof!

Add Parametric Morphism (R : cadesc -> cadesc -> Prop) : (MultisetGT R)
with signature meq ==> meq ==> iff
as MultisetGT_morph_equiv.

see also: mord_meq_compat

Proof.

  intros xL xR H yL yR H0; split; intro; inversion H1.
  constructor 1 with X Y Z. assumption.
  rewrite <- H. assumption.
  rewrite <- H0. assumption.
  assumption.
  constructor 1 with X Y Z. assumption.
  rewrite H. assumption.
  rewrite H0. assumption.
  assumption.
Qed.

Lemma singleton_empty_gt:
forall R s,
MultisetGT R {{s}} empty.

Proof.

  intros.
  rewrite <- (union_empty_r {{s}}).
  apply union_singleton_gt.
Qed.

The following lemmas are known in CoLoR as mord_ext_l and mord_ext_r. I did the proof before finding out about them, and my statements have less restrictive hypotheses, so I keep them.

Lemma union_covariant_l:
  forall R m1 m2 m,
  MultisetGT R m1 m2 ->
  MultisetGT R (m1 + m) (m2 + m).

Proof.

  introv h. inversion h as [ ? ? ? ? hm1 hm2 ? ].
  apply MSetGT with (X := X) (Y := Y) (Z := Z + m); auto.
  rewrite (union_comm m1). rewrite (union_comm Z). rewrite <- union_assoc. rewrite hm1. auto.
  rewrite (union_comm m2). rewrite (union_comm Z). rewrite <- union_assoc. rewrite hm2. auto.
Qed.

Lemma union_covariant_r:
  forall R m1 m2 m,
  MultisetGT R m1 m2 ->
  MultisetGT R (m + m1) (m + m2).

Proof.

intros. do 2 rewrite (union_comm m). auto using union_covariant_l.
Qed.

Lemma union_covariant_lr:
  forall R m1a m2a m1b m2b,
  MultisetGT R m1a m2a ->
  MultisetGT R m1b m2b ->
  MultisetGT R (m1a + m1b) (m2a + m2b).

Proof.

  introv [ Xa Ya Za ? hm1a hm2a hda ] [ Xb Yb Zb ? hm1b hm2b hdb ].
  apply MSetGT with (X := Xa + Xb) (Y := Ya + Yb) (Z := Za + Zb).
  auto with multisets.
  rewrite hm1a. rewrite hm1b. solve_meq.
  rewrite hm2a. rewrite hm2b. solve_meq.
  introv h. destruct (member_union h); clear h.
  forwards: hda. eassumption. unpack. eauto with multisets.
  forwards: hdb. eassumption. unpack. eauto with multisets.
Qed.

Lemma union_covariant_l_empty:
  forall R m1 m,
  MultisetGT R m1 empty ->
  MultisetGT R (m1 + m) m.

Proof.

  introv h.
  generalize (union_covariant_l m h); clear h; intro h.
  rewrite union_empty_l in h. assumption.
Qed.

Lemma union_covariant_r_empty:
  forall R m1 m,
  MultisetGT R m1 empty ->
  MultisetGT R (m + m1) m.

Proof.

intros. rewrite union_comm. auto using union_covariant_l_empty.
Qed.

Lemma gt_excess_l:
  forall R m1 m2 m,
  MultisetGT R m1 m2 ->
  MultisetGT R (m1 + m) m2.

Proof.

  introv h. inversion h as [ ? ? ? ? hm1 hm2 i ].
  apply MSetGT with (X := X + m) (Y := Y) (Z := Z); auto using union_notempty.
  rewrite hm1. rewrite union_assoc. auto.
  intros y yY. destruct (i y yY) as [ x ? ? ]. exists x. apply member_union_l. assumption. assumption.
Qed.

Lemma gt_excess_r:
  forall R m1 m2 m,
  MultisetGT R m1 m2 ->
  MultisetGT R (m + m1) m2.

Proof.

intros. rewrite union_comm. eauto using gt_excess_l.
Qed.

-------------------------------------------------------------------------

These lemmas are really specific to gt.

Lemma max_left:
forall s1 s2,
S (max s1 s2) > s1.

Proof.

intros. generalize (le_max_l s1 s2). omega.
Qed.

Lemma max_right:
forall s1 s2,
S (max s1 s2) > s2.

Proof.

intros. generalize (le_max_r s1 s2). omega.
Qed.

Lemma singleton_multiset_ordering:
  forall s1 m,
  (forall s2, member s2 m -> gt s1 s2) ->
  MultisetGT gt {{ s1 }} m.

Proof.

  intros.
  apply MSetGT with (X := {{ s1 }}) (Y := m) (Z := empty).
  apply singleton_notempty.
  rewrite union_empty_l. auto.
  rewrite union_empty_l. auto.
  intros y hy.
  exists s1. apply singleton_member. auto.
Qed.

Lemma gt_singleton_singleton:
  forall s1 s2,
  gt s1 s2 ->
  MultisetGT gt {{s1}} {{s2}}.

Proof.

intros. eapply singleton_multiset_ordering. intros.
forwards: singleton_member_eqA. eassumption. unfold CaDescSet.eqA in *. subst. assumption.
Qed.

-------------------------------------------------------------------------

Definition of and facts about the non-strict multiset ordering.

Definition MultisetGE R m1 m2 :=
  MultisetGT R m1 m2 \/ m1 =mul= m2.

Lemma MultisetGE_reflexive:
  forall R m1 m2,
  m1 =mul= m2 ->
  MultisetGE R m1 m2.

Proof.

intros. right. assumption.
Qed.

Lemma MultisetGT_transitive:
  forall x y z,
  MultisetGT gt x y ->
  MultisetGT gt y z ->
  MultisetGT gt x z.

Proof.

eapply mOrd_trans.
unfold transitive. intros. eapply lexprod_transitive; eauto.
Qed.

Lemma MultisetGTGE_transitive:
  forall x y z,
  MultisetGT gt x y ->
  MultisetGE gt y z ->
  MultisetGT gt x z.

Proof.

  introv ? [ ? | eq2 ].
  eauto using MultisetGT_transitive.
  rewrite <- eq2. assumption.
Qed.

Lemma MultisetGE_transitive:
  forall x y z,
  MultisetGE gt x y ->
  MultisetGE gt y z ->
  MultisetGE gt x z.

Proof.

  introv [ ? | eq1 ] [ ? | eq2 ].
  left. eauto using MultisetGT_transitive.
  left. rewrite <- eq2. assumption.
  left. rewrite eq1. assumption.
  right. congruence.
Qed.

Lemma ge_singleton_singleton:
  forall x y,
  ge x y ->
  MultisetGE gt {{ x }} {{ y }}.

Proof.

  introv [ ? | ? ].
  right. congruence.
  left. eapply gt_singleton_singleton. assumption.
Qed.

Lemma union_covariant_gt_ge:
  forall R m1a m2a m1b m2b,
  MultisetGT R m1a m2a ->
  MultisetGE R m1b m2b ->
  MultisetGT R (m1a + m1b) (m2a + m2b).

Proof.

  introv h1 h2.
  destruct h2 as [ h2 | h2 ].
  eauto using union_covariant_lr.
  rewrite h2. eauto using union_covariant_l.
Qed.

Lemma union_covariant_ge_gt:
  forall R m1a m2a m1b m2b,
  MultisetGE R m1a m2a ->
  MultisetGT R m1b m2b ->
  MultisetGT R (m1a + m1b) (m2a + m2b).

Proof.

intros. rewrite (union_comm m1a). rewrite (union_comm m2a). eapply union_covariant_gt_ge; eassumption.
Qed.

Lemma union_covariant_gt_ge_singleton_empty:
  forall R s m1b m2b,
  MultisetGE R m1b m2b ->
  MultisetGT R ({{s}} + m1b) m2b.

Proof.

  intros. rewrite <- (union_empty_l m2b).
  eapply union_covariant_gt_ge.
  eapply singleton_empty_gt.
  assumption.
Qed.

Lemma ge_covariant_union:
  forall R m1a m1b m2a m2b,
  MultisetGE R m1a m1b ->
  MultisetGE R m2a m2b ->
  MultisetGE R (m1a + m2a) (m1b + m2b).

Proof.

  introv h1 h2.
  destruct h1 as [ ? | h1 ]. left. eauto using union_covariant_gt_ge.
  destruct h2 as [ ? | h2 ]. left. rewrite h1. eapply union_covariant_r. assumption.
  right. rewrite h1. rewrite h2. auto.
Qed.

Lemma ge_excess:
forall m n,
MultisetGE gt (m + n) n.

Proof.

intros.

Either m is empty, or it isn't.

destruct (empty_dec m) as [ eq |].

If it is, we are done.

right. rewrite eq. rewrite union_empty_l. reflexivity.

Otherwise, apply the definition of the multiset ordering.

  left. econstructor.
    eassumption.
    eapply union_comm.
    symmetry. eapply union_empty_r.
    intros. false. eapply member_notempty. eassumption. eauto.
Qed.

The multiset ordering is well-founded.

Lemma MultisetLT_wf:
well_founded (MultisetLT gt).

Proof.

  apply mOrd_wf.
  unfold CaDescSet.eqA. intros; subst; assumption.
  apply well_founded_gt.
Qed.

Lemma MultisetGTLT:
  forall R m1 m2,
  MultisetGT R m1 m2 ->
  MultisetLT R m2 m1.

Proof.

auto.
Qed.

This declaration allows exploiting equations between multisets in a goal of the form MultisetGE _ _ _.

Add Parametric Morphism (R : cadesc -> cadesc -> Prop) : (MultisetGE R)
with signature meq ==> meq ==> iff
as MultisetGE_morph_equiv.

Proof.

  intros m1 n1 eq1 m2 n2 eq2. split.
  intros [ ? | ? ]; [ left | right ]. rewrite <- eq1. rewrite <- eq2. assumption. congruence.
  intros [ ? | ? ]; [ left | right ]. rewrite eq1. rewrite eq2. assumption. congruence.
Qed.

-------------------------------------------------------------------------

Tactics to reason about multiset expressions -- by Arthur Charguéraud.

Notation "{{}}" := (empty)
  : container_scope.
Notation "m1 '+++' m2" := (union m1 m2)
  (at level 37, right associativity) : container_scope.
Notation "m1 '>>' m2" := (MultisetGT gt m1 m2)
  (at level 38) : container_scope.
Local Notation "\{ x }" := (singleton x)
  : container_scope.

Open Scope container_scope.

Hint Rewrite <- union_assoc : rew_permut_simpl.
Hint Rewrite union_empty_l union_empty_r : rew_permut_simpl.
Ltac rew_permut_simpl :=
  autorewrite with rew_permut_simpl.
Ltac rews_permut_simpl :=
  autorewrite with rew_permut_simpl in *.

Implicit Types l : Multiset.

Lemma permut_get_1 : forall l1 l2,
  (l1 +++ l2) =mul= (l1 +++ l2).

Proof.

intros. auto. Qed.

Lemma permut_get_2 : forall l1 l2 l3,
(l1 +++ l2 +++ l3) =mul= (l2 +++ l1 +++ l3).

Proof.

intros. apply union_comm_assoc. Qed.

Lemma permut_get_3 : forall l1 l2 l3 l4,
(l1 +++ l2 +++ l3 +++ l4) =mul= (l2 +++ l3 +++ l1 +++ l4).

Proof.

intros. do 2 rewrite (union_assoc l2). apply permut_get_2.
Qed.

Lemma permut_get_4 : forall l1 l2 l3 l4 l5,
(l1 +++ l2 +++ l3 +++ l4 +++ l5)
=mul= (l2 +++ l3 +++ l4 +++ l1 +++ l5).

Proof.

intros. do 2 rewrite (union_assoc l2). apply permut_get_3.
Qed.

Lemma permut_get_5 : forall l1 l2 l3 l4 l5 l6,
(l1 +++ l2 +++ l3 +++ l4 +++ l5 +++ l6)
=mul= (l2 +++ l3 +++ l4 +++ l5 +++ l1 +++ l6).

Proof.

intros. do 2 rewrite (union_assoc l2). apply permut_get_4.
Qed.

Lemma permut_get_6 : forall l1 l2 l3 l4 l5 l6 l7,
(l1 +++ l2 +++ l3 +++ l4 +++ l5 +++ l6 +++ l7)
=mul= (l2 +++ l3 +++ l4 +++ l5 +++ l6 +++ l1 +++ l7).

Proof.

intros. do 2 rewrite (union_assoc l2). apply permut_get_5.
Qed.

Lemma permut_get_7 : forall l1 l2 l3 l4 l5 l6 l7 l8,
(l1 +++ l2 +++ l3 +++ l4 +++ l5 +++ l6 +++ l7 +++ l8)
=mul= (l2 +++ l3 +++ l4 +++ l5 +++ l6 +++ l7 +++ l1 +++ l8).

Proof.

intros. do 2 rewrite (union_assoc l2). apply permut_get_6.
Qed.

Lemma permut_get_8 : forall l1 l2 l3 l4 l5 l6 l7 l8 l9,
(l1 +++ l2 +++ l3 +++ l4 +++ l5 +++ l6 +++ l7 +++ l8 +++ l9)
=mul= (l2 +++ l3 +++ l4 +++ l5 +++ l6 +++ l7 +++ l8 +++ l1 +++ l9).

Proof.

intros. do 2 rewrite (union_assoc l2). apply permut_get_7.
Qed.

Lemma permut_tactic_setup : forall l1 l2,
MultisetGT gt ({{}} +++ l1 +++ {{}}) (l2 +++ {{}}) -> MultisetGT gt l1 l2.

Proof.

intros. rews_permut_simpl. eauto. Qed.

Lemma permut_tactic_keep : forall l1 l2 l3 l4,
MultisetGT gt ((l1 +++ l2) +++ l3) l4 ->
MultisetGT gt (l1 +++ (l2 +++ l3)) l4.

Proof.

intros. rews_permut_simpl. eauto. Qed.

Lemma permut_tactic_trans : forall l1 l2 l3,
l3 =mul= l2 -> MultisetGT gt l1 l3 -> MultisetGT gt l1 l2.

Proof.

introv h. rewrite h. auto. Qed.

* permut_lemma_get n returns the lemma permut_get_n for the given value of n

* permut_prepare applies to a goal of the form permut l l' and sets l and l' in the form l1 +++ l2 +++ .. +++ {{}}, (some of the lists li are put in the form x::{{}}).

Ltac permut_simpl_prepare :=
   rew_permut_simpl;
   apply permut_tactic_setup;
   repeat rewrite <- union_assoc.

* todo : doc

Ltac permut_index_of l lcontainer :=
  match constr:(lcontainer) with
  | l +++ _ => constr:(1)
  | _ +++ l +++ _ => constr:(2)
  | _ +++ _ +++ l +++ _ => constr:(3)
  | _ +++ _ +++ _ +++ l +++ _ => constr:(4)
  | _ +++ _ +++ _ +++ _ +++ l +++ _ => constr:(5)
  | _ +++ _ +++ _ +++ _ +++ _ +++ l +++ _ => constr:(6)
  | _ +++ _ +++ _ +++ _ +++ _ +++ _ +++ l +++ _ => constr:(7)
  | _ +++ _ +++ _ +++ _ +++ _ +++ _ +++ _ +++ l +++ _ => constr:(8)
  | _ => constr:(0)
  end.

* permut_simplify simplifies a goal of the form permut l l' where l and l' are lists built with concatenation and consing

Ltac permut_simpl_once_for permut_tactic_simpl :=
  let go l0 l' :=
    match l0 with
    | _ +++ {{}} => fail 1
    | _ +++ (?l +++ ?lr) =>
      match permut_index_of l l' with
      | 0 => apply permut_tactic_keep
      | ?n => let F := permut_lemma_get n in
             eapply permut_tactic_trans;
             [ eapply F; try typeclass
             | apply permut_tactic_simpl ]
      end
     end in
   match goal with
   | |- _ ?x ?y => go x y
   | |- _ _ ?x ?y => go x y
   | |- _ _ _ ?x ?y => go x y
   | |- _ _ _ _ ?x ?y => go x y
   end.

Ltac permut_conclude :=
  eauto using union_singleton_gt, singleton_empty_gt, gt_excess_l,
  union_covariant_l_empty, union_covariant_r_empty, union_covariant_l,
  union_covariant_r.

Ltac permut_simpl_for permut_tactic_simpl :=
  permut_simpl_prepare;
  repeat permut_simpl_once_for permut_tactic_simpl;
  rew_permut_simpl;
  try permut_conclude.

Lemma permut_tactic_simpl_eq : forall l1 l2 l3 l4,
  (l1 +++ l3) =mul= l4 ->
  (l1 +++ (l2 +++ l3)) =mul= (l2 +++ l4).

Proof.

introv h. rewrite <- h. apply permut_get_2. Qed.

Lemma permut_tactic_simpl_incl : forall l1 l2 l3 l4,
(l1 +++ l3) >> l4 ->
(l1 +++ (l2 +++ l3)) >> (l2 +++ l4).

Proof.

  intros.
  rewrite union_assoc.
  rewrite (union_comm l1).
  rewrite <- union_assoc.
  auto using union_covariant_r.
Qed.

Ltac get_premut_tactic_simpl tt :=
  match goal with
  | |- ?x =mul= ?y => constr:(permut_tactic_simpl_eq)
  | |- ?x >> ?y => constr:(permut_tactic_simpl_incl)
  end.

Ltac permut_simpl_once :=
  let L := get_premut_tactic_simpl tt in permut_simpl_once_for L.

Ltac permut_simpl :=
  let L := get_premut_tactic_simpl tt in permut_simpl_for L.

Section Demo.

Lemma demo_multiset_union_permut_simpl_1 :
  forall l1 l2 l3 l4,
  MultisetGT gt l4 empty ->
  MultisetGT gt (l1 +++ l2 +++ l3 +++ l4) (l3 +++ l2 +++ l1).

Proof.

  intros.
  permut_simpl_prepare.
  permut_simpl_once.
  permut_simpl_once.
  permut_simpl_once.
  rew_permut_simpl.
  permut_conclude.
Qed.

Lemma demo_multiset_union_permut_simpl_2 :
  forall x y l1 l2 l3,
  (l1 +++ l2 +++ \{y} +++ (\{x} +++ l3))
  >>
  (l1 +++ \{x} +++ l3 +++ l2).

Proof.

  intros.
  permut_simpl_prepare.
  permut_simpl_once.
  permut_simpl_once.
  permut_simpl_once.
  permut_simpl_once.
  rew_permut_simpl.
  permut_conclude.
Qed.

Lemma demo_multiset_union_permut_simpl_3 :
  forall x y l1 l1' l2 l3 l4,
  l1 >> l4 +++ l1' ->
  (l1 +++ (\{x} +++ l2) +++ \{x} +++ (\{y} +++ l3)) >>
  (\{y} +++ \{x} +++ (l1' +++ l2 +++ l4) +++ (\{x} +++ l3)).

Proof.

intros. dup.

details

  permut_simpl_prepare.
  permut_simpl_once.
  permut_simpl_once.
  permut_simpl_once.
  permut_simpl_once.
  permut_simpl_once.
  try permut_simpl_once.
  rew_permut_simpl.
  rewrite union_comm.
  permut_conclude.

short

  permut_simpl.
  rewrite union_comm.
  permut_conclude.
Qed.

End Demo.

-------------------------------------------------------------------------

More random lemmas.

Lemma union_comm_assoc_variant:
forall x y z,
x +++ y +++ z =mul= x +++ z +++ y.

Proof.

intros. rewrite (union_comm y z). reflexivity.
Qed.