Library Permissions

Require Import HahnBase.
Require Import List.
Require Import ListSet.
Require Import Permutation.
Require Import PermutationTactic.
Require Import Prelude.
Require Import QArith.
Require Import Qcanon.
Require Import Utf8.

Import ListNotations.

Open Scope Qc_scope.

Permissions

Prerequisites

Below are some basic properties and results on rational numbers.

Lemma Q2Qc_correct :
  forall q : Q, Q2Qc q == q.

Lemma Qcplus_lt_compat :
  forall x y z t : Qc,
  x < y -> z < t -> x + z < y + t.

Lemma Qcplus_le_mono_l :
  forall x y z : Qc, x <= y <-> z + x <= z + y.

Lemma Qcplus_le_mono_r :
  forall x y z : Qc, x <= y <-> x + z <= y + z.

Lemma Qclt_nge :
  forall x y : Qc, x < y <-> ~ y <= x.

Lemma Qclt_irrefl :
  forall q : Qc, ~ q < q.

Lemma Qclt_asymm :
  forall q1 q2 : Qc,
  q1 < q2 -> ~ q2 < q1.

Lemma Qcplus_lt_mono_l :
  forall x y z : Qc, x < y <-> z + x < z + y.

Lemma Qcplus_lt_mono_r :
  forall x y z : Qc, x < y <-> x + z < y + z.

Lemma Qcplus_lt_compat_le_l :
  forall x y z t : Qc,
  x <= y -> z < t -> x + z < y + t.

Lemma Qcplus_lt_compat_le_r :
  forall x y z t : Qc,
  x < y -> z <= t -> x + z < y + t.

Lemma Qcplus_pos_nonneg :
  forall p q : Qc, 0 < p -> 0 <= q -> 0 < p + q.

Lemma Qcplus_swap_l :
  forall q1 q2 q3 : Qc, q1 + (q2 + q3) = q2 + (q1 + q3).

Lemma Qcplus_swap_r :
  forall q1 q2 q3 : Qc, q1 + (q2 + q3) = q3 + (q2 + q1).

Lemma Qcplus_pos_le_elim :
  forall q1 q2 q : Qc, q1 + q2 <= q -> 0 <= q2 -> q1 <= q.

Lemma Qcplus_pos_lt_elim :
  forall q1 q2 q : Qc, q1 + q2 < q -> 0 <= q2 -> q1 < q.

Lemma Qcplus_le_weaken :
  forall q1 q2 q : Qc, 0 < q -> q1 <= q2 -> q1 <= q2 + q.

Lemma Qcplus_lt_weaken :
  forall q1 q2 q : Qc,
  0 < q -> q1 <= q2 -> q1 < q2 + q.

Lemma Qcle_diff :
  forall q1 q2 : Qc, q1 <= q2 -> exists q, q2 = q1 + q.

Lemma Qclt_diff :
  forall q1 q2 : Qc, q1 < q2 -> exists q, q2 = q + q1.

Lemma Qclt_mono_pos :
  forall q1 q2 : Qc, 0 < q1 -> q2 < q2 + q1.

Lemma Qcle_plus_elim :
  forall q1 q2 q3 : Qc, 0 <= q1 -> 0 <= q2 -> q1 + q2 <= q3 -> q1 <= q3.

Lemma Qcle_weaken :
  forall q1 q2 : Qc, q1 = q2 -> q1 <= q2.

Lemma Qcplus_canc_l :
  forall q1 q2 q : Qc, q + q1 = q + q2 -> q1 = q2.

Lemma Qcplus_canc_r :
  forall q1 q2 q : Qc, q1 + q = q2 + q -> q1 = q2.

Lemma Qcplus_neg_dist :
  forall q1 q2 : Qc, -(q1 + q2) = (-q1) + (-q2).

Lemma Qcplus_pos_le :
  forall q1 q2 : Qc, 0 < q2 -> q1 <= q1 + q2.

Fractional permissions

Fractional permissions are rational numbers in the range (0..1].

Definition perm_full := 1%Qc.

Validity

Any rational number q is a valid fractional permission, written perm_valid q, if q is within the range (0..1].

Definition perm_valid (q : Qc) : Prop := 0 < q /\ q <= 1.

Lemma perm_valid_mono :
  forall q1 q2, perm_valid q1 -> q2 < q1 + q2.

Lemma perm_valid_pos :
  forall q : Qc, perm_valid q -> 0 < q.

Hint Resolve perm_valid_pos : core.

Lemma perm_valid_full_neg :
  forall q, perm_valid q -> ~ perm_full < q.

Lemma perm_valid_full :
  forall q, perm_valid q -> perm_full <= q -> q = perm_full.

Disjointness

Two permissions q1 and q2 are disjoint, written perm_disj q1 q2, if they are both positive and their sum does not exceed 1.

Definition perm_disj (q1 q2 : Qc) : Prop :=
0 < q1 /\ 0 < q2 /\ q1 + q2 <= 1.

Permission disjointness is a symmetric relation.

Instance perm_disj_symm :
Symmetric perm_disj.

Permission disjointness implies validity of its operands.

Lemma perm_disj_valid_l :
  forall q1 q2, perm_disj q1 q2 -> perm_valid q1.

Lemma perm_disj_valid_r :
  forall q1 q2, perm_disj q1 q2 -> perm_valid q2.

Lemma perm_disj_valid :
  forall q1 q2, perm_disj q1 q2 -> perm_valid q1 /\ perm_valid q2.

Below are several other useful properties of disjointness.

Lemma perm_disj_add_l :
  forall q1 q2 q3,
  perm_disj q1 q2 -> perm_disj (q1 + q2) q3 -> perm_disj q2 q3.

Lemma perm_disj_add_r :
  forall q1 q2 q3,
  perm_disj q2 q3 -> perm_disj q1 (q2 + q3) -> perm_disj q1 q2.

Lemma perm_disj_assoc_l :
  forall q1 q2 q3,
  perm_disj q1 q2 -> perm_disj (q1 + q2) q3 -> perm_disj q1 (q2 + q3).

Lemma perm_disj_assoc_r :
  forall q1 q2 q3,
  perm_disj q2 q3 -> perm_disj q1 (q2 + q3) -> perm_disj (q1 + q2) q3.

Lemma perm_add_valid :
  forall q1 q2, perm_disj q1 q2 -> perm_valid (q1 + q2).

Lemma perm_lt_weaken :
  forall q q1 q2, perm_disj q1 q2 -> q < q1 -> q < q1 + q2.

Lemma perm_le_weaken :
  forall q q1 q2, perm_disj q1 q2 -> q <= q1 -> q <= q1 + q2.

Lemma perm_disj_full_neg_l :
  forall q, ~ perm_disj q perm_full.

Lemma perm_disj_full_neg_r :
  forall q, ~ perm_disj perm_full q.

Lemma perm_lt_diff :
  forall q1 q2,
  perm_valid q1 ->
  perm_valid q2 ->
  q1 < q2 ->
  exists q3, perm_disj q1 q3 /\ q1 + q3 = q2.

Lemma perm_disj_lt :
  forall q1 q2 q3,
  perm_valid q1 ->
  perm_disj q2 q3 ->
  q1 < q2 ->
  perm_disj q1 q3.

Lemma perm_disj_le :
  forall q1 q2 q3,
  perm_valid q1 ->
  perm_disj q2 q3 ->
  q1 <= q2 ->
  perm_disj q1 q3.

Permission sequences

This section defines operations on sequences of fractional permissions.

Validity

A sequence of fractional permissions is valid if all permissions are valid individually.

Fixpoint perm_valid_list (xs : list Qc) : Prop :=
  match xs with
    | nil => True
    | q :: xs' => perm_valid q /\ perm_valid_list xs'
  end.

Notation "√ qs" := (perm_valid_list qs) (only printing, at level 80).

Lemma perm_valid_list_single :
  forall q, perm_valid_list [q] <-> perm_valid q.

Hint Resolve perm_valid_list_single : core.

Lemma perm_valid_list_permutation :
  forall xs1 xs2,
  Permutation xs1 xs2 -> perm_valid_list xs1 -> perm_valid_list xs2.

Add Parametric Morphism : perm_valid_list
  with signature @Permutation Qc ==> iff
    as perm_valid_list_permut_mor.

Positivity

A sequence of fractional permissions is positive if all rationals in the list are positive.

Fixpoint perm_pos_list (xs : list Qc) : Prop :=
  match xs with
    | nil => True
    | q :: xs' => 0 < q /\ perm_pos_list xs'
  end.

Lemma perm_pos_list_In :
  forall qs q, perm_pos_list qs -> In q qs -> 0 < q.

Lemma perm_pos_list_permutation :
  forall xs ys,
  Permutation xs ys -> perm_pos_list xs -> perm_pos_list ys.

Add Parametric Morphism : perm_pos_list
  with signature @Permutation Qc ==> iff
    as perm_pos_list_permut_mor.

Ltac perm_pos_list_solve :=
  match goal with
    | [ _ : (perm_pos_list ?X) |- (perm_pos_list _) ] =>
      apply perm_pos_list_permutation with X; auto; list_permutation;
        fail "perm_pos_list_solve can not solve this system."
    | [ |- _ ] => fail "perm_pos_list_solve can not be applied."
  end.

Lemma perm_pos_list_add_left :
  forall q1 q2 qs,
  perm_pos_list (q1 :: q2 :: qs) -> perm_pos_list (q1 + q2 :: qs).

Lemma perm_pos_list_add :
  forall qs1 q1 q2 qs2,
  perm_pos_list (qs1 ++ q1 :: q2 :: qs2) ->
  perm_pos_list (qs1 ++ q1 + q2 :: qs2).

Lemma perm_pos_list_tail :
  forall q qs,
  perm_pos_list (q :: qs) -> perm_pos_list qs.

Lemma perm_pos_list_sub_l :
  forall xs ys,
  perm_pos_list (xs ++ ys) -> perm_pos_list xs.

Lemma perm_pos_list_sub_r :
  forall xs ys,
  perm_pos_list (xs ++ ys) -> perm_pos_list ys.

Lemma perm_pos_list_remove :
  forall q xs ys,
  perm_pos_list (xs ++ q :: ys) -> perm_pos_list (xs ++ ys).

Lemma perm_pos_list_remove_list :
  forall xs ys zs,
  perm_pos_list (xs ++ ys ++ zs) -> perm_pos_list (xs ++ zs).

Lemma perm_valid_list_pos :
  forall qs, perm_valid_list qs -> perm_pos_list qs.

Hint Resolve perm_valid_list_pos : core.

Lemma perm_pos_list_cons :
  forall q qs,
  0 < q -> perm_pos_list qs -> perm_pos_list (q :: qs).

Lemma perm_pos_list_app :
  forall xs ys,
  perm_pos_list xs -> perm_pos_list ys -> perm_pos_list (xs ++ ys).

Lemma perm_pos_list_assoc_l :
  forall q1 q2 q3 qs,
  perm_pos_list [q2; q3] ->
  perm_pos_list (q1 :: q2 + q3 :: qs) ->
  perm_pos_list (q1 + q2 :: q3 :: qs).

Lemma perm_pos_list_assoc_r :
  forall q1 q2 q3 qs,
  perm_pos_list [q1; q2] ->
  perm_pos_list (q1 + q2 :: q3 :: qs) ->
  perm_pos_list (q1 :: q2 + q3 :: qs).

Lemma perm_pos_list_set_remove :
  forall xs x,
  perm_pos_list xs -> perm_pos_list (set_remove Qc_eq_dec x xs).

Lemma perm_pos_list_sublist :
  forall xs ys,
  sublist Qc_eq_dec xs ys -> perm_pos_list ys -> perm_pos_list xs.

Addition

The addition of a sequence of fractional permissions is defined as classical summation.

Fixpoint perm_add_list (xs : list Qc) : Qc :=
  match xs with
    | nil => 0
    | q :: xs' => q + perm_add_list xs'
  end.

Notation "∑ xs" := (perm_add_list xs) (only printing, at level 80).

Lemma perm_add_list_permutation :
  forall xs ys,
  Permutation xs ys -> perm_add_list xs = perm_add_list ys.

Add Parametric Morphism : perm_add_list
  with signature @Permutation Qc ==> eq
    as perm_add_list_permut_mor.

Lemma perm_add_list_single :
  forall q, perm_add_list [q] = q.

Hint Rewrite perm_add_list_single : core.

Lemma perm_add_list_nonneg :
  forall qs, perm_pos_list qs -> 0 <= perm_add_list qs.

Lemma perm_add_list_add_left :
  forall q1 q2 qs,
  perm_add_list (q1 :: q2 :: qs) = perm_add_list (q1 + q2 :: qs).

Lemma perm_add_list_add :
  forall qs1 q1 q2 qs2,
  perm_add_list (qs1 ++ q1 :: q2 :: qs2) = perm_add_list (qs1 ++ q1 + q2 :: qs2).

Lemma perm_add_list_left :
  forall x xs,
  perm_add_list (x :: xs) = x + perm_add_list xs.

Lemma perm_add_list_set_remove :
  forall qs q,
  set_In q qs ->
  perm_add_list (set_remove Qc_eq_dec q qs) = perm_add_list qs + - q.

Lemma perm_add_list_sublist :
  forall xs ys,
  sublist Qc_eq_dec xs ys ->
  perm_pos_list ys ->
  perm_add_list xs <= perm_add_list ys.

Disjointness

A sequence of fractional permissions is disjoint if all the rationals are positive and the sum of all rationals in the list does not exceed one.

Definition perm_disj_list (qs : list Qc) : Prop :=
  perm_pos_list qs /\ perm_add_list qs <= 1.

Notation "⫡ xs" := (perm_disj_list xs) (only printing, at level 80).

Lemma perm_disj_list_permutation :
  forall xs ys,
  Permutation xs ys -> perm_disj_list xs -> perm_disj_list ys.

Add Parametric Morphism : perm_disj_list
  with signature @Permutation Qc ==> iff
    as perm_disj_list_permut_mor.

Lemma perm_disj_list_single :
  forall q, perm_disj_list [q] <-> perm_valid q.

Hint Resolve perm_disj_list_single : core.

Lemma perm_disj_list_binary :
  forall q1 q2,
  perm_disj_list [q1; q2] <-> perm_disj q1 q2.

Lemma perm_disj_list_tail :
  forall q qs,
  perm_disj_list (q :: qs) -> perm_disj_list qs.

Lemma perm_disj_list_sub_r :
  forall xs ys,
  perm_disj_list (xs ++ ys) -> perm_disj_list ys.

Lemma perm_disj_list_sub_l :
  forall xs ys,
  perm_disj_list (xs ++ ys) -> perm_disj_list xs.

Lemma perm_disj_list_remove :
  forall q xs ys,
  perm_disj_list (xs ++ q :: ys) -> perm_disj_list (xs ++ ys).

Lemma perm_disj_list_remove_list :
  forall xs ys zs,
  perm_disj_list (xs ++ ys ++ zs) -> perm_disj_list (xs ++ zs).

Lemma perm_disj_list_add_left :
  forall q1 q2 qs,
  perm_disj_list (q1 :: q2 :: qs) -> perm_disj_list (q1 + q2 :: qs).

Lemma perm_disj_list_add :
  forall q1 q2 qs1 qs2,
  perm_disj_list (qs1 ++ q1 :: q2 :: qs2) ->
  perm_disj_list (qs1 ++ q1 + q2 :: qs2).

Lemma perm_disj_list_valid_head :
  forall q qs,
  perm_disj_list (q :: qs) -> perm_valid q.

Lemma perm_disj_list_valid :
  forall qs, perm_disj_list qs -> perm_valid_list qs.

Lemma perm_disj_list_pos :
  forall qs,
  perm_disj_list qs -> perm_pos_list qs.

Lemma perm_disj_list_elim_left :
  forall q1 q2 qs,
  perm_pos_list [q1; q2] ->
  perm_disj_list (q1 + q2 :: qs) ->
  perm_disj_list (q1 :: q2 :: qs).

Lemma perm_disj_list_elim :
  forall q1 q2 qs1 qs2,
  perm_pos_list [q1; q2] ->
  perm_disj_list (qs1 ++ q1 + q2 :: qs2) ->
  perm_disj_list (qs1 ++ q1 :: q2 :: qs2).

Lemma perm_disj_list_elim_remove_l :
  forall q1 q2 qs1 qs2,
  perm_pos_list [q1; q2] ->
  perm_disj_list (qs1 ++ q1 + q2 :: qs2) ->
  perm_disj_list (qs1 ++ q1 :: qs2).

Lemma perm_disj_list_elim_remove_r :
  forall q1 q2 qs1 qs2,
  perm_pos_list [q1; q2] ->
  perm_disj_list (qs1 ++ q1 + q2 :: qs2) ->
  perm_disj_list (qs1 ++ q2 :: qs2).

Lemma perm_disj_list_assoc_left :
  forall q1 q2 q3 qs,
  perm_pos_list [q2; q3] ->
  perm_disj_list (q1 :: q2 + q3 :: qs) ->
  perm_disj_list (q1 + q2 :: q3 :: qs).

Lemma perm_disj_list_assoc :
  forall q1 q2 q3 qs1 qs2,
  perm_pos_list [q2; q3] ->
  perm_disj_list (qs1 ++ q1 :: q2 + q3 :: qs2) ->
  perm_disj_list (qs1 ++ q1 + q2 :: q3 :: qs2).

Lemma perm_disj_list_sublist :
  forall xs ys,
  sublist Qc_eq_dec xs ys ->
  perm_disj_list ys ->
  perm_disj_list xs.

Lemma perm_disj_list_lt :
  forall x y xs,
  perm_valid x ->
  x < y ->
  perm_disj_list (y :: xs) ->
  perm_disj_list (x :: xs).

Lemma perm_disj_list_le :
  forall x y xs,
  perm_valid x ->
  x <= y ->
  perm_disj_list (y :: xs) ->
  perm_disj_list (x :: xs).

Ltac permlist_solve1_with id :=
  match goal with
    | [ H : perm_disj_list ?X |- perm_disj_list ?Y ] =>
        match H with
          | id => apply perm_disj_list_permutation with X; auto; list_permutation;
              fail "permlist_solve can not solve this system"
        end
    | [ |- _ ] => fail "permlist_solve can not be applied"
  end.

Ltac permlist_solve1 :=
  match goal with
    | [ H : perm_disj_list ?X |- perm_disj_list ?Y ] =>
        permlist_solve1_with H
    | [ |- _ ] => fail "permlist_solve can not be applied"
  end.

Ltac permlist_solve2_with id :=
  match goal with
    | [ H : perm_disj_list ?X |- perm_disj_list ?Y ] =>
      match H with
        | id => apply perm_disj_list_sublist with X;
          [repeat (simpls; desf; intuition)|auto];
          fail "permlist_solve can not solve this system"
      end
    | [ |- _ ] => fail "permlist_solve can not be applied"
  end.

Ltac permlist_solve2 :=
  match goal with
    | [ H : perm_disj_list ?X |- perm_disj_list ?Y ] =>
        permlist_solve2_with H
    | [ |- _ ] => fail "permlist_solve can not be applied"
  end.

Ltac permlist_solve :=
  try permlist_solve1;
  try permlist_solve2;
  fail "permlist_solve can not solve this system".

Tactic Notation "permlist_solve" "with" ident(H) :=
  try permlist_solve1_with H;
  try permlist_solve2_with H;
  fail "permlist_solve can not solve this system".

Ltac perm_disj_list_split :=
  match goal with
    | |- perm_disj_list [?q1+?q2] => apply perm_disj_list_add with (qs1:=[])(qs2:=[]); simpl
    | |- perm_disj_list [?q1+?q2;?a] => apply perm_disj_list_add with (qs1:=[])(qs2:=[a]); simpl
    | |- perm_disj_list [?a;?q1+?q2] => apply perm_disj_list_add with (qs1:=[a])(qs2:=[]); simpl
    | |- perm_disj_list [?q1+?q2;?a;?b] => apply perm_disj_list_add with (qs1:=[])(qs2:=[a;b]); simpl
    | |- perm_disj_list [?a;?q1+?q2;?b] => apply perm_disj_list_add with (qs1:=[a])(qs2:=[b]); simpl
    | |- perm_disj_list [?a;?b;?q1+?q2] => apply perm_disj_list_add with (qs1:=[a;b])(qs2:=[]); simpl
    | |- perm_disj_list [?q1+?q2;?a;?b;?c] => apply perm_disj_list_add with (qs1:=[])(qs2:=[a;b;c]); simpl
    | |- perm_disj_list [?a;?q1+?q2;?b;?c] => apply perm_disj_list_add with (qs1:=[a])(qs2:=[b;c]); simpl
    | |- perm_disj_list [?a;?b;?q1+?q2;?c] => apply perm_disj_list_add with (qs1:=[a;b])(qs2:=[c]); simpl
    | |- perm_disj_list [?a;?b;?c;?q1+?q2] => apply perm_disj_list_add with (qs1:=[a;b;c])(qs2:=[]); simpl
    | |- perm_disj_list [?q1+?q2;?a;?b;?c;?d] => apply perm_disj_list_add with (qs1:=[])(qs2:=[a;b;c;d]); simpl
    | |- perm_disj_list [?a;?q1+?q2;?b;?c;?d] => apply perm_disj_list_add with (qs1:=[a])(qs2:=[b;c;d]); simpl
    | |- perm_disj_list [?a;?b;?q1+?q2;?c;?d] => apply perm_disj_list_add with (qs1:=[a;b])(qs2:=[c;d]); simpl
    | |- perm_disj_list [?a;?b;?c;?q1+?q2;?d] => apply perm_disj_list_add with (qs1:=[a;b;c])(qs2:=[d]); simpl
    | |- perm_disj_list [?a;?b;?c;?d;?q1+?q2] => apply perm_disj_list_add with (qs1:=[a;b;c;d])(qs2:=[]); simpl
    | |- perm_disj_list [?q1+?q2;?a;?b;?c;?d;?e] => apply perm_disj_list_add with (qs1:=[])(qs2:=[a;b;c;d;e]); simpl
    | |- perm_disj_list [?a;?q1+?q2;?b;?c;?d;?e] => apply perm_disj_list_add with (qs1:=[a])(qs2:=[b;c;d;e]); simpl
    | |- perm_disj_list [?a;?b;?q1+?q2;?c;?d;?e] => apply perm_disj_list_add with (qs1:=[a;b])(qs2:=[c;d;e]); simpl
    | |- perm_disj_list [?a;?b;?c;?q1+?q2;?d;?e] => apply perm_disj_list_add with (qs1:=[a;b;c])(qs2:=[d;e]); simpl
    | |- perm_disj_list [?a;?b;?c;?d;?q1+?q2;?e] => apply perm_disj_list_add with (qs1:=[a;b;c;d])(qs2:=[e]); simpl
    | |- perm_disj_list [?a;?b;?c;?d;?e;?q1+?q2] => apply perm_disj_list_add with (qs1:=[a;b;c;d;e])(qs2:=[]); simpl
    | [ |- _ ] => fail "perm_disj_list_split can not be applied."
  end.

Ltac perm_disj_list_split_in id :=
  match goal with
    | H : perm_disj_list ?T |- _ =>
      match H with
        | id => match T with
            | [?q1+?q2] => apply perm_disj_list_elim with q1 q2 [] [] in H; simpl in H; auto
            | [?q1+?q2;?a] => apply perm_disj_list_elim with q1 q2 [] [a] in H; simpl in H; auto
            | [?a;?q1+?q2] => apply perm_disj_list_elim with q1 q2 [a] [] in H; simpl in H; auto
            | [?q1+?q2;?a;?b] => apply perm_disj_list_elim with q1 q2 [] [a;b] in H; simpl in H; auto
            | [?a;?q1+?q2;?b] => apply perm_disj_list_elim with q1 q2 [a] [b] in H; simpl in H; auto
            | [?a;?b;?q1+?q2] => apply perm_disj_list_elim with q1 q2 [a;b] [] in H; simpl in H; auto
            | [?q1+?q2;?a;?b;?c] => apply perm_disj_list_elim with q1 q2 [] [a;b;c] in H; simpl in H; auto
            | [?a;?q1+?q2;?b;?c] => apply perm_disj_list_elim with q1 q2 [a] [b;c] in H; simpl in H; auto
            | [?a;?b;?q1+?q2;?c] => apply perm_disj_list_elim with q1 q2 [a;b] [c] in H; simpl in H; auto
            | [?a;?b;?c;?q1+?q2] => apply perm_disj_list_elim with q1 q2 [a;b;c] [] in H; simpl in H; auto
            | [?q1+?q2;?a;?b;?c;?d] => apply perm_disj_list_elim with q1 q2 [] [a;b;c;d] in H; simpl in H; auto
            | [?a;?q1+?q2;?b;?c;?d] => apply perm_disj_list_elim with q1 q2 [a] [b;c;d] in H; simpl in H; auto
            | [?a;?b;?q1+?q2;?c;?d] => apply perm_disj_list_elim with q1 q2 [a;b] [c;d] in H; simpl in H; auto
            | [?a;?b;?c;?q1+?q2;?d] => apply perm_disj_list_elim with q1 q2 [a;b;c] [d] in H; simpl in H; auto
            | [?a;?b;?c;?d;?q1+?q2] => apply perm_disj_list_elim with q1 q2 [a;b;c;d] [] in H; simpl in H; auto
            | [?q1+?q2;?a;?b;?c;?d;?e] => apply perm_disj_list_elim with q1 q2 [] [a;b;c;d;e] in H; simpl in H; auto
            | [?a;?q1+?q2;?b;?c;?d;?e] => apply perm_disj_list_elim with q1 q2 [a] [b;c;d;e] in H; simpl in H; auto
            | [?a;?b;?q1+?q2;?c;?d;?e] => apply perm_disj_list_elim with q1 q2 [a;b] [c;d;e] in H; simpl in H; auto
            | [?a;?b;?c;?q1+?q2;?d;?e] => apply perm_disj_list_elim with q1 q2 [a;b;c] [d;e] in H; simpl in H; auto
            | [?a;?b;?c;?d;?q1+?q2;?e] => apply perm_disj_list_elim with q1 q2 [a;b;c;d] [e] in H; simpl in H; auto
            | [?a;?b;?c;?d;?e;?q1+?q2] => apply perm_disj_list_elim with q1 q2 [a;b;c;d;e] [] in H; simpl in H; auto
            | _ => fail "perm_disj_list_split_in can not be applied."
          end
        | _ => fail "perm_disj_list_split_in can not be applied."
      end
    | [ |- _ ] => fail "perm_disj_list_split_in can not be applied."
  end.

Tactic Notation "permlist_split" := perm_disj_list_split.

Tactic Notation "permlist_split" "in" ident(H) :=
  perm_disj_list_split_in H;
  try (apply perm_disj_list_pos; clear H; permlist_solve).

Ltac perm_disj_list_remove q id :=
  match goal with
    | H : perm_disj_list ?T |- _ =>
      match H with
        | id => match T with
            | [q] => apply perm_disj_list_remove_list with [] [q] [] in H; simpl in H
            | [q;?a] => apply perm_disj_list_remove_list with [] [q] [a] in H; simpl in H
            | [?a;q] => apply perm_disj_list_remove_list with [a] [q] [] in H; simpl in H
            | [q;?a;?b] => apply perm_disj_list_remove_list with [] [q] [a;b] in H; simpl in H
            | [?a;q;?b] => apply perm_disj_list_remove_list with [a] [q] [b] in H; simpl in H
            | [?a;?b;q] => apply perm_disj_list_remove_list with [a;b] [q] [] in H; simpl in H
            | [q;?a;?b;?c] => apply perm_disj_list_remove_list with [] [q] [a;b;c] in H; simpl in H
            | [?a;q;?b;?c] => apply perm_disj_list_remove_list with [a] [q] [b;c] in H; simpl in H
            | [?a;?b;q;?c] => apply perm_disj_list_remove_list with [a;b] [q] [c] in H; simpl in H
            | [?a;?b;?c;q] => apply perm_disj_list_remove_list with [a;b;c] [q] [] in H; simpl in H
            | [q;?a;?b;?c;?d] => apply perm_disj_list_remove_list with [] [q] [a;b;c;d] in H; simpl in H
            | [?a;q;?b;?c;?d] => apply perm_disj_list_remove_list with [a] [q] [b;c;d] in H; simpl in H
            | [?a;?b;q;?c;?d] => apply perm_disj_list_remove_list with [a;b] [q] [c;d] in H; simpl in H
            | [?a;?b;?c;q;?d] => apply perm_disj_list_remove_list with [a;b;c] [q] [d] in H; simpl in H
            | [?a;?b;?c;?d;q] => apply perm_disj_list_remove_list with [a;b;c;d] [q] [] in H; simpl in H
            | [q;?a;?b;?c;?d;?e] => apply perm_disj_list_remove_list with [] [q] [a;b;c;d;e] in H; simpl in H
            | [?a;q;?b;?c;?d;?e] => apply perm_disj_list_remove_list with [a] [q] [b;c;d;e] in H; simpl in H
            | [?a;?b;q;?c;?d;?e] => apply perm_disj_list_remove_list with [a;b] [q] [c;d;e] in H; simpl in H
            | [?a;?b;?c;q;?d;?e] => apply perm_disj_list_remove_list with [a;b;c] [q] [d;e] in H; simpl in H
            | [?a;?b;?c;?d;q;?e] => apply perm_disj_list_remove_list with [a;b;c;d] [q] [e] in H; simpl in H
            | [?a;?b;?c;?d;?e;q] => apply perm_disj_list_remove_list with [a;b;c;d;e] [q] [] in H; simpl in H
            | _ => fail "perm_disj_list_remove does not apply here."
          end
        | _ => fail "perm_disj_list_remove does not apply here."
      end
    | [ |- _ ] => fail "perm_disj_list_remove does not apply here."
  end.

Tactic Notation "permlist_remove" constr(q) "in" ident(H) := perm_disj_list_remove q H.