LibSepSimplAppendix - Simplification of Entailments

Set Implicit Arguments.
From SLF Require Export LibCore.
From SLF Require Export LibSepTLCbuffer.

A Functor for Separation Logic Entailment

This file consists of a functor that provides a tactic for simplifying entailment relations. This tactic is somewhat generic in that it can be used for several variants of Separation Logic, hence the use of a functor to implement the tactic with respect to abstract definitions of heap predicates.
The file provides a number of lemmas that hold in any variant of Separation Logic satisfying the requirements of the functor. It also provides the following key tactics:
  • xsimpl simplifies heap entailments.
  • xpull is a restricted version of xsimpl that only act over the left-hand side of the entailment, leaving the right-hand side unmodified.
  • xchange performs transitivity steps in entailments, it enables replacing a subset of the heap predicates on the right-hand side with another set of heap predicates entailed by the former.
Bonus: the tactic rew_heap normalizes heap predicate expressions; it is not used in the course.

Assumptions of the functor

Module Type XsimplParams.

Operators

The notion of heap predicate and entailment must be provided.
Parameter hprop : Type.
Parameter himpl : hprop → hprop → Prop.
Definition qimpl A (Q1 Q2:A→hprop) :=
  ∀ r, himpl (Q1 r) (Q2 r).
The core operators of Separation Logic must be provided.
Parameter hempty : hprop.
Parameter hstar : hprop → hprop → hprop.
Parameter hpure : Prop → hprop.
Parameter htop : hprop.
Parameter hgc : hprop.
Parameter hwand : hprop → hprop → hprop.
Parameter qwand : ∀ A, (A→hprop) → (A→hprop) → hprop.
Parameter hexists : ∀ A, (A→hprop) → hprop.
Parameter hforall : ∀ A, (A→hprop) → hprop.
The predicate haffine must be provided. For a fully linear logic, use the always-false predicate. For a fully affine logic, use the always-true predicate.
Parameter haffine : hprop → Prop.

Notation

The following notation is used for stating the required properties.
Declare Scope heap_scope.
Notation "H1 ==> H2" := (himpl H1 H2)
  (at level 55) : heap_scope.
Notation "Q1 ===> Q2" := (qimpl Q1 Q2)
  (at level 55) : heap_scope.
Notation "\[]" := (hempty)
  (at level 0) : heap_scope.
Notation "\[ P ]" := (hpure P)
  (at level 0, format "\[ P ]") : heap_scope.
Notation "\Top" := (htop) : heap_scope.
Notation "\GC" := (hgc) : heap_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
  (at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" := (fun x ⇒ hstar (Q x) H)
  (at level 40) : heap_scope.
Notation "H1 \−∗ H2" := (hwand H1 H2)
  (at level 43, right associativity) : heap_scope.
Notation "Q1 \−−∗ Q2" := (qwand Q1 Q2)
  (at level 43) : heap_scope.
Notation "'\exists' x1 .. xn , H" :=
  (hexists (fun x1 ⇒ .. (hexists (fun xn ⇒ H)) ..))
  (at level 39, x1 binder, H at level 50, right associativity,
   format "'[' '\exists' '/ ' x1 .. xn , '/ ' H ']'") : heap_scope.
Notation "'\forall' x1 .. xn , H" :=
  (hforall (fun x1 ⇒ .. (hforall (fun xn ⇒ H)) ..))
  (at level 39, x1 binder, H at level 50, right associativity,
   format "'[' '\forall' '/ ' x1 .. xn , '/ ' H ']'") : heap_scope.
Local Open Scope heap_scope.

Properties Assumed by the Functor

The following properties must be satisfied.
Implicit Types P : Prop.
Implicit Types H : hprop.
Entailment must be an order.
Parameter himpl_refl : ∀ H,
  H ==> H.
Parameter himpl_trans : ∀ H2 H1 H3,
  (H1 ==> H2) →
  (H2 ==> H3) →
  (H1 ==> H3).
Parameter himpl_antisym : ∀ H1 H2,
  (H1 ==> H2) →
  (H2 ==> H1) →
  (H1 = H2).
The star and the empty heap predicate must form a commutative monoid.
Parameter hstar_hempty_l : ∀ H,
  \[] \* H = H.
Parameter hstar_hempty_r : ∀ H,
  H \* \[] = H.
Parameter hstar_comm : ∀ H1 H2,
   H1 \* H2 = H2 \* H1.
Parameter hstar_assoc : ∀ H1 H2 H3,
  (H1 \* H2) \* H3 = H1 \* (H2 \* H3).
The frame property for entailment must hold.
Parameter himpl_frame_lr : ∀ H1 H1' H2 H2',
  H1 ==> H1' →
  H2 ==> H2' →
  (H1 \* H2) ==> (H1' \* H2').
Parameter himpl_hstar_trans_l : ∀ H1 H2 H3 H4,
  H1 ==> H2 →
  H2 \* H3 ==> H4 →
  H1 \* H3 ==> H4.
Characterization of hpure
Parameter himpl_hempty_hpure : ∀ P,
  P →
  \[] ==> \[P].
Parameter himpl_hstar_hpure_l : ∀ P H H',
  (P → H ==> H') →
  (\[P] \* H) ==> H'.
Characterization of hexists
Parameter himpl_hexists_l : ∀ A H (J:A→hprop),
  (∀ x, J x ==> H) →
  (hexists J) ==> H.
Parameter himpl_hexists_r : ∀ A (x:A) H J,
  (H ==> J x) →
  H ==> (hexists J).
Parameter hstar_hexists : ∀ A (J:A→hprop) H,
  (hexists J) \* H = hexists (fun x ⇒ (J x) \* H).
Characterization of hforall
Parameter himpl_hforall_r : ∀ A (J:A→hprop) H,
  (∀ x, H ==> J x) →
  H ==> (hforall J).
Parameter hstar_hforall : ∀ H A (J:A→hprop),
  (hforall J) \* H ==> hforall (J \*+ H).
Characterization of hwand
Parameter hwand_equiv : ∀ H0 H1 H2,
  (H0 ==> H1 \−∗ H2) ↔ (H1 \* H0 ==> H2).
Parameter hwand_curry_eq : ∀ H1 H2 H3,
  (H1 \* H2) \−∗ H3 = H1 \−∗ (H2 \−∗ H3).
Parameter hwand_hempty_l : ∀ H,
  (\[] \−∗ H) = H.
Characterization of qwand
Parameter qwand_equiv : ∀ H A (Q1 Q2:A→hprop),
  H ==> (Q1 \−−∗ Q2) ↔ (Q1 \*+ H) ===> Q2.
Parameter hwand_cancel : ∀ H1 H2,
  H1 \* (H1 \−∗ H2) ==> H2.
Parameter qwand_specialize : ∀ A (x:A) (Q1 Q2:A→hprop),
  (Q1 \−−∗ Q2) ==> (Q1 x \−∗ Q2 x).
Characterization of htop
Parameter himpl_htop_r : ∀ H,
  H ==> \Top.
Parameter hstar_htop_htop :
  \Top \* \Top = \Top.
Characterization of hgc
Parameter haffine_hempty :
  haffine \[].
Parameter himpl_hgc_r : ∀ H,
  haffine H →
  H ==> \GC.
Parameter hstar_hgc_hgc :
  \GC \* \GC = \GC.
End XsimplParams.

Body of the Functor

When all the assumptions of the functor are statisfied, all the lemmas stated below hold, and all the tactics defined below may be used.
Module XsimplSetup (HP : XsimplParams).
Import HP.
Local Open Scope heap_scope.
Implicit Types H : hprop.
Implicit Types P : Prop.
#[global]
Hint Resolve himpl_refl.

Properties of himpl

Lemma himpl_of_eq : ∀ H1 H2,
  H1 = H2 →
  H1 ==> H2.
Proof. intros. subst. applys¬himpl_refl. Qed.
Lemma himpl_of_eq_sym : ∀ H1 H2,
  H1 = H2 →
  H2 ==> H1.
Proof. intros. subst. applys¬himpl_refl. Qed.

Properties of qimpl

Lemma qimpl_refl : ∀ A (Q:A→hprop),
  Q ===> Q.
Proof using. intros. hnfs*. Qed.
#[global] Hint Resolve qimpl_refl.
Lemma qimpl_trans : ∀ A (Q2 Q1 Q3:A→hprop),
  (Q1 ===> Q2) →
  (Q2 ===> Q3) →
  (Q1 ===> Q3).
Proof using. introv M1 M2. intros v. applys* himpl_trans. Qed.
Lemma qimpl_antisym : ∀ A (Q1 Q2:A→hprop),
  (Q1 ===> Q2) →
  (Q2 ===> Q1) →
  (Q1 = Q2).
Proof using. introv M1 M2. apply fun_ext_1. intros v. applys* himpl_antisym. Qed.

Properties of hstar

Lemma hstar_comm_assoc : ∀ H1 H2 H3,
  H1 \* H2 \* H3 = H2 \* H1 \* H3.
Proof using.
  intros. rewrite <- hstar_assoc.
  rewrite (@hstar_comm H1 H2). rewrite¬hstar_assoc.
Qed.

Representation Predicates

The arrow notation typically takes the form x ~> R x, to indicate that X is the logical value that describes the heap structure x, according to the representation predicate R. It is just a notation for the heap predicate R X x.
Definition repr (A:Type) (S:A→hprop) (x:A) : hprop :=
  S x.
Notation "x '~>' S" := (repr S x)
  (at level 33, no associativity) : heap_scope.
Lemma repr_eq : ∀ (A:Type) (S:A→hprop) (x:A),
  (x ~> S) = (S x).
Proof using. auto. Qed.
x ~> Id X holds when x is equal to X in the empty heap. Id is called the identity representation predicate.
Definition Id {A:Type} (X:A) (x:A) :=
  \[ X = x ].
xrepr_clean simplifies instances of p ~> (fun _ ⇒ _) by unfolding the arrow, but only when the body does not captures mklocally bound variables. This tactic should normally not be used directly
Ltac xrepr_clean_core tt :=
  repeat match goal with ⊢ context C [?p ~> ?E] ⇒
   match E with (fun _ ⇒ _) ⇒
     let E' := eval cbv beta in (E p) in
     let G' := context C [E'] in
     let G := match goal with ⊢ ?G ⇒ G end in
     change G with G' end end.
Tactic Notation "xrepr_clean" :=
  xrepr_clean_core tt.
Lemma repr_id : ∀ A (x X:A),
  (x ~> Id X) = \[X = x].
Proof using. intros. unfold Id. xrepr_clean. auto. Qed.

rew_heap Tactic to Normalize Expressions with hstar

rew_heap removes empty heap predicates, and normalizes w.r.t. associativity of star.
rew_heap_assoc only normalizes w.r.t. associativity. (It should only be used internally for tactic implementation.
Lemma star_post_empty : ∀ B (Q:B→hprop),
  Q \*+ \[] = Q.
Proof using. extens. intros. rewrite* hstar_hempty_r. Qed.
#[global]
Hint Rewrite hstar_hempty_l hstar_hempty_r
            hstar_assoc star_post_empty hwand_hempty_l : rew_heap.
Tactic Notation "rew_heap" :=
  autorewrite with rew_heap.
Tactic Notation "rew_heap" "in" "*" :=
  autorewrite with rew_heap in *.
Tactic Notation "rew_heap" "in" hyp(H) :=
  autorewrite with rew_heap in H.
Tactic Notation "rew_heap" "~" :=
  rew_heap; auto_tilde.
Tactic Notation "rew_heap" "~" "in" "*" :=
  rew_heap in *; auto_tilde.
Tactic Notation "rew_heap" "~" "in" hyp(H) :=
  rew_heap in H; auto_tilde.
Tactic Notation "rew_heap" "*" :=
  rew_heap; auto_star.
Tactic Notation "rew_heap" "*" "in" "*" :=
  rew_heap in *; auto_star.
Tactic Notation "rew_heap" "*" "in" hyp(H) :=
  rew_heap in H; auto_star.
#[global]
Hint Rewrite hstar_assoc : rew_heap_assoc.
Tactic Notation "rew_heap_assoc" :=
  autorewrite with rew_heap_assoc.

Auxiliary Tactics Used by xpull and xsimpl

Ltac remove_empty_heaps_from H :=
  match H with context[ ?H1 \* \[] ] ⇒
    match is_evar_as_bool H1 with
    | false ⇒ rewrite (@hstar_hempty_r H1)
    | true ⇒ let X := fresh in
              set (X := H1);
              rewrite (@hstar_hempty_r X);
              subst X
    end end.
Ltac remove_empty_heaps_haffine tt :=
  repeat match goal with ⊢ haffine ?H ⇒ remove_empty_heaps_from H end.
Ltac remove_empty_heaps_left tt :=
  repeat match goal with ⊢ ?H1 ==> _ ⇒ remove_empty_heaps_from H1 end.
Ltac remove_empty_heaps_right tt :=
  repeat match goal with ⊢ _ ==> ?H2 ⇒ remove_empty_heaps_from H2 end.

Tactics xsimpl and xpull for Heap Entailments

The implementation of the tactics is fairly involved. The high-level specification of the tactic appears in the last appendix of: http://www.chargueraud.org/research/2020/seq_seplogic/seq_seplogic.pdf.

xaffine placeholder

Ltac xaffine_core tt := (* to be generalized lated *)
  try solve [ assumption | apply haffine_hempty ].
Tactic Notation "xaffine" :=
  xaffine_core tt.

Hints for tactics such as xsimpl

Inductive Xsimpl_hint : list Boxer → Type :=
  | xsimpl_hint : ∀ (L:list Boxer), Xsimpl_hint L.
Ltac xsimpl_hint_put L :=
  let H := fresh "Hint" in
  generalize (xsimpl_hint L); intros H.
Ltac xsimpl_hint_next cont :=
  match goal with H: Xsimpl_hint ((boxer ?x)::?L) ⊢ _ ⇒
    clear H; xsimpl_hint_put L; cont x end.
Ltac xsimpl_hint_remove tt :=
  match goal with H: Xsimpl_hint _ ⊢ _ ⇒ clear H end.

Lemmas hstars_reorder_.. to flip an iterated hstar.

hstars_flip tt applies to a goal of the form H1 \* .. \* Hn \* \[]= ?H and instantiates H with Hn \* ... \* H1 \* \[]. If n > 9, the maximum arity supported, the tactic unifies H with the original LHS.
Lemma hstars_flip_0 :
  \[] = \[].
Proof using. auto. Qed.
Lemma hstars_flip_1 : ∀ H1,
  H1 \* \[] = H1 \* \[].
Proof using. auto. Qed.
Lemma hstars_flip_2 : ∀ H1 H2,
  H1 \* H2 \* \[] = H2 \* H1 \* \[].
Proof using. intros. rew_heap. rewrite (hstar_comm H2). rew_heap¬. Qed.
Lemma hstars_flip_3 : ∀ H1 H2 H3,
  H1 \* H2 \* H3 \* \[] = H3 \* H2 \* H1 \* \[].
Proof using. intros. rewrite <- (hstars_flip_2 H1). rew_heap. rewrite (hstar_comm H3). rew_heap¬. Qed.
Lemma hstars_flip_4 : ∀ H1 H2 H3 H4,
  H1 \* H2 \* H3 \* H4 \* \[] = H4 \* H3 \* H2 \* H1 \* \[].
Proof using. intros. rewrite <- (hstars_flip_3 H1). rew_heap. rewrite (hstar_comm H4). rew_heap¬. Qed.
Lemma hstars_flip_5 : ∀ H1 H2 H3 H4 H5,
  H1 \* H2 \* H3 \* H4 \* H5 \* \[] = H5 \* H4 \* H3 \* H2 \* H1 \* \[].
Proof using. intros. rewrite <- (hstars_flip_4 H1). rew_heap. rewrite (hstar_comm H5). rew_heap¬. Qed.
Lemma hstars_flip_6 : ∀ H1 H2 H3 H4 H5 H6,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* \[]
  = H6 \* H5 \* H4 \* H3 \* H2 \* H1 \* \[].
Proof using. intros. rewrite <- (hstars_flip_5 H1). rew_heap. rewrite (hstar_comm H6). rew_heap¬. Qed.
Lemma hstars_flip_7 : ∀ H1 H2 H3 H4 H5 H6 H7,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* \[]
  = H7 \* H6 \* H5 \* H4 \* H3 \* H2 \* H1 \* \[].
Proof using. intros. rewrite <- (hstars_flip_6 H1). rew_heap. rewrite (hstar_comm H7). rew_heap¬. Qed.
Lemma hstars_flip_8 : ∀ H1 H2 H3 H4 H5 H6 H7 H8,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* \[]
  = H8 \* H7 \* H6 \* H5 \* H4 \* H3 \* H2 \* H1 \* \[].
Proof using. intros. rewrite <- (hstars_flip_7 H1). rew_heap. rewrite (hstar_comm H8). rew_heap¬. Qed.
Lemma hstars_flip_9 : ∀ H1 H2 H3 H4 H5 H6 H7 H8 H9,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* \[]
  = H9 \* H8 \* H7 \* H6 \* H5 \* H4 \* H3 \* H2 \* H1 \* \[].
Proof using. intros. rewrite <- (hstars_flip_8 H1). rew_heap. rewrite (hstar_comm H9). rew_heap¬. Qed.
Ltac hstars_flip_lemma i :=
  match number_to_nat i with
  | 0%nat ⇒ constr:(hstars_flip_0)
  | 1%nat ⇒ constr:(hstars_flip_1)
  | 2%nat ⇒ constr:(hstars_flip_2)
  | 3%nat ⇒ constr:(hstars_flip_3)
  | 4%nat ⇒ constr:(hstars_flip_4)
  | 5%nat ⇒ constr:(hstars_flip_5)
  | 6%nat ⇒ constr:(hstars_flip_6)
  | 7%nat ⇒ constr:(hstars_flip_7)
  | 8%nat ⇒ constr:(hstars_flip_8)
  | 9%nat ⇒ constr:(hstars_flip_9)
  | _ ⇒ constr:(hstars_flip_1) (* unsupported *)
  end.
Ltac hstars_arity i Hs :=
  match Hs with
  | \[] ⇒ constr:(i)
  | ?H1 \* ?H2 ⇒ hstars_arity (S i) H2
  end.
Ltac hstars_flip_arity tt :=
  match goal with ⊢ ?HL = ?HR ⇒ hstars_arity 0%nat HL end.
Ltac hstars_flip tt :=
  let i := hstars_flip_arity tt in
  let L := hstars_flip_lemma i in
  eapply L.

Lemmas hstars_pick_... to extract hyps in depth.

hstars_search Hs test applies to an expression Hs of the form either H1 \* ... \* Hn \* \[] or H1 \* ... \* Hn. It invokes the function test i Hi for each of the Hi in turn until the tactic succeeds. In the particular case of invoking test n Hn when there is no trailing \[], the call is of the form test (hstars_last n) Hn where hstars_last is an identity tag.
Definition hstars_last (A:Type) (X:A) := X.
Ltac hstars_search Hs test :=
  let rec aux i Hs :=
    first [ match Hs with ?H \* _ ⇒ test i H end
          | match Hs with _ \* ?Hs' ⇒ aux (S i) Hs' end
          | match Hs with ?H ⇒ test (hstars_last i) H end ] in
  aux 1%nat Hs.
hstars_pick_lemma i returns one of the lemma below, which enables reordering in iterated stars, by extracting the i-th item to bring it to the front.
Lemma hstars_pick_1 : ∀ H1 H,
  H1 \* H = H1 \* H.
Proof using. auto. Qed.
Lemma hstars_pick_2 : ∀ H1 H2 H,
  H1 \* H2 \* H = H2 \* H1 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H1). Qed.
Lemma hstars_pick_3 : ∀ H1 H2 H3 H,
  H1 \* H2 \* H3 \* H = H3 \* H1 \* H2 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H2). applys hstars_pick_2. Qed.
Lemma hstars_pick_4 : ∀ H1 H2 H3 H4 H,
  H1 \* H2 \* H3 \* H4 \* H = H4 \* H1 \* H2 \* H3 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H3). applys hstars_pick_3. Qed.
Lemma hstars_pick_5 : ∀ H1 H2 H3 H4 H5 H,
  H1 \* H2 \* H3 \* H4 \* H5 \* H = H5 \* H1 \* H2 \* H3 \* H4 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H4). applys hstars_pick_4. Qed.
Lemma hstars_pick_6 : ∀ H1 H2 H3 H4 H5 H6 H,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H
  = H6 \* H1 \* H2 \* H3 \* H4 \* H5 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H5). applys hstars_pick_5. Qed.
Lemma hstars_pick_7 : ∀ H1 H2 H3 H4 H5 H6 H7 H,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H
  = H7 \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H6). applys hstars_pick_6. Qed.
Lemma hstars_pick_8 : ∀ H1 H2 H3 H4 H5 H6 H7 H8 H,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H
  = H8 \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H7). applys hstars_pick_7. Qed.
Lemma hstars_pick_9 : ∀ H1 H2 H3 H4 H5 H6 H7 H8 H9 H,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* H
  = H9 \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H.
Proof using. intros. rewrite¬(hstar_comm_assoc H8). applys hstars_pick_8. Qed.
Lemma hstars_pick_last_1 : ∀ H1,
  H1 = H1.
Proof using. auto. Qed.
Lemma hstars_pick_last_2 : ∀ H1 H2,
  H1 \* H2 = H2 \* H1.
Proof using. intros. rewrite¬(hstar_comm). Qed.
Lemma hstars_pick_last_3 : ∀ H1 H2 H3,
  H1 \* H2 \* H3 = H3 \* H1 \* H2.
Proof using. intros. rewrite¬(hstar_comm H2). applys hstars_pick_2. Qed.
Lemma hstars_pick_last_4 : ∀ H1 H2 H3 H4,
  H1 \* H2 \* H3 \* H4 = H4 \* H1 \* H2 \* H3.
Proof using. intros. rewrite¬(hstar_comm H3). applys hstars_pick_3. Qed.
Lemma hstars_pick_last_5 : ∀ H1 H2 H3 H4 H5,
  H1 \* H2 \* H3 \* H4 \* H5 = H5 \* H1 \* H2 \* H3 \* H4.
Proof using. intros. rewrite¬(hstar_comm H4). applys hstars_pick_4. Qed.
Lemma hstars_pick_last_6 : ∀ H1 H2 H3 H4 H5 H6,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6
  = H6 \* H1 \* H2 \* H3 \* H4 \* H5.
Proof using. intros. rewrite¬(hstar_comm H5). applys hstars_pick_5. Qed.
Lemma hstars_pick_last_7 : ∀ H1 H2 H3 H4 H5 H6 H7,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7
  = H7 \* H1 \* H2 \* H3 \* H4 \* H5 \* H6.
Proof using. intros. rewrite¬(hstar_comm H6). applys hstars_pick_6. Qed.
Lemma hstars_pick_last_8 : ∀ H1 H2 H3 H4 H5 H6 H7 H8,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8
  = H8 \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7.
Proof using. intros. rewrite¬(hstar_comm H7). applys hstars_pick_7. Qed.
Lemma hstars_pick_last_9 : ∀ H1 H2 H3 H4 H5 H6 H7 H8 H9,
    H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9
  = H9 \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8.
Proof using. intros. rewrite¬(hstar_comm H8). applys hstars_pick_8. Qed.
Ltac hstars_pick_lemma i :=
  let unsupported tt := fail 100 "hstars_pick supports only arity up to 9" in
  match i with
  | hstars_last ?j ⇒ match number_to_nat j with
    | 1%nat ⇒ constr:(hstars_pick_last_1)
    | 2%nat ⇒ constr:(hstars_pick_last_2)
    | 3%nat ⇒ constr:(hstars_pick_last_3)
    | 4%nat ⇒ constr:(hstars_pick_last_4)
    | 5%nat ⇒ constr:(hstars_pick_last_5)
    | 6%nat ⇒ constr:(hstars_pick_last_6)
    | 7%nat ⇒ constr:(hstars_pick_last_7)
    | 8%nat ⇒ constr:(hstars_pick_last_8)
    | 9%nat ⇒ constr:(hstars_pick_last_9)
    | _ ⇒ unsupported tt
    end
  | ?j ⇒ match number_to_nat j with
    | 1%nat ⇒ constr:(hstars_pick_1)
    | 2%nat ⇒ constr:(hstars_pick_2)
    | 3%nat ⇒ constr:(hstars_pick_3)
    | 4%nat ⇒ constr:(hstars_pick_4)
    | 5%nat ⇒ constr:(hstars_pick_5)
    | 6%nat ⇒ constr:(hstars_pick_6)
    | 7%nat ⇒ constr:(hstars_pick_7)
    | 8%nat ⇒ constr:(hstars_pick_8)
    | 9%nat ⇒ constr:(hstars_pick_9)
    | _ ⇒ unsupported tt
    end
  end.

Documentation for the Tactic xsimpl

... doc for xsimpl to update
At the end, there remains a heap entailment with a simplified LHS and a simplified RHS, with items not cancelled out. At this point, if the goal is of the form H ==> \GC or H ==> \Top or H ==> ?H' for some evar H', then xsimpl solves the goal. Else, it leaves whatever remains.
For the cancellation part, xsimpl cancels out H from the LHS with H' from the RHS if either H' is syntactically equal to H, or if H and H' both have the form x ~> ... for the same x. Note that, in case of a mismatch with x ~> R X on the LHS and x ~> R' X' on the RHS, xsimpl will produce a goal of the form (x ~> R X) = (x ~> R' X') which will likely be unsolvable. It is the user's responsability to perform the appropriate conversion steps prior to calling xsimpl.
Remark: the reason for the special treatment of x ~> ... is that it is very useful to be able to automatically cancel out x ~> R X from the LHS with x ~> R ?Y, for some evar ?Y which typically is introduced from an existential, e.g. \∃ Y, x ~> R Y.
Remark: importantly, xsimpl does not attempt any simplification on a representation predicate of the form ?x ~> ..., when the ?x is an uninstantiated evar. Such situation may arise for example with the following RHS: \∃ p, (r ~> Ref p) \* (p ~> Ref 3).
As a special feature, xsimpl may be provided optional arguments for instantiating the existentials (instead of introducing evars). These optional arguments need to be given in left-right order, and are used on a first-match basis: the head value is used if its type matches the type expected by the existential, else an evar is introduced for that existential.
Xsimpl (Hla, Hlw, Hlt) (Hra, Hrg, Hrt) is interepreted as the entailment Hla \* Hlw \* Hlt ==> Hra \* Hrg \* Hrt where
  • Hla denotes "cleaned up" items from the left hand side
  • Hlw denotes the H1 \−∗ H2 and Q1 \−−∗ Q2 items from the left hand side
  • Hlt denotes the remaining items to process items from the left hand side
  • Hra denotes "cleaned up" items from the right hand side
  • Hrg denotes the \GC and \Top items from the right hand side
  • Hrt denotes the remaining items to process from the right hand side
Note: we assume that all items consist of iterated hstars, and are always terminated by an empty heap.
Definition Xsimpl (HL HR:hprop*hprop*hprop) :=
  let '(Hla,Hlw,Hlt) := HL in
  let '(Hra,Hrg,Hrt) := HR in
  Hla \* Hlw \* Hlt ==> Hra \* Hrg \* Hrt.
protect X is use to prevent xsimpl from investigating inside X
Definition protect (A:Type) (X:A) : A := X.
Auxiliary lemmas to prove lemmas for xsimpl implementation.
Lemma Xsimpl_trans_l : ∀ Hla1 Hlw1 Hlt1 Hla2 Hlw2 Hlt2 HR,
  Xsimpl (Hla2,Hlw2,Hlt2) HR →
  Hla1 \* Hlw1 \* Hlt1 ==> Hla2 \* Hlw2 \* Hlt2 →
  Xsimpl (Hla1,Hlw1,Hlt1) HR.
Proof using.
  introv M1 E. destruct HR as [[Hra Hrg] Hrt]. unfolds Xsimpl.
  applys* himpl_trans M1.
Qed.
Lemma Xsimpl_trans_r : ∀ Hra1 Hrg1 Hrt1 Hra2 Hrg2 Hrt2 HL,
  Xsimpl HL (Hra2,Hrg2,Hrt2) →
  Hra2 \* Hrg2 \* Hrt2 ==> Hra1 \* Hrg1 \* Hrt1 →
  Xsimpl HL (Hra1,Hrg1,Hrt1).
Proof using.
  introv M1 E. destruct HL as [[Hla Hlw] Hlt]. unfolds Xsimpl.
  applys* himpl_trans M1.
Qed.
Lemma Xsimpl_trans : ∀ Hla1 Hlw1 Hlt1 Hla2 Hlw2 Hlt2 Hra1 Hrg1 Hrt1 Hra2 Hrg2 Hrt2,
  Xsimpl (Hla2,Hlw2,Hlt2) (Hra2,Hrg2,Hrt2) →
  (Hla2 \* Hlw2 \* Hlt2 ==> Hra2 \* Hrg2 \* Hrt2 →
   Hla1 \* Hlw1 \* Hlt1 ==> Hra1 \* Hrg1 \* Hrt1) →
  Xsimpl (Hla1,Hlw1,Hlt1) (Hra1,Hrg1,Hrt1).
Proof using. introv M1 E. unfolds Xsimpl. eauto. Qed.

Basic cancellation tactic used to establish lemmas used by xsimpl

Lemma hstars_simpl_start : ∀ H1 H2,
  H1 \* \[] ==> \[] \* H2 \* \[] →
  H1 ==> H2.
Proof using. introv M. rew_heap¬in *. Qed.
Lemma hstars_simpl_keep : ∀ H1 Ha H Ht,
  H1 ==> (H \* Ha) \* Ht →
  H1 ==> Ha \* H \* Ht.
Proof using. introv M. rew_heap in *. rewrite¬hstar_comm_assoc. Qed.
Lemma hstars_simpl_cancel : ∀ H1 Ha H Ht,
  H1 ==> Ha \* Ht →
  H \* H1 ==> Ha \* H \* Ht.
Proof using. introv M. rewrite hstar_comm_assoc. applys¬himpl_frame_lr. Qed.
Lemma hstars_simpl_pick_lemma : ∀ H1 H1' H2,
  H1 = H1' →
  H1' ==> H2 →
  H1 ==> H2.
Proof using. introv M. subst¬. Qed.
Ltac hstars_simpl_pick i :=
  (* Remark: the hstars_pick_last lemmas should never be needed here *)
  let L := hstars_pick_lemma i in
  eapply hstars_simpl_pick_lemma; [ apply L | ].
Ltac hstars_simpl_start tt :=
  match goal with ⊢ ?H1 ==> ?H2 ⇒ idtac end;
  applys hstars_simpl_start;
  rew_heap_assoc.
Ltac hstars_simpl_step tt :=
  match goal with ⊢ ?Hl ==> ?Ha \* ?H \* ?H2 ⇒
    first [
      hstars_search Hl ltac:(fun i H' ⇒
        match H' with H ⇒ hstars_simpl_pick i end);
      apply hstars_simpl_cancel
    | apply hstars_simpl_keep ]
  end.
Ltac hstars_simpl_post tt :=
  rew_heap; try apply himpl_refl.
Ltac hstars_simpl_core tt :=
  hstars_simpl_start tt;
  repeat (hstars_simpl_step tt);
  hstars_simpl_post tt.
Tactic Notation "hstars_simpl" :=
  hstars_simpl_core tt.

Transition lemmas

Transition lemmas to start the process
Lemma xpull_protect : ∀ H1 H2,
  H1 ==> protect H2 →
  H1 ==> H2.
Proof using. auto. Qed.
Lemma xsimpl_start : ∀ H1 H2,
  Xsimpl (\[], \[], (H1 \* \[])) (\[], \[], (H2 \* \[])) →
  H1 ==> H2.
Proof using. introv M. unfolds Xsimpl. rew_heap¬in *. Qed.
(* Note: repeat rewrite hstar_assoc after applying this lemma *)
Transition lemmas for LHS extraction operations
Ltac xsimpl_l_start M :=
  introv M;
  match goal with HR: hprop*hprop*hprop ⊢ _ ⇒
    destruct HR as [[Hra Hrg] Hrt]; unfolds Xsimpl end.
Ltac xsimpl_l_start' M :=
  xsimpl_l_start M; applys himpl_trans (rm M); hstars_simpl.
Lemma xsimpl_l_hempty : ∀ Hla Hlw Hlt HR,
  Xsimpl (Hla, Hlw, Hlt) HR →
  Xsimpl (Hla, Hlw, (\[] \* Hlt)) HR.
Proof using. xsimpl_l_start' M. Qed.
Lemma xsimpl_l_hpure : ∀ P Hla Hlw Hlt HR,
  (P → Xsimpl (Hla, Hlw, Hlt) HR) →
  Xsimpl (Hla, Hlw, (\[P] \* Hlt)) HR.
Proof using.
  xsimpl_l_start M. rewrite hstars_pick_3. applys* himpl_hstar_hpure_l.
Qed.
Lemma xsimpl_l_hexists : ∀ A (J:A→hprop) Hla Hlw Hlt HR,
  (∀ x, Xsimpl (Hla, Hlw, (J x \* Hlt)) HR) →
  Xsimpl (Hla, Hlw, (hexists J \* Hlt)) HR.
Proof using.
  xsimpl_l_start M. rewrite hstars_pick_3. rewrite hstar_hexists.
  applys* himpl_hexists_l. intros. rewrite¬<- hstars_pick_3.
Qed.
Lemma xsimpl_l_acc_wand : ∀ H Hla Hlw Hlt HR,
  Xsimpl (Hla, (H \* Hlw), Hlt) HR →
  Xsimpl (Hla, Hlw, (H \* Hlt)) HR.
Proof using. xsimpl_l_start' M. Qed.
Lemma xsimpl_l_acc_other : ∀ H Hla Hlw Hlt HR,
  Xsimpl ((H \* Hla), Hlw, Hlt) HR →
  Xsimpl (Hla, Hlw, (H \* Hlt)) HR.
Proof using. xsimpl_l_start' M. Qed.
Transition lemmas for LHS cancellation operations Hlt is meant to be empty there
Lemma xsimpl_l_cancel_hwand_hempty : ∀ H2 Hla Hlw Hlt HR,
  Xsimpl (Hla, Hlw, (H2 \* Hlt)) HR →
  Xsimpl (Hla, ((\[] \−∗ H2) \* Hlw), Hlt) HR.
Proof using. xsimpl_l_start' M. Qed.
Lemma xsimpl_l_cancel_hwand : ∀ H1 H2 Hla Hlw Hlt HR,
  Xsimpl (\[], Hlw, (Hla \* H2 \* Hlt)) HR →
  Xsimpl ((H1 \* Hla), ((H1 \−∗ H2) \* Hlw), Hlt) HR.
Proof using. xsimpl_l_start' M. applys¬hwand_cancel. Qed.
Lemma xsimpl_l_cancel_qwand : ∀ A (x:A) (Q1 Q2:A→hprop) Hla Hlw Hlt HR,
  Xsimpl (\[], Hlw, (Hla \* Q2 x \* Hlt)) HR →
  Xsimpl ((Q1 x \* Hla), ((Q1 \−−∗ Q2) \* Hlw), Hlt) HR.
Proof using.
  xsimpl_l_start' M. rewrite hstar_comm. applys himpl_hstar_trans_l.
  applys qwand_specialize x. rewrite hstar_comm. applys hwand_cancel.
Qed.
Lemma xsimpl_l_keep_wand : ∀ H Hla Hlw Hlt HR,
  Xsimpl ((H \* Hla), Hlw, Hlt) HR →
  Xsimpl (Hla, (H \* Hlw), Hlt) HR.
Proof using. xsimpl_l_start' M. Qed.
Lemma xsimpl_l_hwand_reorder : ∀ H1 H1' H2 Hla Hlw Hlt HR,
  H1 = H1' →
  Xsimpl (Hla, ((H1' \−∗ H2) \* Hlw), Hlt) HR →
  Xsimpl (Hla, ((H1 \−∗ H2) \* Hlw), Hlt) HR.
Proof using. intros. subst*. Qed.
Lemma xsimpl_l_cancel_hwand_hstar : ∀ H1 H2 H3 Hla Hlw Hlt HR,
  Xsimpl (Hla, Hlw, ((H2 \−∗ H3) \* Hlt)) HR →
  Xsimpl ((H1 \* Hla), (((H1 \* H2) \−∗ H3) \* Hlw), Hlt) HR.
Proof using.
  xsimpl_l_start' M. rewrite hwand_curry_eq. applys hwand_cancel.
Qed.
Lemma xsimpl_l_cancel_hwand_hstar_hempty : ∀ H2 H3 Hla Hlw Hlt HR,
  Xsimpl (Hla, Hlw, ((H2 \−∗ H3) \* Hlt)) HR →
  Xsimpl (Hla, (((\[] \* H2) \−∗ H3) \* Hlw), Hlt) HR.
Proof using. xsimpl_l_start' M. Qed.
Transition lemmas for RHS extraction operations
Ltac xsimpl_r_start M :=
  introv M;
  match goal with HL: hprop*hprop*hprop ⊢ _ ⇒
    destruct HL as [[Hla Hlw] Hlt]; unfolds Xsimpl end.
Ltac xsimpl_r_start' M :=
  xsimpl_r_start M; applys himpl_trans (rm M); hstars_simpl.
Lemma xsimpl_r_hempty : ∀ Hra Hrg Hrt HL,
  Xsimpl HL (Hra, Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, (\[] \* Hrt)).
Proof using. xsimpl_r_start' M. Qed.
Lemma xsimpl_r_hwand_same : ∀ H Hra Hrg Hrt HL,
  Xsimpl HL (Hra, Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, ((H \−∗ H) \* Hrt)).
Proof using. xsimpl_r_start' M. rewrite hwand_equiv. rew_heap¬. Qed.
Lemma xsimpl_r_hpure : ∀ P Hra Hrg Hrt HL,
  P →
  Xsimpl HL (Hra, Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, (\[P] \* Hrt)).
Proof using.
  introv HP. xsimpl_r_start' M. applys* himpl_hempty_hpure.
Qed.
Lemma xsimpl_r_hexists : ∀ A (x:A) (J:A→hprop) Hra Hrg Hrt HL,
  Xsimpl HL (Hra, Hrg, (J x \* Hrt)) →
  Xsimpl HL (Hra, Hrg, (hexists J \* Hrt)).
Proof using. xsimpl_r_start' M. applys* himpl_hexists_r. Qed.
Lemma xsimpl_r_id : ∀ A (x X:A) Hra Hrg Hrt HL,
  (X = x) →
  Xsimpl HL (Hra, Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, (x ~> Id X \* Hrt)).
Proof using.
  introv →. xsimpl_r_start' M. rewrite repr_id.
  applys* himpl_hempty_hpure.
Qed.
Lemma xsimpl_r_id_unify : ∀ A (x:A) Hra Hrg Hrt HL,
  Xsimpl HL (Hra, Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, (x ~> Id x \* Hrt)).
Proof using. introv M. applys¬xsimpl_r_id. Qed.
Lemma xsimpl_r_keep : ∀ H Hra Hrg Hrt HL,
  Xsimpl HL ((H \* Hra), Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, (H \* Hrt)).
Proof using. xsimpl_r_start' M. Qed.
Transition lemmas for \Top and \GC cancellation
  (* H meant to be \GC or \Top *)
Lemma xsimpl_r_hgc_or_htop : ∀ H Hra Hrg Hrt HL,
  Xsimpl HL (Hra, (H \* Hrg), Hrt) →
  Xsimpl HL (Hra, Hrg, (H \* Hrt)).
Proof using. xsimpl_r_start' M. Qed.
Lemma xsimpl_r_htop_replace_hgc : ∀ Hra Hrg Hrt HL,
  Xsimpl HL (Hra, (\Top \* Hrg), Hrt) →
  Xsimpl HL (Hra, (\GC \* Hrg), (\Top \* Hrt)).
Proof using. xsimpl_r_start' M. applys himpl_hgc_r. xaffine. Qed.
Lemma xsimpl_r_hgc_drop : ∀ Hra Hrg Hrt HL,
  Xsimpl HL (Hra, Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, (\GC \* Hrt)).
Proof using. xsimpl_r_start' M. applys himpl_hgc_r. xaffine. Qed.
Lemma xsimpl_r_htop_drop : ∀ Hra Hrg Hrt HL,
  Xsimpl HL (Hra, Hrg, Hrt) →
  Xsimpl HL (Hra, Hrg, (\Top \* Hrt)).
Proof using. xsimpl_r_start' M. applys himpl_htop_r. Qed.
Transition lemmas for LHS/RHS cancellation meant to be applied when Hlw and Hlt are empty
Ltac xsimpl_lr_start M :=
  introv M; unfolds Xsimpl; rew_heap in *.
Ltac xsimpl_lr_start' M :=
  xsimpl_lr_start M; hstars_simpl;
  try (applys himpl_trans (rm M); hstars_simpl).
Lemma xsimpl_lr_cancel_same : ∀ H Hla Hlw Hlt Hra Hrg Hrt,
  Xsimpl (Hla, Hlw, Hlt) (Hra, Hrg, Hrt) →
  Xsimpl ((H \* Hla), Hlw, Hlt) (Hra, Hrg, (H \* Hrt)).
Proof using. xsimpl_lr_start' M. Qed.
Lemma xsimpl_lr_cancel_htop : ∀ H Hla Hlw Hlt Hra Hrg Hrt,
  Xsimpl (Hla, Hlw, Hlt) (Hra, (\Top \* Hrg), Hrt) →
  Xsimpl ((H \* Hla), Hlw, Hlt) (Hra, (\Top \* Hrg), Hrt).
Proof using.
  xsimpl_lr_start M. rewrite (hstar_comm_assoc Hra) in *.
  rewrite <- hstar_htop_htop. rew_heap. applys himpl_frame_lr M.
  applys himpl_htop_r.
Qed.
Lemma xsimpl_lr_cancel_hgc : ∀ Hla Hlw Hlt Hra Hrg Hrt,
  Xsimpl (Hla, Hlw, Hlt) (Hra, (\GC \* Hrg), Hrt) →
  Xsimpl ((\GC \* Hla), Hlw, Hlt) (Hra, (\GC \* Hrg), Hrt).
Proof using.
  xsimpl_lr_start M. rewrite (hstar_comm_assoc Hra).
  rewrite <- hstar_hgc_hgc at 2. rew_heap.
  applys¬himpl_frame_lr. applys himpl_trans M. hstars_simpl.
Qed.
Lemma xsimpl_lr_cancel_eq : ∀ H1 H2 Hla Hlw Hlt Hra Hrg Hrt,
  (H1 = H2) →
  Xsimpl (Hla, Hlw, Hlt) (Hra, Hrg, Hrt) →
  Xsimpl ((H1 \* Hla), Hlw, Hlt) (Hra, Hrg, (H2 \* Hrt)).
Proof using. introv →. apply¬xsimpl_lr_cancel_same. Qed.
Lemma xsimpl_lr_cancel_eq_repr : ∀ A p (E1 E2:A→hprop) Hla Hlw Hlt Hra Hrg Hrt,
  E1 = E2 →
  Xsimpl (Hla, Hlw, Hlt) (Hra, Hrg, Hrt) →
  Xsimpl (((p ~> E1) \* Hla), Hlw, Hlt) (Hra, Hrg, ((p ~> E2) \* Hrt)).
Proof using. introv M. subst. apply¬xsimpl_lr_cancel_same. Qed.
Lemma xsimpl_lr_hwand : ∀ H1 H2 Hla,
  Xsimpl (\[], \[], (H1 \* Hla)) (\[], \[], H2 \* \[]) →
  Xsimpl (Hla, \[], \[]) ((H1 \−∗ H2) \* \[], \[], \[]).
Proof using.
  xsimpl_lr_start' M. rewrite hwand_equiv.
  applys himpl_trans (rm M). hstars_simpl.
Qed.
Lemma xsimpl_lr_hwand_hfalse : ∀ Hla H1,
  Xsimpl (Hla, \[], \[]) ((\[False] \−∗ H1) \* \[], \[], \[]).
Proof using.
  intros. generalize True. xsimpl_lr_start M. rewrite hwand_equiv.
  applys himpl_hstar_hpure_l. auto_false.
Qed.
Lemma xsimpl_lr_qwand : ∀ A (Q1 Q2:A→hprop) Hla,
  (∀ x, Xsimpl (\[], \[], (Q1 x \* Hla)) (\[], \[], Q2 x \* \[])) →
  Xsimpl (Hla, \[], \[]) ((Q1 \−−∗ Q2) \* \[], \[], \[]).
Proof using.
  xsimpl_lr_start M. rewrite qwand_equiv. intros x.
  specializes M x. rew_heap¬in M.
Qed.
Lemma xsimpl_lr_qwand_unit : ∀ (Q1 Q2:unit→hprop) Hla,
  Xsimpl (\[], \[], (Q1 tt \* Hla)) (\[], \[], (Q2 tt \* \[])) →
  Xsimpl (Hla, \[], \[]) ((Q1 \−−∗ Q2) \* \[], \[], \[]).
Proof using. introv M. applys xsimpl_lr_qwand. intros []. applys M. Qed.
Lemma xsimpl_lr_hforall : ∀ A (J:A→hprop) Hla,
  (∀ x, Xsimpl (\[], \[], Hla) (\[], \[], J x \* \[])) →
  Xsimpl (Hla, \[], \[]) ((hforall J) \* \[], \[], \[]).
Proof using.
  xsimpl_lr_start M. applys himpl_hforall_r. intros x.
  specializes M x. rew_heap¬in M.
Qed.
Lemma himpl_lr_refl : ∀ Hla,
  Xsimpl (Hla, \[], \[]) (Hla, \[], \[]).
Proof using. intros. unfolds Xsimpl. hstars_simpl. Qed.
Lemma himpl_lr_qwand_unify : ∀ A (Q:A→hprop) Hla,
  Xsimpl (Hla, \[], \[]) ((Q \−−∗ (Q \*+ Hla)) \* \[], \[], \[]).
Proof using. intros. unfolds Xsimpl. hstars_simpl. rewrite¬qwand_equiv. Qed.
Lemma himpl_lr_htop : ∀ Hla Hrg,
  Xsimpl (\[], \[], \[]) (\[], Hrg, \[]) →
  Xsimpl (Hla, \[], \[]) (\[], (\Top \* Hrg), \[]).
Proof using.
  xsimpl_lr_start M. rewrite <- (hstar_hempty_l Hla).
  applys himpl_hstar_trans_l M. hstars_simpl. apply himpl_htop_r.
Qed.
Lemma himpl_lr_hgc : ∀ Hla Hrg,
  haffine Hla →
  Xsimpl (\[], \[], \[]) (\[], Hrg, \[]) →
  Xsimpl (Hla, \[], \[]) (\[], (\GC \* Hrg), \[]).
Proof using.
  introv N. xsimpl_lr_start M. rewrite <- (hstar_hempty_l Hla).
  applys himpl_hstar_trans_l M. hstars_simpl. apply* himpl_hgc_r.
Qed.
Lemma xsimpl_lr_exit_nogc : ∀ Hla Hra,
  Hla ==> Hra →
  Xsimpl (Hla, \[], \[]) (Hra, \[], \[]).
Proof using. introv M. unfolds Xsimpl. hstars_simpl. auto. Qed.
Lemma xsimpl_lr_exit : ∀ Hla Hra Hrg,
  Hla ==> Hra \* Hrg →
  Xsimpl (Hla, \[], \[]) (Hra, Hrg, \[]).
Proof using. introv M. unfolds Xsimpl. hstars_simpl. rewrite¬hstar_comm. Qed.
Lemmas to flip accumulators back in place
Lemma xsimpl_flip_acc_l : ∀ Hla Hra Hla' Hrg,
  Hla = Hla' →
  Xsimpl (Hla', \[], \[]) (Hra, Hrg, \[]) →
  Xsimpl (Hla, \[], \[]) (Hra, Hrg, \[]).
Proof using. introv E1 M. subst*. Qed.
Lemma xsimpl_flip_acc_r : ∀ Hla Hra Hra' Hrg,
  Hra = Hra' →
  Xsimpl (Hla, \[], \[]) (Hra', Hrg, \[]) →
  Xsimpl (Hla, \[], \[]) (Hra, Hrg, \[]).
Proof using. introv E1 M. subst*. Qed.
Ltac xsimpl_flip_acc_l tt :=
  eapply xsimpl_flip_acc_l; [ hstars_flip tt | ].
Ltac xsimpl_flip_acc_r tt :=
  eapply xsimpl_flip_acc_r; [ hstars_flip tt | ].
Ltac xsimpl_flip_acc_lr tt :=
  xsimpl_flip_acc_l tt; xsimpl_flip_acc_r tt.

Lemmas to pick the hypothesis to cancel

xsimpl_pick i applies to a goal of the form Xsimpl ((H1 \* .. \* Hi \* .. \* Hn), Hlw, Hlt) HR and turns it into Xsimpl ((Hi \* H1 .. \* H{i-1} \* H{i+1} \* .. \* Hn), Hlw, Hlt) HR.
Lemma xsimpl_pick_lemma : ∀ Hla1 Hla2 Hlw Hlt HR,
  Hla1 = Hla2 →
  Xsimpl (Hla2, Hlw, Hlt) HR →
  Xsimpl (Hla1, Hlw, Hlt) HR.
Proof using. introv M. subst¬. Qed.
Ltac xsimpl_pick i :=
  let L := hstars_pick_lemma i in
  eapply xsimpl_pick_lemma; [ apply L | ].
xsimpl_pick_st f applies to a goal of the form Xsimpl ((H1 \* .. \* Hi \* .. \* Hn), Hlw, Hlt) HR and turns it into Xsimpl ((Hi \* H1 .. \* H{i-1} \* H{i+1} \* .. \* Hn), Hlw, Hlt) HR for the first i such that f Hi returns true.
Ltac xsimpl_pick_st f :=
  match goal with ⊢ Xsimpl (?Hla, ?Hlw, ?Hlt) ?HR ⇒
    hstars_search Hla ltac:(fun i H ⇒
      match f H with true ⇒ xsimpl_pick i end)
  end.
xsimpl_pick_syntactically H is a variant of the above that only checks for syntactic equality, not unifiability.
Ltac xsimpl_pick_syntactically H :=
  xsimpl_pick_st ltac:(fun H' ⇒
    match H' with H ⇒ constr:(true) end).
xsimpl_pick_unifiable H applies to a goal of the form Xsimpl (Hla, Hlw, Hlt) HR, where Hla is of the form H1 \* .. \* Hn \* \[]. It searches for H among the Hi. If it finds it, it moves this Hi to the front, just before H1. Else, it fails.
Ltac xsimpl_pick_unifiable H :=
  match goal with ⊢ Xsimpl (?Hla, ?Hlw, ?Hlt) ?HR ⇒
    hstars_search Hla ltac:(fun i H' ⇒
      unify H H'; xsimpl_pick i)
  end.
xsimpl_pick_same H is a choice for one of the above two, it is the default version used by xsimpl. Syntactic matching is faster but less expressive.
Ltac xsimpl_pick_same H :=
  xsimpl_pick_unifiable H.
xsimpl_pick_applied Q applies to a goal of the form Xsimpl (Hla, Hlw, Hlt) HR, where Hla is of the form H1 \* .. \* Hn \* \[]. It searches for Q ?x among the Hi. If it finds it, it moves this Hi to the front, just before H1. Else, it fails.
Ltac xsimpl_pick_applied Q :=
  xsimpl_pick_st ltac:(fun H' ⇒
    match H' with Q _ ⇒ constr:(true) end).
repr_get_predicate H applies to a H of the form p ~> R _ ... _ and it returns R.
Ltac repr_get_predicate H :=
  match H with ?p ~> ?E ⇒ get_head E end.
xsimpl_pick_repr H applies to a goal of the form Xsimpl (Hla, Hlw, Hlt) HR, where Hla is of the form H1 \* .. \* Hn \* \[], and where H is of the form p ~> R _ (same as repr _ p). It searches for p ~> R _ among the Hi. If it finds it, it moves this Hi to the front, just before H1. Else, it fails.
Ltac xsimpl_pick_repr H :=
  match H with ?p ~> ?E ⇒
    let R := get_head E in
    xsimpl_pick_st ltac:(fun H' ⇒
      match H' with (p ~> ?E') ⇒
        let R' := get_head E' in
        match R' with R ⇒ constr:(true) end end)
  end.

Tactic start and stop

Opaque Xsimpl.
Ltac xsimpl_handle_qimpl tt :=
  match goal with
  | ⊢ @qimpl _ _ ?Q2 ⇒ is_evar Q2; apply qimpl_refl
  | ⊢ @qimpl unit ?Q1 ?Q2 ⇒ let t := fresh "_tt" in intros t; destruct t
  | ⊢ @qimpl _ _ _ ⇒ let r := fresh "r" in intros r
  | ⊢ himpl _ ?H2 ⇒ is_evar H2; apply himpl_refl
  | ⊢ himpl _ _ ⇒ idtac
  | ⊢ @eq hprop _ _ ⇒ applys himpl_antisym
  | ⊢ @eq (_ → hprop) _ _ ⇒ applys fun_ext_1; applys himpl_antisym
  | _ ⇒ fail 1 "not a goal for xsimpl/xpull"
  end.
Ltac xsimpl_intro tt :=
  applys xsimpl_start.
Ltac xpull_start tt :=
  pose ltac_mark;
  intros;
  xsimpl_handle_qimpl tt;
  applys xpull_protect;
  xsimpl_intro tt.
Ltac xsimpl_start tt :=
  pose ltac_mark;
  intros;
  xsimpl_handle_qimpl tt;
  xsimpl_intro tt.
Ltac xsimpl_post_before_generalize tt :=
  idtac.
Ltac xsimpl_post_after_generalize tt :=
  idtac.
Ltac himpl_post_processing_for_hyp H :=
  idtac.
Ltac xsimpl_handle_false_subgoals tt :=
  tryfalse.
Ltac xsimpl_clean tt :=
  try remove_empty_heaps_right tt;
  try remove_empty_heaps_left tt;
  try xsimpl_hint_remove tt.
Ltac gen_until_mark_with_processing_and_cleaning cont :=
  match goal with H: ?T ⊢ _ ⇒
  match T with
  | ltac_Mark ⇒ clear H
  | _ ⇒ cont H;
         let T := type of H in
         generalize H; clear H;
         (* discard non-dependent hyps that are not of type Prop *)
         try (match goal with ⊢ _ → _ ⇒
              match type of T with
              | Prop ⇒ idtac
              | _ ⇒ intros _
              end end);
         gen_until_mark_with_processing cont
  end end.
Ltac xsimpl_generalize tt :=
  xsimpl_post_before_generalize tt;
  xsimpl_handle_false_subgoals tt;
  gen_until_mark_with_processing_and_cleaning
    ltac:(himpl_post_processing_for_hyp);
  xsimpl_post_after_generalize tt.
Ltac xsimpl_post tt :=
  xsimpl_clean tt;
  xsimpl_generalize tt.
Ltac xpull_post tt :=
  xsimpl_clean tt;
  unfold protect;
  xsimpl_generalize tt.

Auxiliary functions step

xsimpl_lr_cancel_eq_repr_post tt is meant to simplify goals of the form E1 = E2 that arises from cancelling p ~> E1 with p ~> E2 in the case where E1 and E2 share the same head symbol, that is, the same representation predicate R.
Ltac xsimpl_lr_cancel_eq_repr_post tt :=
  try fequal; try reflexivity.
  (* Later refined for records *)
xsimpl_r_hexists_apply tt is a tactic to apply xsimpl_r_hexists by exploiting a hint if one is available (see the hint section above) to specify the instantiation of the existential.
(* Note: need to use nrapply instead of eapply to correctly handle \∃ (EA:Enc ?A) *)
Ltac xsimpl_r_hexists_apply tt :=
  first [
    xsimpl_hint_next ltac:(fun x ⇒
      match x with
      | __ ⇒ nrapply xsimpl_r_hexists
      | _ ⇒ apply (@xsimpl_r_hexists _ x)
      end)
  | nrapply xsimpl_r_hexists ].
xsimpl_hook H can be customize to handle cancellation of specific kind of heap predicates (e.g., hsingle).
Ltac xsimpl_hook H := fail.

Tactic step

Ltac xsimpl_hwand_hstars_l tt :=
  match goal with ⊢ Xsimpl (?Hla, ((?H1s \−∗ ?H2) \* ?Hlw), \[]) ?HR ⇒
    hstars_search H1s ltac:(fun i H ⇒
      let L := hstars_pick_lemma i in
      eapply xsimpl_l_hwand_reorder;
      [ apply L
      | match H with
        | \[] ⇒ apply xsimpl_l_cancel_hwand_hstar_hempty
        | _ ⇒ xsimpl_pick_same H; apply xsimpl_l_cancel_hwand_hstar
        end
      ])
  end.
Ltac xsimpl_step_l tt :=
  match goal with ⊢ Xsimpl ?HL ?HR ⇒
  match HL with
  | (?Hla, ?Hlw, (?H \* ?Hlt)) ⇒
    match H with
    | \[] ⇒ apply xsimpl_l_hempty
    | \[?P] ⇒ apply xsimpl_l_hpure; intro
    | ?H1 \* ?H2 ⇒ rewrite (@hstar_assoc H1 H2)
    | hexists ?J ⇒ apply xsimpl_l_hexists; intro
    | ?H1 \−∗ ?H2 ⇒ apply xsimpl_l_acc_wand
    | ?Q1 \−−∗ ?Q2 ⇒ apply xsimpl_l_acc_wand
    | _ ⇒ apply xsimpl_l_acc_other
    end
  | (?Hla, ((?H1 \−∗ ?H2) \* ?Hlw), \[]) ⇒
      match H1 with
      | \[] ⇒ apply xsimpl_l_cancel_hwand_hempty
      | (_ \* _) ⇒ xsimpl_hwand_hstars_l tt
      | _ ⇒ first [ xsimpl_pick_same H1; apply xsimpl_l_cancel_hwand
                   | apply xsimpl_l_keep_wand ]
      end
  | (?Hla, ((?Q1 \−−∗ ?Q2) \* ?Hlw), \[]) ⇒
      first [ xsimpl_pick_applied Q1; eapply xsimpl_l_cancel_qwand
            | apply xsimpl_l_keep_wand ]
  end end.
Ltac xsimpl_hgc_or_htop_cancel cancel_item cancel_lemma :=
  (* Applies to goal of the form:
     match goal with ⊢ Xsimpl (?Hla, \[], \[]) (?Hra, (?H \* ?Hrg), ?Hrt) ⇒ *)
  repeat (xsimpl_pick_same cancel_item; apply cancel_lemma).
Ltac xsimpl_hgc_or_htop_step tt :=
  match goal with ⊢ Xsimpl (?Hla, \[], \[]) (?Hra, ?Hrg, (?H \* ?Hrt)) ⇒
    match constr:((Hrg,H)) with
    | (\[], \GC) ⇒ applys xsimpl_r_hgc_or_htop;
                    xsimpl_hgc_or_htop_cancel (\GC) xsimpl_lr_cancel_hgc
    | (\[], \Top) ⇒ applys xsimpl_r_hgc_or_htop;
                    xsimpl_hgc_or_htop_cancel (\GC) xsimpl_lr_cancel_htop;
                    xsimpl_hgc_or_htop_cancel (\Top) xsimpl_lr_cancel_htop
    | (\GC \* \[], \Top) ⇒ applys xsimpl_r_htop_replace_hgc;
                            xsimpl_hgc_or_htop_cancel (\Top) xsimpl_lr_cancel_htop
    | (\GC \* \[], \GC) ⇒ applys xsimpl_r_hgc_drop
    | (\Top \* \[], \GC) ⇒ applys xsimpl_r_hgc_drop
    | (\Top \* \[], \Top) ⇒ applys xsimpl_r_htop_drop
    end end.
Ltac xsimpl_cancel_same H :=
  xsimpl_pick_same H; apply xsimpl_lr_cancel_same.
Ltac xsimpl_step_r tt :=
  match goal with ⊢ Xsimpl (?Hla, \[], \[]) (?Hra, ?Hrg, (?H \* ?Hrt)) ⇒
  match H with
  | ?H' ⇒ xsimpl_hook H (* else continue *)
  | \[] ⇒ apply xsimpl_r_hempty
  | \[?P] ⇒ apply xsimpl_r_hpure
  | ?H1 \* ?H2 ⇒ rewrite (@hstar_assoc H1 H2)
  | ?H \−∗ ?H'eqH ⇒
      match H with
      | \[?P] ⇒ fail 1 (* don't cancel out cause P might contain a contradiction *)
      | _ ⇒
        match H'eqH with
        | H ⇒ apply xsimpl_r_hwand_same
     (* | protect H => we purposely refuse to unify if proetcted*)
        end
      end
  | hexists ?J ⇒ xsimpl_r_hexists_apply tt
  | \GC ⇒ xsimpl_hgc_or_htop_step tt
  | \Top ⇒ xsimpl_hgc_or_htop_step tt
  | protect ?H' ⇒ apply xsimpl_r_keep
  | protect ?Q' _ ⇒ apply xsimpl_r_keep
  | ?H' ⇒ is_not_evar H; xsimpl_cancel_same H (* else continue *)
  | ?p ~> _ ⇒ xsimpl_pick_repr H; apply xsimpl_lr_cancel_eq_repr;
               [ xsimpl_lr_cancel_eq_repr_post tt | ] (* else continue *)
  | ?x ~> Id ?X ⇒ has_no_evar x; apply xsimpl_r_id
    | ?x ~> ?T_evar ?X_evar ⇒ has_no_evar x; is_evar T_evar; is_evar X_evar;
                           apply xsimpl_r_id_unify
  | _ ⇒ apply xsimpl_r_keep
  end end.
Ltac xsimpl_step_lr tt :=
  match goal with ⊢ Xsimpl (?Hla, \[], \[]) (?Hra, ?Hrg, \[]) ⇒
    match Hrg with
    | \[] ⇒
       match Hra with
       | ?H1 \* \[] ⇒
         match H1 with
         | ?Hra_evar ⇒ is_evar Hra_evar; rew_heap; apply himpl_lr_refl (* else continue *)
         | ?Q1 \−−∗ ?Q2 ⇒ is_evar Q2; eapply himpl_lr_qwand_unify
         | \[False] \−∗ ?H2 ⇒ apply xsimpl_lr_hwand_hfalse
         | ?H1 \−∗ ?H2 ⇒ xsimpl_flip_acc_l tt; apply xsimpl_lr_hwand
         | ?Q1 \−−∗ ?Q2 ⇒
             xsimpl_flip_acc_l tt;
             match H1 with
             | @qwand unit ?Q1' ?Q2' ⇒ apply xsimpl_lr_qwand_unit
             | _ ⇒ apply xsimpl_lr_qwand; intro
             end
         | hforall _ ⇒ xsimpl_flip_acc_l tt; apply xsimpl_lr_hforall; intro
                                 end
       | \[] ⇒ apply himpl_lr_refl
       | _ ⇒ xsimpl_flip_acc_lr tt; apply xsimpl_lr_exit_nogc
       end
    | (\Top \* _) ⇒ apply himpl_lr_htop
    | (\GC \* _) ⇒ apply himpl_lr_hgc;
                    [ try remove_empty_heaps_haffine tt; xaffine | ]
    | ?Hrg' ⇒ xsimpl_flip_acc_lr tt; apply xsimpl_lr_exit
  end end.

Ltac xsimpl_step tt :=
  first [ xsimpl_step_l tt
        | xsimpl_step_r tt
        | xsimpl_step_lr tt ].

Tactic Notation

Ltac xpull_core tt :=
  xpull_start tt;
  repeat (xsimpl_step tt);
  xpull_post tt.
Tactic Notation "xpull" := xpull_core tt.
Tactic Notation "xpull" "~" := xpull; auto_tilde.
Tactic Notation "xpull" "*" := xpull; auto_star.
Ltac xsimpl_core tt :=
  xsimpl_start tt;
  repeat (xsimpl_step tt);
  xsimpl_post tt.
Tactic Notation "xsimpl" := xsimpl_core tt.
Tactic Notation "xsimpl" "~" := xsimpl; auto_tilde.
Tactic Notation "xsimpl" "*" := xsimpl; auto_star.
Tactic Notation "xsimpl" constr(L) :=
  match type of L with
  | list Boxer ⇒ xsimpl_hint_put L
  | _ ⇒ xsimpl_hint_put (boxer L :: nil)
  end; xsimpl.
Tactic Notation "xsimpl" constr(X1) constr(X2) :=
  xsimpl (>> X1 X2).
Tactic Notation "xsimpl" constr(X1) constr(X2) constr(X3) :=
  xsimpl (>> X1 X2 X3).
Tactic Notation "xsimpl" "~" constr(L) :=
  xsimpl L; auto_tilde.
Tactic Notation "xsimpl" "~" constr(X1) constr(X2) :=
  xsimpl X1 X2; auto_tilde.
Tactic Notation "xsimpl" "~" constr(X1) constr(X2) constr(X3) :=
  xsimpl X1 X2 X3; auto_tilde.
Tactic Notation "xsimpl" "*" constr(L) :=
  xsimpl L; auto_star.
Tactic Notation "xsimpl" "*" constr(X1) constr(X2) :=
  xsimpl X1 X2; auto_star.
Tactic Notation "xsimpl" "*" constr(X1) constr(X2) constr(X3) :=
  xsimpl X1 X2 X3; auto_star.

Tactic xchange

xchange performs rewriting on the LHS of an entailment. Essentially, it applies to a goal of the form H1 \* H2 ==> H3, and exploits an entailment H1 ==> H1' to replace the goal with H1' \* H2 ==> H3.
The tactic is actually a bit more flexible in two respects:
  • it does not force the LHS to be exactly of the form H1 \* H2
  • it takes as argument any lemma, whose instantiation result in a heap entailment of the form H1 ==> H1'.
Concretely, the tactic is just a wrapper around an application of the lemma called xchange_lemma, which appears below.
xchanges combines a call to xchange with calls to xsimpl on the subgoals.
Lemma xchange_lemma : ∀ H1 H2 H3 H4,
  H1 ==> H2 →
  H3 ==> H1 \* (H2 \−∗ protect H4) →
  H3 ==> H4.
Proof using.
  introv M1 M2. applys himpl_trans (rm M2).
  applys himpl_hstar_trans_l (rm M1). applys hwand_cancel.
Qed.
Ltac xchange_apply L :=
  eapply xchange_lemma; [ eapply L | ].
(* Below, the modifier is either __ or himpl_of_eq
   or himpl_of_eq_sym *)
Ltac xchange_build_entailment modifier K :=
  match modifier with
  | __ ⇒
     match type of K with
     | _ = _ ⇒ constr:(@himpl_of_eq _ _ K)
     | _ ⇒ constr:(K)
     end
  | _ ⇒ constr:(@modifier _ _ K)
  end.
Ltac xchange_perform L modifier cont :=
  forwards_nounfold_then L ltac:(fun K ⇒
    let X := fresh "TEMP" in
    set (X := K); (* intermediate set seems necessary *)
    let M := xchange_build_entailment modifier K in
    clear X;
    xchange_apply M;
    cont tt).
Ltac xchange_core L modifier cont :=
  pose ltac_mark;
  intros;
  match goal with
  | ⊢ _ ==> _ ⇒ idtac
  | ⊢ _ ===> _ ⇒ let x := fresh "r" in intros x
  end;
  xchange_perform L modifier cont;
  gen_until_mark.
Error reporting support for xchange (not for xchanges)
Definition xchange_hidden (P:Type) (e:P) := e.
Notation "'__XCHANGE_FAILED_TO_MATCH_PRECONDITION__'" :=
  (@xchange_hidden _ _).
Ltac xchange_report_error tt :=
  match goal with ⊢ context [?H1 \−∗ protect ?H2] ⇒
    change (H1 \−∗ protect H2) with (@xchange_hidden _ (H1 \−∗ protect H2)) end.
Ltac xchange_xpull_cont tt :=
  xsimpl; first
  [ xchange_report_error tt
  | unfold protect; try solve [ apply himpl_refl ] ].
Ltac xchange_xpull_cont_basic tt := (* version without error reporting *)
  xsimpl; unfold protect; try solve [ apply himpl_refl ].
Ltac xchange_xsimpl_cont tt :=
  unfold protect; xsimpl; try solve [ apply himpl_refl ].
Ltac xchange_nosimpl_base E modifier :=
  xchange_core E modifier ltac:(idcont).
Tactic Notation "xchange_nosimpl" constr(E) :=
  xchange_nosimpl_base E __.
Tactic Notation "xchange_nosimpl" "->" constr(E) :=
  xchange_nosimpl_base E himpl_of_eq.
Tactic Notation "xchange_nosimpl" "<-" constr(E) :=
  xchange_nosimpl_base himpl_of_eq_sym.
Ltac xchange_base E modif :=
  xchange_core E modif ltac:(xchange_xpull_cont).
Tactic Notation "xchange" constr(E) :=
  xchange_base E __.
Tactic Notation "xchange" "~" constr(E) :=
  xchange E; auto_tilde.
Tactic Notation "xchange" "*" constr(E) :=
  xchange E; auto_star.
Tactic Notation "xchange" "->" constr(E) :=
  xchange_base E himpl_of_eq.
Tactic Notation "xchange" "~" "->" constr(E) :=
  xchange → E; auto_tilde.
Tactic Notation "xchange" "*" "->" constr(E) :=
  xchange → E; auto_star.
Tactic Notation "xchange" "<-" constr(E) :=
  xchange_base E himpl_of_eq_sym.
Tactic Notation "xchange" "~" "<-" constr(E) :=
  xchange <- E; auto_tilde.
Tactic Notation "xchange" "*" "<-" constr(E) :=
  xchange <- E; auto_star.
Ltac xchanges_base E modif :=
  xchange_core E modif ltac:(xchange_xsimpl_cont).
Tactic Notation "xchanges" constr(E) :=
  xchanges_base E __.
Tactic Notation "xchanges" "~" constr(E) :=
  xchanges E; auto_tilde.
Tactic Notation "xchanges" "*" constr(E) :=
  xchanges E; auto_star.
Tactic Notation "xchanges" "->" constr(E) :=
  xchanges_base E himpl_of_eq.
Tactic Notation "xchanges" "~" "->" constr(E) :=
  xchanges → E; auto_tilde.
Tactic Notation "xchanges" "*" "->" constr(E) :=
  xchanges → E; auto_star.
Tactic Notation "xchanges" "<-" constr(E) :=
  xchanges_base E himpl_of_eq_sym.
Tactic Notation "xchanges" "~" "<-" constr(E) :=
  xchanges <- E; auto_tilde.
Tactic Notation "xchanges" "*" "<-" constr(E) :=
  xchanges <- E; auto_star.
Tactic Notation "xchange" constr(E1) "," constr(E2) :=
  xchange E1; try xchange E2.
Tactic Notation "xchange" constr(E1) "," constr(E2) "," constr(E3) :=
  xchange E1; try xchange E2; try xchange E3.
Tactic Notation "xchange" constr(E1) "," constr(E2) "," constr(E3) "," constr(E4) :=
  xchange E1; try xchange E2; try xchange E3; try xchange E4.

Demos

rew_heap demos

Lemma rew_heap_demo_with_evar : ∀ H1 H2 H3,
  (∀ H, H1 \* (H \* H2) \* \[] = H3 → True) → True.
Proof using.
  introv M. dup 3.
  { eapply M. rewrite hstar_assoc. rewrite hstar_assoc. demo. }
  { eapply M. rew_heap_assoc. demo. }
  { eapply M. rew_heap. demo. }
Abort.

hstars demos

Lemma hstars_flip_demo : ∀ H1 H2 H3 H4,
  (∀ H, H1 \* H2 \* H3 \* H4 \* \[] = H → H = H → True) → True.
Proof using.
  introv M. eapply M. hstars_flip tt.
Abort.
Lemma hstars_flip_demo_0 :
  (∀ H, \[] = H → H = H → True) → True.
Proof using.
  introv M. eapply M. hstars_flip tt.
Abort.

xsimpl_hint demos

Lemma xsimpl_demo_hints : ∃ n, n = 3.
Proof using.
  xsimpl_hint_put (>> 3 true).
  xsimpl_hint_next ltac:(fun x ⇒ ∃ x).
  xsimpl_hint_remove tt.
Abort.

hstars_pick demos

Lemma demo_hstars_pick_1 : ∀ H1 H2 H3 H4 Hresult,
  (∀ H, H1 \* H2 \* H3 \* H4 = H → H = Hresult → True) → True.
Proof using.
  introv M. dup 2.
  { eapply M. let L := hstars_pick_lemma 3 in eapply L. demo. }
  { eapply M. let L := hstars_pick_lemma (hstars_last 4) in eapply L. demo. }
Qed.

hstars_simpl demos

Lemma demo_hstars_simpl_1 : ∀ H1 H2 H3 H4 H5,
  H2 ==> H5 →
  H1 \* H2 \* H3 \* H4 ==> H4 \* H5 \* H3 \* H1.
Proof using.
  intros. dup.
  { hstars_simpl_start tt.
    hstars_simpl_step tt.
    hstars_simpl_step tt.
    hstars_simpl_step tt.
    hstars_simpl_step tt.
    hstars_simpl_post tt. auto. }
  { hstars_simpl. auto. }
Qed.
Lemma demo_hstars_simpl_2 : ∀ H1 H2 H3 H4 H5,
  (∀ H, H \* H2 \* H3 \* H4 ==> H4 \* H5 \* H3 \* H1 → True) → True.
Proof using.
  introv M. eapply M. hstars_simpl.
Abort.

xsimpl_pick demos

Lemma xsimpl_pick_demo : ∀ (Q:bool→hprop) (P:Prop) H1 H2 H3 Hlw Hlt Hra Hrg Hrt,
  (∀ HX HY,
    Xsimpl ((H1 \* H2 \* H3 \* Q true \* (\[P] \−∗ HX) \* HY \* \[]), Hlw, Hlt)
           (Hra, Hrg, Hrt)
  → True) → True.
Proof using.
  introv M. applys (rm M).
  let L := hstars_pick_lemma 2%nat in set (X:=L).
  eapply xsimpl_pick_lemma. apply X.
  xsimpl_pick 2%nat.
  xsimpl_pick_same H3.
  xsimpl_pick_applied Q.
  xsimpl_pick_same H2.
  xsimpl_pick_unifiable H3.
  xsimpl_pick_unifiable \[True].
  xsimpl_pick_unifiable (\[P] \−∗ H1).
Abort.

xpull and xsimpl demos

Tactic Notation "xpull0" := xpull_start tt.
Tactic Notation "xsimpl0" := xsimpl_start tt.
Tactic Notation "xsimpl1" := xsimpl_step tt.
Tactic Notation "xsimpl2" := xsimpl_post tt.
Tactic Notation "xsimpll" := xsimpl_step_l tt.
Tactic Notation "xsimplr" := xsimpl_step_r tt.
Tactic Notation "xsimpllr" := xsimpl_step_lr tt.
Declare Scope xsimpl_scope.
Notation "'HSIMPL' Hla Hlw Hlt =====> Hra Hrg Hrt" := (Xsimpl (Hla, Hlw, Hlt) (Hra, Hrg, Hrt))
  (at level 69, Hla, Hlw, Hlt, Hra, Hrg, Hrt at level 0,
   format "'[v' 'HSIMPL' '/' Hla '/' Hlw '/' Hlt '/' =====> '/' Hra '/' Hrg '/' Hrt ']'")
  : xsimpl_scope.
Local Open Scope xsimpl_scope.
Lemma xpull_demo : ∀ H1 H2 H3 H,
  (H1 \* \[] \* (H2 \* \∃ (y:int) z (n:nat), \[y = y + z + n]) \* H3) ==> H.
Proof using.
  dup.
  { intros. xpull0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl2. demo. }
  { xpull. intros. demo. }
Abort.
Lemma xsimpl_demo_stars : ∀ H1 H2 H3 H4 H5,
  H1 \* H2 \* H3 \* H4 ==> H4 \* H3 \* H5 \* H2.
Proof using.
  dup 3.
  { xpull. demo. }
  { intros. xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. demo. }
  { intros. xsimpl. demo. }
Abort.
Lemma xsimpl_demo_keep_order : ∀ H1 H2 H3 H4 H5 H6 H7,
  H1 \* H2 \* H3 \* H4 ==> H5 \* H3 \* H6 \* H7.
Proof using. intros. xsimpl. demo. Abort.
Lemma xsimpl_demo_stars_top : ∀ H1 H2 H3 H4 H5,
  H1 \* H2 \* H3 \* H4 \* H5 ==> H3 \* H1 \* H2 \* \Top.
Proof using.
  dup.
  { intros. xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { intros. xsimpl. }
Abort.
Lemma xsimpl_demo_hint : ∀ H1 (Q:int→hprop),
  Q 4 ==> Q 3 →
  H1 \* Q 4 ==> \∃ x, Q x \* H1.
Proof using.
  introv W. dup.
  { intros. xsimpl_hint_put (>> 3).
    xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl2. auto. }
  { xsimpl 3. auto. }
Qed.
Lemma xsimpl_demo_stars_gc : ∀ H1 H2,
  haffine H2 →
  H1 \* H2 ==> H1 \* \GC.
Proof using.
  dup.
  { intros. xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. }
  { intros. xsimpl¬. }
Abort.
Lemma xsimpl_demo_evar_1 : ∀ H1 H2,
  (∀ H, H1 \* H2 ==> H → True) → True.
Proof using. intros. eapply H. xsimpl. Abort.
Lemma xsimpl_demo_evar_2 : ∀ H1,
  (∀ H, H1 ==> H1 \* H → True) → True.
Proof using.
  introv M. dup.
  { eapply M. xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { eapply M. xsimpl¬. }
Abort.
Lemma xsimpl_demo_htop_both_sides : ∀ H1 H2,
  H1 \* H2 \* \Top ==> H1 \* \Top.
Proof using.
  dup.
  { intros. xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { intros. xsimpl¬. }
Abort.
Lemma xsimpl_demo_htop_multiple : ∀ H1 H2,
  H1 \* H2 \* \Top ==> H1 \* \Top \* \Top.
Proof using. intros. xsimpl¬. Abort.
Lemma xsimpl_demo_hgc_multiple : ∀ H1 H2,
  haffine H2 →
  H1 \* H2 \* \GC ==> H1 \* \GC \* \GC.
Proof using. intros. xsimpl¬. Qed.
Lemma xsimpl_demo_hwand : ∀ H1 H2 H3 H4,
  (H1 \−∗ (H2 \−∗ H3)) \* H1 \* H4 ==> (H2 \−∗ (H3 \* H4)).
Proof using.
  dup.
  { intros. xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { intros. xsimpl¬. }
Qed.
Lemma xsimpl_demo_qwand : ∀ A (x:A) (Q1 Q2:A→hprop) H1,
  H1 \* (H1 \−∗ (Q1 \−−∗ Q2)) \* (Q1 x) ==> (Q2 x).
Proof using. intros. xsimpl¬. Qed.
Lemma xsimpl_demo_hwand_r : ∀ H1 H2 H3,
  H1 \* H2 ==> H1 \* (H3 \−∗ (H2 \* H3)).
Proof using. intros. xsimpl¬. Qed.
Lemma xsimpl_demo_qwand_r : ∀ A (x:A) (Q1 Q2:A→hprop) H1 H2,
  H1 \* H2 ==> H1 \* (Q1 \−−∗ (Q1 \*+ H2)).
Proof using. intros. xsimpl. Qed.
Lemma xsimpl_demo_hwand_multiple_1 : ∀ H1 H2 H3 H4 H5,
  H1 \−∗ H4 ==> H5 →
  (H2 \* ((H1 \* H2 \* H3) \−∗ H4)) \* H3 ==> H5.
Proof using. introv M. xsimpl. auto. Qed.
Lemma xsimpl_demo_hwand_multiple_2 : ∀ H1 H2 H3 H4 H5,
  (H1 \* H2 \* ((H1 \* H3) \−∗ (H4 \−∗ H5))) \* (H2 \−∗ H3) \* H4 ==> H5.
Proof using. intros. xsimpl. Qed.
Lemma xsimpl_demo_hwand_hempty : ∀ H1 H2 H3,
  (\[] \−∗ H1) \* H2 ==> H3.
Proof using. intros. xsimpl. Abort.
Lemma xsimpl_demo_hwand_hstar_hempty : ∀ H0 H1 H2 H3,
  ((H0 \* \[]) \−∗ \[] \−∗ H1) \* H2 ==> H3.
Proof using. intros. xsimpl. rew_heap. Abort.
(* xsimpl does not simplify inner \[] \−∗ H1, known limitation. *)
Lemma xsimpl_demo_hwand_iter : ∀ H1 H2 H3 H4 H5,
  H1 \* H2 \* ((H1 \* H3) \−∗ (H4 \−∗ H5)) \* H4 ==> ((H2 \−∗ H3) \−∗ H5).
Proof using.
  intros. dup.
  { xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { xsimpl. }
Qed.
Lemma xsimpl_demo_repr_1 : ∀ p q (R:int→int→hprop),
  p ~> R 3 \* q ~> R 4 ==> \∃ n m, p ~> R n \* q ~> R m.
Proof using.
  intros. dup.
  { xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { xsimpl¬. }
Qed.
Lemma xsimpl_demo_repr_2 : ∀ p (R R':int→int→hprop),
  R = R' →
  p ~> R' 3 ==> \∃ n, p ~> R n.
Proof using. introv E. xsimpl. subst R'. xsimpl. Qed.
Lemma xsimpl_demo_repr_3 : ∀ p (R:int→int→hprop),
  let R' := R in
  p ~> R' 3 ==> \∃ n, p ~> R n.
Proof using.
  intros. dup.
  { xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { xsimpl¬. }
Qed.
Lemma xsimpl_demo_repr_4 : ∀ p n m (R:int→int→hprop),
  n = m + 0 →
  p ~> R n ==> p ~> R m.
Proof using. intros. xsimpl. math. Qed.
Lemma xsimpl_demo_gc_0 : ∀ H1 H2,
  H1 ==> H2 \* \GC \* \GC.
Proof using. intros. xsimpl. Abort.
Lemma xsimpl_demo_gc_1 : ∀ H1 H2,
  H1 ==> H2 \* \GC \* \Top \* \Top \* \GC.
Proof using.
  intros. dup.
  { xsimpl0. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl2. demo. }
  { xsimpl¬. demo. }
Abort.
Lemma xsimpl_demo_gc_2 : ∀ H1 H2 H3,
  H1 \* H2 \* \Top \* \GC \* \Top ==> H3 \* \GC \* \GC.
Proof using. intros. xsimpl. Abort.
  (* Note that no attempt to collapse \Top or \GC on the RHS is performed,
     they are dealt with only by cancellation from the LHS *)
Lemma xsimpl_demo_gc_3 : ∀ H1 H2,
  H1 \* H2 \* \GC \* \GC ==> H2 \* \GC \* \GC \* \GC.
Proof using. intros. xsimpl. xaffine. Abort.
Lemma xsimpl_demo_gc_4 : ∀ H1 H2,
  H1 \* H2 \* \GC ==> H2 \* \GC \* \Top \* \Top \* \GC.
Proof using. intros. xsimpl. Abort.

xchange demos

Lemma xchange_demo_1 : ∀ H1 H2 H3 H4 H5 H6,
  H1 ==> H2 \* H3 →
  H1 \* H4 ==> (H5 \−∗ H6).
Proof using.
  introv M. dup 3.
  { xchange_nosimpl M. xsimpl. demo. }
  { xchange M. xsimpl. demo. }
  { xchanges M. demo. }
Qed.
Lemma xchange_demo_2 : ∀ A (Q:A→hprop) H1 H2 H3,
  H1 ==> \∃ x, Q x \* (H2 \−∗ H3) →
  H1 \* H2 ==> \∃ x, Q x \* H3.
Proof using.
  introv M. dup 3.
  { xchange_nosimpl M. xsimpl. unfold protect. xsimpl. }
  { xchange M. xsimpl. }
  { xchanges M. }
Qed.
Lemma xchange_demo_4 : ∀ A (Q1 Q2:A→hprop) H,
  Q1 ===> Q2 →
  Q1 \*+ H ===> Q2 \*+ H.
Proof using. introv M. xchanges M. Qed.
Lemma xsimpl_demo_hfalse : ∀ H1 H2,
  H1 ==> \[False] →
  H1 \* H2 ==> \[False].
Proof using.
  introv M. dup.
  { xchange_nosimpl M. xsimpl0. xsimpl1. xsimpl1. xsimpl1.
    xsimpl1. xsimpl1. xsimpl1. xsimpl1. }
  { xchange M. }
Qed.
Lemma xchange_demo_hforall_l :
 ∀ (hforall_specialize : ∀ A (x:A) (J:A→hprop), (hforall J) ==> (J x)),
 ∀ (Q:int→hprop) H1,
  (\∀ x, Q x) \* H1 ==> Q 2 \* \Top.
Proof using.
  intros. xchange (>> hforall_specialize 2). xsimpl.
Qed.
End XsimplSetup.
(* 2023-10-01 07:24 *)