Library abst

Require Import ssreflect ssrbool eqtype ssrnat.
Require Import ZArith_ext Lists_ext.
Require Import nodup.

Require Import bipl.
Require Import seplog.
Require Import integral_type.
Module seplog_Z := Seplog ZIT.

Import seplog_Z.
Import assert_m.expr_m.
Import assert_m.

Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope seplog_assert_scope.
Local Open Scope heap_scope.

Inductive cont : Type :=
| cont_seq : cmd0 -> cont -> cont
| cont_nondeter : var.v -> cont -> cont
| cont_halt : cont
| cont_abort : cont
| cont_goto : nat -> cont
| cont_branch : list expr_b -> list cont -> cont.

Notation "c ; d" := (cont_seq c d) (at level 81, right associativity) : abst_scope.
Notation "x '<-?;' c" := (cont_nondeter x c) (at level 81, right associativity) : abst_scope.
Notation "'assume' e ;; k" := (cont_branch (e::nil) (k::nil)) (at level 81, right associativity) : abst_scope.
Local Open Scope abst_scope.

Definition prog := list (nat * cont).

Variable next : Z.

Inductive ls : expr -> expr -> expr -> assert :=
| ls_nil : forall n e1 e2 s h, emp s h ->
  [ n ]e_s = 0 ->
  [ e1 ]e_s = [ e2 ]e_s ->
  ls n e1 e2 s h
| ls_cons : forall n first tail z s h h1 h2, h1 # h2 -> h = h1 +++ h2 ->
  (0 < [ n ]e_s) ->
  (first |~>_ ** first +e cst_e next |~> z) s h1 ->
  ls (n .-e cst_e 1) z tail s h2 ->
  ls n first tail s h .

Lemma ls_nil_inv : forall n e1 e2 s h, ls n e1 e2 s h ->
  [ n ]e_s = 0 ->
  h = heap.emp /\ [ e1 ]e_s = [ e2 ]e_s.

Lemma ls_cons_inv : forall n e1 e2 s h, ls n e1 e2 s h ->
  0 < [ n ]e_s -> exists h1, exists h2, exists z,
    h1 # h2 /\ h = h1 +++ h2 /\
    (e1 |~>_ ** e1 +e cst_e next |~> z) s h1 /\
    ls (n .-e cst_e 1) z e2 s h2.

Lemma ls_equiv : forall n s h e1 e2, ls n e1 e2 s h ->
  forall n' e1' e2' s',
    [ n ]e_s = [ n' ]e_s' -> [ e1 ]e_s = [ e1' ]e_s' -> [ e2 ]e_s = [ e2' ]e_s' ->
    ls n' e1' e2' s' h.

Lemma ls_app_cons : forall n1 e1 e2 s h1, ls n1 e1 e2 s h1 ->
  forall z h2, h1 # h2 ->
    (e2 |~>_ ** e2 +e cst_e next |~> z) s h2 ->
    ls (n1 +e cst_e 1) e1 z s (h1 +++ h2).

Definition NIL := cst_e 0.

Variable left right : Z.

Inductive tree : expr -> expr -> assert :=
| tree_nil : forall n r s h, emp s h ->
  [ n ]e_s = 0 -> [ r ]e_s = 0 ->
  tree n r s h
| tree_cons : forall n r s h n1 n2 lc rc h0 h1 h2,
  h0 # h1 -> h1 # h2 -> h0 # h2 -> h = h0 +++ h1 +++ h2 ->
  (0 < [ n ]e_s) ->
  [ n1 ]e_s < [ n ]e_s ->
  [ n2 ]e_s < [ n ]e_s ->
  (r |~>_ ** r +e cst_e left |~> lc ** r +e cst_e right |~> rc)%seplog_assert s h0 ->
  tree n1 lc s h1 ->
  tree n2 rc s h2 ->
  tree n r s h.

Lemma tree_equiv : forall n r s h, tree n r s h ->
  forall n' r' s', [ n ]e_s = [ n' ]e_s' -> [ r ]e_s = [ r' ]e_s' ->
    tree n' r' s' h.

Inductive expr' : Type :=
  | fvar_e : var.v -> expr'
  | bvar_e : nat -> expr'
  | cst_e' : ZIT.t -> expr'
  | bop_e' : binop_e -> expr' -> expr' -> expr'

  | uop_e' : unaop_e -> expr' -> expr'.

Notation "e1 '+e' e2" := (bop_e' add_e e1 e2) (at level 75) : abst_scope.
Notation "e1 '.-e' e2" := (bop_e' min_e e1 e2) (at level 75) : abst_scope.
Notation "e1 '*e' e2" := (bop_e' mul_e e1 e2) (at level 75) : abst_scope.
Notation "e1 './e' e2" := (bop_e' div_e e1 e2) (at level 75) : abst_scope.
Notation "e1 'mode' e2" := (bop_e' mod_e e1 e2) (at level 75) : abst_scope.
Definition field' x f := fvar_e x +e cst_e' f.
Notation "x '-.>' f " := (field' x f) (at level 75) : abst_scope.

Fixpoint expr'2expr e' : option expr :=
  match e' with
    | fvar_e x => Some (var_e x)
    | bvar_e _ => None
    | cst_e' c => Some (cst_e c)
    | bop_e' b e1' e2' =>
      match (expr'2expr e1', expr'2expr e2') with
        | (Some e1, Some e2) => Some (bop_e b e1 e2)
        | _ => None
      end

    | uop_e' u e1' => match expr'2expr e1' with
                        | Some e1 => Some (uop_e u e1)
                        | _ => None
                      end
    end.

Fixpoint inj_expr e : expr' :=
  match e with
    | var_e x => fvar_e x
    | cst_e v => cst_e' v
    | bop_e b e1 e2 => bop_e' b (inj_expr e1) (inj_expr e2)

    | uop_e u e1 => uop_e' u (inj_expr e1)
  end.

Definition closed e' :=
  match expr'2expr e' with Some _ => true | None => false end.

Lemma closed_bop_e' : forall b e1 e2, closed (bop_e' b e1 e2) -> closed e1 /\ closed e2.

Lemma closed_uop_e' : forall e u, closed (uop_e' u e) -> closed e.

Definition eval' e' s :=
  match expr'2expr e' with
    | Some e => Some (eval e s)
    | _ => None
  end.

Fixpoint expr'_eq (e1 e2 : expr') : bool :=
  match e1 with
    | fvar_e w1 =>
      match e2 with fvar_e w2 => beq_nat w1 w2 | _ => false end
    | bvar_e w1 =>
      match e2 with bvar_e w2 => beq_nat w1 w2 | _ => false end
    | cst_e' i1 =>
      match e2 with cst_e' i2 => ZIT.t_eqb i1 i2 | _ => false end
    | bop_e' bo e11 e12 =>
      match e2 with
        | bop_e' bo' e21 e22 =>
          binop_e_eq bo bo' && expr'_eq e11 e21 && expr'_eq e12 e22
        | _ => false
      end

    | uop_e' uo e11 =>
      match e2 with
        uop_e' uo' e22 => unaop_e_eq uo uo' && expr'_eq e11 e22 | _ => false
      end
  end.

Fixpoint subst_e' (e patt repl : expr') : expr' :=
  match e with
    | fvar_e w => match expr'_eq e patt with
                 | true => repl
                 | _ => e
               end
    | bvar_e w => match expr'_eq e patt with
                 | true => repl
                 | _ => e
               end
    | cst_e' i => match expr'_eq e patt with
                   | true => repl
                   | _ => e
                 end
    | bop_e' bo e1 e2 =>
      match expr'_eq e patt with
        | true => repl
        | _ => bop_e' bo (subst_e' e1 patt repl) (subst_e' e2 patt repl)
      end

    | uop_e' u e' => match expr'_eq e patt with
                       | true => repl
                       | _ => uop_e' u (subst_e' e' patt repl)
                     end
  end.

Lemma subst_e'_free : forall e i repl,
  closed e -> subst_e' e (bvar_e i) repl = e.

Fixpoint expr'_fvar_set (e : expr') : list var.v :=
  match e with
    | fvar_e x => x :: nil
    | bvar_e _ => nil
    | cst_e' z => nil
    | bop_e' _ e1 e2 =>
      Lists_ext.app_set beq_nat (expr'_fvar_set e1) (expr'_fvar_set e2)

    | uop_e' _ e' => expr'_fvar_set e'
  end.

Inductive expr_b' : Type :=
| true_b'
| bop_b' : binop_b -> expr' -> expr' -> expr_b'
| neg_b' : expr_b' -> expr_b'
| bop_b2' : binop_b2 -> expr_b' -> expr_b' -> expr_b'.

Notation "e =e e'" := (bop_b' eq_b e e') (at level 76) : abst_scope.
Notation "e <>e e'" := (bop_b' neq_b e e') (at level 76) : abst_scope.
Notation "e >>= e'" := (bop_b' ge_b e e') (at level 76) : abst_scope.
Notation "e >> e'" := (bop_b' gt_b e e') (at level 76) : abst_scope.
Notation "e &e e'" := (bop_b2' and_b e e') (at level 77) : abst_scope.
Notation "e |e e'" := (bop_b2' or_b e e') (at level 77) : abst_scope.
Notation "e << e'" := (neg_b' (bop_b' ge_b e e')) (at level 76) : abst_scope.
Notation "e <<= e'" := (neg_b' (bop_b' gt_b e e')) (at level 76) : abst_scope.
Notation "~e e" := (neg_b' e) (at level 77) : abst_scope.

Fixpoint inj_expr_b e : expr_b' :=
  match e with
    | true_b => true_b'
    | bop_b b e1 e2 => bop_b' b (inj_expr e1) (inj_expr e2)
    | neg_b e1 => neg_b' (inj_expr_b e1)
    | bop_b2 b e1 e2 => bop_b2' b (inj_expr_b e1) (inj_expr_b e2)
  end.

Fixpoint expr_b'2expr_b e' : option expr_b :=
  match e' with
    | true_b' => Some true_b
    | bop_b' b e1' e2' => match (expr'2expr e1', expr'2expr e2') with
                            | (Some e1, Some e2) => Some (bop_b b e1 e2)
                            | _ => None
                          end
    | neg_b' e1' => match expr_b'2expr_b e1' with
                      | Some e1 => Some (neg_b e1)
                      | _ => None
                    end
    | bop_b2' b e1' e2' => match (expr_b'2expr_b e1', expr_b'2expr_b e2') with
                            | (Some e1, Some e2) => Some (bop_b2 b e1 e2)
                            | _ => None
                          end
  end.

Definition closed_b (e' : expr_b') :=
  match expr_b'2expr_b e' with Some _ => true | None => false end.

Lemma closed_b_bop_b' : forall b e1 e2, closed_b (bop_b' b e1 e2) ->
  closed e1 /\ closed e2.

Definition eval_b' e' s :=
  match expr_b'2expr_b e' with
    | Some e => Some (eval_b e s)
    | _ => None
  end.

Fixpoint subst_b' (e : expr_b') (patt repl : expr') : expr_b' :=
  match e with
    | true_b' => true_b'
    | bop_b' bo f g =>
      bop_b' bo (subst_e' f patt repl) (subst_e' g patt repl)
    | bop_b2' bo f g =>
      bop_b2' bo (subst_b' f patt repl) (subst_b' g patt repl)
    | neg_b' e => neg_b' (subst_b' e patt repl)
  end.

Fixpoint expr_b'_fvar_set (e : expr_b') : list var.v :=
  match e with
    | true_b' => nil
    | bop_b' _ e1 e2 => Lists_ext.app_set beq_nat (expr'_fvar_set e1) (expr'_fvar_set e2)
    | bop_b2' _ e1 e2 => Lists_ext.app_set beq_nat (expr_b'_fvar_set e1) (expr_b'_fvar_set e2)
    | ~e e => expr_b'_fvar_set e
  end.

Inductive spatial : Type :=
| spa_mapsto : expr' -> expr' -> spatial
| spa_cell : expr' -> spatial
| spa_emp : spatial
| spa_ls : expr' -> expr' -> expr' -> spatial
| spa_tree : expr' -> expr' -> spatial.

Notation "e1 '|~>' e2" := (spa_mapsto e1 e2) (at level 77, no associativity) : abst_scope.
Notation " e '|~>_' " := (spa_cell e) (right associativity, at level 77) : abst_scope.

Definition spa_fvars (f : spatial) : list var.v :=
match f with
  | e1 |~> e2 => app_set beq_nat (expr'_fvar_set e1) (expr'_fvar_set e2)
  | e |~>_ => expr'_fvar_set e
  | spa_emp => nil
  | spa_ls e1 e2 e3 => app_set beq_nat (expr'_fvar_set e1) (app_set beq_nat (expr'_fvar_set e2) (expr'_fvar_set e3))
  | spa_tree e1 e2 => app_set beq_nat (expr'_fvar_set e1) (expr'_fvar_set e2)
end.

Definition spa_closed (f : spatial) : bool :=
  match f with
    | e1 |~> e2 => closed e1 && closed e2
    | e |~>_ => closed e
    | spa_emp => true
    | spa_ls e1 e2 e3 => closed e1 && closed e2 && closed e3
    | spa_tree e1 e2 => closed e1 && closed e2
  end.

Definition subst_spa (f : spatial) (x : nat) (e : expr') : spatial :=
  match f with
    | e1 |~> e2 => (subst_e' e1 (bvar_e x) e) |~> (subst_e' e2 (bvar_e x) e)
    | e' |~>_ => (subst_e' e' (bvar_e x) e) |~>_
    | spa_emp => spa_emp
    | spa_ls e1 e2 e3 =>
      spa_ls (subst_e' e1 (bvar_e x) e) (subst_e' e2 (bvar_e x) e) (subst_e' e3 (bvar_e x) e)
    | spa_tree e1 e2 => spa_tree (subst_e' e1 (bvar_e x) e) (subst_e' e2 (bvar_e x) e)
  end.

Inductive formula : Type :=
| for_bool : expr_b' -> formula
| for_spa : spatial -> formula
| for_con : formula -> formula -> formula
| for_and : formula -> formula -> formula
| for_or : formula -> formula -> formula
| for_exists : formula -> formula.

Notation "s ** t" := (for_con s t) (at level 80) : abst_scope.
Notation "s //\\ t" := (for_and s t) (at level 80) : abst_scope.
Notation "s \\// t" := (for_or s t) (at level 80) : abst_scope.
Local Open Scope abst_scope.

Definition spatial_interp (p : spatial) : assert :=
  match p with
    | e1' |~> e2' => fun s h =>
      match (expr'2expr e1', expr'2expr e2') with
        | (Some e1, Some e2) => (e1 |~> e2)%seplog_assert s h /\ eval e1 s <> 0%Z
        | _ => False
      end
    | e' |~>_ => fun s h =>
      match expr'2expr e' with
        | Some e => exists e2, (e |~> e2)%seplog_assert s h /\ eval e s <> 0%Z
        | _ => False
      end
    | spa_emp => assert_m.emp
    | spa_ls n' e1' e2' =>
      match (expr'2expr n', expr'2expr e1', expr'2expr e2') with
        | (Some n, Some e1, Some e2) => ls n e1 e2
        | _ => FF
      end
    | spa_tree n' r' =>
      match (expr'2expr n', expr'2expr r') with
        | (Some n, Some r) => tree n r
        | _ => FF
      end
end.

Fixpoint formula_fvars (f : formula) : list var.v :=
  match f with
    | for_bool eb => expr_b'_fvar_set eb
    | for_spa spa => spa_fvars spa
    | f1 ** f2 => app_set beq_nat (formula_fvars f1) (formula_fvars f2)
    | f1 //\\ f2 => app_set beq_nat (formula_fvars f1) (formula_fvars f2)
    | f1 \\// f2 => app_set beq_nat (formula_fvars f1) (formula_fvars f2)
    | for_exists f' => formula_fvars f'
  end.

Fixpoint formula_closed (f : formula) : bool :=
  match f with
    | for_bool eb => closed_b eb
    | for_spa spa => spa_closed spa
    | f1 ** f2 => formula_closed f1 && formula_closed f2
    | f1 //\\ f2 => formula_closed f1 && formula_closed f2
    | f1 \\// f2 => formula_closed f1 && formula_closed f2
    | for_exists _ => false
  end.

Fixpoint subst_formula (f : formula) (i : nat) (e : expr') : formula :=
  match f with
    | for_bool eb => for_bool (subst_b' eb (bvar_e i) e)
    | for_spa f' => for_spa (subst_spa f' i e)
    | f1 ** f2 => subst_formula f1 i e ** subst_formula f2 i e
    | f1 //\\ f2 => subst_formula f1 i e //\\ subst_formula f2 i e
    | f1 \\// f2 => subst_formula f1 i e \\// subst_formula f2 i e
    | for_exists f1 => for_exists (subst_formula f1 (S i) e)
  end.

Fixpoint formula_size (f : formula) : nat :=
  match f with
    | f1 ** f2 => (1 + formula_size f1 + formula_size f2)%nat
    | f1 //\\ f2 => (1 + formula_size f1 + formula_size f2)%nat
    | f1 \\// f2 => (1 + formula_size f1 + formula_size f2)%nat
    | for_exists f' => (1 + formula_size f')%nat
    | for_bool _ => O
    | for_spa _ => O
  end.

Fixpoint formula_interp' (a : formula) (n : nat) : assert :=
  match n with
    | O =>
      match a with
        | for_bool e =>
          fun s _ => match eval_b' e s with Some x => x | _ => False end
        | for_spa p => spatial_interp p
        | _ => FF
      end
    | S n' =>
      match a with
        | s1 ** s2 =>
          (formula_interp' s1 n' ** formula_interp' s2 n')%seplog_assert
        | s1 //\\ s2 =>
          (formula_interp' s1 n' //\\ formula_interp' s2 n')%seplog_assert
        | s1 \\// s2 =>
          (formula_interp' s1 n' \\// formula_interp' s2 n')%seplog_assert
        | for_exists sig =>
          fun s h => exists v, formula_interp' (subst_formula sig O (cst_e' v)) n' s h
        | for_bool e =>
          fun s _ => match eval_b' e s with Some x => x | _ => False end
        | for_spa p =>
          spatial_interp p
      end
  end.

Definition formula_interp a := formula_interp' a (formula_size a).

Lemma formula_size_subst_formula : forall f v n,
  formula_size (subst_formula f n (cst_e' v)) = formula_size f.

Lemma formula_interp'_formula_size : forall l f s h, (l >= formula_size f)%nat ->
  formula_interp' f l s h ->
  formula_interp' f (formula_size f) s h.

Lemma formula_size_subst_formula_fvar_e : forall f x n,
  formula_size (subst_formula f n (fvar_e x)) = formula_size f.

Lemma subst_e'_bvar_e : forall e v x,
  ~ In x (expr'_fvar_set e) ->
  subst_e' e (bvar_e 0) (cst_e' v) =
  subst_e' (subst_e' e (bvar_e 0) (fvar_e x)) (fvar_e x) (cst_e' v).

Fixpoint expr'_bvar_set (e : expr') : list nat :=
  match e with
    | fvar_e _ => nil
    | bvar_e x => x :: nil
    | cst_e' z => nil
    | bop_e' _ e1 e2 =>
      Lists_ext.app_set beq_nat (expr'_bvar_set e1) (expr'_bvar_set e2)

    | uop_e' _ e' => expr'_bvar_set e'
  end.

Fixpoint expr_b'_bvar_set (e : expr_b') : list nat :=
  match e with
    | true_b' => nil
    | bop_b' _ e1 e2 => Lists_ext.app_set beq_nat (expr'_bvar_set e1) (expr'_bvar_set e2)
    | bop_b2' _ e1 e2 => Lists_ext.app_set beq_nat (expr_b'_bvar_set e1) (expr_b'_bvar_set e2)
    | ~e e => expr_b'_bvar_set e
  end.

Definition spa_bvars (f : spatial) : list nat :=
match f with
  | e1 |~> e2 => app_set beq_nat (expr'_bvar_set e1) (expr'_bvar_set e2)
  | e |~>_ => expr'_bvar_set e
  | spa_emp => nil
  | spa_ls e1 e2 e3 => app_set beq_nat (expr'_bvar_set e1) (app_set beq_nat (expr'_bvar_set e2) (expr'_bvar_set e3))
  | spa_tree e1 e2 => app_set beq_nat (expr'_bvar_set e1) (expr'_bvar_set e2)
end.

Fixpoint formula_bvars (f : formula) : list nat :=
  match f with
    | for_bool eb => expr_b'_bvar_set eb
    | for_spa spa => spa_bvars spa
    | f1 ** f2 => app_set beq_nat (formula_bvars f1) (formula_bvars f2)
    | f1 //\\ f2 => app_set beq_nat (formula_bvars f1) (formula_bvars f2)
    | f1 \\// f2 => app_set beq_nat (formula_bvars f1) (formula_bvars f2)
    | for_exists f' => formula_bvars f'
  end.

Lemma eval'_None_inv : forall e s, eval' e s = None -> expr'2expr e = None.

Lemma eval'_bop_e'_inv : forall b e1 e2 s w,
  eval' (bop_e' b e1 e2) s = Some w ->
  exists v1, exists v2, eval' e1 s = Some v1 /\ eval' e2 s = Some v2.

Lemma eval'_uop_e'_inv : forall e uo w s,
  eval' (uop_e' uo e) s = Some w -> exists u, eval' e s = Some u.

Lemma eval_b'_bop_b'_inv : forall b e1 e2 s w,
  eval_b' (bop_b' b e1 e2) s = Some w ->
  exists v1, exists v2, eval' e1 s = Some v1 /\ eval' e2 s = Some v2.

Lemma eval_b'_neg_b'_inv : forall b' w s, eval_b' (~e b') s = Some w ->
  exists v, eval_b' b' s = Some v.

Lemma eval_b'_bop_b2'_inv : forall b b1 b2 s w,
  eval_b' (bop_b2' b b1 b2) s = Some w ->
  exists v1, exists v2, eval_b' b1 s = Some v1 /\ eval_b' b2 s = Some v2.

Lemma incl_expr'_bvar_set : forall e v s w,
  eval' (subst_e' e (bvar_e 0) (cst_e' v)) s = Some w ->
  incl (expr'_bvar_set e) (O :: nil).

Lemma incl_expr_b'_bvar_set : forall b v s w,
  eval_b' (subst_b' b (bvar_e 0) (cst_e' v)) s = Some w ->
  incl (expr_b'_bvar_set b) (O :: nil).

Lemma eval'_subst_e'_bvar_e_cst_e' : forall e v s x i,
  ~ In x (expr'_fvar_set e) ->
  eval' (subst_e' e (bvar_e i) (fvar_e x)) (store.upd x v s) = eval' (subst_e' e (bvar_e i) (cst_e' v)) s.

Lemma eval_b'_subst_b'_bvar_e_cst_e' : forall b v s x i,
  ~ In x (expr_b'_fvar_set b) ->
  eval_b' (subst_b' b (bvar_e i) (fvar_e x)) (store.upd x v s) = eval_b' (subst_b' b (bvar_e i) (cst_e' v)) s.

Lemma formula_interp'_subst_formula_spa : forall f s h x v i,
  ~ In x (formula_fvars (for_spa f)) ->
  formula_interp' (subst_formula (for_spa f) i (cst_e' v)) O s h ->
  formula_interp' (subst_formula (for_spa f) i (fvar_e x)) O (store.upd x v s) h.

Lemma formula_interp'_formula_size2 : forall l f s h,
  (l >= formula_size f)%nat ->
  formula_interp' f (formula_size f) s h ->
  formula_interp' f l s h.

Lemma In_expr'_fvar_set_inv : forall e x n v,
  In x (expr'_fvar_set (subst_e' e (bvar_e n) (cst_e' v))) ->
  In x (expr'_fvar_set e).

Lemma In_expr_b'_fvar_set_inv : forall e x v n,
  In x (expr_b'_fvar_set (subst_b' e (bvar_e n) (cst_e' v))) ->
  In x (expr_b'_fvar_set e).

Lemma In_spa_fvars_inv : forall f x n v,
  In x (spa_fvars (subst_spa f n (cst_e' v))) -> In x (spa_fvars f).

Lemma In_formula_fvars_subst_formula_inv : forall f x v n,
  In x (formula_fvars (subst_formula f n (cst_e' v))) ->
  In x (formula_fvars f).

Lemma subst_e'_swap : forall e i j x v,
  i <> j ->
  subst_e' (subst_e' e (bvar_e i) (fvar_e x)) (bvar_e j) (cst_e' v) =
  subst_e' (subst_e' e (bvar_e j) (cst_e' v)) (bvar_e i) (fvar_e x).

Lemma subst_b'_swap : forall e i j x v,
  i <> j ->
  subst_b' (subst_b' e (bvar_e i) (fvar_e x)) (bvar_e j) (cst_e' v) =
  subst_b' (subst_b' e (bvar_e j) (cst_e' v)) (bvar_e i) (fvar_e x).

Lemma subst_spa_swap : forall f i j x v,
  i <> j ->
  for_spa (subst_spa (subst_spa f i (fvar_e x)) j (cst_e' v)) =
  for_spa (subst_spa (subst_spa f j (cst_e' v)) i (fvar_e x)).

Lemma subst_formula_swap : forall f i j x v,
  i <> j ->
  subst_formula (subst_formula f i (fvar_e x)) j (cst_e' v) =
  subst_formula (subst_formula f j (cst_e' v)) i (fvar_e x).

Lemma subst_e'_swap2 : forall e i j x v,
  i <> j ->
  subst_e' (subst_e' e (bvar_e i) (cst_e' x)) (bvar_e j) (cst_e' v) =
  subst_e' (subst_e' e (bvar_e j) (cst_e' v)) (bvar_e i) (cst_e' x).

Lemma subst_b'_swap2 : forall e i j x v,
  i <> j ->
  subst_b' (subst_b' e (bvar_e i) (cst_e' x)) (bvar_e j) (cst_e' v) =
  subst_b' (subst_b' e (bvar_e j) (cst_e' v)) (bvar_e i) (cst_e' x).

Lemma subst_spa_swap2 : forall f i j x v, i <> j ->
  for_spa (subst_spa (subst_spa f i (cst_e' x)) j (cst_e' v)) =
  for_spa (subst_spa (subst_spa f j (cst_e' v)) i (cst_e' x)).

Lemma subst_formula_swap2 : forall f i j x v,
  i <> j ->
  subst_formula (subst_formula f i (cst_e' x)) j (cst_e' v) =
  subst_formula (subst_formula f j (cst_e' v)) i (cst_e' x).

Lemma formula_interp'_subst_formula : forall n Q,
  (formula_size Q = n)%nat ->
  forall s h x v i, ~ In x (formula_fvars Q) ->
  formula_interp' (subst_formula Q i (cst_e' v)) (formula_size Q) s h ->
  formula_interp' (subst_formula Q i (fvar_e x)) (formula_size Q) (store.upd x v s) h.

Lemma formula_interp_subst_formula : forall s h Q x v, ~ In x (formula_fvars Q) ->
  formula_interp (subst_formula Q 0 (cst_e' v)) s h ->
  formula_interp (subst_formula Q 0 (fvar_e x)) (store.upd x v s) h.

Lemma tree_unroll : forall n r,
  formula_interp (for_spa (spa_tree (fvar_e n) (fvar_e r))) ===>
  formula_interp (
    for_bool (fvar_e n =e cst_e' 0 &e fvar_e r =e cst_e' 0) \\//
    (for_bool (fvar_e n >> cst_e' 0) //\\
      for_exists (for_exists (
        for_bool (bvar_e 1 << fvar_e n &e bvar_e 0 << fvar_e n) //\\
        for_exists (for_exists (
          for_spa (fvar_e r |~>_) **
          for_spa (r -.> left |~> bvar_e 1) **
          for_spa (r -.> right |~> bvar_e 0) **
          for_spa (spa_tree (bvar_e 3) (bvar_e 1)) **
          for_spa (spa_tree (bvar_e 2) (bvar_e 0)))))))).

Definition Gamma_type := list (nat * formula).

Require OrderedTypeEx FSetList.

Module varset_m := FSetList.Make (OrderedTypeEx.Nat_as_OT).

Local Open Scope seplog_hoare_scope.

Inductive cont_hoare : formula -> cont -> formula -> Prop :=
| hoare_def : forall P c Q,
  {{ formula_interp P }} while.cmd_cmd0 c {{ formula_interp Q }} ->
  cont_hoare P (c ; cont_halt) Q.

Reserved Notation " G |- Q -| k' <| V |> k" (at level 82, no associativity).

Inductive abst : Gamma_type -> formula -> cont -> varset_m.t -> cont -> Prop :=
| abst_halt : forall G Q V,
  G |- Q -| cont_halt <| V |> cont_halt

| abst_goto : forall G l V Q,
  assoc_get l G = Some Q ->
  G |- Q -| cont_goto l <| V |> cont_goto l

| abst_command : forall G Q c k_hat V k Q',
  cont_hoare Q (c; cont_halt) Q' ->
  G |- Q' -| k_hat <| V |> k ->
  G |- Q -| c ; k_hat <| V |> c ; k
| abst_branch : forall G Q es k_hats V ks,

  length es = length k_hats -> length k_hats = length ks ->
   (forall i, (i < length ks)%nat ->
     G |- Q //\\ for_bool (inj_expr_b (nth i es true_b)) -|
       nth i k_hats cont_abort <| V |> nth i ks cont_abort) ->
   G |- Q -| cont_branch es k_hats <| V |> cont_branch es ks

| abst_inst_assign : forall G Q x e k_hat V k Q',
  varset_m.mem x V ->
  cont_hoare Q (x <- e; cont_halt) Q' ->
  abst G Q' k_hat V k ->
  G |- Q -| (x <- e; k_hat) <| V |> k

| abst_inst_assume : forall G Q eb k_hat V k,
  formula_interp Q ===> formula_interp (for_bool (inj_expr_b eb)) ->
  G |- Q -| k_hat <| V |> k ->
  G |- Q -| cont_branch (eb :: nil) (k_hat :: nil) <| V |> k

| abst_inst_exists : forall G x Q k_hat V k x' L,
  ~ In x' L ->
  varset_m.mem x V ->
  G |- subst_formula Q O (fvar_e x') -| k_hat <| V |> k ->
  G |- for_exists Q -| (x <-?; k_hat) <| V |> k

| abst_stren : forall G Q p_hat V p Q',
  formula_interp Q ===> formula_interp Q' ->
  G |- Q' -| p_hat <| V |> p ->
  G |- Q -| p_hat <| V |> p

where "G |- Q -| k' <| V |> k" := (abst G Q k' V k) : abst_scope.

Definition ls_prg x := (cont_branch
  ((var_e x <>e NIL) :: (var_e x =e NIL) :: nil)
  ((x <-* x -.> next ; cont_goto 1) :: cont_halt :: nil))%seplog_expr.

Definition instrumented_ls_prg (x n1 n2 : var.v) := (cont_branch
  ((var_e x <>e NIL) :: (var_e x =e NIL) :: nil)
  ((x <-* x -.> next ;
    n1 <- var_e n1 +e cst_e 1 ;
    n2 <- var_e n2 .-e cst_e 1 ;
    cont_goto 1) :: cont_halt :: nil))%seplog_expr.

Definition ls_Gamma_1 (x : var.v) (n1 n2 : expr') : formula :=
  for_exists
  (for_spa (spa_ls n1 (bvar_e O) (fvar_e x)) ** for_spa (spa_ls n2 (fvar_e x) (inj_expr NIL))).

Lemma example_53a : forall (x n1 n2 : var.v),
  nodup (x :: n1 :: n2 :: nil) ->
  (1%nat, ls_Gamma_1 x (fvar_e n1) (fvar_e n2)) :: nil |- ls_Gamma_1 x (fvar_e n1) (fvar_e n2) -|
    instrumented_ls_prg x n1 n2 <| varset_m.add n1 (varset_m.singleton n2) |> ls_prg x.

Fixpoint lift_expr' e :=
  match e with
    | fvar_e x => fvar_e x
    | bvar_e i => bvar_e i.+1
    | cst_e' v => cst_e' v
    | bop_e' b e1' e2' => bop_e' b (lift_expr' e1') (lift_expr' e2')
    | uop_e' a e1 => uop_e' a (lift_expr' e1)
  end.

Fixpoint lift_expr_b' eb :=
  match eb with
    | true_b' => true_b'
    | bop_b' b e1' e2' => bop_b' b (lift_expr' e1') (lift_expr' e2')
    | neg_b' e1' => neg_b' (lift_expr_b' e1')
    | bop_b2' b e1' e2' => bop_b2' b (lift_expr_b' e1') (lift_expr_b' e2')
  end.

Definition lift_spatial f :=
  match f with
    | e1 |~> e2 => (lift_expr' e1) |~> (lift_expr' e2)
    | e1 |~>_ => (lift_expr' e1) |~>_
    | spa_emp => spa_emp
    | spa_ls n e1 e2 => spa_ls (lift_expr' n) (lift_expr' e1) (lift_expr' e2)
    | spa_tree e1 e2 => spa_tree (lift_expr' e1) (lift_expr' e2)
  end.

Lemma for_exists_swap_b : forall (e : expr_b') (g : formula),
  closed_b e ->
  formula_interp (for_bool e ** for_exists g) ===>
  formula_interp (for_exists (for_bool e ** g)).

Lemma for_exists_swap_b2 : forall f g,
  closed_b f ->
  formula_interp (for_bool f ** for_exists (for_exists g)) ===>
  formula_interp (for_exists (for_exists (for_bool f ** g))).

Definition tree_prg (r : var.v) :=
  cont_branch
  ((var_e r <>e NIL) :: (var_e r =e NIL) :: nil)%seplog_expr
  (cont_branch
    (true_b :: true_b :: nil)
    ((r <-* r -.> left ; cont_goto 1) :: (r <-* r -.> right; cont_goto 1) :: nil)
    :: cont_halt :: nil)%seplog_expr.

Definition instrumented_tree_prg (r n1 n2 n : var.v) :=
  cont_branch
  ((var_e r <>e NIL) :: (var_e r =e NIL) :: nil)%seplog_expr
  ((n1 <-?; n2 <-?;
    assume (var_e n1 << var_e n &e var_e n2 << var_e n)%seplog_expr ;; cont_branch
    (true_b :: true_b :: nil)
    ((r <-* r -.> left ; n <- var_e n1; cont_goto 1) :: (r <-* r -.> right; n <- var_e n2; cont_goto 1) :: nil))
    :: cont_halt :: nil)%seplog_expr.

Definition tree_Gamma_1 (r : expr') (n : expr') : formula :=
  (for_bool true_b' ** (for_spa (spa_tree n r))).

Definition Q' (r n:var.v) (n1 n2 : expr') :=
  for_bool (fvar_e n >> cst_e' 0) //\\
  for_bool ( n1 << fvar_e n) //\\
  for_bool ( n2 << fvar_e n) //\\
  for_exists (for_exists
    ((for_spa (fvar_e r |~>_) **
      (for_spa (r -.> left |~> bvar_e 1 )) **
      (for_spa (r -.> right |~> bvar_e 0 )) **
      (for_spa (spa_tree ( (lift_expr' (lift_expr' n1))) (bvar_e 1 ))) **
      (for_spa (spa_tree ( (lift_expr' (lift_expr' n2))) (bvar_e 0 )))))).

Lemma coucou : forall x,
  formula_interp (for_bool (fvar_e x <>e cst_e' 0)) ===>
  formula_interp (for_exists (for_bool (bvar_e 0 <>e cst_e' 0))).

Definition Q (r n : var.v) :=
  for_exists (for_exists (Q' r n (bvar_e 1) (bvar_e 0))).

Lemma example_53b : forall (r n1 n2 n : var.v),
  nodup (r :: n1 :: n2 :: n :: nil) ->
  (1%nat, tree_Gamma_1 (fvar_e r) (fvar_e n)) :: nil |- tree_Gamma_1 (fvar_e r) (fvar_e n) -|
    instrumented_tree_prg r n1 n2 n <| varset_m.add n (varset_m.add n1 (varset_m.singleton n2)) |> tree_prg r.