NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library frag_list_entail

Require Import Bool Omega List EqNat.
Require Import ssreflect ssrbool.
Require Import Arith_ext ZArith_ext.
Require Import integral_type seplog.
Require Import expr_b_dp.
Import seplog_Z_m.assert_m.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.

Local Close Scope Z_scope.
Local Close Scope positive_scope.
Local Open Scope heap_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_assert_scope.

Definition and properties of lists

Inductive Lst : expr -> expr -> assert :=
| Lst_end: forall e1 e2 s h,
  [ e1 ]e_s = [ e2 ]e_s ->
  assert_m.emp s h ->
  Lst e1 e2 s h
| Lst_next: forall e1 e2 e3 e4 s h h1 h2,
  h1 # h2 -> h = h1 +++ h2 ->
  [ e1 ]e_s <> [ e3 ]e_s ->
  [ e1 ]e_s <> 0%Z ->
  [ e1 +e nat_e 1 ]e_s <> 0%Z ->
  (e1 |~> e2 ** (e1 +e nat_e 1 |~> e4)) s h1 ->
  Lst e2 e3 s h2 ->
  Lst e1 e3 s h.

Lemma Lst_equiv' : forall s h e1 e2, Lst e1 e2 s h ->
  forall e1' e2' s', [ e1 ]e_s = [ e1' ]e_s' -> [ e2 ]e_s = [ e2' ]e_s' ->
    Lst e1' e2' s' h.

Lemma Lst_equiv : forall s h e1 e2, Lst e1 e2 s h ->
  forall e1' e2', eval e1 s = eval e1' s -> eval e2 s = eval e2' s ->
    Lst e1' e2' s h.

Lemma Lst_app : forall e1 e2 s h1, Lst e1 e2 s h1 ->
  forall e3 h2 h3 h, Lst e2 e3 s h2 ->
    (exists v, (e3 |~> cst_e v) s h3) ->
    h1 # h2 -> h1 # h3 -> h = h1 +++ h2 ->
    Lst e1 e3 s h.

Lemma Lst_app' : forall e1 e2 s h1, Lst e1 e2 s h1 ->
  forall e3 h2 h, Lst e2 e3 s h2 ->
    h1 # h2 ->
    h = h1 +++ h2 ->
    eval e3 s = 0%Z ->
    Lst e1 e3 s h.

a Sigma formula is a spatial formula composed of the following connectives
Inductive Sigma : Type :=
| singl : expr -> expr -> Sigma
| cell : expr -> Sigma
| emp : Sigma
| star : Sigma -> Sigma -> Sigma
| lst : expr -> expr -> Sigma.

Fixpoint Sigma_interp (a : Sigma) : assert :=
  match a with
    | singl e1 e2 => fun s h => (e1 |~> e2) s h /\ eval e1 s <> 0%Z
    | emp => assert_m.emp
    | star s1 s2 => Sigma_interp s1 ** Sigma_interp s2
    | cell e => fun s h => (exists v, (e |~> cst_e v) s h) /\ eval e s <> 0%Z
    | lst e1 e2 => Lst e1 e2
  end.

an assrt is a pair of an expr_b and a Sigma formula
Definition assrt := (expr_b * Sigma)%type.

Definition assrt_interp (a : assrt) : assert :=
  match a with
    | (pi, sigm) => fun s h => eval_b pi s /\ Sigma_interp sigm s h
  end.

an Assrt is a disjunction of assrts
Definition Assrt := list assrt.

Fixpoint Assrt_interp (l : Assrt) : assert :=
  match l with
    | nil => fun s h => False
    | hd :: tl => fun s h => assrt_interp hd s h \/ Assrt_interp tl s h
  end.

Notation "{{{ P }}} c {{{ Q }}}" := (while.hoare store.t heap.t cmd0 expr_b
(fun eb s => eval_b eb (fst s)) hoare0 (assrt_interp P) c (Assrt_interp (Q :: nil))) (at level 80) : frag_list_scope.
Local Open Scope frag_list_scope.

A proof system for assrt entailment

Notation "s ** t" := (star s t) (at level 80) : entail_scope.
Local Open Scope entail_scope.

Inductive entail : assrt -> assrt -> Prop :=
final rules
| entail_incons : forall pi1 pi2 sig1 sig2,
  (forall s, [ pi1 ]b_s -> False) ->
  entail (pi1, sig1) (pi2, sig2)

| entail_tauto : forall pi1 pi2,
  (forall s, [ pi1 ]b_s -> [ pi2 ]b_s) ->
  entail (pi1, emp) (pi2, emp)
structural rules
| entail_coml : forall pi1 sig1 sig2 L,
  entail (pi1, sig2 ** sig1) L -> entail (pi1, sig1 ** sig2) L

| entail_comr : forall pi1 sig1 sig2 L,
  entail L (pi1, sig2 ** sig1) -> entail L (pi1, sig1 ** sig2)

| entail_assocl : forall pi1 sig1 sig2 sig3 L,
  entail (pi1, (sig1 ** sig2) ** sig3) L ->
  entail (pi1, sig1 ** (sig2 ** sig3)) L

| entail_assocr : forall pi1 sig1 sig2 sig3 L,
  entail L (pi1, (sig1 ** sig2) ** sig3) ->
  entail L (pi1, sig1 ** (sig2 ** sig3))

| entail_empeliml : forall pi1 sig1 L,
  entail (pi1, sig1) L -> entail (pi1, sig1 ** emp) L

| entail_empelimr : forall pi1 sig1 L,
  entail L (pi1, sig1) -> entail L (pi1, sig1 ** emp)

| entail_empintrol : forall pi1 sig1 L,
  entail (pi1, sig1 ** emp) L -> entail (pi1, sig1) L

| entail_empintror : forall pi1 sig1 L,
  entail L (pi1, sig1 ** emp) -> entail L (pi1, sig1)
elimination rules for list
| entail_lstnilelimr : forall pi1 sig1 pi2 sig2 e1 e2,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e2) s) ->
  entail (pi1, sig1) (pi2, sig2) ->
  entail (pi1, sig1) (pi2, sig2 ** (lst e1 e2))

| entail_lstnileliml : forall pi1 sig1 pi2 sig2 e1 e2,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e2) s) ->
  entail (pi1, sig1) (pi2, sig2) ->
  entail (pi1, sig1 ** (lst e1 e2)) (pi2, sig2)

| entail_lstsamelst : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s) ->
  (forall s, eval_b pi1 s -> eval_b (e2 =e e4) s) ->
  entail (pi1, sig1) (pi2, sig2) ->
  entail (pi1, sig1 ** (lst e1 e2)) (pi2, sig2 ** (lst e3 e4))

| entail_lstelim : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s) ->
  entail (pi1, sig1 ** (cell e4)) (pi2, sig2 ** (lst e2 e4)) ->
  entail (pi1, (sig1 ** (cell e4)) ** (lst e1 e2)) (pi2, sig2 ** (lst e3 e4))

| entail_lstelim_v2 : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4 sig1',
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s = true) ->
  entail (pi1, sig1) (pi1, (sig1' ** (cell e4))) ->
  entail (pi1, sig1' ** (cell e4)) (pi2, sig2 ** (lst e2 e4)) ->
  entail (pi1, sig1 ** (lst e1 e2)) (pi2, sig2 ** (lst e3 e4))

| entail_lstelim' : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4 e5,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  (forall s, eval_b pi1 s -> eval_b (e4 <>e e5) s ) ->
  entail (pi1, sig1 ** (lst e4 e5)) (pi2, sig2 ** (lst e2 e4)) ->
  entail (pi1, (sig1 ** (lst e4 e5)) ** (lst e1 e2)) (pi2, sig2 ** (lst e3 e4))

| entail_lstelim'_v2 : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4 e5 sig1',
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  entail (pi1, sig1) (pi1, sig1' ** (lst e4 e5)) ->
  (forall s, eval_b pi1 s -> eval_b (e4 <>e e5) s ) ->
  entail (pi1, sig1' ** (lst e4 e5)) (pi2, sig2 ** (lst e2 e4)) ->
  entail (pi1, sig1 ** (lst e1 e2)) (pi2, sig2 ** (lst e3 e4))

| entail_lstelim'' : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  (forall s, eval_b pi1 s -> eval_b (e4 =e cst_e 0%Z) s ) ->
  entail (pi1, sig1) (pi2, sig2 ** (lst e2 e4)) ->
  entail (pi1, sig1 ** (lst e1 e2)) (pi2, sig2 ** (lst e3 e4))

| entail_lstelim''' : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  (forall s, eval_b pi1 s -> eval_b (e1 <>e e4) s ) ->
  (forall s, eval_b pi1 s -> eval_b (e1 <>e cst_e 0%Z) s ) ->
  entail (pi1, sig1) (pi2, sig2 ** ((cell (e1 +e nat_e 1)) ** (lst e2 e4))) ->
  entail (pi1, sig1 ** (singl e1 e2)) (pi2, sig2 ** (lst e3 e4))
rule to eliminate mapstos
| entail_star_elim : forall pi1 pi2 sig1 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  (forall s, eval_b pi1 s -> eval_b (e2 =e e4) s ) ->
  entail (pi1, sig1) (pi2, sig2) ->
  entail (pi1, sig1 ** (singl e1 e2)) (pi2, sig2 ** (singl e3 e4))

| entail_star_elim': forall pi1 pi2 sig1 sig2 e1 e2 e3,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  entail (pi1, sig1) (pi2, sig2) ->
  entail (pi1, sig1 ** (singl e1 e2)) (pi2, sig2 ** (cell e3))

| entail_star_elim'': forall pi1 pi2 sig1 sig2 e1 e3,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  entail (pi1, sig1) (pi2, sig2) ->
  entail (pi1, sig1 ** (cell e1)) (pi2, sig2 ** (cell e3))
rule to generate constraints
| entail_star_neq : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4,
  entail (pi1 &e (e1 <>e e3), sig1 ** ((singl e1 e2) ** (singl e3 e4))) (pi2, sig2) ->
  entail (pi1, sig1 ** ((singl e1 e2) ** (singl e3 e4))) (pi2, sig2)

| entail_star_neq' : forall pi1 sig1 pi2 sig2 e1 e2 e3,
  entail (pi1 &e (e1 <>e e3), sig1 ** ((singl e1 e2) ** (cell e3))) (pi2, sig2) ->
  entail (pi1, sig1 ** ((singl e1 e2) ** (cell e3))) (pi2, sig2)

| entail_star_neq'' : forall pi1 sig1 pi2 sig2 e1 e3,
  entail (pi1 &e (e1 <>e e3), sig1 ** ((cell e1) ** (cell e3))) (pi2, sig2) ->
  entail (pi1, sig1 ** ((cell e1) ** (cell e3))) (pi2, sig2)

| entail_star_neq''' : forall pi1 sig1 pi2 sig2 e1 e2 e3,
  (forall s, eval_b pi1 s -> eval_b (e1 <>e e2) s ) ->
  entail (pi1 &e (e1 <>e e3), sig1 ** ((lst e1 e2) ** (cell e3))) (pi2, sig2) ->
  entail (pi1, sig1 ** ((lst e1 e2) ** (cell e3))) (pi2, sig2)

| entail_star_neq'''' : forall pi1 sig1 pi2 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 <>e e2) s ) ->
  entail (pi1 &e (e1 <>e e3), sig1 ** ((lst e1 e2) ** (singl e3 e4))) (pi2, sig2) ->
  entail (pi1, sig1 ** ((lst e1 e2) ** (singl e3 e4))) (pi2, sig2)

| entail_star_neq''''': forall pi1 sig1 pi2 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 <>e e2) s ) ->
  (forall s, eval_b pi1 s -> eval_b (e3 <>e e4) s ) ->
  entail (pi1 &e (e1 <>e e3), sig1 ** ((lst e1 e2) ** (lst e3 e4))) (pi2, sig2) ->
  entail (pi1, sig1 ** ((lst e1 e2) ** (lst e3 e4))) (pi2, sig2)

| entail_singl_not_null : forall pi1 sig1 pi2 sig2 e1 e2,
  entail (pi1 &e (e1 <>e (nat_e 0)), sig1 ** (singl e1 e2)) (pi2, sig2) ->
  entail (pi1, sig1 ** (singl e1 e2)) (pi2, sig2)

| entail_cell_not_null : forall pi1 sig1 pi2 sig2 e1,
  entail (pi1 &e (e1 <>e (nat_e 0)), sig1 ** (cell e1)) (pi2, sig2) ->
  entail (pi1, sig1 ** (cell e1)) (pi2, sig2)

| entail_lst_not_null : forall pi1 sig1 pi2 sig2 e1 e2,
  (forall s, eval_b pi1 s -> eval_b (e2 <>e (nat_e 0)) s ) ->
  entail (pi1 &e (e1 <>e (nat_e 0)), sig1 ** (lst e1 e2)) (pi2, sig2) ->
  entail (pi1, sig1 ** (lst e1 e2)) (pi2, sig2)

| entail_monotony : forall pi1 pi2 sig11 sig12 sig21 sig22,
  entail (pi1,sig11) (pi2, sig21) ->
  entail (pi1,sig12) (pi2, sig22) ->
  entail (pi1, sig11 ** sig12) (pi2, sig21 ** sig22)
  
| entail_destructlist: forall pi1 pi2 sig1 sig2 e1 e2,
  (entail (pi1 &e (e1 =e e2), sig1 ** (lst e1 e2)) (pi2, sig2)) ->
  (entail (pi1 &e (e1 <>e e2), sig1 ** (lst e1 e2)) (pi2, sig2)) ->
  entail (pi1, star sig1 (lst e1 e2)) (pi2, sig2).

Notation "s '|--' t" := (entail s t) (at level 80) : entail_scope.

derived rules

Lemma entail_id : forall sig pi, (pi, sig) |-- (pi, sig).

Lemma entail_star_elim_lst : forall pi1 sig1 pi2 sig2 e1 e2,
  (pi1, sig1) |-- (pi2, sig2) ->
  (pi1, sig1 ** (lst e1 e2)) |-- (pi2, sig2 ** (lst e1 e2)).

Lemma entail_star_elim_star : forall s pi1 sig1 pi2 sig2,
  (pi1, sig1) |-- (pi2, sig2) -> (pi1, sig1 ** s) |-- (pi2, sig2 ** s).

Soundness of the proof system

Lemma entail_soundness : forall P Q, P |-- Q -> assrt_interp P ===> assrt_interp Q.

Lemma entail_to_Sigma_impl : forall sig1 sig2,
  (true_b, sig1) |-- (true_b, sig2) -> Sigma_interp sig1 ===> Sigma_interp sig2.

Local Close Scope entail_scope.

tactics to prove a entail goal

Tactic that turn the left/right hand side of entailment and that add an empty is there is only one subheap
Ltac Entail_turnl :=
  match goal with
    | |- entail (?Pi, cell ?e) ?L => eapply entail_empintrol; eapply entail_coml; repeat eapply entail_assocl
    | |- entail (?Pi, singl ?e1 ?e2) ?L => eapply entail_empintrol; eapply entail_coml; repeat eapply entail_assocl
    | |- entail (?Pi, lst ?e1 ?e2) ?L => eapply entail_empintrol; eapply entail_coml; repeat eapply entail_assocl
    | |- entail (?Pi, star ?e1 ?e2) ?L => eapply entail_coml; repeat eapply entail_assocl
    | _ => eapply entail_empintrol; eapply entail_coml; repeat eapply entail_assocl
  end.

Ltac Entail_turnr :=
  match goal with
    | |- entail ?L (?Pi, cell ?e) => eapply entail_empintror; eapply entail_comr; repeat eapply entail_assocr
    | |- entail ?L (?Pi, singl ?e1 ?e2) => eapply entail_empintror; eapply entail_comr; repeat eapply entail_assocr
    | |- entail ?L (?Pi, lst ?e1 ?e2) => eapply entail_empintror; eapply entail_comr; repeat eapply entail_assocr
    | |- entail ?L (?Pi, star ?e1 ?e2) => eapply entail_comr; repeat eapply entail_assocr
    | _ => eapply entail_empintror; eapply entail_comr; repeat eapply entail_assocr
  end.

Eliminate left most subheap from lhs and rhs

Ltac Elim_subheap := repeat eapply entail_assocl; repeat eapply entail_assocr;
  match goal with
    | |- entail (?pi1, star ?sig1 (singl ?e1 ?e2)) (?pi2, star ?sig2 (singl ?e3 ?e4)) =>
      apply entail_star_elim;
        [ (do 2 intro; omegab) | (do 2 intro; omegab) | idtac]
      
    | |- entail (?pi1, star ?sig1 (singl ?e1 ?e2)) (?pi2, star ?sig2 (cell ?e3)) =>
      apply entail_star_elim'; [ (do 2 intro; omegab) | idtac]
      
    | |- entail (?pi1, star ?sig1 (cell ?e1)) (?pi2, star ?sig2 (cell ?e3)) =>
      apply entail_star_elim'' ; [ (do 2 intro; omegab) | idtac]

    | |- entail (?pi1, star ?sig1 (lst ?e1 ?e2)) (?pi2, star ?sig2 (lst ?e3 ?e4)) =>
      (apply entail_lstsamelst; [ (do 2 intro; omegab) | (do 2 intro; omegab) | idtac]) ||
      (apply entail_lstelim''; [ (do 2 intro; omegab) | (do 2 intro; omegab) | idtac])

    | |- entail (?pi1, star ?sig1 (singl ?e1 ?e2)) (?pi2, star ?sig2 (lst ?e3 ?e4)) =>
      apply entail_lstelim''';
        [ (do 2 intro; omegab) | (do 2 intro; omegab) | (do 2 intro; omegab) | idtac]

    | |- entail (?pi1, star ?sig1 ?s) (?pi2, star ?sig2 ?s) =>
      eapply entail_star_elim_star

  end.

Prove simpl goal (= that does not need subheap elimination)

Ltac Entail_arith_impl :=
  match goal with
    | |- entail (?pi, ?sig) (?pi, ?sig) =>
      eapply entail_id
    | |- entail (?pi1, emp) (?pi2, emp) => eapply entail_tauto; [(do 2 intro; omegab)]
    | |- entail (?pi1, emp) (?pi2, emp) => eapply entail_incons; [(do 2 intro; omegab)]
  end.

eliminate every empty subheap

Ltac Entail_elim_emp :=
  match goal with
    | |- entail (?pi1, star ?sig1 emp) (?pi2, ?sig2) => eapply entail_empeliml; Entail_elim_emp
    | |- entail (?pi1, ?sig1) (?pi2, star ?sig2 emp) => eapply entail_empelimr; Entail_elim_emp
    | |- _ => idtac
  end.

add location not null constraints

Ltac Entail_not_nul_constraint :=
  match goal with
    | |- entail (?pi1, star ?sig1 (cell ?e)) (?pi2, ?sig2) =>
      eapply entail_cell_not_null; idtac
    | |- entail (?pi1, star ?sig1 (singl ?e1 ?e2)) (?pi2, ?sig2) =>
      eapply entail_singl_not_null; idtac
    | |- entail (?pi1, star ?sig1 (lst ?e1 ?e2)) (?pi2, ?sig2) =>
      apply entail_lst_not_null; [ (do 2 intro; omegab) | idtac ]
    | |- _ => idtac
  end.

compute the number of subheaps

Ltac Entail_count_subheap sig :=
  match sig with
    | star ?sig1 ?sig2 =>
      let x := Entail_count_subheap sig1 in
        let y := Entail_count_subheap sig2 in
          constr:(x + y)
    | _ =>
      constr:(1)
  end.


Turn the rhs at most m time until an elimination could be performed

Ltac Entail_elim_right n m :=
  let y := (constr:(nat_gt n m)) in
    match (eval compute in y) with
      | true => idtac
      | false =>
        Entail_turnr; (Elim_subheap || (
        let x := (constr:(S n)) in Entail_elim_right x m))
    end.

try to solve the goal or try to eliminate the left most subheap of lhs

Ltac Entail_elim_left := Entail_not_nul_constraint;
  match goal with
    | |- entail (?pi1, ?sig1) (?pi2, ?sig2) =>
      Entail_elim_emp; Entail_arith_impl
    | |- entail (?pi1, ?sig1) (?pi2, ?sig2) =>
      let x := Entail_count_subheap sig2 in (
        let vx := eval compute in x in
          Entail_elim_right 0 vx
      ); Entail_turnl
  end.

Ltac Entail := repeat Entail_elim_left.

Example in the PPL 2007 draft

Module examples.

Definition nil : expr := nat_e 0.
Definition e : expr := var_e 0.
Definition e' : expr := var_e 1.
Definition e'' : expr := var_e 2.

Goal
entail
(true_b,
star (lst e e') (
star (singl e' e'') (
star (cell (e' +e (nat_e 1))) (
lst e'' (nat_e 0)
))))
(true_b, lst e (nat_e 0)).

Definition null : expr := nat_e 0.
Definition v1 : expr := var_e 4.
Definition v2 : expr := var_e 5.
Definition x1 : expr := var_e 0.
Definition x2 : expr := var_e 1.
Definition x3 : expr := var_e 2.
Definition x4 : expr := var_e 3.
Definition x5 : expr := var_e 4.
Definition x6 : expr := var_e 5.

Definition P := ((x3 <>e null) &e (x5 <>e null) &e (x6 =e null) &e (x3 <>e x5),
  (star (lst x1 x3)
    (star (singl x3 x5)
      (star (cell (x3 +e (nat_e 1)))
        (lst x5 x6))))).

Definition Q' := ( true_b, star (lst x1 x5) (lst x5 x6) ).

Definition Q := ( true_b, (lst x1 x6) ).

Ltac Print h :=
  let y := (eval compute in h) in assert (y = y); auto.

Ltac Nb_sig_elt sig :=
  match sig with
    | singl ?e1 ?e2 =>
      constr:1
    | cell ?e1 =>
      constr:1
    | emp =>
      constr:1
    | star ?sig1 ?sig2 =>
      let x := (Nb_sig_elt sig1) in
        let y := (Nb_sig_elt sig2) in
          constr:(x + y)
    | lst ?e1 ?e2 =>
      constr:1
  end.

Ltac Nb_sig_elt_entail_right :=
  match goal with
    | |- entail (?pi1,?sig1) (?pi2,?sig2) =>
      Nb_sig_elt sig2
  end.

Ltac Nb_sig_elt_entail_left :=
  match goal with
    | |- entail (?pi1,?sig1) (?pi2,?sig2) =>
      Nb_sig_elt sig1
  end.

Goal (assrt_interp P) ===> (assrt_interp Q).

Goal (assrt_interp P) ===> (assrt_interp Q').

End examples.

load the decision procedure for expr_b

Fixpoint remove_empty_heap (pi : expr_b) (sig : Sigma) {struct sig} : Sigma :=
  match sig with
    | star sig1 sig2 =>
      match remove_empty_heap pi sig1 with
        | emp => remove_empty_heap pi sig2
        | sig1' => match remove_empty_heap pi sig2 with
                   | emp => sig1'
                   | sig2' => star sig1' sig2'
                 end
      end
    | lst e1 e2 => if expr_b_dp (pi =b> (e1 =e e2)) then emp else sig
    | _ => sig
  end.

Lemma remove_empty_heap_correct : forall sig pi s, [ pi ]b_s ->
  forall h, Sigma_interp (remove_empty_heap pi sig) s h -> Sigma_interp sig s h.

Lemma remove_empty_heap_correct' : forall sig pi s, [ pi ]b_s ->
  forall h, Sigma_interp sig s h -> Sigma_interp (remove_empty_heap pi sig) s h.

returns true if <env,sig> contains (cell e), (singl e _), or (lst e _) <>e emp
Fixpoint cell_in_sigma (pi : expr_b) (sig : Sigma) (e : expr) {struct sig} : bool :=
  match sig with
    | singl e1 e2 => expr_b_dp (pi =b> (e1 =e e))
    | cell e1 => expr_b_dp (pi =b> (e1 =e e))
    | lst e1 e2 => andb
      (expr_b_dp (pi =b> (e1 =e e)))
      (expr_b_dp (pi =b> (e1 <>e e2)))
    | star s1 s2 => orb (cell_in_sigma pi s1 e ) (cell_in_sigma pi s2 e)
    | _ => false
  end.

Lemma cell_in_sigma_correct: forall sig e pi, cell_in_sigma pi sig e ->
  forall s h, [ pi ]b_s ->
    Sigma_interp sig s h -> ((Sigma_interp (cell e)) ** TT) s h.

Opaque remove_empty_heap.

returns true if two sigmas are the two same singl, cell ou lst
Definition sigma_eq (pi : expr_b) (sig1 sig2 : Sigma) : bool :=
  match (sig1, sig2) with
    | (emp, emp) => true
    | (singl e1 e2, singl e3 e4) => andb (expr_b_dp (pi =b> (e1 =e e3))) (expr_b_dp (pi =b> (e2 =e e4)))
    | (singl e1 e2, cell e3) => expr_b_dp (pi =b> (e1 =e e3))
    | (cell e1, cell e3) => expr_b_dp (pi =b> (e1 =e e3))
    | (lst e1 e2, lst e3 e4) => andb (expr_b_dp (pi =b> (e1 =e e3))) (expr_b_dp (pi =b> (e2 =e e4)))
    | (_, _) => false
  end.

Lemma sigma_eq_correct: forall sig1 sig2 pi, sigma_eq pi sig1 sig2 ->
  forall s h,
    [ pi ]b_s ->
    (Sigma_interp sig1 s h -> Sigma_interp sig2 s h).

remove the cell sig of the heap (sig ** sig1) from the heap sig2
Fixpoint elim_common_cell (pi : expr_b) (sig1 remainder sig2 : Sigma) {struct sig2} : option (Sigma * Sigma) :=
  match sig2 with
    | star sig21 sig22 =>
      match elim_common_cell pi sig1 remainder sig21 with
        | None =>
          match elim_common_cell pi sig1 remainder sig22 with
            | None => None
            | Some (sig1', sig2') => Some (sig1', remove_empty_heap pi (star sig21 sig2'))
          end
        | Some (sig1', sig2') => Some (sig1', remove_empty_heap pi (star sig2' sig22))
      end
    | _ =>
      if sigma_eq pi sig1 sig2 then Some (emp, emp) else
        match (sig1, sig2) with
          | (lst e11 e12, lst e21 e22) =>
            if andb
              (expr_b_dp (pi =b> (e11 =e e21)))
              (orb
                (expr_b_dp (pi =b> (e22 =e nat_e 0)))
                (cell_in_sigma pi remainder e22) )
              then Some (emp, lst e12 e22)
              else None
          | (singl e1 e2, lst e3 e4) =>
            if andb (expr_b_dp (pi =b> (e1 =e e3)))
              (andb (expr_b_dp (pi =b> (e1 <>e e4)))
                (expr_b_dp (pi =b> (e1 <>e nat_e 0))))
              then Some (emp, (star (cell (e1 +e nat_e 1)) (lst e2 e4)))
                
              else None
          | (emp, lst e3 e4) =>
            if expr_b_dp (pi =b> (e3 =e e4))
              then Some (emp, emp)
              else Some (emp, sig2)
          | (emp, _) => Some (emp, sig2)
          | _ => None
        end
  end.

Lemma elim_common_cell_mp : forall sig2 sig1 remainder pi sig1' sig2',
  elim_common_cell pi sig1 remainder sig2 = Some (sig1', sig2') ->
  (Sigma_interp sig1 ===> (Sigma_interp sig1' -* Sigma_interp sig1) ** Sigma_interp sig1').

Lemma elim_common_cell_correct : forall sig2 sig1 remainder pi sig1' sig2',
  elim_common_cell pi sig1 remainder sig2 = Some (sig1', sig2') ->
  forall s, [ pi ]b_s ->
    forall h1 h2 h3 h,
      Sigma_interp sig2' s h1 ->
      (Sigma_interp sig1' -* Sigma_interp sig1) s h2 ->
      Sigma_interp remainder s h3 ->
      h = h1 +++ h2 ->
      h1 # h2 ->
      h2 # h3 ->
      Sigma_interp sig2 s h.

try to match sig1 with sig2, remainder is that part of sig1 that is left aside
Fixpoint elim_common_subheap (pi : expr_b) (sig1 sig2 remainder : Sigma) {struct sig1} : option (Sigma * Sigma) :=
  match sig1 with
    | star sig11 sig12 =>
      match elim_common_subheap pi sig11 sig2 (star sig12 remainder) with
        | None => None
        | Some (sig11', sig12') => Some (remove_empty_heap pi (star sig11' sig12), sig12')
      end
    | _ => elim_common_cell pi sig1 remainder sig2
  end.

Lemma elim_common_subheap_correct: forall sig1 sig2 remainder pi sig1' sig2',
  elim_common_subheap pi sig1 sig2 remainder = Some (sig1', sig2') ->
  forall s, [ pi ]b_s ->
    (forall h, Sigma_interp (star remainder sig1') s h -> Sigma_interp sig2' s h) ->
    (forall h, Sigma_interp (star sig1 remainder) s h -> Sigma_interp sig2 s h).

Fixpoint star_assoc_left (sig1 sig2 : Sigma) {struct sig1} : Sigma :=
  match sig1 with
    | star sig11 sig12 => star_assoc_left sig12 (star sig2 sig11)
    | _ => match sig2 with
             | emp => sig1
             | _ => star sig2 sig1
           end
  end.

Lemma star_assoc_left_correct: forall sig1 sig2,
  Sigma_interp (star_assoc_left sig1 sig2) ===> Sigma_interp (star sig1 sig2).

Lemma star_assoc_left_correct' : forall sig1 sig2,
  Sigma_interp (star sig1 sig2) ===> Sigma_interp (star_assoc_left sig1 sig2).

Definition star_com (sig : Sigma) : Sigma :=
  match sig with
    | star sig1 sig2 => star sig2 sig1
    | _ => sig
  end.

Lemma star_com_correct : forall sig,
  Sigma_interp (star_com sig) ===> Sigma_interp sig.

Lemma star_com_correct' : forall sig,
  Sigma_interp sig ===> Sigma_interp (star_com sig).

Definition rearrange_elim_common_subheap (pi : expr_b) (sig1 sig2 : Sigma) : Sigma * Sigma :=
  match elim_common_subheap pi sig1 sig2 emp with
    | None => (remove_empty_heap pi (star_com (star_assoc_left sig1 emp)), sig2)
    | Some s => s
  end.

Lemma rearrange_elim_common_subheap_correct : forall sig1 sig2 pi sig1' sig2',
  rearrange_elim_common_subheap pi sig1 sig2 = (sig1', sig2') ->
  forall s, [ pi ]b_s ->
    (forall h, Sigma_interp sig1' s h -> Sigma_interp sig2' s h) ->
    forall h, Sigma_interp sig1 s h -> Sigma_interp sig2 s h.

Fixpoint elim_common_subheap_iterate (pi : expr_b) (sig1 sig2 : Sigma) (step : nat) {struct step} : Sigma * Sigma :=
  match step with
    | 0 => (sig1, sig2)
    | S n =>
      match rearrange_elim_common_subheap pi sig1 sig2 with
        | (sig1', sig2') => elim_common_subheap_iterate pi sig1' sig2' n
      end
  end.

Lemma elim_common_subheap_iterate_correct: forall n sig1 sig2 pi sig1' sig2',
  elim_common_subheap_iterate pi sig1 sig2 n = (sig1',sig2') ->
  forall s,[ pi ]b_s ->
    (forall h, Sigma_interp sig1' s h -> Sigma_interp sig2' s h) ->
    forall h, Sigma_interp sig1 s h -> Sigma_interp sig2 s h.

Transparent remove_empty_heap.

Fixpoint sigma_size (sig : Sigma) : nat :=
  match sig with
    | singl e1 e2 => 1
    | cell e1 => 1
    | lst e1 e2 => 3
    | star s1 s2 => sigma_size s1 + sigma_size s2
    | emp => 1
  end.

Inductive resul (A : Type) : Type :=
  | Good : resul A
  | Error : A -> resul A.

Implicit Arguments Good [A].
Implicit Arguments Error [A].

Definition sigma_impl (pi : expr_b) (sig1 sig2 : Sigma) : resul (Sigma * Sigma) :=
  match elim_common_subheap_iterate pi sig1 sig2 ((sigma_size sig1 + sigma_size sig2) * 2) with
    | (emp, emp) => Good
    | e => Error e
  end.

Lemma sigma_impl_correct: forall sig1 sig2 pi, sigma_impl pi sig1 sig2 = Good ->
  forall s, [ pi ]b_s ->
    forall h, Sigma_interp sig1 s h -> Sigma_interp sig2 s h.

Definition frag_entail_fun (a1 a2 : assrt) : resul (assrt * assrt) :=
  let (pi1, sig1) := a1 in
    let (pi2, sig2) := a2 in
      if expr_b_dp (~e pi1) then
        
        Good
        else
          match sigma_impl pi1 sig1 sig2 with
            | Good => if expr_b_dp (pi1 =b> pi2) then
              Good
              else
                Error ((pi1, emp), (pi2, emp))
            | Error (s1, s2) => Error ((pi1, s1), (pi2, s2))
          end.

Lemma frag_entail_fun_correct: forall a1 a2,
  frag_entail_fun a1 a2 = Good -> assrt_interp a1 ===> assrt_interp a2.


Definition compute_constraint_cell (pi : expr_b) (sig1 sig2 : Sigma) : expr_b :=
  match (sig1,sig2) with
    | (singl e1 e2, singl e3 e4) =>
      if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
        pi &e (e1 <>e e3)
    | (singl e1 e2, cell e3) =>
      if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
        pi &e (e1 <>e e3)
    | (cell e1, singl e3 e4) =>
      if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
        pi &e (e1 <>e e3)
    | (cell e1, cell e3) =>
      if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
        pi &e (e1 <>e e3)
    | (singl e1 e2, lst e3 e4) =>
      if expr_b_dp (pi =b> (e3 <>e e4)) then
        if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
          pi &e (e1 <>e e3)
        else pi
    | (lst e1 e2, singl e3 e4) =>
      if expr_b_dp (pi =b> (e1 <>e e2)) then
        if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
          pi &e (e1 <>e e3)
        else pi
    | (cell e1, lst e3 e4) =>
      if expr_b_dp (pi =b> (e3 <>e e4)) then
        if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
          pi &e (e1 <>e e3)
        else pi
    | (lst e1 e2, cell e3) =>
      if expr_b_dp (pi =b> (e1 <>e e2)) then
        if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
          pi &e (e1 <>e e3)
        else pi
    | (lst e1 e2, lst e3 e4) =>
      if expr_b_dp (pi =b> (e1 <>e e2)) && expr_b_dp (pi =b> (e3 <>e e4)) then
        if expr_b_dp (pi =b> (e1 <>e e3)) then pi else
          pi &e (e1 <>e e3)
        else pi
    | (_, _) => pi
  end.

Lemma compute_constraint_cell_correct : forall sig1 sig2 pi,
  assrt_interp (pi, star sig1 sig2) ===> assrt_interp (compute_constraint_cell pi sig1 sig2, star sig1 sig2).

Fixpoint compute_constraint_cell_sigma (pi: expr_b) (sig1 sig2:Sigma) {struct sig2} : expr_b :=
  match sig2 with
    | star sig21 sig22 => compute_constraint_cell_sigma (compute_constraint_cell_sigma pi sig1 sig21) sig1 sig22
    | _ => compute_constraint_cell pi sig1 sig2
  end.

Lemma compute_constraint_cell_sigma_correct : forall sig2 sig1 pi,
  assrt_interp (pi, star sig1 sig2) ===> assrt_interp (compute_constraint_cell_sigma pi sig1 sig2, star sig1 sig2).

Fixpoint compute_constraints' (pi : expr_b) (sig : Sigma) {struct sig} : expr_b :=
  match sig with
    | star sig1 sig2 => compute_constraints' (compute_constraint_cell_sigma pi sig2 sig1) sig1
    | _ => pi
  end.

Lemma compute_constraints'_correct : forall sig pi,
  assrt_interp (pi, sig) ===> assrt_interp (compute_constraints' pi sig, sig).

Definition compute_constraints (pi : expr_b) (sig : Sigma) : expr_b :=
  compute_constraints' pi (star_assoc_left sig emp).

Lemma compute_constraints_correct : forall pi sig,
  assrt_interp (pi,sig) ===> assrt_interp (compute_constraints pi sig, sig).

Fixpoint cell_loc_not_null (pi : expr_b) (sig : Sigma) {struct sig} : expr_b :=
  match sig with
    | emp => pi
    | lst e1 e2 => pi
    | cell e1 =>
      if expr_b_dp (pi =b> (e1 <>e nat_e 0)) then pi else
          pi &e (e1 <>e (nat_e 0))
    | singl e1 e2 =>
      if expr_b_dp (pi =b> (e1 <>e nat_e 0)) then pi else
          pi &e (e1 <>e nat_e 0)
    | star s1 s2 =>
      cell_loc_not_null (cell_loc_not_null pi s1) s2
  end.

Lemma cell_loc_not_null_correct: forall sig pi,
  assrt_interp (pi,sig) ===> assrt_interp ((cell_loc_not_null pi sig), sig).

Definition assrt_entail_fun (a1 a2 : assrt) : resul (assrt * assrt) :=
  let (pi1,sig1) := a1 in frag_entail_fun (compute_constraints (cell_loc_not_null pi1 sig1) sig1, sig1) a2.

Lemma assrt_entail_fun_correct : forall a1 a2, assrt_entail_fun a1 a2 = Good ->
  assrt_interp a1 ===> assrt_interp a2.




Fixpoint orassrt_impl_Assrt1 (a : assrt) (A : Assrt) (l:list (assrt * assrt)) {struct A} : resul (list (assrt * assrt)) :=
  match A with
    | nil => Error l
    | hd::tl =>
      match assrt_entail_fun a hd with
        | Good => Good
        | Error e => orassrt_impl_Assrt1 a tl (e :: l)
      end
  end.

This lemma prove that the rule 1 is correct

Lemma orassrt_impl_Assrt1_correct: forall A a l,
  orassrt_impl_Assrt1 a A l = Good -> assrt_interp a ===> Assrt_interp A.



Fixpoint orpi (l : list assrt) : expr_b :=
  match l with
    | nil => neg_b true_b
    | (pi, sig) :: tl => pi |e (orpi tl)
  end.


Fixpoint orassrt_impl_Assrt2 (a : assrt) (A : Assrt) (l : list (assrt * assrt)) {struct A} : resul (list (assrt * assrt)) :=
  match A with
    | nil => Error l
    | (pi, sig) :: tl =>
      match a with
        | (pi', sig') =>
          match sigma_impl (pi' &e pi) sig' sig with
            | Error (s1, s2) => Error (((pi', s1), (pi, s2)) :: l)
            | Good =>
              match tl with
                | nil => Good
                | _ => orassrt_impl_Assrt2 a tl l
              end
          end
      end
  end.

This lemma prove that the rule 2 is correct

Lemma orassrt_impl_Assrt2_correct: forall A pi sig l,
  orassrt_impl_Assrt2 (pi, sig) A l = Good ->
  forall s h,
    [ pi =b> (orpi A) ]b_s ->
    ((assrt_interp (pi,sig)) s h -> (Assrt_interp A) s h).
entry point

Definition entail_fun (a : assrt) (A : Assrt) (l : list (assrt * assrt)) : resul (list (assrt * assrt)) :=
  match a with
    | (pi, sig) =>
      if expr_b_dp (pi =b> (orpi A)) then
        match orassrt_impl_Assrt2 a A nil with
          | Good => Good
          | Error e => orassrt_impl_Assrt1 a A nil
        end
        else
          orassrt_impl_Assrt1 a A nil
  end.

Lemma entail_fun_correct: forall A a l, entail_fun a A l = Good ->
  (assrt_interp a ===> Assrt_interp A).

This function is only used by bigtoe, to provide verification of entailments

Fixpoint Assrt_entail_Assrt_dp (A1 A2 : Assrt) (l : list (assrt * assrt)) {struct A1} : resul (list (assrt * assrt)) :=
  match A1 with
    | nil => Good
    | hd :: tl =>
      match entail_fun hd A2 nil with
        | Good => Assrt_entail_Assrt_dp tl A2 l
        | Error e => Error (e ++ l)
      end
  end.

Lemma Assrt_entail_Assrt_dp_correct : forall A1 A2 l,
  Assrt_entail_Assrt_dp A1 A2 l = Good ->
  Assrt_interp A1 ===> Assrt_interp A2.