Module ResourcesReconfiguration

Set Implicit Arguments.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import List.
Require Import Coq.Sorting.Permutation.
Require Import MyTactics.
Require Import Resources.

This is perhaps not really necessary, but it helps to fix the type of resources.

Require Import ResourcesContinued.

My view of star as a three-place relation can be really heavyweight when it comes to reconfiguring resources. Typically, one starts with a tree where each internal node represents an instance of star, and one would like to reconfigure this tree into a different shape, with the same multiset of leaves. Doing this by hand is next to impossible as soon as the trees have more than two nodes. In this file, I develop an automated tactic for reconfiguration.

In doing so, I use stronger properties of star than just commutativity and associativity. I use the fact that star is deterministic, that is, it coincides with the function add where it is defined. I use the fact that add is commutative and associative, everywhere, even where star is not defined. I introduce a notion of compatibility between resources, and I use the fact that it behaves well with respect to star.

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

Trees.

A tree is a data structure that reflects a conjunction of star assertions.

Inductive tree (A : Type) :=
| Leaf: A -> tree A
| Node: tree A -> tree A -> tree A.

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

The fringe of a tree.

Our trees have non-empty fringes, so we return the fringe as a pair of an element and a list. This allows us to fold over the fringe without providing a seed.

Fixpoint fringe A (t : tree A) : A * list A :=
  match t with
  | Leaf a => (a, nil)
  | Node t1 t2 =>
      let (a1, tail1) := fringe t1 in
      let (a2, tail2) := fringe t2 in
      (a1, tail1 ++ a2 :: tail2)
  end.

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

Interpreting trees according to a binary operator op.

Fixpoint interpret A (op : A -> A -> A) (t : tree A) : A :=
  match t with
  | Leaf a => a
  | Node t1 t2 => op (interpret op t1) (interpret op t2)
  end.

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

A tree can also be interpreted via its fringe. If op is commutative and associative, this yields an identical result.

Definition interpret_fringe A (op : A -> A -> A) (t : tree A) : A :=
  let (a, tail) := fringe t in
  fold_left op tail a.

Lemma interpret_fringe_correct:
  forall A (op : A -> A -> A),
  (forall a1 a2, op a1 a2 = op a2 a1) ->
  (forall a1 a2 a3, op a1 (op a2 a3) = op (op a1 a2) a3) ->
  forall t,
  interpret op t = interpret_fringe op t.

Proof.

  introv a c.
  unfold interpret_fringe. induction t; simpl; eauto.
  rewrite IHt1. rewrite IHt2. clear IHt1 IHt2.
  destruct (fringe t1) as [ a1 tail1 ]. destruct (fringe t2) as [ a2 tail2 ]. clear t1 t2.
  generalize a1; clear a1. induction tail1; simpl; intro a1.
    generalize a2; clear a2. induction tail2; simpl; intro a2.
      eauto.
      rewrite IHtail2. f_equal. eauto.
    eauto.
Qed.

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

If two lists are permutations of one another, then folding a commutative and associative operator over them produces the same result.

Lemma ac_fold_permutation:
  forall A (op : A -> A -> A),
  (forall a1 a2, op a1 a2 = op a2 a1) ->
  (forall a1 a2 a3, op a1 (op a2 a3) = op (op a1 a2) a3) ->
  forall (xs ys : list A),
  Permutation xs ys ->
  forall seed,
  fold_left op xs seed = fold_left op ys seed.

Proof.

  introv c a. induction 1; simpl; intro; eauto.
  f_equal. rewrite <- a. rewrite <- a. f_equal. eapply c.
  congruence.
Qed.

Lemma permutation_cons_nil:
  forall A (x : A) (xs : list A),
  Permutation (x :: xs) nil ->
  False.

Proof.

intros. forwards: Permutation_length. eassumption. discriminate.
Qed.

Here is a slightly awkward reformulation of this result, which concerns nonempty lists and does not require a seed.

Lemma ac_fold_permutation_nonempty:
  forall A (op : A -> A -> A),
  (forall a1 a2, op a1 a2 = op a2 a1) ->
  (forall a1 a2 a3, op a1 (op a2 a3) = op (op a1 a2) a3) ->
  forall (xs ys : list A) (x y : A),
  Permutation (x :: xs) (y :: ys) ->
  fold_left op xs x = fold_left op ys y.

Proof.

  introv c a h. dependent induction h.
  eauto using ac_fold_permutation.
  simpl. f_equal. eauto.
  match goal with h: Permutation (_ :: _) ?l |- _ => destruct l as [| z zs ] end. false; eauto using permutation_cons_nil.
  erewrite IHh1; [ idtac | assumption | assumption | reflexivity | reflexivity ]. eauto.
Qed.

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

As a result, two trees whose fringes a permutation of each other have the same interpretation.

Definition fringe_permutation A (t1 t2 : tree A) :=
  let (a1, tail1) := fringe t1 in
  let (a2, tail2) := fringe t2 in
  Permutation (a1 :: tail1) (a2 :: tail2).

Lemma interpret_is_up_to_permutation:
  forall A (op : A -> A -> A),
  (forall a1 a2, op a1 a2 = op a2 a1) ->
  (forall a1 a2 a3, op a1 (op a2 a3) = op (op a1 a2) a3) ->
  forall (t1 t2 : tree A),
  fringe_permutation t1 t2 ->
  interpret op t1 = interpret op t2.

Proof.

  unfold fringe_permutation. intros.
  do 2 (rewrite interpret_fringe_correct; eauto).
  unfold interpret_fringe.
  destruct (fringe t1) as [ a1 tail1 ]. destruct (fringe t2) as [ a2 tail2 ].
  eapply ac_fold_permutation_nonempty; eauto.
Qed.

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

To prove that two lists are permutations of one another, we use the following tactic, which is borrowed from the Coq documentation. The search has exponential time complexity, while the proof term that is produced has quadratic size (I think). The search might even loop if the goal is false. This is pretty bad, but still good enough for our purposes: our resource trees have very few elements, typically at most 4.

One might wish to sort the two lists, but this is impossible, as we are dealing with lists of resources, and there is no ordering over resources.

This tactic works as soon as the list have a closed spine, that is, known length. They need not have known elements, i.e., their elements can be variables.

Lemma permut_append:
forall (A : Type) (x : A) (xs : list A),
Permutation (x :: xs) (xs ++ x :: nil).

Proof.

intros. eapply Permutation_cons_app. rewrite <- app_nil_end. eapply Permutation_refl.
Qed.

Ltac Permut n :=
  match goal with
  | |- (@Permutation _ ?l ?l) =>
      apply Permutation_refl
  | |- (@Permutation _ (?a :: ?l1) (?a :: ?l2)) =>
      let newn := eval compute in (length l1) in
      (apply perm_skip; Permut newn)
  | |- (@Permutation ?A (?a :: ?l1) ?l2) =>
      match eval compute in n with
      | 1 =>

we are looking at two singleton lists; if their elements were equal, the above cases would have succeeded; so, they are different; fail.

fail
| _ =>

The first elements do not match; perform a rotation of the first list and try again.

          let l1' := constr:(l1 ++ a :: nil) in
          (apply (@perm_trans A (a :: l1) l1' l2);
            [ apply permut_append | compute; Permut (pred n) ])
      end
  end.

Ltac PermutProve :=
  match goal with
  | |- (@Permutation _ ?l1 ?l2) =>
      match eval compute in (length l1 = length l2) with
      | (?n = ?n) => Permut n
      end
  end.

Goal
  Permutation (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).

Proof.

PermutProve.
Qed.

Goal
forall (A : Type) (x y z : A), Permutation (x :: y :: z :: nil) (z :: y :: x :: nil).

Proof.

intros. PermutProve.
Qed.

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

This yields a tactic to prove that two trees (with known shape) have the same fringe up to a permutation.

Ltac TreeProve :=
  unfold fringe_permutation; simpl; PermutProve.

Goal
   forall (A : Type) (x y z : A),
   fringe_permutation
     (Node (Leaf x) (Node (Leaf y) (Leaf z)))
     (Node (Node (Leaf z) (Leaf y)) (Leaf x)).

Proof.

intros. TreeProve.
Qed.

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

The assertion leaf a t means that a is a leaf of t.

Inductive leaf (A : Type) : A -> tree A -> Prop :=
| LeafLeaf:
    forall a, leaf a (Leaf a)
| LeafNodeLeft:
    forall a t1 t2, leaf a t1 -> leaf a (Node t1 t2)
| LeafNodeRight:
    forall a t1 t2, leaf a t2 -> leaf a (Node t1 t2).

Hint Constructors leaf : tree.

Assertions of the form leaf a t, where t is a concrete tree, are proven easily by eauto. Here is an example.

Goal leaf 2 (Node (Leaf 1) (Node (Leaf 2) (Leaf 3))).

Proof.

eauto with tree.
Qed.

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

Compatibility.

Two resources are compatible if their separating conjunction is defined.

Definition compatible (R1 R2 : resource) :=
  exists R, star R1 R2 R.

Lemma star_compatible:
  forall R1 R2 R,
  star R1 R2 R ->
  compatible R1 R2.

Proof.

unfold compatible. eauto.
Qed.

Lemma compatible_commutative:
  forall R1 R2,
  compatible R1 R2 ->
  compatible R2 R1.

Proof.

unfold compatible. intros. unpack. eauto using (@star_commutative resource).
Qed.

Because star is deterministic, compatibility can be phrased as follows.

Lemma compatible_star_add:
  forall R1 R2,
  compatible R1 R2 ->
  star R1 R2 (add R1 R2).

Proof.

unfold compatible. intros. unpack. star_deterministic. eauto.
Qed.

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

Validity.

Because star is deterministic -- it corresponds to the function add -- a resource tree can be interpreted, or evaluated, to yield a resource that corresponds to the root of the tree.

Definition interpret_tree (t : tree resource) : resource :=
interpret add t.

However, the function add produces a meaningful result only when its arguments are compatible resources. In other words, the above interpretation is not always meaningful. It makes sense only for valid trees, where each binary node actually corresponds to a well-formed instance of star. Here is one possible definition of validity.

Inductive valid_tree : tree resource -> Prop :=
| ValidLeaf:
    forall R,
    valid_tree (Leaf R)
| ValidNode:
    forall t1 t2,
    valid_tree t1 ->
    valid_tree t2 ->
    star (interpret_tree t1) (interpret_tree t2) (interpret_tree (Node t1 t2)) ->
    valid_tree (Node t1 t2).

The above definition of ValidNode is pleasant when performing inversion, but is a bit too strong when performing construction. The following lemma provides a weaker form of ValidNode. The two forms are equivalent because star is deterministic.

Lemma valid_node:
  forall t1 t2,
  valid_tree t1 ->
  valid_tree t2 ->
  compatible (interpret_tree t1) (interpret_tree t2) ->
  valid_tree (Node t1 t2).

Proof.

intros. econstructor; eauto. eapply compatible_star_add; eauto.
Qed.

Inversion lemmas for validity. These allow eauto to easily prove that any subtree of a valid tree is valid.

Lemma valid_inversion_left:
  forall t1 t2,
  valid_tree (Node t1 t2) ->
  valid_tree t1.

Proof.

introv h. inversion h. auto.
Qed.

Lemma valid_inversion_right:
  forall t1 t2,
  valid_tree (Node t1 t2) ->
  valid_tree t2.

Proof.

introv h. inversion h. auto.
Qed.

Hint Resolve valid_inversion_left valid_inversion_right : tree.

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

Interaction between compatible and star, top-down.

If R1 and R2 are compatible, and if R1 is split, then the pieces are compatible with R2.

Lemma compatible_via_father_left:
  forall R1a R1b R1 R2,
  star R1a R1b R1 ->
  compatible R1 R2 ->
  compatible R1a R2.

Proof.

introv h1 [ R h2 ].

The following is a left permutation, but we haven't defined permute_left yet.

forwards: (@star_associative resource). eapply star_commutative. eexact h1. eexact h2. unpack. star_comm R.
eauto using star_compatible.
Qed.

Lemma compatible_via_father_right:
  forall R1a R1b R1 R2,
  star R1a R1b R1 ->
  compatible R1 R2 ->
  compatible R1b R2.

Proof.

introv h1 [ R h2 ].

The following is a right rotation, but we haven't defined rotate_right yet.

forwards: (@star_associative resource). eexact h1. eexact h2. unpack.
eauto using star_compatible.
Qed.

By induction, this implies that, if the root of some valid tree t1 is compatible with R2, then any leaf of t1 is compatible with R2.

Lemma compatible_via_ancestor:
  forall R1 t1 R2,
  leaf R1 t1 ->
  valid_tree t1 ->
  compatible (interpret_tree t1) R2 ->
  compatible R1 R2.

Proof.

introv h; induction 1; simpl; intros; dependent destruction h;
eauto using compatible_via_father_left, compatible_via_father_right.
Qed.

By symmetry, this implies that, if two valid trees have compatible roots, then any leaf of one is compatible with any leaf of the other.

Lemma compatible_via_ancestors:
  forall R1 R2 t1 t2,
  leaf R1 t1 ->
  leaf R2 t2 ->
  valid_tree t1 ->
  valid_tree t2 ->
  compatible (interpret_tree t1) (interpret_tree t2) ->
  compatible R1 R2.

Proof.

  intros.
  eapply compatible_via_ancestor; try eassumption.
  apply compatible_commutative.
  eapply compatible_via_ancestor; try eassumption.
  eauto using compatible_commutative.
Qed.

In particular, this means that, within a valid tree, if two leaves R1 and R2 have a least common ancestor Node t1 t2, where R1 is leaf of t1 and R2 is a leaf of t2, then R1 and R2 are compatible. (This statement must be carefully phrased, to avoid the case where R1 and R2 are the same leaf.)

Lemma valid_trees_have_compatible_leaves:
  forall R1 R2 t1 t2,
  leaf R1 t1 ->
  leaf R2 t2 ->
  valid_tree (Node t1 t2) ->
  compatible R1 R2.

Proof.

introv ? ? h. dependent destruction h.
eauto using compatible_via_ancestors, star_compatible.
Qed.

The tactic compatibility_rec t proves a goal of the form compatible R1 R2. The tree t must have leaves R1 and R2. The tactic attempts to apply the above lemma at t, and if this fails, goes down into the left-hand or right-hand side. This can be viewed as a naive implementation of searching for the least common ancestor.

Ltac compatibility_rec t :=
  match goal with
  | |- compatible ?R1 ?R2 =>
    match t with
    | Node ?t1 ?t2 =>
      solve [
        apply (@valid_trees_have_compatible_leaves R1 R2 t1 t2); eauto with tree
      | apply compatible_commutative; apply (@valid_trees_have_compatible_leaves R2 R1 t1 t2); eauto with tree
      | compatibility_rec t1
      | compatibility_rec t2
      ]
    end
  end.

The tactic compatibility proves a goal of the form compatible R1 R2. It looks in the context for a hypothesis of the form valid_tree t, where the tree t has leaves R1 and R2.

Ltac compatibility :=
  match goal with
  | |- compatible ?R1 ?R2 =>
    match goal with
    | h: valid_tree ?t |- _ =>
        match type of h with context[?R1] =>
          match type of h with context[?R2] =>
            compatibility_rec t
          end
        end
    end
  end.

Here is an example.

Goal
  forall a b c d : resource,
  valid_tree (Node (Leaf a) (Node (Leaf b) (Leaf c))) ->
  compatible c b /\ compatible a b /\ compatible a c.

Proof.

intros. intuition compatibility.
Qed.

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

Interaction between compatible and star, bottom-up.

According to compatible_split, if R1 is split and if both pieces are compatible with R2, then R1 itself is compatible with R2. This works even if the split is not a valid one, which is nice, as the number of proof obligations would otherwise grow quadratically and we would have to be smarter than we presently are.

Lemma compatible_via_sons_left:
  forall R1a R1b R2,
  compatible R1a R2 ->
  compatible R1b R2 ->
  compatible (add R1a R1b) R2.

Proof.

introv [ R1a2 ha ] [ R1b2 hb ]. exists (add (add R1a R1b) R2).
eapply compatible_split; eassumption.
Qed.

Lemma compatible_via_sons_right:
  forall R1a R1b R2,
  compatible R2 R1a ->
  compatible R2 R1b ->
  compatible R2 (add R1a R1b).

Proof.

eauto using compatible_via_sons_left, compatible_commutative.
Qed.

The above properties mean that it is easy to prove that two trees are compatible. It suffices to decompose them and to prove any leaf of the left-hand tree and any leaf of the right-hand tree are compatible. This is pretty expensive, as the number of compatibility goals at the leaves is quadratic. It is acceptable for small trees.

Lemma compatible_trees_via_sons_left:
  forall t1 t2 t,
  compatible (interpret_tree t1) (interpret_tree t) ->
  compatible (interpret_tree t2) (interpret_tree t) ->
  compatible (interpret_tree (Node t1 t2)) (interpret_tree t).

Proof.

introv ? ?. eapply compatible_via_sons_left; eauto.
Qed.

Lemma compatible_trees_via_sons_right:
  forall t1 t2 t,
  compatible (interpret_tree t) (interpret_tree t1) ->
  compatible (interpret_tree t) (interpret_tree t2) ->
  compatible (interpret_tree t) (interpret_tree (Node t1 t2)).

Proof.

introv ? ?. eapply compatible_via_sons_right; eauto.
Qed.

Lemma compatible_trees_leaves:
  forall R1 R2,
  compatible R1 R2 ->
  compatible (interpret_tree (Leaf R1)) (interpret_tree (Leaf R2)).

Proof.

auto.
Qed.

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

A tactic for proving that two trees are compatible. The goal is reduced to proving compatibility assertions about the leaves.

Ltac compatible_trees :=
  match goal with
  | |- compatible (interpret_tree (Leaf ?R1)) (interpret_tree (Leaf ?R2)) =>
      apply compatible_trees_leaves
  | |- compatible (interpret_tree (Node ?t1 ?t2)) (interpret_tree ?t) =>
      apply compatible_trees_via_sons_left; [ compatible_trees | compatible_trees ]
  | |- compatible (interpret_tree ?t) (interpret_tree (Node ?t1 ?t2)) =>
      apply compatible_trees_via_sons_right; [ compatible_trees | compatible_trees ]
  end.

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

A tactic for proving that a tree is valid. This boils down to checking that every internal node has compatible sons, which itself boils down to proving compatibility assertions about the leaves.

We are now able to prove that the validity of some tree implies the validity of any reconfiguration. Here is an example.

Goal
  forall a b c d e : resource,
  valid_tree (Node (Leaf e) (Node (Node (Leaf b) (Leaf a)) (Node (Leaf d) (Leaf c)))) ->
  valid_tree (Node (Node (Leaf a) (Leaf b)) (Node (Leaf c) (Node (Leaf d) (Leaf e)))).

Proof.

intros. valid_tree; compatibility.
Qed.

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

If two valid trees have the same multiset of leaves, then they have the same root.

Lemma leaves_determine_root:
  forall t1 t2,
  fringe_permutation t1 t2 ->
  interpret_tree t1 = interpret_tree t2.

Proof.

intros. eapply interpret_is_up_to_permutation; eauto. eapply add_commutative. eapply add_associative.
Qed.

Here is an example.

Goal
  forall a b c d e : resource,
  forall t1 t2,
  t1 = Node (Leaf e) (Node (Node (Leaf b) (Leaf a)) (Node (Leaf d) (Leaf c))) ->
  t2 = Node (Node (Leaf a) (Leaf b)) (Node (Leaf c) (Node (Leaf d) (Leaf e))) ->
  interpret_tree t1 = interpret_tree t2.

Proof.

intros. subst. apply leaves_determine_root. TreeProve.
Qed.

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

Another interpretation of trees.

So far, we have interpreted a tree as a resource. For the purposes of reflection, we also need to interpret a tree as a predicate over a resource.

Fixpoint tree_predicate (t : tree resource) (R : resource) : Prop :=
  match t with
  | Leaf R0 =>
      R = R0
  | Node t1 t2 =>
      exists R1 R2, star R1 R2 R /\ tree_predicate t1 R1 /\ tree_predicate t2 R2
  end.

Naturally, the two interpretations are equivalent.

The resource at the root of a valid tree t satisfies the predicate associated with t.

Lemma equivalence_1:
  forall t,
  valid_tree t ->
  tree_predicate t (interpret_tree t).

Proof.

  induction 1.
  reflexivity.
  simpl in *. eauto.
Qed.

Conversely, if some resource R satisfies the predicate associated with t, then R is the resource at the root of t, and t is valid.

Lemma equivalence_2:
  forall t R,
  tree_predicate t R ->
  R = interpret_tree t /\ valid_tree t.

Proof.

  induction t; introv h; unpack.
  split. auto. constructor.
  destruct h as [ ? [ ? [ ? [ ? ? ]]]].
  forwards: IHt1. eassumption. unpack.
  forwards: IHt2. eassumption. unpack.
  subst.
  assert (keep: forall A B : Prop, A -> (A -> B) -> A /\ B). tauto. apply keep.
  apply star_deterministic. auto.
  intro. constructor; auto. congruence.
Qed.

By combining the two directions, we find that if R is at the root of t1, and if t2 is a valid reconfiguration of t1, then R is at the root of t2.

Lemma reconfiguration:
  forall t1 t2 R,
  tree_predicate t1 R ->
  valid_tree t2 ->
  fringe_permutation t1 t2 ->
  tree_predicate t2 R.

Proof.

  introv ? valid2 ?.
  forwards [ root1 valid1 ] : equivalence_2. eassumption.
  rewrite root1.
  forwards roots: leaves_determine_root. eassumption.
  rewrite roots.
  apply equivalence_1. assumption.
Qed.

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

This leads us to the main tactic. The user must provide the trees t1 and t2 as well as (the name of) the resource found at the root of t1. The tactic checks that the context contains a number of star hypotheses that correspond to t1. It then reconfigures to t2, producing a new set of star assertions, with the same resource R at their root.

Ltac reconfig t1 t2 R :=
  assert (reconfig1: tree_predicate t1 R); [
    simpl; intuition eauto 30 |
  assert (reconfig2: valid_tree t1); [
    eapply equivalence_2; eassumption |
  assert (reconfig3: valid_tree t2); [
    valid_tree; compatibility |
  assert (reconfig4: tree_predicate t2 R); [
    eapply reconfiguration; [
      eassumption |
      eassumption |
      TreeProve
    ] |
  clear reconfig1 reconfig2 reconfig3;
  simpl in reconfig4;
  unpack; subst
  ]]]].

Here is an example.

Goal
  forall a b ab c abc : resource,
  star a b ab ->
  star ab c abc ->
  exists ca,
  star c a ca /\
  star b ca abc.

Proof.

  intros.
  reconfig
    (Node (Node (Leaf a) (Leaf b)) (Leaf c))
    (Node (Leaf b) (Node (Leaf c) (Leaf a)))
    abc.
  intuition eauto.
Qed.

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

To make things slightly more comfortable and make the tactic even more high-tech, we can actually build t1 automatically, just by examining the star hypotheses in the context.

Ltac reflect R :=
  match goal with
  | h: star ?R1 ?R2 R |- _ =>
      let t1 := reflect R1 in
      let t2 := reflect R2 in
      constr:(Node t1 t2)
  | _ =>
      constr:(Leaf R)
  end.

Ltac reconfigure R t2 :=
  let t1 := reflect R in
  reconfig t1 t2 R.

Goal
  forall a b ab c abc : resource,
  star a b ab ->
  star ab c abc ->
  exists ca,
  star c a ca /\
  star b ca abc.

Proof.

  intros.
  reconfigure abc (Node (Leaf b) (Node (Leaf c) (Leaf a))).
  intuition eauto.
Qed.

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

Some simple reconfiguration patterns are common enough that we name them.

We use lemmas, because the use of lemmas is more efficient and predictable than the direct use of tactics. Do not attempt to eliminate these lemmas: defining the tactics below as abbreviations for certain uses of reconfigure would be a bad idea.

Right rotation. This is in fact exactly the associativity of star. Before: R / \ /\ R3 R1 R2 After: R / \ R1 /\ R2 R3

Lemma rotate_right:
  forall { R1 R2 R3 x R : resource },
  star R1 R2 x ->
  star x R3 R ->
  exists y,
  star R2 R3 y /\
  star R1 y R.

Proof.

intros. reconfigure R (Node (Leaf R1) (Node (Leaf R2) (Leaf R3))). eauto.
Qed.

Ltac rotate_right :=
  match goal with h1: star ?R1 ?R2 ?x, h2: star ?x ?R3 ?R |- _ =>
    unpack (rotate_right h1 h2)
  end.

Left rotation. This is the inverse of the right rotation. Before: R / \ R1 /\ R2 R3 After: R / \ /\ R3 R1 R2

Lemma rotate_left:
  forall { R1 R2 R3 y R : resource },
  star R1 y R ->
  star R2 R3 y ->
  exists x,
  star R1 R2 x /\
  star x R3 R.

Proof.

intros. reconfigure R (Node (Node (Leaf R1) (Leaf R2)) (Leaf R3)). eauto.
Qed.

Ltac rotate_left :=
  match goal with h1: star ?R1 ?x ?R, h2: star ?R2 ?R3 ?x |- _ =>
    unpack (rotate_left h1 h2)
  end.

Left permutation. Before: R / \ /\ R3 R1 R2 After: R / \ /\ R2 R1 R3

Lemma permute_left:
  forall { R1 R2 R3 x R : resource },
  star R1 R2 x ->
  star x R3 R ->
  exists y,
  star R1 R3 y /\
  star y R2 R.

Proof.

intros. reconfigure R (Node (Node (Leaf R1) (Leaf R3)) (Leaf R2)). eauto.
Qed.

Ltac permute_left :=
  match goal with h1: star ?R1 ?R2 ?x, h2: star ?x ?R3 ?R |- _ =>
    unpack (permute_left h1 h2)
  end.