Lemma Triple_is_empty: forall p L,
  Triple (is_empty p)
    (p ~> MList L)
    (fun (r: bool) => \[r = isTrue (L = nil)] \* p ~> MList L).
forall p (L : list credits),
SPEC (is_empty p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : bool =>
       ⟬Star┆⟬Pure┆r = isTrue (L = nil)⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
Proof.
forall p (L : list credits),
SPEC (is_empty p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : bool =>
       ⟬Star┆⟬Pure┆r = isTrue (L = nil)⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
  xwp.
p: loc
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
CODE (`App val_eq p null)
⟬*POST@ fun x : bool =>
        ⟬Star┆⟬Star┆⟬Pure┆x = isTrue (L = nil)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_eq_val.
p: loc
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
isTrue (p = null) = isTrue (L = nil)⟭┆⟬PointsTo┆p┆⟦
$MList ┆ L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ destruct L; rewrite isTrue_eq_isTrue_eq.
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ nil⟧⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
p = null <-> nil = nil⟭┆⟬PointsTo┆p┆⟦$MList ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
p: loc
z: credits
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ z :: L⟧⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
p = null <-> z :: L = nil⟭┆⟬PointsTo┆p┆⟦$MList ┆ z :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  -
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ nil⟧⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
p = null <-> nil = nil⟭┆⟬PointsTo┆p┆⟦$MList ┆ nil⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ rewrite MList_nil.
p: loc
⟬*PRE@⟬Pure┆p = null⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
p = null <-> nil = nil⟭┆⟬Pure┆p = null⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xsimpl*.
  -
p: loc
z: credits
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ z :: L⟧⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
p = null <-> z :: L = nil⟭┆⟬PointsTo┆p┆⟦$MList ┆ z :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xchanges~ MList_cons_not_null.
p: loc
z: credits
L: list credits
H: p <> null
p = null <-> z :: L = nil firstorder; congruence.
Qed.

Lemma Triple_get_elem: forall p x L,
  Triple (get_elem p)
    (p ~> MList (x :: L))
    (fun (r: Z) => \[r = x] \* p ~> MList (x :: L)).
forall p (x : credits) (L : list credits),
SPEC (get_elem p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun r : credits => ⟬Star┆⟬Pure┆r = x⟭┆⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭⟭*⟭
Proof.
forall p (x : credits) (L : list credits),
SPEC (get_elem p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun r : credits => ⟬Star┆⟬Pure┆r = x⟭┆⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭⟭*⟭
  xwp.
p: loc
x: credits
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
CODE (`App (val_get_field head) p)
⟬*POST@ fun x0 : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x0 = x⟭┆⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MList_cons; intros q.
p: loc
x: credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭
CODE (`App (val_get_field head) p)
⟬*POST@ fun x0 : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x0 = x⟭┆⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  mxapp ListNull.Triple_get_head.
p: loc
x: credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆x = x⟭┆⟬PointsTo┆p┆⟦
$MList ┆ x :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  xchanges* <- MList_cons.
Qed.

Lemma Triple_get_next: forall p x L,
  Triple (get_next p)
    (p ~> MList (x :: L))
    (fun (q: loc) => p ~> MCell x q \* q ~> MList L).
forall p (x : credits) (L : list credits),
SPEC (get_next p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun q => ⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦$MList ┆ L⟧⟭⟭*⟭
Proof.
forall p (x : credits) (L : list credits),
SPEC (get_next p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun q => ⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦$MList ┆ L⟧⟭⟭*⟭
  xwp.
p: loc
x: credits
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
CODE (`App (val_get_field tail) p)
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆x0⟧⟭┆⟬PointsTo┆x0┆⟦
        $MList ┆ L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MList_cons; intros q.
p: loc
x: credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭
CODE (`App (val_get_field tail) p)
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆x0⟧⟭┆⟬PointsTo┆x0┆⟦
        $MList ┆ L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  mxapp ListNull.Triple_get_tail.
p: loc
x: credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xsimpl*.
Qed.

Lemma Triple_set_elem: forall p x x' L,
  Triple (set_elem p ``x')
    (p ~> MList (x :: L))
    (fun (_: unit) => p ~> MList (x' :: L)).
forall p (x x' : credits) (L : list credits),
SPEC (set_elem p ``x')
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p┆⟦$MList ┆ x' :: L⟧⟭*⟭
Proof.
forall p (x x' : credits) (L : list credits),
SPEC (set_elem p ``x')
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p┆⟦$MList ┆ x' :: L⟧⟭*⟭
  xwp.
p: loc
x, x': credits
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
CODE (`App (val_set_field head) p (``x'))
⟬*POST@ fun _ : unit => ⟬Star┆⟬PointsTo┆p┆⟦$MList ┆ x' :: L⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MList_cons; intros q.
p: loc
x, x': credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭
CODE (`App (val_set_field head) p (``x'))
⟬*POST@ fun _ : unit => ⟬Star┆⟬PointsTo┆p┆⟦$MList ┆ x' :: L⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
  mxapp ListNull.Triple_set_head.
p: loc
x, x': credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x'┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬PointsTo┆p┆⟦$MList ┆ x' :: L⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
  xchanges <- MList_cons.
Qed.

Lemma Triple_set_next: forall p q' x L,
  Triple (set_next p ``q')
    (p ~> MList (x :: L))
    (fun (_: unit) => p ~> MCell x q' \* \exists q, q ~> MList L).
forall p q' (x : credits) (L : list credits),
SPEC (set_next p ``q')
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun _ : unit =>
       ⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q'⟧⟭┆⟬Exist┆q┆⟬PointsTo┆q┆⟦
       $MList ┆ L⟧⟭⟭⟭*⟭
Proof.
forall p q' (x : credits) (L : list credits),
SPEC (set_next p ``q')
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
⟬*POST@fun _ : unit =>
       ⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q'⟧⟭┆⟬Exist┆q┆⟬PointsTo┆q┆⟦
       $MList ┆ L⟧⟭⟭⟭*⟭
  xwp.
p, q': loc
x: credits
L: list credits
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
CODE (`App (val_set_field tail) p (``q'))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q'⟧⟭┆⟬Exist┆q┆⟬PointsTo┆q┆⟦
        $MList ┆ L⟧⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MList_cons; intros q.
p, q': loc
x: credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭
CODE (`App (val_set_field tail) p (``q'))
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q'⟧⟭┆⟬Exist┆q0┆⟬PointsTo┆q0┆⟦
        $MList ┆ L⟧⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  mxapp ListNull.Triple_set_tail.
p, q': loc
x: credits
L: list credits
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q'⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q'⟧⟭┆⟬Exist┆q0┆⟬PointsTo┆q0┆⟦
$MList ┆ L⟧⟭⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xsimpl.
Qed.

Lemma Triple_size: forall L p,
  Triple (size p)
    (p ~> MList L)
    (fun (r: Z) => \[r = length L] \* p ~> MList L).
forall (L : list credits) p,
SPEC (size p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = length L⟭┆⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭⟭*⟭
Proof.
forall (L : list credits) p,
SPEC (size p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = length L⟭┆⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭⟭*⟭
  induction L as [| x L IH];
    xwp;
    mxapp Triple_is_empty; mxapp Triple_neg; xif; intros; try easy; try solve [mxvals*].
x: credits
L: list credits
IH: forall p,
SPEC (size p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = length L⟭┆⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭⟭*⟭
p: loc
H: x :: L <> nil
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭*⟭
CODE (`Let {A1 EA1} V1 := `Let {A1 EA1} V1 := `App get_next p in
                           `App size (``V1) in
       `App val_add (``V1) 1)
⟬*POST@ fun x0 : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x0 = length (x :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ x :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  mxapp Triple_get_next; intros q.
x: credits
L: list credits
IH: forall p,
SPEC (size p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = length L⟭┆⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭⟭*⟭
p: loc
H: x :: L <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭
CODE (`App size (``q))
⟬*POST@ Bind X : ?A1 In
        `(App val_add (``X) 1)
        ;
        fun x0 : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x0 = length (x :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ x :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp IH.
x: credits
L: list credits
IH: forall p,
SPEC (size p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = length L⟭┆⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭⟭*⟭
p: loc
H: x :: L <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ L⟧⟭┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭⟭*⟭
CODE (`App val_add (``(length L)) 1)
⟬*POST@ fun x0 : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x0 = length (x :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ x :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_add.
x: credits
L: list credits
IH: forall p,
SPEC (size p)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = length L⟭┆⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭⟭*⟭
p: loc
H: x :: L <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ L⟧⟭┆⟬PointsTo┆p┆⟦$MCell┆x┆q⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
length L + 1 = length (x :: L)⟭┆⟬PointsTo┆p┆⟦$MList ┆ x :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  xchanges* <- MList_cons.
Qed.

Lemma Triple_nth: forall L n p,
  n < length L ->
  Triple (nth p (nat_to_Z n))
    (p ~> MList L)
    (fun (r: Z) => \[r = LibList.nth n L] \* p ~> MList L).
forall (L : list credits) (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
Proof.
forall (L : list credits) (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
  induction L;
    simpl; [rewrite length_nil; solve [math] |].
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
forall (n : nat) p,
n < length (a :: L) ->
SPEC (trm_apps nth (p :: n :: nil))
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n (a :: L)⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ a :: L⟧⟭⟭*⟭
  xwp.
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: n < length (a :: L)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭
CODE (`Let b0 := `App val_eq n (0%nat) in
       `If_ b0 Then 
          `App get_elem p
        Else
          `Let {A1 EA1} V1 := `App get_next p in
           `Let {A0 EA0} V0 := `App val_sub n 1 in
            `App nth (``V1) (``V0))
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth n (a :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_eq_val; auto_star.
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: n < (1 + length L)%nat
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭
CODE (`If_ isTrue (n = 0%nat) Then 
         `App get_elem p
       Else
         `Let {A1 EA1} V1 := `App get_next p in
          `Let {A0 EA0} V0 := `App val_sub n 1 in
           `App nth (``V1) (``V0))
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth n (a :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  destruct n; xif; subst; simpl; try easy; intros _.
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
p: loc
H: 0%nat < (1 + length L)%nat
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭
CODE (`App get_elem p)
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth 0 (a :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: S n < (1 + length L)%nat
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭
CODE (`Let {A1 EA1} V1 := `App get_next p in
       `Let {A0 EA0} V0 := `App val_sub (S n) 1 in
        `App nth (``V1) (``V0))
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth (S n) (a :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  -
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
p: loc
H: 0%nat < (1 + length L)%nat
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭
CODE (`App get_elem p)
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth 0 (a :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_get_elem; xsimpl*.
  -
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: S n < (1 + length L)%nat
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭
CODE (`Let {A1 EA1} V1 := `App get_next p in
       `Let {A0 EA0} V0 := `App val_sub (S n) 1 in
        `App nth (``V1) (``V0))
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth (S n) (a :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_get_next; intros q.
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: S n < (1 + length L)%nat
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆a┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭
CODE (`Let {A1 EA1} V1 := `App val_sub (S n) 1 in
       `App nth (``q) (``V1))
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth (S n) (a :: L)⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    mxapp* Triple_sub.
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: S n < (1 + length L)%nat
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MCell┆a┆q⟧⟭┆⟬PointsTo┆q┆⟦
$MList ┆ L⟧⟭⟭*⟭
CODE (`App nth (``q) (``n))
⟬*POST@ fun x : credits =>
        ⟬Star┆⟬Star┆⟬Pure┆x = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
        $MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp* IHL.
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: S n < (1 + length L)%nat
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ L⟧⟭┆⟬PointsTo┆p┆⟦$MCell┆a┆q⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
LibList.nth n L = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
    xchange <- MList_cons.
a: credits
L: list credits
IHL: forall (n : nat) p,
n < length L ->
SPEC (nth p n)
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ L⟧⟭*⟭
⟬*POST@fun r : credits =>
       ⟬Star┆⟬Pure┆r = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦
       $MList ┆ L⟧⟭⟭*⟭
n: nat
p: loc
H: S n < (1 + length L)%nat
q: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭*⟭==>⟬*POST@⟬Star┆⟬Star┆⟬Pure┆
LibList.nth n L = LibList.nth n L⟭┆⟬PointsTo┆p┆⟦$MList ┆ a :: L⟧⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xsimpl*.
Qed.

Lemma Triple_append_aux: forall p1 L1 p2 L2,
  L1 <> nil ->
  Triple (append_aux p1 p2)
    (p1 ~> MList L1 \* p2 ~> MList L2)
    (fun (_: unit) => p1 ~> MList (L1++L2)).
forall p1 (L1 : list credits) p2 (L2 : list credits),
L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ L1 ++ L2⟧⟭*⟭
Proof.
forall p1 (L1 : list credits) p2 (L2 : list credits),
L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ L1 ++ L2⟧⟭*⟭
  intros p1 L1; gen p1.
L1: list credits
forall p1 p2 (L2 : list credits),
L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ L1 ++ L2⟧⟭*⟭
  induction L1 as [| x L1]; [easy |].
x: credits
L1: list credits
IHL1: forall p1 p2 (L2 : list credits),
L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ L1 ++ L2⟧⟭*⟭
forall p1 p2 (L2 : list credits),
x :: L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ x :: L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ (x :: L1) ++ L2⟧⟭*⟭
  xwp.
x: credits
L1: list credits
IHL1: forall p1 p2 (L2 : list credits),
L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ L1 ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: L1 <> nil
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ x :: L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`Let {A EA} X := `App get_next p1 in
       `Let b0 := `App is_empty (``X) in
        `If_ b0 Then 
           `App set_next p1 p2
         Else
           `App append_aux (``X) p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: L1) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_get_next; intros q.
x: credits
L1: list credits
IHL1: forall p1 p2 (L2 : list credits),
L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ L1 ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: L1 <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆q⟧⟭┆⟬Star┆⟬PointsTo┆q┆⟦
$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦$MList ┆ L2⟧⟭⟭⟭*⟭
CODE (`Let b0 := `App is_empty (``q) in
       `If_ b0 Then 
          `App set_next p1 p2
        Else
          `App append_aux (``q) p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: L1) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
  mxapp Triple_is_empty.
x: credits
L1: list credits
IHL1: forall p1 p2 (L2 : list credits),
L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ L1 ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: L1 <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ L1⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭⟭*⟭
CODE (`If_ isTrue (L1 = nil) Then 
         `App set_next p1 p2
       Else
         `App append_aux (``q) p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: L1) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
  destruct L1; xif; try easy; intros _.
x: credits
IHL1: forall p1 p2 (L2 : list credits),
nil <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ nil ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: nil <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ nil⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭⟭*⟭
CODE (`App set_next p1 p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: nil) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
x, z: credits
L1: list credits
IHL1: forall p1 p2 (L2 : list credits),
z :: L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ z :: L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: z :: L1 <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ z :: L1⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭⟭*⟭
CODE (`App append_aux (``q) p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: z :: L1) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
  -
x: credits
IHL1: forall p1 p2 (L2 : list credits),
nil <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ nil ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: nil <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ nil⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭⟭*⟭
CODE (`App set_next p1 p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: nil) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange <- MList_cons.
x: credits
IHL1: forall p1 p2 (L2 : list credits),
nil <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ nil ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: nil <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ x :: nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`App set_next p1 p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: nil) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp~ Triple_set_next.
x: credits
IHL1: forall p1 p2 (L2 : list credits),
nil <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ nil ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: nil <> nil
q, x0: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆p2⟧⟭┆⟬Star┆⟬PointsTo┆x0┆⟦
$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦$MList ┆ L2⟧⟭⟭⟭*⟭==>⟬*POST@⟬Star┆⟬PointsTo┆p1┆⟦
$MList ┆ (x :: nil) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
    xchange~ MList_nil.
x: credits
IHL1: forall p1 p2 (L2 : list credits),
nil <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ nil ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: nil <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆p2⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: nil) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchanges <- MList_cons.
  -
x, z: credits
L1: list credits
IHL1: forall p1 p2 (L2 : list credits),
z :: L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ z :: L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: z :: L1 <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ z :: L1⟧⟭┆⟬Star┆⟬PointsTo┆p1┆⟦$MCell┆x┆q⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭⟭*⟭
CODE (`App append_aux (``q) p2)
⟬*POST@ fun _ : unit =>
        ⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ (x :: z :: L1) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp* IHL1.
x, z: credits
L1: list credits
IHL1: forall p1 p2 (L2 : list credits),
z :: L1 <> nil ->
SPEC (append_aux p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ z :: L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun _ : unit => ⟬PointsTo┆p1┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭*⟭
p1, p2: loc
L2: list credits
H: x :: z :: L1 <> nil
q: loc
⟬*PRE@⟬Star┆⟬PointsTo┆q┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭┆⟬PointsTo┆p1┆⟦$MCell┆x┆q⟧⟭⟭*⟭==>⟬*POST@⟬Star┆⟬PointsTo┆p1┆⟦
$MList ┆ (x :: z :: L1) ++ L2⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchanges <- MList_cons.
Qed.

Lemma Triple_append: forall p1 L1 p2 L2,
  Triple (append p1 p2)
    (p1 ~> MList L1 \* p2 ~> MList L2)
    (fun (r: loc) => r ~> MList (L1++L2) \* \[L1 <> nil -> r = p1]).
forall p1 (L1 : list credits) p2 (L2 : list credits),
SPEC (append p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun r : loc =>
       ⟬Star┆⟬PointsTo┆r┆⟦$MList ┆ L1 ++ L2⟧⟭┆⟬Pure┆
       L1 <> nil -> r = p1⟭⟭*⟭
Proof.
forall p1 (L1 : list credits) p2 (L2 : list credits),
SPEC (append p1 p2)
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
⟬*POST@fun r : loc =>
       ⟬Star┆⟬PointsTo┆r┆⟦$MList ┆ L1 ++ L2⟧⟭┆⟬Pure┆
       L1 <> nil -> r = p1⟭⟭*⟭
  xwp.
p1: loc
L1: list credits
p2: loc
L2: list credits
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`Let b0 := `App is_empty p1 in
       `If_ b0 Then 
          `$p2
        Else
          `(`App append_aux p1 p2) ;
           `$p1)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ L1 ++ L2⟧⟭┆⟬Pure┆
        L1 <> nil -> x = p1⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  mxapp Triple_is_empty.
p1: loc
L1: list credits
p2: loc
L2: list credits
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`If_ isTrue (L1 = nil) Then 
         `$p2
       Else
         `(`App append_aux p1 p2) ;
          `$p1)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ L1 ++ L2⟧⟭┆⟬Pure┆
        L1 <> nil -> x = p1⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  destruct L1; xif; intros; try easy.
p1, p2: loc
L2: list credits
H: nil = nil
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`$p2)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ nil ++ L2⟧⟭┆⟬Pure┆
        nil <> nil -> x = p1⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
p1: loc
z: credits
L1: list credits
p2: loc
L2: list credits
H: z :: L1 <> nil
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ z :: L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`(`App append_aux p1 p2) ;
       `$p1)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭┆⟬Pure┆
        z :: L1 <> nil -> x = p1⟭⟭┆⟬Opaque┆GC⟭⟭*⟭
  -
p1, p2: loc
L2: list credits
H: nil = nil
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ nil⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`$p2)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ nil ++ L2⟧⟭┆⟬Pure┆
        nil <> nil -> x = p1⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange~ MList_nil.
p2: loc
L2: list credits
H: nil = nil
⟬*PRE@⟬PointsTo┆p2┆⟦$MList ┆ L2⟧⟭*⟭
CODE (`$p2)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ L2⟧⟭┆⟬Pure┆
        nil <> nil -> x = null⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxvals*.
  -
p1: loc
z: credits
L1: list credits
p2: loc
L2: list credits
H: z :: L1 <> nil
⟬*PRE@⟬Star┆⟬PointsTo┆p1┆⟦$MList ┆ z :: L1⟧⟭┆⟬PointsTo┆p2┆⟦
$MList ┆ L2⟧⟭⟭*⟭
CODE (`(`App append_aux p1 p2) ;
       `$p1)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭┆⟬Pure┆
        z :: L1 <> nil -> x = p1⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp* Triple_append_aux.
p1: loc
z: credits
L1: list credits
p2: loc
L2: list credits
H: z :: L1 <> nil
⟬*PRE@⟬PointsTo┆p1┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭*⟭
CODE (`$p1)
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬Star┆⟬PointsTo┆x┆⟦$MList ┆ (z :: L1) ++ L2⟧⟭┆⟬Pure┆
        z :: L1 <> nil -> x = p1⟭⟭┆⟬Opaque┆GC⟭⟭*⟭ mxvals*.
Qed.