Require Export NaiveTermAbstractions.
Require Import Kernel.
Require Import MiscUtils.
Require Import BoundedIteration.

Open Scope string_scope.

Bind Scope cond_scope with cond.
Bind Scope term_scope with term.
Delimit Scope cond_scope with cond.
Delimit Scope term_scope with term.

Infix "+" := (tbin PLUS): term_scope.
Infix "-" := (tbin MINUS): term_scope.
Infix "×" := (tbin MULT): term_scope.
Infix "/" := (tbin DIV): term_scope.
Infix "∧" := (bin AND): cond_scope.
Infix "∨" := (bin OR): cond_scope.
Infix "≤" := (Conditions.atom LE): cond_scope.
Infix "=" := (Conditions.atom EQ): cond_scope.

Open Scope cond_scope.
Open Scope term_scope.

Hint Rewrite add_in: rchecker.

Program Definition explore (targ: term) (min max: Z) (label: alabel) (subst: certif) :=
{| concrete := concrete subst;
   abstract :=
        Kseq (require (min ≤ targ ∧ targ ≤ max))
             (Kgjoin min max (fun z ⇒ Kdeflabel label z (Kseq (ensure (targ = z)) (abstract subst))));
   certif_correctness := _
|}.
Obligation 1.
  intuition.
  autorewrite with zof_value in × |-.
  case (Z_eq_dec (Zof (teval targ s)) min).
  intros; eapply certif_correctness.
  eapply H0; intuition.
  apply Zof_intro; autorewrite with zof_value; auto.
  intros; eapply certif_correctness.
  apply H0 with (z:=Zof (teval targ s)).
  omega.
  apply Zof_intro; autorewrite with zof_value; auto.
Qed.

Program Definition casescmp (t1 t2: term) (label: alabel) (p:certif) :=
{| concrete := (concrete p) ;
   abstract :=
     let p := abstract p in
     Kjoin (Kseq (ensure (t1 ≤ t2)) (Kdeflabel label 0 p))
           (Kseq (ensure (t2+1 ≤ t1)) (Kdeflabel label 1 p));
   certif_correctness := _
|}.
Obligation 1.
  case (Z_le_dec (Zof (teval t1 s)) (Zof (teval t2 s))).
  intros; lapply H; intuition eauto with checker echecker.
  intros; lapply H0; intuition eauto with checker echecker.
  autorewrite with zof_value; simpl.
  omega.
Qed.

Ltac zof_simplify := try (apply Zof_intro); autorewrite with zof_value in × |- *; simpl in × |- ×.

Ltac zof_ring_rewrite := zof_simplify; ring.

Ltac hoare_term_simplify :=
  autorewrite with rchecker; simpl; intuition; simpl in × |- *; zof_simplify.


Program Definition mult_right_cte (t1 t2:term) (c: Z) : hoare_term (t1×t2) :=
{| hname:="mult_abs_right_cte" ;
   htpre:= t2=c ;
   htpost:= fun res ⇒ res=(told t1)*c ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
Qed.

Program Definition mult_pos_low (t1 t2: term) (low:Z) : hoare_term (t1×t2) :=
{| hname:="mult_pos_low" ;
   htpre:= 0 ≤ t1 ∧ low ≤ t2 ;
   htpost:= fun res ⇒ (told t1)*low ≤ res ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
  apply Zmult_le_compat_l; auto.
Qed.

Program Definition mult_pos_up (t1 t2: term) (up:Z) : hoare_term (t1×t2) :=
{| hname:="mult_pos_up" ;
   htpre:= 0 ≤ t1 ∧ t2 ≤ up ;
   htpost:= fun res ⇒ res ≤ (told t1)*up ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
  apply Zmult_le_compat_l; auto.
Qed.

Program Definition mult_pos_interv (t1 t2: term) (lu:Z×Z) : hoare_term (t1×t2) :=
  let (low,up) := lu in
  abs_rename "mult_pos_interv"
  (abs_simplify_pre (coq_abs_conj (mult_pos_low t1 t2 low) (mult_pos_up t1 t2 up))
                    (0 ≤ t1 ∧ low ≤ t2 ∧ t2 ≤ up)).


Lemma neg_left_le (n m p q: Z):
 ( (-m × q) ≤ (-n × p))%Z → (n × p ≤ m × q)%Z.
Proof.
  rewrite <- Zopp_mult_distr_l.
  rewrite <- Zopp_mult_distr_l.
  omega.
Qed.

Program Definition mult_neg_low (t1 t2: term) (low:Z) : hoare_term (t1×t2) :=
{| hname:="mult_neg_low" ;
   htpre:= t1 ≤ 0 ∧ low ≤ t2 ;
   htpost:= fun res ⇒ res ≤ (told t1)*low ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
  apply neg_left_le.
  apply Zmult_le_compat_l; auto.
  omega.
Qed.

Program Definition mult_neg_up (t1 t2: term) (up:Z) : hoare_term (t1×t2) :=
{| hname:="mult_neg_up" ;
   htpre:= t1 ≤ 0 ∧ t2 ≤ up ;
   htpost:= fun res ⇒ (told t1)*up ≤ res ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
  apply neg_left_le.
  apply Zmult_le_compat_l; auto.
  omega.
Qed.

Program Definition mult_neg_interv (t1 t2: term) (lu:Z×Z) : hoare_term (t1×t2) :=
  let (low,up) := lu in
  abs_rename "mult_neg_interv"
  (abs_simplify_pre (coq_abs_conj (mult_neg_up t1 t2 up) (mult_neg_low t1 t2 low))
                    (t1 ≤ 0 ∧ low ≤ t2 ∧ t2 ≤ up)).


Program Definition mult_left_cte (t1 t2:term) (c: Z) : hoare_term (t1×t2) :=
{| hname:="mult_abs_left_cte" ;
   htpre:= t1=c ;
   htpost:= fun res ⇒ res=(told t2)*c ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
  rewrite Zmult_comm.
  auto.
Qed.

Program Definition mult_low_pos (t1 t2: term) (low:Z) : hoare_term (t1×t2) :=
{| hname:="mult_low_pos" ;
   htpre:= low ≤ t1 ∧ 0 ≤ t2 ;
   htpost:= fun res ⇒ (told t2)*low ≤ res ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
  rewrite Zmult_comm.
  apply Zmult_le_compat_r; auto.
Qed.

Program Definition mult_up_pos (t1 t2: term) (up:Z) : hoare_term (t1×t2) :=
{| hname:="mult_up_pos" ;
   htpre:= t1 ≤ up ∧ 0 ≤ t2 ;
   htpost:= fun res ⇒ res ≤ (told t2)*up ;
   htproof:= _
|}.
Obligation 1.
  hoare_term_simplify.
  rewrite Zmult_comm.
  apply Zmult_le_compat_l; auto.
Qed.

Program Definition mult_interv_pos (t1 t2: term) (lu:Z×Z) : hoare_term (t1×t2) :=
  let (low,up):=lu in
  abs_rename "mult_interv_pos"
  (abs_simplify_pre (coq_abs_conj (mult_low_pos t1 t2 low) (mult_up_pos t1 t2 up))
                    (low ≤ t1 ∧ t1 ≤ up ∧ 0 ≤ t2)).



Definition Zdiv_by_pos_cte (tn td: term) (d:Z): hoare_term (tn / td).
refine
{| hname:="Zdiv_by_pos" ;
   htpre:= d = td ∧ 1 ≤ td;
   htpost:= fun res ⇒ res×d ≤ (told tn) ∧ (told tn) ≤ res×d+(d-1)%Z ;
   htproof:= _
|}.
abstract (
  simpl; intros x s; autorewrite with rchecker; simpl;
  intros H; case H; clear H; intros H1 H2;
  rewrite <- H1 in × |- *; intuition; simpl in × |- *;
  autorewrite with zof_value in × |- *; simpl in × |- × ; [
  
  rewrite Zmult_comm;
  apply Z_mult_div_ge;
  omega |
  
  generalize (Zof (teval tn s)) ;
  intros a; rewrite Zmult_comm ;
  rewrite Z_div_mod_eq_full with (a:=a) (b:=d) at 1; try omega;
  apply Zplus_le_compat; try omega;
  generalize (Z_mod_lt a d) ;
  omega] ).
Defined.