Library expr_b_dp

The goal of this decision procedure:

prove that for every environment a system of arithmetic constraint is true ==> We try to eliminate all the variables, such that to evaluate the system we do not need an environment (and thus this evaluation is the same for every environment)

Note: in fact we negate the formula of the system and find if for every environment its evaluation is false ( comes from the fact that ~ forall x, P x <-> exists x, ~ P x )

Require Import ssreflect ssrbool.
Require Import Bool_ext EqNat_ext ZArith_ext Lists_ext.
Require Import omegaz.

Local Close Scope Z_scope.
Local Close Scope positive_scope.

Require Import seplog integral_type.
Module Import seplog_Z_m := Seplog ZIT.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.assert_m.

Local Open Scope heap_scope.
Local Open Scope seplog_expr_scope.

We put a formula of expr_b into the disjunctive normal form (... /\ ...) \/ (... /\ ...) This is perform in three steps: 1) we propagate negation to final constructor 2) we translate the expr_b formula into a orlist (data-structure representing a disjunctive normal form), and we replace final (possibly negative) constructor by counter part of form >=

step 1: propagation of negation

Propagation of negation preserves the semantics of a formula

Lemma neg_propagate_preserve : forall b n s,
[ neg_propagate b n ]b_ s = [ if n then (neg_b b) else b ]b_ s.

we now prove the correctness of the function bneg_propagate. We first build the predicate is_bneg_propagate, which asserts that no connectives is under a negation

Inductive is_neg_propagate : expr_b -> Prop :=

| true_b_is_neg_propagate: is_neg_propagate true_b
| eq_b_is_neg_propagate: forall e1 e2, is_neg_propagate (e1 =e e2)
| neq_b_is_neg_propagate: forall e1 e2, is_neg_propagate (e1 <>e e2)
| ge_b_is_neg_propagate: forall e1 e2, is_neg_propagate (e1 >>= e2)
| gt_b_is_neg_propagate: forall e1 e2, is_neg_propagate (e1 >>e2)

| neg_b_is_neg_propagate: forall e, Expr_B_size e = 1 -> is_neg_propagate (neg_b e)

| and_b_is_neg_propagate: forall e1 e2,
  is_neg_propagate e1 -> is_neg_propagate e2 ->
  is_neg_propagate (e1 &e e2)
| or_is_neg_propagate: forall e1 e2,
  is_neg_propagate e1 -> is_neg_propagate e2 ->
  is_neg_propagate (e1 |e e2).

Lemma neg_propagate_correct : forall b n, is_neg_propagate (neg_propagate b n).

step 2: put in normal disjunctive form

definitions of arithmetic constraints and normal forms

Definition constraint := expr.

Definition constraint_sem (c : constraint) : expr_b := (nat_e 0) >>= c.

andlists representent conjunctions of constraints

Definition andlist := list constraint.

Fixpoint andlist_sem (l : andlist) : expr_b :=
match l with
   | nil => true_b
   | hd :: tl => (constraint_sem hd) &e (andlist_sem tl)
end.

Definition andlist_plus (c1 c2 : andlist) : andlist := c1 ++ c2.

Lemma andlist_plus_sem : forall l1 l2 s,
  [ andlist_sem (andlist_plus l1 l2) ]b_ s =
  [ (andlist_sem l1) &e (andlist_sem l2) ]b_ s.

an orlist is a disjunction of andlists

Definition orlist := list andlist.

Fixpoint orlist_sem (l : orlist) : expr_b :=
  match l with
    | nil => ~e true_b
    | hd :: tl => (andlist_sem hd) |e (orlist_sem tl)
  end.

Definition orlist_plus (d1 d2 : orlist) : orlist := d1 ++ d2.

Lemma orlist_plus_sem : forall b1 b2 s,
  [ orlist_sem (orlist_plus b1 b2) ]b_s =
  [ orlist_sem b1 ]b_s || [ orlist_sem b2 ]b_s.

Fixpoint andlist_mult_orlist (c : andlist) (d : orlist) {struct d} : orlist :=
  match d with
    | nil => nil
    | hd :: tl => orlist_plus ((andlist_plus c hd) :: nil) (andlist_mult_orlist c tl)
  end.

Lemma andlist_mult_orlist_sem: forall b2 b1 s,
  [ orlist_sem (andlist_mult_orlist b1 b2) ]b_s =
  [ andlist_sem b1 ]b_s && [ orlist_sem b2 ]b_s.

Fixpoint orlist_mult_orlist (d1 d2 : orlist) {struct d1} : orlist :=
  match d1 with
    | nil => nil
    | hd :: tl => orlist_plus (andlist_mult_orlist hd d2) (orlist_mult_orlist tl d2)
  end.

Lemma orlist_mult_orlist_sem: forall b1 b2 s,
  [ orlist_sem (orlist_mult_orlist b1 b2) ]b_ s =
  [ orlist_sem b1 ]b_s && [ orlist_sem b2 ]b_s.

the main function of step 2

Fixpoint disj_nf (b : expr_b) : orlist :=
  match b with
    | e1 &e e2 =>
      orlist_mult_orlist (disj_nf e1) (disj_nf e2)
    | e1 |e e2 =>
      orlist_plus (disj_nf e1) (disj_nf e2)
    | neg_b b1 =>
      match b1 with
        | true_b => (nat_e 1 :: nil ) :: nil
        | e1 =e e2 => ((e1 +e (nat_e 1) .-e e2) :: nil ) :: ((e2 +e (nat_e 1) .-e e1)::nil ) :: nil
        | e1 <>e e2 => ((e1 .-e e2)::(e2 .-e e1) :: nil ) :: nil
        | e1 >>= e2 => ((e1 +e (nat_e 1) .-e e2) :: nil ) :: nil
        | e1 >> e2 => ((e1 .-e e2) :: nil ) :: nil
        | _ => nil
      end
    | true_b => (nat_e 0 :: nil ) :: nil
    | e1 =e e2 => ((e1 .-e e2)::(e2 .-e e1)::nil ) :: nil
    | e1 <>e e2 => ((e1 +e (nat_e 1) .-e e2)::nil ) :: ((e2 +e (nat_e 1) .-e e1)::nil ) :: nil
    | e1 >>= e2 => ((e2 .-e e1)::nil ) :: nil
    | e1 >>e2 => ((e2 +e (nat_e 1) .-e e1)::nil ) :: nil
  end.

disj_nf preserves the semantics of neg_propagated formula

Require Import ROmega.

Lemma disj_nf_preserve : forall b, is_neg_propagate b ->
forall s, [ orlist_sem (disj_nf b) ]b_ s = [ b ]b_ s.

We compose both step in one

Definition expr_b2constraints (b : expr_b) : orlist :=
disj_nf (neg_propagate b false).

Lemma expr_b2constraints_correct: forall b s,
[ orlist_sem (expr_b2constraints b) ]b_ s = [ b ]b_ s.

Local Open Scope Z_scope.

return Some z where z is the value of the expression if this expression is variable-free, None o.w.

Fixpoint expr_compute (e : expr) : option Z :=
   match e with
     | var_e x => None
     | cst_e x => Some x
     | e1 +e e2 => match expr_compute e1 with
                     | None => None
                     | Some e1' =>
                       match expr_compute e2 with
                         | None => None
                         | Some e2' => Some (ZIT.t_plus e1' e2')
                       end
                   end
     | e1 .-e e2 => match expr_compute e1 with
                     | None => None
                     | Some e1' =>
                       match expr_compute e2 with
                         | None => None
                         | Some e2' => Some (ZIT.t_minus e1' e2')
                       end
                   end
     | e1 *e e2 => match expr_compute e1 with
                     | None =>
                       match expr_compute e2 with
                         | None => None
                         | Some e2' => if Zeq_bool e2' 0 then Some 0 else None
                       end
                     | Some e1' =>
                       if Zeq_bool e1' 0 then Some 0 else
                         match expr_compute e2 with
                           | None => None
                           | Some e2' => Some (e1' * e2')
                         end
                   end
     | _ => None
   end.

if an arithmetic expression can be evaluated without environment, this value is correct

Lemma expr_compute_correct : forall e z, expr_compute e = Some z ->
  forall s, [ e ]e_s = z.

Fixpoint simpl_expr' (e : expr) : expr :=
  match e with
    | var_e v => var_e v
    | cst_e z => cst_e z
    | e1 +e e2 =>
      match expr_compute (simpl_expr' e1) with
        | None =>
          match expr_compute (simpl_expr' e2) with
            | None => e
            | Some e2' =>
              if Zeq_bool e2' 0 then e1 else e1 +e (cst_e e2')
          end
        | Some e1' =>
          if Zeq_bool e1' 0 then
            match expr_compute (simpl_expr' e2) with
              | None => e2
              | Some e2' =>
                if Zeq_bool e2' 0 then cst_e 0 else cst_e e2'
            end
            else
              match expr_compute (simpl_expr' e2) with
                | None => (cst_e e1') +e e2
                | Some e2' =>
                  if Zeq_bool e2' 0 then cst_e e1' else cst_e (e1' + e2')
              end
      end
    | e1 .-e e2 =>
      match expr_compute (simpl_expr' e1) with
        | None =>
          match expr_compute (simpl_expr' e2) with
            | None => e
            | Some e2' =>
              if Zeq_bool e2' 0 then e1 else e1 .-e (cst_e e2')
          end
        | Some e1' =>
          if Zeq_bool e1' 0 then
            match expr_compute (simpl_expr' e2) with
                | None => (cst_e 0 .-e e2)
                | Some e2' =>
                  if Zeq_bool e2' 0 then cst_e 0 else cst_e ( - e2')
              end
            else
              match expr_compute (simpl_expr' e2) with
                | None => (cst_e e1') .-e e2
                | Some e2' =>
                  if Zeq_bool e2' 0 then cst_e e1' else cst_e (e1' - e2')
              end
      end
    | e1 *e e2 =>
      match expr_compute (simpl_expr' e1) with
        | None =>
          match expr_compute (simpl_expr' e2) with
            | None => e
            | Some e2' =>
              if Zeq_bool e2' 0 then
                cst_e 0 else
                  if Zeq_bool e2' 1 then e1 else e1 *e (cst_e e2')
          end
        | Some e1' =>
          if Zeq_bool e1' 0 then
            cst_e 0 else
              if Zeq_bool e1' 1 then
                match expr_compute (simpl_expr' e2) with
                    | None => e2
                    | Some e2' =>
                      if Zeq_bool e2' 0 then cst_e 0 else cst_e (e2')
                  end
                 else
                match expr_compute (simpl_expr' e2) with
                    | None => (cst_e e1') *e e2
                    | Some e2' =>
                      if Zeq_bool e2' 0 then
                        cst_e 0 else
                          if Zeq_bool e2' 1 then cst_e e1' else cst_e (e1' * e2')
                end
      end
    | _ => e
  end.

Lemma simpl_expr'_correct: forall e s, [ e ]e_s = [ simpl_expr' e ]e_s.

Fixpoint simpl_expr_fp (e : expr) (n : nat) {struct n} : expr :=
  match n with
    | O => e
    | S n' =>
      match e with
        | var_e v => var_e v
        | cst_e z => cst_e z
        | e1 +e e2 => simpl_expr' ((simpl_expr_fp e1 n') +e (simpl_expr_fp e2 n'))
        | e1 .-e e2 => simpl_expr' ((simpl_expr_fp e1 n') .-e (simpl_expr_fp e2 n'))
        | e1 *e e2 => simpl_expr' ((simpl_expr_fp e1 n') *e (simpl_expr_fp e2 n'))
        | _ => e
      end
  end.

Lemma simpl_expr_fp_correct: forall n e s, [ e ]e_ s = [ simpl_expr_fp e n ]e_s.

Require Import Max.

Local Open Scope nat_scope.

Fixpoint expr_depth (e : expr) : nat :=
  match e with
    | e1 +e e2 => 1 + max (expr_depth e1) (expr_depth e2)
    | e1 .-e e2 => 1 + max (expr_depth e1) (expr_depth e2)
    | e1 *e e2 => 1 + max (expr_depth e1) (expr_depth e2)
    | _ => 1
  end.

Local Close Scope nat_scope.

Definition simpl_expr (e : expr) : expr := simpl_expr_fp e (expr_depth e).

Lemma simpl_expr_correct : forall e s, [ e ]e_ s = [ simpl_expr e ]e_ s.

Fixpoint expr_fact' (e : expr) (v : nat) { struct e } : (expr * expr) :=
  match e with
    | var_e x => if beq_nat x v then (nat_e 1, nat_e 0) else (nat_e 0, var_e x)
    | cst_e x => (nat_e 0, cst_e x)
    | e1 +e e2 => match expr_fact' e1 v with
                    | (e11, e12) => match expr_fact' e2 v with
                                      | (e21, e22) => (e11 +e e21, e12 +e e22)
                                    end
                  end
    | e1 .-e e2 => match expr_fact' e1 v with
                    | (e11, e12) => match expr_fact' e2 v with
                                      | (e21, e22) => (e11 .-e e21, e12 .-e e22)
                                    end
                   end
    | e1 *e e2 => match expr_fact' e1 v with
                    | (e11, e12) => match expr_fact' e2 v with
                                     | (e21, e22) =>
                                       (((e12 *e e21) +e (e11 *e e22))
                                         +e
                                         (var_e v *e (e11 *e e21)),
                                       e12 *e e22)
                                   end
                  end
    | e1 ./e e2 => (nat_e 0, e1 ./e e2)
    | e1 mode e2 => (nat_e 0, e1 mode e2)
    | uop_e valabs_e e' => (nat_e 0, uop_e valabs_e e')
    | uop_e negate_e e' => match expr_fact' e' v with
                             | (e'1, e'2) => (nat_e O .-e e'1, cst_e 0 .-e e'2)
                           end
  end.

Lemma expr_fact'_correct : forall e v e1 e2, expr_fact' e v = (e1, e2) ->
  forall s, [ e ]e_ s = [ (var_e v *e e1) +e e2 ]e_ s.

Simplify a constraint for a given list a variables

Simplify means that it tries to replace coefficient of variables by a value (evaluation without environment)

Fixpoint simpl_varlist_constraint (c : constraint) (v : list nat) {struct v} : constraint :=
  match v with
    | nil => simpl_expr c
    | hd :: tl =>
      match expr_fact' c hd with
        | (e1, e2) =>
          simpl_expr ((simpl_expr (var_e hd *e (simpl_varlist_constraint e1 tl)))
            +e
            (simpl_expr (simpl_varlist_constraint e2 tl)))
      end
  end.

an arithmetic expression and its simplification evaluate similarly for every environment

Lemma simpl_varlist_constraint_correct: forall v c c',
simpl_varlist_constraint c v = c' -> (forall s, [ c ]e_ s = [ c' ]e_ s).

Definition simpl_constraint (c : constraint) : constraint :=
  simpl_varlist_constraint c (vars_set c).

Lemma simpl_constraint_correct: forall c s, [ c ]e_ s = [ simpl_constraint c ]e_s.

Fixpoint simpl_expr_b (b : expr_b) : expr_b :=
  match b with
    | bop_b b e1 e2 => bop_b b (simpl_constraint e1) (simpl_constraint e2)
    | bop_b2 b e1 e2 => bop_b2 b (simpl_expr_b e1) (simpl_expr_b e2)
    | neg_b e => neg_b (simpl_expr_b e)
    | _ => b
  end.

Lemma simpl_expr_b_correct: forall b s, eval_b b s = eval_b (simpl_expr_b b) s.

simplification of every constraints of an andlist

Fixpoint simpl_andlist (l : andlist) : andlist :=
  match l with
    | nil => nil
    | hd :: tl => simpl_constraint hd :: simpl_andlist tl
  end.

simplification preserves evaluation

Lemma simpl_andlist_correct: forall l s,
  eval_b (andlist_sem l) s = eval_b (andlist_sem (simpl_andlist l)) s.

Fixpoint simpl_orlist (l : orlist) : orlist :=
  match l with
    | nil => nil
    | hd :: tl => simpl_andlist hd :: simpl_orlist tl
  end.

Lemma simpl_orlist_correct: forall l s,
  eval_b (orlist_sem l) s = eval_b (orlist_sem (simpl_orlist l)) s.

Definition expr_fact (e : expr) (v : nat) : expr * expr :=
  match expr_fact' e v with
    | (e1, e2) => (simpl_constraint e1, simpl_constraint e2)
  end.

Lemma expr_fact_correct : forall c v e1 e2, expr_fact c v = (e1, e2) ->
  forall s, [ c ]e_ s = [ (var_e v *e e1) +e e2 ]e_ s.

Variable elimination: c1 and c2 are two constraints containing the variable v. By computing the coefficients of v we can compute if the variables can be eliminated (for details on the elimination mechanism see the following lemma)

Definition elim_var_constraint (c1 c2 : constraint) (v : nat) : constraint :=
  match expr_fact c1 v with
    | (e11, e12) =>
      match expr_fact c2 v with
        | (e21, e22) =>
          match expr_compute (simpl_constraint e11) with
            | None => simpl_constraint c2
            | Some e11' =>
              match expr_compute (simpl_constraint e21) with
                | None => simpl_constraint c2
                | Some e21' =>
                  if Zlt_bool e11' 0 && Zlt_bool 0 e21' then
                    simpl_constraint ((e21 *e e12) .-e (e11 *e e22))
                    else
                      (if Zlt_bool 0 e11' && Zlt_bool e21' 0 then
                        simpl_constraint ((e11 *e e22) .-e (e21 *e e12))
                        else
                          simpl_constraint c2)
              end
          end
      end
   end.

Lemma fourier_motzkin_for_integers: forall a1 b1 a2 b2 x,
  a1 < 0 -> 0 < a2 ->
  0 >= x * a1 + b1 -> 0 >= x * a2 + b2 ->
  a1 * b2 >= a2 * b1.

The two constraints allowing the variables elimination implies the constraint resulting from elimination

Lemma elim_var_constraint_correct : forall c1 c2 v s,
[ (constraint_sem c1) &e (constraint_sem c2) ]b_s ->
[ constraint_sem (elim_var_constraint c1 c2 v) ]b_s.

Given a constraint c, a list a constraint l and a variable v, we build the list l' of constraints such that it contains i) all the constraints of l where v does not appear ii) all the constraints of l where v appears but cannot be eliminated using c iii) all constraints of l where v appears and have been eliminated using c

Fixpoint elim_var_andlist' (c: constraint) (l l':andlist) (v: nat) {struct l} : andlist :=
  match l with
    | nil => l'
    | hd :: tl =>
      if inb beq_nat v (vars_set (simpl_constraint hd)) then
        elim_var_andlist' c tl (elim_var_constraint c hd v :: l') v
      else
        elim_var_andlist' c tl l' v
  end.

Lemma elim_var_andlist'_correct : forall l l' c v s,
  [ andlist_sem (c :: l ++ l') ]b_s ->
  [ andlist_sem (elim_var_andlist' c l l' v) ]b_s.

For a given variable v, find the next constraint containing v, and use it to eliminate v on the rest of the list

Fixpoint elim_var_andlist (l l' : andlist) (v : nat) {struct l} : andlist :=
  match l with
    | nil => l'
    | hd :: tl => if inb beq_nat v (vars_set (simpl_constraint hd)) then
      elim_var_andlist tl (l' ++ (elim_var_andlist' hd tl nil v)) v
      else
        elim_var_andlist tl (hd :: l') v
  end.

Lemma elim_var_andlist_correct: forall l l' v s, [ andlist_sem (andlist_plus l l') ]b_s ->
  [ andlist_sem (elim_var_andlist l l' v) ]b_s.

elimination of the variable v in the orlist

Fixpoint elim_var_orlist (l : orlist) (v : nat) {struct l} : orlist :=
   match l with
      | nil => nil
      | hd::tl => elim_var_andlist hd nil v :: elim_var_orlist tl v
   end.

Lemma elim_var_orlist_correct: forall l v s,
  eval_b (orlist_sem l) s -> eval_b (orlist_sem (elim_var_orlist l v)) s.

Elimination of a list of variables

Fixpoint elim_varlist_orlist (l : orlist) (v : list nat) {struct v} : orlist :=
  match v with
    | nil => simpl_orlist l
    | hd :: tl => elim_varlist_orlist (elim_var_orlist l hd) tl
  end.

Lemma elim_varlist_orlist_correct: forall v l s, eval_b (orlist_sem l) s ->
  eval_b (orlist_sem (elim_varlist_orlist l v)) s.

boolean evaluation of a constraint without environment

Definition eval_constraint (c : constraint) : option bool :=
   match expr_compute c with
     | Some z => Some (Zge_bool 0 z)
     | _ => None
   end.

if possible, evaluation is valid for every environment

Lemma eval_constraint2constraint_sem: forall c b,
eval_constraint c = Some b ->
forall s, eval_b (constraint_sem c) s = b.

evaluation of a not empty andlist without environment

if evaluation was possible, it holds for every environment

Lemma eval_andlist'2andlist_sem: forall a b,
eval_andlist' a = Some b ->
forall s, eval_b (andlist_sem a) s = b.

Evaluation of an andlist without environment. If empty => error !Z

Definition eval_andlist (a : andlist) : option bool :=
  if beq_nat (length a) 0 then
    None
  else
    eval_andlist' a.

if the evaluation is possible, it holds for every environment

Lemma eval_andlist2andlist_sem: forall a b, eval_andlist a = Some b ->
forall s, eval_b (andlist_sem a) s = b.

Evaluation of a non empty orlist without environment

Fixpoint eval_orlist' (o : orlist) : option bool :=
   match o with
     | nil => Some false
     | hd :: tl => orb_option (eval_andlist hd) (eval_orlist' tl)
   end.

if possible, evaluation holds for every environment

Lemma eval_orlist'2orlist_sem: forall a b,
eval_orlist' a = Some b ->
forall s, eval_b (orlist_sem a) s = b.

evaluation of an orlist without environement

Definition eval_orlist (a : orlist) : option bool :=
  if beq_nat (length a) 0 then
    None
  else
    eval_orlist' a.

if possible, evaluation holds for every environment

Lemma eval_orlist2orlist_sem: forall a b,
eval_orlist a = Some b -> (forall s, eval_b (orlist_sem a) s = b).

The algorithm: i) put the boolean expression in normal form ii) eliminate all its variables iii) evaluate without environment iv) return the negation

Definition expr_b_dp (b : expr_b) : bool :=
  match eval_orlist (elim_varlist_orlist
    (simpl_orlist (expr_b2constraints (simpl_expr_b (~e b))))
    (vars_b_set (simpl_expr_b b))) with
    | None => false
    | Some res => negb res
  end.

if the function result is true then the original expression is true for every environment

Lemma expr_b_dp_correct: forall b, expr_b_dp b -> forall s, [ b ]b_s.

FrontEnd Tactics for the expr_b_dp function

Determine if t is a Coq positive variable

Ltac Is_pos_var p :=
  match p with
    | xH => false
    | xI ?n => false
    | xO ?n => false
    | _ => true
  end.

Determine if t is a Coq Z variable

Ltac Is_Z_var t :=
  match t with
    | Z0 => false
    | Zpos ?e => Is_pos_var e
    | Zneg ?e => Is_pos_var e
    | _ => true
  end.

add an element to a list only if not already present

Ltac Add_list e l :=
  match l with
    | e :: ?tl => l
    | ?hd :: ?tl => let x := Add_list e tl in constr:(hd :: x)
    | (@nil Z) => constr:(e :: nil)
  end.

concatenate two lists without adding duplicates

Ltac Concat_list l1 l2 :=
  match l1 with
    | ?hd :: ?tl => let x:= Add_list hd l2 in Concat_list tl x
    | nil => l2
  end.

Build the list of the Coq variable inside the term t Such a list is used as an environment

Ltac Build_env t :=
  match t with
    | (?t1 + ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 - ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 * ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 = ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 -> ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 > ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 < ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 >= ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 <= ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 /\ ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 \/ ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (?t1 <> ?t2)%Z =>
      let x := Build_env t1 in let y := Build_env t2 in
      Concat_list x y
    | (~ ?t1)%Z => let x := Build_env t1 in x
    | _ => let x := Is_Z_var t in
        match eval compute in x with
          | true => constr: (t :: nil)
          | false => constr: (@nil Z)
        end
  end.

return the index of variable v in list l

Ltac Get_var_index v l := Find_var Z v l O.

translate a Coq term to an arithmetic expression using a list of variables l

Ltac To_expr t l :=
  match t with
    | (?t1 + ?t2)%Z =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (x +e y)
    | (?t1 - ?t2)%Z =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (x .-e y)
    | (?t1 * ?t2)%Z =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (x *e y)
    | _ =>
      let x:= Is_Z_var t in
        match eval compute in x with
          | true => let y := Find_var Z t l O in
                    constr: (var_e y)
          | false => constr: (cst_e t)
        end
  end.

Translate a Coq term to a boolean expression using a list of variables l

Ltac To_expr_b t l :=
  match t with
    | (?t1 = ?t2) =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (x =e y)
    | (?t1 > ?t2)%Z =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (x >> y)
    | (?t1 >= ?t2)%Z =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (x >>= y)
    | (?t1 < ?t2)%Z =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (~e (x >>= y))
    | (?t1 <= ?t2)%Z =>
      let x := To_expr t1 l in let y := To_expr t2 l in
      constr: (~e (x >> y))
    | (?t1 -> ?t2) =>
      let x := To_expr_b t1 l in let y := To_expr_b t2 l in
      constr:(x =b > y)
    | (?t1 /\ ?t2) =>
      let x := To_expr_b t1 l in let y := To_expr_b t2 l in
      constr: (x &e y)
    | (?t1 \/ ?t2) =>
      let x := To_expr_b t1 l in let y := To_expr_b t2 l in
      constr: (x |e y)
    | (?t1 <> ?t2) =>
      let x := To_expr_b t1 l in let y := To_expr_b t2 l in
      constr: (x <>e y)
    | (~ ?t1) =>
      let x := To_expr_b t1 l in constr: (~e x)
  end.

Fixpoint list2store (l : list Z) { struct l } : store.t :=
   match l with
     | nil => store.emp
     | hd::tl => store.upd (length l - 1)%nat hd (list2store tl)
   end.

Require Import bipl.

Lemma lookup_list2store : forall l x, store.get x (list2store l) = nth x (rev l) 0%Z.

Ltac Expr_b_dp_reflect :=
  match goal with
    | |- ?G =>

      let l := (Build_env G) in

      let x := (To_expr_b G l) in
      let s := constr:(list2store (rev l)) in

      cut (eval_b x s)
  end.

Ltac expr_b_dp_decision :=

Introduction of all relevant hypothesis

  match goal with
    | |- ?G =>
      let l := (Build_env G) in
      let x := (To_expr_b G l) in
      let s := constr:(list2store (rev l)) in
      cut (eval_b x s) ;

     [

       let h:= fresh in
       intro h;
       let y := fresh in
       generalize (proj1 (expr_bP x s) h); clear h; intro y; simpl in y;
       repeat (rewrite lookup_list2store in y); simpl in y; firstorder
       |
       (apply expr_b_dp_correct; vm_compute; apply refl_equal)
     ]
  end.

Ltac Reflection_is_correct :=
  match goal with
    | [ |- is_true (eval_b ?e ?s) -> ?P ] =>
       let h:= fresh in
       intro h;
       let y := fresh in
       generalize (proj1 (expr_bP e s) h); clear h; intro y; simpl in y;
       repeat (rewrite lookup_list2store in y); simpl in y; firstorder

  end.

Ltac Apply_dp := apply expr_b_dp_correct; vm_compute; reflexivity.

Lemma btest1 : forall x y : Z, x = y -> x = y.

Lemma btest2 : forall x y z res,
  (res = x /\ x >= y /\ x >= z) -> (res >= x /\ res >= y /\ res >= z).

Lemma btest3 : forall x y z res, (res = x /\ x >= y /\ x >= z) -> res >= x.

Lemma btest4 : forall x y z res, (res = x /\ x >= y /\ x >= z) -> res >= x.

Lemma btest5 : forall x y, x = 1 -> y = 1 -> x = y.

Lemma btest6 : forall z, z > 0 -> 2 * z + 1 > z.

Lemma btest7 : forall a b, (a < b \/ b < a) -> a <> b.

Lemma btest8 : forall a b c, (a > b /\ a < b) -> a=c.

Lemma btest9 : 1 <= 1.

Definition pp (n: nat) : Z := Z_of_nat n * 66.

Lemma btest10 : forall a b c, pp a > b -> b > c -> pp a > c.

Lemma btest11 : forall a b c, a >= b -> b > c -> a > c.

Lemma btest12 : forall a b c, a < b -> b < c -> a < c.

Lemma btest13 : forall a b c, a < b -> b < c -> a < c.

Module Import ZIT_prop_m := IntegralType_Prop ZIT.

Lemma btest14 : forall a b, (a + b) * (a + b) = a * a + b * b + 2 * a * b.

Lemma btest15 : forall a b, (a + b) * (a + b) = a * a + b * b + 2 * a * b.

Lemma btest16 : forall m n, 1 + 2 * m <> 2 * n.

Lemma btest17 : forall x y, 0 < x /\ y < x -> y + 1 < 2 * x.